arxiv: 2602.13100 · v2 · submitted 2026-02-13 · 💻 cs.FL · cs.DS

Recognition: 2 theorem links

· Lean Theorem

Out-of-Order Membership in Regular Languages

Antoine Amarilli , Sebastien Labbe , Charles Paperman

Authors on Pith no claims yet

Pith reviewed 2026-05-15 22:39 UTC · model grok-4.3

classification 💻 cs.FL cs.DS

keywords out-of-order evaluationregular languagesspace complexityfinite monoidssemigroupsstreaming algorithmsmembership testing

0 comments

The pith

Out-of-order monoid product evaluation requires constant space for commutative monoids, O(log n) for one subclass, and linear space for all others.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies membership testing for regular languages when the symbols of an input word arrive in arbitrary order, with each position index given exactly once and the total length known ahead of time. It reduces the problem to out-of-order evaluation of a fixed finite monoid or semigroup, which requires computing the ordered product from elements presented out of sequence. For monoids the authors establish a precise trichotomy on space complexity as a function of input length n: constant space suffices exactly when the monoid is commutative, a specific non-commutative class admits an O(log n) algorithm, and every remaining monoid demands linear space. The same algebraic lens yields a coarser classification for semigroups, separating those that admit constant space from those that require at least logarithmic space. All cases remain solvable with linear space and constant time per incoming symbol.

Core claim

For any fixed finite monoid, out-of-order evaluation of the product can be performed with space complexity Θ(1) precisely when the monoid is commutative, with space O(log n) for a particular non-commutative subclass, and with space Θ(n) for every other monoid; for semigroups a class admitting constant space is characterized while all others require at least Ω(log n) space.

What carries the argument

The algebraic structure of the target monoid or semigroup, which determines how much state must be retained to track the running product without knowing the arrival order of factors.

Load-bearing premise

The length n of the input is known in advance and the stream contains each position index exactly once.

What would settle it

An explicit non-commutative monoid that admits a deterministic constant-space out-of-order evaluation algorithm would contradict the claimed separation between constant-space and higher-space cases.

read the original abstract

We introduce the task of out-of-order membership to a formal language L, where the letters of a word w are revealed one by one in an adversarial order. The length |w| is known in advance, but the content of w is streamed as pairs (i, w[i]), received exactly once for each position i, in arbitrary order. We study efficient algorithms for this task when L is regular, seeking tight complexity bounds as a function of |w| for a fixed target language. Most of our results apply to an algebraically defined variant dubbed out-of-order evaluation: this problem is defined for a fixed finite monoid or semigroup S, and our goal is to compute the ordered product of the streamed elements of w. We show that, for any fixed regular language or finite semigroup, both problems can be solved in constant time per streamed symbol and in linear space. However, the precise space complexity strongly depends on the algebraic structure of the target language or evaluation semigroup. Our main contributions are therefore to show (deterministic) space complexity characterizations, which we do for out-of-order evaluation of monoids and semigroups. For monoids, we establish a trichotomy: the space complexity is either {\Theta}(1), {\Theta}(log n), or {\Theta}(n), where n = |w|. More specifically, the problem admits a constant-space solution for commutative monoids, while all non-commutative monoids require {\Omega}(log n) space. We further identify a class of monoids admitting an O(log n)-space algorithm, and show that all remaining monoids require {\Omega}(n) space. For general semigroups, the situation is more intricate. We characterize a class of semigroups admitting constant-space algorithms for out-of-order evaluation, and show that semigroups outside this class require at least {\Omega}(log n) space.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a clean algebraic trichotomy for space complexity in out-of-order monoid and semigroup evaluation.

read the letter

The main point is that out-of-order membership for regular languages reduces to evaluating products over a fixed monoid or semigroup, and the space needed splits neatly by algebraic properties. For monoids the bounds are constant space exactly when the monoid is commutative, O(log n) for one identified subclass, and linear space for everything else; semigroups get a constant-space class and otherwise at least log n. That is the actual new piece: the problem variant itself plus the explicit trichotomy tied to commutativity and related structure. The work does well by keeping the model explicit (known length, each index appears once) and by deriving the bounds from standard monoid theory without introducing new parameters or circular definitions. The constant-space cases feel natural and the lower bounds look tight from the abstract. The soft spot is that the precise O(log n) monoid subclass is only named, not described in detail here, so it is hard to judge how broad or artificial it is without the full text. The semigroup side is acknowledged as more intricate, which is honest but leaves the characterization less complete. Proofs are not visible, so any edge-case handling in the derivations remains unchecked, though nothing in the stated claims suggests a gap. This is for people working on streaming automata or algebraic complexity who want tight classifications rather than general algorithms. It is worth a serious referee because the results are precise, the model is well-defined, and the algebraic link is direct.

Referee Report

2 major / 3 minor

Summary. The paper introduces out-of-order membership testing for regular languages and the related out-of-order evaluation problem over finite monoids and semigroups. Inputs arrive as (index, symbol) pairs in arbitrary order with known length n and each index appearing exactly once; the goal is to decide membership or compute the ordered product. The authors give constant-time-per-symbol algorithms using linear space in all cases and prove tight space characterizations: monoids admit a trichotomy of Θ(1) (exactly the commutative ones), Θ(log n) (an identified subclass), or Θ(n) (the remainder), while semigroups admit constant space precisely for a certain algebraic class and require Ω(log n) otherwise.

Significance. If the characterizations hold, the work supplies a clean algebraic classification of space complexity for streaming product computation, directly linking constant space to commutativity and isolating the precise boundary between logarithmic and linear space. This strengthens the bridge between automata theory and streaming models and yields falsifiable predictions about which monoids/semigroups permit sublinear space.

major comments (2)

[§4] §4 (Monoid trichotomy): the Ω(log n) lower bound for all non-commutative monoids is load-bearing for the claimed separation; the reduction or adversary argument must be checked to ensure it does not inadvertently rely on the monoid being outside the O(log n) subclass identified later in the same section.
[Theorem 5.3] Theorem 5.3 (semigroup constant-space class): the algebraic characterization of the constant-space semigroups is central; the proof should explicitly verify that the class is closed under the relevant operations and that the constant-space algorithm correctly reconstructs the ordered product without using the known length n beyond indexing.

minor comments (3)

[§2] The preliminaries should include a short table comparing the standard streaming model with the out-of-order model to highlight the exact differences in input presentation.
[§3] Notation for the streamed product (e.g., the symbol used for the out-of-order multiplication) is introduced late; moving the definition to the first paragraph of §3 would improve readability.
[Figure 2] Figure 2 (space-complexity diagram for monoids) uses shading that is hard to distinguish in grayscale; adding pattern fills or explicit labels would help.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment and constructive comments on our manuscript. We address the two major comments point by point below. Both points can be resolved by adding clarifying text and explicit verifications; we will incorporate these changes in the revised version.

read point-by-point responses

Referee: [§4] §4 (Monoid trichotomy): the Ω(log n) lower bound for all non-commutative monoids is load-bearing for the claimed separation; the reduction or adversary argument must be checked to ensure it does not inadvertently rely on the monoid being outside the O(log n) subclass identified later in the same section.

Authors: We have re-examined the Ω(log n) lower-bound argument in Section 4. The proof relies exclusively on the existence of a pair of non-commuting elements a, b (i.e., ab ≠ ba) and constructs an adversary that forces the algorithm to distinguish sufficiently many possible interleavings of these elements. This construction uses only the non-commutativity assumption and does not invoke any additional algebraic properties that would exclude the monoid from the O(log n) subclass defined later in the section. The O(log n) subclass is characterized by further conditions (allowing a compact representation of the necessary ordering information), but the lower bound applies uniformly to every non-commutative monoid. We will insert a short clarifying paragraph immediately after the lower-bound statement to emphasize this independence. revision: yes
Referee: [Theorem 5.3] Theorem 5.3 (semigroup constant-space class): the algebraic characterization of the constant-space semigroups is central; the proof should explicitly verify that the class is closed under the relevant operations and that the constant-space algorithm correctly reconstructs the ordered product without using the known length n beyond indexing.

Authors: We agree that these points deserve explicit treatment. In the revised proof of Theorem 5.3 we will add a dedicated paragraph establishing closure of the class under direct products and subsemigroups. We will also clarify the algorithm’s use of n: the known length is used only to allocate a fixed-size array that records each incoming symbol in its correct position; once the symbols are placed, the ordered product is computed solely from the algebraic properties of the class (controlled commutation of certain elements) without any further dependence on the numerical value of n. This separation ensures the algorithm remains constant-space as claimed. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The derivation relies on standard algebraic automata theory applied to the explicitly defined out-of-order evaluation problem (known n, each index appears once). The trichotomy for monoids follows from algebraic distinctions (commutativity, specific subclasses) without any quantity being defined in terms of the target space bound or any prediction reducing to a fitted input by construction. No load-bearing self-citations or ansatzes are invoked; the model assumptions are stated upfront as part of the problem rather than smuggled in. The results are therefore self-contained against external algebraic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The characterizations rely on the standard correspondence between regular languages and finite monoids together with basic facts about semigroup multiplication.

axioms (2)

standard math Every regular language is recognized by a finite monoid via the syntactic monoid construction
Invoked implicitly when the paper reduces membership to monoid product evaluation
standard math Multiplication in a finite semigroup is associative
Used to guarantee that the final product is independent of arrival order

pith-pipeline@v0.9.0 · 5648 in / 1234 out tokens · 46045 ms · 2026-05-15T22:39:06.826010+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat ≃ Nat recovery; embed_strictMono_of_one_lt unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

For monoids, we establish a trichotomy: the space complexity is either Θ(1), Θ(log n), or Θ(n)... constant-space solution for commutative monoids... FL∨Com... all remaining monoids require Ω(n) space.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel; dAlembert_to_ODE_general unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

The variety FL∨Com... equation (xa)ω sxtu (xb)ω = (xa)ω stxu (xb)ω

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.