Algebraic Decomposition Theory for Transformer Length Generalization

Published as a conference paper at COLM 2026

Algebraic Decomposition Theory for Transformer Length Generalization Andy Yang1∗

Blerta Veseli2 ∗ Corentin Barloy3

Andreas Krebs5

Charles Paperman6

Michaël Cadilhac4

Howard Straubing7

Michael Hahn2

1 University of Notre Dame, 2 Saarland University, 3 Ruhr University Bochum 4 DePaul University, 5 University of Tübingen, 6 University of Lille, 7 Boston College

arXiv:2608.13433v1 [cs.FL] 13 Aug 2026

Abstract Transformer-based language models are known to sometimes generalize to sequences longer than seen during training, but we lack a precise characterization of which tasks admit length generalization. It is not even known which regular languages transformers length-generalize on – and this is a foundational class of languages. Our contributions are to establish the first complete characterization of which regular languages transformers length-generalize on and provide a decision algorithm running in polynomial time in the size of the language’s syntactic monoid. These results rely on an effective characterization of the regular languages in C-RASP, a recently-established formalism that expresses which languages transformers length-generalize on. This characterization is challenging because classical tools like Krohn-Rhodes decomposition theory for finite semigroups are insufficient for C-RASP. Firstly, the basic building blocks of Krohn-Rhodes theory – flip-flop and simple groups – are not expressible in C-RASP. Secondly, the basic building block of C-RASP (unbounded counting) is not expressible by the finite semigroups of Krohn-Rhodes theory. Thus, length generalization on regular languages is controlled by an algebraic property that is invisible to classical finite decomposition theory. We generalize classical decomposition theory from finite semigroups to the infinite additive group on the integers, allowing us to characterize C-RASP in terms of iterated wreath products of the integers and derive a provable polynomial-time decision algorithm for regular language membership. Experiments across a broad test suite of regular languages confirm that our theory captures transformers’ length-generalization behavior more accurately than existing classifications.1

1

Introduction

What state-tracking capabilities do transformer language models possess? To answer this question we study the regular languages on which transformers can length-generalize. First, regular languages give us a formal framework to describe the structure of state-tracking algorithms that transformers can implement. Second, probing for length-generalization gives us an empirical confirmation that the transformer learns an implementation of the underlying algorithm. Even though this is a fundamental question about an important architecture, we still lack a precise answer. For instance as shown in fig. 1, two structurally similar state-tracking tasks (recognizing ( ab + bbaa)∗ and ( ab + aabb)∗ ) may diverge sharply in terms of length-generalizability – and all existing theory fails to explain this discrepancy. This line of inquiry has a deep history in machine learning. In fact, Kleene (1956) invented regular expressions specifically for the purpose of analyzing the capabilities of McCulloch∗ AY and BV are co-first authors. Contact: ayang4@nd.edu,{blerta.veseli,mhahn}@uni-saarland.de 1 Code available at GitHub repository.

1

Published as a conference paper at COLM 2026

b

a a

b

100

a

b

75

75

b

50

50

25

b

a

0

100

25 [lmin ,50]

[51,100]

a

[101,150]

b

0

[lmin ,50]

[51,100]

[101,150]

Figure 1: DFAs for ( ab + bbaa)∗ and ( ab + aabb)∗ and transformer length generalization on both. Transformers were trained on strings of length [lmin , 50], where lmin denotes the length of the shortest valid string in the respective language, and the tested on a held-out sets of strings from bins of length up to 150. Existing theory fails to explain why lengthgeneralization differs between these simple regular languages with very similar structure.

Pitts neural networks. Regular language recognition is a fundamental task in the theory of computation that provides us a systematic method of determining the sequence-processing capabilities of a model (Sipser, 1996). The task is simple: given a sequence of inputs, each of which triggers a transition in a deterministic finite automaton (DFA), track the state of the machine after each transition. These finite state-tracking tasks arise concretely in the context of language models, which we sketch below. Constrained decoding: A user may want a language model to generate text in a structured format, such as JSON or code, which can pose challenges (Schall & de Melo, 2025). Even as outputs grow in length, their structured formats often follow regular constraints (e.g. matching curly braces to a fixed depth in JSON). Agentic workflows: AI agents in practice follow workflows consisting of compositional sequences of actions (Schluntz & Zhang, 2024). Keeping track of the state of the environment and deciding the next action to take can then explicitly be seen as simulating a DFA. Natural language: Morphemes in natural languages typically follow constraints that can be modeled by regular languages (Kaplan & Kay, 1994). Natural language semantics also involves maintaining the states of different referents over time (Kim & Schuster, 2023). Previous work provides a theoretical foundation for our study by providing characterizations of which regular languages can be expressed by the transformer architecture. Liu et al. (2023b); Merrill & Sabharwal (2025) showed transformers with log(n) depth could express all regular languages, while constant depth transformers could express all solvable regular languages. The containment of poly(n)-precision transformers within TC0 suggests transformers cannot express non-solvable regular languages (assuming TC0 ̸= NC1 , as is common) (Merrill & Sabharwal, 2023; Chiang, 2025). Hahn (2020) showed that hard attention transformers recognized only languages in AC0 , which Yang et al. (2024) later refined to the star-free regular languages, and Jerad et al. (2025) finally refined to the Rtrivial languages (when using leftmost tie breaking). Similarly, Li et al. (2024) showed that finite-precision transformers recognized only star-free languages, which Li & Cotterell (2025) refined to the R-trivial languages. In contrast, Bhattamishra et al. (2020); Huang et al. (2025) showed that transformers can learn languages both in and outside of each class discussed above, implying that existing expressivity characterizations do not account for transformer length generalization on regular languages. In particular, strong empirical evidence show that transformers tend to lengthgeneralize on and only on the languages expressible in C-RASP, a programming language defining a subclass of the languages expressible by a transformer (Huang et al., 2025; Jobanputra et al., 2025; Yang et al., 2025; Yang & Chiang, 2024). However, prior to this work, there did not exist a complete characterization of the regular languages in C-RASP. Formal language theory has a vibrant tradition of producing beautiful characterizations of regular language membership for different classes. For instance, Barrington et al. (1992) 2

Published as a conference paper at COLM 2026

REG A Rω C-RASP

A

C-RASP

wpc(Dy) R

C-RASP

TC0

B1 B0

AC0

(a) regular and subregular

.. .

(b) circuits

(c) dot depth hierarchy

Figure 2: C-RASP is situated orthogonal to well-known classes of languages. C-RASP contains all R-trivial languages but not all star-free ones (fig. 2a). C-RASP is contained in TC0 , but incomparable to AC0 (fig. 2b). C-RASP intersects every level of the dot depth hierarchy, while remaining incomparable to the full hierarchy (fig. 2c). showed that a regular language is in AC0 if and only if its syntactic morphism is quasiaperiodic, thus providing a decision procedure. Simon (1975) showed that a language is piece-wise testable iff its syntactic monoid is J-trivial. On the frontier, regular language membership in TC0 is equivalent to the 40 year old open problem of whether or not TC0 ̸= NC1 (Barrington, 1989), and regular language membership in all levels of the dot-depth hierarchy is a 50 year old open problem (Pin, 2017). Our work follows in this tradition, tackling the same question in the case of C-RASP. This is a deep and challenging theoretical question because classical tools for characterizing regular languages – namely the Krohn-Rhodes decomposition theory of Krohn & Rhodes (1965) – are insufficient for C-RASP. On one front, the building blocks of Krohn-Rhodes theory (flip-flop units and simple groups) are not expressible in C-RASP (Huang et al., 2025). On a second front, the basic building blocks of C-RASP (unbounded counting units) are not expressible by the finite semigroups of Krohn-Rhodes theory. Our core innovation is to develop an analogous algebraic decomposition theory for transformers using the additive group on the integers. We effectively characterize the regular languages in C-RASP, and provide a polynomial-time algorithm that decides DFA membership in C-RASP. A simpler necessary (but not sufficient) criterion is proven via a profinite equation. Finally, we validate empirically that regular language membership in C-RASP predicts transformer length-generalization better than any existing characterization.

2

Algebraic Preliminaries

Our characterization of the regular languages that languages transformers length-generalize on (i.e. those in C-RASP) builds upon the algebraic theory of formal languages (Pin, 2025). 2.1

Basics: Algebraic Theory of Formal Languages

We refer to section C for additional definitions. The essential ones are presented here. Definition 1 (Monoid). A monoid ( M, ·, 1) is a set M with an associative binary operation and an identity element. We will just write M when the operation and identity are clear. A finite monoid M together with a homomorphism ϕ : Σ∗ → M behaves like a finite automaton: after reading string w = w1 · · · wn , the automaton is in state ϕ(w1 ) · · · ϕ(wn ). Like a finite automaton, a monoid M recognizes a language L if there exists an accepting subset X ⊆ M and a homomorphism ϕ : Σ∗ → M such that L = ϕ−1 ( X ). Two monoids will serve as basic units for us (the latter is the “flip-flop” alluded to above). Definition 2. The monoid U1 is the set {0, 1} where 0 · 1 = 1 · 0 = 0 · 0 = 0 and 1 · 1 = 1. The monoid U2 is the set {1, a, b} where x · a = a, x · b = b, and 1 · x = x = x · 1 for any x ∈ U2 . As an example, consider L = Σ∗ aΣ∗ and the homomorphism ϕ : Σ∗ → U1 where ϕ(σ ) = 0 iff σ = a. Then for any w ∈ Σ∗ we have that ϕ(w) = 0 ∈ U1 iff in w ∈ L. In some sense, U1 3

Published as a conference paper at COLM 2026

captures the structure of L (i.e. it detects if a ever occurs in the string). In fact, any monoid recognizing L is divided by U1 , in the following sense: Definition 3 (Division). A monoid M divides a monoid N iff there is a submonoid T of N and homomorphism ϕ : T → M such that M = ϕ( T ). Division is transitive. For a language L, the syntactic monoid M ( L) is the unique monoid which recognizes L and divides all other M that also recognize L. In the example above, U1 is the syntactic monoid of L = Σ∗ aΣ∗ . We will consider classes of monoids that enjoy closure properties that will be useful for effective characterizations. Definition 4 (Pseudovariety). A pseudovariety of monoids is a collection of monoids closed under division and finite direct products. Some pseudovarieties relevant to our characterization are R (the R-trivial monoids (Brzozowski & Fich, 1980), A (the aperiodic monoids (Schützenberger, 1965)), REG (all regular languages), and Dy (the pseudovariety generated by all bounded Dyck monoids). 2.2

Background: Classical Algebraic Decomposition Theory of Regular Languages

The classical algebraic operation for composing monoids is the wreath product. Here we will sometimes use + to notate the monoid multiplication to decongest the notation, but we do not intend to suggest it is commutative. Definition 5 (Classical Wreath Product). The wreath product M ◦ N of finite monoids ( M, +) and ( N, ·) is the monoid M N × N with multiplication given by ( f 1 , n1 )( f 2 , n2 ) = ( f 1 + n1 f 2 , n1 n2 ), where the left action n f is given by n f (n′ ) = f (n′ n). The wreath product M ◦ N together with a homomorphism ϕ : Σ∗ → M ◦ N behaves like the composition of a finite automaton and a finite transducer. Let ϕ M and ϕN be such that ϕ( a) = (ϕ M ( a), ϕN ( a)) for all a ∈ Σ. After reading a prefix w1 · · · wt , the automaton is in state qt = ϕN (w1 ) · · · ϕN (wt ), and the transducer is in state ϕ M (w1 )(q0 ) + ϕ M (w2 )(q1 ) + ϕ M (w3 )(q2 ) + . . . + ϕ M (wt)(qt−1 ). Wreath products are the backbone of the fundamental result in the decomposition theory of finite monoids, the Krohn-Rhodes Theorem: Theorem 6 (Krohn-Rhodes Theorem (Krohn & Rhodes, 1965)). Every finite monoid M divides an iterated wreath product of U2 and simple groups G that divide M. Unfortunately, Krohn-Rhodes theory is insufficient for handling the monoids involved in transformer length-generalization. C-RASP defines languages with infinite syntactic monoids (Krohn-Rhodes only applies to finite monoids), while U2 is not definable in C-RASP (Huang et al., 2025) (the Krohn-Rhodes flip-flop unit is useless for C-RASP). The essential monoid for us will be the syntactic monoid of the bounded Dyck monoid, which can be defined in C-RASP. Definition 7 (Bounded depth Dyck language). Define D1 := ( ab)∗ and Dk+1 := ( aDk b)∗ . In short: transformers simultaneously succeed at length-generalizing on languages beyond the scope of Krohn-Rhodes theory (Bhattamishra et al., 2020), and fail to length generalize on the fundamental units in scope of Krohn-Rhodes theory (Liu et al., 2023a). This necessitates a new decomposition theory to handle C-RASP.

3

Algebraic Characterization of C-RASP

Huang et al. (2025) showed that transformer length-generalization can be guaranteed for all languages in C-RASP, and strong empirical evidence suggests failure of lengthgeneralization outside of C-RASP (Jobanputra et al., 2025). Furthermore, a form of fixedprecision transformer is equivalent to C-RASP (Yang et al., 2025). In this section we develop an algebraic characterization of C-RASP, which crucially requires moving beyond KrohnRhodes theory to infinite monoids. We refer to Yang & Chiang (2024); Huang et al. (2025) for an exposition of C-RASP and provide a formal definition in section F. 4

Published as a conference paper at COLM 2026

3.1

Typed Monoids

Krebs (2008) developed a framework for using infinite monoids to recognize languages. We present a restriction of the aforementioned framework to the case of wreath products (a one-sided version of the block product used in previous work), which ultimately provides an exact algebraic characterization of C-RASP. The core issue here is that the wreath product of infinite monoids can generate uncountably many elements, which can be too powerful. Proposition 8. Consider the classic wreath product Z◦Z. Then M ( L) ⪯ Z◦Z for every L. Proof. Without loss of generality let Σ = {0, 1}. Consider the submonoid of Z◦Z generated by the image of Σ∗ under the homomorphism σ 7→ ( f σ , 1) where f σ ( x ) = σ · 2| x| . In essence, this creates a mapping w 7→ ( f w , |w|) where f w (0) outputs the integer value of the binary number w. Thus, Z◦Z can recognize arbitrary languages. This problem motivates the definition of typed monoids, which restricts the accepting sets to be collection of sets closed under union, intersection and complement. Definition 9. A typed monoid is a triple ( M, T M , EM ) where M is a finitely generated monoid, T M is a finite Boolean algebra over M, and EM is a finite subset of M. Elements of T M are the types and elements of EM are the units. A language L is recognized by ( M, T M , EM ) if there exists a homomorphism h : Σ∗ → M such that h(Σ) ⊆ EM and L = h−1 (M) for some M ∈ T M . As an example, the language MAJORITY (there are more a’s than b’s) is recognized by the typed monoid (Z, {(−∞, 0], [1, ∞), Z, ∅}, {−1, 1}) via the type [1, ∞) and the homomorphism a 7→ 1 and b 7→ −1. We will typically refer to this typed monoid as Z. Now the typed wreath product follows the same intuition as the classical wreath product, except the computations are restricted so as not to have more distinguishing power than provided by the types. Definition 10 (Typed Wreath Product). Let ( M, T M , EM ), ( N, T N , EN ) be two typed monoids, and let C ⊆ N be a finite set. The typed wreath product

(U, TU , EU ) = ( M, T M , EM )◦· C ( N, T N , EN ) of ( M, T M , EM ) with ( N, T N , EN ) using constants C is defined such that • EU consists of elements ( f , n), where n ∈ EN , and f : N → EM is a type respecting function (see definition 32) with respect to ( N, T N , EN ) and C • U is the submonoid of M ◦ N generated by EU • TU consists of types UM,N = {( f , n) | f (1 N ) ∈ M, n ∈ N}, where M ∈ T M , N ∈ T N Multiplication is the same as in the classical wreath product. 3.2

Wreath Product Characterization

With the notion of typed monoids in hand, we can give an algebraic characterization of C-RASP. Let wpc( M, T M , EM ) denote the wreath product closure of a typed monoid, which closes iterated wreath products of this monoid under Boolean combinations and other basic operations. The precise definition will be found in section E.2. The typed wreath product closure turns out to be the precise algebraic “glue” that connects integer counting to C-RASP programs. The proof is given in section F.4. Theorem 11. L ∈ C-RASP ⇐⇒ M ( L) ∈ wpc(Z)

4

Decomposition Theory for Regular Languages in C-RASP

So far, we have characterized C-RASP in terms of iterated wreath products of Z. We will turn this into an algebraic decision algorithm: given a regular language L, we determine if M ( L) divides a wreath product of Z (or not). A priori, such a question is a formidable problem, due to multiple challenges: Z is infinite, and we do not even know how many Z factors are needed. In fact, there even examples in the finite case where the problem 5

Published as a conference paper at COLM 2026

ends up undecidable (Rhodes, 1999). Our second main result will be that, using a detailed understanding of wreath products of Z, this problem is decidable. In the depth-1 case, it is easy to check if M ( L) divides Z (this is true e.g. for the AND language, L = 1∗ ). How would we check if M ( L) ≺ Z◦Z? If we could “divide” out the right factor to obtain an object “M ( L)/Z”, we could check if “M ( L)/Z′′ ≺ Z. If this is not the case, we could “divide” by Z again, and iterate until we either reach division of Z (i.e., L is in C-RASP), or a fixed point (i.e., L is not in C-RASP). This is the basic idea of our decision procedure. There are three challenges at hand: First, understanding how to “divide” by a wreath product factor; second, making this computable even though Z is infinite; third, understanding how to identify the fixed point. 4.1

Categories

What do you get when you “divide” one monoid by another? For this first challenge, there is a well-understood technique using categories as algebraic structures (Tilson, 1987). We informally present the main idea, but defer the precise definitions to section G. In group theory, this question has a simple answer. With a surjective group homomorphism between groups ϕ : G → H, we can “divide” G by ker ϕ with a “quotient” of H, such that G ⪯ (ker ϕ)◦ H. However, since we are dealing with monoids (and C-RASP does not even contain any non-trivial finite groups), this is of no use for us. For monoid homomorphisms ϕ : M → N, we may not be able to “divide” M by ker ϕ, as monoids’ lack of inverses obstructs such a clean division. What is the divisor in the division ϕ : M(D1 ) → U2 ? Intuitively, the wreath product M (D1 ) ⪯ N ◦U2 should form a structure that contains elements (last symbol = a) and (last symbol = b). However, composition in this structure will be highly restricted – e.g. (this symbol = b)(last symbol = a) is an illegal composition. It turns out the cleanest way to handle this is by lifting monoids and homomorphisms to higher order structures – categories and relational morphisms . A category X consists of a set of objects Obj( X ) and hom-sets X ( x1 , x2 ), which are collections of arrows α : x1 → x2 for each pair of objects x1 , x2 ∈ X. Arrows can compose associatively, and each object has an identity arrow. A relational morphism of monoids ϕ : M ◁ N is a relation where ϕ(m) ̸= ∅, ϕ(m1 )ϕ(m2 ) ⊆ ϕ(m1 m2 ), and 1 N ∈ ϕ(1 M ). This is a generalization of the classical morphism, where elements may map to sets of elements. Now for any relational morphism of monoids ϕ : M◁ N, the correct notion of divisor turns out to be the derived category Dϕ . Here, Obj( Dϕ ) = ϕ( M ) and Dϕ (n1 , n2 ) = {n1 →(m,n) | n ∈ ϕ(m), n1 n = n2 }. Arrows compose via the rule n0 →(m1 ,n1 ) n0 n1 →(m2 ,n2 ) = n0 →(m1 m2 ,n1 n2 ) , and we merge arrows that have the same behavior under composition. The Derived Category Theorem (Tilson, 1987) states that given a relational morphism ϕ : M ◁ N, and a division Dϕ ⪯ V, we obtain a division M ⪯ V ◦ N. Thus, if ϕ : M ◁Z, then Dϕ formalizes the object “M/Z” alluded to in the previous section. Going forward, we work with an extension of the notions of relational morphisms and division in which the left-hand side can also be a category. 4.2

Decomposition of D1 into wreath products of Z

We explain our decision procedure by walking through the division of the syntactic monoid of D1 = ( ab)∗ into an iterated wreath product of Z, via carefully selected relational morphisms into Z. We will visualize objects of a category as rectangles (to prevent confusion with automata) and arrows as labels on edges between squares. Colors indicate the monoid each element comes from. We can view M (D1 ) as a category with a single object and arrows corresponding to monoid elements. We take a relational morphism into ϕ1 : M(D1 )◁Z where ϕ1 (⊥) = Z, ϕ1 ( a) = {1}, ϕ1 (b) = {−1}, ϕ1 (ϵ) = ϕ1 ( ab) = ϕ1 (ba) = {0}. 6

ϵ a b ab ba ⊥ M

Published as a conference paper at COLM 2026

In the derived category Dϕ1 there are infinitely many objects, corresponding to each integer. We omit starting or ending objects of arrows where clear by the diagram, combine isomorphic arrows, and let low-opacity arrows and objects denote transitions to ⊥ elements.

→(ϵ,0) →(ab,0)

···

−2

−1

→(ϵ,0) →(ba,0)

0→(b,−1) 0

2

1

1→(a,1)

···

We have not yet arrived at a division M (D1 ) ⪯ Z because Dϕ1 has hom-sets containing multiple arrows (Tilson, 1987, Lemma 3.1, Lemma 4.1). To proceed, we take another relational morphism ψ1 : Dϕ1 ◁Z where ψ1 ( x →(⊥,1) ) = ψ1 ( x →(⊥,−1) ) = [1, ∞) for all x; arrows not associated to ⊥ are instead mapped to {0}. From ϕ 1 , ψ1 we define a relational morphism ϕ2 : M (Do 1 )◁Z◦Z where we let ϕ2 ( m ) = n f (m,y) , y | y ∈ ϕ1 (m), ∀ x : f (m,y) ( x ) = ψ1 x →(m,y)

. We visualize the derived cate-

gory Dϕ2 below (writing ( f m , y) as shorthand for ϕ2 (m) whenever it is unique).

→(ϵ,( f ϵ ,0)) →(ϵ,( f ϵ ,0)) →(ab,( f ab ,0))

→(ba,( f ba ,0))

→(ab,( f ab ,0)) →(a,( f a ,1))

( f ϵ , 0)

→(b,( f b ,−1))

→(b,( f b ,−1))

→(b,( f b ,−1)) ( f ab , 0)

· · · ( f ⊥ , −2)

→(a,( f a ,1))

→(ϵ,( f ϵ ,0)) →(ba,( f ba ,0))

( f b , −1)

( f a , 1)

( f ⊥ , −1)

( f ⊥ , 0)

→(a,( f a ,1))

( f ⊥ , 1)

( f ba , 0) ( f ⊥ , 2) · · ·

We still do not have a division because there are still two arrows in a single homset of Dϕ2 , for instance ϕ2 (ϵ) and ϕ2 ( ab) act the same on ( f ab , 0). To handle this, we define a final relational morphism ϕ3 : M (D1 )◁Z◦Z◦Z such that ϕ3 (m) = ( g, ϕ2 (m)) where g( x ) = 0 iff x = ( f (ϵ,0) , 0). We ultimately obtain the division. ϕ3 : M (D1 ) ⪯ Z◦Z◦Z. In this example, we chose the correct relational morphisms into Z so as to obtain a division, but in principle there are infinitely many choices of morphisms. Guiding the choice of relational morphisms to reach a termination is a major challenge we address in our decision procedure. 4.3

Algebraic Decision Procedure

We now address the second challenge of maintaining computability despite the existence of infinitely many relational morphisms into Z. First, we divide M ( L) into equivalence classes via the R relation, a classical relation in semigroup theory which characterizes which elements are reachable by other elements via right-multiplication (Pin, 2025). We construct a sequence of iterated relational morphisms into Z by iterating over the R-classes in order. At step i + 1, we assume that a relational morphism ϕi covers all R-classes up to Ri , and extend to a relational morphism ϕi+1 that covers Ri+1 . This is done by iteratively computing nontrivial relational morphisms whose values are bounded on Ri . This process terminates, because the set of such bounded relational morphisms forms a finitely generated Z-module (an integer analogue of vector spaces), and every step finds a morphism linearly independent of the previous ones. 7

Published as a conference paper at COLM 2026

Finally we address the termination conditions by proving completeness of the algorithm. If the algorithm terminates with success, we have constructed a division from M ( L) into a wreath product of Z (and thus C-RASP by theorem 11). Otherwise, if the algorithm terminates with failure, we show no such division exists. In this case, assume for sake of contradiction that M ( L) divides a T-fold iterated wreath product of Z via a relational morphism ψ : M ( L) ⪯ Z◦ · · · ◦Z (where T is minimal). The rightmost component defines a relational morphism ω : M( L)◁Z. Either ω is bounded, and it would have been chosen as part of the decomposition had it provided any useful information, or ω is unbounded which renders long strings indistinguishable by types in Z since values may run to infinity. In either case, we can remove the rightmost component of ψ, and obtain a division from M into a ( T − 1)-fold iterated wreath product of Z, contradicting the minimality of T. To formalize the above proof, we choose relational morphisms to Z which truncate values beyond a threshold k (which results in relational morphisms to Dk ). This allows us to formalize the proof using finite category theory (avoiding the use of types on the category side). A formal writeup can be found in section H.3. 4.4

Necessary (but not Sufficient) Condition via Equations

In this section use profinite equations to give an alternative characterization of the regular languages in C-RASP. These equations are a technique drawing ideas from topology to derive elegant and decidable characterizations for classes of monoids. We defer a precise definition to Pin (2009). Definition 12. Define Rω as an equation and the corresponding variety of monoids2 as Rω : ( xyω )ω x = ( xyω )ω . For our purposes, a finite monoid M satisfies Rω if for any m1 , m2 ∈ M we have that (m1 m2ω )ω = (m1 m2ω )ω m1 , where mω denotes mk such that mk = m2k (i.e. the unique idempotent generated by m). We give an exact characterization of the monoids in Rω , the proof of which is in section I. Theorem 13. M ∈ Rω iff M is aperiodic and every R-class of M contains at most one idempotent. Equivalently, Rω = R◦G ∩ A, where R denotes the monoids where each R-class is singleton, G denotes the finite groups, and A denotes the aperiodic monoids. In our experiments below, we will draw languages from the larger class R◦G rather than Rω for testing lengthgeneralization. While both the main decision procedure and Rω require iterating over the R-classes of the monoid, the former needs to iteratively compute relational morphisms, while the latter only needs to count idempotents. This gives a much simpler criterion that is necessary for membership in C-RASP, though we can show it is not sufficient. 4.5

Algebraic Characterization

The decision procedure results an an exact algebraic characterization of the regular languages in C-RASP – namely, they are wreath products of bounded-depth Dyck languages. We thus derive a small hierarchy within the classes of finite monoids surrounding C-RASP. Theorem 14. C-RASP ∩ REG = wpc(Dy). Hence R ⊊ C-RASP ∩ REG ⊊ Rω ⊊ A ⊊ REG A proof is given in section I. Furthermore, the decision procedure runs in polynomial time in the size of the monoid. This allows us to efficiently decide whether or not we expect a transformer to length-generalize on any given regular language. A proof is in section H.3. Theorem 15. Membership of M ∈ C-RASP ∩ REG is decidable in O(poly(| M |)) time.

5

Experiments

We empirically evaluate whether our characterization of regular languages in C-RASP predicts transformer length-generalization. In particular, we examine the different levels 2 Rω alludes to the equation for R-trivial monoids, ( xy )ω = ( xy )ω x (Almeida & Azevedo, 1989)

8

Accuracy

1.0 0.8 0.6 0.4 0.2 0.0

Accuracy

Published as a conference paper at COLM 2026

1.0 0.8 0.6 0.4 0.2 0.0

[0,50]

[101,150]

C RASP

Not C RASP

R

R G C RASP

C RASP R

Not in R G

[201,250]

[301,350]

[401,450]

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

Figure 3: Length generalization on regular languages. Models are trained on strings of lengths in [lmin , 50], and evaluated on bins [lmin , 50] (in-distribution) up to [451, 500] in bins of width 50. Each curve corresponds to a language. Green curves denote languages in C-RASP, while red curves denote languages not in C-RASP. Languages in C-RASP maintain near-perfect accuracy well beyond the training range, whereas languages outside C-RASP exhibit rapid degradation, typically failing shortly after. Each panel includes all languages in the corresponding class from Table 1 in appendix B.3. of the hierarchy shown in theorem 14 to determine the efficacy of each class in predicting length-generalization by transformers. Because Rω \ C-RASP ∩ REG contains few samples, we report results based on membership in R◦G (whose aperiodic fragment is Rω ). 5.1

Languages

We construct a diverse suite of 125 regular languages, including both representative examples from prior work (Li & Cotterell, 2025; Huang et al., 2025) and systematically generated ones. We provide the full table of languages in Table 1, appendix B.3). To generate languages within the classes discussed in theorem 14, we sample regular expressions using a probabilistic context-free grammar (PCFG) for which we tune the probabilities to obtain diverse class membership. For each language, we determined membership in C-RASP using an automata-based version of the algebraic procedure, which we explain in section J. 5.2

Experimental Setup

Task Definition. The task is state prediction, i.e. tracking automaton states over prefixes. Let w = a1 . . . an , and denote by w1:i = a1 . . . ai the prefix of length i. Each symbol ai triggers a transition, and the model must predict the sequence of DFA states q1 , . . . , qn , where qi is the state reached after processing w1:i . Training and Evaluation. Per formal language, we train GPT-2 models on 10,000 words sampled from the training length range [lmin , 50] with lmin being the length of the shortest valid word in the respective language. We use an 80/20 train-test split. We then evaluate generalization on test length ranges [51, 100], [101, 150] . . . [451, 500], with 1,000 words in each test set. We define successful length generalization as maintaining near in-distribution performance at lengths beyond 2× the maximum training length 50. Following Huang et al. (2025) we used AdamW with weight decay 0.01 and dropout 0.0. We performed a hyperparameter sweep over layers {1, 2, 4}, heads {1, 2, 4}, dimension {16, 64, 256} and learning rates {0.001, 0.0001} – training every combination in the grid with early stopping when 100% accuracy is achieved on in-distribution test data. For those languages, where in-distribution accuracy never reached 100%, we additionally performed a hyperparameter sweep over layers {6, 8, 12}, heads {4, 8}, dimensions {64, 256} and learning rates {0.001, 0.0001}. We adopted optimization choices and hyperparameter ranges from Huang et al. (2025). Per 9

Published as a conference paper at COLM 2026

language, we choose the configuration that achieves the highest accuracy on the longest test length range among those whose accuracy on in-distribution length [lmin , 50] is 100%. We break remaining ties by successively considering the next-longest ranges and finally preferring the smallest model (fewest layers, then attention heads, then hidden dimension). The chosen configuration was then used for a multi-seed run, in which models were trained under different random model initializations, an approach commonly used in prior work (Li & Cotterell, 2025; Huang et al., 2025). A run was considered successful if it achieved 100% accuracy on the in-distribution test set. We evaluated random initializations sequentially, up to a maximum of 1,000 trials, and ended the search once five successful runs were found. We report the best successful seed in Figure 3 and show the average performance across all successful seeds in B. Architectural Constraints. To align empirical results with our theoretical setup, state prediction should depend on the evolving prefix rather than local information. We therefore introduce two constraints: first, we remove positional information by replacing positional embeddings with the zero function (NoPE) forcing the model to rely on the sequential order of tokens provided by the causal attention mask. Second, while NoPE removes absolute positional information, the model still has direct access to the most recent input symbol ai when predicting the target state qi , which provides a positional signal through alignment with the prediction target. This can enable shortcuts in which the model predicts the state based solely on the final symbol, rather than the full prefix. To prevent this, we insert a separator token & between symbols (see below) and require the model to predict the state qi only at these separator positions. Consequently, access to the most recent symbol is also mediated through the attention mechanism. Word symbols receive placeholder targets # and are excluded from the cross-entropy loss. Each target sequence begins with the initial DFA state, predicted at the first separator following <bos>. Input <BOS> & a & b & a & b & a & b & <EOS>

5.3

Positional Encoding

0

0 0 0 0 0 0 0 0 0 0 0 0 0

0

Target

#

1 # 3 # 1 # 3 # 1 # 3 # 1

#

Results

Figure 3 shows that C-RASP membership is a strong predictor of transformer lengthgeneralization. Languages in C-RASP generalize reliably to substantially longer lengths, while languages outside C-RASP fail to do so, with accuracy rapidly collapsing beyond the training length. This demonstrates that across all evaluated languages C-RASP provides an accurate characterization of length generalization.

6

Conclusion

We have precisely characterized the regular languages on which transformers lengthgeneralize using a decision procedure for regular language membership in C-RASP (which runs in polynomial-time). Experiments on a range of languages in and outside of C-RASP demonstrate that the theory accurately predicts when transformers do and do not lengthgeneralize. The decision procedure is based on a novel algebraic decomposition theory for C-RASP that is distinguished from the classical Krohn-Rhodes theory due to the inclusion of infinite monoids and the omission of the aperiodic flip-flop unit U2 . A simpler criterion which is necessary (but not sufficient) for membership in C-RASP is also given in the form of a profinite equation. Our results provide a deeper understanding of the state-tracking capabilities of transformers on the machine learning front, as well as a deeper understanding of counting, on the algebraic front.

10

Published as a conference paper at COLM 2026

Acknowledgments We thank Dana Angluin, Michael Benedikt, David Chiang, and Will Merrill for fruitful discussion and feedback. We thank the anonymous reviewers for their helpful comments. Funded in part by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – GRK 2853/1 “Neuroexplicit Models of Language, Vision, and Action” - project number 471607914, and the US National Science Foundation (grant number 2502292). AY is supported by the US National Science Foundation Graduate Research Fellowship Program under Grant No. 2236418. MH acknowledges support from the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – Project number 560456343.

References Jorge Almeida and Assis Azevedo. The join of the pseudovarieties of R-trivial and L-trivial monoids. Journal of Pure and Applied Algebra, 60(2):129–137, 1989. ISSN 0022-4049. doi: https://doi.org/10.1016/0022-4049(89)90125-4. URL https://www.sciencedirect.com/ science/article/pii/0022404989901254. Eric Alsmann, Lowejatan Noori, and Martin Lange. On the expressiveness of state space models via temporal logics. In The Fourteenth International Conference on Learning Representations, 2026. URL https://openreview.net/forum?id=Vg511oJScS. David A. Barrington. Bounded-width polynomial-size branching programs recognize exactly those languages in nc1. Journal of Computer and System Sciences, 38(1):150–164, 1989. ISSN 0022-0000. doi: https://doi.org/10.1016/0022-0000(89)90037-8. URL https: //doi.org/10.1016/0022-0000(89)90037-8. David A. Mix Barrington, Kevin Compton, Howard Straubing, and Denis Thérien. Regular languages in NC1 . Journal of Computer and System Sciences, 44(3):478–499, 1992. ISSN 0022-0000. doi: https://doi.org/10.1016/0022-0000(92)90014-A. URL https://doi.org/ 10.1016/0022-0000(92)90014-A. Christoph Behle, Andreas Krebs, and Stephanie Reifferscheid. Typed monoids – an eilenberglike theorem for non regular languages. In Franz Winkler (ed.), Algebraic Informatics, pp. 97–114, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. ISBN 978-3-642-21493-6. doi: https://doi.org/10.1007/978-3-642-21493-6 6. Satwik Bhattamishra, Kabir Ahuja, and Navin Goyal. On the Ability and Limitations of Transformers to Recognize Formal Languages. In Bonnie Webber, Trevor Cohn, Yulan He, and Yang Liu (eds.), Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pp. 7096–7116, Online, November 2020. Association for Computational Linguistics. doi: 10.18653/v1/2020.emnlp-main.576. URL https:// aclanthology.org/2020.emnlp-main.576/. J.A. Brzozowski and Faith E. Fich. Languages of R-trivial monoids. Journal of Computer and System Sciences, 20(1):32–49, 1980. ISSN 0022-0000. doi: https://doi.org/10.1016/ 0022-0000(80)90003-3. David Chiang. Transformers in uniform TC0 . Transactions on Machine Learning Research, 2025. ISSN 2835-8856. URL https://openreview.net/forum?id=ZA7D4nQuQF. Mai Gehrke and Andreas Krebs. Stone duality for languages and complexity. ACM SIGLOG News, 4(2):29–53, May 2017. doi: 10.1145/3090064.3090068. URL https://doi.org/10. 1145/3090064.3090068. Michael Hahn. Theoretical limitations of self-attention in neural sequence models. Transactions of the Association for Computational Linguistics, 8:156–171, 01 2020. ISSN 2307-387X. doi: 10.1162/tacl a 00306. URL https://doi.org/10.1162/tacl a 00306. 11

Published as a conference paper at COLM 2026

Xinting Huang, Andy Yang, Satwik Bhattamishra, Yash Sarrof, Andreas Krebs, Hattie Zhou, Preetum Nakkiran, and Michael Hahn. A formal framework for understanding length generalization in transformers. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=U49N5V51rU. Selim Jerad, Anej Svete, Jiaoda Li, and Ryan Cotterell. Unique hard attention: A tale of two sides. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar (eds.), Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), pp. 977–996, Vienna, Austria, July 2025. Association for Computational Linguistics. ISBN 979-8-89176-252-7. doi: 10.18653/v1/2025.acl-short.76. URL https://aclanthology.org/2025.acl-short.76/. Mayank Jobanputra, Yana Veitsman, Yash Sarrof, Aleksandra Bakalova, Vera Demberg, Ellie Pavlick, and Michael Hahn. Born a transformer – always a transformer? On the effect of pretraining on architectural abilities. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. URL https://openreview.net/forum?id= Huw15LqglI. Ravindran Kannan and Achim Bachem. Polynomial algorithms for computing the smith and hermite normal forms of an integer matrix. SIAM Journal on Computing, 8(4):499–507, 1979. doi: 10.1137/0208040. URL https://doi.org/10.1137/0208040. Ronald M. Kaplan and Martin Kay. Regular models of phonological rule systems. Computational Linguistics, 20(3):331–378, 1994. URL https://aclanthology.org/J94-3001/. Najoung Kim and Sebastian Schuster. Entity tracking in language models. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 3835–3855, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10.18653/v1/2023. acl-long.213. URL https://aclanthology.org/2023.acl-long.213/. S. C. Kleene. Representation of Events in Nerve Nets and Finite Automata, pp. 3–42. Princeton University Press, Princeton, 1956. ISBN 9781400882618. doi: doi:10.1515/ 9781400882618-002. URL https://doi.org/10.1515/9781400882618-002. Andreas Krebs. Typed Semigroups, Majority Logic, and Threshold Circuits. PhD thesis, Universität Tübingen, 2008. URL https://nbn-resolving.org/urn:nbn:de:bsz:21-opus-36244. URN: urn:nbn:de:bsz:21-opus-36244. Kenneth Krohn and John Rhodes. Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines. Transactions of the American Mathematical Society, 116:450–464, 1965. doi: 10.1090/S0002-9947-1965-0188316-1. URL https://doi. org/10.1090/S0002-9947-1965-0188316-1. Jiaoda Li and Ryan Cotterell. Characterizing the expressivity of fixed-precision transformer language models. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. URL https://openreview.net/forum?id=29LwAgLFpj. Zhiyuan Li, Hong Liu, Denny Zhou, and Tengyu Ma. Chain of thought empowers transformers to solve inherently serial problems. In The Twelfth International Conference on Learning Representations, 2024. URL https://openreview.net/forum?id=3EWTEy9MTM. Bingbin Liu, Jordan T. Ash, Surbhi Goel, Akshay Krishnamurthy, and Cyril Zhang. Exposing attention glitches with flip-flop language modeling. In Thirty-seventh Conference on Neural Information Processing Systems, 2023a. URL https://openreview.net/forum?id= VzmpXQAn6E. Bingbin Liu, Jordan T. Ash, Surbhi Goel, Akshay Krishnamurthy, and Cyril Zhang. Transformers learn shortcuts to automata. In The Eleventh International Conference on Learning Representations, 2023b. URL https://openreview.net/forum?id=De4FYqjFueZ. 12

Published as a conference paper at COLM 2026

William Merrill and Ashish Sabharwal. A logic for expressing log-precision transformers. In A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine (eds.), Advances in Neural Information Processing Systems, volume 36, pp. 52453–52463. Curran Associates, Inc., 2023. URL https://proceedings.neurips.cc/paper files/paper/2023/ file/a48e5877c7bf86a513950ab23b360498-Paper-Conference.pdf. William Merrill and Ashish Sabharwal. A little depth goes a long way: The expressive power of log-depth transformers. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. URL https://openreview.net/forum?id=5pHfYe10iX. Jean-Eric Pin. Profinite Methods in Automata Theory. In Susanne Albers and Jean-Yves Marion (eds.), 26th International Symposium on Theoretical Aspects of Computer Science, volume 3 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 31–50, Dagstuhl, Germany, 2009. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. ISBN 978-3-93989709-5. doi: 10.4230/LIPIcs.STACS.2009.1856. URL https://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.STACS.2009.1856. Jean-Eric Pin. The dot-depth hierarchy, 45 years later. In Stavros Konstantinidis, Nelma Moreira, Rogério Reis, and Jeffrey Shallit (eds.), The Role of Theory in Computer Science Essays Dedicated to Janusz Brzozowski, The Role of Theory in Computer Science - Essays Dedicated to Janusz Brzozowski. World Scientific, 2017. doi: 10.1142/9789813148208\ 0008. URL https://hal.science/hal-01614357. Jean-Éric Pin. Mathematical foundations of automata theory. Lecture notes, MPRI, IRIF, CNRS and Université de Paris. Available at https://www.irif.fr/∼jep/PDF/MPRI/MPRI. pdf, 2025. John Rhodes. Undecidability, automata, and pseudovarities of finite semigroups. International Journal of Algebra and Computation, 9(3):455–474, 1999. doi: 10.1142/ S0218196799000278. URL https://doi.org/10.1142/S0218196799000278. Yash Sarrof, Yana Veitsman, and Michael Hahn. The expressive capacity of state space models: A formal language perspective. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. URL https://openreview.net/forum?id=eV5YIrJPdy. Maximilian Schall and Gerard de Melo. The hidden cost of structure: How constrained decoding affects language model performance. In Galia Angelova, Maria Kunilovskaya, Marie Escribe, and Ruslan Mitkov (eds.), Proceedings of the 15th International Conference on Recent Advances in Natural Language Processing - Natural Language Processing in the Generative AI Era, pp. 1074–1084, Varna, Bulgaria, September 2025. INCOMA Ltd., Shoumen, Bulgaria. URL https://aclanthology.org/2025.ranlp-1.124/. Erik Schluntz and Barry Zhang. Building effective agents. https://www.anthropic.com/ engineering/building-effective-agents, December 2024. Accessed: 2026-03-23. M. P. Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8:190–194, 1965. doi: https://doi.org/10.1016/S0019-9958(65)90108-7. Imre Simon. Piecewise testable events. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pp. 214–222, Berlin, Heidelberg, 1975. Springer-Verlag. ISBN 3540074074. doi: https://doi.org/10.1007/3-540-07407-4 23. Michael Sipser. Introduction to the Theory of Computation. International Thomson Publishing, 1st edition, 1996. ISBN 053494728X. URL https://dl.acm.org/doi/10.5555/524279. Price Stiffler Jr. Extension of the fundamental theorem of finite semigroups. Advances in Mathematics, 11(2):159–209, 1973. doi: https://doi.org/10.1016/0001-8708(73)90007-8. Robert Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1 (2):146–160, 1972. doi: https://doi.org/10.1137/0201010. Denis Thérien and Thomas Wilke. Temporal logic and semidirect products: An effective characterization of the until hierarchy. SIAM Journal on Computing, 31(3):777–798, 2001. doi: https://doi.org/10.1137/S0097539797322772. 13

Published as a conference paper at COLM 2026

Bret Tilson. Categories as algebra: An essential ingredient in the theory of monoids. Journal of Pure and Applied Algebra, 48(1):83–198, 1987. ISSN 0022-4049. doi: https://doi.org/10. 1016/0022-4049(87)90108-3. Sam van der Poel, Dakotah Lambert, Kalina Kostyszyn, Tiantian Gao, Rahul Verma, Derek Andersen, Joanne Chau, Emily Peterson, Cody St. Clair, Paul Fodor, Chihiro Shibata, and Jeffrey Heinz. Mlregtest: A benchmark for the machine learning of regular languages. Journal of Machine Learning Research, 25(283):1–45, 2024. URL http://jmlr.org/papers/ v25/23-0518.html. Andy Yang and David Chiang. Counting like transformers: Compiling temporal counting logic into softmax transformers. In First Conference on Language Modeling, 2024. URL https://openreview.net/forum?id=FmhPg4UJ9K. Andy Yang, David Chiang, and Dana Angluin. Masked hard-attention transformers recognize exactly the star-free languages. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. URL https://openreview.net/forum?id=FBMsBdH0yz. Andy Yang, Michaël Cadilhac, and David Chiang. Knee-deep in c-RASP: A transformer depth hierarchy. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. URL https://openreview.net/forum?id=jPduiyxyfw.

14

Published as a conference paper at COLM 2026

Contents 1

Introduction

1

2 Algebraic Preliminaries

3

2.1

Basics: Algebraic Theory of Formal Languages . . . . . . . . . . . . . . . . .

3

2.2

Background: Classical Algebraic Decomposition Theory of Regular Languages

4

3 Algebraic Characterization of C-RASP

4

5

6

4

3.1

Typed Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5

3.2

Wreath Product Characterization . . . . . . . . . . . . . . . . . . . . . . . . .

5

Decomposition Theory for Regular Languages in C-RASP

5

4.1

Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6

4.2

Decomposition of D1 into wreath products of Z . . . . . . . . . . . . . . . .

6

4.3

Algebraic Decision Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

4.4

Necessary (but not Sufficient) Condition via Equations . . . . . . . . . . . .

8

4.5

Algebraic Characterization . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8

Experiments

8

5.1

Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9

5.2

Experimental Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9

5.3

Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10

Conclusion

10

A FAQ

16

B Additional Experimental Results

19

B.1 Additional Results on the Main Language Suite . . . . . . . . . . . . . . . . .

19

B.1.1

Results by C-RASP Membership . . . . . . . . . . . . . . . . . . . . .

19

B.1.2

Length Generalization Across Seeds and Languages . . . . . . . . . .

19

B.1.3

Increased Training Data Size . . . . . . . . . . . . . . . . . . . . . . .

20

B.2 Experiments on More Complex Languages . . . . . . . . . . . . . . . . . . .

21

B.2.1

Length Generalization . . . . . . . . . . . . . . . . . . . . . . . . . . .

21

B.2.2

Results by C-RASP Membership . . . . . . . . . . . . . . . . . . . . .

22

B.2.3

Length Generalization Across Seeds and Languages . . . . . . . . . .

22

B.3 Regular Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

23

C Algebraic Preliminaries

23

D Linear RASP programs

26 15

Published as a conference paper at COLM 2026

E Typed Monoids

27

E.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

28

E.2 Proof of Typed Wreath Product Principle . . . . . . . . . . . . . . . . . . . .

30

F C-RASP

32

F.1

Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

32

F.2

C-RASP as a pseudovariety of Languages . . . . . . . . . . . . . . . . . . . .

33

F.3

Existing Characterizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

34

F.4

Algebraic Characterization of C-RASP . . . . . . . . . . . . . . . . . . . . . .

34

G Derived Categories

34

H Algebraic Decision Procedure

36

H.1 Relevant Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

36

H.2 Bounded-Depth Dyck Monoids . . . . . . . . . . . . . . . . . . . . . . . . . .

36

H.3 Decidability Proof (via Finite Derived Categories) . . . . . . . . . . . . . . .

37

H.3.1 Key Properties of the Procedure . . . . . . . . . . . . . . . . . . . . .

39

H.3.2 Establishing Completeness . . . . . . . . . . . . . . . . . . . . . . . .

42

H.3.3 Deriving Main Results . . . . . . . . . . . . . . . . . . . . . . . . . . .

46

H.4 Defining Division between Categories and Typed Monoids . . . . . . . . . .

47

I

Algebraic Characterization (Necessary but not Sufficient Criterion)

48

J

Automata proof of C-RASP ∩ REG

49

K Implementation

53

Author Contributions AY led paper writing, drafted the proof of Theorem 11 and the implementation of the decision procedure, contributed to the discovery and proof of Theorems 14 and 15, drafted Appendix J, and drafted Sections 1–4 of the paper. BV designed, implemented, and carried out the experiments, and drafted Section 5 of the paper. CB, MC, AK, CP, HS contributed to the discovery and proof of Theorems 14 and 15, and provided input to the paper writing. HS further contributed Theorem 13. MH contributed to the discovery and proof of Theorems 14 and 15, drafted the proof of Theorems 14 and 15 in Appendix H and an early draft of Appendix J, and contributed to paper writing.

A

FAQ 1. Q: How does the work relate and compare to Liu et al. (2023b)? Liu et al. (2023b) primarily looked at expressivity, not length generalization. Indeed, their experiments also confirmed that transformers may not length-generalize on the particular regular languages that they were able to express and learn to a fixed length. Our results may also apply to the expressive power of transformers under a particular fixed-precision assumption, because C-RASP was shown to be equivalent to these transformers by Yang et al. (2025). 16

Published as a conference paper at COLM 2026

2. Q: How about other architectures? Like log-depth transformers, state-space models, ...? It is already known that log-depth architectures can simulate arbitrary automata, so a characterization of the regular languages they can express is not needed (Liu et al., 2023b; Merrill & Sabharwal, 2025). As for length-generalization, we do not presently know what regular languages these architectures length-generalize on. Analyzing architectures with limited recurrence, like state-space models, would be an interesting future question. Under varying assumptions, state-space models are able to simulate flip-flops and counting (Sarrof et al., 2024; Alsmann et al., 2026). The techniques we have developed to handle counting could be extended to handle these cases as well. 3. Q: Why not evaluate LLMs? We’re more interested in the architecture itself. LLM abilities depend on prompt format and are strongly impacted by what’s in the training data. There is work suggesting that the capabilities of LLMs are ultimately bounded by C-RASP (Jobanputra et al., 2025), though a precise investigation in the case of regular language length-generalization is out of the scope of this work. 4. Q: How does C-RASP compare to other classes, such as subregular classes, circuit classes, and the dot depth hierarchy? Could they on their own already predict transformer length generalization? C-RASP is distinct from known classes, and much more successful at predicting length generalization than those are. Here, we will expand on fig. 2. In fact, all existing classes do not predict length-generalization on transformers. • Regular and subregular: The regular languages in C-RASP define a strict subset of the star-free languages. As we show, even Rω only covers star-free languages (and in fact it is a strict subset). • Circuit classes: The circuit classes most relevant to transformers are AC0 and TC0 ; neither of them captures C-RASP or transformer length generalization well. C-RASP is a strict subset of TC0 , as was shown in Huang et al. (2025). This extends to regular languages: E.g., the PARITY language (b∗ ab∗ ab∗ ) (checking if the number of a’s is even) is in TC0 but not in C-RASP. In general, C-RASP is incomparable with AC0 . Interestingly, on the level of regular languages, C-RASP is a strict subset of AC0 : C-RASP only includes star-free languages (and all of those are in AC0 ), but, for instance, { a, b}∗ b is in AC0 but not in C-RASP. • Dot-depth hierarchy. Given the containment inside the star-free languages, one could consider stratifications of these languages. One of the most well-studied ones is the dot-depth hierarchy. C-RASP can express every bounded-depth dyck languages, and thus can touch every single level of the dot-depth hierarchy, while not covering the entire hierarchy. 5. Q: What about the role of positional encodings? This is an important question for future work that would result in a different characterization than the one we have derived here. Huang et al. (2025) showed that C-RASP[periodic, local] characterizes the languages which transformers with APE can length-generalize on. Obtaining a decision procedure on the algebraic side would require additional techniques from the ones used in this paper. 6. Q: Why did you not use MLRegTest for your experiments (van der Poel et al., 2024)? We looked into this, but unfortunately a significant portion of the languages in the dataset contain strictly local patterns, which are not expressible in C-RASP without positional encodings (Huang et al., 2025). Future work extending the characterization of C-RASP to handle positional encodings should use this benchmark. 7. Q: The experiments deliberately prevent residual-stream access to the last token in state prediction. Why? Could the theory handle the case where one actually wants this access? We argue that state tracking should be robust to the insertion of “do-nothing” actions not changing the state, or other unrelated extra material. In formal language theory, such actions are referred to as neutral symbols. Invariance under the inclusion of such neutral symbols is a natural property of characterizations in terms of syntactic 17

Published as a conference paper at COLM 2026

monoids, as we have done here. An example where this plays a role is { a, b}∗ b (where the state – is the last symbol seen a b? – can be easily tracked based on the last symbol), which has the same syntactic monoid as the language { a, b, e}∗ be∗ resulting from adding a neutral symbol e, which is difficult for Transformer length generalization (Liu et al., 2023a; Huang et al., 2025). Neither is definable in C-RASP. 8. Q: Why do your empirical results differ from that of Li & Cotterell (2025) and Huang et al. (2025) who both test length generalization for regular languages in C-RASP? We think addressing the empirical and theoretical results of Huang et al. (2025) and Li & Cotterell (2025) in light of our findings is an important question. Li & Cotterell (2025) suggested that transformers consistently fail to length-generalize on languages outside of R, providing evidence when trained on length N and tested on length 12N. While Huang et al. (2025) showed length-generalization in languages in C-RASP \ R, they only trained on length N and tested up to 3N, so the results may be incomparable. In the present work, we specifically probed languages in C-RASP ∩ REG \ R and found length-generalization from length N to 10N, suggesting a more optimistic picture of length-generalization than Li & Cotterell (2025). We suspect the difference in our empirical observations might be attributed to the small number of languages in C-RASP ∩ REG \ R tested by Li & Cotterell (2025) – only 3 such languages were tested. Indeed, prior to this work there existed no sizeable dataset of languages in C-RASP ∩ REG \ R, as there was no computable membership criterion for C-RASP ∩ REG. An additional difference is that Li & Cotterell (2025) use a language classification task where the model is trained on both positive and negative examples. The experiments done by Bhattamishra et al. (2020); Huang et al. (2025); Yang et al. (2025), and this work on C-RASP all use a next-token prediction setup.

18

Published as a conference paper at COLM 2026

B

Additional Experimental Results

In this section, we provide additional experimental results supporting Section 5. We first report complementary analyses on the language suite from Table 1 used for the experiments in Figure 3 shown in the main paper. Specifically, we present best seed results grouped directly by C-RASP membership in Section B.1.1, results across multiple random seeds in Section B.1.2, and experiments with increased training data (from 10K to 100K) in Section B.1.3. We then evaluate a second suite of more complex regular languages with greater nesting depth (Table 2). For these languages, we extend the training range from [lmin , 50] to [lmin , 200] and report the corresponding experiments in Section B.2. We present length generalization results across the classes R, C-RASP, and R ◦ G in Section B.2.1, directly compare languages in and outside of C-RASP in Section B.2.2, and evaluate performance across multiple random seeds in Section B.2.3. Finally, Section B.3 provides the complete lists of regular languages used in both experimental suites, together with their membership in R, Rω , R ◦ G, and C-RASP.

B.1 B.1.1

Additional Results on the Main Language Suite Results by C-RASP Membership

Accuracy

The main paper reports length generalization results separately for languages in R, C-RASP \ R, R ◦ G \ C-RASP, and outside R ◦ G (Figure 3). Here, we provide an alternative view of the same experimental results by grouping languages according to their C-RASP membership only. Figure 4 shows a clear separation between languages, where languages in C-RASP reliably generalize beyond the training length range, whereas languages outside C-RASP consistently fail to do so.

1.0 0.8 0.6 0.4 0.2 0.0

C RASP

[0,50]

[101,150]

[201,250]

[301,350]

Not in C RASP

[401,450]

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

Figure 4: Length generalization by C-RASP membership. Models are trained on strings of lengths in [lmin , 50] and evaluated on ranges from [lmin , 50] (in-distribution) up to [451, 500] in steps of 50. Each curve corresponds to a language from Table 1.

B.1.2

Length Generalization Across Seeds and Languages

The results in the main paper report the best successful seed for each language. To assess whether the observed length generalization behavior is robust across random seeds (i.e. random model initializations), we additionally aggregate results over the five best successful seeds per language, where a seed is considered successful if it achieves 100% accuracy on the in-distribution test data. Figure 5 reports these results across R, C-RASP \ R, R ◦ G \ C-RASP, and outside R ◦ G, while Figure 6 groups them only by C-RASP membership. Results show that languages outside C-RASP consistently fail to length generalize across languages and across random seeds. 19

Published as a conference paper at COLM 2026

Accuracy

1.0

Not C − RASP

R

R ∘ G ∖ C−RASP

C − RASP ∖ R

Not in R ∘ G

0.5

0.0 1.0

Accuracy

C − RASP

0.5

0.0

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

Figure 5: Length generalization on regular languages (aggregated across languages and seeds). Models are trained on strings of lengths in [lmin , 50] and evaluated on length ranges from [lmin , 50] (in-distribution) up to [451, 500] in steps of 50. For each language we compute the mean accuracy across its 5 best successful seeds, where a seed is considered successful if it achieves 100% accuracy on the in-distribution test data. Solid lines show the mean of these per-language curves within each group, and shaded regions show one standard deviation across languages. Green corresponds to languages in C-RASP, while red corresponds to languages not in C-RASP. Each panel includes all languages in the corresponding group from Table 1.

C-RASP

Accuracy

1.0

Not in C-RASP

0.8 0.6 0.4 0.2 0.0

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

Figure 6: Length generalization by C-RASP membership, aggregated across languages and seeds. Models are trained on strings of lengths in [lmin , 50] and evaluated on length ranges from [lmin , 50] (in-distribution) up to [451, 500] in steps of 50. For each language, we compute the mean accuracy across its 5 best successful seeds, where a seed is considered successful if it achieves 100% accuracy on the in-distribution test data. Solid lines show the mean of these per-language curves for languages within and outside C-RASP, and shaded regions show one standard deviation across languages. In contrast to Figure 5, which separates languages into R, C-RASP \ R, R ◦ G \ C-RASP, and those outside R ◦ G, here we group the same languages by C-RASP membership only, providing an overall view of length generalization within and outside C-RASP. Each panel includes all languages in the corresponding group from Table 1.

B.1.3

Increased Training Data Size

Finally, we test how increased training data size affects length generalization within different classes. We repeat the experiments with 100K sampled words per language, using an 80/20 train-test split, compared to 10K training examples in the original experiments. We otherwise follow the same training and hyperparameter search procedure described in Section 5. Figure 7 shows that increasing the amount of training data does not change trends in length generalization: languages in C-RASP continue to generalize beyond the training lengths, while languages outside C-RASP do not. In Figure 8 we again regroup the same results from Figure 7 into languages in and outside of C-RASP only. 20

Published as a conference paper at COLM 2026

Not C RASP

R

R G C RASP

C RASP R

Not in R G

Accuracy

1.0

C RASP 0.5 0.0

Accuracy

1.0 0.5 0.0

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

Accuracy

Figure 7: Length generalization on regular languages with increased training data. Models are trained on strings of lengths in [lmin , 50] using a larger training set (100K examples instead of 10K), and evaluated on lengths from [lmin , 50] (in-distribution) up to [401, 500] in steps of 50. Each curve corresponds to a language. We report the best seed per language. Increasing the training data does not change trends in length generalization: languages in C-RASP continue to generalize, while languages not in C-RASP consistently fail to generalize beyond the training range. For these experiments, we used the systematically generated subset of languages listed in Table 1, consisting of 100 languages in total.

1.0 0.8 0.6 0.4 0.2 0.0

C RASP

[0,50]

[101,150]

[201,250]

[301,350]

Not in C RASP

[401,450]

[0,50]

[101,150]

[201,250]

[301,350]

[401,450]

Figure 8: Length generalization by C-RASP membership with increased training data. Models are trained on strings of lengths in [lmin , 50] using a larger training set (100K examples instead of 10K) and evaluated on length ranges from [lmin , 50] (in-distribution) up to [401, 500] in steps of width 50. Each curve corresponds to a language, and we report the best seed per language. In contrast to Figure 7, which separates languages into the four groups R, C-RASP\ R, R ◦ G\C-RASP, and languages outside R ◦ G, here we group the same languages solely by C-RASP membership, providing an overall view of length generalization within and outside C-RASP. For these experiments, we used the systematically generated subset of languages listed in Table 1, consisting of 100 languages in total. B.2

Experiments on More Complex Languages

To test whether our findings extend to more complex languages, we repeat our experiments on a systematically generated set of 50 regular languages with greater nesting depth (Table 2), following the same experimental procedure described in Section 5. In addition, we increase the maximum training length from 50 to 200, allowing us to examine length generalization behavior when models are trained on longer strings. B.2.1

Length Generalization

In Figure 9 we show results across R, C-RASP \ R, R ◦ G \ C-RASP, and those outside R ◦ G, confirming length generalization trends seen on simpler languages and shorter training lengths. Figure 10 highlights this length generalization trends further by dividing languages into subsets of in and outside of C-RASP providing a more summarized overview. 21

Published as a conference paper at COLM 2026

Accuracy

1.0

Not C − RASP

R

R ∘ G ∖ C−RASP

C − RASP ∖ R

Not in R ∘ G

0.5

0.0 1.0

Accuracy

C − RASP

0.5

0.0

[0,200]

[201,300]

[301,400]

[401,500]

[0,200]

[201,300]

[301,400]

[401,500]

Figure 9: Length generalization on regular languages (longer training length). Models are trained on strings of lengths in [lmin , 200], and evaluated on length ranges [lmin , 200] (in-distribution) up to [401, 500] in steps of 100. Each curve corresponds to a language. Green curves denote languages in C-RASP, while red curves denote languages not in C-RASP. Languages in C-RASP maintain near-perfect accuracy well beyond the training range, whereas languages outside C-RASP exhibit rapid degradation, typically failing shortly after. Languages corresponding to this plot can be viewed in Table 2.

B.2.2

Results by C-RASP Membership

C-RASP

Accuracy

1.0

Not in C-RASP

0.8 0.6 0.4 0.2 0.0

[0,200]

[201,300]

[301,400]

[401,500]

[0,200]

[201,300]

[301,400]

[401,500]

Figure 10: Length generalization by C-RASP membership (longer training length). Models are trained on strings of lengths in [lmin , 200] and evaluated on length ranges from [lmin , 200] (in-distribution) up to [401, 500] in steps of 100. Each curve corresponds to a language. In contrast to Figure 9, which separates languages into the four groups R, C-RASP \ R, R ◦ G\C-RASP, and languages outside R ◦ G, here we group the same languages by C-RASP membership, providing an overall view of length generalization within and outside C-RASP. Each panel includes all languages in the corresponding group from Table 2.

B.2.3

Length Generalization Across Seeds and Languages

Similar to Section B.1.2, we evaluate how consistent length generalization trends are across random seeds (i.e. random model initializations) and languages within a class. We compute the mean accuracy across the five best successful seeds for each language and aggregate these results across languages. Figure 11 shows that same length generalization trends persist across seeds: languages in C-RASP maintain high accuracy beyond the training length range, while languages outside C-RASP consistently degrade with increasing length. Figure 12 further emphasizes this difference by grouping languages in and outside of C-RASP. 22

Published as a conference paper at COLM 2026

Accuracy

1.0

Not C − RASP

R

R ∘ G ∖ C−RASP

C − RASP ∖ R

Not in R ∘ G

0.5

0.0 1.0

Accuracy

C − RASP

0.5

0.0

[0,200]

[201,300]

[301,400]

[401,500]

[0,200]

[201,300]

[301,400]

[401,500]

Figure 11: Length generalization on regular languages (aggregated across languages and seeds). Models are trained on strings of lengths in [lmin , 200] and evaluated on length ranges from [lmin , 200] (in-distribution) up to [401, 500] in steps of 100. For each language we compute the mean accuracy across its 5 best successful seeds, where a seed is considered successful if it achieves 100% accuracy on the in-distribution test data. Solid lines show the mean of these per-language curves within each class, and shaded regions show one standard deviation across languages. Green corresponds to languages in C-RASP, while red corresponds to languages not in C-RASP. Results for individual best seeds are shown in Figure 9. Each panel includes all languages in the corresponding class from Table 2. C-RASP

Accuracy

1.0

Not in C-RASP

0.8 0.6 0.4 0.2 0.0

[0,200]

[201,300]

[301,400]

[401,500]

[0,200]

[201,300]

[301,400]

[401,500]

Figure 12: Length generalization by C-RASP membership, aggregated across languages and seeds. Models are trained on strings of lengths in [lmin , 200] and evaluated on length ranges from [lmin , 200] (in-distribution) up to [401, 500] in steps of 100. For each language, we compute the mean accuracy across its 5 best successful seeds, where a seed is considered successful if it achieves 100% accuracy on the in-distribution test data. Solid lines show the mean of these per-language curves for languages within and outside C-RASP, and shaded regions show one standard deviation across languages. In contrast to Figure 11, which separates languages into the four groups R, C-RASP \ R, R ◦ G \ C-RASP, and languages outside R ◦ G, here we group the same languages solely by C-RASP membership, providing an overall view of length generalization within and outside C-RASP. Each panel includes all languages in the corresponding group from Table 2. B.3

Regular Languages

We report the complete set of regular languages used in our experimental evaluation in the main paper and appendix. Tables 1 and 2 provide a comprehensive overview of the dataset. For each language, we indicate membership in R, Rω , R ◦ G, and C-RASP.

C

Algebraic Preliminaries

Definition 16 (Recognition; Syntactic Monoid). Let L ⊆ Σ∗ be a language. A monoid M recognizes L iff there is a homomorphism h : Σ∗ → M and a subset X ⊆ M such that L = h−1 ( X ). 23

Published as a conference paper at COLM 2026

Formal Language

(bbac)∗ (bab + b)∗ (c + b( a)∗ )∗ b + (bb)∗ acabcc(c)∗ bbcc( aa)∗ ( ab( a)∗ )∗ (cc)∗ (( a)∗ ac)∗ ((b)∗ ab)∗ ( ac( a)∗ )∗ (cca + a)∗ cb( a)∗ + abbc aa( a)∗ c ( aa + aa)∗ ( a + c)∗ cbbb bc(b)∗ abbb (ca)∗ (cb)∗ (cc)∗ ccb + b (( a)∗ )∗ ( ac)∗ bccb( aa)∗ (ba)∗ (b)∗ bc ( ac)∗ ba(b)∗ ( a)∗ b + acab (ca)∗ ( a)∗ bb (b)∗ (b)∗ ( aa)∗ b + ca + b(c + a)∗ (cbb + b)∗ c + cab + (bc)∗ (c)∗ b + b(b)∗ (ca(c)∗ )∗ bab(ba)∗ bbbc(ca)∗ ( abcb)∗ cc + cc(bb)∗ bcba + ( a)∗ aa a + c( a)∗ cb + a (cb(c)∗ )∗ ((b)∗ bc)∗ ( a + aac)∗ (cb)∗ caa + b caaba + ( a)∗ (cc)∗ bac (b + ac + c)∗ ( acba)∗ cbac( a)∗ ( a)∗ ( a)∗ (bb)∗ (( a)∗ ab)∗ baca(bc)∗ (ca)∗ (cc)∗ ( ab + aabb)∗ ( aa)∗ ( ab)+ a+ ( ab)+ a+ b+ a+ (( ab)+ b+ )k ( ab)+ b( ab)+ ( a + b+)k ( ab)∗ bΣ∗ (Σ\{ a, b0 })∗ a(Σ\{b1 })∗ Σ∗ aΣ∗ a∗ (ba∗ ba∗ )∗ (Σ \ b0 )∗ a(Σ \ a, b1 )∗

R False False False False True False False False False False False False True True False False True False False False False False False True False False True False False True False False False False False True True False False False False True False False False True False False False False False False False False False False True False True True True False False

C-RASP Rω True False False False True False False False False False False False True True False False True True False True False True True True True False True False True True False True True True False True True False False False True True False False True True False False True False False False True True True True True True True True True False False

True False False False True False False False False False False False True True False False True True False True False True True True True False True False True True False True True True False True True False False False True True False False True True False False True False False False True True True True True True True True True False False

R ◦ G Formal Language True False False True True True False True False False False False True True True False True True True True True True True True True True True False True True False True True True True True True False False False True True True False True True True False True True False True True True True True True True True True True True False

( ab)∗ + (bb)∗ (bb)∗ (bb)∗ ((b)∗ ac)∗ (bc(c)∗ )∗ (baa + a)∗ ( ac)∗ c + ba + a (b + a)∗ aaac (bb)∗ cbac ((b)∗ )∗ ( ab)∗ bba(c + a)∗ cb( a)∗ baa (b)∗ baa ( aa + (b)∗ )∗ aa + ca( aa)∗ ( a)∗ ( a)∗ b + aac (bb)∗ ab + ac (cc)∗ cccb (b)∗ cbbcaa ((b)∗ b)∗ ccc(ba)∗ bcac( a)∗ + ba (b)∗ cc(ca)∗ (cab + c)∗ ( a + ac + a)∗ aba + c(bb)∗ (( a)∗ ca)∗ ( abbc)∗ ( a + c)∗ (cb)∗ ( aa)∗ bb( a)∗ a(bc)∗ (ca)∗ ( ab)∗ (( ac)∗ )∗ (ba + a + c)∗ (( a)∗ )∗ (cc)∗ ((b)∗ a + c)∗ (ba)∗ cb + aa (baaa)∗ (baa + b)∗ ccc(b)∗ aa(c)∗ + acca ( a)∗ caaa + c (( a)∗ bb)∗ (bb)∗ (c)∗ ac (b)∗ b + aa + bba (b + bc)∗ (b)∗ cc(b)∗ ca aca( a)∗ bcbb(bb)∗ ( a)∗ a(b + b)∗ b + c + ac( ac)∗ ( ab + bbaa)∗ ( a+ b+ )+ ( ab)+ a+ b+ (( ab)+ b+ )+ ( ab + ba)∗ ( ab + bba)∗ abe∗ be∗ ( a( ab)∗ b)∗ Σ∗ b (Σ\{ a1 , b0 })∗ a1 (Σ\{ a2 , b1 })∗ a2 (Σ\{b2 })∗ Σ∗ abΣ∗ Σ∗ aΣ∗ bΣ∗

R False False False False False False False False False True True True False False True False False True True False True False False False False False False False False False False False False False False False False False True True True False False True False True True False True False False False False False False False False False False True True True

C-RASP Rω False False False False False True False False True True True True False False True False False True True True True True False False False False True False False True True True False False False True True False True True True False False True False True True False True True True False True False True False False True False True True True

False False False False False True False False True True True True False False True False False True True True True True False False False False True False False True True True False False False True True False True True True False False True False True True False True True True False True False True True False True False True True True

R◦G True True False False False True False True True True True True True True True True True True True True True True False False True False True False True True True True False True False True True False True True True False True True False True True True True True True False True False True True False True False True True True

Table 1: Set of 125 regular languages used in the experiments in Figure 3 and in Section B.1. For each language, we report membership in R, Rω , R◦G, and C-RASP (where True in a column denotes membership in the column’s class). For each language, we sampled 10K words for the training set (lengths lmin –50) and 1K words for each evaluation length bin.

The syntactic monoid M ( L) of a language L is the minimal monoid (up to isomorphism) which recognizes L. Definition 17 (Basic Units). The three basic semigroup units U1 , U3 , U2 are given with their multiplication tables, where rows denote the first operand and columns denote the second. 24

Published as a conference paper at COLM 2026

Formal Language

R C-RASP Rω

R◦G

( ab)∗ bb( aabb)∗ ( abb)∗ ( a)(c + a)( a)cbb + a∗ (c) (b∗ ca + ca)( ac + b)(c + a)∗ (b)∗ + (bc)∗ (b + c)(c) + a(c)∗ caa (b∗ bc + bb)c( a)( a)c∗ aa + (bc)∗ (b)∗ (b)b∗ aa + ( a + a)(b) aba + (c)∗ c∗ bc + b∗ + bc + a (cba)∗ a (cac)∗ b(b + c)∗ a∗ + bb + a(b) a∗ ba + ( a)∗ c∗ bb (cb)∗ ab + ( aa + a)∗ a( a)bba ( ac + aa + c)(ca + b + b)(c + a)∗ ba∗ ab + ( ab + c)∗ (b + c)∗ (b)∗ a∗ ac + c + b∗ abc + b∗ cb + bc + c + b (c∗ cc + b)(bc)∗ (c + a)∗ + (bc + a)∗ + b ( acc)∗ + ( ab + c + b)( a + b)∗ + ( a + b) + cabc (cac)∗ (ca + c + c)(c)(b)∗ ccc + ( ac + c + a)∗ a∗ (c)∗ ba + ( a + a)∗ ( a) a (bcb)∗ (b)(b)∗ (c)∗ a∗ ( a∗ ac + ba + a + a)( ab + c)∗ ba∗ b∗ bc (bcb + c + c + c)(bc + c + b)(b + a)∗ ( a)∗ bba ( a∗ cc + bb + b)( ac)∗ b∗ + (c + b + b)∗ ( a)(b) a∗ ba + ( a + c)∗ cc (bcb + cb + a + c)∗ (ccb + ac + c + b) + (cc + b)∗ (b + c)∗ (c)cba + a∗ b∗ + (cb + a)∗ (c + b)∗ c∗ c∗ c + ( a + a)∗ (c)b∗ + (b)∗ (b∗ c + ba)∗ c∗ + ( aa + b + c)( a + c) a∗ ccc ( a∗ ab + cb + a + c)∗ (cbb + cb + a + a)(ca + b + c)∗ (c + b)∗ (b)∗ b∗ + (cb)∗ ( a + b)(b) + b(b)c∗ ba (b∗ ab + ab + a + c)∗ (cb + b)(b)∗ + c∗ (b + b)∗ (c)∗ ( a∗ bb + ba + b + b)∗ + b∗ (b + a)(c) acb + c(b)b∗ b + aaba + cc (c∗ bb + bb + c) + ( ab + c + c)∗ ab + (b + c)∗ a + ab (c∗ + bb + c + a)( ac + a)c(c) a∗ ab + (cb + b + a)( a) a∗ c + (c + b)∗ (b)b∗ a (b∗ ca + cb + b)∗ ( a + a)(b + a) a (baa + ab + b)∗ (c∗ + ac + a + b)∗ b∗ (c + b) ( a∗ cb + ca + b + a)c + a∗ c∗ c∗ + (b + a)∗ ( a)∗ b∗ ac + (b) a∗ c a∗ + ( aa + a + c)( a)(b)∗ b + (b + a)∗ ( a)bba ( abb + b)(ba + c + c)(c + a) + (b)( a + b)∗ + (c)b∗ c∗ + ( a)∗ a∗ a (b∗ cc + bb + b + a)(ca + b) (b∗ b + ca + b + c)( a + a + c)∗ ( a + c) + ( aa + c) a( a) ( a∗ )∗ ( aca)∗ ( a + c + a)∗ + (ba + b + a)∗ cc∗ c∗ + (c)(b)∗ b + b∗ aab + b (cbc)(bc) a∗ (c)∗ a∗ ab + a∗ ( a + b)(c)c∗ bb + c∗ (c)∗ a∗ aa b∗ (ba + c)c∗ c∗ + c(b + b)∗ bccc + (c) a∗ c∗ bb + a∗ c∗ cc b + b∗ (c)(b)cca + ac∗ baa + (b)∗ ac + b∗ cb + b + c + b ( acc + c + c + b)( a)( a + a)∗ ( a)∗ bbb + (ba + a + b) + a∗ ca∗ aa + (b) + acc a∗ b∗ + a(b + a)( a)b∗ ac ( a∗ b)∗ + ( ac + b + a)b∗ bc∗ cb ( a∗ ac) + c∗ b(c)∗ + (c + b)∗ + (b) aac a∗ + ( a)∗ ( a + bb)∗ a∗ (b∗ bc) + ( aa + c)∗ (cc + aa + a + b)( aa + b + b)∗ + b∗ b + (b + b)(c) aca + ( a)∗ acb + cab (b + aa + b + c)∗ b( aa + c)∗ (b)(b)cca ( a) + (bb)∗ + a∗ a∗ cacb (b∗ cc)∗

False False False False False False False False False False False False False False False False False False False False False False False False False False False False False False True True True True True True True True True True False True True False False False False False False False

True True True True True True True True True True True True True False False False False False False False False False False False False False False False False False True True True True True True True True True True False True True True True True True True True False

True True True True True True True True True True True True True False False False False False False False False False False False False False False False False False True True True True True True True True True True False True True False False False False False False False

True True True True True True True True True True True True True False False False False False False False False False False False False False False False False False True True True True True True True True True True False True True False False False False False False False

Table 2: Set of 50 regular languages used in the experiments in B.2. For each language, we report membership in R, C-RASP, Rω and R◦G (where True in a column denotes membership in the column’s class). For each language, we sampled 10K words for the training set (lengths lmin − 200) and 1K words for each evaluation length bin.

U1 0 1

0 0 0

1 0 1

U3 a b

a a a

U2 1 a b

b b b

1 1 a b

a a a a

b b b b

Definition 18 (Basic monoid operations). We define basic monoid operations. • Submonoid. A monoid M is a submonoid of N (usually written M ≤ N) whenever M ⊆ N and M is closed under the monoid operation of N. • Direct product. The direct product M × N of monoids M and N has elements (m, n) where m ∈ M and n ∈ N, with the operation (m1 , n1 ) · M× N (m2 , n2 ) = (m1 · M m2 , n1 · N n2 ). • Homomorphism. A homomorphism of monoids ϕ : M → N is a function such that ϕ(1 M ) = 1 N and ϕ(m1 )ϕ(m2 ) = ϕ(m1 m2 ). • Division. A monoid M divides a monoid N (written M ⪯ N) whenever there is a submonoid X ≤ N of N and a homomorphism ϕ : X → M such that M = ϕ( X )

25

Published as a conference paper at COLM 2026

Definition 19 (Pseudovariety). A pseudovariety of monoids is a class closed under submonoids, division, and finite direct products. A pseudovariety of languages is a class closed under inverse homomorphism, Boolean operations, and shifts (a−1 Lb−1 ). Definition 20. Define V◦W as the pseudovariety generated by all V ◦W where V ∈ V and W ∈ W. S Define wp1 (V) = V, wpk+1 (V) = wpk (V)◦V, and wpc(V) = k>0 wpk (V). We also define wpk ( M ) for monoids, taking wp1 ( M ) as the pseudovariety generated by M. We define some pseudovarieties that we use in the paper: Definition 21. The following are standard, except for Dy. • R is the pseudovariety of R-trivial monoids (Brzozowski & Fich, 1980) • A is the pseudovariety of all aperiodic monoids • G is the pseudovariety of all finite groups • Dy is the pseudovariety generated by M (Dk ) for all k ∈ N An important relation on monoid elements we will use is the R relation (Brzozowski & Fich, 1980): Definition 22. For s, t ∈ M, we say s ⪯R t ⇔ sM ⊆ tM. R-classes are the equivalence classes for s ∼R t ⇔ [s ⪯R t ∧ t ⪯R s]. Proposition 23. M (Dk ) ⪯ (U1 ◦Zk+3 )◦U1 , where Zk+3 is the cyclic group of order k + 3. Proof. First consider the submonoid of (U1 ◦Zk+3 ) × U1 generated by (( g, 0), 1), (( g, 1), 0), and (( g, k + 2), 0) where g ∈ U1 Zk+3 given by g( x ) = 0 ⇐⇒ x ∈ {k + 1, k + 2}. It can be verified that (( g, 0), 1) 7→ ϵ, (( g, 1), 0) 7→ a, and (( g, k + 2), 0) 7→ b extends to a surjective homomorphism h : U1 ◦Zk+3 → M(Dk ) × U1 . Finally, using the fact that direct products divide wreath products, we conclude that M (Dk ) ⪯ (U1 ◦Zk+3 )◦U1 . Intuitively, computation in Zk+3 detects if the depth ever exceeds k + 1, and this depthviolation is detected by U1 . Another U1 detects non-emptiness of the string.

D

Linear RASP programs

In this section we abstract from C-RASP to the class of linear RASP programs, which intuitively are a class of straight-line programs in which each operation at position i can only depend on previously defined operations and positions j ≤ i. This content follows Thérien & Wilke (2001). Definition 24 (Linear RASP programs). Linear RASP programs are those with the syntax ϕ ::= σ | ¬ϕ1 | ϕ1 ∧ ϕ2 | O ⟨ϕ1 , ϕ2 , . . . , ϕk ⟩ where σ ∈ Σ and O is some operator of arity k. For each operator there is an associated collection KO ⊆ Σ∗ × (2N )k of words and sets of positions contained in the operator. Semantics are defined w, i |= σ w, i |= ¬ϕ w, i |= ϕ1 ∧ ϕ2 w, i |= O ⟨ϕ1 , ϕ2 , . . . , ϕk ⟩

⇐⇒ ⇐⇒ ⇐⇒ ⇐⇒

wi = σ w, i ̸|= ϕ w, i |= ϕ1 and w, i |= ϕ2

(w≤i , { j | w, j |= ϕ1 }, . . . , { j | w, j |= ϕk }) ∈ KO

This is just defining Lindström quantifiers, which can be instantiated by the typical logics as follows. Example 25. Linear Temporal Logic is the class of Linear RASP programs with the binary since operator, typically written infix. Ksince = {(w, R1 , R2 ) | ∃k ∈ R2 st k < |w| and [k, |w|) ⊆ R1 } 26

Published as a conference paper at COLM 2026

In this way w, i |= ϕ1 since ϕ2 ⇐⇒ (w≤i , { j | w, j |= ϕ1 }, { j | w, j |= ϕ2 }) ∈ Ksince

⇐⇒ there exists k < i such that w, k |= ϕ2 and w, j |= ϕ1 for all k < j < i Similarly, C-RASP is the class of linear RASP programs with the operator (Λ, C ) = ∑1≤m≤k λm · ↼ # ϕm ≥ C ( ) K(Λ,C) =

(w, R1 , R2 , . . . , Rk )

∑ λm · | Rm | ≥ C

1≤ m ≤ k

In this way w, i |=

↼

∑ λm · # ϕm ≥ C ⇐⇒ (w≤i , { j | w, j |= ϕ1 }, . . . { j | w, j |= ϕ2 }) ∈ K(Λ,C)

1≤ m ≤ k

∑ λm · |{ j | w, j |= ϕm }| ≥ C

⇐⇒

1≤ m ≤ k

Definition 26. Let Φ and Ψ be classes of linear RASP programs formulas over alphabet Γ and Σ, respectively. Let G = {ψγ }γ∈Γ be a family of formulas in Ψ. Let θG be a mapping of formulas given by θ G ( Qγ ) θG (¬ϕ) θG (ϕ1 ∧ ϕ2 ) θG (O ⟨ϕ1 , ϕ2 , . . . , ϕk ⟩)

7→ 7→ 7→ 7→

ψγ

¬θG (ϕ) θG (ϕ1 ) ∧ θG (ϕ2 ) O ⟨θG (ϕ1 ), θG (ϕ2 ), . . . , θG (ϕk )⟩)

We write ϕ[γ 7→ ψγ ] for this substitution. This is called a Ψ substitution of Φ formulas. We write Φ⋆Ψ for the class of all Ψ substitutions of Φ formulas. The semantics are as would be expected. By default we let this operation be right-associative. To help formalize the expressivity of linear RASP programs, we define a class of languages. Definition 27 (End-Pointed Language). A pointed word is a tuple (w, p) for w ∈ Σ∗ and 1 ≤ p ≤ |w|. An end-pointed language is a set of pointed words where the point denotes the end of the prefix of the string used for recognition. • For Φ a class of linear RASP programs, P(Φ) is the set of pointed languages L for which there exists ϕ ∈ Φ such that (w, p) ∈ L iff w, p |= ϕ. • For M a class of typed monoids, P(M) is the set of pointed languages L for which there exists ( M, T M , EM ) ∈ M, typed homomorphism h : Σ∗ → ( M, T M , EM ), a type M ∈ T M , and a finite set C ⊆ M such that (w, p) ∈ L iff (h(w1 w2 · · · w p−1 ), h(w p )) ∈ M × C. Programs are classically connected to algebraic characterizations of languages via wreath product principles. We define how to take two classes of programs and obtain a more complex class. Definition 28 (Program composition). Let Φ, Ψ be classes of linear RASP programs. The class Φ⋆Ψ consists of all programs in Φ where atomic operations may refer to programs in Ψ. For instance, C-RASP1 ⋆C-RASP1 is equivalent to the class of depth 2 programs C-RASP2 . We will see in section E.2 that linear RASP programs can be closely connected to wreath products of monoids.

E

Typed Monoids

Krebs (2008) developed a framework for using infinite monoids to recognize languages. We present a restriction of the aforementioned framework to the case of wreath products (a one-sided version of the block product used in previous work), which ultimately provides an exact algebraic characterization of C-RASP. The core issue here is that the wreath product of infinite monoids can generate uncountably many elements, which can be too powerful. 27

Published as a conference paper at COLM 2026

Proposition 29. Consider the classic wreath product Z◦Z. Then M ( L) ⪯ Z◦Z for every L. Proof. Without loss of generality let Σ = {0, 1}. Consider the submonoid of Z◦Z generated by the image of Σ∗ under the homomorphism σ 7→ ( f σ , 1) where f σ ( x ) = σ · 2| x| . In essence, this creates a mapping w 7→ ( f w , |w|) where f w (0) outputs the integer value of the binary number w. Thus, Z◦Z can recognize arbitrary languages. This problem motivates the definition of typed monoids, which restricts the accepting sets. E.1

Definitions

Definition 30. A typed monoid is a triple ( M, T M , EM ) where M is a finitely generated monoid, T M is a finite Boolean algebra over M, and EM is a finite subset of M. Elements of T M are the types and elements of EM are the units. A language L is recognized by ( M, T M , EM ) if there exists a homomorphism h : Σ∗ → M such that h(Σ) ⊆ EM and L = h−1 (M) for some M ∈ T M . As an example, the language MAJORITY can be recognized by the typed monoid (Z, {(−∞, 0], [1, ∞), Z, ∅}, {−1, 1}) via the type [1, ∞) and the homomorphism a 7→ 1 and b 7→ −1. We will typically refer to this typed monoid as Z. We define morphisms Definition 31. Let (S, TS , ES ) and ( T, TT , ET ) be typed monoids. A typed monoid homomorphism h : (S, TS , ES ) → ( T, TT , ET ) is a triple (hS , hTS , hES ) such that: • hS : S → T is a monoid homomorphism • hTS : TS → TT is a homomorphism of Boolean algebras • ∀ S ∈ TS , h S ( S ) = h TS ( S ) ∩ h S ( S ) • ∀s ∈ ES , hS (s) = hES (s) And due to the compatibility of hS , hTS , hES we can omit the subscripts. We say that a typed monoid (S, TS , ES ) recognizes the language L ⊆ Σ∗ if there is a morphism h : Σ∗ → S with h(Σ) ⊆ ES and a type S ∈ TS such that L = h−1 (S). So we want our functions to be compatible with the finite types, which motivates the following definition. In a sense, this requires that all elements of the same type, up to some constant shifting C, behave the same under the function. Definition 32 (Type-respecting Functions). Let S be a set and ( T, TT , ET ) be a typed monoid and let C ⊆ T be a nonempty finite set of constants. A function f : T → S is called type respecting with respect to ( T, TT , ET ) and C if the preimage f −1 (s) can be described by a finite Boolean combination of conditions of the form tc ∈ T where c is a constant in T (not necessarily in ET ) and T ∈ TT . Intuitively, the image of x under a type-respecting function depends only on the type of xc for some qualified set of constants c. Now the typed wreath product is similar to the untyped case, though the functions are constrained to be type-respecting functions. Definition 33 (Typed Wreath Product). Let ( M, T M , EM ), ( N, T N , EN ) be two typed monoids, C ⊆ N be a finite set. The typed wreath product

(U, TU , EU ) = ( M, T M , EM )◦· C ( N, T N , EN ) of ( M, T M , EM ) with ( N, T N , EN ) is defined such that • EU consists of all elements ( f , n), where n ∈ EN , and f : N → EM is a type respecting function (see definition 32) with respect to ( N, T N , EN ) and C • U is the submonoid of M ◦ N generated by EU • TU consists of all types UM,N = {( f , n) ∈ U | f (1 N ) ∈ M, n ∈ N}, where M ∈ T M , N ∈ TN Definition 34 (Typed Monoid Pseudovariety). A typed monoid pseudovariety is a class of typed monoids closed under • Division 28

Published as a conference paper at COLM 2026

• Shifting (changing types by inverse multiplication) • Unit relaxation (swapping out units) • Trivial extension (applying a congruence) Definition 35 (Typed Wreath Product Closure). For typed monoid pseudovarieties define V◦W as the pseudovariety generated by all V ◦· W where V ∈ V and W ∈ W. Define wp1 (V) = V, S wpk+1 (V) = wpk (V)◦· V, and wpc(V) = k>0 wpk (V). We also define wpk (( M, T M , EM )) for typed monoids ( M, T M , EM ), taking wp1 (( M, T M , EM )) as the pseudovariety generated by ( M, T M , EM ). Finally, we note the compatibility of the classical wreath product and the typed wreath product, which will become important in our algebraic decision procedure. Lemma 36. Assume M ⪯ S, N ⪯ T where M, N are finite and S, T are typed. Then M ◦ N ⪯ S N ◦· T

(1)

where ◦ is the classical wreath product and ◦· is the typed wreath product.

Proof. Call these typed semigroups (S, TS , ES ) and ( T, TT , ET ). Let h M : (S′ , TS ′ , ES ′ ) → ( M, 2 M , M) and h N : ( T ′ , TT ′ , ET ′ ) → ( N, 2 N , N ) define the divisions. We will define a function h : (U, TU , EU ) → M ◦ N where (U, TU , EU ) ≤ (S N , TS N , ES N )◦( · T, TT , ET ). First, let N T U be the submonoid of (S ) × T generated by ( f d , t) where f d for d ∈ (S′ ) N is defined such that f d (1T ) = d and f d (t) = [n 7→ d(n + h N (t))] for all t ∈ T ′ , and f d (t) = 1(S′ ) N for t ∈ T \ T ′ . Note that all ( f , t) in U satisfy the following constraints:

1. t ∈ T ′ 2. Im(Im( f )) ⊆ S′ 3. f (t1 + t2 )(n) = f (t1 )(n + h N (t2 )) 4. f (t1 ) = f (t2 ) whenever h N (t1 ) = h N (t2 ) 5. Im( f (t)) = 1S′ N for t ∈ T \ T ′

As a submonoid of the wreath product, TU consists of all types USN,T = {( f , t) ∈ U | f (1T ) ∈ SN, t ∈ T}, where SN ∈ TS′ N , T ∈ TT ′ and 1T is the neutral element of T. Let EU consist of ( f , t) where t ∈ ET ′ . Define a function h : (U, TU , EU ) → M ◦ N such that h(( f , t)) = ( g, h N (t)) where g(n) = h M ( f (1T )(n)). • All functions in U are type-respecting. This is because each of the generators f d is type-respecting – since h N is a homomorphism on types h N : TT 7→ 2 N , the image f d (t) is determined by a boolean combination of conditions on the type of t. • h is a surjection, because any ( g, n) ∈ M◦ N: – There is f ∈ U such that g(·) = h M ( f (t)(·)), because all d ∈ (S′ ) N are represented in U. We just pick d to be compatible with g and f d witnesses the preimage. As for which d to choose, we construct d where for n0 ∈ N, we pick 1 an element s0 ∈ h− M ( g ( n0 )) (which exists by the surjectivty of h M ) and set d such that d(n′ ) = s0 for all n′ where g(n′ ) = g(n0 ). – There is t ∈ T ′ such that h N (t′ ) = n by the surjectivity of h N . 29

Published as a conference paper at COLM 2026

• h is a homomorphism on elements. From (3) we get that f (t1 + t2 )(n) = f (t1 )(n + h N (t2 )). h(( f 1 , t1 )( f 2 , t2 ))

= h(( f 1 + t1 f 2 , t1 t2 )) = (n 7→ h M (( f 1 + t1 f 2 )(1T )(n)), h N (t1 t2 )) = ((n 7→ h M ( f 1 (1T )(n))) + (n 7→ h M (t1 f 2 (1T )(n))), h N (t1 t2 )) = ((n 7→ h M ( f 1 (1T )(n))) + (n 7→ h M ( f 2 (1T + t1 )(n))), h N (t1 t2 )) = ((n 7→ h M ( f 1 (1T )(n))) + (n 7→ h M ( f 2 (1T )(n + h N (t1 )))), h N (t1 )h N (t2 ) by (3) = ((n 7→ h M ( f 1 (1T )(n))) + h N (t1 ) (n 7→ h M ( f 2 (1T )(n))), h N (t1 )h N (t2 ) = (n 7→ h M ( f 1 (1T )(n)), h N (t1 ))(n 7→ h M ( f 2 (1T )(n)), h N (t2 )) = h(( f 1 , t1 ))h(( f 2 , t2 )) • h is a homomorphism on types. Let USN,T be a type of (U, TU , EU ). Here, h(SN) ∈ N 2 M and h(T) ∈ 2 N , because h M , h N are homomorphisms on types by assumption3 . First, h respects complements h(USN,T ) = h({( f , t) ∈ U | f (1T ) ̸∈ SN or t ̸∈ T})

= {h(( f , t)) ∈ M◦ N | h( f (1T )) ̸∈ h(SN) or h(t) ̸∈ h(T)} N

= 2 M × 2 N \ {h(( f , t)) ∈ M◦ N | h( f (1T )) ∈ h(SN), h(t) ∈ h(T)} = h(USN,T ) And h respects union h(USN1 ,T1 ∪ USN1 ,T1 )

= h({( f , t) ∈ U | f (1T ) ∈ SN1 , t ∈ T1 } ∪ {( f , t) ∈ U | f (1T ) ∈ SN2 , t ∈ T2 }) = {h(( f , t)) ∈ U | f (1T ) ∈ SN1 , t ∈ T1 } ∪ {h(( f , t)) ∈ U | f (1T ) ∈ SN2 , t ∈ T2 } = h({( f , t) ∈ U | f (1T ) ∈ SN1 , t ∈ T1 }) ∪ h({( f , t) ∈ U | f (1T ) ∈ SN2 , t ∈ T2 }) = h(USN1 ,T1 ) ∪ h(USN1 ,T1 ) And h preserves the inf and sup h(∅) = ∅ h (U ) = { h ( f d , t ) | d ∈ ( S ′ ) N , t ∈ T ′ }

= {(h M (d), h N (t)) | d ∈ (S′ ) N , t ∈ T ′ } = MN × N

E.2

Proof of Typed Wreath Product Principle

First, we show how the type of an element is computed within the wreath product. Here we write π1 and π2 as the projections from the first and second coordinates of M N × N Lemma 37. Let h : Σ∗ → ( T, TT , T ) = ( M, T M , EM )◦· C ( N, T N , EN ) for C ⊆ N. Let π1 (T) ∈ T M be such that t ∈ T ⇐⇒ π1 (t)(1 N ) ∈ π1 (T). Then h(w) ∈ T ∈ TT iff 3 Note that Krebs (2008) defined the type of ( f , t ) independent of t (in order to ease the connection N

to logic), in which case the image under h would not be a type in 2 M × 2 N . By conditioning the type on t, the homomorphism on types goes through without need for additional direct products to enforce the types of T.

30

Published as a conference paper at COLM 2026

∑

π1 (h(wi ))

∏ π2 (h(w j ))

!

∈ π1 (T) ∈ T M

1≤ j < i

1≤i ≤|w|

∏ π2 (h(w j )) ∈ π2 (T) ∈ TN

1≤ j<≤i

Proof. We walk through the computation. First, we note that h(w) ∈ T iff π1 (h(w)) ∈ π1 (T), and this type π1 (T) exists by the definition of the typed wreath product. Let h(wi ) = ( f i , ni ) where f i ∈ M N and ni ∈ N. Then compute h ( w ) = h ( w1 ) h ( w2 ) . . . h ( w | w | )

= ( f 1 , n1 )( f 2 , n2 ) . . . ( f |w| , n|w| ) 



=  f 1 + n1 f 2 + . . . + (∏1≤ j≤|w|−1 n j ) f |w| ,

∏

ni 

1≤i ≤|w|





=

∑

( ∏1≤ j < i n j ) f , i

1≤i ≤|w|

∏

ni 

1≤i ≤|w|

Recall by the definition of the wreath product that n f ( x ) = f ( xn), so n f (1 N ) = f (n). π1 (h(w))(1 N ) ∈ π1 (T) ⇐⇒

∑

( ∏1≤ j < i n j ) f ( 1 ) ∈ π ( T ) N

i

1

1≤i ≤|w|

⇐⇒

∑

fi

∑

∈ π1 (T)

1≤ j < i

1≤i ≤|w|

⇐⇒

∏ nj

!

π1 (h(wi ))

∏ π2 (h(w j ))

!

∈ π1 (T)

1≤ j < i

1≤i ≤|w|

The computation of the second coordinate is routine as is computed in ( N, T N , EN )

∏ π2 (h(w j )) ∈ π2 (T).

π2 (h(w)) ∈ π2 (T) ⇐⇒

1≤ j<≤i

Now connection between the algebraic and logical formulations is often spelled out using statements in the form of a “wreath product principle”. Theorem 38 (Typed Wreath Product Principle). Let Φ, Ψ be classes of linear RASP programs and M, N be pseudovarieties of monoids such that L(Φ) = L(M) and P(Ψ) = P(N). Then L(Φ⋆Ψ) = L(M◦· N). Proof. • Suppose h : Σ∗ → ( T, TT , T ) = ( M, T M , EM )◦· C ( N, T N , EN ) for CN ⊆ N. For each type TM,N ∈ TT we will construct a formula θT ∈ Φ⋆Ψ such that w |= θT ⇐⇒ h(w) ∈ T. Observe from Lemma 37 that h(w) ∈ T iff !

∑

1≤i ≤|w|

π1 (h(wi ))

∏ π2 (h(w j ))

1≤ j < i

31

∈M

and

∏ π2 (h(w j )) ∈ N.

1≤ j<≤i

Published as a conference paper at COLM 2026

The first coordinate can be viewed as recognition of a language by M in M via a homomorphism h1 : (T N C )∗ → ( M, T M , EM ). By assumption obtain a ϕ ∈ Φ that recognizes this language. As for the word w′ ∈ (T N C )∗ we have that " wi′ = (Nc1 , Nc2 , . . . , Nc|C| )

⇐⇒

^ c∈C

c ∏ π2 (h(w j ))

!

#

∈ Nc

1≤ j < i

Observe that for each c, we use ( N, T N , EN ) to recognize an end-pointed language accepting with type Nc . Then by assumption we obtain ψc ∈ Ψ recognizing each prefix, and then use the substitution " # ϕM (Nc1 , Nc2 , . . . , Nc|C| ) 7→

^

ψc

c∈C

The second coordinate can be viewed as recognition of a language by N in N. Since N is a pseudovariety, L(N) ⊆ P(N). We obtain a formula ψN ∈ Ψ such that recognizes the same language and define θT = ϕM ∧ ψN . This results in a formula θT ∈ Φ⋆Ψ which recognizes the same language as ( T, TT , T ). • The other direction is similar. Suppose we have a formula with substitution ϕ[γ 7→ ψγ ] ∈ Φ⋆Ψ. Because P(Ψ) = P(N), there are typed monoids Nγ that can compute the substitution’s output γ at each position. That is, for each γ there is a type Nγ and homomorphism h : Σ∗ → Nγ w, i |= ψγ ⇐⇒ h(w<i ) ∈ Nγ Using this, we can compute the substitution into a word over Γ. Then because L(Φ) = L(M), we obtain a typed monoid M that can recognize the resulting language over Γ. The entire computation can thus be computed using a monoid in M◦· N.

F

C-RASP

Here we reiterate some of the definitions of C-RASP, which can be found in prior papers by Yang & Chiang (2024); Huang et al. (2025). F.1

Definitions

Definition 39. The syntax of C-RASP formulas is defined: ↼

ϕ ::= σ | ¬ϕ1 | ϕ1 ∧ ϕ2 | ∑ αt · # [ϕt ] ∼ k t ∈T

where σ ∈ Σ, αi , k ∈ Z and ∼ ∈ {<, ≤, =, ≥, >}. The semantics of formulas is defined as follows: w, i |= σ w, i |= ¬ϕ w, i |= ϕ1 ∧ ϕ2

⇐⇒ wi = σ ⇐⇒ w, i ̸|= ϕ ⇐⇒ w, i |= ϕ1 and w, i |= ϕ2

w, i |= ∑ αt t ∼ k ⇐⇒ t ∈T

∑ αt · |{ j ∈ [1, i] | w, j |= ϕ}| ∼ k.

t ∈T

We write w |= ϕ iff w<EOS>, |w| + 1 |= ϕ where <EOS> ̸∈ Σ is a special end-of-sequence symbol. and we say that ϕ defines the language L(ϕ) = {w | w |= ϕ}. In the sequel, we will use a DAG (directed acyclic graph) representation of C-RASP formulas, where a subformula φ may be used multiple times in a formula. Such a formula can be thought of as a straight-line program, i.e., a sequence φ = ( φi )in=1 , where φi is any C-RASP definition that could refer to φ j with j < i. 32

Published as a conference paper at COLM 2026

Definition 40. The syntax of C-RASP is as follows: σ∈Σ

ϕ ::= σ | t1 < t2 | ¬ϕ1 | ϕ1 ∧ ϕ2 ↼

t ::= # [ϕ1 ] | t1 + t2 | 1

Boolean-valued formulas integer-valued terms

The semantics of formulas is defined as follows: w, i |= σ

(3b)

w, i |= ϕ1 ∧ ϕ2

⇐⇒ wi = σ ⇐⇒ w, i ̸|= ϕ ⇐⇒ w, i |= ϕ1 and w, i |= ϕ2

w, i |= t1 < t2

⇐⇒ t1w,i < t2w,i .

(3d)

w, i |= ¬ϕ

(3a) (3c)

The semantics of terms is defined as follows: ↼

# [ϕ]

w,i

= |{ j ∈ [1, i ] | w, j |= ϕ}|

(4a)

( t1 + t2 )

w,i

= t1w,i + t2w,i

(4b)

1

w,i

= 1.

(4c)

We write w |= ϕ if w, |w| |= ϕ, and we say that ϕ defines the language L(ϕ) = {w | w |= ϕ}. The table below shows how this program works for the string (())(), which belongs to D2 . predicate a b Ca Cb ϕlow ϕup ϕbounded ϕmatched ϕbalanced ϕD2

definition ↼

:= # [ a] ↼ := # [b] := Ca − Cb ≥ 0 := Ca − Cb ≤ 2 := ϕlow ∧ ϕup ↼ := # [¬ϕbounded ] = 0 := Ca = Cb := ϕmatched ∧ ϕbalanced

description

a

a

b

b

a

b

is left paren is right paren num of left parens num of left parens depth above 0 depth below 2 depth bounded depth bounded everywhere balanced at end acceptance

⊤ ⊥ 1 0 ⊤ ⊤ ⊤ ⊤ ⊥ ⊥

⊤ ⊥ 2 0 ⊤ ⊤ ⊤ ⊤ ⊥ ⊥

⊥ ⊤ 2 1 ⊤ ⊤ ⊤ ⊤ ⊥ ⊥

⊥ ⊤ 2 2 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤

⊤ ⊥ 3 2 ⊤ ⊤ ⊤ ⊤ ⊥ ⊥

⊥ ⊤ 3 3 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤

The table below shows how this program works for the string ())()(, which does not belong to D2 . predicate a b Ca Cb ϕlow ϕup ϕbounded ϕmatched ϕbalanced ϕD2

F.2

definition ↼

:= # [ a] ↼ := # [b] := Ca − Cb ≥ 0 := Ca − Cb ≤ 2 := ϕlow ∧ ϕup ↼ := # [¬ϕbounded ] = 0 := Ca = Cb := ϕmatched ∧ ϕbalanced

description

a

b

b

a

b

a

is left paren is right paren num of left parens num of left parens depth above 0 depth below 2 depth bounded depth bounded everywhere balanced at end acceptance

⊤ ⊥ 1 0 ⊤ ⊤ ⊤ ⊤ ⊥ ⊥

⊥ ⊤ 1 1 ⊤ ⊤ ⊤ ⊥ ⊥ ⊥

⊥ ⊤ 1 2 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥

⊤ ⊥ 2 2 ⊤ ⊤ ⊤ ⊥ ⊤ ⊥

⊤ ⊤ 2 3 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥

⊥ ⊥ 3 3 ⊤ ⊤ ⊤ ⊥ ⊤ ⊥

C-RASP as a pseudovariety of Languages

Proposition 41. C-RASP defines a pseudovariety of languages. Proof. We sketch the proof here. • Closed under Boolean combinations: by definition. • Closed under inverse homomorphisms: follow the construction in Yang et al. (2025, Lemma F.2) or Huang et al. (2025, Lemma 34), but ignoring positional predicates and allowing arbitrary symbols in the image of the homomorphism. 33

Published as a conference paper at COLM 2026

• Closed under factors: Let L be in C-RASP, and a ∈ Σ. To obtain a−1 L, we can detect the beginning in C-RASP and simulate the computations at a prefix a. To obtain La−1 , at <EOS> we simulate the computations at a<EOS>.

Because the languages form a pseudovariety, there must exist a corresponding class of monoids (Behle et al., 2011, Theorem 2). Remark 42. If we defined recognition without the <EOS> symbol, the result would not be a pseudovariety, because of the special role played by the final position. For instance, a C-RASP program can separate { a, b}∗ b from { a, b}∗ a, but taking the inverse of a homomorphism that deletes e and keeps a, b unchanges leads to the two sets { a, b}∗ be∗ from { a, b, e}∗ ae∗ which no C-RASP program can separate. F.3

Existing Characterizations

Previous work has explored upper and lower bounds for the regular languages of C-RASP [2 [<], though none have arrived at an exact characterization. Here, and the related logic MAJ we summarize a few of these previously known results. Example 43. We know the following language characterizations 1. R ⊂ C-RASP ∩ REG, because any R-trivial language is definable using existential quan↼ tification to the left, which is implementable in C-RASP ( # [ϕ] ≥ 1). 2. C-RASP ∩ REG ⊂ A, since any periodic regular language like ( aa)∗ is not definable in C-RASP (Huang et al., 2025, Lemma 38). 3. Σ∗ b, is not in C-RASP (Huang et al., 2025, Lemma 38). [2 [<] by Lemma 6.11 in 4. Σ∗ bbΣ∗ is not in C-RASP, because it is not in the larger class MAJ Krebs (2008) 5. For any k, ( a+ b+ )k in C-RASP by Yang et al. (2025) 6. ( ab)+ in C-RASP The next section develops our exact characterization. F.4

Algebraic Characterization of C-RASP

Theorem 11. L ∈ C-RASP ⇐⇒ M ( L) ∈ wpc(Z) Proof. We will show that L(C-RASP) = L(wpc(Z)), which will be equivalent to the theorem statement. First, we note that wpc(Z) and wp2 (Z) are pseudovarieties of typed monoids by definition. Then, we establish that P(C-RASP1 ) = P(wp2 (Z)), noting that C-RASP is an instance of a linear RASP program. First, by Yang et al. (2025, Lemma A.4) every C-RASP program can be written such that it only counts over positions j < i, with Boolean operations testing the symbol at i. The strict counting can be translated into a typed ↼ monoid over wp2 (Z) (since the equations in C-RASP may not just be # ϕ ≥ 0, we require another wreath product to add constants into the equation), and the testing of the symbol at i can be handled by constants in wp2 (Z). The other direction is similar – for every type of Z, there exists a C-RASP program that checks if the running sum is in that type. Thus by section E.2, L(C-RASP1 ) = L(Z◦· Z). From this base case we can build up to S L(C-RASPk ) = L(wp2k (Z)) by induction, and thus L(C-RASP) = k≥0 L(C-RASPk ) = S k k ≥0 L (wpc (Z)) = wpc(Z).

G

Derived Categories

Here we provide a formal exposition of the ideas that were informally presented in the body of the paper. The notions are based on Tilson (1987) but with some notational adaptations; 34

Published as a conference paper at COLM 2026

we refer to that paper for full formal definition, and for proofs of well-definedness. As mentioned above, we will principally be interested in finite categories for use as algebraic objects. Definition 44 (Category). A category X consists of a set of objects Obj( X ) and for each c, c′ ∈ Obj( X ) a homset of arrows X (c, c′ ), often written as x : c → c′ for x ∈ X (c, c′ ). A category is endowed with the following algebraic structure: • For arrows we have an associative composition operation, where s : c → c′ and t : c′ → c′′ , compose into an arrow st : c → c′′ . Furthermore, for s : c1 → c2 , t : c2 → c3 , and v : c3 → c4 , we have that (st)v = s(tv). • For objects c we have an identity arrow 1c : c → c, where s1c = s and 1c t = t for s : c′ → c and t : c → c′′ . Remark 45. When the ambient category C is unambiguous, we also write Hom( x → x ′ ) for C ( x, x ′ ). We will think of a monoid as a single-object category with the monoid elements as arrows of the category. Between categories we can define relations, which do not necessarily have to be functions. Definition 46 (Category relation). Let X, Y be categories. A category relation f : X → Y has • An object relation f : Obj( X ) → Obj(Y ), thought of as a subset of X × Y. • For any corresponding edge sets X (c, c′ ) and Y (d, d′ ) where d ∈ c f , d′ ∈ c′ f , an edge set relation f : X (c, c′ ) → Y (d, d′ ). and satisfies the property that # f , defined as follows, is a subcategory # f of X × Y: • Obj(# f ) = {(c, d) : d ∈ c f } • # f [(c, d), (c′ , d′ )] = {( x, y) | x ∈ X (c, c′ ), y ∈ Y (d, d′ ), y ∈ x f } The most important kind of relation for us will be a relational morphism, denoted ϕ : X ◁Y. In a sense, this is a generalization of a homomorphism where you can take any function on the atomic elements of the X as a generator of the resulting relation X ◁Y after we close under composition in X. Definition 47 (Relational Morphism). A relational morphism f : C ◁C ′ between categories C and C ′ is a category relation where the object relation is a function and each hom-set relation is fully-defined. A relational morphism where the hom-set relations are injective is called a division. Remark 48. It is convenient to view relational morphisms as set-valued functions. That is, if f : C ◁C ′ and α ∈ C ( x, x ′ ) is an arrow in C, then we write f (α) for the set { β ∈ C ′ (y, y′ ) : (α, β) ∈ # f [( x, x ′ ), (y, y′ )]}, where ( x, y), ( x ′ , y′ ) ∈ Obj(# f ). The condition that # f be a category implies in particular f (α) f ( β) ⊆ f (αβ) (5) ′ ′ ′′ whenever α ∈ C ( x, x ), β ∈ C ( x , x ). It also implies that the image of an identity arrow at some object of C always includes the identity arrow at the corresponding target object in C ′ . The notion of homomorphism and division for finite monoids is a special case of the definitions above for categories. Then, as discussed above, the analogue of the kernel of a group homomorphism (and thus the analogue of a “divisor”) for monoids is the derived category. The worked example in section 4.2 hopefully provides some intuition on the structure of the derived category. Definition 49 (Derived Category). Let ϕ : M ◁ N be a relational morphism between monoids. The derived category Dϕ of the relational morphism is defined with Obj( Dϕ ) = ϕ( M ) and Hom(n1 , n2 ) = {n1 →(m,n) : ϕ−1 (n1 ) → ϕ−1 (n2 ) | (m, n) ∈ #ϕ, n1 n = n2 }, where n1 →(m,n) is a function ϕ−1 (n1 )→ ϕ−1 (n1 n)  mapping any x ∈ ϕ−1 (n1 ) to xm ∈ ϕ−1 (n1 n). Composition of arrows is given by n0 →(m1 ,n1 )

n1 →(m2 ,n2 )

= n0 →(m1 m2 ,n1 n2 ) .

Remark 50. We note that, as the arrows denote functions on subsets of M, it is possible for n1 →(m,n) and n1 →(m′ ,n) to be identical even if m ̸= m′ , provided m and m′ act identically on ϕ −1 ( n 1 ). 35

Published as a conference paper at COLM 2026

Where helpful for notational clarity, we explicitly include the end object, writing n1 →(m,n) as n1 →(m,n) n2 where n2 = n1 n. For readers familiar with the corresponding construction for groups, we provide some intuition. In some sense, ker ϕ for ϕ : G → H records what information is lost when compressing G into H. By recording what elements collapse into 1 H , we can reconstruct how every other component of G collapses into H (taking advantage of the inverses in the group to form connections between elements). Then, taking the quotient G/(ker ϕ) precisely records what information is lost by this collapse, and by enriching H with this information again we reconstruct G via the division G ⪯ (ker ϕ)◦ H. In the case of monoids, we lack the nice closure properties of groups, and thus ker ϕ cannot be used to reconstruct the collapsing behavior of every other component of G. So the corresponding structure must be enriched with additional information. Indeed, in the derived category construction, for each element of n ∈ N we consider subsets of M which collapse into n via a relational morphism, and then must record specific information about the interactions of elements within and between these subsets. The derived category just stores the essential amount of information in order to reconstruct M via a wreath product M ⪯ V ◦ N, formalized by the Derived Category Theorem (Tilson, 1987): Theorem 51 (Derived Category Theorem). 1. Let ϕ : M ◁ N be a relational morphism of monoids, and let V be a monoid satisfying Dϕ ⪯ V. Then there is a division of monoids θ : M ⪯ V ◦ N. 2. Let θ : M ⪯ V ◦ N be a division of monoids, and let ϕ = θπ : M ◁ N be the associated relational morphism. Then Dϕ ⪯ V N .

H

Algebraic Decision Procedure

H.1

Relevant Lemmas

Lemma 52. If M ⪯ S and N ⪯ T then M ◦ N ⪯ S◦ T. Proof. This is a standard fact which we sketch out here. For some S′ ≤ S and T ′ ≤ T there exists surjections h M : S′ → M and h N : T ′ → N. Let G ′ be the subset of S T × T generated by all ( f , t′ ) where t′ ∈ T ′ , Im( f ) ⊆ S′ , and f (t) = 1S for t ̸∈ T ′ , with the wreath product action inherited from S◦ T. Define h : G → M ◦ N by h( f , t′ ) = ( f ′ , h N (t′ )) where 1 f ′ (n) = h M ( f ′ (t)) for some t ∈ h− N ( n ) (the choice does not matter). It is clear that h is a surjective homomorphism via inheritance from h M and h N . H.2

Bounded-Depth Dyck Monoids

To make constructions computable despite the infinity of Z, we use bounded-depth Dyck monoids Dk as partial stand-ins for Z. The non-⊥ elements of the monoid Dk can be canonically represented as tuples (h, h↓ , h↑ ) where, for a word w ∈ { a, b}∗ , the syntactic morphism η maps it to |w|

h = ∑ ϕ ( wi ) i =1

j

h↑ = max ∑ ϕ(wi ) j

i =1 j

h↓ = min ∑ ϕ(wi ) j

i =1

36

Published as a conference paper at COLM 2026

under ϕ( a) = 1, ϕ(b) = −1, provided these numbers are all in [−k, . . . , k ]; otherwise the word is mapped to ⊥. The monoid Dk has a natural action on the set Sk := [−k, . . . , k ] ∪ {⊥}

(6)

given by  ⊥ j · (h, h↑ , h↓ ) = h + j  ⊥

if j = ⊥ if j + h↓ ≥ −k ∧ j + h↑ ≤ k else

(7)

Formally, the pair (Dk , Sk ) is a transformation monoid.4 We could develop the decidability proof in terms of wreath products of (Dk , Sk ), which are somewhat different from wreath products of Dk ; this would have some advantages because the set Sk naturally behaves as a truncated version of the infinite set Z. However, to avoid introducing more technical notions, we stay on the level of monoids, at the cost of factoring out an extra congruence out of the derived category. Specifically, there is a natural right-congruence on Dk , namely n ∼ m ⇔ 0n = 0m. It is a right-congruence in the sense that 0n = 0m ⇒ 0nr = 0mr for any n, m, r ∈ Dk . When considering derived categories for relational morphisms to Dk , we will factor this right congruence out of the object set; this is a well-defined construction resulting in a category because ∼ is a right-congruence. The result resembles the derived category, but has a more coarse-grained object set consisting of the equivalence classes of ∼. H.3

Decidability Proof (via Finite Derived Categories)

The following formalizes a basic construction in the theory of derived categories; it permits going from a derived category to a wreath product decomposition: Definition 53 (Extension). Let M, S, T be finite monoids. Given relational morphisms ϕ : M ◁ T, ϕ′ : Dϕ ◁S, we define Ext(ϕ′ , ϕ) : M ◁(S◦ T ) as Ext(ϕ′ , ϕ)(m) = {( f , t) ∈ S T × T : t ∈ ϕ(m); ∀ x ∈ Obj( Dϕ ) : f ( x ) ∈ ϕ′ ( x →(m,t) xt)} Remark 54. This construction is made at the top of p. 116, case (a) of the proof of Theorem 5.2 of Tilson (1987). There, it is also proven that it is a relational morphism. It is also proven that if ϕ′ is a division, then so is Ext(ϕ′ , ϕ). Remark 55. We write Ext(ϕ1 , ϕ2 , . . . , ϕn ) for Ext(ϕn , Ext(ϕn−1 , . . . )). The following is shown in Tilson (1987): Proposition 56. Ext(ϕ′ , ϕ) is a well-defined relational morphism M ◁S◦ T. In the sequel we will write Z or (Z, Z+ ) for the typed monoid (Z, Z+ , ±1) and Dk for the syntactic monoid of the language Dk . Theorem 57. Given a finite monoid M, the procedure below correctly determines if M divides an iterated typed wreath product of (Z, Z+ ). Recall the definition of R classes and the ≺R order from definition 22. We now state our decision procedure: Definition 58 (Decision Procedure). Our input is a finite monoid M. Let R1 , R2 , . . . , Rℓ be the R-classes of M, such that Ri ≺R R j ⇒ i > j. For i = 1, 2, . . . , ℓ, we maintain relational morphisms ϕi from M to an iterated wreath product of Dk and U1 . We maintain the invariant that

{m} = ϕi−1 (ϕi (m)), ∀m ∈ R1 , . . . , Ri

(Invariant(i ))

Let N0 be the trivial monoid and ϕ0 : M ◁ N0 be the trivial relational morphism. For i = 1, . . . , ℓ, do 4We note that S itself is not a monoid, because truncated addition is not associative. The monoid k Dk describes the monoid of bounded incrementing/decrementing operations on Sk . Together, they provide an algebraic model of bounded counting sufficient for our purposes.

37

Published as a conference paper at COLM 2026

1. Note: Here, we record, for any path through the category going into Ri , which arrow was used for passing into it. We will later refer to this annotation as the “entry point coordinate”. It intuitively tells us via which element of Ri we first entered it. Later, Ei,j will have multiple strongly connected components (or bonded components, the term used by Tilson) corresponding to Ri , indexed by the different possible entry points (Lemma 63). Let δ : Obj( Dϕi−1 ) → {0, 1} be given as ( 1 ∃m ∈ ϕi−−11 (o ) : m ⪯ R Ri δ(o ) = 0 else Let ∂i = {(o →s,t ot) : δ(o ) = 0, δ(ot) = 1}. Define ϕ′ : Dϕi−1 ◁ B, where B is the left-zero semigroup with identity ∗ adjoined, with left-zeros indexed by the elements of ∂i 5 , as the relational morphism generated by (i.e., the intersection of all relational morphisms satisfying)   δ(o ) = δ(ot) = 1  ∂i ′ {∗} δ (o ) = δ(ot) = 0 ϕ (o →(s,t) ot) ⊇ (8)  {(o → (s,t) ot )} δ (o ) = 0, δ ( ot ) = 1 where we note δ(o ) = 1, δ(ot) = 0 cannot occur. By definition, ∗ ̸∈ ϕ′ (1 →(s,o) o ) iff s ⪯ R Ri . We note that B is R-trivial; hence it divides an iterated wreath product of U1 . This is a relational morphism. Set ϕi,1 := Ext(ϕ′ , ϕi−1 ) : M ◁ Ni,1 where Ni,1 = B◦ Ni−1 . 2. Build a sequence of relational morphisms ϕi,2 , ϕi,3 , . . . as follows, over j = 1, 2, 3, . . . : (a) Intuition: We simplify Dϕi,j in two ways. First, all information from earlier annotation is removed once we have entered Ri . This simplifies our proof by avoiding any complications arising from interactions between old and new annotation. Second, elements of Dk provide extra information beyond bounded counting; here, we project its elements to the underlying set of truncated integers. Write an element of Ni,j as a = ( f i,j , . . . , f i,1 , f ). where f i,j : Ni,j−1 → Dk . Define its “retained signature” by
sigi,j ( a) := 0 · f i,j (1 Ni,j−1 ), . . . , 0 · f i,2 (1 Ni,1 ), f i,1 (1 Ni−1 ) , | {z } | {z } ∈B

∈ Dk

|

{z

∈ Sk

}

where we view Dk as acting on Sk := [−k, . . . , k ] ∪ {⊥} from the right (7). We define a right congruence6 ρi,j on Ni,j by setting a ρi,j b whenever (i) a = b, or (ii) a (1 b f i,1 Ni−1 ) ̸ = ∗, f i,1 (1 Ni−1 ) ̸ = ∗, and sigi,j ( a ) = sigi,j ( b ). We define Ei,j as the category obtained from Dϕi,j and the right-congruence ρi,j (based on the discussion in Section H.2). (b) Consider the set Ωi,j of algebraic relational morphisms ϕ′ : Ei,j ◁Z such that for each s ∈ Ri and any t ∈ ϕi,j (s), ϕ′ (1 →s,t t) is a finite set. 7 Note: In the automaton-based 5 B : = ∂ ∪ {∗}, ∗ b = b, rb = r whenever r ∈ ∂ , b ∈ B. i i 6 In the sense that aρb ⇒ arρbr for any a, b, r ∈ N . i,j 7Without loss of generality, we restrict to relational morphisms ϕ′ where, for each object o with non-∗ entry annotation, every vlaueSof ϕ′ on an arrow 1 → o is generated by factorization through a prefix ending inside Ri : ϕ′ (α) = α= βγ,β∈π −1 ( Ri ) ϕ′ ( β)ϕ′ (γ). This condition is imposed because

relational morphisms may add values that are not generated by any nontrivial factorization of an arrow. The construction in Lemma 69 satisfies this condition.

38

Published as a conference paper at COLM 2026

proof, the key requirement is for the relabelings to be balanced. Here, we formulate this in terms of finite sets. (c) If there is ϕ′ ∈ Ωi,j such that at least one of the following is satisfied: i. Condition A: ϕ′ : Ei,j ◁Z assigns disjoint images to two arrows in Hom(o → o ′ ) where o, o ′ both are in Ri (in the sense of Definition 59). ii. Condition B: There exist objects x, y ∈ Obj( Ei,j ), arrows a ∈ Hom( x → y); b ∈ Hom(y → x ); ℓ ∈ Hom( x → x ) such that x, y are inside Ri 8 , but no arrow in Hom( x, y) ends in Ri 9 , whereas ℓ ends in Ri 10 and ϕ′ ( ab) ∩ ϕ′ (ℓ) = ∅. then we take such a ϕ′ , turn it to a relational morphism ϕ̃′ : Ei,j ◁Dk 11 , pull it back to b′ : Dϕi,j ◁Dk and build ϕi,j+1 := Ext(ϕ b′ , ϕi,j ) : M ◁ Ni,j+1 , where Ni,j+1 := Dk ◦ Ni,j . ϕ (d) Otherwise, we terminate this inner loop. −1 (e) One possibility is that ϕi,j (ϕi,j (m)) = {m} for each m ∈ Ri . By induction, we have satisfied Invariant(i ). Then, set ϕi := ϕi,j : M◁ Ni and pass to the next iteration in the outer loop. Else, we exit from the entire algorithm and declare failure. We declare success and return Nℓ if we iterated through all i = 1, . . . , ℓ without ever declaring failure. Note: Motivation of this algorithm: The generic strategy would be to keep generating relational morphisms to Z, but that would not suffice for decidability, because (i) we wouldn’t know how often to iterate, and (ii) wouldn’t know which types to use. We “guide” the process by (i) proceeding along R classes, (ii) considering morphisms to well-selected finite monoids, (iii) passing to Ei,j instead of the more complicated Dϕi,j , and (iv) focusing on the sets Ωi,j . Throughout, we write 1 ∈ Obj( Ei,j ) for the object arising from the identity element of Ni,j . Definition 59. For any of the categories Ei,j constructed in the decision procedure, we define the following notions. Let π : Ei,j ≺ M be the canonical division. 1. Let Si be the set of arrows o →s,t ot such that there are arrows 1 →s′ ,o o and ot →s′′ ,t′′ ott′′ such that ss′ s′′ ∈ Ri . 2. We say an arrow α ∈ Hom(o → o ′ ) “ends” in Ri if there is an arrow β ∈ Hom(1 → o ) such that βα is defined and βα ∈ π −1 ( Ri ). 3. We say an arrow α ∈ Hom(o → o ′ ) “starts” in Ri if there is an arrow β ∈ Hom(1 → o ) such that βα is defined and β ∈ π −1 ( Ri ). 4. We say an object o is “inside Ri ” if Hom(1 → o ) ∩ π −1 ( Ri ) ̸= ∅. H.3.1

Key Properties of the Procedure

Lemma 60 (Correctness). If the algorithm succeeds, then M divides an iterated wreath product of (Z, Z+ ), of the form (((. . . Z)◦· Z)◦· Z). 8 In the sense of Definition 59:

Hom(1, x ) ∩ π −1 ( Ri ) ̸= ∅; Hom(1, y) ∩ π −1 ( Ri ) ̸= ∅,, where

π : Ei,j ◁ M is the canonical division. 9 In the sense of Definition 59: ∀ β ∈ Hom ( x → y ); Hom (1 → x ) β ∩ π −1 ( R ) = ∅,, where π : E ◁ M i i,j is the canonical division. 10 In the sense of Definition 59: Hom (1, x ) ℓ ∩ π −1 ( R ) ̸ = ∅, i 11 For sufficiently large k, greater than the absolute value of, for each s ∈ R and any t ∈ ϕ ( s ), the i i,j entries of the finite set ϕ′ (1 →s,t t). To convert a relational morphism to Z into one on Dk , map 1 to a, -1 to b, etc., and close to make it a relational morphism. Choosing k large enough will ensure ⊥ is avoided on these homsets. Also, on these homsets, this resulting relational morphism is at least as finegrained as the original one, since one can get back the original one by mapping Dyck elements to their height.

39

Published as a conference paper at COLM 2026

Proof. We refer to a wreath product of the form (. . . ◦·) · ◦·) · ◦·) · ◦· · as left-associative. First, if the algorithm succeeds we obtain a relational morphism ϕk : M ◁ N where N divides a left-associative wreath product of U1 and Dk . By the invariant maintained in the Decision Procedure, ϕk is injective, making it a division. We now need to explain why M also divides a product of the form (((. . . Z)◦· Z)◦· Z). First, by we can obtain a representation in terms of Dk ⪯ ((U1 )2k ◦· Z) and U1 , in the left-associative bracketing due to the associativity of the finite wreath product at the level of pseudovarieties (Tilson, 1987). By repeated application of lemma 61, we then obtain a left-associative wreath product where the factors are either direct products of U1 or just Z. Because direct products divide wreath products, we know that M ⪯ (S◦( · N × U1 ))◦· T implies M ⪯ ((S◦· N )◦· U1 )◦· T. Iteratively applying this identity, we obtain a division into a left-associative wreath product of U1 and Z (with much greater depth). Finally because U1 ⪯ Z, we can conclude that M divides a left-associative wreath product of Z.

Lemma 61. For typed monoids T, S, we have that T ◦( · U1 ◦· S) ⪯ ( T ◦· U1 |TS | )◦· S

Proof. We show the proof ignoring any constants in the wreath product to put less strain on notation, but it is easy to add them back in. Let ( f 1 , ( g1 , h1 ))( f 2 , ( g2 , h2 )) · · · ( f n , ( gn , hn )) S be a multiplication in T ◦( · U1 ◦· S) where hi ∈ S, gi ∈ U1 S , and f i ∈ T U1 ×S . We will write multiplication in all monoids using Π, but assume the distinction is clear. By lemma 37 we can compute the type of this multiplication by computing the following and checking the types of the indicated terms 1, 2, and 3   n −1   ∏ fi   i =1 |

j −1

i −1

∏ g j ∏ hk j =1

!

k =1

{z 1

  ! !!   i −1 n −1  i −1  n −1    ,  ∏ gi ∏ h j , ∏ h i   , ∏ hj   i =1 j =1 i =1   j =1 } | {z } | {z } 2

3

We will simulate this computation in ( T ◦· U1 |TS | )◦· S. That is, the desired computation is given by the following injective relational morphism given below. Intuitively, U1 |TS | records which of the finitely many types have been seen. Since f must be type-respecting, this suffices to recreate the computation of T ◦( · U1 ◦· S). ϕ : T ◦( · U1 ◦· S) → ( T ◦· U1 |TS | )◦· S α f ,g ∈ ( T U1 γ f ,ζ ∈ T U1

|TS |

× U1 |TS | )S

|TS |

ϕ(( f , ( g, h))) = (α f ,g , h)  α f ,g (ζ ) = (γ f ,ζ , (λS1 , λS2 , . . . , λS|T | )) S

λS = Im( β) ⊆

γ f ,ζ ((λS1 , λS2 , . . . , λS|T | )) = f ( β, ζ ) S

1 0

ζ∈S ζ ̸∈ S

\

S

S∈TS ;λS =1

Note that γ f ,ζ is well-defined because f (( β, ζ )) identical for all β whose images are contained in the same set of types, since f is type-respecting. Now, this mapping is injective because every type-respecting function g ∈ U1 S is represented by some (λS1 , λS2 , . . . , λS|T | )) ∈ U1 |TS | , and every type-respecting function f is represented as some γ f ,ζ . 40

S

Published as a conference paper at COLM 2026

Thus the sequence ( f 1 , ( g1 , h1 ))( f 2 , ( g2 , h2 )) · · · ( f n , ( gn , hn )) maps homomorphically to the sequence (α f1 ,g1 , h1 )(α f2 ,g2 , h2 ) · · · (α f n ,gn , hn ) which is evaluated as   !  n −1 i −1 n −1     ∏ α f i ,gi ∏ h j , ∏ hi    i =1 j =1 i =1 | {z } 3

Observe that the type 3 is already computed in the second coordinate. We will see that 1 and 2 are also computed in the first coordinate: ! ! n −1

i −1

∏ α fi ,gi ∏ h j

i =1

n −1

= α f1 ,g1 (0) α f2 ,g2 (h1 ) · · · α f n ,gn

j =1

∏ hj j =1

= (γ f1 ,0 , Λ1 )(γ f2 ,h1 , Λ2 ) · · · (γ f ,∏n−1 h , Λn ) i i =1 j   !! !  n −1 i −1 n −1 i −1    =  ∏ f i 1, ∏ h j , ∏ gi ∏ h j    i =1  j =1 i =1 j =1 | {z } | {z } 1

2

The following properties of ω ∈ Ωi,j are key: Lemma 62 (Balance on Loops). Let ω ∈ Ωi,j . 1. Let u ∈ Ri , ρ ∈ M such that uρ = u. Consider arrows 1 →(u,o) o →(ρ,t) ot in Ei,j . Then in fact ot = o, and ω (o →(ρ,t) o ) = {0Z } where 0Z is the neutral element of Z. 2. Let u be such that Ri u = Ri . For v ∈ Ri , consider arrows

1 →(v,o) o →(u,t) ot

in Ei,j . Then ω (o →(u,t) ot) is a singleton. Proof. For the first point, we have two claims to prove: that (a) ot = o, and that (b) the image is {0Z }. We first note that (a) holds at j = 1: u ∈ Ri , uρ = u and 1 →(u,o) o →(ρ,t) ot in Ei,j , then in fact ot = o by construction of Ei,1 . We also note that, if (b) has been shown for 1, . . . , j, then (a) follows for 1, . . . , j + 1. We thus need to perform the inductive step for (b). We consider the arrow o →(ρ,t) o. Assume z ∈ ω (o →(ρ,t) o ) and z ̸= 0. Now, for all k ≥ 0, uρk = u; hence, ω (1 →(u,o) o ) is infinite. This is a contradiction to ω ∈ Ωi,j . For the second point, from Ri u = Ri , obtain ρ such that vuρ = v. We consider arrows: 1 →(v,o) o →(u,t) ot →(ρ,t′ ) ott′ By (1), in fact, ott′ = o and ω (o →(u,t) ot →(ρ,t′ ) ott′ ) = {0Z }. Because ω is a relational morphism and Z is a group, this entails ω (o →(u,t) ot) must be a singleton. We deduce the following structural properties of Ei,j , which are used both for termination and for completeness of the procedure. As foreshadowed when we defined the “entrypoint coordinate” ϕi,1 , we find that Ri is reflected in Ei,j in multiple strongly connected components (or “bonded components”), each indexed by a different entry arrow of the “boundary set” ∂i we defined there: 41

Published as a conference paper at COLM 2026

Lemma 63 (Structure of Ei,j ). 1. Let α := (o →(s,t) ot) ∈ ∂i , and let m ∈ Ri . Then there is exactly one u ∈ Obj( Ei,j ) such that both of the following hold: (i) there is an arrow 1 →(m,u) u, and (ii) the ϕi,1 component of u is α. 2. Let α = (1 →(m,u) u), α′ = (1 →(m′ ,u′ ) u′ ) be arrows in Ei,j , where m, m′ ∈ Ri ; and assume u, u′ have the same ϕi,1 component. Then there is β ∈ Hom(u, u′ ) such that α′ = αβ. Proof. We show this by induction over j. The claims are immediate at j = 1. For the first claim, we show the inductive step using Lemma 62. For any arrow α = (1 →(m,o) o ) with m ∈ Ri , Lemma 62.2 entails that ω is single-valued on all arrows β = (o →(m′ ,t) ot) with mm′ ∈ Ri ; hence, inductively, after passing to Ei,j+1 , only a single arrow is derived from β. The second claim follows by choosing n such that m′ = mn; the first claim enforces the presence of an arrow covering n in Hom(u, u′ ). Lemma 64 (Termination). The inner loop always terminates. Proof. A new morphism ϕi,j can only be accepted because it separates two arrows in a homset Hom(o → o ′ ) where o, o ′ are both inside Ri . We need to show that this can only happen a bounded number of times. To this end, we first note by the first point of Structure of Ei,j that, for each entry arrow α, we can uniquely assign a single o for every r ∈ Ri , and this mapping is a surjection onto the objects inside Ri . Also, with every j iteration, this structure becomes finer, i.e., a homset Hom(o → o ′ ) where o, o ′ are in Ri can split into several ones that (save for arrows leaving Ri , where arrows carrying the same M-label might go into into different descendant homsets) each exactly carry some subset of the original arrows. Thus, the total number of times this happens must be bounded. Lemma 65 (Computability). In each step of the inner loop, we can effectively decide if there is a ϕ′ satisfying the requirements. Proof. We can always construct a relational morphism of the second type if it exists. We can always apply this case when it is available. We need to check when a relational morphism of the first type exists. For the arrows that start and end in Ri , since they will be single-valued, we can check the Z-module of functions defined on these arrows satisfying the balancedness condition. For arrows in the connected components of objects in Ri that however do not end Ri , all of them will receive a nonempty set of values by closing this under composition, for, otherwise, we would have been able to choose a relational morphism of the second type. We can extend any solution from a single connected component to a full morphism, by the Extension Lemma (Lemma 69).

H.3.2

Establishing Completeness

Assume that, after constructing Ei,j , the procedure terminates with failure. We localize this failure into a smaller, focused category. Definition 66. For each object o inside Ri , we consider the strongly connected component (or “bonded component” in Tilson (1987)) of o: Obj(Co ) :={o ′ ∈ Obj( Ei,j ) : Hom(o → o ′ ) ̸= ∅, Hom(o ′ → o ) ̸= ∅} 42

Published as a conference paper at COLM 2026

As above, let π be the canonical division π : Ei,j ≺ M. Within any homset Hom(o ′ → o ′′ ) in Co , we merge any two arrows β, β′ such that, in Ei,j , Hom(1 → o ′ ) β and Hom(1 → o ′ ) β′ both are not S in π −1 ( j≤i R j ). By construction, Co is a well-defined category, and Co ≺ Ei,j ≺ M. Lemma 67. Every homset Hom(u → u′ ) in Co hosts an arrow ending in Ri . Proof. Otherwise, a morphism ϕ′ satisfying the second condition would have been selected. Lemma 68. Failure of the algorithm entails that some Co contains a non-singleton homset, i.e., Co is not trivial. −1 Proof. Failure of the algorithm implies that there is m ∈ Ri such that ϕi,j (ϕi,j (m)) ⊋ {m}.

Now consider m′ ∈ M, m ̸= m′ such that there is some ô ∈ ϕi,j (m) ∩ ϕi,j (m′ ). Let o be the corresponding element of Ei,j . This means that, in Ei,j , there are distinct arrows 1 →(m,õ) o and 1 →(m′ ,o) o. Now we consider the ϕi,1 coordinate of o (“entry point coordinate”); this is of the form (u →(s,t) v) corresponding to some arrow of Dϕi−1 . By the inductive hypothesis “(Invariant(i))”, Hom(1 → u) in that category had exactly one object 1 →(s′ ,u) u, where s′ ∈ Rk for some k < i. We can thus factorize     1 →(m,õ) o = 1 →(s′ ,u) u u →(s,t) v v →(w,... ) o

(9)

    1 →(m′ ,õ) o = 1 →(s′ ,u) u u →(s,t) v v →(w′ ,... ) o

(10)

Now let v be the corresponding entry object, which must be contained in Co (by Lemma 63.1); then (by Lemma 63.2) there is an arrow α = 1 →(s′ s,v) v such that there are β, β′ ∈ Hom(v, o ) with 1 →(m,õ) o = αβ and 1 →(m′ ,o) o = αβ′ . We thus have shown Hom(v, o ) to be nonsingleton. Lemma 69 (Extension Lemma). Assume ω : Co ◁Z stays finite-image on all arrows in Co that end in Ri . Then there is an algebraic relational morphism ω̃ : Ei,j ◁Z such that ω̃ (1 →(s,t) t) is a singleton set whenever s ∈ Ri , and ω̃ |Co ≡ ω. Proof. There are two aspects here: achieving ω̃ |Co ≡ ω – this is easy because Co is a bonded component – and achieving that ω̃ (1 →(s,t) s) is a finite set for s ∈ Ri – which requires care. We first define  ω∗ ( α ) : =

α ∈ Co else

ω (α) {0}

(11)

which is not in general a relational morphism. We define ω̃ as the closure under composition, so that ω̃ is a relational morphism. Constructively, we can write ω̃ (α) =

[

n

∑ ω ∗ ( γi )

(12)

γ1 ...γn =α i =1

where “∑” is to be understood in a set-valued sense as A + B = { a + b : a ∈ A, b ∈ B}. Because Co is a strongly connected component, ω̃ |Co ≡ ω. Now consider α : 1 →(s,t) t for some s ∈ Ri . One option is that t ̸∈ Co ; in this case, no path through Co can multiply out to this arrow, and ω̃ (α) = {0}, which is a finite set. The other option is that t ∈ Co . 43

Published as a conference paper at COLM 2026

Assume ω (α) is infinite. Then, for each n, there is a path of the form: α = γ1 γ2 γ3 . . . γn

(13)

where ∑in=2 ω∗ (γi ) contains unboundedly (positive or negative) large numbers; we can WLOG choose this so that ω∗ (γ2 ) ̸= {0} by multiplying the initial prefix out into γ1 if needed. By construction, γ2 ∈ Co ; hence, γ1 must end in Co . But then we can set β := γ2 · · · · · γn , which starts and ends in Co , and also ends in Ri because α does. But then ω̃ ( β(n)) has unboundedly large numbers as n → ∞, which is a contradiction to ω̃ |Co ≡ ω. Lemma 70. Consider two arrows in the same homset in Co : β 1 := u →(s,t) ut and β 2 := u →(s′ ,t′ ) ut. If β 1 ̸= β 2 , then 1. there is λ ∈ Ri ∩ π ( Hom(1 → u)) such that λs ̸= λs′ . 2. there is α ∈ Hom(o → u) such that αβ 1 ̸= αβ 2 . Proof. This follows from the derived category construction; the right-congruences applied afterwards preserve it. Lemma 71 (Completeness). If the procedure terminates with failure, M does not divide an iterated wreath product of (Z, Z+ ). Proof. Assume that, after constructing Ei,j , the procedure terminates with failure. Setting up a division Choose as C ′′ one nontrivial Co (it doesn’t matter which one); from now on this fixes o. For the purposes of defining typed division, we view Co as rooted in o (Definition 75). Assume M divides an iterated wreath product of (Z, Z+ ), then so does C ′′ (in the sense of Definition 75) by Lemma 77. Consider a division of a minimum-depth wreath product of Z, ψ : C ′′ ≺ Z . . ◦· Z} (here all Z are typed like (Z, Z+ )); in particular, | ◦· .{z T times

because C ′′ is not trivial, T ≥ 1. Let ω = π (T ) ◦ ψ; by definition, ω : C ′′ ◁Z. Our goal is to create a division µ : C ′′ ≺ Z . . ◦· Z} (again in the sense of Definition 75). This would | ◦· .{z T −1 times

be a contradiction to the minimality of T. As a consequence, C ′′ cannot divide any wreath product of (Z, Z+ ). Note: The basic idea is to show that ω cannot have provided any useful information, and in particular gives the same values across different arrows in a given hom-set. Either it stays finite-image on all arrows going into Ri (in which case ω provides as much information as an element of Ωi,j – and the algorithm having terminated indicates that no such element would have been helpful), or it is infinite-image (in which case we can pass to a limiting element ±∞, showing that ω contributes no information useful to (Z, Z+ )-based recognizers). Case 1: ω stays finite-image on all arrows ending in Ri inside C ′′ First, assume ω stays finite-image on all arrows ending in Ri inside C ′′ . We obtain ω̃ : Ei,j ◁Z via Lemma 69. We observe that ω̃ ∈ Ωi,j ; hence, ω̃ must assign singleton images to any arrow in Co that ends inside Ri . The algorithm having terminated means that ω̃, and hence ω, cannot assign distinct images to any two arrows staying inside Ri that appear in a single homset in Co ; also, any of these needs to be mapped to a singleton set. It also means that, when considering an arrow that is in Co but ends outside of Ri , it might in fact be assigned some further set of values, but it must overlap with the value assigned to the arrows staying inside Ri . That is, in any homset, there is one single value shared across all arrows; also, there potentially is a further set of values assigned to the arrows that end outside of Ri . For each homset Hom(u → u′ ), we obtain a unique θu,u′ ∈ Z such that ω (α) = {θu,u′ } whenever α ∈ Hom(u → u′ ) ends in Ri ; also, when the homset contains an arrow leaving 44

Published as a conference paper at COLM 2026

Ri (we can write it as β : u →(⊥,... ) u′ ), θu,u′ ∈ ω ( β). We write νu := θo,u ; importantly, νut = νu θu,ut . We obtain the desired division µ : Co ≺ (Z◦· . . . ◦· Z) as follows. Note that any object in the | {z } T −1 times

image of ψ has the form ( g, . . . ) where g : Z → (Z◦· . . . ◦· Z). For any arrow u →(s,t) ut in | {z } T −1 times

Co , we define: µ(u →(s,t) ut) := { g(νu ) : ( g, θu,ut ) ∈ ψ(u →(s,t) ut)}

(14)

which is a nonempty subset of (Z◦· . . . ◦· Z). | {z } T −1 times

We first show that µ is an algebraic relational morphism. Consider arrows α : u →(s,t) ut and β : ut →(s′ ,t′ ) utt′ in Co . Then: µ(α)µ( β) ={ g(νu ) : ( g, θu,ut ) ∈ ψ(α)}{ g′ (νut ) : ( g′ , θut,utt′ ) ∈ ψ( β)}

={ g(νu ) g′ (νut ) : ( g, θu,ut ) ∈ ψ(α), ( g′ , θut,utt′ ) ∈ ψ( β)} ⊆{ g(νu ) : ( g, θu,utt′ ) ∈ ψ(αβ)} =µ(αβ) where the “⊆” step used the fact that ψ is an algebraic relational morphism. We, second, show that µ is a typed division. Consider two arrows β 1 := u →s,t ut, β 2 := u →s′ ,t ut in C ′′ ; if they are distinct, we find α ∈ Hom(o → u) such that αβ 1 ̸= αβ 2 (Lemma 70). Then there are disjoint types T1 , T2 of Z . . ◦· Z} such that ψ(αβ 1 ) ⊆ T1 , | ◦· .{z T times

ψ(αβ 2 ) ⊆ T2 . That is, for any gs , gs′ selected for the two arrows, we have

( gα (·) gs (·θo,u ), θo,u θo,ut ) ∈ ψ(αβ 1 ) ⊆ T1

(15)

( gα (·) gs′ (·θo,u ), θo,u θo,ut ) ∈ ψ(αβ 2 ) ⊆ T2

(16)

Hence, there must be disjoint types V1 , V2 of Z . . ◦· Z} such that | ◦· .{z T −1 times

But then

µ(αβ 1 ) = gα (0) gs (θo,u ) ∈ V1

(17)

µ(αβ 2 ) = gα (0) gs′ (θo,u ) ∈ V2

(18)

gs (θo,u ) ∈ gα (0)−1 V1

(19)

gs′ (θo,u ) ∈ gα (0)−1 V2

(20)

where V1 ∩ V2 = ∅, the types gα (0)−1 V1 and gα (0)−1 V2 are also disjoint types.12 The above assumes that T1 , T2 are defined simply by first-coordinate evaluation at zero; if they instead arise as Boolean combinations of multiple observations, µ would instead map into a direct product of multiple copies where we evaluate g at different coordinates; in this case, the proof here would be lifted to depth-T wreath products of direct products of Z. Case 2: ω is infinite-image on some arrow ending in Ri inside C ′′ Let α =  u0 →(s0 ,t0 ) u0 t0 in C ′′ be an arrow ending in Ri which is associated with an infinite number of different values under ω. Without loss of generality, we may assume that sup ω (α) = +∞ (else, inf ω (α) = −∞ and we replace +∞ by −∞ below). 12 Here, we take a more general definition of types that are closed under (left) quotients, in line with the topological perspective on typed monoids (Gehrke & Krebs, 2017). This does not change the underlying expressivity of wpc(Z).

45

Published as a conference paper at COLM 2026

Note that any object in the image of ψ has the form ( g, . . . ) where g : Z → (Z◦· . . . ◦· Z). | {z } T −1 times

Because g arises from a composition of type-respecting functions, g(∞) := limx→∞ g( x ) is well-defined and in Z. We define µ(u →(s,t) ut) := { g(∞) : ( g, . . . ) ∈ ψ(u →(s,t) ut)}

(21)

which is a subset of (Z◦· . . . ◦· Z). {z } | T −1 times

This is an algebraic relational morphism µ : C ′′ ◁ (Z◦· . . . ◦· Z): For arrows β, β′ such that ββ′ | {z } T −1 times

is defined, we have: µ( β)µ( β′ ) ={ g(∞)h(∞) : ( g, . . . ) ∈ ψ( β), (h, . . . ) ∈ ψ( β′ )}

={ lim ( g( x )h( x )) : g..., h...} x →∞

={ lim ( g( x )h( xτ1 )) : g..., h...} x →∞

⊆{ G (∞) : ( G, . . . ) ∈ ψ( ββ′ )} =µ( ββ′ ) We need to show that it is typed and injective; the proof is similar to Case 1. Consider two distinct arrows in the same homset in C ′′ : β 1 := u →(s,t) ut

β 2 := u →(s′ ,t′ ) ut

If β 1 ̸= β 2 , that means there is λ ∈ Ri ∩ π −1 ( Hom(1 → u)) such that λs ̸= λs′ , by Lemma 70. We now construct ρ1 , ρ2 ∈ M such that α := 1 →(ρ1 ,u0 ) u0 →(s0 ,t0 ) u0 t0 →(ρ2 ,t′ ) u = 1 →(ρ1 s0 ρ2 ,u) u

(22)

in Hom(1 → u) satisfies λ ∈ π −1 (α).13 Hence, αβ ̸= αβ′ in Ei,j . In C ′′ , α′ := u0 →(s0 ,t0 ) u0 t0 →(ρ2 ,t′ ) u satisfies α′ β ̸= α′ β′ . Now, we note that sup ω (α′ ) = +∞; this enforces that µ( β) ∩ µ( β′ ) = ∅. Overall, we have obtained a division µ in either case, and, by contradiction, established that M does not divide an iterated wreath product of (Z, Z+ ). H.3.3

Deriving Main Results

Theorem 15. Membership of M ∈ C-RASP ∩ REG is decidable in O(poly(| M |)) time. Proof. We need to show that (i) the algorithm from Definition 58 correctly determines membership in C-RASP (shown in Theorem 57), and (ii) that it runs in polynomial time in | M|. For (ii), one route is via the automaton-based formulation of the algorithm in Appendix J, with proof of time polynomial in the number of automaton states (hence the size of the syntactic monoid) in Corollary 88. Another route is by noting that one can identify candidate morphisms ϕ′ : Ei,j ◁Z by restricting to the strongly-connected component Co , encoding (i) respecting composition, (ii) zeros on idempotent arrows as linear constraints. The number of such linear constraints is polynomial in the size of M; an integral basis of the solution space can then be found in polynomial time. A solution can be extended to an element of Ωi,j via the Extension Lemma 69. Corollary 72. C-RASP ∩ REG = wpc(Dy). 13 Choose ρ ∈ R just to produce the first arrow. Now we choose ρ ∈ M such that ρ s ρ = λ, 2 1 1 0 2 i using that ρ1 s0 ρ2 and λ both are in Ri . Now applying Lemma 62 (Claim 2) inductively to each j, there is an arrow uo t0 →(ρ2 ,t′ ) u.

46

Published as a conference paper at COLM 2026

Proof. The “⊇” direction is implied by the proof of Lemma 60. The “⊆” direction follows because the algorithm from Definition 58, when it succeeds on a monoid M, supplies a division M ≺ Dk1 ◦ . . . ◦Dkr . H.4

Defining Division between Categories and Typed Monoids

Here, we define relational morphisms and divisions between finite categories and typed monoids. The definitions are naturally typed extensions of the usual definitions for finite categories (Tilson, 1987). Definition 73. An algebraic relational morphism ϕ : X ◁ M from a category X to a monoid M specifies, for each arrow α in X a nonempty set ϕ(α) ⊆ M, such that ϕ(α)ϕ( β) ⊆ ϕ(αβ) when α ∈ Hom(o → o ′ ), β ∈ Hom(o ′ → o ′′ ), and 1 M ∈ ϕ(1o ) where 1o ∈ Hom(o → o ) is the local identity arrow. This definition matches the definition of relational morphisms in Tilson (1987) in the special case where the target is a monoid; we add the qualifier “algebraic” to highlight that type structure does not yet enter its definition. We do the same for division: Definition 74. An algebraic division ψ : X ⪯ N is an algebraic relational morphism ψ : X ◁ N where, for any two distinct arrows α, α′ ∈ Hom(o → o ′ ), we have ψ(α) ∩ ψ(α′ ) = ∅. We expand this definition of division to the case where type structure is present: Definition 75. Let C be a finite category and let S = (S, TS , ES ) be a typed monoid. A typed division ψ : C ⪯ S is an algebraic division ψ : C ◁S, such that, for each homset H = HomC (o → o ′ ), for each α ∈ H, there is a type T ∈ TS such that ψ(α) = T ∩ ψ( H ). We first note that, in the case of finite monoids with discrete types (i.e., each subset of the monoid is a type), the notions of typed relational morphisms and typed divisions reduce to the usual definitions from Tilson (1987). We can further link the definition to typed recognition,14 considering the setting of a finite monoid M such that any language it recognizes (in the ordinary sense) via the surjective morphism η is also recognized (in the typed sense) by S. Then: Lemma 76. Let M be a finite monoid, and let S be a typed monoid. Let η : Σ∗ ↠ M be a surjective morphism, and h : Σ∗ → S a morphisms. Assume that for every P ⊆ M, there is TP ∈ TS such that η −1 ( P) = h−1 ( TP ). Then M ⪯ S in the sense of Definition 75, viewing M as a single-object category. Proof. Consider the relation ψ ⊆ M × S defined by ψ := h ◦ η −1 . Because η is surjective, this is an algebraic relational morphism. The assumption also ensures that it is an algebraic division. Then, for any α ∈ M, there is a type Tα ∈ TS such that η −1 (α) = h−1 ( Tα ). This entails ψ(α) = h(η −1 (α)) = h(h−1 ( Tα )) = Tα ∩ ψ( M ). Thus, our definitions here are compatible with the relevant pre-existing definitions from prior work. We now verify compatibility of our extended notion of division with composition. Lemma 77. Let C be a finite category, let M be a finite monoid, and let S = (S, TS , ES ) be a typed monoid. Assume that M and S satisfy the assumptions of Lemma 76. Assume C ⪯ M (in the sense of Tilson (1987)). Then C ⪯ S (in the sense of Definition 75). We will apply this to the setting where M is the syntactic monoid of a regular language that is definable in C-RASP; this then provides an iterated wreath product of Z recognizing all languages recognized by the syntactic morphism of M. 14We note that there is also a notion of division in Krebs (2008), but here we link our relational definition directly to language recognition.

47

Published as a conference paper at COLM 2026

Proof. Let ϕ : C ◁ M be an algebraic division and let θ : M◁S be a typed division. Define their composite relation ψ : C ◁S by [ ψ(α) = θ (m) m∈ϕ(α)

for each arrow α of C. Because algebraic relational morphisms and divisions composeTilson (1987), ψ is again an algebraic relational morphism and a division from C to the underlying monoid of S. It remains to check that ψ is also a typed relational morphism. Because M is a one-object category, the hypothesis that θ is typed yields a single ambient set A ⊆ S such that for every m ∈ M there is a type m ∈ TS with θ (m) = A ∩ m. S ψ Fix a homset H of C, and put A H := β∈ H ψ( β). For α ∈ H,

ψ(α) =

[

ψ

ψ

( A H ∩ m) = A H ∩

m∈ϕ(α)

 [

 m .

m∈ϕ(α)

Because M is finite and TS is a Boolean algebra, the finite union [

a :=

m

m∈ϕ(α)

is again a type of S. Thus ψ

ψ(α) = A H ∩ a, so ψ is a typed relational morphism.

I

Algebraic Characterization (Necessary but not Sufficient Criterion)

Theorem 13. M ∈ Rω iff M is aperiodic and every R-class of M contains at most one idempotent. Proof. We note that R◦G ∩ A is exactly the aperiodic monoids with at most one idempotent in each R-class. First, we show Rω ⊆ R◦G ∩ A. Suppose M ∈ Rω . By substituting 1 for y in Rω we obtain that M satisfies xω x = xω which implies M ∈ A (Pin, 2009). Next, assume for sake of contradiction that M ̸∈ R◦G. Then there is a R-class of M which contains at least 2 idempotents (Stiffler Jr, 1973, Theorem 3.18). Let e1 ̸= e2 be R-equivalent idempotents, where e1 = e2 m2 and e2 = e1 m1 . Then

(e1 e2 )ω = (e1 e1 m1 )ω = (e1 m1 )ω = e2ω = e2 while

( e1 e2 ) ω e1 = e2 e1 = e2 e2 m 2 = e2 m 2 = e1 . This implies (e1 e2 )ω ̸= (e1 e2 )ω e1 , and thus M ̸∈ Rω , a contradiction. Thus M ∈ R◦G. Now we show R◦G ∩ A ⊆ Rω . Let m1 , m2 ∈ M. First, we note that (m1 m2ω )ω = (m2ω m1 )ω . This is because

(m1 m2ω )ω = (m1 m2ω )ω +1 = m1 (m2ω m1 )ω m2ω ≤R m1 (m2ω m1 )ω ≤R (m1 m2ω m1 )ω m1 ≤R (m2ω m1 )ω 48

by aperiodicity

Published as a conference paper at COLM 2026

and similarly we have (m2ω m1 )ω ≤R (m1 m2ω )ω . Then, because R-equivalent idempotents are equal in M ∈ R◦G ∩ A. Now consider the elements(m1 m2ω )ω and (m1 m2ω )ω (m2ω m1 )ω , which are both idempotent. We show these are R-equivalent. First (m1 m2ω )ω ≥R (m1 m2ω )ω m1 ≥R (m1 m2ω )ω +1 , so by aperiodicity (m1 m2ω )ω ≡R (m1 m2ω )ω m1 . Then

(m1 m2ω )ω (m2ω m1 )ω = (m1 m2ω )ω m2ω (m1 m2ω )ω m1 = (m1 m2ω )ω m1 m2ω m2ω (m1 m2ω )ω m1 = (m1 m2ω )ω m1 Since these are in fact both R-equivalent idempotents, they are equal (Stiffler Jr, 1973). Thus using the above equalities we can conclude

(m1 m2ω )ω = (m1 m2ω )ω (m2ω m1 )ω = (m1 m2ω )ω m1 .

Theorem 14. C-RASP ∩ REG = wpc(Dy). Hence R ⊊ C-RASP ∩ REG ⊊ Rω ⊊ A ⊊ REG Proof. The first claim is shown using the decision procedure (corollary 72): every finite monoid in C-RASP can be decomposed into wreath products of U1 and Dk – in this case U1 ⪯ D1 . In the other direction, Dk ∈ C-RASP, and thus wpc(Dy) contains only monoids in C-RASP, using section E.2. We use this to show the other strict inclusions. • First, R = wpc(U1 ). U1 ∈ Dy. Then we have that C-RASP ∩ REG = wpc(Dy), so R ⊆ C-RASP ∩ REG. For a strict separation, D1 ∈ C-RASP ∩ REG but D1 ̸∈ R (Brzozowski & Fich, 1980). • We have that C-RASP ∩ REG = wpc(Dy). Then by proposition 23 we know Dk divides into a wreath product of U1 and cyclic groups. We can move all U1 factors to the left, obtaining a monoid in R◦G (Stiffler Jr, 1973). Furthermore, since all monoids C-RASP are aperiodic, this results in a monoid in Rω , by theorem 13. For a strict separation, the monoid M (( ab + bba)∗ ) ∈ Rω \ C-RASP (this can be computed by the decision procedure) • First, Rω ⊆ A ⊊ REG by theorem 13. The strict separation can be witnessed by M (( ab + aabb)∗ ), which is aperiodic but has two idempotents in a single R-class • A ⊊ REG is a standard fact. For instance, M ((b∗ ab∗ ab∗ )∗ ) (i.e. Z/2Z) witnesses the strict separation.

J

Automata proof of C-RASP ∩ REG

We attempt to track the states of a DFA by a C-RASP program by iterating over the reachability order of the DFA. Whenever we encounter a nontrivial strongly connected component, we need to check if the program can be extended to cover it. If we succeed for all strongly connected components, the language of the DFA is recognized by a C-RASP program. Otherwise, we show that failure at any component entails non-membership in C-RASP. First, we will define a property of DFAs which determines their definability in C-RASP. Then, we will argue this property is decidable in polynomial time. We make the following assumptions, which simplify the presentation of the proof but do not affect the expressivity of C-RASP: ↼

1. All atoms occur bound within # (unbound atoms have a constant truth value since we would evaluate them on an <EOS> token). 2. No atom appears negatively (since atoms are disjoint, we didn’t need negation on them anyways). 49

Published as a conference paper at COLM 2026

Throughout, write A = ( Q, δ, Σ) for a semiautomaton where δ is extended to Σ∗ as usual. We write tq,w,i for the value of a C-RASP term t at position i of w when the run starts in state q, and q, w, i |= ϕ for the truth of a formula at that position. We write tq,w as shorthand for tq,w,|w| . We write L(A, q0 , F ) to denote the language recognized by A with start state q0 ∈ Q and accepting states F ⊆ Q. Definition 78 (SCC). W ⊆ Q is a strongly connected component of A if it is maximal such that for all q1 , q2 ∈ W there is w ∈ Σ∗ with δ(q1 , w) = q2 . W is trivial if W = {q} and δ(q, σ ) ̸= q for every σ. We will be reasoning about individual SCCs of an automaton, so we formalize what it means to take an SCC out of an automaton. Definition 79 (Extraction). Let W be an SCC of A. The extraction of W is the semiautomaton A ↾W = (W ⊔ SW , δW , Σ) where SW = {δ( p, σ) | p ∈ W, σ ∈ Σ} \ W  δ(q, σ ) q ∈ W δW (q, σ ) = q q ∈ SW . In other words, to extract an SCC you isolate the states of W and all other states reachable in one transition. These external states become sink states in the extracted semiautomaton. If a semiautomaton A is the extraction of a SCC from itself, then we say A is strongly connected. In the sequel, we will denote by SW the external sink states of an extracted SCC. We define the following helper function, which acts differently on internal states and external sink states of an SCC. Definition 80. Let A be a semiautomaton, W a SCC, q0 a state of A, and t a term of C-RASP. We define the following function:  q ,w,i {t 0 | δW (q0 , w≤i ) = q} q∈W Vq0 ,q (t) = {tq0 ,w,i | δW (q0 , w≤i−1 ) ∈ W, δW (q0 , w≤i ) = q} otherwise In other words, for states in W, the function Vq0 ,q take the set of all realizable counts on a path from q0 → q, and for states immediately outside of W we take the counts realizable by a path q0 → q which takes a single step from W to q. We will distinguish states in an automaton using terms which realize distinct sets of counts when in each state. However, only certain sets of counts can be distinguished by C-RASP formulas (which can be formalized by the “types” as in section E.2). Definition 81 (Separated). Let W be an SCC . Distinct q1 , q2 ∈ A ↾W are separated by a term t if there is some q0 ∈ W such that Vq0 ,q1 (t) ∩ Vq0 ,q2 (t) = ∅. We say W is separable if every pair of distinct states in A ↾W is separated by some t. We say W is separable if every pair of distinct states in A ↾W is separated by some t. Definition 82 (Balanced). The subterms of a term t are t itself alongside every term t′ occurring inside a subformula [t′ ≥ C ]. A term t is balanced on W if there is an interval [α, β] such that Vq0 ,q (t) ⊆ [α, β] for all q0 , q ∈ W. A term t is totally balanced on W if all subterms t′ ∈ t are balanced on W. A formula ϕ is balanced on W if every term occurring in ϕ is balanced on W. Intuitively, if ϕ is not balanced on W then we would see arbitrarily large or small values when checking the counters when the DFA is in states in W. An important observation is that for balanced terms, |V (t)| = 1. Lemma 83. If t is balanced on W, then |Vq0 ,q (t)| = 1 for all q0 , q ∈ Q. Proof. Suppose otherwise that some Vq0 ,q (t) holds two values x1 ̸= x2 . Since cycles in W must sum to 0 (otherwise t would be unbalanced), Vq,q0 (t) must contain − x1 and − x2 . However, this implies the existence of some cycle q0 → q0 with weight x1 − x2 ̸= 0. With these notions at hand, we are ready to state the main claim. 50

Published as a conference paper at COLM 2026

Lemma 84 (Definability Criterion). Let A = ( Q, δ, Σ) be a semiautomaton. The following are equivalent 1. L(A, q0 , F ) is recognizable in C-RASP for any q0 ∈ Q and F ⊆ Q. 2. A ↾W is separable by totally balanced terms for every SCC W in A. Proof. First, (2) ⇒ (1) is shown in lemma 84. Then, ¬(2) ⇒ ¬(1) is shown in lemma 84. Lemma 85. [Construction] Suppose every SCC in A is separable by totally balacned terms Fix q0 ∈ Q. Then for each q ∈ Q there exists a C-RASP formula ϕq such that w |= ϕq ⇐⇒ δ(q0 , w) = q. Proof. First, for any q ∈ Q not reachable from q0 we can set ϕq = ⊥. Otherwise, we induct on the reachability order of SCC’s in A. Consider the first SCC W containing q0 . Because W is separable by a totally balanced terms, for each q1 , q2 ∈ A ↾w there exists a totally balanced term t that separates them. We will define a formula ϕq1 ,¬q2 such that strings which land on q1 always satisfy ϕq1 ,q2 while strings that land in q2 do not. Since the sets of counts upon landing in each state form two disjoint finite sets, we can check these counts using a C-RASP formula:     ϕq1 ,¬q2 := 

_

t = c ∧ ¬ 

c∈Vq0 ,q1 (t)

_

t = c

c∈Vq0 ,q2 (t)

Then, we can let ϕq := q′ ̸=q∈A ↾W ϕq,¬q′ . For the inductive step on an SCC W ′ , we have by assumption formulas ϕq′ which detect entry into W ′ (as these are states in SW from previous 0 SCC’s). By assumption, there exists ϕq′ ,q which detects if A is in q if we started in state ϕq′ 0 0 Since, by assumption, no atom appears negatively, we can take ϕq and apply the mapping ↼ σ 7→ (σ ∧ # ϕq′ ≥ 1) to transform ϕq′ ,q 7→ ϕ̂q′ ,q . Intuitively, this transformation tells ϕq′ ,q 0 0 0 0 to ignore all symbols which occurred before the first q0′ (i.e. before we entered W ′ via q0′ ). Now, define the set of entry points EW ′ = {q | δ(q′ , σ ) = q, q′ ̸∈ W ′ }, and then we can let W ϕq = q′ ∈E ′ ϕ̂q′ ,q . V

0

W

0

Lemma 86 (Contradiction). Let A, q0 , F define the minimal automaton of a language. Suppose there exists an SCC W in A which is not separable by any totally balanced terms. Then L(A, q0 , F ) is not definable in C-RASP. Proof. Let ϕ be any C-RASP formula and C0 be larger than any theshold or coefficient in ↼ any subformula of the form ∑ χ · # [ψ] ≥ C. Since W is not separable by totally balanced terms, there are q1 , q2 ∈ W such that for all totally balanced terms t and entry points δ(q0 , x ) = qι , we have that Vqι ,q1 (t) = Vqι ,q2 (t). Let w1 and w2 be the minimal strings such that δ(qι , w1 ) = q1 and δ(qι , w2 ) = q2 . Let v ∈ Σ∗ be any distinguishing suffix of q1 and q2 – such that δ(q1 , v) ∈ F while δ(q2 , v) ̸∈ F –which always exists as q1 , q2 are distinct states in the minimal automaton. We will prepend very large loops around qι , carefully chosen so that all unbalanced terms ≫ C0 or ≪ C0 . Order all unbalanced terms t1 , t2 , . . . , tk . First, we note that for all unbalanced ti there exists q ,u u q ,u some loop ui ∈ Σ∗ such that δ(qι , ui ) = qι and the loop sum ti ι i i − ti ι i ̸= 0 – otherwise, Vqι ,qι (ti ) would be bounded and ti would not be unbalanced on W. Then, there exists some k

k −1

constant c such that the loop u := u1c u2c · · · uck has a nonzero sum for all terms (The constant is chosen such that no subsequent loop can “undo” the counts accumulated in previous loops, thus guaranteeing that all terms will have a nonzero sum). There exists a sufficiently large exponent N such that over a long prefix xu N , replacing all unbalanced terms with ∞ (or −∞, depending on the sum over u) results in a formula ψ whose truth value matches ϕ on all positions after the prefix in xu N w1 and xu N w2 . Intuitively, any formula [t ≥ C ] converges to ⊤ or ⊥ after enough iterations of u, and the 51

Published as a conference paper at COLM 2026

remaining iterations are used to drown out the finite prefix before convergence. Now, ψ had all unbalanced subformulas replaced with constants, so it is totally balanced. Thus, N N tq0 ,xu w1 = tq0 ,xu w2 , and appending the suffix v does not change this, so ϕ will have the same truth value on xu N w1 v as xu N w2 v – therefore ϕ cannot define L(A, q0 , F ). Now we will show that these conditions are decidable in polynomial time. We say that two terms are equivalent up to separation of states in the following sense: Each term defines an equivalence relation ≡t,q0 over states, where q1 ≈t,q0 q2 whenever Vq0 ,q1 (t) = Vq0 ,q2 (t). Lemma 87. [Depth-1 Balanced] Let A = ( Q, δ, Σ) be an SCC. The set of all depth-1 C-RASP terms up to equivalent separability of states can be computed in O(poly(| Q|, |Σ|) time. ↼

Proof. Let q0 ∈ Q. For every term ∑ χ p # [ϕ p ] occurring in a balanced depth-1 we must have
w,|w| ↼ that ∑ χσ # [σ] = 0 over any loop w, i.e. when δ(q0 , w) = q0 . Here, we use the fact that balanced terms are single-valued on each state of an SCC (lemma 83). First, we assert that such a balanced term exists iff there exists a function E : Σ → Z and V : Q → Z such that the following condition is satisfied: If δ(q1 , σ ) = q2 then V (q2 ) = V (q1 ) + E(σ )

(23) ↼

If such a function exists, we can obtain a term that sums to 0 on loops via ∑ E(σ ) # [σ]. If ↼ such a term ∑ χσ # [σ] exists, we can obtain the function by setting E(σ ) = χσ and V (q) = ∑1≤i≤|w| E(wi ) for any w such that δ(q0 , w) = q. The only other balanced terms are linear combinations of these terms, but these would all be equivalent with respect to separability of states. Deciding the existence of such a function can be done in O(poly(| Q|, |Σ|) time. There are O(| Q|2 |Σ|) many transitions δ(q1 , σ ) = q2 so we obtain O(| Q|2 · |Σ|) many constraints of the form V (q2 ) = V (q1 ) + E(σ ). These give O(| Q|2 |Σ|)-many linear constraints over O(| Q|2 · |Σ| + | Q|)-many variables. This can be solved in O(poly(| Q|, |Σ|) time (Kannan & Bachem, 1979). Lemma 88. Whether an SCC W is separable by totally balanced terms is decidable in O(poly(| Q|, |Σ|)) time. Proof. We will iteratively refine an equivalence relation ≡ over states, based upon the set of Vq0 ,q (t) over all terms. At the end, if all states are in their own equivalence class, the SCC is separable by a balanced formula. 1. Initialize ≡0 := W × W by setting all elements to the same class. Initialize a set of C-RASP formulas Φ0 := ∅. Fix a start state q0 (since a balanced term is balanced given any start state, the exact choice is immaterial). Then perform the loop (2) − (4): 2. Generate the set Bk of all terms that count over formulas in Φk−1 , up to equivalent separability of states using lemma 87. 3. Denote the indicator for K ⊆ W induced by t as the formula _

ψK :=

t = Vq0 ,q .

q∈K

We generate the collection of indicators of separable state sets by all t ∈ Bk as the collection Ψk := {ψK | Vq0 ,q1 (t) = Vq0 ,q2 (t) for all q1 , q2 ∈ K }. 4. Now there are two cases • If Ψk ̸⊆ Φk−1 , then define Φk to refine Φk−1 via intersection with Ψk . Φk := {ψK1 ∩ ψK2 | ψK1 ∈ Φk−1 , ψK2 ∈ Ψk }. Next, set ≡k := {(q1 , q2 ) | q1 , q2 ∈ K for some ϕK ∈ Φk }. Then, return to step (2) for iteration k + 1. 52

Published as a conference paper at COLM 2026

• If Ψk ⊆ Φk−1 , then we have reached a fixed point. Set Φ := Φk and ≡:=≡k and move to step (5). 5. If [q]≡ is a singleton for all q, output TRUE and return Φ. Otherwise, output FALSE. Correctness: Since each ϕK ∈ Φ is balanced, all its subterms are balanced and thus if [q]≡ are singletons we can obtain totally balanced terms which separate each pair of states. If some [q]≡ is not a singleton, we know there are two states that no totally balanced term can separate. Thus, the algorithm is correct. Polynomial running time: We crucially maintain that ≡k is monotonoically refined at each step, and Φ keeps only the formulas that define equivalence classes via ≡k , and thus there are only O(| Q|2 ) many of them at each iteration. The first step (1) runs in O(| Q|2 ) time. Step (2) takes O(poly(| Q|, |Σ|) time by lemma 87. Step (3) runs in O(poly(| Q|, |Σ|) time by generating in O(| Q|2 ) time the equivalence class where Vq0 ,q1 (t) = Vq0 ,q2 (t) for each of the O(poly(| Q|, |Σ|) terms t ∈ B. Step (4) runs in O(poly(| Q|, |Σ|) time, since the inclusion check is over polynomially sized sets and the intersection only needs to be done via pairs in Φk−1 × Ψk , since each formula identifies a disjoint set of states K. Step (5) also just needs to check if the equivalence relation has size | Q|, achievable in O(| Q|) time. Finally, we only need to iterate the (2 − 4) loop O(| Q|2 ) many times, as the equivalence relation ≡k is strictly refined at each step until a fixed-point is reached. Thus, this algorithm runs in polynomial time. Theorem 89. Checking whether or not every SCC in A is separable by a totally balanced terms is decidable in time polynomial in the size of A. Proof. We iterate over O(poly(| Q|, |Σ|) many SCCs (e.g. using Tarjan’s algorithm (Tarjan, 1972)), and only need to perform a O(poly(| Q|, |Σ|) time query on each one, as in lemma 88.

K

Implementation

A sketch of the algorithm used in the python implementation we have provided. For simplicity the implementation uses a looser version the algorithm which enumerates all loops in a strongly conected component (of which there may be exponentially many), though one could modify it to strictly be a polynomial time algorithm, as proven above. For each simple loop in a strongly connected component, the helper function B ALANCED L ABELS B ASIS computes the basis of all morphisms into Z given the constraint that all loops must be “balanced” (i.e. have the images of the symbols sum to 0). By computing the nullspace of this basis, we find all possible morphisms that sum to 0 on loops, and iteratively relable the symbols according to these morphisms. At the end, the helper function S EPARATED checks if all states have differing sets of outgoing transition labels (hence the states can be distinguished only using iterated counting – and thus being expressible in C-RASP).

53

Published as a conference paper at COLM 2026

Algorithm 1 C-RASP Membership 1: procedure D ECIDE M EMBERSHIP(A) 2: SCCs ← S TRONGLY C ONNECTED C OMPONENTS (A ) 3: for all SCC ∈ SCCs do 4: Bprev ← ∅ 5: Bcurr ← B ALANCED L ABELS B ASIS (SCC ) 6: if N ULLSPACE ( Bcur ) ̸= ∅ then 7: while Bcurr ̸∈ S PAN ( Bprev ) do 8: labels[σi ] ← [vi ]v∈ Bcurr 9: for all loop ∈ L OOPS A ROUND (q0 , SCC ) do 10: for all 0 ≤ i ≤ L EN (loop) do 11: (qi , σi , qi+1 ) ← loop  [i ]  h

 i SCC.δ.R EPLACE (qi , σ, qi+1 ), qi , σi , ∑1≤ j≤i labels[σj ] , qi+1 13: end for 14: Bprev ← Bcurr 15: Bcurr ← B ALANCED L ABELS B ASIS (SCC ) 16: end for 17: end while 18: end if 19: if ¬ S EPARATED (SCC ) then 20: return ⊥ 21: end if 22: end for 23: return ⊤ 24: end procedure

12:

54

Related documents

• Transformer MLP Gate Thresholds Are Couplings to a Carried Reference Direction#1115912
• Fast and Accurate CP-HIFI Tensor Decompositions: Exploiting Kronecker Structure#629952
• Fast and Accurate CP-HIFI Tensor Decompositions: Exploiting Kronecker Structure#628090
• Unitary Branching for $\mathfrak{sl}(m\vert n), \mathfrak{osp}(m\vert 2n)$ and $F(4)$#1034096
• Graded multiplicities in the Kostant-Rallis setting#798547