Paper deep dive

Algebraic Decomposition Theory for Transformer Length Generalization

Andy Yang, Blerta Veseli, Corentin Barloy, Michaël Cadilhac, Andreas Krebs, Charles Paperman, Howard Straubing, Michael Hahn

Year: 2026Venue: arXiv preprintArea: cs.FLType: PreprintEmbeddings: 234

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%

Last extracted: 8/16/2026, 2:28:37 AM

Summary

This paper establishes the first complete algebraic characterization of which regular languages transformer-based language models can length-generalize on, identifying this class as C-RASP. The authors generalize classical Krohn-Rhodes decomposition theory from finite semigroups to the infinite additive group of integers (Z), showing that C-RASP corresponds to languages whose syntactic monoids divide iterated wreath products of Z. They provide a polynomial-time decision algorithm for membership in C-RASP based on the size of the syntactic monoid, validated by experiments showing superior predictive accuracy over existing theories.

Entities (8)

Transformer · model-architecture · 98%C-RASP · formalism · 97%Length Generalization · capability · 96%Regular Languages · language-class · 95%Integers (Z) · mathematical-object · 93%Krohn-Rhodes Decomposition Theory · theory · 92%Wreath Product · mathematical-operation · 91%Syntactic Monoid · mathematical-object · 90%

Relation Signals (6)

Transformer → lengthgeneralizeson → C-RASP

confidence 95% · strong empirical evidence show that transformers tend to length-generalize on and only on the languages expressible in C-RASP

C-RASP → characterizedby → Wreath Product

confidence 94% · characterize C-RASP in terms of iterated wreath products of the integers

C-RASP → uses → Integers (Z)

confidence 93% · generalize classical decomposition theory from finite semigroups to the infinite additive group on the integers

Krohn-Rhodes Decomposition Theory → insufficientfor → C-RASP

confidence 92% · classical tools like Krohn-Rhodes decomposition theory for finite semigroups are insufficient for C-RASP

C-RASP → contains → Regular Languages

confidence 90% · establish the first complete characterization of which regular languages transformers length-generalize on

Syntactic Monoid → determines → Length Generalization

confidence 88% · decision algorithm running in polynomial time in the size of the language's syntactic monoid

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

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.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

232,425 characters extracted from source content.

Expand or collapse full text

Algebraic Decomposition Theory for Transformer Length Generalization Andy Yang Blerta Veseli Thanks: AY and BV are co-first authors. Contact: ayang4@nd.edu,blerta.veseli,mhahn@uni-saarland.de Corentin Barloy Michaël Cadilhac Andreas Krebs Charles Paperman Howard Straubing Affiliation: DePaul University, University of Tübingen, University of Lille, Boston College Michael Hahn [1ex] University of Notre Dame Saarland University Ruhr University Bochum 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.11 1 Code available at GitHub repository. 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)∗(ab+bbaa)^* and (ab+aabb)∗(ab+aabb)^*) may diverge sharply in terms of length-generalizability – and all existing theory fails to explain this discrepancy. abbbaa0255075100[lminl_min,50][51,100][101,150] ababb0255075100[lminl_min,50][51,100][101,150] Figure 1: DFAs for (ab+bbaa)∗(ab+bbaa)^* and (ab+aabb)∗(ab+aabb)^* and transformer length generalization on both. Transformers were trained on strings of length [lmin,50][l_min,50], where lminl_min 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 150150. Existing theory fails to explain why length-generalization differs between these simple regular languages with very similar structure. 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-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) (n) depth could express all regular languages, while constant depth transformers could express all solvable regular languages. The containment of ⁡(n) poly(n)-precision transformers within 0 TC^0 suggests transformers cannot express non-solvable regular languages (assuming 0≠1 TC^0≠ NC^1, as is common) (Merrill & Sabharwal 2023; Chiang 2025). Hahn 2020 showed that hard attention transformers recognized only languages in 0 AC^0, which Yang et al. 2024 later refined to the star-free regular languages, and Jerad et al. 2025 finally refined to the ℛR-trivial 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 length-generalize 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 showed that a regular language is in 0 AC^0 if and only if its syntactic morphism is quasi-aperiodic, 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 0 TC^0 is equivalent to the 4040 year old open problem of whether or not 0≠1 TC^0≠ NC^1 (Barrington 1989), and regular language membership in all levels of the dot-depth hierarchy is a 5050 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. - C-RASPRwpc() wpc(Dy)ωR^ωAREG (a) regular and subregular 0 TC^00 AC^0- C-RASP (b) circuits ℬ0B_0ℬ1B_1⋮ A- C-RASP (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. 2(a)). - C-RASP is contained in 0 TC^0, but incomparable to 0 AC^0 (fig. 2(b)). - C-RASP intersects every level of the dot depth hierarchy, while remaining incomparable to the full hierarchy (fig. 2(c)). 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 appendix C for additional definitions. The essential ones are presented here. Definition 1 (Monoid). A monoid (M,⋅,1)(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φ ^*→ M behaves like a finite automaton: after reading string w=w1⋯wnw=w_1·s w_n, the automaton is in state ϕ(w1)⋯ϕ(wn)φ(w_1)·sφ(w_n). Like a finite automaton, a monoid M recognizes a language L if there exists an accepting subset X⊆MX M and a homomorphism ϕ:Σ∗→Mφ ^*→ M such that L=ϕ−1(X)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 U1U_1 is the set 0,1\0,1\ where 0⋅1=1⋅0=0⋅0=00· 1=1· 0=0· 0=0 and 1⋅1=11· 1=1. The monoid U2U_2 is the set 1,a,b\1,a,b\ where x⋅a=ax· a=a, x⋅b=bx· b=b, and 1⋅x=x=x⋅11· x=x=x· 1 for any x∈U2x∈U_2. As an example, consider L=Σ∗aΣ∗L= ^*a ^* and the homomorphism ϕ:Σ∗→U1φ ^*→U_1 where ϕ⁡(σ)=0φ(σ)=0 iff σ=aσ=a. Then for any w∈Σ∗w∈ ^* we have that ϕ⁡(w)=0∈U1φ(w)=0∈U_1 iff in w∈Lw∈L. In some sense, U1U_1 captures the structure of LL (i.e. it detects if a ever occurs in the string). In fact, any monoid recognizing LL is divided by U1U_1, 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φ T→ M such that M=ϕ⁡(T)M=φ(T). Division is transitive. For a language L, the syntactic monoid M⁡(L)M(L) is the unique monoid which recognizes L and divides all other M that also recognize L. In the example above, U1U_1 is the syntactic monoid of L=Σ∗aΣ∗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∘NM N of finite monoids (M,+)(M,+) and (N,⋅)(N,·) is the monoid MN×NM^N× N with multiplication given by (f1,n1)(f2,n2)=(f1+f2n1,n1n2)(f_1,n_1)(f_2,n_2)=(f_1+^n_1f_2,n_1n_2), where the left action fn^nf is given by fn(n′)=f⁡(n′n)^nf(n )=f(n n). The wreath product M∘NM N together with a homomorphism ϕ:Σ∗→M∘Nφ ^*→ M N behaves like the composition of a finite automaton and a finite transducer. Let ϕM _M and ϕN _N be such that ϕ⁡(a)=(ϕM(a),ϕN(a))φ(a)=( _M(a), _N(a)) for all a∈Σa∈ . After reading a prefix w1⋯wtw_1·s w_t, the automaton is in state qt=ϕN(w1)⋯ϕN(wt)q_t= _N(w_1)·s _N(w_t), and the transducer is in state ϕM(w1)(q0)+ϕM(w2)(q1)+ϕM(w3)(q2)+…+ϕM(wt)(qt−1) _M(w_1)(q_0)+ _M(w_2)(q_1)+ _M(w_3)(q_2)+…+ _M(wt)(q_t-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 U2U_2 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 U2U_2 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 1:=(ab)∗D_1:=(ab)^* and k+1:=(akb)∗D_k+1:=(aD_kb)^*. 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 length-generalization outside of - C-RASP (Jobanputra et al. 2025). Furthermore, a form of fixed-precision 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 Krohn-Rhodes 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 appendix F. 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)⪯ℤ∘ℤM(L) Z for every LL. Proof. Without loss of generality let Σ=0,1 =\0,1\. Consider the submonoid of ℤ∘ℤZ Z generated by the image of Σ∗ ^* under the homomorphism σ↦(fσ,1)σ (f_σ,1) where fσ(x)=σ⋅2|x|f_σ(x)=σ· 2^|x|. In essence, this creates a mapping w↦(fw,|w|)w (f_w,|w|) where fw(0)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,M,ℰM)(M, T_M,E_M) where M is a finitely generated monoid, M T_M is a finite Boolean algebra over M, and ℰME_M is a finite subset of M. Elements of M T_M are the types and elements of ℰME_M are the units. A language L is recognized by (M,M,ℰM)(M, T_M,E_M) if there exists a homomorphism h:Σ∗→Mh ^*→ M such that h⁡(Σ)⊆ℰMh( ) E_M and L=h−1()L=h^-1( M) for some ∈M M∈ T_M. As an example, the language MAJORITY (there are more a’s than b’s) is recognized by the typed monoid (ℤ,(−∞,0],[1,∞),ℤ,∅,−1,1)(Z,$-∞,0],[1,∞),Z, \,\-1,1$ via the type [1,∞)[1,∞) and the homomorphism a↦1a 1 and b↦−1b -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,M,ℰM)(M, T_M,E_M), (N,N,ℰN)(N, T_N,E_N) be two typed monoids, and let C⊆NC N be a finite set. The typed wreath product (U,U,ℰU)=(M,M,ℰM)⋅∘C(N,N,ℰN)(U, T_U,E_U)=(M, T_M,E_M) 1.07639pt· _C(N, T_N,E_N) of (M,M,ℰM)(M, T_M,E_M) with (N,N,ℰN)(N, T_N,E_N) using constants C is defined such that • ℰUE_U consists of elements (f,n)(f,n), where n∈ℰNn∈E_N, and f:N→ℰMf:N→E_M is a type respecting function (see definition 32) with respect to (N,N,ℰN)(N, T_N,E_N) and C • U is the submonoid of M∘NM N generated by ℰUE_U • U T_U consists of types ,=(f,n)∣f(1N)∈,n∈ U_ M, N=\(f,n) f(1_N)∈ M,n∈ N\, where ∈M M∈ T_M, ∈N 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,M,ℰM) wpc(M, T_M,E_M) 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∈-⇔M⁡(L)∈wpc(ℤ)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 LL, we determine if M⁡(L)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 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-11 case, it is easy to check if M⁡(L)M(L) divides ℤZ (this is true e.g. for the AND language, L=1∗L=1^*). How would we check if M⁡(L)≺ℤ∘ℤM(L) Z? If we could “divide” out the right factor to obtain an object “M⁡(L)/ℤM(L)/Z”, we could check if ``M(L)/ℤ′≺ℤ``M(L)/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., LL 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 appendix G. In group theory, this question has a simple answer. With a surjective group homomorphism between groups ϕ:G→Hφ G→ H, we can “divide” G by ker⁡ϕ φ with a “quotient” of H, such that G⪯(ker⁡ϕ)∘HG ( φ) 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φ 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⁡(1)→U2φ M(D_1)→U_2? Intuitively, the wreath product M⁡(1)⪯N∘U2M(D_1) N U_2 should form a structure that contains elements (last symbol=a)(last symbol=a) and (last symbol=b)(last symbol=b). However, composition in this structure will be highly restricted – e.g. (this symbol=b)(last symbol=a)(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)Obj(X) and hom-sets X⁡(x1,x2)X(x_1,x_2), which are collections of arrows α:x1→x2α x_1→ x_2 for each pair of objects x1,x2∈Xx_1,x_2∈ X. Arrows can compose associatively, and each object has an identity arrow. A relational morphism of monoids ϕ:M⊲Nφ M N is a relation where ϕ⁡(m)≠∅φ(m)≠ , ϕ⁡(m1)ϕ(m2)⊆ϕ⁡(m1m2)φ(m_1)φ(m_2) φ(m_1m_2), and 1N∈ϕ⁡(1M)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φ M N, the correct notion of divisor turns out to be the derived category DϕD_φ. Here, Obj(Dϕ)=ϕ(M)Obj(D_φ)=φ(M) and Dϕ(n1,n2)=n1→(m,n)∣n∈ϕ(m),n1n=n2D_φ(n_1,n_2)=\n_1 _(m,n)\, n∈φ(m),n_1n=n_2\. Arrows compose via the rule n0→(m1,n1)n0n1→(m2,n2)=n0→(m1m2,n1n2)n_0 _(m_1,n_1)\,n_0n_1 _(m_2,n_2)\,=n_0 _(m_1m_2,n_1n_2)\,, 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φ M N, and a division Dϕ⪯VD_φ V, we obtain a division M⪯V∘NM V N. Thus, if ϕ:M⊲ℤφ:M Z, then DϕD_φ formalizes the object “M/ℤ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 1D_1 into wreath products of ℤZ We explain our decision procedure by walking through the division of the syntactic monoid of 1=(ab)∗D_1=(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⁡(1)M(D_1) as a category with a single object and arrows corresponding to monoid elements. We take a relational morphism into ϕ1:M⁡(1)⊲ℤ _1 M(D_1) [rgb]0.8477,0.1055,0.375Z where ϕ1(⊥)=ℤ _1( [rgb]0.1172,0.5352,0.8984 )= [rgb]0.8477,0.1055,0.375Z, ϕ1(a)=1 _1( [rgb]0.1172,0.5352,0.8984a)=\ [rgb]0.8477,0.1055,0.3751\, ϕ1(b)=−1 _1( [rgb]0.1172,0.5352,0.8984b)=\ [rgb]0.8477,0.1055,0.375-1\, ϕ1(ϵ)=ϕ1(ab)=ϕ1(ba)=0 _1( [rgb]0.1172,0.5352,0.8984ε)= _1( [rgb]0.1172,0.5352,0.8984ab)= _1( [rgb]0.1172,0.5352,0.8984ba)=\ [rgb]0.8477,0.1055,0.3750\. M [rgb]0.1172,0.5352,0.8984Mϵ [rgb]0.1172,0.5352,0.8984εa [rgb]0.1172,0.5352,0.8984ab [rgb]0.1172,0.5352,0.8984bab [rgb]0.1172,0.5352,0.8984abba [rgb]0.1172,0.5352,0.8984ba⊥ [rgb]0.1172,0.5352,0.8984 In the derived category Dϕ1D_ _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 ⊥ [rgb]0.1172,0.5352,0.8984 elements.0 [rgb]0.8477,0.1055,0.3750→(ϵ,0) _( [rgb]0.1172,0.5352,0.8984ε, [rgb]0.8477,0.1055,0.3750)\,→(ab,0) _( [rgb]0.1172,0.5352,0.8984ab, [rgb]0.8477,0.1055,0.3750)\,1 [rgb]0.8477,0.1055,0.3751→(ϵ,0) _( [rgb]0.1172,0.5352,0.8984ε, [rgb]0.8477,0.1055,0.3750)\,→(ba,0) _( [rgb]0.1172,0.5352,0.8984ba, [rgb]0.8477,0.1055,0.3750)\,−1 [rgb]0.8477,0.1055,0.375-12 [rgb]0.8477,0.1055,0.3752−2 [rgb]0.8477,0.1055,0.375-2⋯·s⋯·s0→(b,−1) [rgb]0.8477,0.1055,0.3750 _( [rgb]0.1172,0.5352,0.8984b, [rgb]0.8477,0.1055,0.375-1)\,1→(a,1) [rgb]0.8477,0.1055,0.3751 _( [rgb]0.1172,0.5352,0.8984a, [rgb]0.8477,0.1055,0.3751)\, We have not yet arrived at a division M⁡(1)⪯ℤM(D_1) because Dϕ1D_ _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⊲ℤ _1 D_ _1 [rgb]1,0.7578,0.0273Z where ψ1(x→(⊥,1))=ψ1(x→(⊥,−1))=[1,∞) _1( [rgb]0.8477,0.1055,0.375x _( [rgb]0.1172,0.5352,0.8984 , [rgb]0.8477,0.1055,0.3751)\,)= _1( [rgb]0.8477,0.1055,0.375x _( [rgb]0.1172,0.5352,0.8984 , [rgb]0.8477,0.1055,0.375-1)\,)=[ [rgb]1,0.7578,0.02731, [rgb]1,0.7578,0.0273∞) for all x [rgb]0.8477,0.1055,0.375x; arrows not associated to ⊥ [rgb]0.1172,0.5352,0.8984 are instead mapped to 0\ [rgb]1,0.7578,0.02730\. From ϕ1 _1, ψ1 _1 we define a relational morphism ϕ2:M⁡(1)⊲ℤ∘ℤ _2 M(D_1) [rgb]1,0.7578,0.0273Z [rgb]0.8477,0.1055,0.375Z where we let ϕ2(m)=(f(m,y),y)∣y∈ϕ1(m),∀x:f(m,y)(x)=ψ1(x→(m,y)) _2( [rgb]0.1172,0.5352,0.8984m)= \ ( [rgb]1,0.7578,0.0273f_( [rgb]0.1172,0.5352,0.8984m, [rgb]0.8477,0.1055,0.375y), [rgb]0.8477,0.1055,0.375y ) [rgb]0.8477,0.1055,0.375y∈ _1( [rgb]0.1172,0.5352,0.8984m),∀ [rgb]0.8477,0.1055,0.375x: [rgb]1,0.7578,0.0273f_( [rgb]0.1172,0.5352,0.8984m, [rgb]0.8477,0.1055,0.375y)( [rgb]0.8477,0.1055,0.375x)= _1 ( [rgb]0.8477,0.1055,0.375x _( [rgb]0.1172,0.5352,0.8984m, [rgb]0.8477,0.1055,0.375y)\, ) \. We visualize the derived category Dϕ2D_ _2 below (writing (fm,y)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984m, [rgb]0.8477,0.1055,0.375y) as shorthand for ϕ2(m) _2( [rgb]0.1172,0.5352,0.8984m) whenever it is unique).(fab,0)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ab, [rgb]0.8477,0.1055,0.3750)(fa,1)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984a, [rgb]0.8477,0.1055,0.3751)(fb,−1)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984b, [rgb]0.8477,0.1055,0.375-1)(fba,0)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ba, [rgb]0.8477,0.1055,0.3750)(f⊥,0)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984 , [rgb]0.8477,0.1055,0.3750)(f⊥,1)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984 , [rgb]0.8477,0.1055,0.3751)(f⊥,2)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984 , [rgb]0.8477,0.1055,0.3752)(f⊥,−1)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984 , [rgb]0.8477,0.1055,0.375-1)(f⊥,−2)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984 , [rgb]0.8477,0.1055,0.375-2)⋯·s⋯·s(fϵ,0)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ε, [rgb]0.8477,0.1055,0.3750)→(ϵ,(fϵ,0)) _( [rgb]0.1172,0.5352,0.8984ε,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ε, [rgb]0.8477,0.1055,0.3750))\,→(a,(fa,1)) _( [rgb]0.1172,0.5352,0.8984a,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984a, [rgb]0.8477,0.1055,0.3751))\,→(ab,(fab,0)) _( [rgb]0.1172,0.5352,0.8984ab,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ab, [rgb]0.8477,0.1055,0.3750))\,→(ba,(fba,0)) _( [rgb]0.1172,0.5352,0.8984ba,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ba, [rgb]0.8477,0.1055,0.3750))\,→(b,(fb,−1)) _( [rgb]0.1172,0.5352,0.8984b,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984b, [rgb]0.8477,0.1055,0.375-1))\,→(b,(fb,−1)) _( [rgb]0.1172,0.5352,0.8984b,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984b, [rgb]0.8477,0.1055,0.375-1))\,→(a,(fa,1)) _( [rgb]0.1172,0.5352,0.8984a,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984a, [rgb]0.8477,0.1055,0.3751))\,→(a,(fa,1)) _( [rgb]0.1172,0.5352,0.8984a,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984a, [rgb]0.8477,0.1055,0.3751))\,→(b,(fb,−1)) _( [rgb]0.1172,0.5352,0.8984b,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984b, [rgb]0.8477,0.1055,0.375-1))\,→(ϵ,(fϵ,0)) _( [rgb]0.1172,0.5352,0.8984ε,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ε, [rgb]0.8477,0.1055,0.3750))\,→(ab,(fab,0)) _( [rgb]0.1172,0.5352,0.8984ab,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ab, [rgb]0.8477,0.1055,0.3750))\,→(ϵ,(fϵ,0)) _( [rgb]0.1172,0.5352,0.8984ε,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ε, [rgb]0.8477,0.1055,0.3750))\,→(ba,(fba,0)) _( [rgb]0.1172,0.5352,0.8984ba,( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ba, [rgb]0.8477,0.1055,0.3750))\, We still do not have a division because there are still two arrows in a single homset of Dϕ2D_ _2, for instance ϕ2(ϵ) _2( [rgb]0.1172,0.5352,0.8984ε) and ϕ2(ab) _2( [rgb]0.1172,0.5352,0.8984ab) act the same on (fab,0)( [rgb]1,0.7578,0.0273f_ [rgb]0.1172,0.5352,0.8984ab, [rgb]0.8477,0.1055,0.3750). To handle this, we define a final relational morphism ϕ3:M⁡(1)⊲ℤ∘ℤ∘ℤ _3 M(D_1) Z [rgb]1,0.7578,0.0273Z [rgb]0.8477,0.1055,0.375Z such that ϕ3(m)=(g,ϕ2(m)) _3( [rgb]0.1172,0.5352,0.8984m)=(g, _2( [rgb]0.1172,0.5352,0.8984m)) where g⁡(x)=0g(x)=0 iff x=(f(ϵ,0),0)x=( [rgb]1,0.7578,0.0273f_( [rgb]0.1172,0.5352,0.8984ε, [rgb]0.8477,0.1055,0.3750), [rgb]0.8477,0.1055,0.3750). We ultimately obtain the division. ϕ3:M⁡(1)⪯ℤ∘ℤ∘ℤ _3 M(D_1) [rgb]1,0.7578,0.0273Z [rgb]0.8477,0.1055,0.375Z. 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)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+1i+1, we assume that a relational morphism ϕi _i covers all ℛR-classes up to RiR_i, and extend to a relational morphism ϕi+1 _i+1 that covers Ri+1R_i+1. This is done by iteratively computing nontrivial relational morphisms whose values are bounded on RiR_i. 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. 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)M(L) into a wreath product of ℤZ (and thus - C-RASP by 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)M(L) divides a T-fold iterated wreath product of ℤZ via a relational morphism ψ:M(L)⪯ℤ∘⋯∘ℤψ M(L) ·s Z (where T is minimal). The rightmost component defines a relational morphism ω:M⁡(L)⊲ℤω: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)(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 kD_k). 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 monoids22 2 ωR^ω alludes to the equation for ℛR-trivial monoids, (xy)ω=(xy)ωx(xy)^ω=(xy)^ωx (Almeida & Azevedo 1989) as ω:(xyω)ωx=(xyω)ω.R^ω:(xy^ω)^ωx=(xy^ω)^ω. For our purposes, a finite monoid M satisfies ωR^ω if for any m1,m2∈Mm_1,m_2∈ M we have that (m1m2ω)ω=(m1m2ω)ωm1(m_1m_2^ω)^ω=(m_1m_2^ω)^ωm_1, where mωm^ω denotes mkm^k such that mk=m2km^k=m^2k (i.e. the unique idempotent generated by m). We give an exact characterization of the monoids in ωR^ω, the proof of which is in appendix I. Theorem 13. M∈ω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 length-generalization. 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. -∩=wpc() C-RASP∩REG= wpc(Dy). Hence ⊊-∩⊊ω⊊R C-RASP∩REG R^ω A REG A proof is given in appendix 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∈-∩M∈ C-RASP∩REG is decidable in O⁡(⁡(|M|))O( poly(|M|)) time. 5 Experiments Figure 3: Length generalization on regular languages. Models are trained on strings of lengths in [lmin,50][l_ ,50], and evaluated on bins [lmin,50][l_ ,50] (in-distribution) up to [451,500][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. We empirically evaluate whether our characterization of regular languages in - C-RASP predicts transformer length-generalization. In particular, we examine the different levels of the hierarchy shown in 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 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 appendix J. 5.2 Experimental Setup Task Definition. The task is state prediction, i.e. tracking automaton states over prefixes. Let w=a1…anw=a_1… a_n, and denote by w1:i=a1…aiw_1:i=a_1… a_i the prefix of length i. Each symbol aia_i triggers a transition, and the model must predict the sequence of DFA states q1,…,qnq_1,…,q_n, where qiq_i is the state reached after processing w1:iw_1:i. Training and Evaluation. Per formal language, we train GPT-2 models on 10,000 words sampled from the training length range [lmin,50][l_min,50] with lminl_min 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][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×2× the maximum training length 5050. 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\1,2,4\, heads 1,2,4\1,2,4\, dimension 16,64,256\16,64,256\ and learning rates 0.001,0.0001\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\6,8,12\, heads 4,8\4,8\, dimensions 64,256\64,256\ and learning rates 0.001,0.0001\0.001,0.0001\. We adopted optimization choices and hyperparameter ranges from Huang et al. 2025. Per 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][l_min,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 aia_i when predicting the target state qiq_i, 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 qiq_i 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> 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 # 5.3 Results Figure 3 shows that - C-RASP membership is a strong predictor of transformer length-generalization. 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 length-generalize 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 length-generalize. 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 U2U_2. 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. 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 Almeida & Azevedo (1989) 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://w.sciencedirect.com/science/article/pii/0022404989901254. Alsmann et al. (2026) 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. Barrington (1989) 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. Barrington et al. (1992) 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. Behle et al. (2011) Christoph Behle, Andreas Krebs, and Stephanie Reifferscheid. Typed monoids – an eilenberg-like theorem for non regular languages. In Franz Winkler (ed.), Algebraic Informatics, p. 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. Bhattamishra et al. (2020) 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), p. 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/. Brzozowski & Fich (1980) 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. Chiang (2025) David Chiang. Transformers in uniform TC0. Transactions on Machine Learning Research, 2025. ISSN 2835-8856. URL https://openreview.net/forum?id=ZA7D4nQuQF. Gehrke & Krebs (2017) 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. Hahn (2020) 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. Huang et al. (2025) 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. Jerad et al. (2025) 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), p. 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/. Jobanputra et al. (2025) 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. Kannan & Bachem (1979) 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. Kaplan & Kay (1994) 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/. Kim & Schuster (2023) 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), p. 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/. Kleene (1956) S. C. Kleene. Representation of Events in Nerve Nets and Finite Automata, p. 3–42. Princeton University Press, Princeton, 1956. ISBN 9781400882618. doi: doi:10.1515/9781400882618-002. URL https://doi.org/10.1515/9781400882618-002. Krebs (2008) 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. Krohn & Rhodes (1965) 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. Li & Cotterell (2025) 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. Li et al. (2024) 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. Liu et al. (2023a) 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. Liu et al. (2023b) 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. Merrill & Sabharwal (2023) 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, p. 52453–52463. Curran Associates, Inc., 2023. URL https://proceedings.neurips.c/paper_files/paper/2023/file/a48e5877c7bf86a513950ab23b360498-Paper-Conference.pdf. Merrill & Sabharwal (2025) 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. Pin (2009) 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), p. 31–50, Dagstuhl, Germany, 2009. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. ISBN 978-3-939897-09-5. doi: 10.4230/LIPIcs.STACS.2009.1856. URL https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1856. Pin (2017) 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. Pin (2025) Jean-Éric Pin. Mathematical foundations of automata theory. Lecture notes, MPRI, IRIF, CNRS and Université de Paris. Available at https://w.irif.fr/~jep/PDF/MPRI/MPRI.pdf, 2025. Rhodes (1999) 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. Sarrof et al. (2024) 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. Schall & de Melo (2025) 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, p. 1074–1084, Varna, Bulgaria, September 2025. INCOMA Ltd., Shoumen, Bulgaria. URL https://aclanthology.org/2025.ranlp-1.124/. Schluntz & Zhang (2024) Erik Schluntz and Barry Zhang. Building effective agents. https://w.anthropic.com/engineering/building-effective-agents, December 2024. Accessed: 2026-03-23. Schützenberger (1965) 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. Simon (1975) Imre Simon. Piecewise testable events. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, p. 214–222, Berlin, Heidelberg, 1975. Springer-Verlag. ISBN 3540074074. doi: https://doi.org/10.1007/3-540-07407-4˙23. Sipser (1996) 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. Stiffler Jr (1973) 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. Tarjan (1972) 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. Thérien & Wilke (2001) 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. Tilson (1987) 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. van der Poel et al. (2024) 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. Yang & Chiang (2024) 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. Yang et al. (2024) 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. Yang et al. (2025) 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. Contents 1 Introduction 2 Algebraic Preliminaries 2.1 Basics: Algebraic Theory of Formal Languages 2.2 Background: Classical Algebraic Decomposition Theory of Regular Languages 3 Algebraic Characterization of - C-RASP 3.1 Typed Monoids 3.2 Wreath Product Characterization 4 Decomposition Theory for Regular Languages in - C-RASP 4.1 Categories 4.2 Decomposition of 1D_1 into wreath products of ℤZ 4.3 Algebraic Decision Procedure 4.4 Necessary (but not Sufficient) Condition via Equations 4.5 Algebraic Characterization 5 Experiments 5.1 Languages 5.2 Experimental Setup 5.3 Results 6 Conclusion References A FAQ B Additional Experimental Results B.1 Additional Results on the Main Language Suite B.1.1 Results by C-RASP Membership B.1.2 Length Generalization Across Seeds and Languages B.1.3 Increased Training Data Size B.2 Experiments on More Complex Languages B.2.1 Length Generalization B.2.2 Results by C-RASP Membership B.2.3 Length Generalization Across Seeds and Languages B.3 Regular Languages C Algebraic Preliminaries D Linear RASP programs E Typed Monoids E.1 Definitions E.2 Proof of Typed Wreath Product Principle F - C-RASP F.1 Definitions F.2 - C-RASP as a pseudovariety of Languages F.3 Existing Characterizations F.4 Algebraic Characterization of - C-RASP G Derived Categories H Algebraic Decision Procedure H.1 Relevant Lemmas H.2 Bounded-Depth Dyck Monoids H.3 Decidability Proof (via Finite Derived Categories) H.3.1 Key Properties of the Procedure H.3.2 Establishing Completeness H.3.3 Deriving Main Results H.4 Defining Division between Categories and Typed Monoids I Algebraic Characterization (Necessary but not Sufficient Criterion) J Automata proof of -∩ C-RASP∩REG K Implementation 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. Appendix 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. 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 0 AC^0 and 0 TC^0; neither of them captures - C-RASP or transformer length generalization well. - C-RASP is a strict subset of 0 TC^0, as was shown in Huang et al. 2025. This extends to regular languages: E.g., the PARITY language (b∗ab∗ab∗)(b^*ab^*ab^*) (checking if the number of a’s is even) is in 0 TC^0 but not in - C-RASP. In general, - C-RASP is incomparable with AC0AC^0. Interestingly, on the level of regular languages, - C-RASP is a strict subset of 0 AC^0: - C-RASP only includes star-free languages (and all of those are in AC0AC^0), but, for instance, a,b∗b\a,b\^*b is in 0 AC^0 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 monoids, as we have done here. An example where this plays a role is a,b∗b\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∗\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 12N12N. While Huang et al. 2025 showed length-generalization in languages in -∖ C-RASP R, they only trained on length N and tested up to 3N3N, 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 10N10N, 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 33 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. Appendix 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][l_min,50] to [lmin,200][l_min,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 Additional Results on the Main Language Suite B.1.1 Results by C-RASP Membership 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. Figure 4: Length generalization by - C-RASP membership. Models are trained on strings of lengths in [lmin,50][l_min,50] and evaluated on ranges from [lmin,50][l_min,50] (in-distribution) up to [451,500][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%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. Figure 5: Length generalization on regular languages (aggregated across languages and seeds). Models are trained on strings of lengths in [lmin,50][l_min,50] and evaluated on length ranges from [lmin,50][l_min,50] (in-distribution) up to [451,500][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%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. Figure 6: Length generalization by - C-RASP membership, aggregated across languages and seeds. Models are trained on strings of lengths in [lmin,50][l_min,50] and evaluated on length ranges from [lmin,50][l_min,50] (in-distribution) up to [451,500][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%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. Figure 7: Length generalization on regular languages with increased training data. Models are trained on strings of lengths in [lmin,50][l_min,50] using a larger training set (100K examples instead of 10K), and evaluated on lengths from [lmin,50][l_min,50] (in-distribution) up to [401,500][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. Figure 8: Length generalization by - C-RASP membership with increased training data. Models are trained on strings of lengths in [lmin,50][l_min,50] using a larger training set (100K examples instead of 10K) and evaluated on length ranges from [lmin,50][l_min,50] (in-distribution) up to [401,500][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, -∖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. Figure 9: Length generalization on regular languages (longer training length). Models are trained on strings of lengths in [lmin,200][l_min,200], and evaluated on length ranges [lmin,200][l_min,200] (in-distribution) up to [401,500][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 Figure 10: Length generalization by - C-RASP membership (longer training length). Models are trained on strings of lengths in [lmin,200][l_min,200] and evaluated on length ranges from [lmin,200][l_min,200] (in-distribution) up to [401,500][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, -∖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. Figure 11: Length generalization on regular languages (aggregated across languages and seeds). Models are trained on strings of lengths in [lmin,200][l_min,200] and evaluated on length ranges from [lmin,200][l_min,200] (in-distribution) up to [401,500][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%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. Figure 12: Length generalization by - C-RASP membership, aggregated across languages and seeds. Models are trained on strings of lengths in [lmin,200][l_min,200] and evaluated on length ranges from [lmin,200][l_min,200] (in-distribution) up to [401,500][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%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, -∖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. Formal Language R - C-RASP ωR^ω ∘R G Formal Language R - C-RASP ωR^ω ∘R G (bbac)∗(bbac)^* False True True True (ab)∗+(bb)∗(ab)^*+(b)^* False False False True (bab+b)∗(bab+b)^* False False False False (bb)∗(bb)∗(b)^*(b)^* False False False True (c+b(a)∗)∗(c+b(a)^*)^* False False False False ((b)∗ac)∗((b)^*ac)^* False False False False b+(bb)∗b+(b)^* False False False True (bc(c)∗)∗(bc(c)^*)^* False False False False acabcc(c)∗acabcc(c)^* True True True True (baa+a)∗(baa+a)^* False False False False bbcc(aa)∗bbcc(a)^* False False False True (ac)∗c+ba+a(ac)^*c+ba+a False True True True (ab(a)∗)∗(ab(a)^*)^* False False False False (b+a)∗aaac(b+a)^*aaac False False False False (cc)∗(c)^* False False False True (bb)∗cbac(b)^*cbac False False False True ((a)∗ac)∗((a)^*ac)^* False False False False ((b)∗)∗(ab)∗((b)^*)^*(ab)^* False True True True ((b)∗ab)∗((b)^*ab)^* False False False False bba(c+a)∗bba(c+a)^* True True True True (ac(a)∗)∗(ac(a)^*)^* False False False False cb(a)∗baacb(a)^*baa True True True True (cca+a)∗(cca+a)^* False False False False (b)∗baa(b)^*baa True True True True cb(a)∗+abbccb(a)^*+abbc True True True True (aa+(b)∗)∗(a+(b)^*)^* False False False True aa(a)∗caa(a)^*c True True True True aa+ca(aa)∗a+ca(a)^* False False False True (aa+aa)∗(a+a)^* False False False True (a)∗(a)∗b+aac(a)^*(a)^*b+aac True True True True (a+c)∗cbbb(a+c)^*cbbb False False False False (bb)∗ab+ac(b)^*ab+ac False False False True bc(b)∗abbbbc(b)^*abbb True True True True (cc)∗cccb(c)^*cccb False False False True (ca)∗(cb)∗(ca)^*(cb)^* False True True True (b)∗cbbcaa(b)^*cbbcaa True True True True (cc)∗ccb+b(c)^*ccb+b False False False True ((b)∗b)∗((b)^*b)^* True True True True ((a)∗)∗(ac)∗((a)^*)^*(ac)^* False True True True ccc(ba)∗c(ba)^* False True True True bccb(aa)∗bccb(a)^* False False False True bcac(a)∗+babcac(a)^*+ba True True True True (ba)∗(b)∗bc(ba)^*(b)^*bc False True True True (b)∗cc(ca)∗(b)^*c(ca)^* False True True True (ac)∗ba(b)∗(ac)^*ba(b)^* False True True True (cab+c)∗(cab+c)^* False False False False (a)∗b+acab(a)^*b+acab True True True True (a+ac+a)∗(a+ac+a)^* False False False False (ca)∗(a)∗bb(ca)^*(a)^*b False True True True aba+c(bb)∗aba+c(b)^* False False False True (b)∗(b)∗(aa)∗(b)^*(b)^*(a)^* False False False True ((a)∗ca)∗((a)^*ca)^* False False False False b+ca+b(c+a)∗b+ca+b(c+a)^* True True True True (abbc)∗(abbc)^* False True True True (cbb+b)∗(cbb+b)^* False False False False (a+c)∗(cb)∗(a+c)^*(cb)^* False False False False c+cab+(bc)∗c+cab+(bc)^* False True True True (aa)∗bb(a)∗(a)^*b(a)^* False False False True (c)∗b+b(b)∗(c)^*b+b(b)^* True True True True a(bc)∗a(bc)^* False True True True (ca(c)∗)∗(ca(c)^*)^* False False False False (ca)∗(ab)∗(ca)^*(ab)^* False True True True bab(ba)∗bab(ba)^* False True True True ((ac)∗)∗((ac)^*)^* False True True True bbbc(ca)∗bbbc(ca)^* False True True True (ba+a+c)∗(ba+a+c)^* False False False False (abcb)∗(abcb)^* False True True True ((a)∗)∗(cc)∗((a)^*)^*(c)^* False False False True cc+cc(bb)∗c+c(b)^* False False False True ((b)∗a+c)∗((b)^*a+c)^* False False False False bcba+(a)∗aabcba+(a)^*a True True True True (ba)∗cb+aa(ba)^*cb+a False True True True a+c(a)∗cb+a+c(a)^*cb+a True True True True (baaa)∗(baaa)^* False True True True (cb(c)∗)∗(cb(c)^*)^* False False False False (baa+b)∗(baa+b)^* False False False False ((b)∗bc)∗((b)^*bc)^* False False False False ccc(b)∗c(b)^* True True True True (a+aac)∗(a+aac)^* False False False False aa(c)∗+acca(c)^*+acca True True True True (cb)∗caa+b(cb)^*caa+b False True True True (a)∗caaa+c(a)^*caaa+c True True True True caaba+(a)∗caaba+(a)^* True True True True ((a)∗bb)∗((a)^*b)^* False False False False (cc)∗bac(c)^*bac False False False True (bb)∗(c)∗ac(b)^*(c)^*ac False False False True (b+ac+c)∗(b+ac+c)^* False False False False (b)∗b+aa+bba(b)^*b+a+bba True True True True (acba)∗(acba)^* False True True True (b+bc)∗(b+bc)^* False False False False cbac(a)∗cbac(a)^* True True True True (b)∗cc(b)∗ca(b)^*c(b)^*ca True True True True (a)∗(a)∗(bb)∗(a)^*(a)^*(b)^* False False False True aca(a)∗aca(a)^* True True True True ((a)∗ab)∗((a)^*ab)^* False False False False bcbb(bb)∗bcbb(b)^* False False False True baca(bc)∗baca(bc)^* False True True True (a)∗a(b+b)∗(a)^*a(b+b)^* True True True True (ca)∗(cc)∗(ca)^*(c)^* False False False True b+c+ac(ac)∗b+c+ac(ac)^* False True True True (ab+aabb)∗(ab+aabb)^* False False False False (ab+bbaa)∗(ab+bbaa)^* False True True True (aa)∗(a)^* False False False True (a+b+)+(a^+b^+)+ False False False False (ab)+a+(ab)^+a^+ False True True True (ab)+a+b+(ab)^+a^+b^+ False True True True (ab)+a+b+a+(ab)^+a^+b^+a^+ False True True True ((ab)+b+)+((ab)^+b^+)^+ False False False False ((ab)+b+)k((ab)^+b^+)^k False True True True (ab+ba)∗(ab+ba)^* False True True True (ab)+b(ab)+(ab)^+b(ab)^+ False True True True (ab+bba)∗(ab+bba)^* False False True True (a+b+)k(a+b+)^k True True True True abe∗be∗abe^*be^* False False False False (ab)∗(ab)^* False True True True (a(ab)∗b)∗(a(ab)^*b)^* False True True True bΣ∗b ^* True True True True Σ∗b ^*b False False False False (Σ∖a,b0)∗a(Σ∖b1)∗( \! \!\a,b_0\)^*a( \! \!\b_1\)^* True True True True (Σ∖a1,b0)∗a1(Σ∖a2,b1)∗a2(Σ∖b2)∗( \! \!\a_1,b_0\)^*a_1( \! \!\a_2,b_1\)^*a_2( \! \!\b_2\)^* True True True True Σ∗aΣ∗ ^*a ^* True True True True Σ∗abΣ∗ ^*ab ^* True True True True a∗(ba∗ba∗)∗a^*(ba^*ba^*)^* False False False True Σ∗aΣ∗bΣ∗ ^*a ^*b ^* True True True True (Σ∖b0)∗a(Σ∖a,b1)∗( \! \!b_0)^*a( \! \!a,b_1)^* False False False False 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 lminl_min–50) and 1K words for each evaluation length bin. Formal Language R - C-RASP ωR^ω ∘R G (ab)∗bb(aabb)∗(ab)^*b(aabb)^* False True True True (abb)∗(a)(c+a)(a)cbb+a∗(c)(abb)^*(a)(c+a)(a)cbb+a^*(c) False True True True (b∗ca+ca)(ac+b)(c+a)∗(b)∗+(bc)∗(b+c)(c)+a(c)∗caa(b^*ca+ca)(ac+b)(c+a)^*(b)^*+(bc)^*(b+c)(c)+a(c)^*caa False True True True (b∗bc+bb)c(a)(a)c∗aa+(bc)∗(b)∗(b)b∗aa+(a+a)(b)aba+(c)∗c∗bc+b∗+bc+a(b^*bc+b)c(a)(a)c^*a+(bc)^*(b)^*(b)b^*a+(a+a)(b)aba+(c)^*c^*bc+b^*+bc+a False True True True (cba)∗a(cba)^*a False True True True (cac)∗b(b+c)∗a∗+bb+a⁡(b)a∗ba+(a)∗c∗bb(cac)^*b(b+c)^*a^*+b+a(b)a^*ba+(a)^*c^*b False True True True (cb)∗ab+(aa+a)∗a(a)bba(cb)^*ab+(a+a)^*a(a)bba False True True True (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(ac+a+c)(ca+b+b)(c+a)^*ba^*ab+(ab+c)^*(b+c)^*(b)^*a^*ac+c+b^*abc+b^*cb+bc+c+b False True True True (c∗cc+b)(bc)∗(c+a)∗+(bc+a)∗+b(c^*c+b)(bc)^*(c+a)^*+(bc+a)^*+b False True True True (acc)∗+(ab+c+b)(a+b)∗+(a+b)+cabc(acc)^*+(ab+c+b)(a+b)^*+(a+b)+cabc False True True True (cac)∗(ca+c+c)(c)(b)∗ccc+(ac+c+a)∗a∗(c)∗ba+(a+a)∗(a)a(cac)^*(ca+c+c)(c)(b)^*c+(ac+c+a)^*a^*(c)^*ba+(a+a)^*(a)a False True True True (bcb)∗(b)(b)∗(c)∗a∗(bcb)^*(b)(b)^*(c)^*a^* False True True True (a∗ac+ba+a+a)(ab+c)∗ba∗b∗bc(a^*ac+ba+a+a)(ab+c)^*ba^*b^*bc False True True True (bcb+c+c+c)(bc+c+b)(b+a)∗(a)∗bba(bcb+c+c+c)(bc+c+b)(b+a)^*(a)^*bba False False False False (a∗cc+bb+b)(ac)∗b∗+(c+b+b)∗(a)(b)a∗ba+(a+c)∗cc(a^*c+b+b)(ac)^*b^*+(c+b+b)^*(a)(b)a^*ba+(a+c)^*c False False False False (bcb+cb+a+c)∗(bcb+cb+a+c)^* False False False False (ccb+ac+c+b)+(cc+b)∗(b+c)∗(c)cba+a∗(ccb+ac+c+b)+(c+b)^*(b+c)^*(c)cba+a^* False False False False b∗+(cb+a)∗(c+b)∗c∗c∗c+(a+a)∗(c)b∗+(b)∗b^*+(cb+a)^*(c+b)^*c^*c^*c+(a+a)^*(c)b^*+(b)^* False False False False (b∗c+ba)∗c∗+(aa+b+c)(a+c)a∗ccc(b^*c+ba)^*c^*+(a+b+c)(a+c)a^*c False False False False (a∗ab+cb+a+c)∗(a^*ab+cb+a+c)^* False False False False (cbb+cb+a+a)(ca+b+c)∗(c+b)∗(b)∗b∗+(cb)∗(a+b)(b)+b⁡(b)c∗ba(cbb+cb+a+a)(ca+b+c)^*(c+b)^*(b)^*b^*+(cb)^*(a+b)(b)+b(b)c^*ba False False False False (b∗ab+ab+a+c)∗(cb+b)(b)∗+c∗(b+b)∗(c)∗(b^*ab+ab+a+c)^*(cb+b)(b)^*+c^*(b+b)^*(c)^* False False False False (a∗bb+ba+b+b)∗+b∗(b+a)(c)acb+c⁡(b)b∗b+aaba+cc(a^*b+ba+b+b)^*+b^*(b+a)(c)acb+c(b)b^*b+aaba+c False False False False (c∗bb+bb+c)+(ab+c+c)∗ab+(b+c)∗a+ab(c^*b+b+c)+(ab+c+c)^*ab+(b+c)^*a+ab False False False False (c∗+bb+c+a)(ac+a)c(c)a∗ab+(cb+b+a)(a)a∗c+(c+b)∗(b)b∗a(c^*+b+c+a)(ac+a)c(c)a^*ab+(cb+b+a)(a)a^*c+(c+b)^*(b)b^*a False False False False (b∗ca+cb+b)∗(a+a)(b+a)a(b^*ca+cb+b)^*(a+a)(b+a)a False False False False (baa+ab+b)∗(baa+ab+b)^* False False False False (c∗+ac+a+b)∗b∗(c+b)(c^*+ac+a+b)^*b^*(c+b) False False False False (a∗cb+ca+b+a)c+a∗c∗c∗+(b+a)∗(a)∗b∗ac+(b)a∗c(a^*cb+ca+b+a)c+a^*c^*c^*+(b+a)^*(a)^*b^*ac+(b)a^*c False False False False a∗+(aa+a+c)(a)(b)∗b+(b+a)∗(a)bba^*+(a+a+c)(a)(b)^*b+(b+a)^*(a)bba False False False False (abb+b)(ba+c+c)(c+a)+(b)(a+b)∗+(c)b∗c∗+(a)∗a∗a(abb+b)(ba+c+c)(c+a)+(b)(a+b)^*+(c)b^*c^*+(a)^*a^*a True True True True (b∗cc+bb+b+a)(ca+b)(b^*c+b+b+a)(ca+b) True True True True (b∗b+ca+b+c)(a+a+c)∗(a+c)+(aa+c)a(a)(b^*b+ca+b+c)(a+a+c)^*(a+c)+(a+c)a(a) True True True True (a∗)∗(a^*)^* True True True True (aca)∗(a+c+a)∗+(ba+b+a)∗cc∗c∗+(c)(b)∗b+b∗aab+b(aca)^*(a+c+a)^*+(ba+b+a)^*c^*c^*+(c)(b)^*b+b^*aab+b True True True True (cbc)(bc)a∗(c)∗a∗ab+a∗(a+b)(c)c∗bb+c∗(c)∗a∗aa(cbc)(bc)a^*(c)^*a^*ab+a^*(a+b)(c)c^*b+c^*(c)^*a^*a True True True True b∗(ba+c)c∗c∗+c(b+b)∗bccc+(c)a∗c∗bb+a∗c∗ccb^*(ba+c)c^*c^*+c(b+b)^*bccc+(c)a^*c^*b+a^*c^*c True True True True b+b∗(c)(b)cca+ac∗baa+(b)∗ac+b∗cb+b+c+b+b^*(c)(b)cca+ac^*baa+(b)^*ac+b^*cb+b+c+b True True True True (acc+c+c+b)(a)(a+a)∗(a)∗bbb+(ba+a+b)+a∗ca∗aa+(b)+acc(acc+c+c+b)(a)(a+a)^*(a)^*b+(ba+a+b)+a^*ca^*a+(b)+acc True True True True a∗b∗+a⁡(b+a)(a)b∗aca^*b^*+a(b+a)(a)b^*ac True True True True (a∗b)∗+(ac+b+a)b∗bc∗cb(a^*b)^*+(ac+b+a)b^*bc^*cb False False False False (a∗ac)+c∗b(c)∗+(c+b)∗+(b)aac(a^*ac)+c^*b(c)^*+(c+b)^*+(b)aac True True True True a∗+(a)∗a^*+(a)^* True True True True (a+bb)∗a∗(a+b)^*a^* False False False True (b∗bc)+(aa+c)∗(b^*bc)+(a+c)^* False False False True (cc+aa+a+b)(aa+b+b)∗+b∗b+(b+b)(c)aca+(a)∗acb+cab(c+a+a+b)(a+b+b)^*+b^*b+(b+b)(c)aca+(a)^*acb+cab False False False True (b+aa+b+c)∗(b+a+b+c)^* False False False True b(aa+c)∗(b)(b)ccab(a+c)^*(b)(b)cca False False False True (a)+(bb)∗+a∗a∗cacb(a)+(b)^*+a^*a^*cacb False False False True (b∗cc)∗(b^*c)^* 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−200l_min-200) and 1K words for each evaluation length bin. Appendix C Algebraic Preliminaries Definition 16 (Recognition; Syntactic Monoid). Let L⊆Σ∗L ^* be a language. A monoid M recognizes LL iff there is a homomorphism h:Σ∗→Mh ^*→ M and a subset X⊆MX M such that L=h−1(X)L=h^-1(X). The syntactic monoid M⁡(L)M(L) of a language LL is the minimal monoid (up to isomorphism) which recognizes LL. Definition 17 (Basic Units). The three basic semigroup units U1,U3,U2U_1,U_3,U_2 are given with their multiplication tables, where rows denote the first operand and columns denote the second. U1U_1 0 1 0 0 0 1 0 1 U3U_3 a b a a b b a b U2U_2 1 a b 1 1 a b a a a b b b a b Definition 18 (Basic monoid operations). We define basic monoid operations. • Submonoid. A monoid M is a submonoid of N (usually written M≤NM≤ N) whenever M⊆NM N and M is closed under the monoid operation of N. • Direct product. The direct product M×NM× N of monoids M and N has elements (m,n)(m,n) where m∈Mm∈ M and n∈Nn∈ N, with the operation (m1,n1)⋅M×N(m2,n2)=(m1⋅Mm2,n1⋅Nn2)(m_1,n_1)·_M× N(m_2,n_2)=(m_1·_Mm_2,n_1·_Nn_2). • Homomorphism. A homomorphism of monoids ϕ:M→Nφ M→ N is a function such that ϕ⁡(1M)=1Nφ(1_M)=1_N and ϕ⁡(m1)ϕ(m2)=ϕ⁡(m1m2)φ(m_1)φ(m_2)=φ(m_1m_2). • Division. A monoid M divides a monoid N (written M⪯NM N) whenever there is a submonoid X≤NX≤ N of N and a homomorphism ϕ:X→Mφ X→ M such that M=ϕ⁡(X)M=φ(X) 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−1Lb−1a^-1Lb^-1). Definition 20. Define ∘V W as the pseudovariety generated by all V∘WV W where V∈V∈V and W∈W∈W. Define wp1()= wp^1(V)=V, wpk+1()=wpk()∘ wp^k+1(V)= wp^k(V) V, and wpc()=⋃k>0wpk() wpc(V)= _k>0 wp^k(V). We also define wpk(M) wp^k(M) for monoids, taking wp1(M) wp^1(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⁡(k)M(D_k) for all k∈ℕk∈N An important relation on monoid elements we will use is the ℛR relation (Brzozowski & Fich 1980): Definition 22. For s,t∈Ms,t∈ M, we say s⪯ℛt⇔sM⊆tMs _Rt sM tM. ℛR-classes are the equivalence classes for s∼ℛt⇔[s⪯ℛt∧t⪯ℛs]s _Rt [s _Rt t _Rs ]. Proposition 23. M⁡(k)⪯(U1∘ℤk+3)∘U1M(D_k) (U_1 Z_k+3) U_1, where ℤk+3Z_k+3 is the cyclic group of order k+3k+3. Proof. First consider the submonoid of (U1∘ℤk+3)×U1(U_1 Z_k+3)×U_1 generated by ((g,0),1)((g,0),1), ((g,1),0)((g,1),0), and ((g,k+2),0)((g,k+2),0) where g∈U1ℤk+3g∈U_1^Z_k+3 given by g⁡(x)=0⇔x∈k+1,k+2g(x)=0 x∈\k+1,k+2\. It can be verified that ((g,0),1)↦ϵ((g,0),1) ε, ((g,1),0)↦a((g,1),0) a, and ((g,k+2),0)↦b((g,k+2),0) b extends to a surjective homomorphism h:U1∘ℤk+3→M⁡(k)×U1h U_1 Z_k+3→ M(D_k)×U_1. Finally, using the fact that direct products divide wreath products, we conclude that M⁡(k)⪯(U1∘ℤk+3)∘U1M(D_k) (U_1 Z_k+3) U_1. ∎ Intuitively, computation in ℤk+3Z_k+3 detects if the depth ever exceeds k+1k+1, and this depth-violation is detected by U1U_1. Another U1U_1 detects non-emptiness of the string. Appendix 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≤ij≤ i. This content follows Thérien & Wilke 2001. Definition 24 (Linear RASP programs). Linear RASP programs are those with the syntax ϕ φ ::=σ∣¬ϕ1∣ϕ1∧ϕ2|⁡⟨ϕ1,ϕ2,…,ϕk⟩ ::=σ _1 _1 _2 _1, _2,…, _k where σ∈Σσ∈ and O is some operator of arity k. For each operator there is an associated collection K⊆Σ∗×(2ℕ)kK_O ^*×(2^N)^k of words and sets of positions contained in the operator. Semantics are defined w,i⊧σ w,i σ ⇔ wi=σ w_i=σ w,i⊧¬ϕ w,i φ ⇔ w,i⊧̸ϕ w,i φ w,i⊧ϕ1∧ϕ2 w,i _1 _2 ⇔ w,i⊧ϕ1 and w,i⊧ϕ2 w,i _1 and w,i _2 w,i⊧⁡⟨ϕ1,ϕ2,…,ϕk⟩ w,i _1, _2,…, _k ⇔ (w≤i,j∣w,j⊧ϕ1,…,j∣w,j⊧ϕk)∈K (w_≤ i,\j w,j _1\,…,\j w,j _k\)∈ K_O 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. K K_ since =(w,R1,R2)∣∃k∈R2 st k<|w| and [k,|w|)⊆R1 =$w,R_1,R_2) ∃ k∈ R_2 st k<|w| and [k,|w|) R_1\ In this way w,i⊧ϕ1ϕ2 w,i _1 since _2 ⇔(w≤i,j∣w,j⊧ϕ1,j∣w,j⊧ϕ2)∈K (w_≤ i,\j w,j _1\,\j w,j _2$∈ K_ since ⇔there exists k<i such that w,k⊧ϕ2 and w,j⊧ϕ1 for all k<j<i 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( ,C)= _1≤ m≤ k _m· \# to-0.5pt -2.0pt $ $ _m≥ C K(Λ,C) K_( ,C) =(w,R1,R2,…,Rk)|∑1≤m≤kλm⋅|Rm|≥C = $w,R_1,R_2,…,R_k) | _1≤ m≤ k _m·|R_m|≥ C \ In this way w,i⊧∑1≤m≤kλm⋅#↼ϕm≥C w,i _1≤ m≤ k _m· \# to-0.5pt -2.0pt $ $ _m≥ C ⇔(w≤i,j∣w,j⊧ϕ1,…j∣w,j⊧ϕ2)∈K(Λ,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 _m·|\j w,j _m\|≥ C Definition 26. Let Φ and Ψ be classes of linear RASP programs formulas over alphabet Γ and Σ , respectively. Let G=ψγ∈ΓG=\ _γ\_γ∈ be a family of formulas in Ψ . Let θG _G be a mapping of formulas given by θG(Qγ) _G(Q_γ) ↦ ψγ _γ θG(¬ϕ) _G( φ) ↦ ¬θG(ϕ) _G(φ) θG(ϕ1∧ϕ2) _G( _1 _2) ↦ θG(ϕ1)∧θG(ϕ2) _G( _1) _G( _2) θG(⁡⟨ϕ1,ϕ2,…,ϕk⟩) _G(O _1, _2,…, _k ) ↦ OPEN⁡⟨θG(ϕ1),θG(ϕ2),…,θG(ϕk)⟩) _G( _1), _G( _2),…, _G( _k) ) We write ϕ[γ↦ψγ]φ[γ _γ] 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)(w,p) for w∈Σ∗w∈ ^* and 1≤p≤|w|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⁡(Φ)P( ) is the set of pointed languages L for which there exists ϕ∈Φφ∈ such that (w,p)∈L(w,p)∈ L iff w,p⊧ϕw,p φ. • For M a class of typed monoids, P⁡()P(M) is the set of pointed languages L for which there exists (M,M,ℰM)∈(M, T_M,E_M)∈M, typed homomorphism h:Σ∗→(M,M,ℰM)h ^*→(M, T_M,E_M), a type ∈M M∈ T_M, and a finite set C⊆MC M such that (w,p)∈L(w,p)∈ L iff (h(w1w2⋯wp−1),h(wp))∈×C(h(w_1w_2·s 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, -1⋆-1 C-RASP_1 C-RASP_1 is equivalent to the class of depth 22 programs -2 C-RASP_2. We will see in section E.2 that linear RASP programs can be closely connected to wreath products of monoids. Appendix 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. Proposition 29. Consider the classic wreath product ℤ∘ℤZ Z. Then M⁡(L)⪯ℤ∘ℤM(L) Z for every LL. Proof. Without loss of generality let Σ=0,1 =\0,1\. Consider the submonoid of ℤ∘ℤZ Z generated by the image of Σ∗ ^* under the homomorphism σ↦(fσ,1)σ (f_σ,1) where fσ(x)=σ⋅2|x|f_σ(x)=σ· 2^|x|. In essence, this creates a mapping w↦(fw,|w|)w (f_w,|w|) where fw(0)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,M,ℰM)(M, T_M,E_M) where M is a finitely generated monoid, M T_M is a finite Boolean algebra over M, and ℰME_M is a finite subset of M. Elements of M T_M are the types and elements of ℰME_M are the units. A language L is recognized by (M,M,ℰM)(M, T_M,E_M) if there exists a homomorphism h:Σ∗→Mh ^*→ M such that h⁡(Σ)⊆ℰMh( ) E_M and L=h−1()L=h^-1( M) for some ∈M M∈ T_M. As an example, the language MAJORITY can be recognized by the typed monoid (ℤ,(−∞,0],[1,∞),ℤ,∅,−1,1)(Z,$-∞,0],[1,∞),Z, \,\-1,1$ via the type [1,∞)[1,∞) and the homomorphism a↦1a 1 and b↦−1b -1. We will typically refer to this typed monoid as ℤZ. We define morphisms Definition 31. Let (S,S,ℰS)(S, T_S,E_S) and (T,T,ℰT)(T, T_T,E_T) be typed monoids. A typed monoid homomorphism h:(S,S,ℰS)→(T,T,ℰT)h (S, T_S,E_S)→(T, T_T,E_T) is a triple (hS,hS,hℰS)(h_S,h_ T_S,h_E_S) such that: • hS:S→Th_S S→ T is a monoid homomorphism • hS:S→Th_ T_S T_S→ T_T is a homomorphism of Boolean algebras • ∀∈S,hS()=hS()∩hS(S)∀ S∈ T_S,h_S( S)=h_ T_S( S)∩ h_S(S) • ∀∈ℰS,hS()=hℰS()∀s∈E_S,h_S(s)=h_E_S(s) And due to the compatibility of hS,hS,hℰSh_S,h_ T_S,h_E_S we can omit the subscripts. We say that a typed monoid (S,S,ℰS)(S, T_S,E_S) recognizes the language L⊆Σ∗L ^* if there is a morphism h:Σ∗→Sh ^*→ S with h⁡(Σ)⊆ℰSh( ) E_S and a type ∈S S∈ T_S such that L=h−1()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,T,ℰT)(T, T_T,E_T) be a typed monoid and let C⊆TC T be a nonempty finite set of constants. A function f:T→Sf:T→ S is called type respecting with respect to (T,T,ℰT)(T, T_T,E_T) and C if the preimage f−1(s)f^-1(s) can be described by a finite Boolean combination of conditions of the form tc∈tc∈ T where c is a constant in T (not necessarily in ℰTE_T) and ∈T T∈ T_T. Intuitively, the image of x under a type-respecting function depends only on the type of xcxc 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,M,ℰM)(M, T_M,E_M), (N,N,ℰN)(N, T_N,E_N) be two typed monoids, C⊆NC N be a finite set. The typed wreath product (U,U,ℰU)=(M,M,ℰM)⋅∘C(N,N,ℰN)(U, T_U,E_U)=(M, T_M,E_M) 1.07639pt· _C(N, T_N,E_N) of (M,M,ℰM)(M, T_M,E_M) with (N,N,ℰN)(N, T_N,E_N) is defined such that • ℰUE_U consists of all elements (f,n)(f,n), where n∈ℰNn∈E_N, and f:N→ℰMf:N→E_M is a type respecting function (see definition 32) with respect to (N,N,ℰN)(N, T_N,E_N) and C • U is the submonoid of M∘NM N generated by ℰUE_U • U T_U consists of all types ,=(f,n)∈U∣f(1N)∈,n∈ U_ M, N=\(f,n)∈ U f(1_N)∈ M,n∈ N\, where ∈M M∈ T_M, ∈N N∈ T_N Definition 34 (Typed Monoid Pseudovariety). A typed monoid pseudovariety is a class of typed monoids closed under • Division • 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⋅∘WV 1.07639pt· W where V∈V∈V and W∈W∈W. Define wp1()= wp^1(V)=V, wpk+1()=wpk()⋅∘ wp^k+1(V)= wp^k(V) 1.07639pt· V, and wpc()=⋃k>0wpk() wpc(V)= _k>0 wp^k(V). We also define wpk((,,,,,)) wp^k((M, T_M,E_M)) for typed monoids (M,M,ℰM)(M, T_M,E_M), taking wp1((,,,,,)) wp^1((M, T_M,E_M)) as the pseudovariety generated by (M,M,ℰM)(M, T_M,E_M). 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⪯TM S,N T where M,NM,N are finite and S,TS,T are typed. Then M∘N⪯SN⋅∘TM N S^N 1.07639pt· T (1) where ∘ is the classical wreath product and ⋅⁣∘ 1.07639pt· is the typed wreath product. Proof. Call these typed semigroups (S,S,ℰS)(S, T_S,E_S) and (T,T,ℰT)(T, T_T,E_T). Let hM:(S′,S′,ℰS′)→(M,2M,M)h_M (S , T_S ,E_S )→(M,2^M,M) and hN:(T′,T′,ℰT′)→(N,2N,N)h_N (T , T_T ,E_T )→(N,2^N,N) define the divisions. We will define a function h:(U,U,ℰU)→M∘Nh (U, T_U,E_U)→ M N where (U,U,ℰU)≤(SN,SN,ℰSN)⋅∘(T,T,ℰT)(U, T_U,E_U)≤(S^N, T_S^N,E_S^N) 1.07639pt· (T, T_T,E_T). First, let U be the submonoid of (SN)T×T(S^N)^T× T generated by (fd,t)(f_d,t) where fdf_d for d∈(S′)Nd∈(S )^N is defined such that fd(1T)=df_d(1_T)=d and fd(t)=[n↦d(n+hN(t))]f_d(t)=[n d(n+h_N(t))] for all t∈T′t∈ T , and fd(t)=1(S′)Nf_d(t)=1_(S )^N for t∈T∖T′t∈ T T . Note that all (f,t)(f,t) in U satisfy the following constraints: 1. t∈T′t∈ T 2. Im⁡(Im⁡(f))⊆S′Im(Im(f)) S 3. f⁡(t1+t2)(n)=f⁡(t1)(n+hN(t2))f(t_1+t_2)(n)=f(t_1)(n+h_N(t_2)) 4. f⁡(t1)=f⁡(t2)f(t_1)=f(t_2) whenever hN(t1)=hN(t2)h_N(t_1)=h_N(t_2) 5. Im⁡(f⁡(t))=1S′NIm(f(t))=1_S ^N for t∈T∖T′t∈ T T As a submonoid of the wreath product, U T_U consists of all types ,=(f,t)∈U∣f(1T)∈,t∈ U_ SN, T=\(f,t)∈ U f(1_T)∈ SN,t∈ T\, where ∈S′N SN∈ T_S ^N, ∈T′ T∈ T_T and 1T1_T is the neutral element of T. Let ℰUE_U consist of (f,t)(f,t) where t∈ℰT′t∈E_T . Define a function h:(U,U,ℰU)→M∘Nh (U, T_U,E_U)→ M N such that h⁡((f,t))=(g,hN(t))h((f,t))=(g,h_N(t)) where g⁡(n)=hM(f⁡(1T)(n))g(n)=h_M(f(1_T)(n)). • All functions in U are type-respecting. This is because each of the generators fdf_d is type-respecting – since hNh_N is a homomorphism on types hN:T↦2Nh_N T_T 2^N, the image fd(t)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(g,n)∈ M N: – There is f∈Uf∈ U such that g⁡(⋅)=hM(f⁡(t)(⋅))g(·)=h_M(f(t)(·)), because all d∈(S′)Nd∈(S )^N are represented in U. We just pick d to be compatible with g and fdf_d witnesses the preimage. As for which d to choose, we construct d where for n0∈Nn_0∈ N, we pick an element s0∈hM−1(g⁡(n0))s_0∈ h_M^-1(g(n_0)) (which exists by the surjectivty of hMh_M) and set d such that d⁡(n′)=s0d(n )=s_0 for all n′n where g⁡(n′)=g⁡(n0)g(n )=g(n_0). – There is t∈T′t∈ T such that hN(t′)=nh_N(t )=n by the surjectivity of hNh_N. • h is a homomorphism on elements. From (3)(3) we get that f⁡(t1+t2)(n)=f⁡(t1)(n+hN(t2))f(t_1+t_2)(n)=f(t_1)(n+h_N(t_2)). h⁡((f1,t1)(f2,t2)) h((f_1,t_1)(f_2,t_2)) =h⁡((,,,)) =h((f_1+^t_1f_2,t_1t_2)) =(n↦hM((f1+f2t1)(1T)(n)),hN(t1t2)) =(n h_M((f_1+^t_1f_2)(1_T)(n)),h_N(t_1t_2)) =((n↦hM(f1(1T)(n)))+(n↦hM(f2t1(1T)(n))),hN(t1t2)) =((n h_M(f_1(1_T)(n)))+(n h_M(^t_1f_2(1_T)(n))),h_N(t_1t_2)) =((n↦hM(f1(1T)(n)))+(n↦hM(f2(1T+t1)(n))),hN(t1t2)) =((n h_M(f_1(1_T)(n)))+(n h_M(f_2(1_T+t_1)(n))),h_N(t_1t_2)) =((n↦hM(f1(1T)(n)))+(n↦hM(f2(1T)(n+hN(t1)))),hN(t1)hN(t2)CLOSE =((n h_M(f_1(1_T)(n)))+(n h_M(f_2(1_T)(n+h_N(t_1)))),h_N(t_1)h_N(t_2) by (3) =((n↦hM(f1(1T)(n)))+(n↦hM(f2(1T)(n)))hN(t1),hN(t1)hN(t2) =((n h_M(f_1(1_T)(n)))+^h_N(t_1)(n h_M(f_2(1_T)(n))),h_N(t_1)h_N(t_2) =(n↦hM(f1(1T)(n)),hN(t1))(n↦hM(f2(1T)(n)),hN(t2)) =(n h_M(f_1(1_T)(n)),h_N(t_1))(n h_M(f_2(1_T)(n)),h_N(t_2)) =h⁡((f1,t1))h((f2,t2)) =h((f_1,t_1))h((f_2,t_2)) • h is a homomorphism on types. Let , U_ SN, T be a type of (U,U,ℰU)(U, T_U,E_U). Here, h⁡()∈2MNh( SN)∈ 2^M^N and h⁡()∈2Nh( T)∈ 2^N, because hM,hNh_M,h_N are homomorphisms on types by assumption33 3 Note that Krebs 2008 defined the type of (f,t)(f,t) independent of t (in order to ease the connection to logic), in which case the image under h would not be a type in 2MN×2N2^M^N× 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.. First, h respects complements h⁡(,¯) h( U_ SN, T) =h⁡((f,t)∈U∣f⁡(1T)∉ or t∉) =h($f,t)∈ U f(1_T) ∈ SN or t ∈ T$ =h⁡((f,t))∈M∘N∣h⁡(f⁡(1T))∉h⁡() or h(t)∉h⁡() =\h((f,t))∈ M N h(f(1_T)) ∈ h( SN) or h(t) ∈ h( T)\ =2MN×2N∖h((f,t))∈M∘N∣h(f(1T))∈h(),h(t)∈h() =2^M^N× 2^N \h((f,t))∈ M N h(f(1_T))∈ h( SN),h(t)∈ h( T)\ =h⁡(,)¯ = h( U_ SN, T) And h respects union h⁡(1,1∪1,1) h( U_ SN_1, T_1∪ U_ SN_1, T_1) =h((f,t)∈U∣f(1T)∈1,t∈1∪(f,t)∈U∣f(1T)∈2,t∈2) =h($f,t)∈ U f(1_T)∈ SN_1,t∈ T_1\∪\(f,t)∈ U f(1_T)∈ SN_2,t∈ T_2$ =h((f,t))∈U∣f(1T)∈1,t∈1∪h((f,t))∈U∣f(1T)∈2,t∈2 =\h((f,t))∈ U f(1_T)∈ SN_1,t∈ T_1\∪\h((f,t))∈ U f(1_T)∈ SN_2,t∈ T_2\ =h((f,t)∈U∣f(1T)∈1,t∈1)∪h((f,t)∈U∣f(1T)∈2,t∈2) =h($f,t)∈ U f(1_T)∈ SN_1,t∈ T_1$∪ h($f,t)∈ U f(1_T)∈ SN_2,t∈ T_2$ =h⁡(1,1)∪h⁡(1,1) =h( U_ SN_1, T_1)∪ h( U_ SN_1, T_1) And h preserves the inf and sup h⁡(∅) h( ) =∅ = h⁡(U) h(U) =h(fd,t)∣d∈(S′)N,t∈T′ =\h(f_d,t) d∈(S )^N,t∈ T \ =(hM(d),hN(t))∣d∈(S′)N,t∈T′ =\(h_M(d),h_N(t)) d∈(S )^N,t∈ T \ =MN×N =M^N× 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 _1 and π2 _2 as the projections from the first and second coordinates of MN×NM^N× N Lemma 37. Let h:Σ∗→(T,T,)=(M,M,ℰM)⋅∘C(N,N,ℰN)h ^*→(T, T_T,T)=(M, T_M,E_M) 1.07639pt· _C(N, T_N,E_N) for C⊆NC N. Let π1()∈M _1( T)∈ T_M be such that t∈⇔π1(t)(1N)∈π1()t∈ T _1(t)(1_N)∈ _1( T). Then h⁡(w)∈Th(w)∈ T∈ T_T iff ∑1≤i≤|w|π1(h⁡(wi))(∏1≤j<iπ2(h⁡(wj))) _1≤ i≤|w| _1(h(w_i)) ( _1≤ j<i _2(h(w_j)) ) ∈π1()∈M ∈ _1( T)∈ T_M ∏1≤j<≤iπ2(h⁡(wj)) _1≤ j<≤ i _2(h(w_j)) ∈π2()∈N ∈ _2( T)∈ T_N Proof. We walk through the computation. First, we note that h⁡(w)∈h(w)∈ T iff π1(h⁡(w))∈π1() _1(h(w))∈ _1( T), and this type π1() _1( T) exists by the definition of the typed wreath product. Let h⁡(wi)=(fi,ni)h(w_i)=(f_i,n_i) where fi∈MNf_i∈ M^N and ni∈Nn_i∈ N. Then compute h⁡(w) h(w) =h⁡(w1)h(w2)…h(w|w|) =h(w_1)h(w_2)… h(w_|w|) =(f1,n1)(f2,n2)…(f|w|,n|w|) =(f_1,n_1)(f_2,n_2)…(f_|w|,n_|w|) =(f1+f2n1+…+f|w|(∏1≤j≤|w|−1nj),∏1≤i≤|w|ni) = (f_1+^n_1f_2+…+ ( _1≤ j≤|w|-1n_j )f_|w|, _1≤ i≤|w|n_i ) =(∑1≤i≤|w|fi(∏1≤j<inj),∏1≤i≤|w|ni) = ( _1≤ i≤|w| ( _1≤ j<in_j )f_i, _1≤ i≤|w|n_i ) Recall by the definition of the wreath product that fn(x)=f(xn)^nf(x)=f(xn), so fn(1N)=f⁡(n)^nf(1_N)=f(n). π1(h⁡(w))(1N)∈π1() _1(h(w))(1_N)∈ _1( T) ⇔∑1≤i≤|w|fi(∏1≤j<inj)(1N)∈π1() _1≤ i≤|w| ( _1≤ j<in_j )f_i(1_N)∈ _1( T) ⇔∑1≤i≤|w|fi(∏1≤j<inj)∈π1() _1≤ i≤|w|f_i ( _1≤ j<in_j )∈ _1( T) ⇔∑1≤i≤|w|π1(h⁡(wi))(∏1≤j<iπ2(h⁡(wj)))∈π1() _1≤ i≤|w| _1(h(w_i)) ( _1≤ j<i _2(h(w_j)) )∈ _1( T) The computation of the second coordinate is routine as is computed in (N,N,ℰN)(N, T_N,E_N) π2(h⁡(w))∈π2() _2(h(w))∈ _2( T) ⇔∏1≤j<≤iπ2(h⁡(wj))∈π2(). _1≤ j<≤ i _2(h(w_j))∈ _2( T). ∎ Now connection between the algebraic and logical formulations is often spelled out using statements in the form of a “wreath product principle”. theorem [] Theorem 38 (Typed Wreath Product Principle). Let Φ,Ψ , be classes of linear RASP programs and ,M,N be pseudovarieties of monoids such that L⁡(Φ)=L⁡()L( )=L(M) and P⁡(Ψ)=P⁡()P( )=P(N). Then L(Φ⋆Ψ)=L(⋅∘)L( )=L(M 1.07639pt· N). Proof. • Suppose h:Σ∗→(T,T,)=(M,M,ℰM)⋅∘C(N,N,ℰN)h ^*→(T, T_T,T)=(M, T_M,E_M) 1.07639pt· _C(N, T_N,E_N) for CN⊆NC_N N. For each type ,∈T T_ M, N∈ T_T we will construct a formula θ∈Φ⋆Ψ _ T∈ such that w⊧θ⇔h⁡(w)∈w _ T h(w)∈ T. Observe from Lemma 37 that h⁡(w)∈h(w)∈ T iff ∑1≤i≤|w|π1(h⁡(wi))(∏1≤j<iπ2(h⁡(wj)))∈ _1≤ i≤|w| _1(h(w_i)) ( _1≤ j<i _2(h(w_j)) )∈ M and ∏1≤j<≤iπ2(h⁡(wj))∈. _1≤ j<≤ i _2(h(w_j))∈ N. The first coordinate can be viewed as recognition of a language by M in M via a homomorphism h1:(NC)∗→(M,M,ℰM)h_1 ( T_N^C)^*→(M, T_M,E_M). By assumption obtain a ϕ∈Φφ∈ that recognizes this language. As for the word w′∈(NC)∗w ∈( T_N^C)^* we have that wi′=(c1,c2,…,c|C|)⇔⋀c∈C[(c∏1≤j<iπ2(h(wj)))∈c] w _i=( N_c_1, N_c_2,…, N_c_|C|) _c∈ C [ (c _1≤ j<i _2(h(w_j)) )∈ N_c ] Observe that for each c, we use (N,N,ℰN)(N, T_N,E_N) to recognize an end-pointed language accepting with type c N_c. Then by assumption we obtain ψc∈Ψ _c∈ recognizing each prefix, and then use the substitution ϕ[(c1,c2,…,c|C|)↦⋀c∈Cψc] _ M [( N_c_1, N_c_2,…, N_c_|C|) _c∈ C _c ] The second coordinate can be viewed as recognition of a language by N in N. Since N is a pseudovariety, L⁡()⊆P⁡()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,T,)(T, T_T,T). • The other direction is similar. Suppose we have a formula with substitution ϕ[γ↦ψγ]∈Φ⋆Ψφ[γ _γ]∈ . Because P⁡(Ψ)=P⁡()P( )=P(N), there are typed monoids NγN_γ that can compute the substitution’s output γ at each position. That is, for each γ there is a type γ N_γ and homomorphism h:Σ∗→Nγh ^*→ N_γ w,i⊧ψγ⇔h⁡(w<i)∈γw,i _γ h(w_<i)∈ N_γ Using this, we can compute the substitution into a word over Γ . Then because L⁡(Φ)=L⁡()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 1.07639pt· N. ∎ Appendix 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⋅#↼[ϕt]∼k ::=σ _1 _1 _2 _t _t· \# to-0.5pt -2.0pt $ $ [ _t] k where σ∈Σσ∈ , αi,k∈ℤ _i,k and ∼∈<,≤,=,≥,> ∈\<,≤,=,≥,>\. The semantics of formulas is defined as follows: w,i⊧σ w,i σ ⇔ 6.0pt 6.0pt wi=σw_i=σ w,i⊧¬ϕ w,i φ ⇔ 6.0pt 6.0pt w,i⊧̸ϕ w,i φ w,i⊧ϕ1∧ϕ2 w,i _1 _2 ⇔ 6.0pt 6.0pt w,i⊧ϕ1w,i _1 and w,i⊧ϕ2w,i _2 w,i⊧∑t∈αtt∼k w,i _t _tt k ⇔ 6.0pt 6.0pt ∑t∈αt⋅|j∈[1,i]∣w,j⊧ϕ|∼k. _t _t·|\j∈[1,i] w,j φ\| k. We write w⊧ϕw φ iff w<EOS>,|w|+1⊧ϕw <EOS>,|w|+1 φ where <EOS>∉Σ <EOS> ∈ is a special end-of-sequence symbol. and we say that ϕφ defines the language L⁡(ϕ)=w∣w⊧ϕ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)i=1n =( _i)_i=1^n, where φi _i is any - C-RASP definition that could refer to φj _j with j<ij<i. Definition 40. The syntax of - C-RASP is as follows: ϕ φ :⁣:=σ∣t1<t2∣¬ϕ1∣ϕ1∧ϕ2 ::=σ t_1<t_2 _1 _1 _2 σ∈Σ σ∈ Boolean-valued formulas t t :⁣:=#↼[ϕ1]∣t1+t2∣1 ::= \# to-0.5pt -2.0pt $ $ [ _1] t_1+t_2 1 integer-valued terms The semantics of formulas is defined as follows: w,i⊧σ w,i σ ⇔ 6.0pt 6.0pt wi=σw_i=σ (3a) w,i⊧¬ϕ w,i φ ⇔ 6.0pt 6.0pt w,i⊧̸ϕ w,i φ (3b) w,i⊧ϕ1∧ϕ2 w,i _1 _2 ⇔ 6.0pt 6.0pt w,i⊧ϕ1w,i _1 and w,i⊧ϕ2w,i _2 (3c) w,i⊧t1<t2 w,i t_1<t_2 ⇔ 6.0pt 6.0pt t1w,i<t2w,i. t_1^w,i<t_2^w,i. (3d) The semantics of terms is defined as follows: #↼[ϕ]w,i \# to-0.5pt -2.0pt $ $ [φ]^w,i =|j∈[1,i]∣w,j⊧ϕ| =|\j∈[1,i] w,j φ\| (4a) (t1+t2)w,i (t_1+t_2)^w,i =t1w,i+t2w,i =t_1^w,i+t_2^w,i (4b) 1w,i 1^w,i =1. =1. (4c) We write w⊧ϕw φ if w,|w|⊧ϕw,|w| φ, and we say that ϕφ defines the language L⁡(ϕ)=w∣w⊧ϕL(φ)=\w w φ\. The table below shows how this program works for the string (())()(())(), which belongs to 2D_2. predicate definition description aa aa bb bb aa bb aa is left paren ⊤ ⊤ ⊥ ⊥ ⊤ ⊥ bb is right paren ⊥ ⊥ ⊤ ⊤ ⊥ ⊤ CaC_a := #↼[a] \# to-0.5pt -2.0pt $ $ [a] num of left parens 1 2 2 2 3 3 CbC_b := #↼[b] \# to-0.5pt -2.0pt $ $ [b] num of left parens 0 0 1 2 2 3 ϕlow _low := Ca−Cb≥0C_a-C_b≥ 0 depth above 00 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ϕup _up := Ca−Cb≤2C_a-C_b≤ 2 depth below 22 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ϕbounded _bounded := ϕlow∧ϕup _low _up depth bounded ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ϕmatched _matched := #↼[¬ϕbounded]=0 \# to-0.5pt -2.0pt $ $ [ _bounded]=0 depth bounded everywhere ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ϕbalanced _balanced := Ca=CbC_a=C_b balanced at end ⊥ ⊥ ⊥ ⊤ ⊥ ⊤ ϕ2 _D_2 := ϕmatched∧ϕbalanced _matched _balanced acceptance ⊥ ⊥ ⊥ ⊤ ⊥ ⊤ The table below shows how this program works for the string OPEN())()(CLOSE())()(, which does not belong to 2D_2. predicate definition description aa bb bb aa bb aa aa is left paren ⊤ ⊥ ⊥ ⊤ ⊤ ⊥ bb is right paren ⊥ ⊤ ⊤ ⊥ ⊤ ⊥ CaC_a := #↼[a] \# to-0.5pt -2.0pt $ $ [a] num of left parens 1 1 1 2 2 3 CbC_b := #↼[b] \# to-0.5pt -2.0pt $ $ [b] num of left parens 0 1 2 2 3 3 ϕlow _low := Ca−Cb≥0C_a-C_b≥ 0 depth above 00 ⊤ ⊤ ⊥ ⊤ ⊥ ⊤ ϕup _up := Ca−Cb≤2C_a-C_b≤ 2 depth below 22 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ϕbounded _bounded := ϕlow∧ϕup _low _up depth bounded ⊤ ⊤ ⊥ ⊤ ⊥ ⊤ ϕmatched _matched := #↼[¬ϕbounded]=0 \# to-0.5pt -2.0pt $ $ [ _bounded]=0 depth bounded everywhere ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ϕbalanced _balanced := Ca=CbC_a=C_b balanced at end ⊥ ⊥ ⊥ ⊤ ⊥ ⊤ ϕ2 _D_2 := ϕmatched∧ϕbalanced _matched _balanced acceptance ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ F.2 - 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 or Huang et al. 2025, but ignoring positional predicates and allowing arbitrary symbols in the image of the homomorphism. • Closed under factors: Let L be in - C-RASP, and a∈Σa∈ . To obtain a−1La^-1L, we can detect the beginning in - C-RASP and simulate the computations at a prefix a. To obtain La−1La^-1, at <EOS> we simulate the computations at a<EOS>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\a,b\^*b from a,b∗a\a,b\^*a, but taking the inverse of a homomorphism that deletes e and keeps a,ba,b unchanges leads to the two sets a,b∗be∗\a,b\^*be^* from a,b,e∗ae∗\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 and the related logic ^2[<] MAJ_2[<], though none have arrived at an exact characterization. Here, 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 quantification to the left, which is implementable in - C-RASP (OPEN#↼[ϕ]≥1) \# to-0.5pt -2.0pt $ $ [φ]≥ 1). 2. -∩⊂ C-RASP∩REG⊂A, since any periodic regular language like (aa)∗(a)^* is not definable in - C-RASP (Huang et al. 2025, Lemma 38). 3. Σ∗b ^*b, is not in - C-RASP (Huang et al. 2025, Lemma 38). 4. Σ∗bbΣ∗ ^*b ^*is not in - C-RASP, because it is not in the larger class ^2[<] MAJ_2[<] by Lemma 6.11 in Krebs 2008 5. For any k, (a+b+)k(a^+b^+)^k in - C-RASP by Yang et al. 2025 6. (ab)+(ab)^+ in - C-RASP The next section develops our exact characterization. F.4 Algebraic Characterization of - C-RASP See 11 Proof. We will show that L(-)=L(wpc(ℤ))L( C-RASP)=L( wpc(Z)), which will be equivalent to the theorem statement. First, we note that wpc(ℤ) wpc(Z) and wp2(ℤ) wp^2(Z) are pseudovarieties of typed monoids by definition. Then, we establish that P⁡(-1)=P⁡(wp2(ℤ))P( C-RASP_1)=P( wp^2(Z)), noting that - C-RASP is an instance of a linear RASP program. First, by Yang et al. 2025 every - C-RASP program can be written such that it only counts over positions j<ij<i, with Boolean operations testing the symbol at i. The strict counting can be translated into a typed monoid over wp2(ℤ) wp^2(Z) (since the equations in - C-RASP may not just be #↼ϕ≥0 \# to-0.5pt -2.0pt $ $ φ≥ 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(ℤ) wp^2(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(-1)=L(ℤ⋅∘ℤ)L( C-RASP_1)=L(Z 1.07639pt· Z). From this base case we can build up to L⁡(-k)=L⁡(wp2k(ℤ))L( C-RASP_k)=L( wp^2k(Z)) by induction, and thus L⁡(-)=⋃k≥0L⁡(-k)=⋃k≥0L⁡(wpck(ℤ))=wpc(ℤ)L( C-RASP)= _k≥ 0L( C-RASP_k)= _k≥ 0L( wpc^k(Z))= wpc(Z). ∎ Appendix 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; 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)Obj(X) and for each c,c′∈Obj(X)c,c ∈Obj(X) a homset of arrows X⁡(c,c′)X(c,c ), often written as x:c→c′x c→ c for x∈X⁡(c,c′)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′s c→ c and t:c′→c′t c → c , compose into an arrow st:c→c′st c→ c . Furthermore, for s:c1→c2s c_1→ c_2, t:c2→c3t c_2→ c_3, and v:c3→c4v c_3→ c_4, we have that (st)v=s⁡(tv)(st)v=s(tv). • For objects c we have an identity arrow 1c:c→c1_c c→ c, where s1c=s1_c=s and 1ct=t1_ct=t for s:c′→cs c → c and t:c→c′t c→ c . Remark 45. When the ambient category C is unambiguous, we also write Hom(x→x′)Hom(x→ x ) for C⁡(x,x′)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,YX,Y be categories. A category relation f:X→Yf X→ Y has • An object relation f:Obj(X)→Obj(Y)f Obj(X)→Obj(Y), thought of as a subset of X×YX× Y. • For any corresponding edge sets X⁡(c,c′)X(c,c ) and Y⁡(d,d′)Y(d,d ) where d∈cf,d′∈c′fd∈ cf,d ∈ c f, an edge set relation f:X⁡(c,c′)→Y⁡(d,d′)f X(c,c )→ Y(d,d ). and satisfies the property that #f\#f, defined as follows, is a subcategory #f\#f of X×YX× Y: • Obj(#f)=(c,d):d∈cfObj(\#f)=\(c,d) d∈ cf\ • #f[(c,d),(c′,d′)]=(x,y)∣x∈X(c,c′),y∈Y(d,d′),y∈xf\#f[(c,d),(c ,d )]=\(x,y) x∈ X(c,c ),y∈ Y(d,d ),y∈ xf\ The most important kind of relation for us will be a relational morphism, denoted ϕ:X⊲Yφ 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⊲YX Y after we close under composition in X. Definition 47 (Relational Morphism). A relational morphism f:C⊲C′f:C C between categories C and C′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′f:C C and α∈C⁡(x,x′)α∈ C(x,x ) is an arrow in C, then we write f⁡(α)f(α) for the set β∈C′(y,y′):(α,β)∈#f[(x,x′),(y,y′)]\β∈ C (y,y ):(α,β)∈\#f[(x,x ),(y,y )]\, where (x,y),(x′,y′)∈Obj(#f)(x,y),(x ,y )∈ Obj(\#f). The condition that #f\#f be a category implies in particular f⁡(α)f(β)⊆f⁡(αβ)f(α)f(β) f(αβ) (5) whenever α∈C⁡(x,x′),β∈C⁡(x′,x′)α∈ 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′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φ M N be a relational morphism between monoids. The derived category DϕD_φ of the relational morphism is defined with Obj(Dϕ)=ϕ(M)Obj(D_φ)=φ(M) and Hom(n1,n2)=n1→(m,n):ϕ−1(n1)→ϕ−1(n2)∣(m,n)∈#ϕ,n1n=n2Hom(n_1,n_2)=\n_1 _(m,n)\, φ^-1(n_1)→φ^-1(n_2) (m,n)∈\#φ,n_1n=n_2\, where n1→(m,n)n_1 _(m,n)\, is a function ϕ−1(n1)→ϕ−1(n1n)φ^-1(n_1)→φ^-1(n_1n) mapping any x∈ϕ−1(n1)x∈φ^-1(n_1) to xm∈ϕ−1(n1n)xm∈φ^-1(n_1n). Composition of arrows is given by (n0→(m1,n1))(n1→(m2,n2))=n0→(m1m2,n1n2) (n_0 _(m_1,n_1)\, ) (n_1 _(m_2,n_2)\, )=n_0 _(m_1m_2,n_1n_2)\,. Remark 50. We note that, as the arrows denote functions on subsets of M, it is possible for n1→(m,n)n_1 _(m,n)\, and n1→(m′,n)n_1 _(m ,n)\, to be identical even if m≠m′m≠ m , provided m and m′m act identically on ϕ−1(n1)φ^-1(n_1). Where helpful for notational clarity, we explicitly include the end object, writing n1→(m,n)n_1 _(m,n)\, as n1→(m,n)n2n_1 _(m,n)\,n_2 where n2=n1n_2=n_1n. For readers familiar with the corresponding construction for groups, we provide some intuition. In some sense, ker⁡ϕ φ for ϕ:G→Hφ G→ H records what information is lost when compressing G into H. By recording what elements collapse into 1H1_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⁡ϕ)G/( φ) 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⁡ϕ)∘HG ( φ) 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∈Nn∈ 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∘NM V N, formalized by the Derived Category Theorem (Tilson 1987): Theorem 51 (Derived Category Theorem). 1. Let ϕ:M⊲Nφ M N be a relational morphism of monoids, and let V be a monoid satisfying Dϕ⪯VD_φ V. Then there is a division of monoids θ:M⪯V∘Nθ M V N. 2. Let θ:M⪯V∘Nθ M V N be a division of monoids, and let ϕ=θπ:M⊲Nφ=θπ M N be the associated relational morphism. Then Dϕ⪯VND_φ V^N. Appendix H Algebraic Decision Procedure H.1 Relevant Lemmas Lemma 52. If M⪯SM S and N⪯TN T then M∘N⪯S∘TM N S T. Proof. This is a standard fact which we sketch out here. For some S′≤S ≤ S and T′≤T ≤ T there exists surjections hM:S′→Mh_M S → M and hN:T′→Nh_N T → N. Let G′G be the subset of ST×TS^T× T generated by all (f,t′)(f,t ) where t′∈T′t ∈ T , Im⁡(f)⊆S′Im(f) S , and f⁡(t)=1Sf(t)=1_S for t∉T′t ∈ T , with the wreath product action inherited from S∘TS T. Define h:G→M∘Nh G→ M N by h⁡(f,t′)=(f′,hN(t′))h(f,t )=(f ,h_N(t )) where f′(n)=hM(f′(t))f (n)=h_M(f (t)) for some t∈hN−1(n)t∈ h_N^-1(n) (the choice does not matter). It is clear that h is a surjective homomorphism via inheritance from hMh_M and hNh_N. ∎ H.2 Bounded-Depth Dyck Monoids To make constructions computable despite the infinity of ℤZ, we use bounded-depth Dyck monoids kD_k as partial stand-ins for ℤZ. The non-⊥ elements of the monoid kD_k can be canonically represented as tuples (h,h↓,h↑)(h,h_ ,h_ ) where, for a word w∈a,b∗w∈\a,b\^*, the syntactic morphism η maps it to h= h= ∑i=1|w|ϕ⁡(wi) _i=1^|w|φ(w_i) h↑= h_ = max⁡∑i=1j⁡ϕ⁡(wi) _j _i=1^jφ(w_i) h↓= h_ = min⁡∑i=1j⁡ϕ⁡(wi) _j _i=1^jφ(w_i) under ϕ⁡(a)=1φ(a)=1, ϕ⁡(b)=−1φ(b)=-1, provided these numbers are all in [−k,…,k][-k,…,k]; otherwise the word is mapped to ⊥ . The monoid kD_k has a natural action on the set Sk:=[−k,…,k]∪⊥S_k:=[-k,…,k]∪\ \ (6) given by j⋅(h,h↑,h↓)=⊥if j=⊥h+jif j+h↓≥−k∧j+h↑≤k⊥elsej·(h,h_ ,h_ )= cases &if j= \\ h+j&if j+h_ ≥-k j+h_ ≤ k\\ &else cases (7) Formally, the pair (k,Sk)(D_k,S_k) is a transformation monoid.44 4 We note that SkS_k itself is not a monoid, because truncated addition is not associative. The monoid kD_k describes the monoid of bounded incrementing/decrementing operations on SkS_k. Together, they provide an algebraic model of bounded counting sufficient for our purposes. We could develop the decidability proof in terms of wreath products of (k,Sk)(D_k,S_k), which are somewhat different from wreath products of kD_k; this would have some advantages because the set SkS_k 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 kD_k, namely n∼m⇔0n=0mn m 0n=0m. It is a right-congruence in the sense that 0n=0m⇒0nr=0mr0n=0m 0nr=0mr for any n,m,r∈kn,m,r∈D_k. When considering derived categories for relational morphisms to kD_k, 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,TM,S,T be finite monoids. Given relational morphisms ϕ:M⊲Tφ:M T, ϕ′:Dϕ⊲Sφ :D_φ S, we define Ext⁡(ϕ′,ϕ):M⊲(S∘T)Ext(φ ,φ):M (S T) as Ext(ϕ′,ϕ)(m)=(f,t)∈ST×T:t∈ϕ(m);∀x∈Obj(Dϕ):f(x)∈ϕ′(x→(m,t)xt)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⁡(ϕ′,ϕ)Ext(φ ,φ). Remark 55. We write Ext(ϕ1,ϕ2,…,ϕn)Ext( _1, _2,…, _n) for Ext⁡(ϕn,Ext⁡(ϕn−1,…))Ext( _n,Ext( _n-1,…)). The following is shown in Tilson 1987: Proposition 56. Ext⁡(ϕ′,ϕ)Ext(φ ,φ) is a well-defined relational morphism M⊲S∘TM S T. In the sequel we will write ℤZ or (ℤ,ℤ+)(Z,Z_+) for the typed monoid (ℤ,ℤ+,±1)(Z,Z_+,± 1) and kD_k for the syntactic monoid of the language kD_k. 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 22. We now state our decision procedure: Definition 58 (Decision Procedure). Our input is a finite monoid M. Let R1,R2,…,RℓR_1,R_2,…,R_ be the ℛR-classes of M, such that Ri≺ℛRj⇒i>jR_i _RR_j i>j. For i=1,2,…,ℓi=1,2,…, , we maintain relational morphisms ϕi _i from M to an iterated wreath product of kD_k and U1U_1. We maintain the invariant that m=ϕi−1(ϕi(m)),∀m∈R1,…,Ri(Invariant(i))\m\= _i^-1( _i(m)),∀ m∈ R_1,…,R_i\;\;\;\;\;\;\;\;(Invariant(i)) Let N0N_0 be the trivial monoid and ϕ0:M⊲N0 _0 M N_0 be the trivial relational morphism. For i=1,…,ℓi=1,…, , do 1. Note: Here, we record, for any path through the category going into RiR_i, 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 RiR_i we first entered it. Later, Ei,jE_i,j will have multiple strongly connected components (or bonded components, the term used by Tilson) corresponding to RiR_i, indexed by the different possible entry points (Lemma 63). Let δ:Obj(Dϕi−1)→0,1δ:Obj(D_ _i-1)→\0,1\ be given as δ(o)=1∃m∈ϕi−1−1(o):m⪯RRi0elseδ(o)= cases1&∃ m∈ _i-1^-1(o):m _RR_i\\ 0&else cases Let ∂i=(o→s,tot):δ(o)=0,δ(ot)=1 _i=\(o _s,tot):δ(o)=0,δ(ot)=1\. Define ϕ′:Dϕi−1⊲Bφ :D_ _i-1 B, where B is the left-zero semigroup with identity ∗* adjoined, with left-zeros indexed by the elements of ∂i _i55 5 B:=∂i∪∗B:= _i∪\*\, ∗b=b*b=b, rb=rrb=r whenever r∈∂ir∈ _i, b∈Bb∈ B., as the relational morphism generated by (i.e., the intersection of all relational morphisms satisfying) ϕ′(o→(s,t)ot)⊇∂iδ⁡(o)=δ⁡(ot)=1∗δ⁡(o)=δ⁡(ot)=0(o→(s,t)ot)δ⁡(o)=0,δ⁡(ot)=1φ (o _(s,t)ot) cases _i&δ(o)=δ(ot)=1\\ \*\&δ(o)=δ(ot)=0\\ \(o _(s,t)ot)\&δ(o)=0,δ(ot)=1\\ cases (8) where we note δ⁡(o)=1,δ⁡(ot)=0δ(o)=1,δ(ot)=0 cannot occur. By definition, ∗∉ϕ′(1→(s,o)o)* ∈φ (1 _(s,o)o) iff s⪯RRis _RR_i. We note that B is ℛR-trivial; hence it divides an iterated wreath product of U1U_1. This is a relational morphism. Set ϕi,1:=Ext⁡(ϕ′,ϕi−1):M⊲Ni,1 _i,1:=Ext(φ , _i-1):M N_i,1 where Ni,1=B∘Ni−1N_i,1=B N_i-1. 2. Build a sequence of relational morphisms ϕi,2,ϕi,3,… _i,2, _i,3,… as follows, over j=1,2,3,…j=1,2,3,…: (a) Intuition: We simplify Dϕi,jD_ _i,j in two ways. First, all information from earlier annotation is removed once we have entered RiR_i. This simplifies our proof by avoiding any complications arising from interactions between old and new annotation. Second, elements of kD_k provide extra information beyond bounded counting; here, we project its elements to the underlying set of truncated integers. Write an element of Ni,jN_i,j as a=(fi,j,…,fi,1,f).a=(f_i,j,…,f_i,1,f). where fi,j:Ni,j−1→kf_i,j:N_i,j-1→D_k. Define its “retained signature” by sigi,j⁡(a):=(0⋅fi,j(1Ni,j−1)⏟∈k⏟∈Sk,…,0⋅fi,2(1Ni,1),fi,1(1Ni−1)⏟∈B),sig_i,j(a):= ( 0· f_i,j(1_N_i,j-1)_∈D_k_∈ S_k,…,0· f_i,2(1_N_i,1), f_i,1(1_N_i-1)_∈ B ), where we view kD_k as acting on Sk:=[−k,…,k]∪⊥S_k:=[-k,…,k]∪\ \ from the right (7). We define a right congruence66 6 In the sense that aρb⇒arρbraρ b arρ br for any a,b,r∈Ni,ja,b,r∈ N_i,j. ρi,j _i,j on Ni,jN_i,j by setting aρi,jba\, _i,j\,b whenever (i) a=ba=b, or (i) fi,1a(1Ni−1)≠∗,fi,1b(1Ni−1)≠∗,f^a_i,1(1_N_i-1)≠*,f^b_i,1(1_N_i-1)≠*, and sigi,j⁡(a)=sigi,j⁡(b).sig_i,j(a)=sig_i,j(b). We define Ei,jE_i,j as the category obtained from Dϕi,jD_ _i,j and the right-congruence ρi,j _i,j (based on the discussion in Section H.2). (b) Consider the set Ωi,j _i,j of algebraic relational morphisms ϕ′:Ei,j⊲ℤφ :E_i,j Z such that for each s∈Ris∈ R_i and any t∈ϕi,j(s)t∈ _i,j(s), ϕ′(1→s,t)φ (1 _s,tt) is a finite set. 77 7 Without loss of generality, we restrict to relational morphisms ϕ′φ where, for each object o with non-∗* entry annotation, every vlaue of ϕ′φ on an arrow 1→o1→ o is generated by factorization through a prefix ending inside RiR_i: ϕ′(α)=⋃α=βγ,β∈π−1(Ri)ϕ′(β)ϕ′(γ)φ (α)= _α=βγ,β∈π^-1(R_i)φ (β)φ (γ). 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. Note: In the automaton-based 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φ ∈ _i,j such that at least one of the following is satisfied: i. Condition A: ϕ′:Ei,j⊲ℤφ :E_i,j Z assigns disjoint images to two arrows in Hom(o→o′)Hom(o→ o ) where o,o′o,o both are in RiR_i (in the sense of Definition 59). i. Condition B: There exist objects x,y∈Obj(Ei,j)x,y∈ Obj(E_i,j), arrows a∈Hom(x→y);b∈Hom(y→x);ℓ∈Hom(x→x)a∈ Hom(x→ y);b∈ Hom(y→ x); ∈ Hom(x→ x) such that x,yx,y are inside RiR_i88 8 In the sense of Definition 59: Hom(1,x)∩π−1(Ri)≠∅;Hom(1,y)∩π−1(Ri)≠∅,Hom(1,x)∩π^-1(R_i)≠ ;Hom(1,y)∩π^-1(R_i)≠ ,, where π:Ei,j⊲Mπ:E_i,j M is the canonical division., but no arrow in Hom(x,y)Hom(x,y) ends in RiR_i99 9 In the sense of Definition 59: ∀β∈Hom(x→y);Hom(1→x)β∩π−1(Ri)=∅,∀β∈ Hom(x→ y);Hom(1→ x)\,β∩π^-1(R_i)= ,, where π:Ei,j⊲Mπ:E_i,j M is the canonical division., whereas ℓ ends in RiR_i1010 10 In the sense of Definition 59: Hom(1,x)ℓ∩π−1(Ri)≠∅,Hom(1,x)\, ∩π^-1(R_i)≠ , and ϕ′(ab)∩ϕ′(ℓ)=∅.φ (ab)∩φ ( )= . then we take such a ϕ′φ , turn it to a relational morphism ϕ′~:Ei,j⊲k φ :E_i,j D_k1111 11 For sufficiently large k, greater than the absolute value of, for each s∈Ris∈ R_i and any t∈ϕi,j(s)t∈ _i,j(s), the entries of the finite set ϕ′(1→s,t)φ (1 _s,tt). To convert a relational morphism to ℤZ into one on kD_k, 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., pull it back to ϕ^′:Dϕi,j⊲k φ :D_ _i,j D_k and build ϕi,j+1:=Ext⁡(ϕ^′,ϕi,j):M⊲Ni,j+1 _i,j+1:=Ext( φ , _i,j) M N_i,j+1, where Ni,j+1:=k∘Ni,jN_i,j+1:=D_k N_i,j. (d) Otherwise, we terminate this inner loop. (e) One possibility is that ϕi,j−1(ϕi,j(m))=m _i,j^-1( _i,j(m))=\m\ for each m∈Rim∈ R_i. By induction, we have satisfied Invariant⁡(i)Invariant(i). Then, set ϕi:=ϕi,j:M⊲Ni _i:= _i,j M N_i 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ℓN_ if we iterated through all i=1,…,ℓ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 (i) wouldn’t know which types to use. We “guide” the process by (i) proceeding along ℛR classes, (i) considering morphisms to well-selected finite monoids, (i) passing to Ei,jE_i,j instead of the more complicated Dϕi,jD_ _i,j, and (iv) focusing on the sets Ωi,j _i,j. Throughout, we write 1∈Obj(Ei,j)1∈ Obj(E_i,j) for the object arising from the identity element of Ni,jN_i,j. Definition 59. For any of the categories Ei,jE_i,j constructed in the decision procedure, we define the following notions. Let π:Ei,j≺Mπ:E_i,j M be the canonical division. 1. Let SiS_i be the set of arrows o→s,toto _s,tot such that there are arrows 1→s′,o1 _s ,oo and ot→s′,t′ott′ot _s ,t ott such that ss′s′∈Riss s ∈ R_i. 2. We say an arrow α∈Hom(o→o′)α∈ Hom(o→ o ) “ends” in RiR_i if there is an arrow β∈Hom(1→o)β∈ Hom(1→ o) such that βαβα is defined and βα∈π−1(Ri)βα∈π^-1(R_i). 3. We say an arrow α∈Hom(o→o′)α∈ Hom(o→ o ) “starts” in RiR_i if there is an arrow β∈Hom(1→o)β∈ Hom(1→ o) such that βαβα is defined and β∈π−1(Ri)β∈π^-1(R_i). 4. We say an object o is “inside RiR_i” if Hom(1→o)∩π−1(Ri)≠∅Hom(1→ o)∩π^-1(R_i)≠ . 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) 1.07639pt· Z) 1.07639pt· Z). Proof. We refer to a wreath product of the form (…⋅∘⋅)⋅∘⋅)⋅∘⋅)⋅∘⋅(… 1.07639pt· ·) 1.07639pt· ·) 1.07639pt· ·) 1.07639pt· · as left-associative. First, if the algorithm succeeds we obtain a relational morphism ϕk:M⊲N _k:M N where N divides a left-associative wreath product of U1U_1 and kD_k. By the invariant maintained in the Decision Procedure, ϕk _k is injective, making it a division. We now need to explain why M also divides a product of the form (((…ℤ)⋅∘ℤ)⋅∘ℤ)(((…Z) 1.07639pt· Z) 1.07639pt· Z). First, by we can obtain a representation in terms of k⪯((U1)2k⋅∘ℤ)D_k ((U_1)^2k 1.07639pt· Z) and U1U_1, 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 U1U_1 or just ℤZ. Because direct products divide wreath products, we know that M⪯(S⋅∘(N×U1))⋅∘TM (S 1.07639pt· (N×U_1)) 1.07639pt· T implies M⪯((S⋅∘N)⋅∘U1)⋅∘TM ((S 1.07639pt· N) 1.07639pt· U_1) 1.07639pt· T. Iteratively applying this identity, we obtain a division into a left-associative wreath product of U1U_1 and ℤZ (with much greater depth). Finally because U1⪯ℤU_1 , we can conclude that M divides a left-associative wreath product of ℤZ. ∎ Lemma 61. For typed monoids T,ST,S, we have that T⋅∘(U1⋅∘S)⪯(T⋅∘U1|S|)⋅∘ST 1.07639pt· (U_1 1.07639pt· S) (T 1.07639pt· U_1^| T_S|) 1.07639pt· 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 (f1,(g1,h1))(f2,(g2,h2))⋯(fn,(gn,hn))(f_1,(g_1,h_1))(f_2,(g_2,h_2))·s(f_n,(g_n,h_n)) be a multiplication in T⋅∘(U1⋅∘S)T 1.07639pt· (U_1 1.07639pt· S) where hi∈Sh_i∈ S, gi∈U1Sg_i∈U_1^S, and fi∈TU1S×Sf_i∈ T^U_1^S× 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 1, 2 2, and 3 3 (∏i=1n−1fi((∏j=1i−1gj(∏k=1j−1hk),∏j=1i−1hj))⏟1,(∏i=1n−1gi(∏j=1i−1hj)⏟2,∏i=1n−1hi⏟3)) ( _i=1^n-1f_i ( ( _j=1^i-1g_j ( _k=1^j-1h_k ), _j=1^i-1h_j ) )_ 1, ( _i=1^n-1g_i ( _j=1^i-1h_j )_ 2, _i=1^n-1h_i_ 3 ) ) We will simulate this computation in (T⋅∘U1|S|)⋅∘S(T 1.07639pt· U_1^| T_S|) 1.07639pt· S. That is, the desired computation is given by the following injective relational morphism given below. Intuitively, U1|S|U_1^| T_S| 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 1.07639pt· (U_1 1.07639pt· S). ϕ:T⋅∘(U1⋅∘S) φ T 1.07639pt· (U_1 1.07639pt· S) →(T⋅∘U1|S|)⋅∘S →(T 1.07639pt· U_1^| T_S|) 1.07639pt· S αf,g _f,g ∈(TU1|S|×U1|S|)S ∈(T^U_1^| T_S|×U_1^| T_S|)^S γf,ζ _f,ζ ∈TU1|S| ∈ T^U_1^| T_S| ϕ⁡((,,,)) φ((f,(g,h))) =(αf,g,h) =( _f,g,h) αf,g(ζ) _f,g (ζ ) =(γf,ζ,(λ1,λ2,…,λ|S|)) =( _f,ζ,( _ S_1, _ S_2,…, _ S_| T_S|)) λ=1ζ∈0ζ∉ _ S= cases1&ζ∈ S\\ 0&ζ ∈ S cases γf,ζ((,,,,,,,)) _f,ζ(( _ S_1, _ S_2,…, _ S_| T_S|)) =f⁡(β,ζ) =f (β,ζ ) Im(β)⊆⋂∈S;λ=1 (β) _ S∈ T_S; _ S=1 S Note that γf,ζ _f,ζ is well-defined because f⁡((,,,))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∈U1Sg∈U_1^S is represented by some OPEN(λ1,λ2,…,λ|S|))∈U1|S|( _ S_1, _ S_2,…, _ S_| T_S|))∈U_1^| T_S|, and every type-respecting function f is represented as some γf,ζ _f,ζ. Thus the sequence (f1,(g1,h1))(f2,(g2,h2))⋯(fn,(gn,hn))(f_1,(g_1,h_1))(f_2,(g_2,h_2))·s(f_n,(g_n,h_n)) maps homomorphically to the sequence (αf1,g1,h1)(αf2,g2,h2)⋯(αfn,gn,hn)( _f_1,g_1,h_1)( _f_2,g_2,h_2)·s( _f_n,g_n,h_n) which is evaluated as (∏i=1n−1αfi,gi(∏j=1i−1hj),∏i=1n−1hi⏟3) ( _i=1^n-1 _f_i,g_i ( _j=1^i-1h_j ), _i=1^n-1h_i_ 3 ) Observe that the type 3 3 is already computed in the second coordinate. We will see that 1 1 and 2 2 are also computed in the first coordinate: ∏i=1n−1αfi,gi(∏j=1i−1hj) _i=1^n-1 _f_i,g_i ( _j=1^i-1h_j ) =αf1,g1(0)αf2,g2(h1)⋯αfn,gn(∏j=1n−1hj) = _f_1,g_1 (0 ) _f_2,g_2 (h_1 )·s _f_n,g_n ( _j=1^n-1h_j ) =(γf1,0,Λ1)(γf2,h1,Λ2)⋯(γfi,∏i=1n−1hj,Λn) =( _f_1,0, _1)( _f_2,h_1, _2)·s( _f_i, _i=1^n-1h_j, _n) =((∏i=1n−1fi(1,∏j=1i−1hj))⏟1,∏i=1n−1gi(∏j=1i−1hj)⏟2) = ( ( _i=1^n-1f_i (1, _j=1^i-1h_j ) )_ 1, _i=1^n-1g_i ( _j=1^i-1h_j )_ 2 ) ∎ The following properties of ω∈Ωi,jω∈ _i,j are key: Lemma 62 (Balance on Loops). Let ω∈Ωi,jω∈ _i,j. 1. Let u∈Riu∈ R_i, ρ∈Mρ∈ M such that uρ=uρ=u. Consider arrows 1→(u,o)o→(ρ,t)ot1 _(u,o)o _(ρ,t)ot in Ei,jE_i,j. Then in fact ot=oot=o, and ω(o→(ρ,t)o)=0ℤω(o _(ρ,t)o)=\0_Z\ where 0ℤ0_Z is the neutral element of ℤZ. 2. Let u be such that Riu=RiR_iu=R_i. For v∈Riv∈ R_i, consider arrows 1→(v,o)o→(u,t)ot1 _(v,o)o _(u,t)ot in Ei,jE_i,j. Then ω(o→(u,t)ot)ω(o _(u,t)ot) is a singleton. Proof. For the first point, we have two claims to prove: that (a) ot=oot=o, and that (b) the image is 0ℤ\0_Z\. We first note that (a) holds at j=1j=1: u∈Riu∈ R_i, uρ=uρ=u and 1→(u,o)o→(ρ,t)ot1 _(u,o)o _(ρ,t)ot in Ei,jE_i,j, then in fact ot=oot=o by construction of Ei,1E_i,1. We also note that, if (b) has been shown for 1,…,j1,…,j, then (a) follows for 1,…,j+11,…,j+1. We thus need to perform the inductive step for (b). We consider the arrow o→(ρ,t)o _(ρ,t)o. Assume z∈ω(o→(ρ,t)o)z∈ω(o _(ρ,t)o) and z≠0z≠ 0. Now, for all k≥0k≥ 0, uρk=uρ^k=u; hence, ω(1→(u,o)o)ω(1 _(u,o)o) is infinite. This is a contradiction to ω∈Ωi,jω∈ _i,j. For the second point, from Riu=RiR_iu=R_i, obtain ρ such that vuρ=vvuρ=v. We consider arrows: 1→(v,o)o→(u,t)ot→(ρ,t′)ott′1 _(v,o)o _(u,t)ot _(ρ,t )ott By (1), in fact, ott′=oott =o and ω(o→(u,t)ot→(ρ,t′)ott′)=0ℤω(o _(u,t)ot _(ρ,t )ott )=\0_Z\. Because ω is a relational morphism and ℤZ is a group, this entails ω(o→(u,t)ot)ω(o _(u,t)ot) must be a singleton. ∎ We deduce the following structural properties of Ei,jE_i,j, which are used both for termination and for completeness of the procedure. As foreshadowed when we defined the “entry-point coordinate” ϕi,1 _i,1, we find that RiR_i is reflected in Ei,jE_i,j in multiple strongly connected components (or “bonded components”), each indexed by a different entry arrow of the “boundary set” ∂i _i we defined there: Lemma 63 (Structure of Ei,jE_i,j). 1. Let α:=(o→(s,t)ot)∈∂iα:=(o _(s,t)ot)∈ _i, and let m∈Rim∈ R_i. Then there is exactly one u∈Obj(Ei,j)u∈ Obj(E_i,j) such that both of the following hold: (i) there is an arrow 1→(m,u)u1 _(m,u)u, and (i) the ϕi,1 _i,1 component of u is α. 2. Let α=(1→(m,u)u),α′=(1→(m′,u′)u′)α=(1 _(m,u)u),α =(1 _(m ,u )u ) be arrows in Ei,jE_i,j, where m,m′∈Rim,m ∈ R_i; and assume u,u′u,u have the same ϕi,1 _i,1 component. Then there is β∈Hom(u,u′)β∈ Hom(u,u ) such that α′=αβα =αβ. Proof. We show this by induction over j. The claims are immediate at j=1j=1. For the first claim, we show the inductive step using Lemma 62. For any arrow α=(1→(m,o)o)α=(1 _(m,o)o) with m∈Rim∈ R_i, Lemma 62.2 entails that ω is single-valued on all arrows β=(o→(m′,t)ot)β=(o _(m ,t)ot) with mm′∈Rimm ∈ R_i; hence, inductively, after passing to Ei,j+1E_i,j+1, only a single arrow is derived from β. The second claim follows by choosing n such that m′=mnm =mn; the first claim enforces the presence of an arrow covering n in Hom(u,u′)Hom(u,u ). ∎ Lemma 64 (Termination). The inner loop always terminates. Proof. A new morphism ϕi,j _i,j can only be accepted because it separates two arrows in a homset Hom(o→o′)Hom(o→ o ) where o,o′o,o are both inside RiR_i. 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,jE_i,j that, for each entry arrow α, we can uniquely assign a single o for every r∈Rir∈ R_i, and this mapping is a surjection onto the objects inside RiR_i. Also, with every j iteration, this structure becomes finer, i.e., a homset Hom(o→o′)Hom(o→ o ) where o,o′o,o are in RiR_i can split into several ones that (save for arrows leaving RiR_i, 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 RiR_i, 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 RiR_i that however do not end RiR_i, 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,jE_i,j, the procedure terminates with failure. We localize this failure into a smaller, focused category. Definition 66. For each object o inside RiR_i, we consider the strongly connected component (or “bonded component” in Tilson 1987) of o: Obj(Co):= Obj(C_o):= o′∈Obj(Ei,j):Hom(o→o′)≠∅,Hom(o′→o)≠∅ \o ∈ Obj(E_i,j):Hom(o→ o )≠ ,Hom(o → o)≠ \ As above, let π be the canonical division π:Ei,j≺Mπ E_i,j M. Within any homset Hom(o′→o′)Hom(o → o ) in CoC_o, we merge any two arrows β,β′β,β such that, in Ei,jE_i,j, Hom(1→o′)βHom(1→ o )β and Hom(1→o′)β′Hom(1→ o )β both are not in π−1(⋃j≤iRj)π^-1( _j≤ iR_j). By construction, CoC_o is a well-defined category, and Co≺Ei,j≺MC_o E_i,j M. Lemma 67. Every homset Hom(u→u′)Hom(u→ u ) in CoC_o hosts an arrow ending in RiR_i. Proof. Otherwise, a morphism ϕ′φ satisfying the second condition would have been selected. ∎ Lemma 68. Failure of the algorithm entails that some CoC_o contains a non-singleton homset, i.e., CoC_o is not trivial. Proof. Failure of the algorithm implies that there is m∈Rim∈ R_i such that ϕi,j−1(ϕi,j(m))⊋m _i,j^-1( _i,j(m)) \m\. Now consider m′∈Mm ∈ M, m≠m′m≠ m such that there is some o^∈ϕi,j(m)∩ϕi,j(m′) o∈ _i,j(m)∩ _i,j(m ). Let o be the corresponding element of Ei,jE_i,j. This means that, in Ei,jE_i,j, there are distinct arrows 1→(m,o~)o1 _(m, o)o and 1→(m′,o)o1 _(m ,o)o. Now we consider the ϕi,1 _i,1 coordinate of o (“entry point coordinate”); this is of the form (u→(s,t)v)(u _(s,t)v) corresponding to some arrow of Dϕi−1D_ _i-1. By the inductive hypothesis “(Invariant(i))”, Hom(1→u)Hom(1→ u) in that category had exactly one object 1→(s′,u)u1 _(s ,u)u, where s′∈Rks ∈ R_k for some k<ik<i. We can thus factorize 1→(m,o~)o=(1→(s′,u)u)(u→(s,t)v)(v→(w,…)o)1 _(m, o)o= (1 _(s ,u)u ) (u _(s,t)v ) (v _(w,…)o ) (9) 1→(m′,o~)o=(1→(s′,u)u)(u→(s,t)v)(v→(w′,…)o)1 _(m , o)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 CoC_o (by Lemma 63.1); then (by Lemma 63.2) there is an arrow α=1→(s′s,v)vα=1 _(s s,v)v such that there are β,β′∈Hom(v,o)β,β ∈ Hom(v,o) with 1→(m,o~)o=αβ1 _(m, o)o=αβ and 1→(m′,o)o=αβ′1 _(m ,o)o=αβ . We thus have shown Hom(v,o)Hom(v,o) to be nonsingleton. ∎ Lemma 69 (Extension Lemma). Assume ω:Co⊲ℤω:C_o Z stays finite-image on all arrows in CoC_o that end in RiR_i. Then there is an algebraic relational morphism ω~:Ei,j⊲ℤ ω:E_i,j Z such that ω~(1→(s,t)t) ω(1 _(s,t)t) is a singleton set whenever s∈Ris∈ R_i, and ω~|Co≡ω ω|_C_o≡ω. Proof. There are two aspects here: achieving ω~|Co≡ω ω|_C_o≡ω – this is easy because CoC_o is a bonded component – and achieving that ω~(1→(s,t)s) ω(1 _(s,t)s) is a finite set for s∈Ris∈ R_i – which requires care. We first define ω∗(α):=ω⁡(α)α∈Co0else _*(α):= casesω(α)&α∈ C_o\\ \0\&else cases (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 ω~(α)=⋃γ1…γn=α∑i=1nω∗(γi) ω(α)= _ _1… _n=α _i=1^n _*( _i) (12) where “∑Σ” is to be understood in a set-valued sense as A+B=a+b:a∈A,b∈BA+B=\a+b:a∈ A,b∈ B\. Because CoC_o is a strongly connected component, ω~|Co≡ω ω|_C_o≡ω. Now consider α:1→(s,t)tα:1 _(s,t)t for some s∈Ris∈ R_i. One option is that t∉Cot ∈ C_o; in this case, no path through CoC_o can multiply out to this arrow, and ω~(α)=0 ω(α)=\0\, which is a finite set. The other option is that t∈Cot∈ C_o. Assume ω⁡(α)ω(α) is infinite. Then, for each n, there is a path of the form: α=γ1γ2γ3…γnα= _1 _2 _3… _n (13) where ∑i=2nω∗(γi) _i=2^n _*( _i) contains unboundedly (positive or negative) large numbers; we can WLOG choose this so that ω∗(γ2)≠0 _*( _2)≠\0\ by multiplying the initial prefix out into γ1 _1 if needed. By construction, γ2∈Co _2∈ C_o; hence, γ1 _1 must end in CoC_o. But then we can set β:=γ2⋅⋯⋅γnβ:= _2·…· _n, which starts and ends in CoC_o, and also ends in RiR_i because α does. But then ω~(β(n)) ω(β(n)) has unboundedly large numbers as n→∞n→∞, which is a contradiction to ω~|Co≡ω ω|_C_o≡ω. ∎ Lemma 70. Consider two arrows in the same homset in CoC_o: β1:=u→(s,t)ut _1:=u _(s,t)ut and β2:=u→(s′,t′)ut _2:=u _(s ,t )ut. If β1≠β2 _1≠ _2, then 1. there is λ∈Ri∩π⁡(Hom(1→u))λ∈ R_i∩π(Hom(1→ u)) such that λs≠λs′λ s≠λ s . 2. there is α∈Hom(o→u)α∈ Hom(o→ u) such that αβ1≠αβ2α _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,jE_i,j, the procedure terminates with failure. Setting up a division Choose as C′C one nontrivial CoC_o (it doesn’t matter which one); from now on this fixes o. For the purposes of defining typed division, we view CoC_o as rooted in o (Definition 75). Assume M divides an iterated wreath product of (ℤ,ℤ+)(Z,Z_+), then so does C′C (in the sense of Definition 75) by Lemma 77. Consider a division of a minimum-depth wreath product of ℤZ, ψ:C′≺ℤ⋅∘…⋅∘ℤ⏟T timesψ:C Z 1.07639pt· … 1.07639pt· Z_T times (here all ℤZ are typed like (ℤ,ℤ+)(Z,Z_+)); in particular, because C′C is not trivial, T≥1T≥ 1. Let ω=π(T)∘ψω=π^(T) ψ; by definition, ω:C′⊲ℤω:C Z. Our goal is to create a division μ:C′≺ℤ⋅∘…⋅∘ℤ⏟T−1 timesμ:C Z 1.07639pt· … 1.07639pt· Z_T-1 times (again in the sense of Definition 75). This would be a contradiction to the minimality of T. As a consequence, C′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 RiR_i (in which case ω provides as much information as an element of Ωi,j _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 RiR_i inside C′C First, assume ω stays finite-image on all arrows ending in RiR_i inside C′C . We obtain ω~:Ei,j⊲ℤ ω:E_i,j Z via Lemma 69. We observe that ω~∈Ωi,j ω∈ _i,j; hence, ω~ ω must assign singleton images to any arrow in CoC_o that ends inside RiR_i. The algorithm having terminated means that ω~ ω, and hence ω, cannot assign distinct images to any two arrows staying inside RiR_i that appear in a single homset in CoC_o; also, any of these needs to be mapped to a singleton set. It also means that, when considering an arrow that is in CoC_o but ends outside of RiR_i, it might in fact be assigned some further set of values, but it must overlap with the value assigned to the arrows staying inside RiR_i. 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 RiR_i. For each homset Hom(u→u′)Hom(u→ u ), we obtain a unique θu,u′∈ℤ _u,u such that ω⁡(α)=θu,u′ω(α)=\ _u,u \ whenever α∈Hom(u→u′)α∈ Hom(u→ u ) ends in RiR_i; also, when the homset contains an arrow leaving RiR_i (we can write it as β:u→(⊥,…)u′β:u _( ,…)u ), θu,u′∈ω⁡(β) _u,u ∈ω(β). We write νu:=θo,u _u:= _o,u; importantly, νut=νuθu,ut _ut= _u _u,ut. We obtain the desired division μ:Co≺(ℤ⋅∘…⋅∘ℤ)⏟T−1 timesμ:C_o (Z 1.07639pt· … 1.07639pt· Z)_T-1 times as follows. Note that any object in the image of ψ has the form (g,…)(g,…) where g:ℤ→(ℤ⋅∘…⋅∘ℤ)⏟T−1 timesg:Z→ (Z 1.07639pt· … 1.07639pt· Z)_T-1 times. For any arrow u→(s,t)utu _(s,t)ut in CoC_o, we define: μ(u→(s,t)ut):=g(νu):(g,θu,ut)∈ψ(u→(s,t)ut)μ(u _(s,t)ut):=\g( _u):(g, _u,ut)∈ψ(u _(s,t)ut)\ (14) which is a nonempty subset of (ℤ⋅∘…⋅∘ℤ)⏟T−1 times (Z 1.07639pt· … 1.07639pt· Z)_T-1 times. We first show that μ is an algebraic relational morphism. Consider arrows α:u→(s,t)utα:u _(s,t)ut and β:ut→(s′,t′)utt′β:ut _(s ,t )utt in CoC_o. Then: μ⁡(α)μ(β)= μ(α)μ(β)= g⁡(νu):(g,θu,ut)∈ψ⁡(α)g′(νut):(g′,θut,utt′)∈ψ⁡(β) \g( _u):(g, _u,ut)∈ψ(α)\\g ( _ut):(g , _ut,utt )∈ψ(β)\ = = g(νu)g′(νut):(g,θu,ut)∈ψ(α),(g′,θut,utt′)∈ψ(β) \g( _u)g ( _ut):(g, _u,ut)∈ψ(α),(g , _ut,utt )∈ψ(β)\ ⊆ g⁡(νu):(g,θu,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,tut _1:=u _s,tut, β2:=u→s′,tut _2:=u _s ,tut in C′C ; if they are distinct, we find α∈Hom(o→u)α∈ Hom(o→ u) such that αβ1≠αβ2α _1≠α _2 (Lemma 70). Then there are disjoint types T1,T2T_1,T_2 of ℤ⋅∘…⋅∘ℤ⏟T times Z 1.07639pt· … 1.07639pt· Z_T times such that ψ⁡(αβ1)⊆T1ψ(α _1) T_1, ψ⁡(αβ2)⊆T2ψ(α _2) T_2. That is, for any gs,gs′g_s,g_s selected for the two arrows, we have (gα(⋅)gs(⋅θo,u),θo,uθo,ut)∈ψ(αβ1)⊆T1(g_α(·)g_s(· _o,u), _o,u _o,ut)∈ψ(α _1) T_1 (15) (gα(⋅)gs′(⋅θo,u),θo,uθo,ut)∈ψ(αβ2)⊆T2(g_α(·)g_s (· _o,u), _o,u _o,ut)∈ψ(α _2) T_2 (16) Hence, there must be disjoint types V1,V2V_1,V_2 of ℤ⋅∘…⋅∘ℤ⏟T−1 times Z 1.07639pt· … 1.07639pt· Z_T-1 times such that μ⁡(αβ1)=gα(0)gs(θo,u)∈V1μ(α _1)=g_α(0)g_s( _o,u)∈ V_1 (17) μ⁡(αβ2)=gα(0)gs′(θo,u)∈V2μ(α _2)=g_α(0)g_s ( _o,u)∈ V_2 (18) But then gs(θo,u)∈gα(0)−1V1g_s( _o,u)∈ g_α(0)^-1V_1 (19) gs′(θo,u)∈gα(0)−1V2g_s ( _o,u)∈ g_α(0)^-1V_2 (20) where V1∩V2=∅V_1∩ V_2= , the types gα(0)−1V1g_α(0)^-1V_1 and gα(0)−1V2g_α(0)^-1V_2 are also disjoint types.1212 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(ℤ) wpc(Z). The above assumes that T1,T2T_1,T_2 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 RiR_i inside C′C Let α=(u0→(s0,t0)u0t0)α= (u_0 _(s_0,t_0)u_0t_0 ) in C′C be an arrow ending in RiR_i 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). Note that any object in the image of ψ has the form (g,…)(g,…) where g:ℤ→(ℤ⋅∘…⋅∘ℤ)⏟T−1 timesg:Z→ (Z 1.07639pt· … 1.07639pt· Z)_T-1 times. Because g arises from a composition of type-respecting functions, g⁡(∞):=limx→∞g⁡(x)g(∞):= _x→∞g(x) is well-defined and in ℤZ. We define μ(u→(s,t)ut):=g(∞):(g,…)∈ψ(u→(s,t)ut)μ(u _(s,t)ut):=\g(∞):(g,…)∈ψ(u _(s,t)ut)\ (21) which is a subset of (ℤ⋅∘…⋅∘ℤ)⏟T−1 times (Z 1.07639pt· … 1.07639pt· Z)_T-1 times. This is an algebraic relational morphism μ:C′⊲(ℤ⋅∘…⋅∘ℤ)⏟T−1 timesμ:C (Z 1.07639pt· … 1.07639pt· Z)_T-1 times: For arrows β,β′β,β such that ββ′β is defined, we have: μ⁡(β)μ(β′)= μ(β)μ(β )= g(∞)h(∞):(g,…)∈ψ(β),(h,…)∈ψ(β′) \g(∞)h(∞):(g,…)∈ψ(β),\ (h,…)∈ψ(β )\ = = limx→∞(g(x)h(x)):g…,h… \ _x→∞(g(x)h(x)):g...,h...\ = = limx→∞(g(x)h(xτ1)):g…,h… \ _x→∞(g(x)h(x _1)):g...,h...\ ⊆ G⁡(∞):(G,…)∈ψ⁡(ββ′) \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′C : β1:=u→(s,t)utβ2:=u→(s′,t′)ut _1:=u _(s,t)ut\;\;\;\;\;\;\;\;\; _2:=u _(s ,t )ut If β1≠β2 _1≠ _2, that means there is λ∈Ri∩π−1(Hom(1→u))λ∈ R_i∩π^-1(Hom(1→ u)) such that λs≠λs′λ s≠λ s , by Lemma 70. We now construct ρ1,ρ2∈M _1, _2∈ M such that α:=1→(ρ1,u0)u0→(s0,t0)u0t0→(ρ2,t′)u=1→(ρ1s0ρ2,u)uα:=1 _( _1,u_0)u_0 _(s_0,t_0)u_0t_0 _( _2,t )u=1 _( _1s_0 _2,u)u (22) in Hom(1→u)Hom(1→ u) satisfies λ∈π−1(α)λ∈π^-1(α).1313 13 Choose ρ1∈Ri _1∈ R_i just to produce the first arrow. Now we choose ρ2∈M _2∈ M such that ρ1s0ρ2=λ _1s_0 _2=λ, using that ρ1s0ρ2 _1s_0 _2 and λ both are in RiR_i. Now applying Lemma 62 (Claim 2) inductively to each j, there is an arrow uot0→(ρ2,t′)u_ot_0 _( _2,t )u. Hence, αβ≠αβ′αβ≠αβ in Ei,jE_i,j. In C′C , α′:=u0→(s0,t0)u0t0→(ρ2,t′)uα :=u_0 _(s_0,t_0)u_0t_0 _( _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 See 15 Proof. We need to show that (i) the algorithm from Definition 58 correctly determines membership in - C-RASP (shown in Theorem 57), and (i) that it runs in polynomial time in |M||M|. For (i), 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⊲ℤφ :E_i,j Z by restricting to the strongly-connected component CoC_o, encoding (i) respecting composition, (i) 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 _i,j via the Extension Lemma 69. ∎ Corollary 72. -∩=wpc() C-RASP∩REG= wpc(Dy). 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≺k1∘…∘krM _k_1 … D_k_r. ∎ 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φ:X M from a category X to a monoid M specifies, for each arrow α in X a nonempty set ϕ⁡(α)⊆Mφ(α) M, such that ϕ⁡(α)ϕ(β)⊆ϕ⁡(αβ)φ(α)φ(β) φ(αβ) when α∈Hom(o→o′),β∈Hom(o′→o′)α∈ Hom(o→ o ),β∈ Hom(o → o ), and 1M∈ϕ⁡(1o)1_M∈φ(1_o) where 1o∈Hom(o→o)1_o∈ 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ψ:X N is an algebraic relational morphism ψ:X⊲Nψ:X N where, for any two distinct arrows α,α′∈Hom(o→o′)α,α ∈ 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,S,ℰS)S=(S, T_S,E_S) be a typed monoid. A typed division ψ:C⪯Sψ:C S is an algebraic division ψ:C⊲Sψ:C S, such that, for each homset H=HomC(o→o′)H=Hom_C(o→ o ), for each α∈Hα∈ H, there is a type T∈ST∈ T_S such that ψ⁡(α)=T∩ψ⁡(H)ψ(α)=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,1414 14 We note that there is also a notion of division in Krebs 2008, but here we link our relational definition directly to language recognition. 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η: ^* M be a surjective morphism, and h:Σ∗→Sh: ^*→ S a morphisms. Assume that for every P⊆MP M, there is TP∈ST_P∈ T_S such that η−1(P)=h−1(TP).η^-1(P)=h^-1(T_P). Then M⪯SM S in the sense of Definition 75, viewing M as a single-object category. Proof. Consider the relation ψ⊆M×Sψ M× S defined by ψ:=h∘η−1ψ:=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α∈ M, there is a type Tα∈ST_α∈ T_S such that η−1(α)=h−1(Tα)η^-1(α)=h^-1(T_α). This entails ψ⁡(α)=h⁡(η−1(α))=h⁡(h−1(Tα))=Tα∩ψ⁡(M)ψ(α)=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,S,ℰS)S=(S, T_S,E_S) be a typed monoid. Assume that M and S satisfy the assumptions of Lemma 76. Assume C⪯MC M (in the sense of Tilson 1987). Then C⪯SC 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. Proof. Let ϕ:C⊲Mφ C M be an algebraic division and let θ:M⊲Sθ M S be a typed division. Define their composite relation ψ:C⊲Sψ C S by ψ⁡(α)=⋃m∈ϕ⁡(α)θ⁡(m)ψ(α)= _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⊆SA S such that for every m∈Mm∈ M there is a type ∈S m∈ T_S with θ⁡(m)=A∩.θ(m)=A∩ m. Fix a homset H of C, and put AHψ:=⋃β∈Hψ⁡(β)A_H^ψ:= _β∈ Hψ(β). For α∈Hα∈ H, ψ⁡(α)=⋃m∈ϕ⁡(α)(AHψ∩)=AHψ∩(⋃m∈ϕ⁡(α)).ψ(α)= _m∈φ(α)(A_H^ψ∩ m)=A_H^ψ∩ ( _m∈φ(α) m ). Because M is finite and S T_S is a Boolean algebra, the finite union :=⋃m∈ϕ⁡(α) a:= _m∈φ(α) m is again a type of S. Thus ψ⁡(α)=AHψ∩,ψ(α)=A_H^ψ∩ a, so ψ is a typed relational morphism. ∎ Appendix I Algebraic Characterization (Necessary but not Sufficient Criterion) See 13 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∈ωM∈R^ω. By substituting 11 for y in ωR^ω we obtain that M satisfies xωx=xωx^ωx=x^ω which implies M∈M∈A (Pin 2009). Next, assume for sake of contradiction that M∉∘M ∈R G. Then there is a ℛR-class of M which contains at least 22 idempotents (Stiffler Jr 1973, Theorem 3.18). Let e1≠e2e_1≠ e_2 be ℛR-equivalent idempotents, where e1=e2m2e_1=e_2m_2 and e2=e1m1e_2=e_1m_1. Then (e1e2)ω=(e1e1m1)ω=(e1m1)ω=e2ω=e2 (e_1e_2)^ω=(e_1e_1m_1)^ω=(e_1m_1)^ω=e_2^ω=e_2 while (e1e2)ωe1=e2e1=e2e2m2=e2m2=e1. (e_1e_2)^ωe_1=e_2e_1=e_2e_2m_2=e_2m_2=e_1. This implies (e1e2)ω≠(e1e2)ωe1(e_1e_2)^ω≠(e_1e_2)^ωe_1, and thus M∉ωM ∈R^ω, a contradiction. Thus M∈∘M∈R G. Now we show ∘∩⊆ωR G∩A R^ω. Let m1,m2∈Mm_1,m_2∈ M. First, we note that (m1m2ω)ω=(m2ωm1)ω(m_1m_2^ω)^ω=(m_2^ωm_1)^ω. This is because (m1m2ω)ω (m_1m_2^ω)^ω =(m1m2ω)ω+1 =(m_1m_2^ω)^ω+1 by aperiodicity =m1(m2ωm1)ωm2ω =m_1(m_2^ωm_1)^ωm_2^ω ≤ℛm1(m2ωm1)ω _Rm_1(m_2^ωm_1)^ω ≤ℛ(m1m2ωm1)ωm1 _R(m_1m_2^ωm_1)^ωm_1 ≤ℛ(m2ωm1)ω _R(m_2^ωm_1)^ω and similarly we have (m2ωm1)ω≤ℛ(m1m2ω)ω(m_2^ωm_1)^ω _R(m_1m_2^ω)^ω. Then, because ℛR-equivalent idempotents are equal in M∈∘∩M∈R G∩A. Now consider the elements(m1m2ω)ω(m_1m_2^ω)^ω and (m1m2ω)ω(m2ωm1)ω(m_1m_2^ω)^ω(m_2^ωm_1)^ω, which are both idempotent. We show these are ℛR-equivalent. First (m1m2ω)ω≥ℛ(m1m2ω)ωm1≥ℛ(m1m2ω)ω+1(m_1m_2^ω)^ω _R(m_1m_2^ω)^ωm_1 _R(m_1m_2^ω)^ω+1, so by aperiodicity (m1m2ω)ω≡ℛ(m1m2ω)ωm1(m_1m_2^ω)^ω _R(m_1m_2^ω)^ωm_1. Then (m1m2ω)ω(m2ωm1)ω (m_1m_2^ω)^ω(m_2^ωm_1)^ω =(m1m2ω)ωm2ω(m1m2ω)ωm1 =(m_1m_2^ω)^ωm_2^ω(m_1m_2^ω)^ωm_1 =(m1m2ω)ωm1m2ωm2ω(m1m2ω)ωm1 =(m_1m_2^ω)^ωm_1m_2^ωm_2^ω(m_1m_2^ω)^ωm_1 =(m1m2ω)ωm1 =(m_1m_2^ω)^ωm_1 Since these are in fact both ℛR-equivalent idempotents, they are equal (Stiffler Jr 1973). Thus using the above equalities we can conclude (m1m2ω)ω=(m1m2ω)ω(m2ωm1)ω=(m1m2ω)ωm1.(m_1m_2^ω)^ω=(m_1m_2^ω)^ω(m_2^ωm_1)^ω=(m_1m_2^ω)^ωm_1. ∎ See 14 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 U1U_1 and kD_k – in this case U1⪯1U_1 D_1. In the other direction, k∈-D_k∈ C-RASP, and thus wpc() wpc(Dy) contains only monoids in - C-RASP, using section E.2. We use this to show the other strict inclusions. • First, =wpc(U1)R= wpc(U_1). U1∈U_1∈Dy. Then we have that -∩=wpc() C-RASP∩REG= wpc(Dy), so ⊆-∩R C-RASP∩REG. For a strict separation, 1∈-∩D_1∈ C-RASP∩REG but 1∉D_1 ∈R (Brzozowski & Fich 1980). • We have that -∩=wpc() C-RASP∩REG= wpc(Dy). Then by proposition 23 we know kD_k divides into a wreath product of U1U_1 and cyclic groups. We can move all U1U_1 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 13. For a strict separation, the monoid M⁡((ab+bba)∗)∈ω∖-M((ab+bba)^*)∈R^ω C-RASP (this can be computed by the decision procedure) • First, ω⊆⊊R^ω A REG by 13. The strict separation can be witnessed by M⁡((ab+aabb)∗)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∗)∗)M((b^*ab^*ab^*)^*) (i.e. ℤ/2ℤZ/2Z) witnesses the strict separation. ∎ Appendix 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 #↼ \# to-0.5pt -2.0pt $ $ (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). Throughout, write =(Q,δ,Σ)A=(Q,δ, ) for a semiautomaton where δ is extended to Σ∗ ^* as usual. We write tq,w,it^q,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⊧ϕq,w,i φ for the truth of a formula at that position. We write tq,wt^q,w as shorthand for tq,w,|w|t^q,w,|w|. We write L⁡(,q0,F)L(A,q_0,F) to denote the language recognized by A with start state q0∈Qq_0∈ Q and accepting states F⊆QF Q. Definition 78 (SCC). W⊆QW Q is a strongly connected component of A if it is maximal such that for all q1,q2∈Wq_1,q_2∈ W there is w∈Σ∗w∈ ^* with δ⁡(q1,w)=q2δ(q_1,w)=q_2. W is trivial if W=qW=\q\ and δ⁡(q,σ)≠qδ(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 ↾W=(W⊔SW,δW,Σ)A W=(W S_W, _W, ) where SW S_W =δ(p,σ)∣p∈W,σ∈Σ∖W =\δ(p,σ) p∈ W,\ σ∈ \ W δW(q,σ) _W(q,σ) =δ⁡(q,σ)q∈Wqq∈SW. = casesδ(q,σ)&q∈ W\\ q&q∈ S_W. cases 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 SWS_W 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, q0q_0 a state of A, and t a term of - C-RASP. We define the following function: Vq0,q(t) V_q_0,q(t) =tq0,w,i∣δW(q0,w≤i)=qq∈Wtq0,w,i∣δW(q0,w≤i−1)∈W,δW(q0,w≤i)=qotherwise = cases\t^q_0,w,i _W(q_0,w_≤ i)=q\&q∈ W\\ \t^q_0,w,i _W(q_0,w_≤ i-1)∈ W, _W(q_0,w_≤ i)=q\&otherwise\\ cases In other words, for states in W, the function Vq0,qV_q_0,q take the set of all realizable counts on a path from q0→q_0→ q, and for states immediately outside of W we take the counts realizable by a path q0→q_0→ 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∈↾Wq_1,q_2∈A W are separated by a term t if there is some q0∈Wq_0∈ W such that Vq0,q1(t)∩Vq0,q2(t)=∅V_q_0,q_1(t)∩ V_q_0,q_2(t)= . We say W is separable if every pair of distinct states in ↾WA W is separated by some t. We say W is separable if every pair of distinct states in ↾WA W is separated by some t. Definition 82 (Balanced). The subterms of a term t are t itself alongside every term t′t occurring inside a subformula [t′≥C][t ≥ C]. A term t is balanced on W if there is an interval [α,β][α,β] such that Vq0,q(t)⊆[α,β]V_q_0,q(t) [α,β] for all q0,q∈Wq_0,q∈ W. A term t is totally balanced on W if all subterms t′∈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|V(t)|=1. Lemma 83. If t is balanced on W, then |Vq0,q(t)|=1|V_q_0,q(t)|=1 for all q0,q∈Qq_0,q∈ Q. Proof. Suppose otherwise that some Vq0,q(t)V_q_0,q(t) holds two values x1≠x2x_1≠ x_2. Since cycles in W must sum to 00 (otherwise t would be unbalanced), Vq,q0(t)V_q,q_0(t) must contain −x1-x_1 and −x2-x_2. However, this implies the existence of some cycle q0→q0q_0→ q_0 with weight x1−x2≠0x_1-x_2≠ 0. ∎ With these notions at hand, we are ready to state the main claim. Lemma 84 (Definability Criterion). Let =(Q,δ,Σ)A=(Q,δ, ) be a semiautomaton. The following are equivalent 1. L⁡(,q0,F)L(A,q_0,F) is recognizable in - C-RASP for any q0∈Qq_0∈ Q and F⊆QF Q. 2. ↾WA W is separable by totally balanced terms for every SCC W in A. Proof. First, (2)⇒(1)(2) (1) is shown in lemma 84. Then, ¬(2)⇒¬(1) (2) (1) is shown in lemma 84. ∎ Lemma 85. [Construction] Suppose every SCC in A is separable by totally balacned terms Fix q0∈Qq_0∈ Q. Then for each q∈Qq∈ Q there exists a - C-RASP formula ϕq _q such that w⊧ϕq⇔δ⁡(q0,w)=qw _q δ(q_0,w)=q. Proof. First, for any q∈Qq∈ Q not reachable from q0q_0 we can set ϕq=⊥ _q= . Otherwise, we induct on the reachability order of SCC’s in A. Consider the first SCC W containing q0q_0. Because W is separable by a totally balanced terms, for each q1,q2∈↾wq_1,q_2∈A w there exists a totally balanced term t that separates them. We will define a formula ϕq1,¬q2 _q_1, q_2 such that strings which land on q1q_1 always satisfy ϕq1,q2 _q_1,q_2 while strings that land in q2q_2 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 _q_1, q_2 :=(⋁c∈Vq0,q1(t)t=c)∧¬(⋁c∈Vq0,q2(t)t=c) := ( _c∈ V_q_0,q_1(t)t=c ) ( _c∈ V_q_0,q_2(t)t=c ) Then, we can let ϕq:=⋀q′≠q∈↾Wϕq,¬q′ _q:= _q ≠ q∈A W _q, q . For the inductive step on an SCC W′W , we have by assumption formulas ϕq0′ _q_0 which detect entry into W′W (as these are states in SWS_W from previous SCC’s). By assumption, there exists ϕq0′,q _q_0 ,q which detects if A is in q if we started in state ϕq0′ _q_0 Since, by assumption, no atom appears negatively, we can take ϕq _q and apply the mapping σ↦(σ∧#↼ϕq0′≥1)σ (σ \# to-0.5pt -2.0pt $ $ _q_0 ≥ 1) to transform ϕq0′,q↦ϕ^q0′,q _q_0 ,q φ_q_0 ,q. Intuitively, this transformation tells ϕq0′,q _q_0 ,q to ignore all symbols which occurred before the first q0′q_0 (i.e. before we entered W′W via q0′q_0 ). Now, define the set of entry points EW′=q∣δ(q′,σ)=q,q′∉W′E_W =\q δ(q ,σ)=q,q ∈ W \, and then we can let ϕq=⋁q0′∈EW′ϕ^q0′,q _q= _q_0 ∈ E_W φ_q_0 ,q. ∎ Lemma 86 (Contradiction). Let ,q0,FA,q_0,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⁡(,q0,F)L(A,q_0,F) is not definable in - C-RASP. Proof. Let ϕφ be any - C-RASP formula and C0C_0 be larger than any theshold or coefficient in any subformula of the form ∑χ⋅#↼[ψ]≥CΣχ· \# to-0.5pt -2.0pt $ $ [ψ]≥ C. Since W is not separable by totally balanced terms, there are q1,q2∈Wq_1,q_2∈ W such that for all totally balanced terms t and entry points δ⁡(q0,x)=qιδ(q_0,x)=q_ , we have that Vqι,q1(t)=Vqι,q2(t)V_q_ ,q_1(t)=V_q_ ,q_2(t). Let w1w_1 and w2w_2 be the minimal strings such that δ⁡(qι,w1)=q1δ(q_ ,w_1)=q_1 and δ⁡(qι,w2)=q2δ(q_ ,w_2)=q_2. Let v∈Σ∗v∈ ^* be any distinguishing suffix of q1q_1 and q2q_2 – such that δ⁡(q1,v)∈Fδ(q_1,v)∈ F while δ⁡(q2,v)∉Fδ(q_2,v) ∈ F –which always exists as q1,q2q_1,q_2 are distinct states in the minimal automaton. We will prepend very large loops around qιq_ , carefully chosen so that all unbalanced terms ≫C0 C_0 or ≪C0 C_0. Order all unbalanced terms t1,t2,…,tkt_1,t_2,…,t_k. First, we note that for all unbalanced tit_i there exists some loop ui∈Σ∗u_i∈ ^* such that δ⁡(qι,ui)=qιδ(q_ ,u_i)=q_ and the loop sum tiqι,uiui−tiqι,ui≠0t_i^q_ ,u_iu_i-t_i^q_ ,u_i≠ 0 – otherwise, Vqι,qι(ti)V_q_ ,q_ (t_i) would be bounded and tit_i would not be unbalanced on W. Then, there exists some constant c such that the loop u:=u1cku2ck−1⋯ukcu:=u_1^c^ku_2^c^k-1·s u_k^c 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 xuNxu^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 xuNw1xu^Nw_1 and xuNw2xu^Nw_2. Intuitively, any formula [t≥C][t≥ C] converges to ⊤ or ⊥ after enough iterations of u, and the 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, tq0,xuNw1=tq0,xuNw2t^q_0,xu^Nw_1=t^q_0,xu^Nw_2, and appending the suffix v does not change this, so ϕφ will have the same truth value on xuNw1vxu^Nw_1v as xuNw2vxu^Nw_2v – therefore ϕφ cannot define L⁡(,q0,F)L(A,q_0,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 _t,q_0 over states, where q1≈t,q0q2q_1 _t,q_0q_2 whenever Vq0,q1(t)=Vq0,q2(t)V_q_0,q_1(t)=V_q_0,q_2(t). Lemma 87. [Depth-11 Balanced] Let =(Q,δ,Σ)A=(Q,δ, ) be an SCC. The set of all depth-11 - C-RASP terms up to equivalent separability of states can be computed in O⁡(⁡(|Q|,|Σ|)O( poly(|Q|,| |) time. Proof. Let q0∈Qq_0∈ Q. For every term ∑χp#↼[ϕp]Σ _p \# to-0.5pt -2.0pt $ $ [ _p] occurring in a balanced depth-11 we must have that (∑χσ#↼[σ])w,|w|=0 (Σ _σ \# to-0.5pt -2.0pt $ $ [σ] )^w,|w|=0 over any loop w, i.e. when δ⁡(q0,w)=q0δ(q_0,w)=q_0. 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:Σ→ℤE and V:Q→ℤV Q such that the following condition is satisfied: If δ⁡(q1,σ)=q2δ(q_1,σ)=q_2 then V⁡(q2)=V⁡(q1)+E⁡(σ)V(q_2)=V(q_1)+E(σ) (23) If such a function exists, we can obtain a term that sums to 00 on loops via ∑E⁡(σ)#↼[σ]Σ E(σ) \# to-0.5pt -2.0pt $ $ [σ]. If such a term ∑χσ#↼[σ]Σ _σ \# to-0.5pt -2.0pt $ $ [σ] exists, we can obtain the function by setting E⁡(σ)=χσE(σ)= _σ and V⁡(q)=∑1≤i≤|w|E⁡(wi)V(q)= _1≤ i≤|w|E(w_i) for any w such that δ⁡(q0,w)=qδ(q_0,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⁡(⁡(|Q|,|Σ|)CLOSEO( poly(|Q|,| |) time. There are O⁡(|Q|2|Σ|)O(|Q|^2| |) many transitions δ⁡(q1,σ)=q2δ(q_1,σ)=q_2 so we obtain O⁡(|Q|2⋅|Σ|)O(|Q|^2·| |) many constraints of the form V⁡(q2)=V⁡(q1)+E⁡(σ)V(q_2)=V(q_1)+E(σ). These give O⁡(|Q|2|Σ|)O(|Q|^2| |)-many linear constraints over O⁡(|Q|2⋅|Σ|+|Q|)O(|Q|^2·| |+|Q|)-many variables. This can be solved in O⁡(⁡(|Q|,|Σ|)CLOSEO( poly(|Q|,| |) time (Kannan & Bachem 1979). ∎ Lemma 88. Whether an SCC W is separable by totally balanced terms is decidable in O⁡(⁡(|Q|,|Σ|))O( poly(|Q|,| |)) time. Proof. We will iteratively refine an equivalence relation ≡ over states, based upon the set of Vq0,q(t)V_q_0,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 _0:=W× W by setting all elements to the same class. Initialize a set of - C-RASP formulas Φ0:=∅ _0:= . Fix a start state q0q_0 (since a balanced term is balanced given any start state, the exact choice is immaterial). Then perform the loop (2)−(4)(2)-(4): 2. Generate the set BkB_k of all terms that count over formulas in Φk−1 _k-1, up to equivalent separability of states using lemma 87. 3. Denote the indicator for K⊆WK W induced by t as the formula ψK:=⋁q∈Kt=Vq0,q. _K:= _q∈ Kt=V_q_0,q. We generate the collection of indicators of separable state sets by all t∈Bkt∈ B_k as the collection Ψk:=ψK∣Vq0,q1(t)=Vq0,q2(t) for all q1,q2∈K _k:=\ _K V_q_0,q_1(t)=V_q_0,q_2(t) for all $q_1,q_2∈ K$\. 4. Now there are two cases • If Ψk⊈Φk−1 _k _k-1, then define Φk _k to refine Φk−1 _k-1 via intersection with Ψk _k. Φk:=ψK1∩ψK2∣ψK1∈Φk−1,ψK2∈Ψk. _k:=\ _K_1∩ _K_2 _K_1∈ _k-1, _K_2∈ _k\. Next, set ≡k:=(q1,q2)∣q1,q2∈K for some ϕK∈Φk. _k:=\(q_1,q_2) $q_1,q_2∈ K$ for some $ _K∈ _k$\. Then, return to step (2)(2) for iteration k+1k+1. • If Ψk⊆Φk−1 _k _k-1, then we have reached a fixed point. Set Φ:=Φk := _k and ≡:=≡k≡:= _k and move to step (5)(5). 5. If [q]≡[q]_≡ is a singleton for all q, output TRUE and return Φ . Otherwise, output FALSE. Correctness: Since each ϕK∈Φ _K∈ is balanced, all its subterms are balanced and thus if [q]≡[q]_≡ are singletons we can obtain totally balanced terms which separate each pair of states. If some [q]≡[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 _k is monotonoically refined at each step, and Φ keeps only the formulas that define equivalence classes via ≡k _k, and thus there are only O⁡(|Q|2)O(|Q|^2) many of them at each iteration. The first step (1)(1) runs in O⁡(|Q|2)O(|Q|^2) time. Step (2)(2) takes O⁡(⁡(|Q|,|Σ|)CLOSEO( poly(|Q|,| |) time by lemma 87. Step (3)(3) runs in O⁡(⁡(|Q|,|Σ|)CLOSEO( poly(|Q|,| |) time by generating in O⁡(|Q|2)O(|Q|^2) time the equivalence class where Vq0,q1(t)=Vq0,q2(t)V_q_0,q_1(t)=V_q_0,q_2(t) for each of the O⁡(⁡(|Q|,|Σ|)CLOSEO( poly(|Q|,| |) terms t∈Bt∈ B. Step (4)(4) runs in O⁡(⁡(|Q|,|Σ|)CLOSEO( 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 _k-1× _k, since each formula identifies a disjoint set of states K. Step (5)(5) also just needs to check if the equivalence relation has size |Q||Q|, achievable in O⁡(|Q|)O(|Q|) time. Finally, we only need to iterate the (2−4)(2-4) loop O⁡(|Q|2)O(|Q|^2) many times, as the equivalence relation ≡k _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⁡(⁡(|Q|,|Σ|)CLOSEO( poly(|Q|,| |) many SCCs (e.g. using Tarjan’s algorithm (Tarjan 1972)), and only need to perform a O⁡(⁡(|Q|,|Σ|)CLOSEO( poly(|Q|,| |) time query on each one, as in lemma 88. ∎ Appendix 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 BalancedLabelsBasis 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 00). By computing the nullspace of this basis, we find all possible morphisms that sum to 00 on loops, and iteratively relable the symbols according to these morphisms. At the end, the helper function Separated 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). Algorithm 1 - C-RASP Membership 1: procedure DecideMembership(A) 2: SCCs←StronglyConnectedComponents()SCCs← StronglyConnectedComponents(A) 3: for all SCC∈SCCsSCC do 4: Bprev←∅B_prev← 5: Bcurr←BalancedLabelsBasis(SCC)B_curr← BalancedLabelsBasis(SCC) 6: if Nullspace(Bcur)≠∅ Nullspace(B_cur)≠ then 7: while Bcurr∉Span(Bprev)B_curr ∈ Span(B_prev) do 8: labels[σi]←[vi]v∈Bcurrlabels[ _i]←[v_i]_v∈ B_curr 9: for all loop∈LoopsAround(q0,SCC)loop∈ LoopsAround(q_0,SCC) do 10: for all 0≤i≤Len(loop)0≤ i≤ Len(loop) do 11: (qi,σi,qi+1)←loop[i](q_i, _i,q_i+1)← loop[i] 12: SCC.δ.Replace((qi,σ,qi+1),(qi,[σi,∑1≤j≤ilabels[σj]],qi+1))SCC.δ. Replace ((q_i,σ,q_i+1), (q_i, [ _i, _1≤ j≤ ilabels[ _j] ],q_i+1 ) ) 13: end for 14: Bprev←BcurrB_prev← B_curr 15: Bcurr←BalancedLabelsBasis(SCC)B_curr← BalancedLabelsBasis(SCC) 16: end for 17: end while 18: end if 19: if ¬Separated(SCC) Separated(SCC) then 20: return ⊥ 21: end if 22: end for 23: return ⊤ 24: end procedure

Instant research discovery