domain: info math

text:
Thomas Colcombet

Gaëtan Douéneau-Tabot

Aliaume Lopez

Z-polyregular functions

This paper studies a robust class of functions from finite words to integers that we call Z-polyregular functions. We show that it admits natural characterizations in terms of logics, Z-rational expressions, Z-rational series and transducers.

We then study two subclass membership problems. First, we show that the asymptotic growth rate of a function is computable, and corresponds to the minimal number of variables required to represent it using logical formulas. Second, we show that firstorder definability of Z-polyregular functions is decidable. To show the latter, we introduce an original notion of residual transducer, and provide a semantic characterization based on aperiodicity. Formalism Characterization of ZPoly Characterization of ZSF Counting formulas Counting valuations in MSO (Definition II.5) Counting valuations in FO (Definition V.1) Polyregular functions sum • polyregular (Proposition II.13) sum • star-free polyregular (Proposition V.17) Z-rational expressions Closure of rational languages under Cauchy products, sums, and Z-products (Theorem II.20) Closure of star-free languages under Cauchy products, sums, and Z-products (Theorem V.4) Ultimately N -polynomial (Theorem II.31) Ultimately 1-polynomial (Theorem V.13) Z-rational series that are/have Polynomial growth (Theorem II.31) n/a Eigenvalues in {0} ∪ U (Theorem II.31) Eigenvalues in {0, 1} (Theorem V.18) Residual transducer Residual transducer (Corollary IV.19) Counter-free residual transducer (Theorem V.13)

If F is a subset of the set of functions A * → Z and if S ⊆ Z, we let Span S (F ) := { i a i f i : a i ∈ S, f i ∈ F } be the set of S-linear combinations of the functions from F . The set Span N ({#ϕ : ϕ ∈ MSO k , k ≥ 0}) has been recently studied

I. INTRODUCTION

Deterministic finite state automata define the well-known and robust class of regular languages. This class is captured by different formalisms such as expressions (regular expressions [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF]), logic (Monadic Second Order (MSO) logic [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]), and algebra (finite monoids [START_REF] Schützenberger | On the definition of a family of automata[END_REF]). It contains a robust subclass of independent interest: star-free regular languages, which admits equivalent descriptions in terms of machines (counter-free automata [START_REF] Mcnaughton | Counter-Free Automata[END_REF]), expressions (star-free expressions [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF]), logic (first-order (FO) logic [START_REF] Perrin | First-order logic and star-free sets[END_REF]) and algebra (aperiodic monoids [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF]). Furthermore, one can decide if a regular language is star-free, and the proof relies on the existence (and computability) of a canonical object associated to each language (its minimal automaton [START_REF] Mcnaughton | Counter-Free Automata[END_REF] or, equivalently, its syntactic monoid [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF]).

Numerous works have attempted to carry the notion of regularity from languages to word-to-word functions. This work led to a plethora of non-equivalent classes (such as sequential, rational, regular and polyregular functions [START_REF] Bojańczyk | Polyregular Functions[END_REF]). Decision problems, including first-order definability, become more difficult and more interesting for functions [START_REF] Scott | Some definitional suggestions for automata theory[END_REF], mainly due to the lack of canonical objects similar to the minimal automata of regular languages. It was shown recently that first-order definability is decidable for the class of rational functions [START_REF] Filiot | Aperiodicity of rational functions is pspace-complete[END_REF] and that a canonical object can be built [START_REF] Filiot | On canonical models for rational functions over infinite words[END_REF].

This paper is a brochure for a natural class of functions from finite words to integers, which we name Z-polyregular functions. Its definition stems from the logical description of regular languages. Given an MSO formula ϕ( x) with free firstorder variables x, and a word w ∈ A * , we define #ϕ(w) to be the number of valuations ν such that w, ν |= ϕ( x). The indicator functions of regular languages are exactly the functions #ϕ where ϕ is a sentence (i.e. it does not have free variables, hence has at most one valuation: the empty one). We define the class of Z-polyregular functions, denoted ZPoly, as the class of Z-linear combinations of functions #ϕ where ϕ is in MSO with first-order free variables.

The goal of this paper is to advocate for the robustness of ZPoly. To that end, we shall provide numerous characterizations of these functions and relate them to pre-existing models. We also solve several membership problems and provide effective conversion algorithms. This equips ZPoly with a smooth and elegant theory, which subsumes that of regular languages.

Contributions: We introduce the class ZPoly as a natural generalization of regular languages via simple counting of MSO valuations. This definition can be seen as a restricted version of the Quantitative MSO introduced in [START_REF] Kreutzer | Quantitative monadic second-order logic[END_REF]. It also coincides with the linear finite counting automata of [START_REF] Schützenberger | Finite counting automata[END_REF]. We first connect Z-polyregular functions to word-to-word polyregular functions [START_REF] Bojańczyk | Polyregular Functions[END_REF], providing a justification for their name. As a class of functions from finite words to integers, it is then natural to compare ZPoly with the well-studied class of Z-rational series (see e.g. [START_REF] Berstel | Noncommutative rational series with applications[END_REF]). We observe that ZPoly is exactly the subclass of Z-rational series that have polynomial growth, i.e. the functions such that |f (w)| = O(|w| k ) for some k ≥ 0, by making effective the results of Schützenberger [START_REF] Schützenberger | Finite counting automata[END_REF]. As a consequence, we provide a simple syntax of Z-rational expressions to describe ZPoly as those built without the Kleene star. We also show how ZPoly can be described using natural restrictions on the eigenvalues of representations of Z-rational series. This property is built upon a quantitative pumping lemma characterizing the ultimate behavior of Z-polyregular functions as "ultimately N -polynomial" for some N ≥ 0. We summarize these results in the second column of Table I.

We then refine the description of ZPoly by considering for all k ≥ 0, the class ZPoly k of functions described using at most k free variables in the counting MSO formulas. It is easy to check that if f ∈ ZPoly k then |f (w)| = O(|w| k ). Our first main theorem shows that this property is a sufficient and necessary condition for a function of ZPoly to be in ZPoly k (see Figure 1). This result is an analogue of the various "pebble minimization theorems" that were shown for wordto-word polyregular functions [START_REF] Douéneau-Tabot | Pebble transducers with unary output[END_REF], [START_REF] Bojańczyk | Transducers of polynomial growth[END_REF], [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF], [START_REF] Bojańczyk | The growth rate of polyregular functions[END_REF]. We also prove that the membership problem of ZPoly k inside ZPoly is decidable.

Our second main contribution is the definition of an almost canonical object associated to each function of ZPoly. We name this object the residual transducer of the function, and show that it can effectively be built. Its construction is inspired by the residual automaton of a regular language, and heavily relies on the decision procedure from ZPoly to ZPoly k .

Finally, we define the class ZSF of star-free Z-polyregular functions, as the class of linear combinations of #ϕ where ϕ is a first-order formula with free first-order variables. As in the case of ZPoly, observe that the indicator functions of star-free languages are exactly the #ϕ where ϕ is a first-order sentence.

Our third main contribution then applies the construction of the residual transducer to show that the membership problem from ZPoly to ZSF is decidable. Incidentally, we introduce for k ≥ 0 the class ZSF k (defined in a similar way as ZPoly k ) and show that ZSF k = ZSF ∩ ZPoly k , as depicted in Figure 1. Furthermore, we show that the numerous characterizations of ZPoly in terms of existing models can naturally be specialized to build characterizations of ZSF, as depicted in the third column of Table I. Overall, our contribution is the description of a natural theory of functions from finite words to Z, that is the consequence of a reasonable computational power (polynomial growth, i.e. less than Z-rational series) and the ability to correct errors during a computation (using negative numbers). Furthermore, the theory of Z-polyregular functions is built using new and non-trivial proof techniques.

Outline: Section II is devoted to the introduction of the classes ZPoly and ZPoly k . We also compare ZPoly with polyregular functions and with Z-rational series. We then devote Section III to a free variable minimization theorem (Theorem III.3), which is a key result towards the effective computation of a canonical residual transducer in Section IV. We then introduce ZSF and ZSF k in Section V, and use the residual transducer to prove the decidability of ZSF inside ZPoly (Theorem V.8). We conclude by connecting ZSF to polyregular functions and Z-rational series. All of the aforementioned results include algorithms to decide membership and provide effective conversions between the various representations.

II. Z-POLYREGULAR FUNCTIONS

The goal of this section is to define Z-polyregular functions. We first define this class of functions using a logical formalism (monadic second-order formulas with free variables, Section II-A), then we relate it to (word-to-word) regular and polyregular functions (Section II-B) and finally we show that it corresponds to a natural and robust subclass of the wellknown Z-rational series (Sections II-C and II-D).

In the rest of this paper, Z (resp. N) denotes the set of integers (resp. nonnegative integers). If i ≤ j, the set [i:j] is {i, i+1, . . . , j} ⊆ N (empty if j < i). The capital letter A denotes a fixed alphabet, i.e. a finite set of letters. A * (resp. A + ) is the set of words (resp. non-empty words) over A. The empty word is ε ∈ A * . If w ∈ A * , let |w| ∈ N be its length, and for

1 ≤ i ≤ |w| let w[i] be its i-th letter. If I = {i 1 < • • • < i ℓ } ⊆ [1:|w|], let w[I] := w[i 1 ] • • • w[i ℓ ]. If a ∈ A, let
|w| a be the number of letters a occurring in w. We assume that the reader is familiar with the basics of automata theory, in particular the notions of monoid morphisms, idempotents in monoids, monadic second-order (MSO) logic and first-order (FO) logic over finite words (see e.g. [START_REF] Thomas | Languages, automata, and logic[END_REF]).

A. Counting valuations on finite words

Let MSO k be the set of MSO-formulas over the signature (A, <) which have exactly k free first-order variables. We then let MSO := k∈N MSO k . If ϕ(x 1 , . . . , x k ) ∈ MSO k , w ∈ A * and 1 ≤ i 1 , . . . , i k ≤ |w|, we write w |= ϕ(i 1 , . . . , i k ) whenever the valuation x 1 → i 1 , . . . , x k → i k makes the formula ϕ true in the model w.

Definition II.1 (Counting). Given ϕ(x 1 , . . . , x k ) ∈ MSO k , we let #ϕ : A * → N be the function defined by #ϕ(w) := |{(i 1 , . . . , i k ) : w |= ϕ(i 1 , . . . , i k )}|.
The value #ϕ(w) is the number of tuples that make the formula ϕ true in the model w.

Example II.2. If ϕ ∈ MSO 0 , then #ϕ is the indicator function of the (regular) language {w : w |= ϕ} ⊆ A * . Example II.3. Let A := {a, b}. Let ϕ(x, y) := a(x) ∧ b(y), then #ϕ(w) = |w| a × |w| b for all w ∈ A * . Let ψ(x, y) := ϕ(x, y) ∧ x > y, then #ψ(a n0 ba n1 • • • a np ) = p i=0 i × n i .
Example II.4. Let ϕ ∈ MSO k , and x be a fresh variable. Then, x = x ∧ ϕ ∈ MSO k+1 , and by Douéneau-Tabot in [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF] under the name of "polyregular functions with unary output". In the following, we shall call this class the N-polyregular functions.

#(x = x ∧ ϕ)(w) = |w| × #ϕ(w) for every w ∈ A * . Similarly, for all w ∈ A * and a ∈ A, #(a(x) ∧ ϕ)(w) = |w| a × #ϕ(w). Z-rational Z-polyregular Star-free Z-polyregular ZSF 0 ZSF 1 ZSF 2 ZPoly 0 ZPoly 1 ZPoly 2 Polynomial growth O(n 2 ) growth O(n) growth O(1) growth w → 1 L (w) if L is regular but not star-free w → |w| × (-1) |w| w → 1 L (w) if L star-free w → |w| a × |w| b if a, b ∈ A w → (-2) |w|
The goal of this paper is to study the Z-linear combinations of the basic #ϕ functions, which we call Z-polyregular functions. We shall see that this class is a quantitative counterpart of regular languages that admits several equivalent descriptions, and for which various decision problems can be solved. We provide in Definition II.5 a fine-grained definition of this class of functions, depending on the number of free variables which are used within the #ϕ basic functions.

Definition II.5 (Z-polyregular functions). For k ≥ 0, let ZPoly k := Span Z ({#ϕ : ϕ ∈ MSO ℓ , ℓ ≤ k}). We define the class of Z-polyregular functions as ZPoly := k ZPoly k .

We also let ZPoly -1 := {0}.

Remark II.6. For all k ≥ 0, the class ZPoly k is precisely the class of functions computable in QMSO(Σ k

x , ⊕, ⊙ b ) of [START_REF] Kreutzer | Quantitative monadic second-order logic[END_REF]Section IV.A] over the semiring (Z, +, ×).

Remark II.7. For all k ≥ 0, the class ZPoly k is precisely the class of functions computable by linear finite counting automata of order k introduced by [12, p. 91].

Example II.8. ZPoly 0 is exactly the class of Z-linear combinations of indicators 1 L of regular languages L.

Example II.9. Following the construction of Example II.4, for every k, ℓ ≥ 0, and f ∈ ZPoly ℓ , the function g : w → f (w) × |w| k belongs to ZPoly ℓ+k .

Example II.10. Let 1 odd and 1 even be respectively the indicator functions of words of odd length and even length. For all k ≥ 0, the function w

→ (-1) |w| × |w| k is in ZPoly k . Indeed, it is w → 1 even (w) × |w| k -1 odd (w) × |w| k .
Observe that it cannot be written as a single δ#ϕ for some δ ∈ Z, ϕ ∈ MSO ℓ , ℓ ≥ 0, since otherwise its sign would be constant.

The use of negative coefficients in the linear combinations has deep consequences on the expressive power of ZPoly.

Let us consider the function

f : w → (|w| a -|w| b ) 2 . Be- cause f (w) = |w| 2 a -2|w| a |w| b + |w| 2 b , we conclude from Example II.4 that f is in ZPoly 2 . Although f is non-negative, f -1 ({0}) = {w : |w| a = |w| b } is not a regular language, hence f is not a N-polyregular function.
Remark II.11 (More variables). Let ℓ > k ≥ 0, ϕ ∈ MSO k , then for all words w ∈ A + we have:

#ϕ(w) = #(ϕ ∧ x k+1 = • • • = x ℓ ∧ ∀y.x k+1 ≤ y)(w)
the latter being an MSO ℓ formula. This formula also holds for w = ε if k > 0, but it may fail for k = 0 because in that case the right-hand side equals 0 regardless of the formula ϕ (because there is no valuation), whereas #ϕ(ε) may not be 0.

One can refine Remark II.11 to conclude that for all k ≥ 0,

ZPoly k = Span Z ({#ϕ : ϕ ∈ MSO k } ∪ {1 {ε} }).
In the rest of the paper, 1 {ε} will not play any role, and we will safely ignore it in the proofs so that ZPoly k will often be considered equal to Span Z ({#ϕ : ϕ ∈ MSO k }).

B. Regular and polyregular functions

We recall that the class of (word-to-word) functions computed by two-way transducers (or equivalently by MSOtransductions, see e.g. [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF]) is called regular functions. As an easy consequence of its definition, ZPoly k is preserved under pre-composition with a regular function.

Proposition II.12. For all k ≥ 0, the class ZPoly k is (effectively) closed under pre-composition by regular functions. Now, we intend to justify the name "Z-polyregular functions" by showing that this class is deeply connected to the well-studied class of polyregular functions from finite words to finite words. Informally, this class of functions can be defined using the formalism of multidimensional MSO-interpretations. The reader is invited to consult [START_REF] Bojanczyk | String-to-String Interpretations With Polynomial-Size Output[END_REF] for its formal definition, which we skip here. Let sum : {±1} * → Z be the sum operation mapping w ∈ {±1} * to

C. Rational series and rational expressions

The class of rational series over the semiring (Z, +, ×), also known as Z-rational series, is a robust class of functions from finite words to Z that has been largely studied since the 1960 (see e.g. [START_REF] Berstel | Noncommutative rational series with applications[END_REF] for a survey). It can be defined using the indicator functions 1 L of regular languages L ⊆ A * , and the following combinators given f, g : A * → Z and δ ∈ Z:

• the external Z-product δf : w → δ × f (w); • the sum f + g : w → f (w) + g(w); • the Cauchy product f ⊗ g : w → w=uv f (u) × g(v); • if and only if f (ε) = 0, the Kleene star f * := n≥0 f n where f 0 : ε → 1, w = ε → 0 is neutral for Cauchy product and f n+1 := f ⊗ f n .
Definition II.14 (Z-rational series). The class of Z-rational series is the smallest class of functions from finite words to Z that contains the indicator functions of all regular languages, and is closed under taking external Z-products, sums, Cauchy products and Kleene stars.

We intend to connect Z-rational series and Z-polyregular functions. Let us first observe that not all Z-rational series are Z-polyregular. We say that a function f : A * → Z has polynomial growth whenever there exists k ≥ 0 such that |f (w)| = O(|w| k ). It is an easy check that every Z-polyregular function has polynomial growth.

Claim II.15. If k ≥ 0 and f ∈ ZPoly k then |f (w)| = O(|w| k ).
Example II. [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF]. The map f : w → (-2) |w| is a Z-rational series because f = ((-3)1 A + ) * . However f ∈ ZPoly since it does not have polynomial growth.

It is easy to see from the logical definition that the class ZPoly is closed under taking Cauchy products.

Claim II.17. Let k, ℓ ≥ 0. Let f ∈ ZPoly k and g ∈ ZPoly ℓ , then f ⊗ g ∈ ZPoly k+ℓ+1 . The construction is effective.

As a consequence, if L ⊆ A * is regular and f ∈ ZPoly k , then 1 L ⊗ f ∈ ZPoly k+1 . The following result states that such functions actually generate the whole space ZPoly k+1 .

Proposition II.18. Let k ≥ 0, the following (effectively) holds:

ZPoly k+1 = Span Z ({1 L ⊗ f : L regular, f ∈ ZPoly k }).
Example II. [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF]. The map w → (-1) |w| |w| is in ZPoly 1 as it equals 1 odd ⊗ 1 odd +1 even ⊗ 1 even -1 even ⊗ 1 odd -1 odd ⊗ 1 even -1 odd + 1 even . Now, let us show that Z-polyregular functions can be characterized both syntactically and semantically as a subclass of Z-rational series. We prove that the membership problem is decidable and provide an effective conversion algorithm.

Theorem II.20 (Rational series of polynomial growth). Let f : A * → Z, the following are equivalent:

1) f is a Z-polyregular function;
2) f belongs to the smallest class of functions that contains the indicator functions of all regular languages and is closed under taking external Z-products, sums and Cauchy products; 3) f is a Z-rational series having polynomial growth. Furthermore, one can decide whether a Z-rational series is a Z-polyregular function and the translations are effective.

Proof. For Item 2 ⇒ Item 1, observe that ZPoly contains the indicator functions of regular languages, is closed under external Z-products, sums, and Cauchy products (thanks to Claim II.17). For Item 1 ⇒ Item 2, we obtain for all k ≥ 0 as an immediate consequence of Proposition II.18:

ZPoly k = Span Z ({1 L0 ⊗ • • • ⊗ 1 L k : L 0 , . . . , L k regular languages}) (1)
and the result follows.

The equivalence between Item 2 and Item 3 follows (in a non effective way) from [13,

D. Rational series and representations

In this section, we intend to provide another description of Z-polyregular functions among Z-rational series. To that end, we first recall that rational series can also be described using matrices (or, equivalently, weighted automata). Let M n,m (Z) be the set of all n × m matrices with coefficients in Z. We equip M n,m (Z) with the usual matrix multiplication.

Definition II.25 (Linear representation). We say that a triple (I, µ, F ) where µ :

A * → M n,n (Z) is a monoid morphism, I ∈ M 1,n (Z) and F ∈ M n,1 (Z), is a Z-linear representation of a function f : A * → Z if f (w) = Iµ(w)F for all w ∈ A * .
It is well-known since Schützenberger (see e.g. [13, Theorem 7.1 p 17]) that the class of Z-rational series is (effectively) the class of functions that have a Z-linear representation.

Example II.26. The map w → (-1) |w| |w| from Example II.19 is a Z-polyregular function, hence it is a Zrational series. It has the following Z-linear representation:

-1 0 , w → -1 1 0 -1 |w| , 0 1 .
Note that the eigenvalues of any matrix in µ(A * ) are 1 or -1.

Example II. [START_REF] Droste | Aperiodic weighted automata and weighted first-order logic[END_REF] A Z-linear representation (I, µ, F ) of a function f is said to be minimal, when it has minimal dimension n among all the possible representations of f . Given a matrix M ∈ M n,n (Z), we let Spec(M ) ⊆ C be its spectrum, which is the set of all its (complex) eigenvalues. If S ⊆ M n,n (Z), we let Spec(S) := M∈S Spec(M ) be the union of the spectrums. Finally, let B(0, 1) := {x ∈ C : |x| ≤ 1} be the unit disc and U := {x ∈ C : ∃n ≥ 1, x n = 1} be the roots of unity. Now, we show that Z-polyregular functions can be characterized through the eigenvalues of Z-linear representations. More precisely, Theorem II.31 will relate the asymptotic growth of a series to the spectrum of the set of matrices µ(A * ). As a first step, let us observe that the eigenvalues occurring in a minimal representation can be revealed by iterating words.

Lemma II.28. Let f : A * → Z be a Z-rational series and (I, µ, F ) be a minimal Z-linear representation of f . Let w ∈ A * and λ ∈ Spec(µ(w)). There exist coefficients α i,j ∈ C for 1 ≤ i, j ≤ n, and words u 1 , v 1 , . . . , u n , v n ∈ A * such that λ X = n i,j=1 α i,j f (v i w X u j ) for all X ≥ 0. Now, we refine the notion of polynomial growth to explicit the behaviour of a function when iterating factors.

Definition II.29. Let N > 0. A function f : A * → Z is ultimately N -polynomial whenever there exists M ≥ 0 such that for all ℓ ≥ 0, for all α 0 , w 1 , α 1 , . . . , w ℓ , α ℓ ∈ A * , there exists

P ∈ Q[X 1 , . . . , X ℓ ], such that f (α 0 w N X1 1 α 1 • • • w N X ℓ ℓ α ℓ ) = P (X 1 , . . . , X ℓ ), whenever X 1 , . . . , X ℓ ≥ M .
In this section we only need to have ℓ = 1, but Definition II.29 has been made generic so that it can be reused in Section V when dealing with aperiodicity. Now, we observe that ultimate polynomiality is preserved under taking sums, external Z-products and Cauchy products. Lemma II.30 also provides a fine-grained control over the value N of ultimate N -polynomiality, that will mostly be useful in Section V.

Lemma II.30. Let f, g : A * → Z be (respectively) ultimately N 1 -polynomial and ultimately N 2 -polynomial, then:

• f + g and f ⊗ g are ultimately (N 1 × N 2 )-polynomial; • δf is ultimately N 1 -polynomial for δ ∈ Z.
Furthermore, for every regular language L, there exists N > 0 such that 1 L is ultimately N -polynomial. Now, we have all the elements to prove the main theorem of this section.

Theorem II.31 (Polynomial growth and eigenvalues). Let f : A * → Z, the following are equivalent:

1) f is a Z-polyregular function;

2) f is a Z-rational series that is ultimately N -polynomial for some N > 0; 3) f is a Z-rational series and for all minimal Z-linear For Item 2 ⇒ Item 3, let (I, µ, F ) be a minimal representation of f in Z, of dimension n ≥ 0. Let w ∈ A * and λ ∈ Spec(µ(w)). Thanks to Lemma II.28, there exists α i,j , u i , v j for 1 ≤ i, j ≤ n, such that λ X = 1≤i,j≤n α i,j f (v i w X u j ) for X large enough. By assumption, for all 1 ≤ i, j ≤ n, there exists N i,j > 0 such that X → f (v i w Ni,j X u j ) is a polynomial for X large enough. Hence there exists N > 0 (i.e. the product of the N i,j ) such that X → λ N X = (λ N ) X is a polynomial for X large enough, which therefore must be a constant polynomial. Hence λ N ∈ {0, 1}, which implies that λ ∈ {0} ∪ U. Item 3 ⇒ Item 4 is obvious.

representations (I, µ, F ) of f , Spec(µ(A * )) ⊆ U ∪ {0}. 4) f is a Z-rational series and for some minimal Z-linear representation (I, µ, F ) of f , Spec(µ(A * )) ⊆ B(0, 1); Proof. Item 4 ⇒ Item 1 is a direct consequence of [
Remark II.32. Item 3 of Theorem II.31 is optimal, in the sense that for all λ ∈ U ∪ {0}, there exists a Z-rational series of polynomial growth having a minimal representation (I, µ, F ) with λ ∈ Spec(µ(A * )) (if λ ∈ U, we let µ(a) be the companion matrix of the cyclotomic polynomial associated to λ).

Remark II.33. Leveraging the proof scheme used for the implication Item 2 ⇒ Item 3 of Theorem II.31, one can actually show that the following asymptotic polynomial bound characterizes Z-polyregular functions among Z-rational series: for all u, w, v ∈ A * , there exists

P ∈ Q[X], such that |f (uw X v)| ≤ P (X), for X large enough. Remark II.34. Beware that Spec(µ(A)) ⊆ {0} ∪ U has no reason to imply Spec(µ(A * )) ⊆ {0} ∪ U.

III. FREE VARIABLE MINIMIZATION AND GROWTH RATE

In this section, we study the membership problem from ZPoly to ZPoly k for a given k ≥ 0. As observed in Claim II.15, if f ∈ ZPoly k then |f (w)| = O(|w| k ). We show that this asymptotic behavior completely characterizes ZPoly k inside ZPoly. This statement is formalized in Theorem III.3, which also provides both a decision procedure and an effective conversion algorithm. It turns out that Theorem III.3 is also a stepping stone towards computing the residual automaton of a function f ∈ ZPoly, which is done in Section IV.

This can be understood as a result that "minimizes" the number of free variables needed to describe a Z-polyregular function. As such, it is tightly connected with the "pebble minimization" results that exists for (word-to-word) polyregular functions [START_REF] Bojańczyk | The growth rate of polyregular functions[END_REF] and N-polyregular functions [START_REF] Douéneau-Tabot | Pebble transducers with unary output[END_REF]. However, these results cannot be used as black box theorems to minimize the number of free variables of Z-polyregular functions because the negative coefficients of the latter induce non-trivial behaviors.

To capture the growth rate of Z-polyregular functions, we shall introduce a quantitative variant of the traditional pumping lemmas. Before that, let us extend the O notation to multivariate functions f, g : N n → Z as follows: we say that f = O(g) whenever there exist

N, C ≥ 0 such that |f (x 1 , . . . , x n )| ≤ C|g(x 1 , . . . , x n )| for every x 1 , . . . , x n ≥ N . We similarly extend the notation f (x) = Ω(g(x)) to multivariate functions. Definition III.1. A function f : A * → Z is k-pumpable whenever there exist α 0 , . . . , α k ∈ A * , w 1 , . . . , w k ∈ A * , such that |f (α 0 k i=1 w Xi i α i )| = Ω(|X 1 + • • • + X k | k ). Example III.2. For all k ≥ 0, for all f ∈ ZPoly k , f is not (k + 1)-pumpable because |f (w)| = O(|w| k ).
The equivalence between Item 1 and Item 2 in Theorem III.3 is known since [START_REF] Schützenberger | Finite counting automata[END_REF]. However, the equivalence with Item 3 and the effectivity of the result are novel.

Theorem III.3 (Free Variable Minimization). Let f ∈ ZPoly and k ≥ 0. The following conditions are equivalent:

1) f ∈ ZPoly k ; 2) |f (w)| = O(|w| k ); 3) f is not (k + 1)-pumpable.
Furthermore, the minimal k such that f ∈ ZPoly k is computable, and the construction is effective.

The proof of Theorem III.3 is done via induction on k, and follows directly from the following induction step, to which we devote the rest of Section III.

Induction

Step III.4. Let k ≥ 1 and f ∈ ZPoly k . The following conditions are equivalent:

1) f ∈ ZPoly k-1 ; 2) |f (w)| = O(|w| k-1 ); 3) f is not k-pumpable.

Moreover this property can be decided and the construction is effective.

Beware that one must be able to pump several factors at once to detect the growth rate, as illustrated in the following example. This has to be contrasted with Remark II.33.

Example III.5. Let f : a k b ℓ → k × ℓ and w → 0 otherwise. The function f is Z-polyregular and 2-pumpable, however, f (α 0 w X α 1 ) = O(X) for every triple α 0 , w, α 1 ∈ A * .
Our proof of Induction Step III.4 is built upon factorization forests. Given a morphism µ : A * → M into a finite monoid and w ∈ A * , a µ-forest of w is a forest that can be represented as a word over  := A ⊎ { , }, defined as follows.

Definition III.6 (Factorization forest [START_REF] Simon | Factorization forests of finite height[END_REF]). Given a monoid morphism µ : A * → M and w ∈ A * , we say that F is a µ-forest of w when:

• either F = a, and w = a ∈ A;

• or F = F 1 • • • F n , w = w 1 • • • w n and for all 1 ≤ i ≤ n, F i is a µ-forest of w i ∈ A + . Furthermore, if n ≥ 3 then µ(w 1 ) = • • • = µ(w n ) is an idempotent of M .
We let F µ be the language of µ-forests inside ( Â) * . Because forests are (ordered) trees, we will use the standard vocabulary to talk about the nodes, the sibling/parent relation, the root, the leaves and the depth of a forest. We let F µ d ⊆ ( Â) * be the set of µ-forests with depth at most d. Let word:

F µ d → A * be the function mapping a µ-forest of w ∈ A * to w itself. Example III.7. Let M := ({-1, 1, 0}, ×). A forest F ∈ F µ 5
(where µ : M * → M maps a word to the product of its elements) such that word(F ) = (-1)(-1)0(-1)000000 is depicted in Figure 2. Double lines denote idempotent nodes (i.e. nodes with more than 3 children).

When M is a finite monoid, it is known from Simon's celebrated theorem [START_REF] Simon | Factorization forests of finite height[END_REF] that any word in A * has a µ-forest of bounded depth. Furthermore, this small forest can be computed by a regular function (notion introduced in Section II-B).

Theorem III.8 ([23], [START_REF] Colcombet | Green's relations and their use in automata theory[END_REF]). Given a morphism into a finite monoid µ : A * → M , one can effectively compute some d ≥ 0 and a regular function forest : A * → F µ d such that word • forest is the identity function.

In order to prove Induction Step III.4, we shall consider a function (f : A * → Z) ∈ ZPoly k that is not k-pumpable, and show how to compute it as a function in ZPoly k-1 . To that end, we shall construct a function g : Â * → Z ∈ ZPoly k-1 such that f = g • forest. Since forest is regular thanks to Theorem III.8, it will follow that f ∈ ZPoly k-1 by Proposition II.12. Remark that it is only needed to define g on F µ d . Following the classical connections between MSO-formulas and regular languages [START_REF] Thomas | Languages, automata, and logic[END_REF], we prove in Claim III.11 that for every function f ∈ ZPoly k there exist a finite monoid M and a morphism µ : A * → M , such that f (w) can be reconstructed using "simple" MSO-formulas which are evaluated along bounded-depth µ-factorizations of w.

Claim III.9. Given a morphism µ : A * → M into a finite monoid and d ∈ N, the following predicates are MSO definable for words over Â. For all F ∈ F µ d , and w = word(F ), then: [START_REF] Bojańczyk | The growth rate of polyregular functions[END_REF]). For all f ∈ ZPoly k , one can build a finite monoid M , a depth d ∈ N, a surjective morphism µ :

• F |= isleaf(x) if and only if x is a leaf of F ; • F |= between m (x,
A * → M , constants n ≥ 0, δ i ∈ Z for 1 ≤ i ≤ n, formulas ψ i ∈ INV k for 1 ≤ i ≤ n, such that for every word w ∈ A * , for every factorization forest F ∈ F µ d of w, it holds that f (w) = n i=1 δ i × #ψ i (F ).
In the rest of this section, we focus on the number of free variables in Z-linear combinations of #ψ where ψ ∈ INV. The crucial idea is that one can leverage the structure of the forest F ∈ F µ d to compute #ψ more efficiently, at the cost of building a non-INV formula.

For that, we explore the structure of the forest F as follows: given a node t in a forest F , we define its skeleton to be the subforest rooted at that node, containing only the right-most and left-most children recursively. This notion was already used in [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF], [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF], [START_REF] Bojańczyk | The growth rate of polyregular functions[END_REF] for the study of pebble transducers.

Definition III.12. Let F ∈ F µ and t ∈ Nodes(F ), we define the skeleton of t by:

• if t = a ∈ A is a leaf, then Skel(t) := {t}; • otherwise if t = F 1 • • • F n , then Skel(t) := {t} ∪ Skel(F 1 ) ∪ Skel(F n ).
Let w ∈ A * , F be a µ-forest of w, and t ∈ Nodes(F ). The set of nodes Skel(t) defines a µ-forest of a (scattered) subword u of w: the one obtained by concatenating the leaves of F that are in Skel(t). See Figure 2 for an example of a skeleton. A crucial property of Skel(t) seen as a forest is that it preserves the evaluation:

Claim III.13. For all d ≥ 0, finite monoid M , morphism µ : A * → M , forest F ∈ F µ d , node t ∈ F , it holds that µ(word(Skel(t))) = µ(word(t)). -1 -1 0 -1 0 0 0 0 0 0
Fig. 2: A forest F with word(F ) = (-1)(-1)0(-1)000000 together with a skeleton in blue.

Let F be a forest and x be a leaf in F . Observe that Skel(x) is exactly x itself. There may exist several nodes t ∈ F such that x ∈ Skel(t), however only one of them is maximal thanks to Lemma III.14. As a consequence one can partition Leaves(F ) depending on the maximal skeleton (for inclusion) which contains a given leaf (Definition III.15).

Lemma III.14. Let F ∈ F µ d , x ∈ Leaves(F ). There exists t ∈ Nodes(F ) such that x ∈ Skel(t).

Furthermore, for every t, t ′ such that x ∈ Skel(t) ∩ Skel(t ′ ),

Skel(t) ⊆ Skel(t ′ ) or Skel(t ′ ) ⊆ Skel(t).
Definition III.15. Let skel-root: Leaves(F ) → Nodes(F ) map a leaf x to the t ∈ Nodes(F ) such that x ∈ Skel(t) and Skel(t) is maximal for inclusion.

Following the work of [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF], we define a notion of dependency of leaves (Definition III.17) based on the relationship between their maximal skeletons (Definition III. [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF]).

Definition III.16 (Observation). We say that t ′ ∈ Nodes(F ) observes t ∈ Nodes(F ) if either t ′ is an ancestor of t (this includes t itself), or the immediate left or right sibling of an ancestor of t.

Definition III.17 (Dependency). In a forest F , a leaf y depends on a leaf x, written x depends-on y, when skel-root(y) observes skel-root(x).

Beware that the relation x depends-on y is not symmetric. This allows us to ensure that the number of leaves y that depend on a fixed leaf x is uniformly bounded.

Claim III. [START_REF] Thomas | Languages, automata, and logic[END_REF]. Given d ≥ 0, there exists a (computable) bound N d ∈ N such that for all F ∈ F µ d and all leaf x ∈ Leaves(F ), there exist at most N d leaves which depend on x.

It is a routine check that for every fixed d, one can define the predicate sym-dep(x, y) in MSO over F µ d checking whether x depends-on y or y depends-on x, that is the symmetrised version of x depends-on y. We generalize this predicate to tuples x := (x 1 , . . . , x k ) via:

sym-dep( x) :=    ⊤ for k = 0; ⊤ if and only if x 1 is the root for k = 1; i =j sym-dep(x i , x j ) otherwise.
Notice that the independence (or dependence) of a tuple of leaves x only depends on the tuple skel-root(x 1 ), . . . , skel-root(x n ). The notion of dependent leaves is motivated by the fact that counting dependent leaves can be done with one variable less, as shown in Lemma III. [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF].

Lemma III.19. Let d ≥ 0, M be a finite monoid, µ : A * → M , k ≥ 1, and ψ ∈ INV k . One can effectively build a function g : ( Â) * → Z ∈ ZPoly k-1 such that for every F ∈ F µ d , g(F ) = #(ψ( x) ∧ sym-dep( x))(F ).
Definition III.20. Let k ≥ 1 and f ∈ ZPoly k , thanks to Claim III.11 and Theorem III.8, there exists µ :

A * → M , d ≥ 0, δ i ∈ Z, ψ i ∈ INV k such that: f = n i=1 δ i #ψ i ( x) • forest = n i=1 δ i #(ψ i ( x) ∧ sym-dep( x)) :=f dep • forest + n i=1 δ i #(ψ i ( x) ∧ ¬ sym-dep( x)) :=f indep • forest . (2)
We say that f dep is the dependent part of f and f indep is its independent part. Thanks to Lemma III.19 and Proposition II.12, for every

k ≥ 1 and f ∈ ZPoly k , (f dep • forest) ∈ ZPoly k-1 (over F µ d ).
Hence, whether the function f belongs to ZPoly k-1 only depends on its independent part. We will actually prove that in this case, f ∈ ZPoly k-1 if and only if f indep = 0. For that, we will rely on "pumping families" that respect forest.

Definition III.21 (Pumping family). A (µ, d)- pumping family of size k ≥ 1 is given by words α 0 , w 1 , α 2 , . . . , α k-1 , w k , α k ∈ A * , together with a family F X of forests in F µ d , such that for all 1 ≤ i ≤ k, w i = ε, and F X is a µ-forest of w X := α 0 k i=1 (w i ) Xi α i for every X := X 1 , . . . , X k ≥ 0. Remark III.22. A (µ, d)-pumping family of size k satisfies that |w X | = Θ(X 1 +• • •+X k ), and |F X | = Θ(X 1 +• • •+X k ) since the depth of F X is bounded by d.
Lemma III. [START_REF] Simon | Factorization forests of finite height[END_REF]. Let f indep be defined as in Equation [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]. Then, f indep = 0 if and only if there exists a (µ, d)-pumping family of size k such that f (F X ) is ultimately a Z-polynomial in X 1 , . . . , X k with a non-zero coefficient for X

1 • • • X k .
Moreover, one can decide whether f indep = 0. Now, we are almost ready to conclude the proof of Induction Step III.4. The only difficulty left is handled by the following technical lemma which enables to lift a bound on the asymptotic growth of polynomials to a bound on their respective degrees. It is also reused in Section V.

Lemma III.24. Let P, Q be two polynomials in R[X 1 , . . . , X n ]. If |P | = O(|Q|), then deg(P ) ≤ deg(Q).

Proof of Induction

Step III.4. The only non-trivial implication is Item 3 ⇒ Item 1. Let f ∈ ZPoly k satisfying the conditions of Item 3. We can decompose this function following Equation (2). As observed above, we only need to show that f indep = 0.

Consider a pumping family (w X , F X ) of size k, we have:

|f indep (F X )| = |f (w X )-f dep (F X )| = O(|X 1 +• • •+X k | k-1 ).
Assume by contradiction that f indep = 0, Lemma III.23 provides us with a pumping family such that

f indep (F X )
is ultimately a polynomial with non-zero coefficient for

X 1 • • • X k .
As this polynomial is asymptotically bounded by

(X 1 + • • • + X k ) k-1
, Lemma III.24 yields a contradiction. The constructions of forest, f dep , and f indep are effective, therefore so is our procedure. Moreover, one can decide whether f indep = 0 thanks to Lemma III.23.

IV. RESIDUAL TRANSDUCERS

In this section, we provide a canonical object associated to any Z-polyregular function, named its residual transducer. Our construction is effective, and the algorithm heavily relies on Theorem III.3. This new object has its own interest, and it will also be used in Section V to decide first-order definability of Z-polyregular functions, that will extend first-order definability for regular languages (see e.g. [START_REF] Perrin | First-order logic and star-free sets[END_REF] for an introduction).

A. Residuals of a function

We first introduce the notion of residual of a function f : A * → Z under a word u ∈ A * . Note that if L ⊆ A * and u ∈ A * , then u ⊲ 1 L is the characteristic function of the well-known residual language u -1 L := {w ∈ A * : uw ∈ L}. In particular, the set {u ⊲ 1 L : u ∈ A * } is finite if and only if L is regular. However, given f ∈ ZPoly k for k ≥ 1, the set {u ⊲ f : u ∈ A * } is not finite in general (see e.g. Example IV.2). We now intend to show that this set is still finite, up to an identification of the functions whose difference is in ZPoly k-1 .

Definition IV.6 (Growth equivalence). Given k ≥ -1 and f, g :

A * → Z, we let f ∼ k g if and only if f -g ∈ ZPoly k
Let us observe that ∼ k is an equivalence relation, that is compatible with external Z-products, sums, ⊗ and ⊲ .

Claim IV.7. For all k ≥ -1, ∼ k is an equivalence relation and the following holds for all u ∈ A * , δ ∈ Z, and f, g : A * → Z:

• if f ∼ k g, then u ⊲ f ∼ k u ⊲ g; • u ⊲ (1 L ⊗ f ) ∼ k (u ⊲ 1 L ) ⊗ f for L ⊆ A * ; • if f ∼ k g and f ′ ∼ k g ′ then f + f ′ ∼ k g + g ′ ; • if f ∼ k g then δ • f ∼ k δ • g.
By combining these results with the characterization of ZPoly via these combinators in Theorem II.20, we can show that a function f ∈ ZPoly k has a finite number of residuals, up to ∼ k-1 identification.

Lemma IV.8 (Finite residuals). Let k ≥ 0 and f ∈ ZPoly k , then the quotient set Res(f )/ ∼ k-1 is finite.

Remark IV.9. Example IV.3 exhibits a Z-rational series f such that Res(f )/ ∼ k is infinite for all k ≥ 0.

Finally, we note that ∼ k is decidable in ZPoly.

Claim IV.10 (Decidability). Given k ≥ -1 and f, g ∈ ZPoly, one can decide whether f ∼ k g holds.

Proof. Let f, g ∈ ZPoly. For k ≥ 0, f ∼ k g if and only if |(f -g)(w)| = O(|w| k
) and this property is decidable by Theorem III.3. For k = -1, we have f ∼ k g if and only if f = g, which is decidable by Corollary II.24.

B. Residual transducers

Now we intend to show that a function f ∈ ZPoly k can effectively be computed by a canonical machine, whose states are based on the finite set Res(f )/ ∼ k-1 , in the spirit of the residual automaton of a regular language. First, let us introduce an abstract notion of transducer which can call functions on suffixes of its input (this definition is inspired by the marble transducers of [START_REF] Douéneau-Tabot | Register transducers are marble transducers[END_REF], that call functions on prefixes).

Definition IV.11 (H-transducer). Let k ≥ 0 and H be a fixed subset of the functions A * → Z. A H-transducer T = (A, Q, q 0 , δ, H, λ, F ) consists of:

• a finite input alphabet A;

• a finite set of states Q with q 0 ∈ Q initial;

• a transition function δ :

Q × A → Q; • a labelling function λ : Q × A → H; • an output function F : Q → Z.
Given q ∈ Q, we define by induction on w ∈ A * the value T q (w) ∈ Z. For w = ε, we let T q (w) := F (q). Otherwise let T q (aw) := T δ(q,a) (w) + λ(q, a)(w). Finally, the function computed by the H-transducer T is defined as

T q0 : A * → Z.
Observe that all the functions T q are total.

Let us recall the standard definition of δ * via δ * (q, ua) := δ(δ * (q, u), a) and δ * (q, ε) = q. Using this notation, a simple induction shows that T q (w) = uav=w λ(δ * (q, u), a)(v) + F (δ * (q, w)). As a consequence, H-transducers are closely related to Cauchy products.

Example IV.12. We have depicted in Figure 3 a ZPoly -1transducer and a ZPoly 0 -transducer computing the function 1 aA * for A = {a, b}. The first one can easily be identified with the minimal automaton of 1 aA * (up to considering that a state is final if it outputs 1). The second one has a single state and it "hides" its computation into the calls to ZPoly 0 . One can check e.g. that 1 = 1 aA * (aab) = (1 - The reader may guess that every function f ∈ ZPoly k can effectively be computed by a ZPoly k-1 -transducer. We provide a stronger result and show that f can be computed by some specific ZPoly k-1 -transducer whose transition function is uniquely defined by Res(f )/ ∼ k-1 .

1 aA * (ab)) + (1 -1 aA * (b)) -1 aA * (ε) + 0. q0 0 q 1 1 q 2 0 a | 0 b | 0 a, b | 0 a, b | 0 (
Definition IV.13. Let k ≥ 0, let T = (A, Q, q 0 , δ, H, λ, F ) be a ZPoly k-1 -transducer and f : A * → Z. We say that T is a k-residual transducer of f if the following conditions hold:

• T computes f ; • Q = Res(f )/ ∼ k-1 ; • for all w ∈ A * , w ⊲ f ∈ δ * (q 0 , w); • λ(Q, A) ⊆ Span Z (Res(f )) ∩ ZPoly k-1 .
Given a regular language L, the 0-residual transducer of its indicator function 1 L can easily be identified with the minimal automaton of the language L, like in Example IV.12. However, for k ≥ 1, the k-residual transducer of f ∈ ZPoly k may not be unique. More precisely, two k-residual transducers share the same underlying automaton (A, Q, δ, λ), but the labels λ of the transitions may not be the same.

Example IV.14. The ZPoly -1 -transducer (resp. ZPoly 0transducer) from Figure 3

0 a | ((a ⊲ f ) -f ) : w → |w| b b | ((b ⊲ f ) -f ) : w → |w| a (a) A 2-residual transducer of f : w → |w|a|w| b . q0 0 q 1 -1 a | 0 a | ((aa ⊲ g) -g) : w → 2 × (-1) |w| (b) A 1-residual transducer of g : w → (-1) |w| |w|.
Fig. 4: Two residual transducers.

Q O ε ⊲ f f (ε) a ⊲ f f (a) b ⊲ f f (b) aa ⊲ f f (aa) a | 0 b | 0 a | 0 a | aa ⊲ f -b ⊲ f 0 1 2 3 f (aa) = [f (aa) -f (b)] + f (b)
Q = {ε ⊲ f }, O = {a ⊲ f, b ⊲ f }.
The red node is not created, and the blue transition is added instead, corresponding to the "else" branch line 10 of Algorithm 1. Now, let us describe how to build a k-residual transducer for any f ∈ ZPoly k . As an illustration of how Algorithm 1 works, we refer the reader to Figure 5.

Lemma IV.17. Let k ≥ 0. Given f : A * → Z such that Res(f )/ ∼ k-1 is finite, Algorithm 1 builds a k-residual transducer of f . Its steps are effective given f ∈ ZPoly k .

Remark IV. [START_REF] Thomas | Languages, automata, and logic[END_REF]. In Algorithm 1, we need to "choose" a way to range over the elements of O and the letters of A. Different choices may not lead to the same k-residual transducers.

Algorithm 1: Computing a k-residual transducer of f ∈ ZPoly k 1 O := {ε ⊲ f }; 2 Q := ∅; 3 while O = ∅ do 4 choose w ⊲ f ∈ O; 5 for a ∈ A do 6 if wa ⊲ f ∼ k-1 v ⊲ f for all v ⊲ f ∈ O ⊎ Q then 7 O := O ⊎ {wa ⊲ f }; 8 δ(w ⊲ f, a) := wa ⊲ f ; 9 λ(w ⊲ f, a) := 0; 10 else 11 let f ⊲ v ∈ O ⊎ Q be such that wa ⊲ f ∼ k-1 v ⊲ f ; 12 δ(w ⊲ f, a) := v ⊲ f ; 13 λ(w ⊲ f, a) := wa ⊲ f -v ⊲ f ;
Q := Q ⊎ {w ⊲ f }; 18 F (w ⊲ f ) := f (w); 19 end
We deduce from Lemma IV.17 that ZPoly k-1 -transducers describe exactly the class ZPoly k (Corollary IV. [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF]).

Corollary IV. [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF]. For all k ≥ 0, ZPoly k is the class of functions which can be computed by a ZPoly k-1 -transducer. Furthermore, the conversions are effective.

Corollary IV.20 (To be compared to Remark IV.5). For all k ≥ 0, ZPoly k = {f : A * → Z : Res(f )/ ∼ k-1 is finite}.

V. STAR-FREE Z-POLYREGULAR FUNCTIONS

In this section, we study the subclass of Z-polyregular functions that are built by using only FO-formulas, that we call star-free Z-polyregular functions. The term "star-free" will be justified in Theorem V.4. As observed in introduction, very little is known on deciding FO definability of functions (contrary to languages). The main result of this section shows that we can decide if a Z-polyregular function is star-free. Our proof crucially relies on the canonicity of the residual transducer introduced in Section IV. We also provide several characterizations of star-free Z-polyregular functions, that specialize the results of Section II. Definition V.1 (Star-free Z-polyregular). For k ≥ 0, we let Theorem V.4. Let f : A * → Z, the following are (effectively) equivalent:

ZSF k := Span Z ({#ϕ : ϕ ∈ FO ℓ , ℓ ≤ k}). Let ZSF := k ZSF k , it is the class of star-free Z-polyregular functions. We also let ZSF -1 := {0}. Similarly to ZPoly k , ZSF k = Span Z ({#ϕ : ϕ ∈ MSO k } ∪ {1 {ε} }).
1) f is a star-free Z-polyregular function;

2) f belongs to the smallest class of functions that contains the indicator functions of all star-free languages and is closed under taking external Z-products, sums and Cauchy products.

Proof. We apologize for the inconvenience of looking back at Proposition II.18 and noticing that the property holds mutatis mutandis for first-order formulas. In particular, one obtains the equivalent of Equation ( 1) of Theorem II.20

ZSF k = Span Z ({1 L0 ⊗ • • • ⊗ 1 L k : L 0 , . . . , L k star-free languages}) (3)
and the result follows.

Example V.5. The function 1 A * a ⊗ 1 A * : w → |w| a belongs to ZSF 1 , and the function 1

A * a ⊗ 1 A * ⊗ 1 bA * + 1 A * b ⊗ 1 A * ⊗ 1 aA * : w → |w| a × |w| b belongs to ZSF 2 .

A. Deciding star-freeness

Now, we intend to show that given a Z-polyregular function, we can decide if it is star-free. Furthermore, we provide a semantic characterization of star-free Zpolyregular functions leveraging ultimate N -polynomiality. We recall (see Definition II.29) that a function f : A * → Z is ultimately 1-polynomial when, for all α 0 , w 1 , α 1 , . . . , w ℓ , α ℓ ∈ A * , there exists

P ∈ Q[X 1 , . . . , X ℓ ], such that f (α 0 w X1 1 α 1 • • • w X ℓ ℓ α ℓ ) = P (X 1 , .
. . , X ℓ ), for X 1 , . . . , X ℓ large enough. Being ultimately 1-polynomial generalizes star-freeness for regular languages, as easily observed in Claim V.6.

Claim V.6. A regular language L is star-free if and only if

1 L is ultimately 1-polynomial. Example V.7. It is easy to see that w → |w| a × |w| b is ultimately 1-polynomial. As a counterexample, recall the map f : w → (-1) |w| × |w|. The map f is ultimately 2-polynomial because X → (-1) 2X+1 (2X + 1
) and X → (-1) 2X 2X are both polynomials. However, f is not ultimately 1-polynomial since X → (-1) X X is not a polynomial. Now, let us state the main theorem of this section. Theorem V.8. Let k ≥ 0 and f ∈ ZPoly k . The following properties are (effectively) equivalent:

1) f ∈ ZSF; 2) f ∈ ZSF k ;
3) f is 1-ultimately polynomial. Furthermore, this property is decidable.

Let us observe that Theorem V.8 implies an analogue of Theorem III.3 for the classes ZSF k . We conjecture that a direct proof of Corollary V.10 is possible. However, such a proof cannot rely on factorizations forests (that cannot be built in FO), and it would require a (weakened) notion of FO-definable factorization forest as that proposed in [START_REF] Colcombet | First-order separation over countable ordinals[END_REF]. The rest of Section V-A is devoted to sketching the proof of Theorem V.8. Given f ∈ ZPoly k , the main idea is to use its k-residual transducer to decide whether f ∈ ZSF k . Indeed, this transducer somehow contains intrinsic information on the semantic of f . We show that star-freeness faithfully translates to a counter-free property of the k-residual transducer, together with an inductive property on the labels of its transitions. [START_REF] Mcnaughton | Counter-Free Automata[END_REF]). We say that a H-transducer is counter-free if its underlying automaton is so.

Definition V.11 (Counter-free). A deterministic automaton

(A, Q, q 0 , δ) is counter-free if for all q ∈ Q, u ∈ A * , n ≥ 1, if δ(q, u n ) = q then δ(q, u) = q (see e.g.
Example V.12. The ZPoly 0 -transducer depicted in Figure 4b is not counter-free, since δ(q 0 , aa) = q 0 but δ(q 0 , a) = q 0 . Theorem V.8 is a direct consequence of the more precise Theorem V.13. Note that the semantic characterization (Item 2) is not a side result: it is needed within the inductive proof of equivalence between the other items. Theorem V.13. Let k ≥ 0 and f ∈ ZPoly k , the following conditions are equivalent:

1) f ∈ ZSF; 2) f is ultimately 1-polynomial;
3) for all k-residual transducer of f , this transducer is counter-free and has labels in ZSF k-1 ; 4) there exists a counter-free ZSF k-1 -transducer that computes f ;

5) f ∈ ZSF k .
Furthermore, this property is decidable and the constructions are effective.

The proof of Theorem V.13 will be done by induction on k ≥ 0. First, let us note that a counter-free transducer computes a star-free function (provided that the labels are starfree). Lemma V.14. Let k ≥ 0, a counter-free ZSF k-1 -transducer (effectively) computes a function of ZSF k .

We show that star-freeness implies ultimate 1-polynomiality. This result generalizes ultimately 1-polynomiality of the characteristic functions of star-free languages (see Claim V.6). Lemma V.15. Let f ∈ ZSF, then f is ultimately 1-polynomial.

Proof. From Claim V.6 we get that 1 L is ultimately 1polynomial if L is star-free. The result therefore immediately follows from Theorem V.4 and Lemma II.30.

Last but not least, we show that ultimate 1-polynomiality implies that any k-residual transducer is counter-free. Lemma V.16 is the key ingredient for showing Theorem V.13. Lemma V. [START_REF] Douéneau-Tabot | Pebble minimization: the last theorems[END_REF]. Let k ≥ 0. Let f ∈ ZPoly k which is ultimately 1-polynomial and T be a k-residual transducer of f . Then T is counter-free and its label functions are ultimately 1polynomial.

Proof of Theorem V. [START_REF] Berstel | Noncommutative rational series with applications[END_REF]. The (effective) equivalences are shown by induction on k ≥ 0. For Item 5 ⇒ Item 1, the implication is obvious. For Item 1 ⇒ Item 2 we apply Lemma V.15. For Item 2 ⇒ Item 3, we use Lemma V.16 which shows that any k-residual transducer of f is counterfree and has ultimately 1-polynomial labels. Since these labels are in ZPoly k-1 , then by induction hypothesis they belong to ZSF k-1 . For Item 3 ⇒ Item 4, the result follows because there exists a k-residual transducer computing f . For Item 4 ⇒ Item 5 we use Lemma V.14.

It remains to see that this property can be decided, which is also shown by induction on k ≥ 0. Given f ∈ ZPoly k , we can effectively build a k-residual transducer of f by Lemma IV.17. If it is not counter-free, the function is not star-free polyregular. Otherwise, we can check by induction that the labels belong to ZSF k-1 (since they belong to ZPoly k-1 ).

B. Relationship with polyregular functions and rational series

Let us now specialize the multiple characterizations of ZPoly presented in Section II to ZSF, which completes the third column of Table I.

Bojańczyk [7, page 13] introduced the notion of first-order (definable) polyregular functions. It is an easy check that starfree Z-polyregular functions are obtained by post composition with sum, in a similar way as Proposition II.13. Proposition V.17 Theorem V.18 (Star-free). Let f : A * → Z, the following are (effectively) equivalent:

1 Beware: the spectrum of a linear representation may not be a semigroup.

1) f is a star-free Z-polyregular function; 2) f is a Z-rational series and for all minimal linear representation (I, µ, F ) of f , Spec(µ(A * )) ⊆ {0, 1}; 3) f is a Z-rational series and there exists a linear representation (I, µ, F ) of f such that Spec(µ(A * )) ⊆ {0, 1}.

Proof. For Item 2 ⇒ Item 3, the result is obvious.

For Item 1 ⇒ Item 2, consider a minimal presentation of f using (I, µ, F ) of dimension n. Then consider a word w, λ a complex eigenvalue of µ(w). Thanks to Lemma II.28, there exists w, α i,j , u i , v j ∈ A * for 1 ≤ i, j ≤ n such that λ X = n i,j=1 α i,j f (v i w X u j ). Because f ∈ ZSF, f is ultimately 1-polynomial thanks to Theorem V.13. This entails that X → λ X is a polynomial for X large enough. Therefore, λ ∈ {0, 1}.

For Item 3 ⇒ Item 1, let us prove that the computed function is ultimately 1-polynomial, which is enough thanks to Theorem V.13. Because the eigenvalues of the matrix µ(w) ∈ M n,n (Z) for w ∈ A * are all in {0, 1}, its characteristic polynomial splits over Q, hence there exists P ∈ M n,n (Q) such that T := P M w P -1 is upper triangular with diagonal values in {0, 1}. In particular, µ(w) X = P -1 T X P , but a simple induction proves that the coefficients of T X are in Q[X] for large enough X, hence so does µ(w) X . Pumping multiple patterns at once only computes sums of products of polynomials, hence the function is ultimately 1-polynomial. Thanks to Theorem V.13, it is star-free Z-polyregular.

Remark V. [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF]. When showing Item 3 ⇒ Item 1, we have in fact shown that the following weaker form of ultimate 1-polynomiality characterizes ZSF among Z-rational series: for all u, w, v ∈ A * , there exists P ∈ Q[X], such that f (uw X v) = P (X), for X large enough.

Beware that Remark V.19 slightly differs from Remark II.33: the latter deals with a polynomial upper bound, whereas an equality is needed to characterize star-freeness.

Example V.20. Let u, v, w ∈ A * , then |1 odd (uw X v)| ≤ 1 for every X ≥ 0. However, 1 odd ∈ ZSF.
As a concluding example, let us observe that our notion of star-free Z-polyregular functions differs from the functions definable in the weighted first order logic introduced by Droste and Gastin [27, Section 4] when studying rational series.

Example V.21. Thanks to [27, Theorem 1], the map f : w → (-1) |w| |w| is definable in weighted first order logic (however, f ∈ ZSF as shown in Example V.7). Similarly, the indicator function 1 odd is also definable in weighted first order logic, even though the language of words of odd length is not starfree.

VI. OUTLOOK

This paper describes a robust class of functions, which admits several characterizations in terms of logics, rational expressions, rational series and transducers. Furthermore, two natural class membership problems (free variable minimization and first-order definability) are shown decidable. We believe that these results together with the technical tools introduced to prove them open the range towards a vast study of Zand Npolyregular functions. Now, let us discuss a few tracks which seem to be promising for future work.

Weaker logics: Boolean combinations of existential firstorder formulas define a well-known subclass of first-order logic, often denoted B(∃FO). Over finite words, B(∃FO)sentences describe the celebrated class of piecewise testable languages (see e.g. [START_REF] Perrin | First-order logic and star-free sets[END_REF]). In our quantitative setting, one could define for all k ≥ 0 the class of linear combinations of the counting formulas from B(∃FO) k , as we did for ZPoly k (resp. ZSF k ) with MSO k (resp. FO k ). While this class seems to be a good candidate for defining "piecewise testable Zpolyregular functions", it does not admit a free variable minimization theorem depending on the growth rate of the functions. Indeed, let A := {a, b} and consider the indicator function 1), this function cannot be written as a linear combination of counting formulas from B(∃FO) 0 . Indeed, if we assume the converse, then 1 aA * could be written n i=1 δ i 1 Li for some piecewise testable languages L i , which implies that aA * would be piecewise testable, which is not the case.

1 aA * = #ϕ for ϕ(x) := a(x)∧∀y.y ≥ x ∈ B(∃FO) 1 . Even if |1 aA * (w)| = O(

Star-free N-polyregular functions:

A very natural question is, given an N-polyregular function (recall that it is an element of NPoly := Span N (#ϕ : ϕ ∈ MSO)) to decide whether it is in fact a star-free N-polyregular function (i.e. an element of NSF := Span N (#ϕ : ϕ ∈ FO)). In this setting, we conjecture that NSF = NPoly ∩ ZSF. This question seems to be challenging. Indeed, the techniques introduced in the current paper cannot directly be applied to solve it, since the residual automaton (see Section V) of an N-polyregular function may need labels which are not N-polyregular, or even not nonnegative. In other words, replacing the output group by an output monoid seems to prevent from representing the functions with canonical objects based on residuals.

Star-free Z-rational series: In Figure 1, there is no generalization of the class ZSF among the whole class of Zrational series. We are not aware of a way to define a class of "star free Z-rational series", neither with logics nor with Z-rational expressions. Indeed, allowing the use of Kleene star for series automatically builds the whole class of Zrational series (including the indicator functions of all regular languages).

From a logical standpoint, it is tempting to go from polynomial behaviors to exponential ones by shifting from firstorder free variables to second-order free variables. While this approach actually captures the whole class of Z-rational series, it fails to circumscribe star-freeness. To make the above statement precise, let us write MSO X (resp. FO X ) as the set of MSO (resp. FO) formulas with free second-order variables, i.e. of the shape ϕ(X 1 , . . . , X k ). Given ϕ ∈ MSO X , we let #ϕ(w) : A * → Z be the function that counts second-order valuations. As an example of the expressiveness of this model, let us illustrate how to compute w → (-2) |w| ∈ ZPoly.

Example VI.1. Let ϕ(X) := ⊤, then #ϕ(w) = 2 |w| . Let ψ(X) be the first-order formula stating that X contains the first position of the word, X contains the last position of the word, and if x ∈ X, then x + 1 ∈ X and x + 2 ∈ X. It is an easy check that #ψ = 1 odd , even though ψ ∈ FO X (but recall that 1 odd is the indicator function of a non star-free regular language). Now, w → (-2) |w| equals #ϕ × (2#ψ -1).

We are now ready to explain formally how both FO X and MSO X capture Z-rational series.

Proposition VI.2. For every function f : A * → Z, the following are equivalent:

1) f is a Z-rational series; 2) f ∈ Span Z ({#ϕ : ϕ ∈ MSO X }); 3) f ∈ Span Z ({#ϕ : ϕ ∈ FO X }).
In our setting, it seems natural to say that w → 2 |w| should be a star-free Z-rational series, contrary to w → (-2) |w| (as observed in Example V.21, this approach contrasts with the weighted logics of Droste and Gastin [START_REF] Droste | Aperiodic weighted automata and weighted first-order logic[END_REF], for which (-2) |w| is considered as "star free"). Recall that in Theorem V.18, we have characterized ZSF as the class of series whose spectrum falls in {0, 1}. Following this result, we conjecture that a "good" notion of star-free Z-rational series could be those whose spectrum falls in the set R + of nonnegative real numbers. This way, exponential growth is allowed (e.g. for w → 2 |w| ) but no periodic behaviors (e.g. for w → (-2) |w| ).

First, observe that if f, g, h :

A * → Z and γ, δ ∈ Z, then (γf +δg) ⊗ h = γ(f ⊗ g)+δ(g ⊗ h).
Thus it is sufficient to show the result for f = #ϕ and g = #ψ with ϕ(x 1 , . . . , x k ) ∈ MSO k and ψ(y 1 , . . . , y ℓ ) ∈ MSO ℓ . For all w ∈ A * we have:

(#ϕ ⊗ #ψ)(w) = 0≤i≤|w| i1,...,i k ≤i j1,...,j ℓ >i 1 w[1:i]|=ϕ(i1,...,i k ) × 1 w[i+1:|w|]|=ψ ′ (j1,...,j ℓ ) = #ϕ(ε) • #ψ(w) + 1≤i≤|w| i1,...,i k ≤i j1,...,j ℓ >i 1 w[1:i]|=ϕ(i1,...,i k ) × 1 w[i+1:|w|]|=ψ ′ (j1,...,j ℓ ) = #ϕ(ε) • #ψ(w) + #(ϕ ′ (z, x 1 , . . . , x k ) ∧ ψ ′ (z, y 1 , . . . , y l ))(w)
where ϕ ′ (z, x 1 , . . . , x k ) ∈ MSO k+1 is a formula such that w |= ϕ ′ (i, i 1 , . . . , i k ) if and only if i 1 , . . . , i k ≤ i and w[1:i] |= ϕ(i 1 , . . . , i k ) (this is a regular property which is MSO definable), and similarly for ψ ′ .

B. Proof of Proposition II.18

Let k ≥ 0, we want to show that

ZPoly k+1 = Span Z ({1 L ⊗ f : L regular, f ∈ ZPoly k }). Observe that for all f : A * → Z, 1 {ε} ⊗ f equals f , therefore ZPoly k ⊆ Span Z ({1 L ⊗ f : L regular, f ∈ ZPoly k }).
As in the proof of Claim II.17, it is sufficient to show that #ϕ for ϕ(x 1 , . . . , x k+1 ) ∈ MSO k+1 , can be written as a linear combination of 1 L ⊗ f where L is a regular language. Observe that for all w ∈ A + , for all valuation i 1 , . . . , i k of x 1 , . . . , x k , we can define P := {1 ≤ j ≤ k : i j = min{i 1 , . . . , i k }} (i.e. the x j for j ∈ P are the variables with minimal value). Therefore, for all w ∈ A + :

#ϕ(w) = ∅ P ⊆[1:k] w=uv,u =ε #(ϕ ∧ j∈P x j = |u| ∧ j ∈P x j > |u|)(w).
It is an easy check that one can (effectively) build a regular language L P ⊆ A + and a formula ψ P such that for all u ∈ A + , v ∈ A * , uv |= ϕ ∧ j∈P (x j = |u|) ∧ ( j ∈P x j > |u|) if and only if u ∈ L P and v |= ψ P ((x j ) j ∈P ). Thus, for all w ∈ A + :

#ϕ(w) = ∅ P ⊆[1:k] w=uv 1 L P (u) × #ψ P (v) = ∅ P ⊆[1:k] (1 L P ⊗ #ψ P ) :=g (w) .
Notice that ψ P has exactly k -|P | ≤ k -1 free-variables, thus g belongs to Span Z ({1 L ⊗ f : L regular, f ∈ ZPoly k }). Observe moreover that g(ε) = 0 = #ϕ(ε) because k + 1 > 0.

APPENDIX C PROOFS OF SECTION II-D

A. Proof of Lemma II.28

Let f : A * → Z be a Z-rational series and (I, µ, F ) be a minimal Z-linear representation of f of dimension n. First note that (I, µ, F ) is also a minimal Q-linear representation of f by [13, Theorem 1.1 p 121] (Q-linear representations are defined by allowing rational coefficients whithin the matrices and vectors, instead of integers). Let w ∈ A * , λ ∈ Spec(µ(w)) and consider a complex eigenvector V ∈ M n,1 (C) associated to λ. We let ||V || := t V V , observe that it is a positive real number. Because (I, µ, F ) is a minimal Q-linear representation of f , then Span Q ({µ(u)F : u ∈ A * }) = Q n by [13, Proposition 2.1 p 32]. Hence there exists numbers α j ∈ C and words u j ∈ A * such that V = n j=1 α j µ(u j )F . Symmetrically by [13, Proposition 2.1 p 32], there exists numbers β i ∈ C and words v i ∈ A * such that t V = n i=1 β i Iµ(v i ). Therefore:

λ X ||V || = t V µ(w) X V = n i,j=1 α i β j Iµ(v i w X u j )F = n i,j=1 α i β j f (v i w X u j ).
The result follows since ||V || = 0 (it is an eigenvector).

B. Proof of Lemma II.30

If L is a regular language, the fact that 1 L is N -polynomial for some N ≥ 0 follows from the traditional pumping lemmas. Now let f, g : A * → Z be respectively ultimately N 1 -polynomial and ultimately N 2 -polynomial. The fact that f + g and δf for δ ∈ Z are ultimately (N 1 × N 2 )polynomial is obvious. In the rest of Section C-B, we focus on the main difficulty which is the Cauchy product of two functions. For that, we will first prove the following claim about Cauchy products of polynomials.

Claim C.1. For every p ∈ N, X i=0 i p is a polynomial in X. Proof. It is a folklore result, but let us prove it using finite differences. If f : N → Q, let ∆f : n → f (n + 1) -f (n). Let us now prove by induction that every function f : N → Q such that ∆ p f = 0 for some p ≥ 1 is a polynomial. For p = 1, this holds because f must be constant. For p + 1 > 1, if we assume that ∆ p+1 f = 0, then ∆ p f is a constant C. Let g := f -C n p p! , and remark that ∆ p g = 0. By induction hypothesis g is a polynomial, hence so is f . Finally, a simple induction proves that ∆ p+2 (X →

X i=0 i p ) = 0. Claim C.2. Let P, Q ∈ Q[X, Y 1 , . . . , Y ℓ ] be two multivariate polynomials, then their Cauchy product P ⊗ Q(X, Y 1 , . . . , Y ℓ ) := X i=0 P (i, Y 1 , . . . , Y ℓ )Q(Y -i, Y 1 , . . . , Y ℓ ) belongs to Q[X, Y 1 , . . . , Y ℓ ].
Proof. By linearity of the Cauchy product, it suffices to check that the result holds for products of the form

(X p Y p1 1 • • • Y p ℓ ℓ ) ⊗(X q Y q1 1 • • • Y q ℓ ℓ ) = (X p ⊗ X q )×Y p1 1 • • • Y p ℓ ℓ Y q1 1 • • • Y q ℓ ℓ .
Hence, the only thing left to check is that X p ⊗ X q is a polynomial in X.

X p ⊗ X q (Y ) = Y i=0 i p (Y -i) q = Y i=0 i p q k=0 q k Y k (-i) q-k = q k=0 q k Y k Y i=0 i p (-i) q-k = q k=0 q k (-1) q-k Y k Y i=0 i p+q-k
Which is a polynomial thanks to Claim C.1.

Let us now prove that f ⊗ g is ultimately N := (N 1 ×N 2 )-polynomial. For that, let us consider α 0 , u 1 , α 1 , . . . , u ℓ , α ℓ ∈ A * and prove that (f ⊗ g)(α 0 u N X1

1 α 1 • • • u N X ℓ ℓ α ℓ ) is a polynomial for X 1 , . . . , X ℓ large enough. (f ⊗ g)(α 0 u N X1 1 α 1 • • • u N X ℓ ℓ α ℓ ) = f (α 0 u N X1 1 α 1 • • • u N X ℓ ℓ α ℓ )g(ε) + ℓ j=0 |αj |-1 i=0 f (α 0 u N X1 1 α 1 • • • u N Xj j (α j [1:i])) × g((α j [i+1:|α j |])u N Xj+1 j+1 • • • α ℓ ) + ℓ j=1 |u N j |-1 i=0 Xj -1 Y =0 f (α 0 u N X1 1 α 1 • • • u N Y j (u N j [1:i]))× g((u N j [i+1:|u N j |])u N (Xj -Y -1) j • • • α ℓ )
From the hypothesis on f , we deduce that the first term of this sum is ultimately N 1polynomial, hence ultimately N -polynomial. We conclude similarly for the second term of this sum, because the product of two polynomials is a polynomial.

Let us now focus on the third term. Using the induction hypotheses on f and g, there exists polynomials P j,i and Q j,i such that the following equalities ultimately hold, where (X 1 , . . . , Xj , . . . X ℓ ) denotes the tuple obtained by removing the j-th element from (X 1 , . . . , X ℓ ):

f (α 0 u N X1 1 α 1 • • • u N Y j (u N j [1:i])) = P j,i (Y, X 1 , . . . , Xj , . . . X ℓ ) g((u N j [i+1:|u N j |])u N (Xj -Y -1) j • • • α ℓ ) = Q j,i (Y, X 1 , . . . , Xj , . . . X ℓ )
As a consequence, we can rewrite the third term as a Cauchy product of polynomials for large enough values of X 1 , . . . , X ℓ :

ℓ j=1 |u N j |-1 i=0 Xj -1 Y =0 f (α 0 u N X1 1 α 1 • • • u N Y j (u N j [1:i]))g((u N j [i+1:|u N j |])u N (Xj -Y -1) j • • • α ℓ ) = ℓ j=1 |uj |-1 i=0 Xj -1 Y =0 P j,i (Y, X 1 , . . . , Xj , . . . , X ℓ )Q j,i (X j -Y -1, X 1 , . . . , Xj , . . . , X ℓ ) = ℓ j=1 |uj |-1 i=0 P i,j ⊗ Q j,i (X j -1)
Thanks to Claim C.2, we conclude that this third term is also ultimately a polynomial.

APPENDIX D PROOFS OF SECTION III

A. Proof of Lemma III.14

First of all, given a leaf x ∈ Leaves(F ), Skel(x) = {x} contains x. Hence, every leaf is contained in at least one skeleton. It remains to show that if t and t ′ are two nodes such that x ∈ Skel(t) and x ∈ Skel(t ′ ), then Skel(t) ⊆ Skel(t ′ ) or the converse holds.

As Skel(t) contains only children of t, one deduces that x is a children of both t and t ′ . Because F is a tree, parents of x are totally ordered by their height in the tree. As a consequence, without loss of generality, one can assume that t is a parent of t ′ . Because Skel(t) is a subforest of F containing x, it must contain t ′ . Now, by definition of skeletons, it is easy to see that whenever t ′ ∈ Skel(t), we have Skel(t ′ ) ⊆ Skel(t).

B. Proof of Claim III.18

Let x ∈ Leaves(F ), we show that the number of x ′ such that x ′ depends-on x is bounded (independently from x and F ∈ F µ d ). Observe that skel-root(x ′ ) is either an ancestor or the sibling of an ancestor of skel-root(x). Observe that for all t ∈ Nodes(F ), Skel(t) is a binary tree of height at most d, thus is has at most 2 d leaves. Moreover, skel-root(x) has at most d ancestors and 2d immediate siblings of its ancestors. As a consequence, there are at most 3d×2 d leaves that depend on x.

C. Proof of Lemma III.19

Let d ≥ 0, M be a finite monoid, µ : A * → M , k ≥ 1, and ψ ∈ INV k . We want to build a function g ∈ ZPoly k-1 such that for every F ∈ F µ d , g(F ) = #(ψ( x) ∧ sym-dep( x))(F ) (since F µ d is a regular language of  * , it does not matter how g is defined on inputs F ∈ F µ d ).

First, we use the lexicographic order to find the first pair (x i , x j ) that is dependent in the tuple x. This allows to partition our set of valuations as follows:

{ x ∈ Leaves(F ) : F, x |= ψ ∧ sym-dep( x)} = 1≤i<j≤n { x ∈ Leaves(F ) : F, x |= ψ ∧ sym-dep(x i , x j ) ∧ (k,ℓ)<lex(i,j) ¬ sym-dep(x k , x ℓ )} = 1≤i<j≤n { x ∈ Leaves(F ) : F, x |= ψ ∧ x j depends-on x i ∧ (k,ℓ)<lex(i,j) ¬ sym-dep(x k , x ℓ ) :=ψ i→j ( x) } ∪ { x ∈ Leaves(F ) : F, x |= ψ ∧ x i depends-on x j ∧ (k,ℓ)<lex(i,j) ¬ sym-dep(x k , x ℓ ) :=ψ i←j ( x) } As a consequence, #(ψ ∧ sym-dep) = 1≤i<j≤n #ψ i→j + #ψ i←j -#ψ i→j ∧ ψ i←j (
the last term removes the cases when both x i depends-on x j and x j depends-on x i , which occurs e.g. when x i = x j ).

We can now rewrite this sum using ∃ =ℓ x j .ψ to denote the fact that there exists exactly ℓ different values for x so that ψ(. . . , x j , . . . ) holds (this quantifier is expressible in MSO at every fixed ℓ). Thanks to Claim III.18, there exists a bound N d over the maximal number of leaves that dependent on a leaf x i (among forests of depth at most d.) Hence:

#(ψ ∧ sym-dep) = 1≤i<j≤n #ψ i→j + #ψ i←j -#ψ i→j ∧ ψ i←j = 1≤i<j≤n 0≤ℓ≤N d ℓ • #∃ =ℓ x j .ψ i→j + 1≤i<j≤n 0≤ℓ≤N d ℓ • #∃ =ℓ x i .ψ i←j - 1≤i<j≤n 0≤ℓ≤N d ℓ • #∃ =ℓ x i .ψ i→j ∧ ψ i←j

D. Proof of Lemma III.23

In order to prove Lemma III.23, we consider f such that f indep = 0. Our goal is to construct a pumping family to exhibit a growth rate of f indep . To construct such a pumping family, we will rely on the fact that independent tuples of leaves have a very specific behavior with respect to the factorization forest. Given a node t, we write start(t) := min ≤ {y ∈ Leaves(F ) ∩ Skel(t)} and end(t) := max ≤ {y ∈ Leaves(F ) ∩ Skel(t)}.

Claim D.1. Let x 1 , . . . , x k be an independent tuple of k ≥ 1 leaves in a forest F ∈ F µ d factorizing a word w. Let t be the vector of nodes such that t i := skel-root(x i ) for all 1 ≤ i ≤ k. One can order the t i according to their position in the word w so that 1 < start(t 1 ) ≤ end(t 1 ) <

• • • < start(t k ) ≤ start(t k ) < |w|.
Proof. Assume by contradiction that there exists a pair i < j such that start(t j ) ≥ end(t i ). We then know that start(t i ) ≤ start(t j ) ≤ end(t i ). In particular, skel-root(start(t i )) = t i is an ancestor of start(t j ), hence t i is an ancestor of t j . This contradicts the independence of x.

Assume by contradiction that there exists i such that start(t i ) = 1 (resp. end(t i ) = |w|). Then skel-root(x i ) must be the root of F , but then x cannot be an independent tuple. Given an independent tuple x 1 , . . . , x k ∈ Leaves(F ), with skel-root( x) = t, ordered by their position in the word, let us define m

0 := µ(w[1: start(t 1 )-1]), m k := µ(w[end(t k )+1:w |w| ]) and m i := µ(w[end(t k )+1: start(t i+1 )-1]) for 1 ≤ i ≤ k -1.
Definition D.2 (Type of a tuple of skel-root). Let F ∈ F µ d factorizing a word w, x be an independent tuple of leaves in F , and t = skel-root( x). Without loss of generality assume that the nodes are ordered by start. The type s-type( t) in the forest F is defined as the tuple (m 0 , Skel(t 1 ), m 1 , . . . , m k-1 , Skel(t k ), m k ).

At depth d, there are finitely many possible types for tuples of k nodes, which we collect in the set Types d,k . Moreover, given a type T ∈ Types d,k , one can build the MSO formula has-s-type T ( t) over F µ d that tests whether a tuple of nodes t is of type T , and can be obtained as skel-root( x) for some tuple x of independent leaves. The key property of types is that counting types is enough to count independent valuations for a formula ψ ∈ INV.

Claim D.3. Let k ≥ 1, d ≥ 0, M be a finite monoid, µ : A * → M be a morphism. Let T ∈ Types d,k , F ∈ F µ d ,
x and y be two k-tuples of independent leaves of F such that s-type(skel-root(x 1 ), . . . , skel-root(x k )) = s-type(skel-root(y 1 ), . . . , skel-root(y k )) = T . There exists a bijection σ :

L 1 → L 2 , where L 1 := Leaves(F ) ∩ k i=1 Skel(skel-root(x i )) and L 2 := Leaves(F ) ∩ k i=1 Skel(skel-root(y i )), such that for every z ∈ L k 1 , for every formula ψ ∈ INV k , F |= ψ(z) if and only if F |= ψ(σ(z)).
Proof Sketch. Because of the type equality, we know that Skel(skel-root(x i )) and Skel(skel-root(y i )) are isomorphic for 1 ≤ i ≤ k. As the skeletons are disjoint in an independent tuple, this automatically provides the desired bijection σ.

Let us now prove that σ preserves the semantics of invariant formulas. Notice that this property is stable under disjunction, conjunction and negation. Hence, it suffices to check the property for the following three formulas between m (x, y), left m (x), right m (y) and isleaf(x). For isleaf, the result is the consequence of the fact that σ sends leaves to leaves.

Let us prove the result for between m and leave the other and leave the other cases as an exercise. Let (y, z) ∈ L 2 1 . By definition of L 1 , there exists 1 ≤ i, j ≤ k such that y ∈ Leaves(F )∩ Skel(skel-root(x i )) and z ∈ Leaves(F ) ∩ Skel(skel-root(x j )). To simplify the argument, let us assume that y < z and i + 1 = j. Let w := forest(F ), and m y,z := µ(w[y : z]). One can decompose the computation of m y,z as follows:

m y,z = µ(w[y : z]) = µ(w[y : end(x i )]w[end(x i ) + 1 : start(x i+1 ) -1]w[start(x i+1 ) : z]) = µ(w[y : end(x i )])m i µ(w[start(x i ) : z])
Therefore, µ(w[y : z]) only depends on Skel(skel-root(y)) = Skel(skel-root(x i )), the position of y in Skel(skel-root(y)), Skel(skel-root(z)) = Skel(skel-root(x i+1 )), the position of z in Skel(skel-root(z)), and m i , all of which are presreved by the bijection σ. Hence, µ(w[y : z]) = µ(w[σ(y) : σ(z)]). Therefore, F |= between m (y, z) if and only if F |= between m (σ(y), σ(z)).

It is an easy check that a similar argument works when j = i + 1. Now, we show that counting the valuations of a INV formula can be done by counting the number of tuples of each type.

Lemma D.4. Let k ≥ 1, d ≥ 0, M be a finite monoid, µ : A * → M be a morphism. For every ψ ∈ INV k , there exists computable coefficients λ T ≥ 0, such that the following functions from F µ d to N are equal:

#ψ indep := #(ψ ∧ ¬ sym-dep) = T ∈Types d,k λ T • #has-s-type T Proof.
Using the claim, we can now proceed to prove Lemma D.4.

#ψ ∧ ¬ sym-dep(F ) = x indep 1 F |=ψ( x) = T ∈Types d,k t∈Nodes(F ) x indep 1 F |=ψ( x) 1 t=skel-root( x) 1 has-s-type T ( t) = T ∈Types d,k t∈Nodes(F ) 1 has-s-type T ( t)   x indep 1 F |=ψ( x) 1 t=skel-root( x)   = T ∈Types d,k t∈Nodes(F ) 1 has-s-type T ( t) λ T = T ∈Types d,k λ T #(has-s-type T ( t))
The coefficient λ T does not depend on the specfic t such that s-type( t) = T thanks to Claim D.3 and the fact that ψ ∈ INV.

The behavior of the formulas has-s-type T is much more regular and enables us to extract pumping families that clearly distinguishes different types. Namely, we are going to prove that given k ≥ 1, d ≥ 0, a finite monoid M , and a morphism µ : A * → M , {#has-s-type T : T ∈ Types d,k } is a Z-linearly independent family of functions from F µ d to Z.

Lemma D.5 (Pumping Lemma). For all T ∈ Types d,k , there exists a pumping family (w X , F X ) such that for every type T ′ ∈ Types d,k , #( has-s-type T ′ )(F X ) is ultimately a Z-polynomial in X that has non-zero coefficient for X 1 • • • X n if and only if T = T ′ .

Proof. Let T ∈ Types d,k be a type, it is obtained as the type of some tuple x of independent leaves in some F ∈ F µ d factorizing a word w. Let t i := skel-root(x i ) and S i := Skel(t i ) for 1 ≤ i ≤ k. Recall that µ(word(S i )) = µ(word(t i )) thanks to Claim III.13. As a consequence, S i is a subforest of t i that provides a valid µ-forest of a subword of word(t i ). Now, as t i cannot be the root of the forest F and is the highest ancestor of x i that is not a leftmost or rightmost child, it must be the immediate inner child of an idempotent node in F . As a consequence, µ(word(S i )) = µ(word(t i )) is an idempotent. Therefore, for ever X i ∈ N, the tree obtained by replacing t i with X i copies of S i in F is a valid µ-forest. We write F X for the forest F where t i is replaced by X i copies of S i . This is possible because the tuple x is composed of independent leaves, hence t i and t j are disjoint subtrees of F whenever

1 ≤ i = j ≤ k.
Hence, F X is the factorization forest of the word w X := α 0 (w 1 ) X1 α 1 . . . α k-1 (w k ) X k α k where w i = word(S i ), α i = w[end(t i )+1: start(t i )-1] for 2 ≤ i ≤ k -1, α 0 = w[1: start(t 1 )-1], and α k = w[end(t k )+1:|w|] are non-empty factors of w.

We now have to understand the behavior of has-s-type T ′ over F X , for every T ′ ∈ Types d,k . To that end, let us consider T ′ ∈ Types d,k . Let us write E for the set of nodes in F X that are not appearing in any of the X i repetitions of S i , for 1 ≤ i ≤ k. The set E has a size bounded independently of X 1 , . . . , X k . To a tuple s such that F X |= has-s-type T ′ (s), one can associate the mapping ρ s : {1, . . . , k} → {1, . . . , k} ⊎ E, so that ρ s (i) = s i when s i ∈ E, and ρ s (i) = j when s i is a node appearing in one of the X j repetitions of the skeleton S j (there can be at most one j satisfying this property).

Remark D.6. If s-type( s) = T ′ , and ρ s (i) = j, then s i must be the root of one of the X j copies of S j in F X . Indeed, t is obtained as skel-root( y) for some independent tuple y of leaves. Hence, s i = skel-root(y i ) which belong to some copy of S j , hence s i must be the root of this copy of S j , because S j is a binary tree.

Given a map ρ : {1, . . . k} → {1, . . . , k} ⊎ E and a tuple X ∈ N k , we let C ρ ( X) be the set of tuples s of nodes of F X such that s-type( s) = T ′ , and such that ρ s = ρ. This allows us to rewrite the number of such vectors as a finite sum: #( has-s-type T ′ ( t))(F X ) = ρ : {1,...,k}→{1,...,k}⊎E #C ρ ( X) Claim D.7. For every ρ : {1, . . . , k} → {1, . . . , k} ⊎ E, #C ρ ( X) is ultimately a Z-polynomial in X. Moreover, its coefficient for X 1 • • • X k is non-zero if and only if ρ(i) = i for 1 ≤ i ≤ k.

Proof. Assume that C ρ ( X) is non-empty. Then choosing a vector s ∈ C ρ ( X) is done by fixing the image of s i to ρ(i) when ρ(i) ∈ E, and selecting p j := |ρ -1 ({j})| non consecutive copies of S j among among the X j copies available. All nodes are accounted for since Remark D.6 implies that whenever s i is in a copy of S j , then s i is the root of this copy, and since s is independent, they cannot be direct siblings.

The number of ways one can select p non consecutive nodes in among X nodes is (for large enough X) the binomial number X-p+1 p , as it is the same as selecting p positions among X -p + 1 and then adding p -1 separators.

As a consequence, the size of C ρ ( X) is ultimately a product of Xj -pj +1 pj for the non-zero p j , which is a Z-polynomial in X 1 , . . . , X k . Moreover, it has a non-zero coefficient for X 1 . . . X k if and only if p j = 0 for 1 ≤ j ≤ k, which is precisely when ρ(i) = i.

We have proven that #( has-s-type T ′ )(F X ) is a Z-polynomial in X 1 , . . . , X k , and that the only term possibly having a non-zero coefficient for X 1 • • • X k is #C id ( X). Notice that if #C id ( X) is non-zero, we immediately conclude that T = T ′ . Claim D.8. Let P ∈ R[X 1 , . . . , X n ] which evaluates to 0 over N n , then P = 0.

Proof. The proof is done by induction on the number n of variables. If P has one variable and P |N = 0, then P has infinitely many roots and P = 0. Now, let P having n + 1 variables, and such that P (x 1 , . . . , x n , x n+1 ) = 0 for all (x 1 , . . . , x n+1 ) ∈ N n+1 . By induction hypothesis, P (X 1 , . . . , X n , x n+1 ) = 0 for all x n+1 ∈ N. Hence for all x 1 , . . . , x n ∈ R, P (x 1 , . . . , x n , X n+1 ) is a polynomial with one free variable having infinitely many roots, hence P (x 1 , . . . , x n , x n+1 ) = 0 for every x n+1 ∈ R. We have proven that P = 0.

We now have all the ingredients to prove Lemma III.23, allowing us to pump functions built by counting independent tuples of invariant formulas.

Let k ≥ 1, and f indep be a linear combination of #ψ i ∧ ¬ sym-dep, where ψ i ∈ INV k . Assume moreover that f indep = 0. Thanks to Lemma D.4, every #ψ i ∧ ¬ sym-dep can be written as a linear combination of #has-s-type T ( t), hence f indep = T ∈Types d,k λ T #has-s-type T , and the coefficients λ T (now in Z) are computable.

Since f indep = 0, there exists T ∈ Types d,k such that λ T = 0. Using Lemma D.5, there exists a pumping family (w X , F X ) adapted to T . In particular, f (F X ) is ultimately a Z-polynomial in X, and its coefficient in X 1 • • • X k is the sum of the coefficients in X 1 • • • X k of the polynomials #has-s-type T ′ (F X ) multiplied by λ T ′ . This coefficient is non-zero if and only if T = T ′ . Hence, f (F X ) is ultimately a Z-polynomial with a non-zero coefficient for X

1 • • • X k .
As a side result, we have proven that a linear combination of #has-s-type T is the constant function 0 if and only if all the coefficient are 0, which is decidable since one can enumerate all the elements of Types d,k . For the converse implication, one leverages Claim D.8: if one coefficient is non-zero, then the polynomial f (F X ) must be non-zero.

Fig. 1 :

 1 Fig. 1: The classes of functions studied in this paper.

  |w| i=1 w[i]. Proposition II.13. The class ZPoly is (effectively) the class of functions sum •f where f : A * → {±1} * is polyregular.

Definition IV. 1 (

 1 Residual). Given f : A * → Z and u ∈ A * , we define the function u ⊲ f : A * → Z, w → f (uw). We let Res(f ) := {u ⊲ f : u ∈ A * } be the set of residuals of f . Example IV.2. The residuals of the function w → |w| 2 are the functions w → |w| 2 + 2n|w| + n 2 for n ≥ 0. Example IV.3. The residuals of the function w → (-2) |w| are the functions w → (-2) n+|w| for n ≥ 0. It is easy to see that u → u ⊲ f defines a monoid action of A * over A * → Z. Let us observe that this action (effectively) preserves the classes of functions ZPoly k . Claim IV.4. Let k ≥ 0, f ∈ ZPoly k and u ∈ A * . Then u ⊲ f ∈ ZPoly k and this result is effective. Remark IV.5 ([13, Corollary 5.4 p 14]). Let f : A * → Z, this function is a Z-rational series if and only if Span Z (Res(f )) has finite dimension.

0 a | 1 -Fig. 3 :

 013 Fig. 3: Two transducers computing 1 aA * .

  is a 0-residual transducer (resp. 1residual transducer) of 1 aA * . Let us check it for the 1-residual transducer. First note that b ⊲ 1 aA * ∼ 0 a ⊲ 1 aA * ∼ 0 1 aA * , hence | Res(1 aA * )/ ∼ 0 | = 1. Thus a 1-residual transducer of 1 aA * has exactly one state q 0 . Furthermore the labels of the transitions of our transducer belong to λ(Q, A) ⊆ Span Z (Res f (a)) since 1 -1 aA * = (a ⊲ 1 aA * ) -1 aA * . Example IV.15. Let A := {a, b}. The function f : w → |w| a × |w| b ∈ ZPoly 2 has a single residual up to ∼ 1 -equivalence. A 2-residual transducer of f is depicted in Figure 4a. Example IV.16. Let A := {a}. The function g : w → (-1) |w| × |w| ∈ ZPoly 1 has two residuals up to ∼ 0 -equivalence. A 1-residual transducer of g is depicted in Figure 4b.

  q0

Fig. 5 :

 5 Fig. 5: Example of a partial execution of Algorithm 1 to build a k-residual transducer of a function f : A * → Z such that aa ⊲ f ∼ k b ⊲ f . Nodes are labelled by their creation time. At this stage, Q= {ε ⊲ f }, O = {a ⊲ f, b ⊲ f }.The red node is not created, and the blue transition is added instead, corresponding to the "else" branch line 10 of Algorithm 1.

16 O

 16 := O {w ⊲ f };

17

 17

Example V. 2 .

 2 ZSF 0 is exactly the set of functions of the form i δ i 1 Li where the δ i ∈ Z and the 1 Li are indicator functions of star-free languages (compare with Example II.8). Example V.3. The function w → |w| a × |w| b is in ZSF 1 . Indeed, the formulas given in Example II.3 are in FO. Now, we give an analogue of Theorem II.20 that characterizes ZSF as Z-rational expressions based on indicators of star-free languages, forbidding the use of the Kleene star.

Corollary V. 9 .

 9 ZSF k = ZSF ∩ ZPoly k . Corollary V.10 (FO free variable minimization). Let f ∈ ZSF, then f ∈ ZSF k if and only if |f (w)| = O(|w| k ). This property is decidable and the construction is effective. Proof. Let f ∈ ZSF be such that |f (w)| = O(|w| k ). By Theorem III.3 we get f ∈ ZPoly k , thus by Theorem V.8, f ∈ ZSF k . All the steps are effective and decidable.

.

  The class ZSF is (effectively) the class of functions sum •f where f : A * → {±1} * is first-order polyregular. Now, let us provide a description of ZSF in terms of eigenvalues in the spirit of Theorem II.31. Intuitively, it shows that a linear representation (I, µ, F ) computes a function in ZSF if and only if Spec(µ(A * )) contains no non-trivial subgroup, mimicking the notion of aperiodicity for monoids1 .

E

  . Proof of Lemma III.[START_REF] Colcombet | Green's relations and their use in automata theory[END_REF] Let P, Q ∈ R[X 1 , . . . , X n ] be such that |P | = O(|Q|). We show that deg(P ) ≤ deg(Q). If P = 0, then deg(P ) ≤ deg(Q). Otherwise, let us write P = P 1 + P 2 with P 1 containing all the terms of degree exactly deg(P) in P . Because |P | = O(|Q|), there exists N ≥ 0 and C ≥ 0 such that |P (x 1 , . . . , x n )| ≤ C|Q(x 1 , . . . , x n )| for all x 1 , . . . , x n ∈ N such that x 1 , . . . , x n ≥ N .Because P 1 is a non-zero polynomial, there exists a tuple (x 1 , . . . , x n ) ∈ N \ {0} such that α := P 1 (x 1 , . . . , x n ) = 0 (Claim D.8). Let us now consider R(Y) := P (Y x 1 , . . . , Y x n ) ∈ R[Y ],and S(Y) := Q(Y x 1 , . . . , Y x n ) ∈ R[Y ]. Notice that R(Y )has degree exactly deg(P ) and its term of degree deg(P ) is αY deg(P ) . Furthermore, S(Y ) is a polynomial in Y of degree at most deg(Q), with dominant coefficient β = 0. We know that for Y large enough, |R(Y )| ≤ C|S(Y )|. Since |R(Y )| ∼ +∞ |α|Y deg(P ) , and |S(Y )| ∼ +∞ |β|Y deg(S) ≤ |β|Y deg(Q) , we conclude that deg(P ) ≤ deg(Q).

TABLE I :

 I Summary of the characterizations of ZPoly and ZSF expressed in different formalisms.

∈ ZPoly k+ℓ whenever f ∈ ZPoly k and g ∈ ZPoly ℓ .

	Corollary 2.6 p 159]. Furthermore
	polynomial growth is decidable by [13, Corollary 2.4 p 159].
	To provide an effective translation, one can start from a Z-
	rational series f of polynomial growth, enumerate all the Z-
	polyregular functions g, rewrite them as rational series (using
	Item 1 ⇒ Item 2) and check whether f = g since this property
	can be decided for Z-rational series [13, Corollary 3.6 p 38].
	Remark II.21. It follows from Remark II.6, [11, Proposition
	6.1], and Theorem II.20, that Z-rational series of polynomial
	growth are exactly those computable by weigthed automata
	with coefficients in {0, 1, -1} of polynomial ambiguity. We
	are not aware of a direct proof of this correspondence.
	Remark II.22. [19, Theorem 3.3] gives a similar result when
	comparing N-polyregular functions and N-rational series.
	Remark II.23. The class of Z-polyregular functions is also
	closed under Hadamard product (f × g(w) := f (w) × g(w)).
	This can be obtained by generalising Example II.4. Moreover,
	f × g Since the equivalence is decidable for Z-rational series [13,
	Corollary 3.6 p 38], we obtain the following.
	Corollary II.24 (Equivalence problem). One can decide if two
	Z-polyregular functions are equal.

  |= right m (x) if and only if x is a leaf of F , and µ(w[x] . . . w[|w|]) = m. Whenever F ∈ Â * \ F µ d , the semantics are undefined. Definition III.10. The fragment INV is a subset of MSO over Â, which contains the quantifier-free formulas using only the predicates between m , left m , and right m where m ranges over M , and where every free variable x is guarded by the predicate isleaf(x). Furthermore, we let INV k := INV∩MSO k .

	Claim III.11 ([15],

y) if and only if x and y are leaves of F , x ≤ y, and µ(w[x] . . . w[y]) = m; • F |= left m (x) if and only if x is a leaf of F , and µ(w[1] . . . w[x]) = m; • F

APPENDIX A PROOFS OF SECTION II

A. Proof of Proposition II.12

In this section, we show that the functions of ZPoly k are closed by precomposition under a regular function. This proof is somehow classical and inspired by well-known composition techniques for MSO-transductions.

Definition A. 1 (Transduction). A (k-copying) MSO-transduction from A * to B * consists in several MSO formulas over A:

• for all 1 ≤ j ≤ k, a formula ϕ Dom j (x) ∈ MSO 1 ;

• for all 1 ≤ j ≤ k and a ∈ B, a formula ϕ a j (x) ∈ MSO 1 ; • for all 1 ≤ j, j ′ ≤ k, a formula ϕ < j,j ′ (x, x ′ ) ∈ MSO 2 .

Let w ∈ A * , we define the domain D(w) := {(i, j) : 1 ≤ i ≤ |w|, 1 ≤ j ≤ k, w |= ϕ Dom j (i)}. Using the formulas ϕ b j (x) (resp. ϕ < j,j ′ (x, x ′ )), we can label the elements of D(w) with letters of B (resp. define a relation < on the elements of D(w)). The transduction is defined if and only if the structure D(w) equipped with the labels and < is a word v ∈ B * , for all w ∈ A * . In this case, the transduction computes the function that maps w ∈ A * to this v ∈ B * . It follows from [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF] that regular functions can (effectively) be described by MSOtransductions.

Claim A.2. Let ℓ ≥ 0, k ≥ 1, ψ(x 1 , . . . , x ℓ ) ∈ MSO ℓ be a formula over B and f : A * → B * be computed by a k-copying MSO-transduction. Let us write W := {x 1 , . . . , x ℓ } {1,...,k} . There exists formulas θ ρ ∈ MSO ℓ over A where ρ ranges in W , such that for all w ∈ A * , #ϕ(f (w)) = ρ∈W #θ ρ (w).

Proof Sketch. Assume that the transduction is given by formulas ϕ Dom j (x), ϕ a j (x) ∈ MSO 1 for a ∈ B and ϕ < j,j ′ (x, x ′ ) ∈ MSO 2 as in Definition A.1. Let ψ be an MSO formula over B with first order variables x 1 , . . . , x ℓ and second order variables (X 1 , . . . , X k ), (Y 1 , . . . , Y k ), . . . . Let ρ be a mapping from {x 1 , . . . , x ℓ } to {1, . . . , k}. We define by induction on ψ the formula ψ ρ as follows (it roughly translates the formula from B to A using the transduction):

It is then a mechanical check that the translation works as expected. In the following equation, we fix w ∈ A * and we let pos : D(w) → [1:|f (w)|] be the function that maps a tuple (i, j) to the corresponding position in the word f (w) ∈ B * . To simplify notations, given ρ ∈ W , a word w ∈ A * , and a valuation τ : {x 1 , . . . , x ℓ } → [1:|w|], we write

We then let

The result follows immediately since ZPoly ℓ is closed under taking sums and Z-external products.

B. Proof of Proposition II.13

We first show that any Z-polyregular function can be written under the form sum •g where g : A * → {±1} * is polyregular. This is an immediate consequence of the following claims.

Claim A.3. For all ϕ ∈ MSO, there exists a polyregular function f :

Proof. Polyregular functions are characterized in [START_REF] Bojanczyk | String-to-String Interpretations With Polynomial-Size Output[END_REF]Theorem 7] as the functions computed by (multidimensional) MSO-interpretations. Recall that an MSO-interpretation of dimension k ∈ N is given by a formula ϕ ≤ ( x, y) defining a total ordering over k-tuples of positions, a formula ϕ Dom ( x) that selects valid positions, and formulas ϕ a ( x) that place the letters over the output word [21, Definition 1 and 2]. In our specific situation, letting ϕ ≤ be the usual lexicographic ordering of positions (which is MSO-definable) and placing the letter 1 over every element of the output is enough: the only thing left to do is select enough positions of the output word. For that, we let ϕ Dom be defined as ϕ itself. It is an easy check that this MSO-interpretation precisely computes 1 f (w) over w, hence computes f when post-composed with sum.

Claim A.4. The set {sum •f : f : A * → {±1} * polyregular} is closed under sums and external Z-products.

. As polyregular functions are closed under concatenation [START_REF] Bojańczyk | Polyregular Functions[END_REF], the set of interest is closed under sums. To prove that it is closed under external Z-products, it suffices to show that it is closed under negation. This follows because one can permute the 1 and -1 in the output of a polyregular function (polyregular functions are closed under post-composition by a morphism).

Let us consider a polyregular function g : A * → {±1} * . The maps g + : w → |g(w)| 1 and g -: w → |g(w)| -1 are polyregular functions with unary output (since they correspond to a post-composition by the regular function which removes some letter, and polyregular functions are closed under post-composition by a regular function [START_REF] Bojańczyk | Polyregular Functions[END_REF]). Hence g -and g + are polyregular functions with unary output, a.k.a. N-polyregular functions. As a consequence, sum•g = g + -g - lies in ZPoly.

APPENDIX B PROOFS OF SECTION II-C

A. Proof of Claim II.17 Let k ≥ 0, f ∈ ZPoly k and u ∈ A * . We want to show that u ⊲ f ∈ ZPoly k . Notice that for every u, the map u : w → uw is regular, hence u ⊲ f = f • (u ) belongs to ZPoly k thanks to Proposition II.12.

B. Proof of Claim IV.7

The fact that ∼ k is an equivalence relation is obvious from the properties of ZPoly.

and for this we proceed by induction on |u|. By expanding the definitions we note that a ⊲ (1

The result follows since a ⊲ 1 L = 1 a -1 L and by Theorem II.20.

C. Proof of Lemma IV.8

We first note that u ⊲ (δf + ηg) = δ(u ⊲ f ) + η(u ⊲ g), for all f, g : A * → Z, δ, η ∈ Z and u ∈ A * . Hence it suffices to show that Lemma IV.8 holds on a set S of functions such that Span Z (S) = ZPoly k . For k = 0, we can chose S := {1 L : L regular}. As observed above, we have u ⊲ 1 L = 1 u -1 L and the result holds since regular languages have finitely many residual languages. For k ≥ 1, we can choose S := {1 L ⊗ g : g ∈ ZPoly k-1 , L regular} by Proposition II. [START_REF] Thomas | Languages, automata, and logic[END_REF]. Let 1 L ⊗ g ∈ S. Then by Claim IV.7 we get u ⊲ (1

Since a regular language has finitely many residual languages, there are finitely many ∼ k-1 -equivalence classes for the (function) residuals of 1 L ⊗ g.

D. Proof of Lemma IV.17

Let f : A * → Z be a function such that Res(f )/ ∼ k-1 . We apply Algorithm 1, which computes the set of residuals of f and the relations between them. The states of our machine are not labelled by the equivalence classes of Res(f )/ ∼ k-1 , but directly by some elements of Res(f ). Remark that the labels on the transitions are of the form

observe that the construction of these labels is effective and that equivalence of residuals is decidable if we start from f ∈ ZPoly k ). Now, let us justify the correctness and termination of Algorithm 1.

First, we note that it maintains two sets O and

is finite and Q increases at every loop. At the end of its execution, we have for all q ∈ Q and a ∈ A, that δ(q, a) ∼ k-1 a ⊲ q and λ(q, a) = a ⊲ q -δ(q, a).

Let us show by induction on n ≥ 0 that for all

the run labelled by a 1 • • • a n in the underlying automaton , and g 1 • • • g n are the functions which label the transitions, we have

For n = 0 the result is obvious because q 0 = f . Now, assume that the result holds for some n ≥ 0 and let a 1 • • • a n a n+1 ∈ A * . Let q 0 → a1 q 1 → a2 • • • → an+1 q n+1 be the run and g 1 • • • g n+1 be the labels of the transitions. Since

a n+1 w) by induction hypothesis. But since g n+1 = λ(q n , a n+1 ) = a n+1 ⊲ q n -δ(q n , a n+1 ) = a n+1 ⊲ q n -q n+1 we get q n (a n+1 w) = g n+1 (w) + q n+1 (w). We conclude the proof that Algorithm 1 provides a k-residual transducer for f by considering w = ε and the definition of F .

E. Proof of Corollary IV.19

Lemma IV.17 shows that any function from ZPoly k is computed by its k-residual transducer (which is in particular a ZPoly k-1 -transducer). Conversely, given a ZPoly k-1 -transducer computing f , it is easy to write f as a linear combination of elements of the form 1 L ⊗ g (see e.g. Section F-B), where g is the label of a transition, thus f ∈ ZPoly k-1 .

F. Proof of Corollary IV.20

Every map in ZPoly k has finitely many residuals up to ∼ k-1 thanks to Lemma IV.8. We now prove the converse implication. Let f such that Res(f )/ ∼ k-1 is finite. By Lemma IV.17 there exists a k-residual transducer of f (which is in particular a ZPoly k-1 -transducer). Thanks to Corollary IV. [START_REF] Douéneau-Tabot | Hiding pebbles when the output alphabet is unary[END_REF], it follows that f ∈ ZPoly k .

APPENDIX F PROOFS OF SECTION V

A. Proof of Claim V.6

Let L be a regular language such that 1 L is ultimately 1-polynomial. Then, for every u, w, v ∈ A * , there exists a polynomial P ∈ Q[X], such that 1 L (uw X v) = P (X) for X large enough. This implies that P is a constant polynomial, and in particular 1 L (uw X+1 v) = 1 L (uw X v) for X large enough. As a consequence, the syntactic monoid of L is aperiodic, thus L is star-free [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF]. Conversely, assume that L is star-free. It is recognized by a morphism µ into an aperiodic finite monoid M . Because M is aperiodic, for every x ∈ M , x |M|+1 = x |M| . Hence, for all

Let T = (A, Q, q 0 , δ, λ) be a counter-free ZSF k-1 -transducer computing a function f : A * → Z. Since the deterministic automaton (A, Q, q 0 , δ) is counter-free, then by [START_REF] Mcnaughton | Counter-Free Automata[END_REF] for all q ∈ Q the language L q := {u : δ(q 0 , u) = q} is star-free. So is L q a for all a ∈ A. Now observe that:

We conclude thanks to Equation (3).

C. Proof of Lemma V.16

Let k ≥ 0. Let f ∈ ZPoly k which is ultimately 1-polynomial and T = (A, Q, q 0 , δ, H, λ, F ) be a k-residual transducer of f . Since ultimate 1-polynomiality is preserved under taking linear combinations and residuals, the function labels of T are ultimately 1-polynomial (by definition of a k-residual transducer). It remains to show that T is counter-free.

Let α, w ∈ A * and suppose that δ(q 0 , α) = δ(q 0 , αw n ) for some n ≥ 1. We want to show that δ(q 0 , αw) = δ(q 0 , α). Since δ(q 0 , α) = δ(q 0 , αw nX ) and δ(q 0 , αw) = δ(q 0 , ααw nX+1 ) for all X ≥ 1, it is sufficient to show that we have δ(q 0 , αw nX+1 ) = δ(q 0 , αw nX ) for some X ≥ 1.

Let M ≥ 1 given by Definition II.29 for the ultimate 1-polynomiality of f . We want to show that

since the residuals belong to ZPoly. For this, let us pick any α 0 , w 1 , α 1 , • • • , w k , α k ∈ A * . By Theorem III.3, it is sufficient to show that:

Thus by Lemma III.24, P has degree at most k, hence it can be rewritten under the form P 0 + XP 1 + • • • + X k P k where P i (X 1 , . . . , X k ) has degree at most k -i. Therefore:

since the term P 0 vanishes when doing the subtraction. The result follows since the polynomials P i for 1 ≤ i ≤ k have degree at most k-1.

D. Proof of Proposition V.17

The proof of the proposition is essentially the same as Proposition II.13 by noticing that everything remains FO-definable. We will underline the parts where the two proofs differ, and in particular when using stability properties of star-free polyregular functions.

We first show that any star free Z-polyregular function can be written under the form sum •g where g : A * → {±1} * is star-free polyregular. This is a consequence of the following claims.

Claim F.1. For all ϕ ∈ FO, there exists a star-free polyregular function f :

Proof. Star-free polyregular functions are characterized in [START_REF] Bojanczyk | String-to-String Interpretations With Polynomial-Size Output[END_REF]Theorem 7] as the functions computed by (multidimensional) FO-interpretations. Recall that an FO-interpretation of dimension k ∈ N is given by a FO formula ϕ ≤ ( x, y) defining a total ordering over k-tuples of positions, a FO formula ϕ Dom ( x) that selects valid positions, and FO formulas ϕ a ( x) that place the letters over the output word [21, Definition 1 and 2]. In our specific situation, letting ϕ ≤ be the usual lexicographic ordering of positions (which is FO-definable) and placing the letter 1 over every element of the output is enough: the only thing left to do is select enough positions of the output word. For that, we let ϕ Dom be defined as ϕ itself. It is an easy check that this FO-interpretation precisely computes 1 f (w) over w, hence computes f when post-composed with sum.

Claim F.2. The set {sum •f : f : A * → {±1} * star-free polyregular} is closed under sums and external Z-products.

Proof. Notice that sum •f + sum •g = sum •(f • g) where f • g(w) := f (w) • g(w). As star-free polyregular functions are closed under concatenation [START_REF] Bojańczyk | Polyregular Functions[END_REF], the set of interest is closed under sums. To prove that it is closed under external Z-products, it suffices to show that it is closed under negation. This follows because one can permute the 1 and -1 in the output of a star-free polyregular function (star-free polyregular functions are closed under post-composition by a morphism [START_REF] Bojańczyk | Polyregular Functions[END_REF]Theorem 2.6]).

Let us consider a star-free polyregular function g : A * → {±1} * . The maps g + : w → |g(w)| 1 and g -: w → |g(w)| -1 are star-free polyregular functions with unary output (since they correspond to a post-composition by the star-free polyregular function which removes some letter, and polyregular functions are closed under post-composition by a regular function [START_REF] Bojańczyk | Polyregular Functions[END_REF]). Hence g -and g + are star-free polyregular functions with unary output, a.k.a. star-free N-polyregular functions. As a consequence, sum • g = g + -g -lies in ZSF.

E. Proof of Proposition VI.2

Item 3 ⇒ Item 2 is obvious. For Item 2 ⇒ Item 1, it is sufficient to show that if ϕ(X 1 , . . . , X n ) is an MSO X formula, then #ϕ is a Z-polyregular function. We show the result for n = 1, i.e. for a formula ϕ(X). Let us define the language L ⊆ (A × {0, 1}) * such that (w, v) ∈ L if and only if w |= ϕ(S) where S := {1 ≤ i ≤ |w| : v[i] = 1}. Using the classical correspondence between MSO logic and automata (see e.g. [START_REF] Thomas | Languages, automata, and logic[END_REF]), the language L is regular, hence it is computed by a finite deterministic automaton A. Given a fixed w ∈ A * , there exists a bijection between the accepting runs of A whose first component is w and the sets S such that w |= ϕ(S). Consider the (nondeterministic) Z-weighted automaton A ′ (this notion is equivalent to Z-linear representations, see e.g. [START_REF] Berstel | Noncommutative rational series with applications[END_REF]) obtained from A by removing the second component of the input, adding an output 1 to all the transitions of A, and giving the initial values 1 (resp. final values 1) to the initial state (resp. final states) of A. All other transitions and states are given the value 0. Given a fixed w ∈ A * , it is easy to see that A ′ has exactly #ϕ(w) runs labelled by w whose product of the output values is 1 (and the others have product 0). Thus A computes #ϕ. This proof scheme adapts naturally to the case where n ≥ 1.

For Item 1 ⇒ Item 3, let us consider a linear representation (I, µ, F ) of a Z-rational series.

Claim F.3. Without loss of generality, one can assume that µ(A * ) ⊆ M n,n ({0, 1}), at the cost of increasing the dimension of the matrices.

Proof Sketch. Let N := min(1, max{|µ(a) i,j | : a ∈ A, 1 ≤ i, j ≤ n}), we define the new dimension of our system to be m := n × N × 2. As a notation, we assume that matrices in M m,m have their rows and columns indexed by {1, . . . , n} × {1, . . . , N } × {±}. For all a ∈ A, let us define ν(a) ∈ M m,m as follows: for all

Let us now adapt the final vector by defining for every 1 ≤ i ≤ n, 1 ≤ v ≤ N , F ′ (i,v,+) := max(0, F i ), and F ′ (i,v,-) := -min(0, F i ). For the initial vector, let us define for every 1 ≤ i ≤ n, I ′ (i,1,+) = I i and I ′ (i,1,-) = -I i , and let I ′ be zero otherwise. It is then an easy check that (I ′ , ν, F ′ ) computes the same function as (I, µ, F ).

As a consequence, Iµ(w)F = i,j I i µ(w) i,j F j , let us now rewrite this sum as a counting MSO formula with set free variables.

For all 1 ≤ i, j ≤ n, one can write an MSO formula ψ i,j (x) such that for all 1 ≤ p ≤ |w|, w |= ψ i,j (p) if and only if µ(w[p]) i,j = 1. Furthermore, for all 1 ≤ i, j ≤ n, one can write an MSO formula θ i,j with variables X in p , X out p for 1 ≤ p ≤ n such that a word w satisfies θ i,j whenever for every position x of w there exists a unique pair 1 ≤ p, q ≤ n such that x ∈ X in p and x ∈ X out q , if x ∈ X out p then (x + 1) ∈ X in p , the first position of w belongs to X in i and X out i , and the last position of w belongs to X in j and X out j . 1≤i,j≤n

We have proven that Iµ(w)F is a Z-linear combination of the counting formulas τ i,j via Iµ(w)F = i,j I i F j • #τ i,j (w). Notice that all the formulas used never introduced set quantifiers, hence the formulas belong to FO and have MSO free variables.