Lê Thành

Dũng Nguyễn

Camille Noûs

Cécilia Pradic

Tito Nguyễn

Comparison-free polyregular functions

Keywords: 2012 ACM Subject Classification Theory of computation → Transducers pebble transducers, HDT0L systems, polyregular functions

come

Introduction

The theory of transducers (as described in the surveys [START_REF] Filiot | Transducers, Logic and Algebra for Functions of Finite Words[END_REF][START_REF] Muscholl | The Many Facets of String Transducers[END_REF]) has traditionally dealt with devices that take as input strings of length n and output strings of length O(n). However, several recent works have investigated function classes going beyond linear growth. We review three classes in this landscape below.

Polyregular functions ( §2.3) are thus named because they have (at most) polynomial growth and include regular functions ( §2.2) (the most expressive of the traditional string-to-string transduction classes). They were defined in 2018 [4] by four equivalent computational models, one of which -the pebble transducers -is the specialization to strings of a tree transducer model that existed previously in the literature [START_REF] Milo | Typechecking for XML transformers[END_REF] (this specialization had been investigated earlier in [START_REF] Engelfriet | Two-way finite state transducers with nested pebbles[END_REF]16]). A subsequent work [9] gave a logical characterization based on Monadic Second-Order logic (MSO). They enjoy two nice properties: preservation of regular languages (by preimage): if f : Γ * → Σ * is polyregular and L ⊆ Σ * is regular, then f -1 (L) ⊆ Γ * is regular; closure under function composition: if f : Γ * → ∆ * and g : ∆ * → Σ * are both polyregular, then so is g • f : Γ * → Σ * . HDT0L transductions ( §2.1) form another superclass of regular functions, whose output size may be at most exponential in the input size. They are older than polyregular functions, and we shall discuss their history in Section 2.1; suffice to say for now, they also admit various equivalent characterizations scattered in several papers [START_REF] Ferté | Word-Mappings of Level 2[END_REF][START_REF] Filiot | Copyful streaming string transducers[END_REF]15]. These functions preserve regular languages by preimage, but are not closed under composition (the growth rate of a composition of HDT0L transductions may be a tower of exponentials). Very recently, the polynomially bounded HDT0L transductions ( §2.3) have been characterized using two transducer models [15]. One of them, the k-marble transducers (where k ∈ N depends on the function to be computed), is obtained by putting a syntactic constraint on the model of (unbounded) marble transducers [15] which computes HDT0L transductions. But it can also be seen as a restricted variant of pebble transducers; it follows (although this is not explicitly stated in [15]) that a HDT0L transduction has polynomial growth if and only if it is polyregular. Moreover, as claimed in [15, Section 6], the functions computed by k-marble transducers are not closed under composition either, and thus form a strict subclass of polyregular functions.

A new subclass of polyregular functions

In this paper, we start by proving a few results on the above classes (Section 3). For instance, we supply a proof for the aforementioned claim of [15,Section 6], and show that the polyregular functions are exactly those computable by compositions of k-marble transducers. Those complements are not particularly difficult nor surprising and are included mostly for the sake of giving a complete picture.

But our main contribution is the introduction of a new class, giving its title to the paper; as we show, it admits three equivalent definitions: two ways to inductively generate the class (Sections 4 and 6 respectively): by closing regular functions under a certain "composition by substitution" operation; by combining regular functions and a certain kind of squaring functions (less powerful than the squaring plus underlining functions used to characterize general poyregular functions) with usual function composition; a restriction on pebble transducers (Section 5) -we disallow comparing the positions of a transducer's multiple reading heads, hence the name comparison-free polyregular functions (henceforth abbreviated as cfp).

Properties By the third definition above, comparison-free polyregular functions are indeed polyregular, while the second one implies that our new class contains the regular functions and is closed under composition. (In fact, in the proof that our first definition is equivalent to the second one, most of the work goes into showing that the former enjoys closure under composition.) We rule out inclusions involving the other classes that we mentioned by proving some separation results (Section 8): there exist comparison-free polyregular functions that are not HDT0L (we take one example from [15]), and polynomially bounded HDT0L transductions which are not comparison-free: one of our examples follows from a precise characterization of cfp functions over unary input alphabets (extending a known result for regular functions with unary inputs [11]), which we give in Section 9; another example shows that unlike (poly)regular functions, cfp functions are not closed under a certain counterpart of the "map" operation in functional programming. We summarize the inclusions and separations between classes that we get in Figure 1.

Finally, we show in Section 7 that the number of pebbles required to compute a function using a comparison-free transducer is related to its growth rate. The analogous result for pebble transducers was proved recently, with a whole paper dedicated to it [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]; we adapt its arguments to our setting, resulting in our longest and most technical proof. There is a similar property for k-marble transducers [15], but it is proved using very different tools.

Motivations Although this is the first proper paper to introduce comparison-free pebble transducers, we were told that they had already been considered by several colleagues (Mikołaj Bojańczyk, personal communication). But in fact, the starting point in our investigation was a characterization of regular functions using a linear λ-calculus (in the sense of linear logic) that we had previously obtained [START_REF] Thành | Implicit automata in typed λ-calculi II: streaming transducers vs categorical semantics[END_REF]; this was part of a research programme relating automata and functional programming that we initiated in [START_REF] Thành | Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic[END_REF]. As we reported in a previous version of the present paper, by tweaking a parameter in this characterization, one gets the cfp functions instead; we initially defined the latter using composition by substitution, and only later realized the connection with pebble transducers. One interesting feature of the λ-calculus characterization is that it is trivially closed under composition, and this led us to take inspiration from the category-theoretic machinery that we used in [START_REF] Thành | Implicit automata in typed λ-calculi II: streaming transducers vs categorical semantics[END_REF] for our standalone composition proof in this paper.

Added in 2023: an "official" reference for this λ-calculus characterization can now be found in the first author's PhD thesis [START_REF] Thành | Implicit automata in linear logic and categorical transducer theory[END_REF]Theorem 1.2.3].

Preliminaries

Notations The set of natural numbers is N = {0, 1, . . . }. We write |w| for the length of a string w ∈ Σ * ; for Π ⊆ Σ, we write |s| Π for the number of occurrences of letters from Π in w; and for c ∈ Σ, we abbreviate |w| {c} as |w| c . The i-th letter of w ∈ Σ * is denoted by either w i or w [i] (for i ∈ {1, . . . , |w|}). Given monoids M and N , Hom(M, N ) is the set of monoid morphisms. We write ε for the empty word and Σ = {a | a ∈ Σ} for a disjoint copy of the alphabet Σ made of "underlined" letters.

HDT0L transductions and streaming string transducers

L-systems were originally introduced by Lindenmayer [29] in the 1960s as a way to generate formal languages, with motivations from biology. While this language-centric view is still predominant, the idea of considering variants of L-systems as specifications for string-to-string functions -whose range are the corresponding languages -seems to be old. For instance, in a paper from 1980 [START_REF] Engelfriet | Tree transducers, L systems, and two-way machines[END_REF], one can find (multi-valued) string functions defined by ET0L systems.

More recently, Ferté, Marin and Sénizergues [START_REF] Ferté | Word-Mappings of Level 2[END_REF] provided alternative characterizations 1 (by catenative recurrent equations and higher-order pushdown transducers of level 2) of the string-to-string functions that HDT0L systems can express -what we call here HDT0L transductions. Later work by Filiot and Reynier [START_REF] Filiot | Copyful streaming string transducers[END_REF] and then by Douéneau-Tabot, Filiot and Gastin [15] -that does not build on [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF][START_REF] Ferté | Word-Mappings of Level 2[END_REF] -proved the equivalence with, respectively, copyful SSTs (Definition 2.3) and unbounded marble transducers (not presented here).

▶ Definition 2.1 (following [START_REF] Filiot | Copyful streaming string transducers[END_REF]). A HDT0L system consists of: an input alphabet Γ, an output alphabet Σ, and a working alphabet ∆ (all finite); an initial word d ∈ ∆ * ; for each c ∈ Γ, a monoid morphism h c ∈ Hom(∆ * , ∆ * ); a final morphism h ′ ∈ Hom(∆ * , Σ * ).

It defines the transduction taking w

= w 1 . . . w n ∈ Γ * to h ′ • h w1 • . . . • h wn (d) ∈ Σ * .
(The definition of HDT0L systems given in [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF][START_REF] Ferté | Word-Mappings of Level 2[END_REF] makes slightly different choices of presentation 2 .) To define the equivalent model of copyful streaming string transducers, we must first introduce the notion of register assignment.

▶ Definition 2.2. Fix a finite alphabet Σ. Let R and S be two finite sets disjoint from Σ; we shall consider their elements to be "register variables".

For any word ω ∈ (Σ ∪ R) * , we write ω † : (Σ * ) R → Σ * for the map that sends (u r ) r∈R to ω in which every occurrence of a register variable r ∈ R is replaced by u r -formally, we apply to ω the morphism

(Σ ∪ R) * → Σ * that maps c ∈ Σ to itself and r ∈ R to u r . A register assignment 3 α from R to S (over Σ) is a map α : S → (Σ ∪ R) * . It induces the action α † : ⃗ u ∈ (Σ * ) R → (α(s) † (⃗ u)) s∈S ∈ (Σ * ) S (which indeed goes "from R to S").
▶ Definition 2.3 ([24]). A (deterministic copyful) streaming string transducer (SST) with input alphabet Γ and output alphabet Σ is a tuple T = (Q, q 0 , R, δ, ⃗ u I , F ) where Q is a finite set of states and q 0 ∈ Q is the initial state; R is a finite set of register variables, that we require to be disjoint from Σ;

δ : Q × Γ → Q × (R → (Σ ∪ R) * ) is the transition function -we abbreviate δ st = π 1 • δ and δ reg = π 2 • δ, where π i is the projection from X 1 × X 2 to its i-th component X i ;
1 Those characterizations had previously been announced in an invited paper by Sénizergues [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF]. Some other results announced in [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF] are proved in [10]. 2 The family (hc) c∈Γ is presented as a morphism H : Γ * → Hom(∆ * , ∆ * ) (whose codomain is indeed a monoid for function composition). And an initial letter is used instead of an initial word; this is of no consequence regarding the functions that can be expressed (proof sketch: consider ∆ ′ = ∆ ∪ {x} with a new letter x / ∈ ∆, take x as the initial letter and let hc(x) = hc(w), h ′ (x) = h ′ (w)). 3 Some papers e.g. [12,15] call register assignments substitutions. We avoid this name since it differs from its meaning in the context of our "composition by substitution" operation.

⃗ u I ∈ (Σ * ) R describes the initial register values; F : Q → (Σ ∪ R) * describes how to recombine the final values of the registers, depending on the final state, to produce the output. The function

Γ * → Σ * computed by T is w 1 . . . w n → F (q n ) † • δ reg (q n-1 , w n ) † • . . . • δ reg (q 0 , w 1 ) † (⃗ u I )
where the sequence of states (q i ) 0≤i≤n (sometimes called the run of the transducer over the input word) is inductively defined, starting from the fixed initial state q 0 , by q i = δ st (q i-1 , w i ).

▶ Example 2.4. Let Σ = Γ ∪ Γ. We consider a SST T with Q = {q}, R = {X, Y } and ⃗ u I = (ε) r∈R F (q) = Y ∀c ∈ Γ, δ(q, c) = (q, (X → cX, Y → cXY ))
If we write (v, w) for the family (u r ) r∈R with u X = v and u Y = w, then the action of the register assignments may be described as

(X → cX, Y → cXY ) † (v, w) = (c • v, c • v • w).
Let 1, 2, 3, 4 ∈ Γ. After reading 1234 ∈ Γ * , the values stored in the registers of T are

(X → 4X, Y → 4XY ) † • . . . • (X → 1X, Y → 1XY ) † (ε, ε) = (4321, 4321321211)
Since F (q) = Y , the function defined by T maps 1234 to 4321321211 ∈ (Γ ∪ Γ) * = Σ * . This gives us an example of HDT0L transduction Γ * → (Γ ∪ Γ) * , since:

▶ Theorem 2.5 ([24]). A function Γ * → Σ * can be computed by a copyful SST if and only if it can be specified by a HDT0L system.

▶ Remark 2.6. As observed in [START_REF] Filiot | Copyful streaming string transducers[END_REF]Lemma 3.3], there is a natural translation from HDT0L systems to SSTs whose range is composed precisely of the single-state SSTs whose transitions and final output function do not access the letters of their output alphabet -those are called simple SSTs in [15, §5.1]. This involves a kind of reversal: the initial register values correspond to the final morphisms, while the final output function corresponds to the initial word. Thus, Theorem 2.5 is essentially a state elimination result; a direct translation from SSTs to single-state SSTs has also been given by Benedikt et al. [2,Proposition 8]. However, it does not preserve the subclass of copyless SSTs (this would contradict Proposition 3.7).

The lookahead elimination theorem for macro tree transducers [START_REF] Engelfriet | Macro tree transducers[END_REF]Theorem 4.21] arguably generalizes this to trees. Indeed, while those transducers are generally presented as a topdown model, their formal definition can also be read as bottom-up register tree transducers in the style of [8, §4], and top-down lookahead corresponds to bottom-up states.

Regular functions

▶ Definition 2.7 (Alur and Černý [1]). A register assignment α : S → (Σ ∪ R) * from R to S is said to be copyless when each r ∈ R occurs at most once among all the strings α(s) for s ∈ S, i.e. it does not occur at least twice in some α(s), nor at least once in α(s) and at least once in α(s ′ ) for some s ̸ = s ′ . (This restriction does not apply to the letters in Σ.)

A streaming string transducer is copyless if all the assignments in the image of its transition function are copyless. In this paper, we take computability by copyless SSTs as the definition of regular functions (but see Theorem 5.3 for another standard definition).

▶ Remark 2.8. Thanks to Theorem 2.5, every regular function is a HDT0L transduction. ▶ Remark 2.9. The SST of Example 2.4 is not copyless: in a transition α = δ reg (q, c), the register X appears twice, once in α(X) = cX and once in α(Y ) = cXY ; in other words, its value is duplicated by the action α † . In fact, it computes a function whose output size is quadratic in the input size, while regular functions have linearly bounded output.

▶ Example 2.10 (Iterated reverse [4, p. 1]). The following single-state SST is copyless:

Γ = Σ with # ∈ Σ Q = {q} R = {X, Y } ⃗ u I = (ε) r∈R F (q) = XY δ(q, #) = (q, (X → XY #, Y → ε)) ∀c ∈ Σ \ {#}, δ(q, c) = (q, (X → X, Y → cY )) For u 1 , . . . , u n ∈ (Σ \ {#}) * , it maps u 1 # . . . #u n to reverse(u 1 )# . . . #reverse(u n ).
The concrete SSTs (copyless or not) that we have seen for now are all single-state. As a source of stateful copyless SSTs, one can consider the translations of sequential transducers. These are usual finite automata, whose transitions additionally produce a word catenated to the end of the would-be output function. For instance, the one in Figure 2 computes the function {a, b, c} * → {a, b} * that replaces each c in its input by the closest non-c letter on its left (or a if no such letter exists). We do not give a detailed definition (which can be found e.g. in [37, Chapter V]) here, but for our purpose, it suffices to observe any sequential transducer can be translated into a copyless SST with the same set of states and a single register.

Polynomial growth transductions

Next, we recall one way to define Bojańczyk's polyregular functions [4].

▶ Definition 2.11 ([4]). The class of polyregular functions is the smallest class of string-tostring functions closed under composition containing: the functions computed by sequential transducers (for instance, the one of Figure 2); the iterated reverse function of Example 2.10, over any finite alphabet containing #; the squaring with underlining functions squaring Γ : Γ * → (Γ ∪ Γ) * , for any finite Γ, illustrated by squaring Γ (1234) = 1234123412341234.

As mentioned in the introduction, the intersection between the above class and HDT0L transductions has been recently characterized by . ▶ Theorem 2.12 ([15]). Let f : Γ * → Σ * . The following conditions are equivalent:

f is both a polyregular function and a HDT0L transduction; f is a HDT0L transduction and has at most polynomial growth: |f (w)| = |w| O(1) ; there exists k ∈ N such that f is computed by some k-layered SST, defined below. (Another equivalent model, the k-marble transducers, was mentioned in the introduction, but we will not use it in the rest of the paper.) Those k-layered SST propose a compromise between copyful and copyless SSTs: duplication is controlled, but not outright forbidden.

▶ Definition 2.13 ([15]). A register assignment

α : R → (Σ ∪ R) * is k-layered (for k ∈ N) with respect to a partition R = R 0 ⊔ . . . ⊔ R k when for 0 ≤ i ≤ k, for r ∈ R i , we have α(r) ∈ (Σ ∪ R 0 ∪ . . . ∪ R i ) *
; each register variable in R i appears at most once among all the α(r) for r ∈ R i (however, those from R 0 ⊔ . . . ⊔ R i-1 may appear an arbitrary number of times). A SST is k-layered if its registers can be partitioned in such a way that all assignments in the transitions of the SST are k-layered w.r.t. that partition.

Beware: with this definition, the registers of a k-layered SST are actually divided into k + 1 layers, not k. In particular, a SST is copyless if and only if it is 0-layered. (We chose this convention for backwards compatibility with [15]; see also Remark 5.4.)

For instance, the transducer of Example 2.4 is 1-layered with R 0 = {X} and R 1 = {Y }. There also exist register assignments that cannot be made k-layered no matter the choice of partition, such as X → XX. Using such assignments, one can indeed build SSTs that compute functions f such that e.g. |f (w)| = 2 |w| . ▶ Remark 2.14. There is arguably an old precursor to this recent characterization of HDT0L transductions with polynomial growth by a syntactic "layering" condition: Schützenberger's theorem on polynomially bounded Z-rational series, which dates back to the 1960s (see for instance [3, Chapter 9, Section 2] -the preface of the same book describes this theorem as "one of the most difficult results in the area"). Let us give a brief exposition.

A Z-rational series f :

Σ * → Z is a function of the form f : w ∈ Σ * → X T • Φ(w) • Y where X, Y ∈ Z R
and Φ is a morphism from Σ * to the multiplicative monoid of R-indexed square matrices over Z, where R is a finite set. This data (X, Φ, Y ) has a clear interpretation as a "simple SST" (cf. Remark 2.6) with register set R, whose register values are integers rather than strings. Schützenberger's theorem says that any Z-rational series f with polynomial growth (i.e. |f (w)| = |w| O(1) where | • | on the left is the absolute value) can be written as f : w → X T • Φ(w) • Y where (i) the image of Φ has a block triangular structure;

(ii) the projection of this image on each diagonal block is a finite monoid.

The first item gives us a partition of the register into layers where each layer "depends" only on the ones below them. The finiteness condition in the second item is equivalent to having bounded coefficients, which means that the register assignments within each layer are bounded-copy, while in a layered SST, they would be copyless instead -but bounded-copy SSTs are known to be equivalent to copyless SSTs (see e.g. [12]). The theorem also states a relationship between the number of blocks and the growth rate; compare this to Remark 7.2. Via the canonical isomorphism {a} * ∼ = N, HDT0L transductions with unary output alphabet are the same thing as N-rational series. The counterpart of Schützenberger's theorem over N is thus a corollary of the results of [15] on layered SSTs.

Transition monoids for streaming string transducers

To wrap up the preliminaries, let us recall some algebraic tools for working with SSTs (this technical section can be safely skipped on a first reading). Let us start by putting a monoid structure on register assignments (Definition 2.2).

▶ Definition 2.15. Let M R,Σ = R → (Σ ∪ R) * for R ∩ Σ = ∅.
We endow it with the following composition operation, that makes it into a monoid:

α • β = α ⊙ • β where α ⊙ ∈ Hom((Σ ∪ R) * , (Σ ∪ R) * ), α ⊙ (x) = α(x) for x ∈ R x for x ∈ Σ
The monoid M R,Σ thus defined is isomorphic to a submonoid of Hom((Σ ∪ R) * , (Σ ∪ R) * ) with function composition. It admits a submonoid of copyless assignments.

▶ Definition 2.16. We write M cl R,Σ for the set of all α ∈ M R,Σ such that each letter r ∈ R occurs at most once among all the α(r ′ ) for r ′ ∈ R.

▶ Proposition 2.17. M cl R,Σ is a submonoid of M R,Σ . In other words, copylessness is preserved by composition (and the identity assignment is copyless).

The following proposition ensures that this composition does what we expect. Recall from Definition 2.2 that (-

) † sends M R,Σ to (Σ * ) R → (Σ * ) R . ▶ Proposition 2.18. For all α, β ∈ M R,Σ , we have (α • β) † = β † • α † .
To incorporate information concerning the states of an SST, we define below a special case of the wreath product of transformation monoids.

▶ Definition 2.19. Let M be a monoid whose multiplication is denoted by m, m ′ → m • m ′ . We define M ≀ Q as the monoid whose set of elements is Q → Q × M and whose monoid multiplication is, for µ, µ ′ : Q → Q × M , (µ • µ ′ ) : q → (π 1 • µ ′ • π 1 • µ(q), (π 2 • µ(q)) • (π 2 • µ ′ • π 1 • µ(q)))
where

π 1 : Q × M → Q and π 2 : Q × M → M are the projections. For instance, if M is the trivial monoid with one element, Q ≀ M is isomorphic to Q → Q with reverse composition as the monoid multiplication: f • g = g • f .
▶ Proposition 2.20. Let (Q, q 0 , R, δ, ⃗ u I , F ) be an SST that computes f : Γ * → Σ * (using the notations of Definition 2.3). For all c ∈ Γ, we have δ(-, c) ∈ M R,Σ ≀ Q, and the SST is copyless if and only if {δ(-, c)

| c ∈ Γ} ⊆ M cl R,Σ ≀ Q. Furthermore, for all w 1 . . . w n ∈ Γ * , f (w 1 . . . w n ) = F (g(q 0 )) † (α † (⃗ v)) where (g, α) = δ(-, w 1 ) • • • • • δ(-, w n )
Finally, it will sometimes be useful to consider monoids of assignments over an empty output alphabet. This allows us to keep track of how the registers are shuffled around by transitions.

▶ Proposition 2.21. Let R and Σ be disjoint finite sets. There is a monoid morphism In particular, regular functions correspond to 1-layered HDT0L systems.

M R,Σ → M R,∅ , that sends the submonoid M cl R,Σ to M cl R,∅ . For any Q, this extends to a morphism M R,Σ ≀ Q → M R,∅ ≀ Q that sends M cl R,Σ ≀ Q to M cl R,∅ ≀ Q. We
The obvious translation from HDT0L systems to SSTs preserves 1-layeredness and produces a single-state machine, so one may sacrifice copylessness to eliminate states for SSTs.

▶ Corollary 3.3. Every regular function can be computed by a single-state 1-layered SST.

The converse to this corollary does not hold: the single-state 1-layered SST of Example 2.4 computes a function which is not regular (cf. Remark 2.9). The importance of being stateful One interesting aspect of Theorem 3.2 is that 1-layered HDT0L systems can be seen, through Remark 2.6, as a kind of one-way transducer model for regular functions that does not use an explicit control state. This is in contrast with copyless SSTs, whose expressivity critically depends on the states (unlike copyful SSTs).

Polyregular functions vs layered SSTs

▶ Proposition 3.7. The sequential (and therefore regular) function defined by the transducer of Figure 2 (Section 2.2) cannot be computed by a single-state copyless SST.

In fact, the knowledgeable reader can verify that this counterexample belongs to the first-order letter-to-letter sequential functions, one of the weakest classical transduction classes.

Closure under map

The pattern of Example 2.10 (iterated reverse) can be generalized:

▶ Definition 3.8. Let f : Γ * → Σ * and suppose that # / ∈ Γ ∪ Σ. We define the function map(f ) : w 1 # . . . #w n ∈ (Γ ∪ {#}) * → f (w 1 )# . . . #f (w n ) ∈ (Σ ∪ {#}) * .
▶ Proposition 3.9. If f is an HDT0L transduction, then so is map(f ). For each k ≥ 1, the functions that can be computed by k-layered HDT0L systems are also closed under map.

As an immediate corollary, closure under map holds for both regular and polyregular functions, but this was already known. In fact, map(f, [x 1 , . . . , x n ]) = [f (x 1 ), . . . , f (x n )] is an essential primitive in the regular list functions [7] and polynomial list functions [4, §4], two list-processing programming languages that characterize regular and polyregular functions respectively. We will come back to this point in Corollary 8.5 and the subsequent remark.

Composition by substitution

At last, we now introduce the class of comparison-free polyregular functions. The simplest way to define them is to start from the regular functions.

▶ Definition 4.1. Let f : Γ * → I * , and for each i ∈ I, let g i : Γ * → Σ * . The composition by substitution of f with the family (g i ) i∈I is the function

CbS(f, (g i ) i∈I ) : w → g i1 (w) . . . g i k (w) where i 1 . . . i k = f (w)
That is, we first apply f to the input, then every letter i in the result of f is substituted by the image of the original input by g i . Thus,

CbS(f, (g i ) i∈I ) is a function Γ * → Σ * .
▶ Definition 4.2. The smallest class of string-to-string functions closed under CbS and containing all regular functions is called the class of comparison-free polyregular functions.

▶ Example 4.3. The following variant of "squaring with underlining" (cf. Definition 2.11) is comparison-free polyregular:

cfsquaring Γ : 123 ∈ Γ * → 112321233123 ∈ (Γ ∪ Γ) * .
Indeed, it can be expressed as cfsquaring Γ = CbS(f, (g i ) i∈I ) where I = Γ ∪ {#}, the function f : w 1 . . . w n → w 1 # . . . w n # is regular (more than that, a morphism between free monoids) and g # = id, g c : w → c for c ∈ Γ are also regular. Its growth rate is quadratic, while regular functions have at most linear growth. Other examples that also require a single composition by substitution are given in Theorem 8.1.

We can already justify the latter half of the name of our new class. Using the "polynomial list functions" mentioned at the end of the previous section, we prove: ▶ Theorem 4.4. Polyregular functions are closed under composition by substitution.

▶ Corollary 4.5. Every comparison-free polyregular function is, indeed, polyregular.

Fundamentally, Definition 4.2 is inductive: it considers the functions generated from the base case of regular functions by applying compositions by substitution. The variant below with more restricted generators is sometimes convenient.

▶ Definition 4.6. A string-to-string function is said to be: of rank at most 0 if it is regular; of rank at most k + 1 (for k ∈ N) if it can be written as CbS(f, (g i ) i∈I ) where f : Γ * → I * is regular and each g i : Γ * → Σ * is of rank at most k.

▶ Proposition 4.7. A function f is comparison-free polyregular if and only if there exists some k ∈ N such that f has rank at most k. In that case, we write rk(f ) for the least such k and call it the rank of f . If (g i ) i∈I is a family of comparison-free polyregular functions,

rk(CbS(f, (g i ) i∈I )) ≤ 1 + rk(f ) + max i∈I rk(g i )
A straightforward consequence of this definition is that, just like regular functions, cfp functions are closed under regular conditionals and concatenation.

▶ Proposition 4.8. Let f, g : Γ * → Σ * be comparison-free polyregular functions and L ⊆ Γ * be a regular language. The function that coincides with f on L and with g on Γ * \ L is cfp, and so is w ∈ Γ * → f (w) • g(w); both have rank at most max(rk(f ), rk(g)).

Comparison-free pebble transducers

We now characterize our function class by a machine model that will explain our choice of the adjective "comparison-free", as well as the operational meaning of the notion of rank we just defined. It is based on the pebble transducers first introduced for trees by Milo, Suciu and Vianu [START_REF] Milo | Typechecking for XML transformers[END_REF] and later investigated in the special case of strings by Engelfriet and Maneth [19,16]. However, the definition using composition by substitution will remain our tool of choice to prove further properties, so the next sections do not depend on this one.

▶ Definition 5.1. Let k ∈ N with k ≥ 1.
Let Γ, Σ be finite alphabets and ▷, ◁ / ∈ Γ. A k-pebble stack on an input string w ∈ Γ * consists of a list of p positions in the string ▷w◁ (i.e. of p integers between 1 and |w| + 2) for some p ∈ {1, . . . , k}. We therefore write

Stack k = N 0 ∪ N 1 ∪ • • • ∪ N k ,
keeping in mind that given an input w, we will be interested in "legal" values bounded by |w| + 2.

A comparison-free k-pebble transducer (k-CFPT) consists of a finite set of states Q, an initial state q I ∈ Q and a family of transition functions

Q × (Γ ∪ {▷, ◁}) p → Q × (N p → Stack k ) × Σ * for 1 ≤ p ≤ k
where the N p on the left is considered as a subset of Stack k . For a given state and given letters (c 1 , . . . , c p ) ∈ (Γ ∪ {▷, ◁}) p , the allowed values for the stack update function N p → Stack k returned by the transition function are:

(identity) (i1, . . . , ip) → (i1, . . . , ip) ∈ N p (move left, only allowed when cp ̸ = ▷) (i1, . . . , ip) → (i1, . . . , ip -1) ∈ N p (move right, only allowed when cp ̸ = ◁) (i1, . . . , ip) → (i1, . . . , ip + 1) ∈ N p (push, only allowed when p ≤ k -1) (i1, . . . , ip) → (i1, . . . , ip, 1) ∈ N p+1 (pop, only allowed when p ≥ 1) (i1, . . . , ip) → (i1, . . . , ip-1) ∈ N p-1
(Note that the codomains of all these functions are indeed subsets of Stack k .)

The run of a CFPT over an input string w ∈ Γ * starts in the initial configuration comprising the initial state q I , the initial k-pebble stack (1) ∈ N 1 , and the empty string as an initial output log. As long as the current stack is non-empty a new configuration is computed by applying the transition function to q and to ((▷w◁)[i 1 ], . . . , (▷w◁)[i p ]) where (i 1 , . . . , i p ) is the current stack; the resulting stack update function is applied to (i 1 , . . . , i p ) to get the new stack, and the resulting output string in Σ * is appended to the right of the current output log. If the CFPT ever terminates by producing an empty stack, the output associated to w is the final value of the output log. This amounts to restricting in two ways 4 the definition of pebble transducers from [4, §2]: in a general pebble transducer, one can compare positions, i.e. given a stack (i 1 , . . . , i p ), the choice of transition can take into account whether 5 i j ≤ i j ′ (for any 1 ≤ j, j ′ ≤ p); in a "push", new pebbles are initialized to the leftmost position (▷) for a CFPT, instead of starting at the same position as the previous top of the stack (the latter would ensure the equality of two positions at some point; it is therefore an implicit comparison that we must relinquish to be truly "comparison-free"). This limitation is similar to (but goes a bit further than) the "invisibility" of pebbles in a transducer model introduced by Engelfriet et al. [18] (another difference, unrelated to position comparisons, is that their transducers use an unbounded number of invisible pebbles).

▶ Remark 5.2. Our definition guarantees that "out-of-bounds errors" cannot happen during the run of a comparison-free pebble transducer. The sequence of successive configurations is therefore always well-defined. But it may be infinite, that is, it may happen that the final state is never reached. Thus, a CFPT defines a partial function.

That said, the set of inputs for which a given pebble tree transducer does not terminate is always a regular language [START_REF] Milo | Typechecking for XML transformers[END_REF]Theorem 4.7]. This applies a fortiori to CFPTs. Using this, it is possible 6 to extend any partial function f : Γ * ⇀ Σ * computed by a k-CFPT into a total function f ′ : Γ * → Σ * computed by another k-CFPT for the same k ∈ N, such that f ′ (x) = f (x) for x in the domain of f and f ′ (x) = ε otherwise. This allows us to only consider CFPTs computing total functions in the remainder of the paper.

A special case of particular interest is k = 1: the transducer has a single reading head, push and pop are always disallowed.

▶ Theorem 5.3 ([1]).

Copyless SSTs and 1-CFPTs -which are more commonly called two-way (deterministic) finite transducers (2DFTs) -are equally expressive.

Since we took copyless SSTs as our reference definition of regular functions, this means that 2DFTs characterize regular functions. But putting it this way is historically backwards: the equivalence between 2DFTs and MSO transductions came first [17] and made this class deserving of the name "regular functions" before the introduction of copyless SSTs.

▶ Remark 5.4. There are two different numbering conventions for pebble transducers. In [4,[START_REF] Lhote | Pebble minimization of polyregular functions[END_REF], 2DFTs are 1-pebble transducers, which is consistent with our choice. However, several other papers (e.g. [START_REF] Milo | Typechecking for XML transformers[END_REF][START_REF] Engelfriet | Two-way finite state transducers with nested pebbles[END_REF]16,18,13]) consider that a 2DFT is a 0-pebble transducer (likewise, in [15], 2DFTs are 0-marble transducers). This is because they think of a pebble automaton not as a restricted multi-head automaton, but as an enriched 2DFA that can drop stationary markers (called pebbles) on input positions, with a single moving head that is not a pebble.

Let us now show the equivalence with Definition 4.2. The reason for this is similar to the reason why k-pebble transducers are equivalent to the k-nested transducers 7 of [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF], which 4 There is also an inessential difference: the definition given in [4] does not involve end markers and handles the edge case of an empty input string separately. This has no influence on the expressiveness of the transducer model. Our use of end markers follows [17,[START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]. 5 One would get the same computational power, with the same stack size, by only testing whether i j = ip for j ≤ p -1 as in [START_REF] Milo | Typechecking for XML transformers[END_REF] (this is also essentially what happens in the nested transducers of [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]). 6 Proof idea: do a first left-to-right pass to determine whether the input leads to non-termination of the original CFPT; if so, terminate immediately with an empty output; otherwise, move the first pebble back to the leftmost position and execute the original CFPT's behavior. This can be implemented by adding finitely many states, including those for a DFA recognizing non-terminating inputs. 7 Remark: nested transducers should yield a machine-independent definition of polyregular functions as the closure of regular functions under a CbS-like operation that relies on origin semantics [32, §5].

is deemed "trivial" and left to the reader in [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]Remark 6]. But in our case, one direction (Theorem 5.6) involves an additional subtlety compared to in [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]; to take care of it, we use the fact that the languages recognized by pebble automata are regular (this is also part of [START_REF] Milo | Typechecking for XML transformers[END_REF]Theorem 4.7]) together with regular conditionals (Proposition 4.8).

▶ Proposition 5.5. If f is computed by a k-CFPT, and the g i are computed by l-CFPTs, then CbS(f, (g i ) i∈I ) is computed by a (k + l)-CFPT. The hard part is to show that cfp functions are closed under composition. We exploit the following combinatorial phenomenon, often applied to the study of copyless SSTs: a copyless register assignment, i.e. an element of M cl R,∆ (cf. Section 2.4), can be specified by a "shape" described by an element of the finite monoid M cl R,∅ (Proposition 2.23), plus finitely many "labels" in Σ * (where Σ is the output alphabet) describing the constant factors that will be concatenated with the old register contents to give the new ones.

▶ Theorem 5.6. If f : Γ * → Σ * is computed by a k-CFPT, for k ≥ 2,

▶ Proposition 6.2. There is a bijection

M cl R,∆ ∼ = α, ⃗ ℓ α ∈ M cl R,∅ , ⃗ ℓ ∈ r∈R (∆ * ) |α(r)|+1
through which erase ∆ : M cl R,∆ → M cl R,∅ can be seen as simply removing the "labels" ⃗ ℓ.

Proof idea. Let β ∈ M cl R,∆ . For each r ∈ R, one can write β(r) = w 0 r ′ 1 w 1 . . . r ′ n w n with w 0 , . . . , w n ∈ ∆ * and r ′ 1 , . . . , r ′ n ∈ R such that r ′ 1 . . . r ′ n = erase ∆ (β)(r) ∈ R * . ◀
This provides a clear way to represent a copyless register assignment inside the working memory of an SST: store the shape in the state and the labels in registers. Another important fact for us is that given two assignments β, β ′ ∈ M cl R,∆ the labels of β • β ′ can be obtained as a copyless recombination of the labels of β and β ′ .

(There is a subtlety worth mentioning here: while the set of stateful transitions M cl R,∆ ≀ Q also admits a "shape + labels" representation, its monoid multiplication does not have this copylessness property. This prevents a naive proof of the closure under composition of copyless SSTs from working. Nevertheless, the composition of two regular functions is always regular, and we rely on this fact to prove Theorem 6.1.)

The rest of the proof of Theorem 6.1 is relegated to the technical appendix.

Rank vs asymptotic growth

Our next result is the comparison-free counterpart to recent work on polyregular functions by Lhote [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF], whose proof techniques (in particular the use of Ramsey's theorem) we reuse.

Compare item (ii) below to the main theorem of [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF] and item (iii) -which provides yet another definition of cfp functions -to [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]Appendix A].

▶
. , k} × Γ) * → Σ * such that f = g • cfpow (k+1) Γ
, with the following inductive definition: cfpow

(0) Γ : w ∈ Γ * → ε ∈ (∅ × Γ) * and cfpow (n+1) Γ : w → (n, w 1 ) • cfpow (n) Γ (w) • . . . • (n, w |w| ) • cfpow (n) Γ (w) To make (ii) =⇒ (i) more precise, if f is cfp with rk(f ) ≥ 1, then it admits a sequence of inputs w 0 , w 1 , . . . ∈ Γ * such that |w n | → +∞ and |f (w n )| = Ω(|w n | rk(f )+1 ).

Note that cfpow

(2) Γ and cfsquaring Γ are the same up to a bijection {0, 1} × Γ ∼ = Γ ∪ Γ. ▶ Remark 7.2. The growth of an HDT0L transduction is also related, in a very similar way to item (ii) above, to the number of layers required in any SST that computes it [15, §5].

Some proof elements

Let us present a few definitions and lemmas to give an idea of the ingredients that go into the proof. Those technical details take up the rest of this section.

Lhote's paper [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF] makes a heavy use of factorizations of strings that depend on a morphism to a finite monoid. This is also the case for our proof, but we have found that a slightly different definition of the kind of factorization that we want works better for us. ▶ Definition 7.3 (similar but not equivalent to [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]Definition 19]). An r-split of a string s ∈ Γ * according to a morphism φ : Γ * → M is a tuple (u, v 1 , . . . , v r , w) ∈ (Γ * ) r+2 such that: s = uv 1 . . . v r w with v i non-empty for all i ∈ {1, . . . , r};

φ(u) = φ(uv 1 ) = • • • = φ(uv 1 . . . v r ); φ(w) = φ(v r w) = • • • = φ(v 1 . . . v r w).
▶ Proposition 7.4 (immediate from the definition). (u, v 1 , . . . , v r , w) is an r-split if and only if, for all i ∈ {1, . . . , r}, (uv

1 . . . v i-1 , v i , v i+1 . . . v r w) is a 1-split.
The difference with the (1, r)-factorizations of [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]Definition 19] is that we have replaced the equality and idempotency requirements on φ(v 1 ), . . . , φ(v n ) by the "boundary conditions" involving φ(u) and φ(w) (actually, (1, r + 2)-factorizations induce r-splits). This change allows us to establish a subclaim used in the proof of Lemma 7.7 in an elementary way.

The point of r-splits is that given a split of an input string according to the morphism that sends it to the corresponding transition in a SST, we have some control over what happens to the output of the SST if we pump a middle factor in the split. Furthermore, it suffices to consider a quotient of the transition monoid which is finite when the SST is copyless (this is similar to Proposition 2.23). More precisely, we have the key lemma below, which is used pervasively throughout our proof of Theorem 7.1: ▶ Lemma 7.5. Let f : Γ * → Σ * be a regular function. There exist a morphism to a finite monoid ν f : Γ * → N (f ) and, for each c ∈ Σ, a set of producing triples P (f, c) ⊆ N (f ) 3 such that, for any 1-split according to

ν f composed of u, v, w ∈ Γ * -i.e. ν f (uv) = ν f (u) and ν f (vw) = ν f (w) -we have: if (ν f (u), ν f (v), ν f (w)) ∈ P (f, c), then |f (uvw)| c > |f (uw)| c ; otherwise (when the triple is not producing), |f (uvw)| c = |f (uw)| c .
Furthermore, in the producing case, we get as a consequence that ∀n ∈ N, |f (uv n w)| c ≥ n. ▶ Definition 7.6. We fix once and for all a choice of N (f ), ν f and P (f, c) for each c ∈ Σ and regular f : Γ * → Σ * . We say that a 1-split (u, v, w) is producing with respect to (f, c)

when (ν f (u), ν f (v), ν f (w)) ∈ P (f, c). For Π ⊆ Σ, we also set P (f, Π) = c∈Π P (f, c).
Something like Lemma 7.5 (but not exactly) appears in the proof of [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]Lemma 18]. We first apply it to prove the following lemma, which is morally a counterpart to the "k = 1 case" of the central Dichotomy Lemma from [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF], with r-splits instead of (k, r)-factorizations.

▶ Lemma 7.7. Let f : Γ * → Σ * be regular and φ : Γ * → M be a morphism with M finite. Suppose that π • φ = ν f for some other morphism π : M → N (f ). Let r ≥ 1 and Π ⊆ Σ.
We define L(f, Π, φ, r) to be the set of strings that admit an r-split s = uv 1 . . . v r w according to φ such that all the triples (uv 1 . . . v i-1 , v i , v i+1 . . . v r w) are producing with respect to (f, Π) -let us call this a producing r-split with respect to (f, Π, φ).

Then L(f, Π, φ, r) is a regular language, and sup{|f (s

)| Π | s ∈ Γ * \ L(f, Π, φ, r)} < ∞.
Our proof of the above lemma uses the proposition below, analogous to [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]Claim 20]. Its statement is a bit stronger than necessary for this purpose, but it will be reused in the proof of Theorem 8.3; as for its proof, this is where a standard Ramsey argument occurs. ▶ Proposition 7.8. Let Γ be an alphabet, M be a finite monoid, φ : Γ * → M be a morphism and r ≥ 1. There exists N ∈ N such that any string

s = uvw ∈ Γ * such that |v| ≥ N admits an r-split s = u ′ v ′ 1 . . . v ′ r w ′ according to φ in which u is a prefix of u ′ and w is a suffix of w ′ .
To leverage Lemma 7.7, we combine it with an elementary property of composition by substitution that does not depend on the previous technical development. (Compare the assumptions of the lemma below with the conclusion of Lemma 7.7.) ▶ Lemma 7.9. Let g : Γ * → I * be a regular function and, for each i ∈ I, let h i : Γ * → Σ * be comparison-free polyregular of rank at most k. Suppose that sup

s∈Γ * |g(s)| J < ∞ where J = {i ∈ I | rk(h i ) = k} when k ≥ 1 {i ∈ I | |h i (Γ * )| = ∞} when k = 0
(Morally, regular functions with finite range play the role of "comparison-free polyregular functions of rank -1".) Then rk(CbS(g, (h i ) i∈I )) ≤ k.

The above lemma can be compared to [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]Claim 22], but it also seems to be related to the way the "nested transducer" R k+1 is defined in the proof of the Dichotomy Lemma in [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF]: indeed, R k+1 can call either a k-nested subroutine or a (k -1)-nested one.

The remainder of the proof of Theorem 7.1 consists mainly of a rather technical induction on the rank, which we present in the appendix.

Separation results

Let us now demonstrate that the class of cfp functions is incomparable with the class of HDT0L transductions and is a strict subclass of polyregular functions.

▶ Theorem 8.1. There exist comparison-free polyregular functions which are not HDT0L: ▶ Theorem 8.3. Some HDT0L transductions are polyregular but not comparison-free:

(i) the function a n ∈ {a} * → (a n b) n+1 ∈ {a,
(i) f : a n ∈ {a} * → ba n-1 b . . . baabab (with f (ε) = ε and f (a) = b); (ii) map(a n → a n×n ) : a n1 # . . . #a n k → a n1×n1 # . . . #a n k ×n k (cf. Definition 3.8).
▶ Remark 8.4. The function a n1 # . . . #a n k → a n1×n1+•••+n k ×n k obtained by erasing the #s in the output of map(a n → a n×n ) is also not comparison-free. This result implies the second item of Theorem 8.3 by composition with the erasing morphism; we do not prove it here, but it appears in Douéneau-Tabot's aforementioned paper [13]. Therefore, according to [13], not every polyregular function with unary output is comparison-free.

To see why the first of the two functions in Theorem 8.3 is HDT0L, observe that it is Example 2.4 for Γ = {a} (taking b = a). As for the second one, combine Proposition 3.9 and the first observation in Remark 8.2.

The non-membership parts of Theorems 8.1 and 8.3 require more work. For the former, we use pumping arguments on HDT0L systems. Item (ii) of Theorem 8.3 is handled by first appealing to Theorem 7.1 to reduce to showing that map(a n → a n×n ) ̸ = CbS(g, (h i ) i∈I ) when g and all the h i are regular functions; a combination of pumping and of a combinatorial argument then shows that inputs with |I| occurrences of # suffice to discriminate the two sides of the inequality. This result also has the following consequence: ▶ Corollary 8.5. Comparison-free polyregular functions are not closed under map.

▶ Remark 8.6. Contrast with Proposition 3.9. The discussion that follows that proposition lends some significance to the above corollary: the latter rules out the obvious conjectures for a characterization of cfp functions in the style of regular/polynomial list functions.

As for item (i) of Theorem 8.3, it concerns a function whose domain consists of words over a unary alphabet, i.e., up to isomorphism, a sequence. This motivates the study of such sequences, which is the subject of the next section.

9

Comparison-free polyregular sequences ▶ Theorem 9.2. Let s : N → Σ * and k ∈ N. The sequence s is comparison-free polyregular with rk(s) ≤ k if and only if there exists p > 0 such that, for any m < p, there is a polynomial word expression e of star-height at most k + 1 such that ∀n ∈ N, s((n + 1)p + m) = e (n).

In short, the cfp sequences are exactly the ultimately periodic combinations of polypumping sequences. Our proof strategy is an induction on k.

The base case k = 0 says that regular sequences are ultimately periodic combinations of pumping sequences n → u 0 (v 1 ) n . . . (v l ) n u l . An essentially equivalent result is stated with a proof sketch using 2DFTs in [11, p. 90]; we propose an alternative proof using copyless SSTs. (Non-deterministic two-way transducers (2NFTs) taking unary inputs have also been studied [START_REF] Guillon | Input-or output-unary sweeping transducers are weaker than their 2-way counterparts[END_REF]; furthermore, the notion of "k-iterative language" that appears in a pumping lemma for general 2NFTs [39] is related to the shape of the above pumping sequences.)

To make the inductive step go through, it is enough to synchronize the periods of the different poly-pumping sequences involved and to observe that CbS( e , ( e ′ i ) i∈I ) is realized by an expression obtained by substituting the e ′ i for i in e. Coming back to Theorem 8.3, we show that a n → ba n-1 b . . . bab is not comparison-free polyregular by proving that its subsequences are not poly-pumping: for every poly-pumping sequence s : N → {a, b} * , there is a uniform bound on the number of distinct contiguous subwords of the shape baa . . . ab occuring in each s(n) for n ∈ N. Another consequence of Theorem 9.2 that we establish by induction over expressions contrasts with Corollary 8.5:

▶ Corollary 9.3. If f : Γ * → Σ * and s : N → (Γ ∪ {#}) * are cfp, so is map(f ) • s.

Further topics

Functional programming We mentioned in the introduction a forthcoming characterization of cfp functions using Church-encoded strings in a λ-calculus with linear types, in the vein of our previous results [START_REF] Thành | Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic[END_REF][START_REF] Thành | Implicit automata in typed λ-calculi II: streaming transducers vs categorical semantics[END_REF]. Meanwhile, Corollary 8.5 could be understood as negative result in the search for another kind of functional programming characterization (cf. Remark 8.6).

It is also worth noting that the copying discipline of layered SSTs is very similar to what happens in the parsimonious λ-calculus [START_REF] Mazza | Simple Parsimonious Types and Logarithmic Space[END_REF]: a datum of type !τ cannot be duplicated into two copies of the same type !τ , but it may yield an arbitrary number of copies of type τ without the modality '!'. Since the function classes defined following the methodology of [START_REF] Thành | Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic[END_REF][START_REF] Thành | Implicit automata in typed λ-calculi II: streaming transducers vs categorical semantics[END_REF] are automatically closed under composition, Theorem 3.5 leads us to conjecture that polyregular functions can be characterized in a variant of the parsimonious λ-calculus.

First-order interpretations As we already said, regular and polyregular functions both admit logical characterizations using Monadic Second-Order Logic [17,9]. The basic conceit behind these definitions is that a string w may be regarded as a finite model M(w) over a signature containing the order relation ≤ on positions and predicates encoding their labeling.

The classes obtained by replacing MSO with first-order logic (FO) are to (poly)regular functions what star-free languages are to regular languages, see [12,4]. We expect that in the same way, replacing regular functions (i.e. MSO transductions) by FO transductions in Definition 4.2 and Theorem 6.1 results in the same class in both cases, which would then be the natural FO counterpart of cfp functions. Furthermore, we believe it can be defined logically. Given a finite model U = (U, R, . . .), we write U k for the k th power (U k , R 1 , . . . , R k , . . .) where R i (x 1 , . . . , x m ) of arity m is defined as R(π i (x 1 ), . . . , π i (x m )) for 1 ≤ i ≤ k. ▶ Conjecture 10.1. A function f : Γ * → Σ * is "FO comparison-free polyregular" if and only if there exists k ∈ N and a one-dimensional FO interpretation φ such that for every w ∈ Γ * with |w| ≥ 2, there is an isomorphism of structures M(f (w)) ≃ φ M(w) k .

On an intuitive level, this seems to capture the inability to compare the positions of two heads of comparison-free pebble transducers. However, as mentioned to us by M. Bojańczyk, the naive transposition of this conjecture to MSO fails because the direct product, generalized to Henkin structures, does not preserve standard second-order models.

Integer sequences Recall from Remarks 8.2 and 8.4 that for unary outputs, polyregular and layered HDT0L transductions coincide, but comparison-free polyregular functions form a strictly smaller class (those results come from [13]). If we also restrict to unary inputs -in other words, if we consider sequences N → N -then we are fairly confident at this stage that the three classes collapse to a single one, and that this can be shown by routine methods: ▷ Claim 10.2. The classes of polyregular, comparison-free polyregular and layered HDT0L functions coincide on sequences of natural numbers.

Note that we already have a description of cfp integer sequences by specializing Theorem 9.2.

Membership and equivalence

We presented comparison-free polyregular functions as a strict subclass of polyregular functions. This leads to a natural membership problem, for which partial results were recently obtained by Douéneau-Tabot [13]: ▷ Problem 10.3. Is there an algorithm taking as input a (code for a) pebble transducer which decides whether the corresponding function Σ * → Γ * is comparison-free or not? There are many similar problems of interest on the frontier between comparison-free and general polyregular functions. We hope that investigating such issues may also lead to machine/syntax-free characterizations of the containment between the two classes.

Finally, a major open problem on polyregular functions is the equivalence problem:

▷ Problem 10.4. Is there an algorithm taking as input two pebble transducers which decides whether they compute the same function?

Interestingly, a positive answer is known for HDT0L transductions. There is an short proof using Hilbert's basis theorem [START_REF] Honkala | A short solution for the HDT0L sequence equivalence problem[END_REF], which is now understood to be an example of a general approach using polynomial grammars (see e.g. [2,5]). One could hope that a restriction to comparison-free pebble transducers also puts the equivalence problem within reach of known tools. Unfortunately, the extended polynomial grammars that would serve as the natural target for a reduction from 2-CFPT equivalence already have an undecidable zeroness problem (this was shown recently by Schmude [38]). This does not extend, however, to an undecidability proof for the CFPT equivalence problem, so the latter is still open. We recall the "natural" translation of HDT0L systems into single-state SSTs, which is relevant to some proofs in Section 3. Let (Γ, Σ, ∆, d, (h c ) c∈Γ , h ′ ) be a HDT0L system. It is equivalent to the SST specified by the following data: a singleton set of states: Q = {q}; the working alphabet as the set of registers: R = ∆ (minor technicality: if ∆ ∩ Σ ̸ = ∅, one should take R to be a copy of ∆ that is disjoint from Σ);

h c ∈ Hom(∆ * , ∆ * ) ∼ = (∆ → ∆ * ) ⊆ (∆ → (Σ ∪ ∆) * )
as the register assignment associated to an input letter c ∈ Γ -in other words, the transition function is δ : (q, c) → (q, (h c ) ↾∆ ); (h ′ (r)) r∈∆ ∈ (Σ * ) R as the initial register values;

F : q → d as the final output function (d ∈ ∆ * ⊆ (Σ ∪ ∆) *
). The cases of the transition and output functions involve a codomain extension from ∆ * to (Σ ∪ ∆) * . This reflects the intuition that a HDT0L system is the same thing as a single-state SST that "cannot access the output alphabet" (except in the initial register contents).

To prove the equivalence, the key observation is that h c is turned into δ(-, c) by a morphism from Hom(∆ * , ∆ * ) to M ∆,∅ ≀{q} ⊂ M ∆,Σ ≀{q}, using the notations from Section 2.4. We leave the details to the reader.

B Proofs for §3 (HDT0L systems, SSTs & polyregular functions)

B.1 Proof of Theorem 3.2 ▶ Theorem 3.2. For k ∈ N, a function can be computed by a k-layered SST if and only if it can be specified by a (k + 1)-layered HDT0L system. In particular, regular functions correspond to 1-layered HDT0L systems.

Proof of (⇒). The translation from SSTs to HDT0L systems given by [START_REF] Filiot | Copyful streaming string transducers[END_REF]Lemma 3.5] turns out to work. It is also formulated in terms of "simple SSTs" (isomorphic to HDT0L systems, cf. Remark 2.6) in [15, §5.1], where the authors remark that "this construction does not preserve copylessness nor k-layeredness": indeed, what we show is that it increments the number of layers by one! For the sake of clarity, we give an alternative presentation that decomposes it into two steps.

Let Γ be the input alphabet and Σ be the output alphabet. Let T be a SST with a k-layered set of register variables R = R 0 ⊔ • • • ⊔ R k . First, we build a (k + 1)-layered SST T ′ that computes the same function, with the set of registers

R ′ = Σ ∪ R = R ′ 0 ⊔ • • • ⊔ R ′ k+1 R ′ 0 = Σ ∀i ∈ {1, . . . , k + 1}, R ′ i = R i-1
assuming Σ ∩ R = ∅, and whose register assignments are without fresh letters: the range of every α ′ : R ′ → (Σ ∪ R ′ ) * is included in R ′ * , which allows us to write α ′ : R ′ → R ′ * . This already brings us closer to the definition of HDT0L systems, since (R → R * ) ∼ = Hom(R * , R * ).

Similarly, we will ensure that the range of the output function of T ′ is included in R ′ . Let underline Σ ∈ Hom((Σ ∪ R) * , (Σ ∪ R) * ) be defined in the expected way, and note that its codomain is equal to R ′ * . We specify T ′ as follows (and leave it to the reader to check that this works):

the state space Q, initial state and state transitions are the same as those of T ; the initial value of r ′ ∈ R ′ is the same as for T if r ′ ∈ R, or the single letter c if r ′ = c ∈ Σ; every assignment α : R → (Σ ∪ R) that appears in some transition of T becomes, in T ′ ,

α ′ : R ′ * → R ′ * α ′ : c ∈ Σ → c α ′ : r ∈ R → underline Σ (α(r)) its output function is F ′ = underline Σ • F where F : Q → (Σ ∪ R) *
is the output function of T . Thus, the idea is to store a copy of c ∈ Σ in the register c. Since this register may feed in a copyful way all other registers (in a SST, there are no restrictions on the use of output alphabet letters), it must sit at the lowest layer, hence R ′ 0 = Σ and the resulting offset of one layer.

Next, we turn T ′ into an equivalent HDT0L system with (k + 1)-layered working alphabet 1) , . . . , q (n) } be the states of T ′ (which are also those of T ), with q (1) being its initial state8 . Using the fact that T ′ is without fresh letters, let F ′ : Q → R ′ * be its final output function. The initial word of our HDT0L system is then

∆ = R ′ × Q = ∆ 0 ⊔ . . . ⊔ ∆ k+1 ∀i ∈ {0, . . . , k + 1}, ∆ i = R ′ i × Q For q ∈ Q, let pair q ∈ Hom(R ′ * , ∆ * ) be such that pair q (r ′ ) = (r ′ , q) for r ′ ∈ R ′ . Let Q = {q (
d = pair q (1) F ′ q (1) • . . . • pair q (n) F ′ q (n) ∈ ∆ *
From the initial register values (u I,r ′ ) r ′ ∈R ′ ∈ (Σ * ) R ′ of T ′ , we define the final morphism:

h ′ ∈ Hom(∆ * , Σ * ) ∀r ′ ∈ R ′ , h ′ r ′ , q (1) = u I,r ′ and ∀q ̸ = q (1) , h ′ (r ′ , q) = ε Finally, let δ ′ st : Q → Q and δ ′ reg : Q → (R ′ → R ′ * ) be the components of the transition function of T ′ . The morphisms h c ∈ Hom(∆ * , ∆ * ) for c ∈ Γ send (r ′ , q) ∈ ∆ to h c (r ′ , q) = pair q (i 1 ) (δ ′ reg (q (i1) , c)(r ′ )) • . . . • pair q (im) (δ ′ reg (q (im) , c)(r ′ ))
where i 1 < . . . < i m and {q (i1) , . . . , q (im) } = {q (?) ∈ Q | δ ′ st (q (?) , c) = q}. Checking that this HDT0L system computes the right function is a matter of mechanical verification, that has already been carried out in [START_REF] Filiot | Copyful streaming string transducers[END_REF]. To wrap up the proof, we must justify that it is (k + 1)-layered. To do so, let us fix a letter c ∈ Γ and two layer indices i, j ∈ {0, . . . , k + 1}, and count the number N r ′ ,q of occurrences of (r ′ , q) ∈ ∆ i among all the h c (r ′ , q) for (r ′ , q) ∈ ∆ j . The letter (r ′ , q) can only appear in h c (r ′ , q) when q = δ(q, c), and in that case, its occurrences (if any) are in the substring pair q (δ ′ reg (q, c)(r ′ )). So N r ′ ,q counts the occurrences of r ∈ R ′ i among the δ ′ reg (q, c)(r ′ ) for r′ ∈ R ′ j . Since T ′ is a (k + 1)-layered SST, we are done. ◀ Proof of (⇐). The translation from HDT0L systems to single-state SSTs mentioned in Remark 2.6 (see Appendix A) is not enough: starting from a (k + 1)-layered HDT0L system, it gives us a (k + 1)-layered SST. But we can bring this down to k layers by adding states. Let (Γ, Σ, ∆, d, (h c ) c∈Γ , h ′ ) be a HDT0L system (with d ∈ ∆ * , h c ∈ Hom(∆ * , ∆ * ) for c ∈ Γ, and h ∈ Hom(∆ * , Σ * )). Suppose that it is (k + 1)-layered with ∆ = ∆ 0 ⊔ • • • ⊔ ∆ k+1 . This entails that h c (∆ 0 ) ⊆ ∆ * 0 , and furthermore that (h c ) ↾∆0 : ∆ 0 → ∆ * 0 satisfies a copylessness condition, that may succinctly be written as (h c ) ↾∆0 ∈ M cl ∆0,∅ (cf. Definition 2.16). We define a k-layered SST with: M cl ∆0,∅ as the set of states (finite by Proposition 2.23), with the monoid identity as its initial state; the set of registers

R = ∆ \ ∆ 0 = ∆ 1 ⊔ • • • ⊔ ∆ k+1 , whose i-th layer is the (i + 1)-th layer of the original HDT0L system (0 ≤ i ≤ k); the initial register contents (h ′ (r)) r∈R -recall that h ′ is the final morphism; the transition function (α, c) → (α • (h c ) ↾∆0 , (h ′ ↾∆ * 0 • α) ⊙ • (h c ) ↾R ) where (-) ⊙ extends functions ∆ 0 → Σ * into morphisms in Hom((∆ ∪ Σ) * , (R ∪ Σ) * ) that map each letter in R ∪ Σ to itself (since ∆ = ∆ 0 ⊔ R, the domain of these morphisms is (∆ 0 ⊔ R ⊔ Σ) * ); the final output function α → (h ′ ↾∆ * 0 • α) ⊙ (d).
The layering condition for this SST is inherited is a direct consequence of the layering of the original HDT0L system, and one can check the functions computed by the two are the same. ◀

B.2 Proof of Corollary 3.3 ▶ Corollary 3.3. Every regular function can be computed by a single-state 1-layered SST.

Any regular function is definable by some copyless SST, i.e. 0-layered SST. By Theorem 3.2, it can be turned into a 1-layered HDT0L system. The latter can be translated to a single-state SST by the construction of Appendix A. As can readily be seen from the definitions, this construction preserves the 1-layered property.

B.3 Proof of Proposition 3.7

▶ Proposition 3.7. The sequential (and therefore regular) function defined by the transducer of Figure 2 (Section 2.2) cannot be computed by a single-state copyless SST.

Consider any single-state copyless SST computing some g : {a, b, c} * → {a, b} * with a set of registers R. We wish to show g does not coincide with the function computed by the sequential transducer of Figure 2. Let ω ∈ ({a, b} ∪ R) * be the image of the single state by the output function, and for x ∈ {a, b, c}, let α x : R → ({a, b} ∪ R) * be the copyless assignment performed by the SST when it reads x (that is, using the notations of Definition 2.3, ω = F (q) and α x = δ reg (q, x) with Q = {q}). Let ⃗ u be the initial register contents. Then

∀x ∈ {a, b, c} * , ∀n ∈ N, g(x • c n ) = ω † • (α † c ) n • α † x (⃗ u)
Any register assignment β : R → ({a, b, c} ∪ R) * admits a unique extension into a monoid morphism β □ ∈ Hom(({a, b, c} ∪ R) * , ({a, b, c} ∪ R) * ) that maps every letter in {a, b, c} to itself. Let ω n = α □ c n (ω) (so that ω 0 = ω). One can check that, for all n ∈ N:

ω † n = ω † • (α † c ) n ; since α c is copyless, |ω n | r ≤ |ω| r for all r ∈ R, writing |w| x for the number of occurrences of x in w ∈ Σ * for x ∈ Σ. Let (v x,r ) r∈R = α †
x (⃗ u) for x ∈ {a, b, c}; that is, v x,r the value stored in the register r ∈ R after the SST has read the single letter x. We can rewrite the above equation as

∀x ∈ {a, b, c} * , ∀n ∈ N, g(x • c n ) = ω † n ((v x,r ) r∈R )
and derive a numerical (in)equality

∀x ∈ {a, b, c} * , ∀n ∈ N, |g(x • c n )| a = |ω n | a + r∈R |ω n | r |v x,r | a = n→+∞ |ω n | a + O(1)
using the fact that |ω n | r , as a non-negative quantity lower than the constant |ω| r , is O(1).

From this, it follows that as n increases, the difference between |g(a • c n )| a and |g(b • c n )| a stays bounded. This property distinguishes g from the f : {a, b, c} * → {a, b} * computed by the transducer given in Figure 2, since It is stated in the introduction to [4] that all regular functions are polyregular. One way to see this is discussed in Section 5: the characterization by pebble transducers given in [4] generalizes the classical definition of regular functions using two-way finite state transducers. This takes care of one direction of the equivalence; for the converse, observe that: sequential functions are regular, as already mentioned; since the SST of Example 2.10 is copyless, the iterated reverse function is regular.

∀n ∈ N, |f (a • c n )| a = a n+1 a = n + 1 and |f (b • c n )| a = b n+1 a = 0

B.5 Proof of Theorem 3.5

▶ Theorem 3.5. Let f : Γ * → Σ * . The following are equivalent: (i) f is polyregular;

(ii) f can be obtained as a composition of layered SSTs;

(iii) f can be obtained as a composition of single-state 1-layered SSTs.

Proof of (i) ⇒ (iii). Thanks to Proposition 3.4, we know that any polyregular functions can be written as a composition of a sequence of functions, each of which is either regular or equal to squaring Γ for some finite alphabet Γ. It suffices to show that each function in the sequence can in turn be expressed as a composition of single-state 1-layered SSTs. We decompose squaring Γ as

1234 → 4321321211 → 1234123412341234
The first step is performed by the SST of Example 2.4, which has a single state and, as mentioned in Section 2.3, is 1-layered. The second step can be implemented using a SST with a single state q (that we omit below for readability), two registers X (at layer 0) and Y (at layer 1) with empty initial values, an output function F (q) = Y , and

∀c ∈ Γ, δ(c) = (X → X, Y → cY ) and δ(c) = (X → cX, Y → cXY )
As for regular functions, Corollary 3.3 takes care of them. ◀

Proof of (iii) ⇒ (ii). Immediate by definition. ◀

Proof of (ii) ⇒ (i). All functions computed by k-layered SSTs are polyregular; this applies in particular to single-state 1-layered SSTs. Therefore, their composition is also polyregular (according to Definition 2.11, polyregular functions are closed under composition). ◀ B.6 Proof of Proposition 3.9

▶ Proposition 3.9. If f is an HDT0L transduction, then so is map(f ). For each k ≥ 1, the functions that can be computed by k-layered HDT0L systems are also closed under map.

Let (Γ, Σ, ∆, d, (h c ) c∈Γ , h ′ ) be a HDT0L system computing f : Γ * → Σ * . We define below a HDT0L system that computes map(f ) :

(Γ ∪ {#}) * → (Σ ∪ {#}) * . The intermediate alphabet is ∆ = ∆ ∪ Σ ∪ {#, X}, assuming w.l.o.g. that # / ∈ ∆ ∪ Σ, where X / ∈ ∆ ∪ Σ ∪ {#} is an arbitrarily chosen fresh letter. The starting word is Xd ∈ ∆ * . For c ∈ Γ, we extend h c into h c ∈ Hom(∆ * , ∆ * ) by setting h c (x) = x for x ∈ Σ ∪ {#, X}.
Since the input alphabet is now Γ ∪ {#}, we also define the morphism h # as the extension of h ′ (using

Σ ⊂ ∆) such that h # (X) = Xd# and h # (x) = x for x ∈ Σ ∪ {#}. The final morphism h ′ extends h ′ with h ′ (X) = ε and h ′ (x) = x for x ∈ Σ ∪ {#}
This shows that HDT0L transductions are closed under map.

We now prove that for any k ∈ N ≥1 , this closure property holds for k-layered HDT0L transductions (so, in particular, for regular functions by taking k = 1). Suppose that f is computed by a k-layered HDT0L system with intermediate alphabet ∆ and initial word d ∈ ∆ * . One can build a k-layered HDT0L system which computes the same function f and such that the initial word contains at most one occurrence of each letter; the idea is to replace ∆ and d = d 1 . . . d n by ∆ × {1, . . . , n} and (d 1 , 1), . . . , (d n , n) where n = |d|, and to adapt the morphisms accordingly. Applying the above construction then results in a k-layered HDT0L system that computes map(f ); note that if we did not have this property for the inital word, we would get a (k + 1)-layering instead. We start by briefly recalling the definition of polynomial list functions from [4, Section 4]. The explanation is geared towards a reader familiar with the simply typed λ-calculus, which this system extends. The λ-terms defining polynomial list functions are generated by the grammar of simply typed λ-terms enriched with constants, whose meaning can be specified by extending the β-rule. For instance, given a finite set S and a ∈ S, every element of S can be used as a constant, another allowed constant is is S a and we have

C

is S a b = β true if a = b is a b = β false if b ∈ S \ {a}
The grammar of simple types and the typing rules are also extended accordingly. For instance, any finite set S induces a type also written S, such that every element a ∈ S corresponds to a term a : S of this type. There are also operations expressing the cartesian product (×)

and disjoint union (+) of two types; and, for any type τ , there is a type τ * of lists whose elements are in τ . So the constant is S a receives the type is S a : S → {true} + {false} for any finite set S See [4, Section 4] for the other primitive operations that are added to the simply typed λ-calculus; we make use of is, case, map and concat here. Bojańczyk's result is that if Γ and Σ are finite sets, then the polynomial list functions of type Γ * → Σ * correspond exactly the polyregular functions.

▶ Lemma C.1. Let I = {i 1 , . . . , i |I| }.
Then the function match I,τ : I → τ → . . . → τ → τ which returns its (k + 1)-th argument when its 1st argument is i k is a polynomial list function.

Proof idea. By induction on |I|, using is I i (i ∈ I) and case {true},{false},τ . ◀ Proof of closure by CbS. Let f : Γ * → I * , and for i ∈ I, g i : Γ * → Σ * be polyregular functions. Assuming that f and g i (i ∈ I) are defined by polynomial list functions of the same name, the λ-term λw. concat Σ (map

I,Σ * (λi. match I,Σ * i (g i1 w) . . . (g i |I| w)) (f w))
computes CbS(f, (g i ) i∈I ). ◀

C.2 Proof of Proposition 4.7

▶ Proposition 4.7. A function f is comparison-free polyregular if and only if there exists some k ∈ N such that f has rank at most k. In that case, we write rk(f ) for the least such k and call it the rank of f . If (g i ) i∈I is a family of comparison-free polyregular functions,

rk(CbS(f, (g i ) i∈I )) ≤ 1 + rk(f ) + max i∈I rk(g i )
This is equivalent to claiming that the smallest class C of functions such that every regular function is in C, and CbS(f, (g i ) i∈I ) ∈ C for any regular f : Γ * → I * and any (g i : Γ * → Σ * ) i∈I ∈ C I , contains all comparison-free polyregular functions. It suffices to show that C is closed under composition by substitution, which can be done by induction using the equation

CbS(CbS(f, (g i ) i ), (h j ) j ) = CbS(f, (CbS(g i , (h j ) j )) i )
The same equation explains the inequality on the rank that we claim in the proposition.

C.3 Proof of Proposition 4.8

▶ Proposition 4.8. Let f, g : Γ * → Σ * be comparison-free polyregular functions and L ⊆ Γ * be a regular language. The function that coincides with f on L and with g on Γ * \ L is cfp, and so is w ∈ Γ * → f (w) • g(w); both have rank at most max(rk(f ), rk(g)).

Closure under regular conditionals

We first observe that the particular case where f and g are both regular (rk(f ) = rk(g) = 0) already appears in the literature [1]. We shall use it in further appendices, so let us state it as a stand-alone lemma.

▶ Lemma C.2 ([1, Proposition 2]). Let f, g : Γ * → Σ * be regular functions and L ⊆ Γ * be a regular language. The function that coincides with f on L and with g on Γ * \ L is regular.

With this in hand, let us turn to the general case where f, g : Γ * → Σ * are cfp. It means that we have regular functions f ′ and g ′ , as well as families of functions (f ′′ i ) i∈I and (g ′′ j ) j∈J such that

f = CbS(f ′ , (f ′′ i ) i∈I ) and g = CbS(g ′ , (g ′′ j ) j∈J )
(if f (or g) is of rank 0, we can introduce a spurious CbS by taking f ′ (resp. g ′ ) to be a constant function outputting a single letter over the singleton alphabet). Assume without loss of generality that I ∩ J = ∅. Using Lemma C.2 applied to f ′ , g ′ : Γ * → (I ∪ J) * , there is a function h ′ : Γ * → (I ∪ J) * coinciding with f ′ over L and g ′ over L \ Γ * . Setting (h ′′ k ) k∈I∪J to be the family of functions such that h ′′ i = f ′′ i for i ∈ I and h ′′ j = g ′′ j for j ∈ J, we obtain a cfp function h = CbS(h ′ , (h ′′ k ) k∈I∪J ) corresponding to the desired conditional.

Closure under concatenation Similarly, first observe that the result holds for regular functions. Using SSTs, this can be shown using a product construction. Then, taking regular functions f ′ and g ′ , as well as families of functions (f ′′ i ) i∈I and (g ′′ j ) j∈J so that f = CbS(f ′ , (f ′′ i ) i∈I ) and g = CbS(g ′ , (g ′′ j ) j∈J ) with I and J disjoint as above, one check that the pointwise concatenation First note that any k-CFPT can be transformed into an equivalent k-CFPT whose transition functions δ :

f • g is equal to CbS(f ′ • g ′ , (h ′′ k ) k∈I∪J ), which is cfp since f ′ • g ′ is regular.
Q × (Γ ∪ {▷, ◁}) p → Q × (N p → Stack k ) × Σ * are
such that, for every input (q, ⃗ b), we have either π 3 (δ(q, ⃗ b)) = ε (in which case we call δ(q, ⃗ b) a silent transition) or π 3 (δ(q, ⃗ b)) ∈ Σ and π 2 (δ(q, ⃗ b)) is the identity. So, without loss of generality, suppose that we have a k-CFPT T f implementing f is of this shape, with state space Q f and transition function δ f Similarly, we may assume without loss of generality that the current height of the stack is tracked by the state of CFPTs if we allow multiple final states; assume that we have such height-tracking l-CFPT and that we have l-CFPTs T i implementing g i with state spaces Q i and transition functions δ i .

We combine these CFPTs into a single k + l CFPT T ′ with state space

Q ′ = Q f ⊔ Q f × i∈I Q i
The initial and final states are those of T f . The high-level idea is that T ′ behaves as T f until it produces an output i ∈ I; in such a case it "performs a call" to T i that might spawn additional heads to perform its computations. At the end of the execution of T i , we return the control to T f . Formally speaking, the transition function δ ′ of T ′ behaves as follows:

δ ′ (q, ⃗ b) = δ f (q, ⃗ b) if q ∈ Q f and δ f (q, ⃗ b) is silent.
otherwise we take, we have π 3 (δ f (q, ⃗ b)) = i for some i ∈ I. Calling r i the initial state of T i , we set π 1 (δ ′ (q, ⃗ b)) = (q, r i ) and π 2 (δ ′ (q, ⃗ b)) corresponds to push a new pebble onto the stack. We make δ ′ (q, ⃗ b) silent in such a case. δ ′ ((q, r), ⃗ b ⃗ b ′ ) then corresponds to δ i (r, ⃗ b ′ ) if we are not in the situation where the stack height is 1 and the stack update function is pop.

otherwise we take π 1 (δ ′ ((q, r), ⃗ bb ′ )) = π 1 (δ f (q, ⃗ b)), π 2 (δ ′ (q, n + 1, ⃗ bb ′ )) to be a pop action and π 3 (δ ′ ((q, r), ⃗ bb ′ )) = π 3 (δ i ((q, r), ⃗ bb ′ )).

D.2 Proof of Theorem 5.6

▶ Theorem 5.6. If f : Γ * → Σ * is computed by a k-CFPT, for k ≥ 2, then there exist a finite alphabet I, a regular function h : Γ * → I * and a family (g i ) i∈I computed by (k -1)-CFPTs such that f = CbS(h, (g i ) i∈I ).

Assume we have f : Γ * → Σ * computed by a k-CFPT T with state space Q and transition function δ that we assume to be disjoint from Σ. For each q ∈ Q, we describe a k -1 CFPT T q with the same state space, initial state q and transition function δ q such that, for every b ′ ∈ N, ⃗ b ∈ Stack l for l ≤ k -1 and q ′ ∈ Q, δ(q ′ , b ′⃗ b) and δ q (q ′ , ⃗ b) coincide on the first and last component; on the second component, we require they also coincide up to the difference in stack size. If we fix r ∈ Q, by [START_REF] Milo | Typechecking for XML transformers[END_REF]Theorem 4.7], the language consisting of those w ∈ Γ * such that T q halts on r is regular. Since regular languages are closed under intersection, for any map γ ∈ Q Q , the language L γ ⊆ Γ * of those words w such that T q halts on γ(q) is regular.

Now fix γ ∈ Q Q and let us describe a 1-CFPT transducer T γ intended to implement the restriction of a function h : Γ * → (Σ ∪ Q) * to L γ . T γ has the same state space and initial state as T , but has a transition function δ γ defined by

δ γ (q, b) = δ(q, b) if π 2 (δ(q, b)) is not a push (γ(r), (p → p), r) otherwise, for r = π 1 (δ(q, b)) Since Γ * = γ∈Q Q L γ ,
by applying repeatedly Lemma C.2, this determines the regular function h : Γ * → (Σ ∪ Q) * . We can then check that f = CbS(h, (g i ) i∈Σ∪Q ) where g a is the constant function outputting the one-letter word a for a ∈ Σ (which can certainly be implemented by a 1-CFPT) and g q is the function Γ * → Σ * implemented by the (k -1)-CFPT T q .

D.3 Proof of Corollary 5.7

▶ Corollary 5.7. For all k ∈ N, the functions computed by (k + 1)-CFPTs are exactly the comparison-free polyregular functions of rank at most k.

The proof goes by induction over k ∈ N. By Theorem 5.3, the result holds for k = 0 since 2DFTs characterize regular functions; let us detail each direction of the inductive case k > 0:

for the left-to-right inclusion, assume we are given a (k + 1)-CFPT computing f and apply Theorem 5.6 to obtain h and g i s such that f = CbS(h, (g i ) i∈I ) with h regular and the g i s computable by k-CFPTs. The induction hypothesis implies that the g i s have rank < k, and thus f has rank ≤ k. conversely, if f has rank k, it can be written as CbS(h, (g i ) i∈I ) with h regular and the g i s with rank < k; the induction hypothesis implies that the g i s can be computed by k-CFPTs. By Theorem 5.3, h is computable by a 1-CFPT, so by Proposition 5.5, f is computed by a (k + 1)-CFPT

▶ Theorem E.1. Comparison-free polyregular functions are closed under composition.

First, by induction on the rank of the left-hand side of the composition, we can reduce to the case where that side is a mere regular function, using the straightforward identity

CbS(f, (g i ) i∈I ) • h = CbS(f • h, (g i • h) i∈I )
We then treat this case by another induction, this time on the rank of the right-hand side. The base case is handled by invoking the closure under composition of regular functions. Therefore, what remains is the following inductive case.

▶ Lemma E.2. Let f : Γ * → I * be a regular function and let (g i ) i∈I be a family of comparisonfree polyregular functions Γ * → Σ * . Suppose that for all regular h : Σ * → ∆ * and all i ∈ I, the composite h • g i is comparison-free polyregular.

Then, for all regular h : Σ

* → ∆ * , h • CbS(f, (g i ) i∈I
) is comparison-free polyregular.

Our proof of the above lemma and related subclaims rely on the properties of transition monoids introduced in Section 2.4 and on the combinatorics of register transitions discussed in the paragraphs following Proposition 6.2.

▶ Lemma E.3. Let δ be the transition function of some copyless SST Σ * → ∆ * whose sets of states and registers are Q and R respectively, so that δ (-, c) ,c)

∈ M cl R,∆ ≀ Q for c ∈ Σ. Let ψ δ ∈ Hom(Σ * , M cl R,∆ ≀ Q) such that ∀c ∈ Σ, ψ δ (c) = δ(-
and φ δ = erase ∆ • ψ δ as in Remark 2.22, q ∈ Q, r ∈ R, α ∈ M cl R,∅
and j ∈ {0, . . . , |α(r)|}. Then the following function Σ * → ∆ * , defined thanks to Proposition 6.2, is regular:

s → w j where π 2 (ψ δ (s)(q))(r) = w 0 r ′ 1 w 1 . . . r ′ n w ′ n if π 2 (φ δ (s)(q)) = α ε otherwise (recall that π 2 : Q × M → M is the second projection and M ≀ Q = Q → Q × M ).
Proof. We consider during this proof that the names q, r, α and j introduced in the above statement are not in scope, so that we can use those variable names for generic elements of Q, R, M cl R,∅ and N instead. Those data will be given other names when we need them. We build a copyless SST whose set of states is Q × M cl R,∅ . This is made possible by the finiteness of M cl R,∅ (Proposition 2.23). As for the set of registers, we would like it to vary depending on the current state for the sake of conceptual clarity, i.e. to have a family of finite sets indexed by Q × M cl R,∅ ; when the SST moves from state (q, α) to (q ′ , α ′ ), it would perform a register assignment from R q,α to R q ′ ,α ′ (described by a map R q ′ ,α ′ → (∆ ∪ R q,α ) * ). Such devices have been called state-dependent memory copyless SSTs in [START_REF] Thành | Implicit automata in typed λ-calculi II: streaming transducers vs categorical semantics[END_REF], and they are clearly equivalent in expressive power to usual copyless SSTs.

The idea is that we want the configuration (current state plus register contents) of our new SST, after reading s = s 1 . . . s n , to faithfully represent

ψ δ (s)(q 0 ) = (δ(-, s 1 ) • • • • • δ(-, s n ))(q 0 ) ∈ Q × M cl R,∆
where δ and ψ δ are given in the lemma statement, and q 0 is the given state that was called q in that statement. Following Proposition 6.2, since we already have the "shape" stored in the second component M cl ∆,∅ of the set Q × M cl ∆,∅ of new states, it makes sense to use the register to store the "labels", hence R q,α = R α with

R α = {(r, j) | r ∈ R, j ∈ {0, . . . , |α(r)|}} so that (∆ * ) Rα ∼ = r∈R (∆ * ) |α(r)|+1
The configurations of our SST are thus in bijection with Q × M cl R,∆ via Proposition 6.2, and we would like the transition performed when reading c ∈ Σ to correspond through this bijection to (using the notations of Definition 2.3)

(q, β) ∈ Q × M cl R,∆ → (δ st (q), β • δ reg (q)) For a fixed β ′ ∈ M cl R,∆ , let us consider the right multiplication β → β • β ′ in M cl R,∆ . Since erase ∆ : M cl R,∆ → M cl R,
∅ is a morphism, the "shape" of β • β ′ can be obtained from the "shape" of β by multiplying by α ′ = erase ∆ (β ′ ). The important point is to show that we can obtain the new labels from the old ones by a copyless assignment -formally speaking, that for any α ∈ M cl R,∆ there exists a copyless

γ α,β ′ : R α•α ′ → (∆ ∪ R α ) * such that for any β ∈ M cl R,∆ such that erase ∆ (β) = α, which therefore corresponds to α, ⃗ ℓ for some ⃗ ℓ ∈ (∆ * ) Rα ∼ = r∈R (∆ * ) |α(r)|+1
the shape-label pair that corresponds to β

• β ′ is (α • α ′ , γ † α,β ′ ( ⃗ ℓ)) (cf. Definition 2.2). Our next task is to analyze the composite assignment β • β ′ in order to derive a γ α,β ′ that works. Let r ′′ ∈ R. First, if α ′ (r ′′ ) = r ′ 1 . . . r ′ n ∈ R * , then β ′ (r ′′ ) = w ′ 0 r ′ 1 w ′ 1 . . . r ′ n w ′ n for some w ′ 0 , . . . , w ′ n ∈ ∆ *
and by applying the unique morphism β ⊙ ∈ Hom((∆ ∪ R) * , (∆ ∪ R) * ) that extends β and sends letters of ∆ to themselves, we have

(β • β ′ )(r ′′ ) = β ⊙ (β ′ (r)) = w ′ 0 • β(r ′ 1 ) • w ′ 1 • . . . • β(r ′ n ) • w ′ n
Let us decompose further, for i ∈ {1, . . . , n}: Furthermore, each w k for k ∈ {0, . . . , m} is a concatenation of some w ′ i and some w i,j , and from the formal expression of w k depending on these w ′ i and w i,j -which only depends on the shape α and α ′ -we can derive a definition of γ α,β ′ (r ′′ , k). For instance,

β(r ′ i ) = w i,0 r i,
w 42 = w 3,2 w ′ 3 w 4,0 ⇝ γ(r ′′ , 42) = (r ′ 3 , 2) • w ′ 3 • (r ′ 4 , 0) ∈ (∆ ∪ R α•α ′ ) *
Observe that this does not refer to the w i,j ; therefore, γ α,β ′ does not depend on β, as required.

One can check that defined this way, γ α,β ′ is indeed a copyless assignment and that the desired property of γ † α,β ′ holds. What we have just seen is the heart of the proof. We leave it to the reader to finish the construction of the copyless SST. ◀

With this done, we can move on to proving Lemma E.2, which suffices to finish the proof of Theorem E.1.

Proof of Lemma E.2. Let w ∈ Γ * be an input string. In the composition, we feed to a copyless SST T h that computes h the word CbS(f, (g i ) i∈I )(w) = g i1 (w) . . . g i k (w) where f (w) = i 1 . . . i k . A first idea is therefore to tweak T h into a new copyless SST that takes I * as input and which executes, when it reads i ∈ I, the transition of T h induced by g i (w). If we call h ′ w the regular function computed by this new SST, we would then have h ′ w (f (w)) = h • CbS(f, (g i ) i∈I )(w). The issue is of course that h ′ w depends on the input w. More precisely, the data that h ′ w depends on is the family of transitions

(ψ δ • g i (w)) i∈I ∈ (M cl R,∆ ≀ Q) I (see Lemma E.3 for ψ δ )
where Q, R and δ are respectively the set of states, the set of registers and the transition function of T h . We will be able to disentangle this dependency by working with

(φ δ • g i (w)) i∈I = (erase ∆ • ψ δ • g i (w)) i∈I ∈ (M cl R,∅ ≀ Q) I
Concretely:

▷ Claim E.4. For each ⃗ µ ∈ (M cl R,∅ ≀ Q) I ,
: Σ * → ∆ * for λ ∈ Λ; such that for i 1 . . . i n ∈ I * and w ∈ Γ * , if (φ δ • g i (w)) i∈I = ⃗ µ, then h(g i1 (w) • . . . • g in (w)) = replace each λ ∈ Λ ⃗ µ in h ′′ ⃗ µ (i 1 . . . i n ) by l λ • g ι(λ) (w)
Proof. Proposition 6.2 says that every β = ψ δ (g i (w)) ∈ M cl R,∆ can be decomposed into a shape α = erase ∆ (β) ∈ M cl R,∅ and a finite family ⃗ ℓ of strings in ∆ * . Each β(r) for r ∈ R can then be reconstituted as an interleaving of letters in α(r) with labels in ⃗ ℓ, a process that can be decomposed into two steps: first, interleave the letters of α(r) with placeholder letters, taken from an alphabet disjoint from both ∆ and R; then substitute the labels for those letters. Roughly speaking, this will allow us to manipulate an assignment with placeholders without knowing the labels, and then add the labels afterwards.

Let ⃗ µ ∈ (M cl R,∅ ≀ Q) I . We define a copyless SST T ⃗ µ with the same sets of states and registers as T h , namely Q and R. Its initial register values and final output function are also the same. It computes a function I * → (∆ ∪ Λ ⃗ µ ) * , and its transition function is

δ ⃗ µ : (q, i) → π 1 • µ i (q), r → interleave λ q,i,r 0 . . . λ q,i,r |π2(µi(q))(r)| , π 2 (µ i (q))(r)
where interleave(u 0 . . .

u n , v 1 . . . v n ) = u 0 v 1 u 1 . . . v n u n for letters u 0 , . . . , u n , v 1 , . . . , v n over some alphabet (recall also that µ i : Q → Q × M cl R,∅ for i ∈ I)
. Thus, we take

Λ ⃗ µ = λ q,i,r j q ∈ Q, i ∈ I, r ∈ R, j ∈ {0, . . . , |π 2 (µ i (q))(r)|} ι(λ q,i,r j ) = i
and h ′′ ⃗ µ to be the function computed by T ⃗ µ . (Note that although δ ⃗ µ does not involve letters from ∆, the final output function and the initial register contents do.) Finally, given λ = λ q,i,r j ∈ Λ ⃗ µ , we define l λ to be the regular function provided by Lemma E.3 for the transition function δ of T h , the state q 0 (which is the initial state of both T h and T ⃗ µ ), the register r, the assignment shape α = π 2 (µ i (q)) and the position j ∈ {0, . . . , |α(r)|}.

F.1 Proofs for the lemmas in Section 7

Recall that the notion of r-split has been defined in Definition 7.3. ▶ Lemma 7.5. Let f : Γ * → Σ * be a regular function. There exist a morphism to a finite monoid ν f : Γ * → N (f ) and, for each c ∈ Σ, a set of producing triples P (f, c) ⊆ N (f ) 3 such that, for any 1-split according to ν f composed of u, v, w ∈ Γ * -i.e. ν f (uv) = ν f (u) and ν f (vw) = ν f (w) -we have:

if Proof idea. We reuse an idea from [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF], but instead of using transition monoids of two-way transducers, we rely on monoids of copyless register assignments. We shall use the notations introduced in Section 2.4 for these monoids and the operations they support.

(ν f (u), ν f (v), ν f (w)) ∈ P (f,
Let R and Σ be finite alphabets. First, we factor erase Σ :

M cl R,Σ → M cl R,∅ into two surjective morphisms M cl R,Σ → M cl01 R,Σ → M cl R,∅
, going through a new monoid which keeps some information about the letters of Σ but is still finite. To do so, we define an equivalence relation on register assignments as follows: for α, β ∈ M cl R,Σ , we say that α ∼ β when erase Σ (α) = erase Σ (β); for each r ∈ R, the sets of letters from Σ that appear in α(r) and β(r) are equal. One can show that ∼ is a congruence, so we may form the quotient monoid M cl01 R,Σ = M cl R,Σ / ∼. Thanks to the first clause in the definition of ∼, the morphism erase Σ factors through the canonical projection. The quotient is finite since each equivalence class has a representative α such that |α(r)| ≤ |R| + |Σ| for all r ∈ R: essentially, ∼ only takes into account the presence or absence of each letter in Σ, not their multiplicity (hence the notation "01").

Next, let f : Γ * → Σ * be computed by some copyless SST (Q, q 0 , R, δ, ⃗ u I , F ). We take

N (f ) = M cl01 R,Σ ≀ Q and define ν f as a composition Γ * → M cl R,Σ ≀ Q → N (f )
where the first morphism -which we may call ψ δ , as in Lemma E.3 -maps c ∈ Γ to δ(-, c) and the second morphism is the canonical projection.

What we need to show now is that, given a 1-split (u, v, w) ∈ (Γ * ) 3 with respect to ν f , the comparison between |f (uvw)| and |f (uw)| depends only on ν f (x) for x ∈ {u, v, w}.

Let q ′ and ⃗ u ′ I be the state and register values of the SST after reading u; to be more formal, ψ δ (u)(q 0 ) = (q ′ , α) and α † (⃗ u I ) = ⃗ u ′ I . Note that q ′ is also the first component of the pair ν f (u)(q 0 ); since ν f (uv) = ν f (u) (by definition of 1-split), the SST reaches the state q ′ after reading uv as well:

ψ δ (q ′ , v) = (q ′ , β) for some β ∈ M cl R,Σ . Let ψ δ (w)(q ′ ) = (q ′′ , γ). Then f (uvw) = F (q ′′ ) † • (β • γ) † (⃗ u ′ I ) f (uw) = F (q ′′ ) † • γ † (⃗ u ′ I ) Since ν f (vw) = ν f (w), we have erase Σ (β • γ) = erase Σ (γ). Therefore, ω = (β • γ) ⊙ (F (q ′′ ))
and ω ′ = γ ⊙ (F (q ′′ )) have the same letters from R with the same multiplicities (and appearing in the same order, although this does not matter for us here): |ω| r = |ω ′ | r for all r ∈ R. This is why the two sums over R cancel out in the following computation (writing

⃗ u ′ I = (u ′ r ) r∈R ): ∀c ∈ Σ, |f (uvw)| c -|f (uw)| c = |ω † (⃗ u ′ I )| c -|(ω ′ ) † (⃗ u ′ I )| c = |ω| c + r∈R |ω| r • |u ′ r | c -|ω ′ | c - r∈R |ω ′ | r • |u ′ r | c = |ω| c -|ω ′ | c
where β k is not raised to the n-th power in the middle; the left inequality comes from Lemma F.3, while the right inequality is part of the induction hypothesis applied to h i . The case of g requires an additional step. We know that (α 0 β 1 . . . β k-1 α k-1 , β k , α k ) is a producing triple with respect to (g ′ , i, χ); therefore, by Lemma 7.5,

∀n ∈ N, |g ′ (α 0 β 1 . . . β k-1 α k-1 β n k α k )| i ≥ n
To replace g ′ by g in the above inequality, recall that by definition of g ′ , since i ∈ J,

∀s ′ ∈ Γ * , (|g ′ (s ′ )| i ̸ = 0 =⇒ |g ′ (s ′ )| i = |g(s ′ )| i )
One can then conclude by Proposition F.5 below, taking l = k -1. There is a subtlety here: our definitions ensure that ν g factors through ψ i , but this might not be the case for ν g ′ (because ψ i had to be defined before g ′ ). So for this final step, we must work with the function g, whereas to leverage the producing triple, we had to use g ′ . ◀

The following proposition, which we used at the end of the above proof, will also be useful to prove Theorem 8.3. ▶ Proposition F.5. Let g : Γ * → Σ * be a regular function and s = α 0 β 1 α 1 . . . β l α l ∈ Γ * such that every triple (α 0 β 1 . . . α m , β m+1 , α m+1 β m+2 . . . α l ) is a 1-split according to ν g . Then for every c ∈ Σ, the function

(n 1 , . . . , n l ) → |g(α 0 β n1 1 α 1 . . . β n l l α l )| c
is monotone according to the product partial order on N l .

Proof idea. In order to apply Lemma 7.7, the key observation is that the triple

(α 0 β n1 1 . . . α m β nm+1 m+1 , β m+1 , α m+1 β nm+2 m+2 . . . α l )
is also a 1-split. This is because we have, by definition of 1-split, ν g (α 0 β n1 1 ) = ν g (α 0 β 1 ), then ν g (α 0 β 1 α 1 β n2

2 ) = ν g (α 0 β 1 α 1 β 2 ), etc., and similarly on the right side. ◀

After having established Lemma F.4, we can use it to finally wrap up this section.

Proof of Theorem F.1. We apply Lemma F.4 to get a language L(f, φ, rk(f ) + 1) where φ does not matter (take for instance the morphism from Γ * to the trivial monoid). It must be non-empty (or else we would have the contradiction rk(f ) < rk(f )), so we can choose an arbitrary element s

∈ L(f, φ, rk(f ) + 1). Let k = rk(f ) + 1. Lemma F.4 gives us k factorizations s = u (m) v (m) 1 . . . v (m)
k w (m) satisfying certain properties. Note that k plays two roles here that were distinct in the lemma. We claim that thanks to this, there exists a factorization s = α 0 β 1 α 1 . . . β k α k as described in Lemma F.4. This entails that setting s n = α 0 β n 1 α 1 . . . β n k α k proves the theorem. Our task is therefore to select one element in each of the k sets {v (m) l | l ∈ {1, . . . , k}} of substrings of s for m ∈ {1, . . . , k}, such that the selected substrings are pairwise nonoverlapping. There is a strategy for this which is similar to the classical greedy algorithm for computing a maximum independent set in an interval graph. We take β 1 to be the substring of s among the v (m) 1 whose right endpoint is leftmost. One can check that β 1 cannot overlap with any v (m) l for l ≥ 2. Thus, by discarding the set to which β 1 belongs, as well as each v (m) 1 in the other sets, we reduce the remainder of the task to our original goal with k being decremented by 1. At this stage, an induction suffices to conclude the proof. ◀ G Proofs of Theorems 6.1 and 7.1

Now that we have shown that cfp functions are closed under composition and that their asymptotic growth are tightly linked to their ranks, we have the essential ingredients to prove Theorems 6.1 and 7.1. There are a couple of preliminary lemmas helpful for both that we first prove here.

▶ Lemma G.1. For any comparison-free polyregular function f : Γ * → Σ * and k ≥ rk(f ), there exists a regular function f

′ : ({0, . . . , rk(f )} × Γ) * → Σ * such that f = f ′ • cfpow (k+1) Γ
.

Proof. By induction on rk(f ) (with an inductive hypothesis that quantifies over k). Inductive case. Let f = CbS(g, (h i ) i∈I ) with g : Γ * → I * regular and h i : Γ * → Σ * cfp such that rk(h i ) ≤ rk(f ) -1 for all i ∈ I. Using the inductive hypothesis, we know that

Base case (f regular

h i = h ′ i • cfpow (k)
Γ for some family of regular functions (h ′ i ) i∈I . Thus, let us assume we are given 2DFTs T and (T ′ i ) i∈I corresponding to g and the family (h ′ i ) i∈I . Without loss of generality, let us assume further that T always output at most one letter at each transition, never outputs a letter upon reading ◁, and that the T i always terminate on the marker ▷ by a transition that does not move the reading head. With these assumptions, let us describe informally a 2DFT T ′′ corresponding to the function f ′ such that CbS(g, (h

′ i •cfpow (k) Γ ) i∈I ) = f ′ • CbS(g, (h ′ i ) i∈I ) • cfpow (k+1) Γ
. Assuming that the state space of T is Q and the state space of T ′ i is Q ′ i , with Q and the Q ′ i s all pairwise disjoint, we take the state space of T ′′ to be

Q ′′ = Q × {L, R, S} × {•} ⊔ i∈I Q ′ i × {L, R, S}
with initial state (q 0 , R, •), if q 0 is the initial state of T and final states the triples (q f , M, •) such that q f is a final state of T . To guide intuitions, the elements L, R and S should be respectively read as "left", "right" and "stay". With this in mind, the high-level description of computations carried out by T ′′ over words pow

Γ is as follows. When in a state (q 0 , M, •), T ′′ essentially acts as T on letters of the shape (k, a) or end-markers and ignores letters (l, a) for l < k; the central component M then determines whether to seek the next relevant position to the left or to the right when reading such an irrelevant letter. This continues up until upon reading a letter (k, a) in state (q, M, •) such that T would ouput i when reading a in q, T ′′ moves into the state (r, M ′ , (q ′ 0,i , R)) where q ′ 0,i is the initial state of T ′ i and (r, M ′ ) is determined by the transition in T . When in a state (q, M, (q ′ i , M ′ )) for q ′ i ∈ Q ′ i , T behaves exactly as T i as long as the current transition does not reach the final state, treating letters outside of its input alphabets as end markers; this is possible because of the component M ′ of the state, that we use to keep track of the last move of the reading head. Meanwhile the components q ∈ Q and M are untouched. When a final transition is taken, by our assumption we return control to T by going to state (q, M, •) and moving in the direction prescribed by M (recall that, by assumption, we are moving away from (or staying in) the position at which T i started running).

We leave formalizing this definition and checking that T ′′ has a desirable behaviour to the reader. ◀ ▶ Lemma G.2. For every k ∈ N, cfpow

Γ is equal to a a composition of sequential functions and squaring functions cfsquaring ∆ .

Proof. We proceed by induction over k. The cases of k = 0, 1, 2 are immediate as cfpow (k) Γ then corresponds, up to isomorphism of output alphabet, to a constant function, the identity and cfsquaring Γ respectively, so we focus on the inductive step. To achieve the desired result, it suffices to show that there exists a sequential function To make (ii) =⇒ (i) more precise, if f is cfp with rk(f ) ≥ 1, then it admits a sequence of inputs w 0 , w 1 , . . . ∈ Γ * such that |w n | → +∞ and |f (w n )| = Ω(|w n | rk(f )+1 ).

We now treat the case where β(r) is non-empty. By definition, β • β = β * • β where β * ∈ Hom(R * , R * ) extends β : R → R * . Since we know, as a consequence of the idempotency of µ •m , that β • β = β, we have β * (β(r)) = β(r) ̸ = ε. Let us study in general the situation β * (ρ) = β(r) ̸ = ε for ρ ∈ R * . A first observation is that the letters in β(r) cannot be found in any other β(r ′ ) for r ′ ∈ R \ {r} because β is copyless, so ρ / ∈ (R \ {r}) * . We therefore have n ≥ 1 occurrences of r in ρ, so ρ = ρ 0 r . . . rρ n with ρ 0 , . . . , ρ n / ∈ (R \ {r}) * . By coming back to β * (ρ) = β(r), into which we plug this expression for ρ, and using the fact that β(r) has non-zero length, we can see that n = 1 and β * (ρ 0 ) = β * (ρ 1 ) = ε. Let us apply this to ρ = β(r) = erase Σ (γ)(r) and lift the result to γ(r): γ(r) = u r rv r for some u r , v r ∈ (Σ ∪ β -1 ({ε})) *

In the previous case (β(r ′ ) = ε for r ′ ∈ R), we saw that γ(β -1 ({ε})) ⊆ Σ * . Therefore γ ⊙ (u r ), γ ⊙ (v r ) ∈ Σ * , where γ ⊙ ∈ Hom((Σ ∪ R) * , (Σ ∪ R) * ) extends γ : R → (Σ ∪ R) * by being the identity on Σ. Since Σ * is fixed by γ ⊙ , when we iterate, we obtain

γ •(n+1) (r) = (γ ⊙ ) n • γ(r) = (γ ⊙ (u r )) n • u r rv r • (γ ⊙ (v r )) n
Now, let F be the final output function of the SST that computes f , and ⃗ w m+k be the register values after it has read a prefix a m+k . Then after reading a m(n+1)+k , the new register values are (γ •(n+1) ) † ( ⃗ w m+k ). More precisely, the register r contains:

γ(r) ∈ Σ * if β(r) = ε; (γ ⊙ (u r )) n • ((u r rv r ) † ( ⃗ w m+k )) • (γ ⊙ (v r )
) n otherwise. These values are combined by F (q) † -where q is the recurrent state we have been working with all along, and F is the final output function -to produce the output f (a m(n+1)+k ). This yields the desired shape: an interleaved concatenation of finitely many factors that are either constant, (γ ⊙ (u r )) n or (γ ⊙ (v r )) n for some r ∈ R. ◀ Proof of Theorem 9.2. We proceed by induction on the rank of the sequence s : N → Σ * under consideration. If the rank of s is 0, it is regular and we apply Lemma H.1 and the desired polynomial word expression is of the shape u 0 • (v 1 ) * . . . (v l ) * • u l .

If the rank of s is k + 1, thanks to the induction hypothesis and the base case above, it can be written as CbS( e , ( e ′ i ) i∈I ) where e is an expression over the alphabet I with star-height at most one and the e ′ i s expressions over Σ with star-height at most k. Without loss of generality, we may assume that that terminal nodes of polynomial word expressions are words of length at most one. For such an expression over alphabet I, one may define inductively the following substitution operation to obtain an expression of Σ * : We first prove the result for poly-pumping sequences.

j[(e ′ i ) i∈I ] = e ′ j ε[(e ′ i ) i∈I ] = ε (f • f ′ )[(e ′ i ) i∈I ] = f [(e ′ i ) i∈I ] • f ′ [(e ′ i ) i∈I ] f * [(e ′ i ) i∈I ] = (f [(e ′ i ) i∈I ]) *
▶ Lemma H.2. If e : N → (Γ ∪ {#}) * is a poly-pumping sequence and f : Γ * → Σ * is comparison-free polyregular, then map(f ) • e is a cfp sequence.

For the rest of this subsection, we write S for the successor function n → n + 1 over N. We will use the fact that s is a cfp sequence iff s • S also is.

Proof. We first note that if the separator # does not occur at any leaf of e, then the result is immediate as we would have map(f ) • e = f • e . We thus focus on the cases when it does occur, and proceed inductively over e.

If e = w ∈ (Γ ∪ {#}) * , then map(f ) • e is a constant sequence, which is obviously cfp.

If e = (e ′ ) * , with # occuring in e ′ , let h l , h r : N → Γ * and h c : N → (Γ ⊔ {#}) * be the sequences such that

e ′ • S • S = h l • # • h c • # • h r
with h l (n) being the largest #-free prefix of e ′ (n + 2) and h r (n) the largest #-free suffix of e ′ (n + 2). There is a regular function

f ′ : (Γ ⊔ {#}) * → (Γ ⊔ {#}) *
w 0 #w 1 # . . . w n-1 #w n → w 1 # . . . w n-1 (w 0 , . . . , w n ∈ (Γ ⊔ Γ) * ) stripping away the first and last component of its input, so that it satisfies

f ′ • map(f ) • e ′ • S • S = map(f ) • h c
By the inductive hypothesis, we know that map(f ) • e ′ is comparison-free polyregular. We may therefore conclude by composition (cf. Theorem 6.1) that map(f ) • h c is cfp. One can check analogously that h l and h r are also cfp. Then observe that

( e • S • S)(n) = (h l • # • h c • # • h r )(n) n+2 = (h l • (# • h c • # • h r • h l ) n+1 • # • h c • # • h r )(n)
which means that we have

map(f ) • e • S • S =                  (f • h l ) • (# • (map(f ) • hc) • # • (f • (hr • h l ))) * • # • (map(f ) • hc) • # • (f • (hr • h l )) • # • (map(f ) • hc) • # • (f • hr)
Thanks again to the closure under composition, each component of this expression is cfp, so map(f ) • e • S • S is also cfp. Hence, so is map(f ) • e . The last case where e = e ′ • e ′′ is handled similarly after a case analysis determining whether # occurs only in e ′ , e ′′ or in both; we leave it to the reader. ◀

Figure 1

 1 Figure 1 Summary of the known relationships between superlinear transduction classes, taking our results into account. Inclusions ⊂ are strict, and ⊃ ⊂ means that there is no inclusion either way. Finally C * denotes the composition closure of the class C.

Figure 2

 2 Figure 2 An example of sequential transducer.

  Theorem 7.1. Let f : Γ * → Σ * and k ∈ N. The following are equivalent: (i) f is comparison-free polyregular with rank at most k; (ii) f is comparison-free polyregular and |f (w)| = O(|w| k+1 ); (iii) there exists a regular function g : ({0, . .

From

  now on, we identify N with the set of words {a} * and freely speak, for instance, of cfp sequences N → Γ * instead of cfp functions {a} * → Γ * . It turns out that cfp sequences admit a characterization as finite combinations of what we call poly-pumping sequences. ▶ Definition 9.1. A poly-pumping sequence is a function of the form e : N → Σ * where e is a polynomial word expression generated by e ::= w | e • e ′ | e * where w ∈ Σ * ; w (n) = w, e • e ′ (n) = e (n) e ′ (n) and e * (n) = ( e (n)) n . The star-height of a polynomial word expression is defined in the usual way.

B. 4 ▶

 4 Proof of Proposition 3.4 Proposition 3.4. Polyregular functions are the smallest class closed under composition that contains the regular functions and the squaring with underlining functions squaring Γ .

▶

  Theorem 4.4. Polyregular functions are closed under composition by substitution.

▶

  Proposition 5.5. If f is computed by a k-CFPT, and the g i are computed by l-CFPTs, then CbS(f, (g i ) i∈I ) is computed by a (k + l)-CFPT.

  c), then |f (uvw)| c > |f (uw)| c ; otherwise (when the triple is not producing), |f (uvw)| c = |f (uw)| c . Furthermore, in the producing case, we get as a consequence that ∀n ∈ N, |f (uv n w)| c ≥ n.

  ). Consider the unique φ ∈ Hom(({0, . . . , rk(f )} × Γ) * , Γ * ) such that for every c ∈ Γ, φ(k, c) = c and φ(m, c) = ε when m < k. Since regular functions are closed under composition, f ′ = f • φ is regular, and the desired equation follows from the fact that φ • cfpow (k+1) Γ = id Γ * .

f▶Γ

  : (({0, . . . , k} × Γ) ∪ ({0, . . . , k} × Γ)) * → ({0, . . . , k + 1} × Γ) * such that cfpow (k+1) Γ = f • cfsquaring {0,...,k}×Γ • cfpow (k+1) Γ. In fact, the sequential transducer pictured below computes such an f :o i (k, a) | (k + 1, a) (k, a) | (k, a) (m, a) | (m, a) (m, a) | ε (m, a) | ε (k, a) | ε (m, a) | ε (k, a) | (k + 1, a) ε εwhere m designates any element of {0, . . . , k -1}. ◀Now we turn to the proofs of our main theorems.▶ Theorem 6.1. The class of comparison-free polyregular functions is the smallest class closed under usual function composition and containing both all regular functions and the functions cfsquaring Γ (cf. Example 4.3) for all finite alphabets Γ.Proof of Theorem 6.1. The direct implication is obtained by combining the two lemmas above: every cfp function can be written as a composition f • cfpow(k)Γ for some k ∈ N and f regular by Lemma G.1, and Lemma G.2 guarantees that in turn, cfpow (k) Γ is a composition of sequential (and a fortiori regular) functions and squarings. Conversely, that cfp functions are closed under composition is proven in Appendix E, which is enough to conclude as regular functions and cfsquaring Γ are cfp. ◀ Theorem 7.1. Let f : Γ * → Σ * and k ∈ N. The following are equivalent: (i) f is comparison-free polyregular with rank at most k; (ii) f is comparison-free polyregular and |f (w)| = O(|w| k+1 ); (iii) there exists a regular function g : ({0, . . . , k} × Γ) * → Σ * such that f = g • cfpow : w ∈ Γ * → ε ∈ (∅ × Γ) * and cfpow (n+1) Γ : w → (n, w 1 ) • cfpow

  • . . . • (n, w |w| ) • cfpow

  One can then check by induction on the structure of e that e[(e ′ i ) i∈I ] = CbS( e , ( e ′ i ) i∈I ) and that e[(e ′ i ) i∈I ] has star-height bounded by k + We finally show that cfp sequences are closed by post-composing with functions map(f ) for f cfp. ▶ Corollary 9.3. If f : Γ * → Σ * and s : N → (Γ ∪ {#}) * are cfp, so is map(f ) • s.

Proof of Corollary 9. 3 .

 3 Suppose we are given f : Γ * → Σ * and s : N → (Γ ∪ {#}) * cfp. By Theorem 9.2, s is an ultimately periodic combination of poly-pumping sequences, so that there are m > 0 and some expressions e 0 , . . . , e m-1 such that s(m(n+ 1) + k) = e k (n) for every k < m. By Lemma H.2, every map(f ) • e k is cfp. The set L k = {m(n + 1) + k | n ∈ N} is semi-linear, i.e., corresponds to a regular language, and there are regular sequences r k : N → N such that r k (m(n + 1) + k) = n. Further, N = {n | n < m} ∪ k<m L k , so we may use the regular conditional provided by Proposition 4.8 to show that the combination of the map(f ) • e k • r k and the first m values of map(f ) • s, which corresponds exactly to map(f ) • s, is indeed cfp. ◀

shall use the name erase Σ for both morphisms (R and Q being inferred from the context).

	▶ Remark 2.22. Consider an SST with a transition function δ. Let φ δ ∈ Hom(Γ * , M cl R,∅ ≀Q) be
	defined by φ δ (c) = erase Σ (δ(-, c)) for c ∈ Γ. The range φ δ (Γ * ) is precisely the substitution
	transition monoid (STM) defined in [12, Section 3].
	▶ Proposition 2.23. For any finite R, the monoid M cl R,∅ is finite. As a consequence, the
	substitution transition monoid of any copyless SST is finite.
	Proof idea. For all α ∈ M cl R,∅ and r ∈ R, observe that |α(r)| ≤ |R|.	◀
	3

Complements on HDT0L systems, SSTs and polyregular functions

  Let us transpose the layering condition from SSTs to HDT0L systems. The hierarchy of models that we get corresponds with an offset to layered SSTs.

	Layered HDT0L systems ▶ Definition 3.1. A HDT0L system (Γ, Σ, ∆, d, (h c ) c∈Γ , h ′ ) is k-layered if its working alphabet
	can be partitioned as ∆ = ∆ 0 ⊔ • • • ⊔ ∆ k such that, for all c ∈ Γ and i ∈ {0, . . . , k}:
	for r ∈ ∆ i , we have h c (r) ∈ (∆ 0 ⊔ • • • ⊔ ∆ i ) * ;
	each letter in ∆ i appears at most once among all the h c (r) for r ∈ ∆ i (but those in
	∆ 0 ⊔ • • • ⊔ ∆ i-1 may appear an arbitrary number of times).
	▶ Theorem 3.2. For k ∈ N, a function can be computed by a k-layered SST if and only if it
	can be specified by a (k + 1)-layered HDT0L system.
	Before embarking on the study of our new comparison-free polyregular functions, we state
	some minor results that consolidate our understanding of pre-existing classes.

Proposition 3.4. Polyregular

  By applying some results from [4], we can state a variant of Definition 2.11 which is a bit more convenient for us. functions are the smallest class closed under composition that contains the regular functions and the squaring with underlining functions squaring Γ .

	▶ This allows us to show that composing HDT0L transductions with at most polynomial
	growth yields the polyregular functions. One direction of this equivalence is proved by
	encoding squaring Γ as a composition of two SSTs, one of which is Example 2.4. More
	precisely:
	▶

Theorem 3.5. Let f : Γ * → Σ * . The following are equivalent: (i) f is polyregular; (ii) f can be obtained as a composition of layered SSTs; (iii) f can be obtained as a composition of single-state 1-layered SSTs. But layered SSTs by themselves are strictly less expressive than polyregular functions, as we shall see later in Theorem 8.1. Therefore, as promised in the introduction: ▶ Corollary 3.6 (

  claimed in [15, Section 6]). Layered SSTs are not closed under composition.

  then there exist a finite alphabet I, a regular function h : Γ * → I * and a family (g i ) i∈I computed by (k -1)-CFPTs such that f = CbS(h, (g i ) i∈I ).

	▶ Corollary 5.7. For all k ∈ N, the functions computed by (k + 1)-CFPTs are exactly the
	comparison-free polyregular functions of rank at most k.
	6	Composition of basic functions

Another possible definition of cfp functions consists in swapping out squaring Γ for some other function in Proposition 3.4: ▶ Theorem 6.1. The class of comparison-free polyregular functions is the smallest class closed under usual function composition and containing both all regular functions and the functions cfsquaring Γ (cf. Example 4.3) for all finite alphabets Γ.

  b} * for a ̸ = b; (ii) the function w ∈ Σ * → w |w| for |Σ| ≥ 2 (a simplification of Example 4.3);(iii)(from [15, §6]) the cfp functions that map a n #w ∈ Σ * to (w#) n for a, # ∈ Σ, a ̸ = #. ▶ Remark 8.2. The first example in[15, §5] shows that a n → a n×n is HDT0L (via the equivalent model of marble transducers), hence the necessity of |Σ| ≥ 2 above. More generally, Douéneau-Tabot has shown very recently that every polyregular function with unary output alphabet is HDT0L[13]. So polyregular functions with unary output coincide with polynomial growth N-rational series (cf. Remark 2.14), and the latter admit several algebraic characterizations in the literature (see[36] and [3, Chapter 9, Exercise 1.2]).

G Proofs of Theorems 6.1 and 7.1 42 H Comparison-free polyregular sequences 44

  H.1 Proof of Theorem 9.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 H.2 Proof of Corollary 9.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Proof of Theorem 8.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 I.2 Proof of Theorem 8.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 I.2.1 Proof of Theorem 8.3 item (i) . . . . . . . . . . . . . . . . . . . . . . . 48 I.3 Proof of Theorem 8.3 item (ii) . . . . . . . . . . . . . . . . . . . . . . . . . . 49

	I Separation results	47
	I.1 A	Details for Remark 2.6

  1 w i,1 . . . w i,ni r ni for some w i,0 , . . . , w i,ni ∈ ∆ * By plugging this into the previous equation, we have (β • β ′ )(r ′′ ) = w 0 r 1 w 1 . . . r m w m where {r 1 , . . . , r m } =

	n
	{r i,1 , . . . , r i,ni }
	i=1

Rajeev Alur and Pavol Černý. Expressiveness of streaming string transducers. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS

[START_REF] Berstel | Noncommutative Rational Series with Applications[END_REF], December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 1-12. Schloss Dagstuhl -Leibniz-Zentrum fürInformatik, 2010. doi:10.4230/LIPIcs.FSTTCS.2010.1.

Except for that, this enumeration of Q is arbitrary. We write q (i) instead of q i to avoid confusion with the run of an automaton.

Comparison-free Polyregular Functions

This section is dedicated to establishing the following theorem, which constitutes most of the work that goes into proving Theorem 6.1.

Comparison-free Polyregular Functions

Let w ∈ Γ * be such that (φ δ • g i (w)) i∈I = ⃗ µ. Consider χ w ∈ Hom((∆ ∪ Λ ⃗ µ ) * , ∆ * ) which maps each letter of ∆ to itself and each λ ∈ Λ ⃗ µ to l λ • g ι(λ) (w). It lifts to a morphism χ w ∈ Hom(M cl R,∆∪Λ ⃗ µ , M cl R,∆ ), and we have χ w (δ ⃗ µ (-, i)) = ψ δ • g i (w). This leads to the following invariant: the configuration of T h after reading g i1 (w) • . . . • g in (w) is, in a suitable sense, the "image by χ w " of the configuration of T ⃗ µ after reading i 1 . . . i n . (In other words, the "image of the SST T ⃗ µ by χ w " is the copyless SST computing h ′ w that we sketched at the very beginning of this proof of Lemma E.2.) This directly implies the property relating h, h ′′ ⃗ µ and (l λ ) λ∈Λ ⃗ µ that we wanted. ◁

Let us finish proving Lemma E.2 using the fact we just proved. First of all, since the letters of Λ ⃗ µ only serve as placeholders to be eventually substituted, they can be renamed at our convenience. That means that we can take the Λ ⃗ µ to be disjoint for ⃗ µ ∈ (M cl R,∅ ≀ Q) I , and define Λ to be their disjoint union. We also take ι : Λ → I to be the unique common extension of the ι ⃗ µ . In the same spirit, we glue together the functions h ′′ ⃗ µ • f into

From the above equation on h ′′ ⃗ µ , one can then deduce for all w ∈ Γ * without condition that h(CbS(f, (g i ) i∈I )(w)) = CbS(H, (l λ • g ι(λ) ) λ∈Λ )(w)

(strictly speaking, one should have a family indexed by ∆ ∪ Λ on the right-hand side -to comply with that, just extend the family with constant functions equal to x for each x ∈ ∆).

Using the above equation, we can rephrase our goal: we want to prove that the function CbS(H, (l λ •g ι(λ) ) λ∈Λ ) is comparison-free polyregular. This class of functions is -by definition -closed under composition by substitution, so we can reduce this to the following subgoals:

H is comparison-free polyregular: in fact, it is regular, because regular functions are closed under composition and regular conditionals (Lemma C.2). This argument relies on the finiteness of the indexing set (M cl R,∅ ≀ Q) I -a consequence of Proposition 2.23 -and on the regularity of the language {w ∈ Γ * | (φ δ • g i (w)) i∈I = ⃗ µ} for any ⃗ µ. The reasons for the latter are as follows:

φ δ is a morphism whose codomain M cl R,∅ ≀ Q is finite, so φ -1 δ ({µ i }) is regular for i ∈ I; the functions g i for i ∈ I are assumed to be comparison-free polyregular, so they preserve regular languages by inverse image, as all polyregular functions do [4]; regular languages are closed under finite intersections, and I is finite. l λ • g ι(λ) is comparison-free polyregular for all λ ∈ Λ: because our main existence claim states that l λ is regular for all λ ∈ Λ, and one of our assumptions is that any g i (for i ∈ I) postcomposed with any regular function gives us a comparison-free polyregular function.

◀

F

A lower bound on growth from the rank

In this section, we prove a statement that directly implies the last claim of Theorem 7.1:

Let us start by proving the lemmas stated in the main text which this theorem depends on.

Comparison-free Polyregular Functions

From now on, let c ∈ Σ. From the definition of β ⊙ , we have

So we get the dichotomy of the lemma statement: if there exists some

For each r ∈ R, the condition |ω ′ | r > 0 can be checked from q ′ and ν f (w); in turn, q ′ depends only on ν f (u). As for |β(r)| c > 0, since it is a condition on the presence or not of a certain letter from Σ in β(r), without considering its precise multiplicity, it depends only on ν f (v): this is the information that ν f was designed to encode. This gives us the definition of the set of producing triples P (f, c).

There remains a final claim to prove in the lemma statement, concerning |f (uv n w)| c when (u, v, w) ∈ P (f, c) and n ∈ N. Using µ(uv) = µ(u), one can show that for all m ∈ N, the triple (uv m , v, w) is also a producing 1-split. So we have

and since all elements of this sequence are natural numbers, |f (uv n w)| c ≥ n. ◀

Next, we prove Proposition 7.8 before Lemma 7.7, following the order of logical dependency.

▶ Proposition 7.8. Let Γ be an alphabet, M be a finite monoid, φ : Γ * → M be a morphism and r ≥ 1. There exists N ∈ N such that any string

and w is a suffix of w ′ . Proof. By the finite Ramsey theorem for pairs, there exists R ∈ N such that every complete undirected graph with at least R vertices whose edges are colored using |M | colors contains a monochromatic clique with r + 3 vertices. We take N = R -1.

Let s = uvw ∈ Γ * with |v| ≥ N . Let us write s[i . . . j] for the substring of s between two positions i, j ∈ {0, . . . , |s|}. Those indices are considered as positions in-between letters, so, for instance, s = s[0 . . . |s|], while s[(i -1) . . . i] is the i-th letter of s; note also that s

Consider the following coloring of the complete graph over V = {|u|, . . . , |uv|}: the edge (i, j) ∈ V 2 with i < j is given the color φ(s[i . .

We now define u ′ = s[0 . . . i 1 ] and w ′ = s[i r+1 . . . |s|], which ensures that u is a prefix of u ′ and w is a suffix of w ′ since i 1 and i r+1 are positions in v. For m ∈ {1, . . . , r}, we also take

). Thus, by definition, we have an r-split of s. ◀ ▶ Lemma 7.7. Let f : Γ * → Σ * be regular and φ : Γ * → M be a morphism with M finite. Suppose that π • φ = ν f for some other morphism π : M → N (f ). Let r ≥ 1 and Π ⊆ Σ.

We define L(f, Π, φ, r) to be the set of strings that admit an r-split s = uv 1 . . . v r w according to φ such that all the triples (uv 1 . . . v i-1 , v i , v i+1 . . . v r w) are producing with respect to (f, Π) -let us call this a producing r-split with respect to (f, Π, φ).

Then L(f, Π, φ, r) is a regular language, and sup{|f (s

Proof. L(f, Π, φ, r) can be recognized by a non-deterministic automaton that guesses an adequate r-split and computes φ(u), φ(v 1 ), . . . , φ(v r ), φ(w). The hard part is showing that |f (-)| Π is bounded on the complement of this language. By the previous proposition, there exists some N ∈ N such that any string s ∈ Γ * of length at least N admits an r-split according to φ. Thanks to the existence of π, it is also an r-split according to ν f . So if this long string is in Γ * \ L(f, Π, φ, r), then it is of the form s = uv 1 . . . v r w where, for some i ∈ {1, . . . , r}, (uv

The important part is that the argument in the left-hand side is strictly shorter (the definition of r-split contains v i ̸ = ε). Furthermore, we claim that

Once this is established, a strong induction on the length suffices to show that |f (-)| Π restricted to Γ * \ L(f, Π, φ, r) reaches its maximum at some string of length smaller than N , and thus to conclude the proof.

It remains to show that s ′ / ∈ L(f, Π, φ, r). If this were false, then by definition we would have a producing r-split s

Assuming this, we will lift this split to a producing r-split of s in order to contradict s / ∈ L(f, Π, φ, r). We give notations to the components of our non-producing triple: û

Suppose that for some j ∈ {1, . . . , r} and x ∈ Γ * , we have û

Combining the above with the fact that (u ′ , v ′ 1 , . . . , v ′ r , w ′ ) is an r-split of s ′ gives us directly from the definitions that our new (r + 2)-tuple with xvy is an r-split of s. Finally, we must check that it is producing.

Let k ≤ j -1. We must show that (u

) is producing with respect to (f, Π). We have seen previously that the componentwise image by φ of this triple is the same as the one for (u

). The latter is producing (since it comes from an r-split chosen to be producing), and therefore so is the former, because thanks to ν f = π • φ, the image by φ suffices to determine whether a triple is producing.

It would be convenient if xvy and v ′ j had the same image by φ, but this is not guaranteed. Instead, we come back to the dichotomy concerning what happens when we remove the substring xvy in s. This can be done in two steps: first remove v in s, which gives us s ′ , then remove

This means that the 1-split containing xvy must be producing. If the (j, x) chosen previously does not exist, then either u ′ is a prefix of û or w ′ is a suffix of ŵ. In those cases, there is an analogous lifting procedure, and its proof of correctness is simpler; we leave this to the reader. ◀ ▶ Remark F.2. It is not clear whether the above reasoning can be made to work if we require idempotency in the definition of r-split. An analogous argument is made in the first paragraph of the proof of the original Dichotomy Lemma in [START_REF] Lhote | Pebble minimization of polyregular functions[END_REF], but we were unable to

Comparison-free Polyregular Functions

check that s ′ / ∈ L(f, Π, φ, r) when forcing the central elements of producing triples to be idempotent. Thankfully it does not seem to be required to carry out further arguments leading to a proof of Theorem F.1. ▶ Lemma 7.9. Let g : Γ * → I * be a regular function and, for each i ∈ I, let h i : Γ * → Σ * be comparison-free polyregular of rank at most k. Suppose that sup

(Morally, regular functions with finite range play the role of "comparison-free polyregular functions of rank -1".) Then rk(CbS(g, (h i ) i∈I )) ≤ k.

Proof. We write f = CbS(g, (h i ) i∈I ).

First, let us consider the case k = 0. For convenience, we assume w.l.o.g. that I ∩ Σ = ∅.

Let N = sup{|g(s)| J | s ∈ Γ * } -in the degenerate case J = ∅, this leads to N = 0 -and ι n (s) be the n-th letter of J in g(s) if it exists, or else ε. Then we use the equation g(s) = ρ 0 (s)ι 1 (s)ρ 1 (s) . . . ι N (s)ρ N (s) to define uniquely ρ 0 , . . . , ρ N : Γ * → (I \ J) * . One can build for each n ∈ {0, . . . , N } a sequential transducer whose composition with g yields ρ n ; therefore, since g is regular, so is ρ n . We define ψ n (s) next as h ιn(s) (s) when ι n (s) ∈ J, and ε otherwise.

For any n ∈ {1, . . . , N }, since the languages g -1 (((

defined is regular by closure under concatenation (use a product construction on copyless SSTs). Observe that f ′ (s) is obtained by substituting each occurrence of a letter i ∈ J in g(s) by h i (s) (thus, it is equal to g(s) when J = ∅, and to f (s) when J = I).

What remains to do is to substitute the letters of I \ J to get f . To do so, let us define

The function f coincides on L ⃗ w with f ′ postcomposed with the morphism that replaces each i ∈ I \ J by w i ; this is regular by closure under composition. Furthermore, the factors of i∈I\J h i (Γ * ) are finite by definition of J, and I \ J itself is a subset of the finite alphabet I. So there are finitely many L ⃗ w , and they partition Σ * ; they are also all regular, as finite intersections of preimages of singletons by regular functions. Therefore, f is obtained by combining regular functions by a regular conditional, so it is regular, i.e. rk(f ) = 0 as we wanted.

This being done, let us move on to the case

) where all the g ′ i are regular and the h ′ i,x are of rank at most k -1, choosing the X i to be pairwise disjoint as well as disjoint from I. Let f ′ (s) be obtained from g(s) by substituting each occurrence of a letter i ∈ J by g ′ i (s). For the same reasons as those exposed in the first paragraph of the case k = 0, this defines a regular function f ′ . By taking its composition by substitution with the disjoint union of the families (h i ) i∈I\J and (h ′ i,x ) x∈Xi for i ∈ J, we recover f . Since the functions involved in this union family are all of rank at most k -1 (by definition of J), this means that rk(f ) ≤ k. ◀

F.2 Wrapping up the proof of Theorem F.1

▶ Lemma F.3. Let f : Γ * → Σ * be comparison-free polyregular. There exists a morphism to a finite monoid ν ′ f : Γ * → N ′ (f ) such that, for any 1-split according to ν ′ f composed of u, v, w ∈ Γ * and any c ∈ Σ * , the sequence (|f (uv n w)| c ) n∈N is non-decreasing.

Proof. By straightforward induction on rk(f ), using Lemma 7.5: for f = CbS(g, (h i ) i∈I ) where g is regular and the h i are comparison-free, we take

a comparison-free polyregular function. Let φ : Γ * → M be a morphism to a finite monoid and let r ≥ 1. Then there exists a regular language L(f, φ, r) ⊆ Γ * such that: the function which maps L(f, φ, r) to ε and coincides with f on Γ * \ L(f, φ, r) is regular and takes finitely many values if rk(f ) = 0 i.e. f is regular; is comparison-free polyregular with rank strictly lower than rk(f ) otherwise; for any s ∈ L(f, φ, r), there exist k = rk(f ) + 1 r-splits according to φ -let us write them as

r w (m) for m ∈ {1, . . . , k} -such that, for any factorization s = α 0 β 1 α 1 . . . β k α k where, for some permutation σ of {1, . . . , k}, each β m coincides with some v (σ(m)) l (in the sense that their positions as substrings of s are equal), we have

(note that in general, such factorizations s = α 0 β 1 α 1 . . . β k α k might not exist, for instance when r = 1 and all the substrings v (m) 1

overlap)

Proof. We proceed by induction on rk(f ).

Base case: rk(f ) = 0. In this case, f is regular. Let ψ : Γ * → M × N (f ) be the monoid morphism obtained by pairing φ (given in the lemma statement) with ν f (given in Lemma 7.7).

Then, using Lemma 7.7, one can see that taking L(f, φ, r) = L(f, Σ, ψ, r) works.

Inductive case: rk(f ) ≥ 1. In this case, f = CbS(g, (h i ) i∈I ) for some regular g : Γ * → I * and some comparison-free polyregular h i : Γ * → Σ * with rk(h i ) ≤ rk(f ) -1 for all i ∈ I. Let φ and r be as given in the lemma statement. Let J be defined as in Lemma 7.9:

be obtained by combining φ with the morphisms given by Lemmas 7.5 and F.3. We shall consider the regular languages L(h i , ψ i , r) provided by the inductive hypothesis.

Let us take a copy J = {i | i ∈ J} of J such that J ∩ I = ∅. We define the regular function g ′ : Γ * → (I ∪ J) * as follows: for any input s ∈ Γ * , to build the output g ′ (s), we start from g(s) and then, for each i ∈ J such that s / ∈ L(h i , ψ i , r), we replace all the occurrences of i by i. For i ∈ J, we also define h i to be the function which maps L(h i , ψ i , r) to ε and coincides with

Note that g ′ is regular: it is indeed generated from g using regular conditionals and postcomposition by letter-to-letter morphisms. We can therefore build a morphism

in the expected way, and define the language provided by the lemma statement as

According to Lemma 7.7, it is indeed a regular language. Concerning the first item of the lemma statement, the function that it considers can be expressed as

where

We want to show that rk(CbS(g ′′ , (h i ) i∈I∪J )) ≤ rk(f ) -1. The shape of this statement fits with the conclusion of Lemma 7.9, so we just have to check the corresponding assumptions. g ′′ is regular, by closure of regular functions under regular conditionals. for i ∈ I ∪ J, the function h i is comparison-free polyregular of rank at most rk(f ) -1: for i ∈ I, this was required in our choice of expression for f = CbS(g, (h i ) i∈I ) (and such a choice was possible by definition of rank); for i = j ∈ J, we get this by applying the first item of the inductive hypothesis to h j (indeed, the function introduced by this item is none other than h j = h i ). We also get that, with the same J as before,

using again the first item of the inductive hypothesis to handle the case of indices in J.

Finally, by definition of g ′′ and by Lemma 7.7, using the convention sup ∅ = 0,

Let us now check the second item concerning splits and factorizations. Let s ∈ L(f, φ, r). By definition, there exists i ∈ J such that s ∈ L(g ′ , i, χ, r). In particular, |g ′ (s)| i ≥ 1, which entails that s ∈ L(h i , ψ i , r) by definition of g ′ . The inductive hypothesis gives us a family of r-splits s = u (m)

r w (m) according to ψ for m ∈ {1, . . . , k -1} -recall that rk(h i ) + 1 = rk(f ) = k -1. We complete it by taking (u (k) , v

r , w (k) ) to be a producing r-split of s with respect to (g ′ , i, χ), whose existence is guaranteed by definition of L(g ′ , i, χ, r). Since φ factors through both ψ i and χ by construction, this indeed gives us a family of k r-splits according to φ. Now, let s = α 0 β 1 α 1 . . . β k α k be a factorization and σ be a permutation of {1, . . . , k} such each β m coincides with some v (σ(m)) l for some l. Note that from the original expression of f as a composition by substitution, we have

Therefore, our desired inequality will follow once we prove the ones below:

To illustrate the idea, we assume σ(k) = k, so that

for some l, and we invite the reader to convince themself that this is merely a matter of notational convenience for the rest of the proof.

Let us start with h i . Since ν ′ hi factors through χ, the triple

Comparison-free Polyregular Functions

Proof of Theorem 7.1. We prove the circle of implications (i) ⇒ (iii) ⇒ (ii) ⇒ (i). (The claim after this equivalence has already been established in Theorem F.1.)

The first implication (i) ⇒ (iii) corresponds exactly to Lemma G.1 we just proved. The implication (iii) ⇒ (ii) is also relatively easy: cfpow

Γ is cfp (this is a consequence of Lemma G.2 and Theorem 6.1, although cfpow As announced, we prove Theorem 9.2 inductively on the rank of the sequence under consideration. The bulk of the reasoning is concentrated in the base case, stating that regular sequences are exactly the ultimately periodic combinations of pumping sequences.

▶ Lemma H.1. A sequence of words s : N → Σ * is regular if and only if there is m > 0 such that for every k < m, there are words u 0 , . . . , v l , v 1 , . . . , v l such that for every n ∈ N, we have

Proof. The "if" direction is straightforward, so we only prove the "only if" part of the statement. To keep notations harmonized, let us work with f : {a} * → Σ * such that s(n) = f (a n ) for every n ∈ N and fix a copyless SST computing f : {a} * → Σ * whose set of states, set of registers and transition function we call Q, R and δ respectively. We use the monoid

. This m is the one put forth in the lemma statement.

Let us fix k < m. Let (q, α) = µ •m (q 0 ) where q 0 is the initial state of the SST. We have µ

). Thus, q is the state reached by the SST after reading a m(n+1)+k for any n ∈ N. We also have (δ(-, a)) •m (q) = (q, γ) with γ ∈ M cl R,Σ and erase Σ (γ) = β. Given r ∈ R, we distinguish two cases. First, suppose that β(r) = ε or equivalently that γ(r) ∈ Σ * (in general, the codomain of γ is (Σ ∪ R) * ). When the SST is in state q and reads a m , it executes the assignment γ; when β(r) = ε, the new value of the register r is this γ(r) ∈ Σ * which does not depend on the old value of any register. Therefore, for all n ∈ N, the content of the register r after having read a m(n+1)+k (starting from the initial configuration) is the constant γ(r).

I Separation results

I.1 Proof of Theorem 8.1

▶ Theorem 8.1. There exist comparison-free polyregular functions which are not HDT0L:

These examples are comparison-free. We have seen in Example 4.3 that w → w |w| is a comparison-free polyregular function. For the other examples:

) is obtained as a composition by substitution of sequential functions, i.e. functions computed by sequential transducers (cf. Section 2.2), which are in particular regular; for an alphabet Σ with a, # ∈ Σ, there exist sequential functions f : Σ * → {a} * and g : Σ * → Σ * such that f (a n #w) = a n and g(a n #w) = w# for n ∈ N and w ∈ Σ * , so that CbS(f, (g) i∈{a} )(a n #w) = (w#) n .

(i) is not HDT0L. Let us fix a HDT0L system ({a}, {a, b}, ∆, d, (h) i∈{a} , h ′ ) and show that it does not compute a n → (a n b) n+1 . Let letters(w) be the set of letters occurring in the string w at least once. By the infinite pigeonhole principle, there exists an infinite X ⊆ N such that letters(h n (d)) has the same value ∆ ′ for all n ∈ X. Let us do a case analysis: Suppose first that for some r ∈ ∆ ′ and some m ∈ N, the letter b appears twice in h ′ • h m (r); in other words, that the latter contains a factor ba k b for some k ∈ N. Then for all n ∈ X, h ′ • h m+n (d) ∈ Σ * ba k bΣ * . Since X is infinite, this holds for some n such that m + n > k, so that this word -i.e. the output of the HDT0L system for a m+n -is different from (a m+n b) m+n+1 / ∈ Σ * ba k bΣ * . Otherwise, for all r ∈ ∆ ′ (that includes the degenerate case ∆ ′ = ∅) and all m ∈ N, there is at most one occurrence of b in h ′ • h m (r). Then for all m ∈ N, the length of h min(X) (d) bounds the number of occurrences of b in h ′ • h m+min(X) (d), and this bound is independent of m. On the contrary, in the sequence ((a n b) n+1 ) n≥m+min(X) , the number of occurrences of b is unbounded.

(ii) is not HDT0L. The second counterexample, namely w → w |w| , reduces to the first one: indeed, (a n b) n+1 = (a n b) |a n b| for all n ∈ N, which can also be expressed as

Suppose for the sake of contradiction that there is a HDT0L system (Σ, Σ, ∆, d, (h c ) c∈Σ , h ′ ) that computes w → w |w| with |Σ| ≥ 2; we may assume without loss of generality that a, b ∈ Σ. Then ({a}, {a, b}, ∆,

Let Σ ⊇ {a, #} be an alphabet and let (Σ, Σ, ∆, d, (h c ) c∈Σ , h ′ ) be a HDT0L system. We reuse a similar argument to our treatment of the counterexample (i). Let the sets ∆ ′ ⊆ ∆ and X ⊆ N with X infinite be such that letters(h n a (d)) = ∆ ′ for all n ∈ X. Suppose first that for some r ∈ ∆ ′ and some m ∈ N, the string h ′ • h m a • h # (r); contains a factor # • a k • # for some k ∈ N. Then for all n ∈ X, the given HDT0L system maps a m #a n to a string in Σ * • # • a k • # • Σ * . For n > k, this language does not contain (a n #) m ; such a n ∈ X exists because X is infinite.

Comparison-free Polyregular Functions

Otherwise, for any m ∈ N, since # occurs at most once in h ′ • h m a • h # (r) for r ∈ ∆ ′ , the output of the HDT0L system has at most |h min(X) (d)| occurrences of # on input a m #a min(X) . Therefore, for large enough m, this output is different from (a min(X) #) m .

I.2 Proof of Theorem 8.3

Let us recall the theorem.

▶ Theorem 8.3. Some HDT0L transductions are polyregular but not comparison-free:

(i) and (ii) are proven separately.

I.2.1 Proof of Theorem 8.3 item (i)

As mentioned in the body of the paper, this is proven by showing that the lengths of blocks of baa . . . aab, or equivalently, maximal blocks of a in the output of a given regular sequence is determined by a finite number of polynomial expressions. Let us formalize this notion.

▶ Definition I.1. Let Σ be a finite alphabet and c ∈ Σ. Call β c : Σ * → P(N) the function assigning to a word w the set of lengths of its maximal factors lying in {c} * (including ε):

We say that a sequence s : N → Σ * is poly-uniform if for every c ∈ Σ there exists a finite set of polynomials A s,c ⊆ Q[X] such that, for every n ∈ N,

▶ Lemma I.2. Every comparison-free polyregular sequence f : N → Σ * is poly-uniform.

Proof. First, observe that any ultimately periodic combination of poly-uniform sequence is poly-uniform. Indeed, assume that we have such a sequence s and m > 0 so that n → s(m(n + 1) + k) is poly-uniform for every k, and finite sets

witnessing that s is poly-uniform. Hence, by Theorem 9.2, it suffices to show that poly-pumping sequences are all polyuniform. We proceed by induction over polynomial word expressions e, defining suitable finite sets of polynomials A e,c for c ∈ Σ such that β c ( e (n)) ⊆ A e,c (n) and 0 ∈ A e,c :

◀

We can now conclude the proof of the first item of Theorem 8.3 by observing that the function f : a n → ba n-1 b . . . bab does not correspond to a poly-uniform sequence: β c (f (a n )) = {0, . . . , n -1} is unbounded, and thus cannot be covered by a finite set of functions, let alone polynomials in Q[X].

I.3 Proof of Theorem 8.3 item (ii)

Suppose for the sake of contradiction that f = map(a n → a n×n ) is comparison-free. Using Theorem 7.1, it must then have rank 1 since |f (w)| = O(|w| 2 ). Thus, we may write f = CbS(g, (h i ) i∈I ) where g : {a, #} * → I * and all the h i : {a, #} * → {a, #} * are regular.

For each J ⊆ I and k ∈ {0, . . . , |I|} (though the definition would make sense for k ∈ N), let ρ J,k : {a * } → (I \ J) * be uniquely defined by the condition

To put it plainly, ρ J,k (w) is the k-th block of letters from I \ J that appears in g(w) (the block may be the empty string if there are consecutive letters from J), or the empty string if this k-th block does not exist. The function ρ J,k is regular because it is the composition of a sequential function with g. We reuse some tools from Appendix F, especially the notion of producing 1-split from Lemma 7.7. There is a unique sensible way to combine the morphisms ν f ′ : {a, #} * → N (f ′ ) given by this lemma into a morphism

Note that the codomain above is a finite monoid: this allows us to apply Proposition 7.8 to this morphism φ and r = 1, which gives us some N ∈ N. Let s = a N (#a N ) |I| . For each m ∈ {0, . . . , |I|}, we apply the proposition to the factorization s

For f ′ ∈ F (the finite set of functions introduced above), we then define

Thanks Proposition F.5 and to the 1-split conditions that we made sure to get previously, we see that for each letter c in the codomain of f ′ (either {a, #} or I), | f ′ | c : N |I|+1 → N is monotone for the product partial order. Since f = map(a → a n×n ) = CbS(g, (h i ) i∈I ), Since | g| i and | h i | # are monotone for all i ∈ I, and N |I|+1 admits a minimum (0, . . . , 0), the fact that the above sum is constant means that, for each i ∈ I, either one of | g| i and | h i | # is constant equal to 0, or both are non-zero constant. Let J # ⊆ I be the set of indices that fit the second case. We claim that for i ∈ J # , the constant value taken by | h i | # must be 1. If this were not the case, then for all n ∈ N, there would be a substring of the form #a . . . a# in | h i (n, . . . , n)| # , and since f = CbS(g, (h i ) i∈I ) and | g(n, . . . , n)| i ̸ = 0, it would also be a substring of f (n, . . . , n) with length at most | h i (n, . . . , n)| # = O(n) (since h i is regular). This is impossible: for k ∈ {0, . . . , |I|}, the k-th substring of this form in f (n, . . . , n) has length (np k + q k ) 2 + 2 = Θ(n 2 ).

Comparison-free Polyregular Functions

Combining this with the above equation for | f | # , we see that | g| J # is the constant function equal to |I|. Let us abbreviate ρ k = ρ J # ,k ∈ F (recall that we defined it at the beginning of this proof) for k ∈ {0, . . . , |I|}; then ∀x ∈ N |I|+1 , ∃!ι 1 (x), . . . , ι |I| (x) ∈ J # : g(x) = ρ 0 (x)ι 1 (x) ρ 1 (x) . h i (m⃗ e k + n⃗ e l ) is unbounded when n → +∞. The product of those two quantities is a lower bound for the length of the k-th substring of the form #a . . . a# in f (m⃗ e k + n⃗ e l ), which contradicts the fact that this length does not depend on n (it is equal to (mp k + q k ) 2 + 2).