# Z-polyregular functions

Thomas Colcombet, Gaëtan Douéneau-Tabot, Aliaume Lopez

► To cite this version:

Thomas Colcombet, Gaëtan Douéneau-Tabot, Aliaume Lopez. Z-polyregular functions. 2023. hal-04097227

HAL Id: hal-04097227

https://hal.science/hal-04097227

Preprint submitted on 15 May 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Z-polyregular functions

Thomas Colcomb*, Gaëtan Douéneau-Tabot*† and Aliaume Lopez*‡

*Université Paris Cité, CNRS, IRIF, F-75013, Paris, France

† Direction générale de l'armement - Ingénierie des projets, Paris, France

‡ENS Paris-Saclay, CNRS, LMF, France

*Abstract*—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 first-order 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.

# 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 [1]), logic (Monadic Second Order (MSO) logic [2]), and algebra (finite monoids [3]). It contains a robust subclass of independent interest: star-free regular languages, which admits equivalent descriptions in terms of machines (counter-free automata [4]), expressions (star-free expressions [5]), logic (first-order (FO) logic [6]) and algebra (aperiodic monoids [5]). 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 [4] or, equivalently, its syntactic monoid [5]).

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 [7]). Decision problems, including first-order definability, become more difficult and more interesting for functions [8], 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 [9] and that a canonical object can be built [10].

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 $\varphi(\vec{x})$ with free first-order variables $\vec{x}$, and a word $w \in A^*$, we define $\#\varphi(w)$ to be the number of valuations $\nu$ such that $w, \nu \models \varphi(\vec{x})$. The indicator functions of regular languages are exactly the functions $\#\varphi$ where $\varphi$ 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 $\mathbb{ZPoly}$, as the class of Z-linear combinations of functions $\#\varphi$ where $\varphi$ is in MSO with first-order free variables.

The goal of this paper is to advocate for the robustness of $\mathbb{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 $\mathbb{ZPoly}$ with a smooth and elegant theory, which subsumes that of regular languages.

*Contributions:* We introduce the class $\mathbb{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 [11]. It also coincides with the linear finite counting automata of [12]. We first connect Z-polyregular functions to word-to-word polyregular functions [7], providing a justification for their name. As a class of functions from finite words to integers, it is then natural to compare $\mathbb{ZPoly}$ with the well-studied class of Z-rational series (see e.g. [13]). We observe that $\mathbb{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 \ge 0$, by making effective the results of Schützenberger [12]. As a consequence, we provide a simple syntax of Z-rational expressions to describe $\mathbb{ZPoly}$ as those built without the Kleene star. We also show how $\mathbb{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 \ge 0$. We summarize these results in the second column of Table I.

We then refine the description of $\mathbb{ZPoly}$ by considering for all $k \ge 0$, the class $\mathbb{ZPoly}_k$ of functions described using at most $k$ free variables in the counting MSO formulas. It is easy to check that if $f \in \mathbb{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 $\mathbb{ZPoly}$ to be in $\mathbb{ZPoly}_k$ (see Figure 1). This result is an analogue of the various “pebble minimization theorems” that were shown for word-to-word polyregular functions [14], [15], [16], [17]. We also prove that the membership problem of $\mathbb{ZPoly}_k$ inside $\mathbb{ZPoly}$ is decidable.

Our second main contribution is the definition of an almost canonical object associated to each function of $\mathbb{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 $\mathbb{ZPoly}$ to $\mathbb{ZPoly}_k$.

Finally, we define the class $\mathbb{ZSF}$ of star-free Z-polyregular
<table><caption>TABLE I: Summary of the characterizations of ZPoly and ZSF expressed in different formalisms.</caption><thead><tr><th>Formalism</th><th>Characterization of ZPoly</th><th>Characterization of ZSF</th></tr></thead><tbody><tr><td>Counting formulas</td><td>Counting valuations in MSO (Definition II.5)</td><td>Counting valuations in FO (Definition V.1)</td></tr><tr><td>Polyregular functions</td><td>sum ◦ polyregular (Proposition II.13)</td><td>sum ◦ star-free polyregular (Proposition V.17)</td></tr><tr><td>Z-rational expressions</td><td>Closure of rational languages under Cauchy products, sums, and Z-products (Theorem II.20)</td><td>Closure of star-free languages under Cauchy products, sums, and Z-products (Theorem V.4)</td></tr><tr><td rowspan="3">Z-rational series that are/have</td><td>Ultimately N-polynomial (Theorem II.31)</td><td>Ultimately 1-polynomial (Theorem V.13)</td></tr><tr><td>Polynomial growth (Theorem II.31)</td><td>n/a</td></tr><tr><td>Eigenvalues in {0} ∪ U (Theorem II.31)</td><td>Eigenvalues in {0, 1} (Theorem V.18)</td></tr><tr><td>Residual transducer</td><td>Residual transducer (Corollary IV.19)</td><td>Counter-free residual transducer (Theorem V.13)</td></tr></tbody></table>

functions, as the class of linear combinations of $\#\varphi$ where $\varphi$ 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 $\#\varphi$ where $\varphi$ 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 \ge 0$ the class ZSF$_k$ (defined in a similar way as ZPoly$_k$) and show that ZSF$_k = ZSF \cap 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 well-known Z-rational series (Sections II-C and II-D).

In the rest of this paper, Z (resp. $\mathbb{N}$) denotes the set of integers (resp. nonnegative integers). If $i \le j$, the set $[i:j]$ is $\{i, i+1, \dots, j\} \subseteq \mathbb{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 $\varepsilon \in A^*$. If $w \in A^*$, let $|w| \in \mathbb{N}$ be its length, and for $1 \le i \le |w|$ let $w[i]$ be its i-th letter. If $I = \{i_1 < \dots < i_\ell\} \subseteq [1:|w|]$, let $w[I] := w[i_1] \cdots w[i_\ell]$. If $a \in 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. [18]).

### 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 := $\bigcup_{k \in \mathbb{N}}$ MSO$_k$. If $\varphi(x_1, \dots, x_k) \in$ MSO$_k$, $w \in A^*$ and $1 \le i_1, \dots, i_k \le |w|$, we write $w \models = \varphi(i_1, \dots, i_k)$ whenever the valuation $x_1 \mapsto i_1, \dots, x_k \mapsto i_k$ makes the formula $\varphi$ true in the model w.

**Definition II.1 (Counting).** Given $\varphi(x_1, \dots, x_k) \in$ MSO$_k$, we let $\#\varphi: A^* \to \mathbb{N}$ be the function defined by $\#\varphi(w) := |\{(i_1, \dots, i_k) : w \models = \varphi(i_1, \dots, i_k)\}|$.

The value $\#\varphi(w)$ is the number of tuples that make the formula $\varphi$ true in the model w.

**Example II.2.** If $\varphi \in$ MSO$_0$, then $\#\varphi$ is the indicator function of the (regular) language $\{w : w \models = \varphi\} \subseteq A^*$.

**Example II.3.** Let $A := \{a, b\}$. Let $\varphi(x, y) := a(x) \wedge b(y)$, then $\#\varphi(w) = |w|_a \times |w|_b$ for all $w \in A^*$. Let $\psi(x, y) := \varphi(x, y) \wedge x > y$, then $\#\psi(a^n ba^{n_1} \cdots a^{n_p}) = \sum_{i=0}^p i \times n_i$.

**Example II.4.** Let $\varphi \in$ MSO$_k$, and $x$ be a fresh variable. Then, $x = x \wedge \varphi \in$ MSO$_{k+1}$, and $\#(x = x \wedge \varphi)(w) = |w| \times \#\varphi(w)$ for every $w \in A^*$. Similarly, for all $w \in A^*$ and $a \in A$, $\#(a(x) \wedge \varphi)(w) = |w|_a \times \#\varphi(w)$.

If F is a subset of the set of functions $A^* \to Z$ and if $S \subseteq Z$, we let $\text{Span}_S(F) := \{\sum_i a_i f_i : a_i \in S, f_i \in F\}$ be the set of S-linear combinations of the functions from F. The set $\text{Span}_{\mathbb{N}}(\{\#\varphi : \varphi \in$ MSO$_k$, $k \ge 0\})$ has been recently studied
<figure><img src="image_2.png" /><figcaption>Fig. 1: The classes of functions studied in this paper.</figcaption></figure>

by Douéneau-Tabot in [19] under the name of “polyregular functions with unary output”. In the following, we shall call this class the N-polyregular functions.

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 \ge 0$, let $\mathbb{Z}\text{Poly}_k := \text{Span}_{\mathbb{Z}}(\{\#\varphi : \varphi \in \text{MSO}_\ell, \ell \le k\})$. We define the class of Z-polyregular functions as $\mathbb{Z}\text{Poly} := \bigcup_k \mathbb{Z}\text{Poly}_k$.

We also let $\mathbb{Z}\text{Poly}_{-1} := \{0\}$.

**Remark II.6.** For all $k \ge 0$, the class $\mathbb{Z}\text{Poly}_k$ is precisely the class of functions computable in $\text{QMSO}(\Sigma_x^k, \oplus, \odot_b)$ of [11, Section IV.A] over the semiring $(\mathbb{Z}, +, \times)$.

**Remark II.7.** For all $k \ge 0$, the class $\mathbb{Z}\text{Poly}_k$ is precisely the class of functions computable by linear finite counting automata of order $k$ introduced by [12, p. 91].

**Example II.8.** $\mathbb{Z}\text{Poly}_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, \ell \ge 0$, and $f \in \mathbb{Z}\text{Poly}_\ell$, the function $g: w \mapsto f(w) \times |w|^k$ belongs to $\mathbb{Z}\text{Poly}_{\ell+k}$.

**Example II.10.** Let $1_{\text{odd}}$ and $1_{\text{even}}$ be respectively the indicator functions of words of odd length and even length. For all $k \ge 0$, the function $w \mapsto (-1)^{|w|} \times |w|^k$ is in $\mathbb{Z}\text{Poly}_k$. Indeed, it is $w \mapsto 1_{\text{even}}(w) \times |w|^k - 1_{\text{odd}}(w) \times |w|^k$. Observe that it cannot be written as a single $\delta\#\varphi$ for some $\delta \in \mathbb{Z}$, $\varphi \in \text{MSO}_\ell$, $\ell \ge 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 $\mathbb{Z}\text{Poly}$. Let us consider the function $f: w \mapsto (|w|_a - |w|_b)^2$. Because $f(w) = |w|_a^2 - 2|w|_a|w|_b + |w|_b^2$, we conclude from

Example II.4 that $f$ is in $\mathbb{Z}\text{Poly}_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 $\ell > k \ge 0$, $\varphi \in \text{MSO}_k$, then for all words $w \in A^+$ we have:

$$ \#\varphi(w) = \#(\varphi \wedge x_{k+1} = \cdots = x_\ell \wedge \forall y. x_{k+1} \le y)(w) $$

the latter being an $\text{MSO}_\ell$ formula. This formula also holds for $w = \varepsilon$ if $k > 0$, but it may fail for $k = 0$ because in that case the right-hand side equals 0 regardless of the formula $\varphi$ (because there is no valuation), whereas $\#\varphi(\varepsilon)$ may not be 0.

One can refine Remark II.11 to conclude that for all $k \ge 0$, $\mathbb{Z}\text{Poly}_k = \text{Span}_{\mathbb{Z}}(\{\#\varphi : \varphi \in \text{MSO}_k\} \cup \{1_{\{\varepsilon\}}\})$. In the rest of the paper, $1_{\{\varepsilon\}}$ will not play any role, and we will safely ignore it in the proofs so that $\mathbb{Z}\text{Poly}_k$ will often be considered equal to $\text{Span}_{\mathbb{Z}}(\{\#\varphi : \varphi \in \text{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 MSO-transductions, see e.g. [20]) is called regular functions. As an easy consequence of its definition, $\mathbb{Z}\text{Poly}_k$ is preserved under pre-composition with a regular function.

**Proposition II.12.** For all $k \ge 0$, the class $\mathbb{Z}\text{Poly}_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 [21] for its formal definition, which we skip here. Let $\sum : \{\pm 1\}^* \to \mathbb{Z}$ be the sum operation mapping $w \in \{\pm 1\}^*$ to $\sum_{i=1}^{|w|} w[i]$.

**Proposition II.13.** The class $\mathbb{Z}\text{Poly}$ is (effectively) the class of functions $\text{sum} \circ f$ where $f: A^* \to \{\pm 1\}^*$ is polyregular.
### C. Rational series and rational expressions

The class of rational series over the semiring $(\mathbb{Z}, +, \times)$, also known as Z-rational series, is a robust class of functions from finite words to $\mathbb{Z}$ that has been largely studied since the 1960 (see e.g. [13] for a survey). It can be defined using the indicator functions $\mathbf{1}_L$ of regular languages $L \subseteq A^*$, and the following combinators given $f, g: A^* \to \mathbb{Z}$ and $\delta \in \mathbb{Z}$:

* the external Z-product $\delta f: w \mapsto \delta \times f(w)$;

* the sum $f + g: w \mapsto f(w) + g(w)$;

* the Cauchy product $f \otimes g: w \mapsto \sum_{w=uv} f(u) \times g(v)$;

* if and only if $f(\varepsilon) = 0$, the Kleene star $f^* := \sum_{n \ge 0} f^n$ where $f^0: \varepsilon \mapsto 1, w \ne \varepsilon \mapsto 0$ is neutral for Cauchy product and $f^{n+1} := f \otimes 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^* \to \mathbb{Z}$ has polynomial growth whenever there exists $k \ge 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 \ge 0$ and $f \in \mathbb{Z}\mathrm{Poly}_k$ then $|f(w)| = O(|w|^k)$.

**Example II.16.** The map $f: w \mapsto (-2)^{|w|}$ is a Z-rational series because $f = ((-3)\mathbf{1}_{A^+})^*$. However $f \notin \mathbb{Z}\mathrm{Poly}$ since it does not have polynomial growth.

It is easy to see from the logical definition that the class $\mathbb{Z}\mathrm{Poly}$ is closed under taking Cauchy products.

**Claim II.17.** Let $k, \ell \ge 0$. Let $f \in \mathbb{Z}\mathrm{Poly}_k$ and $g \in \mathbb{Z}\mathrm{Poly}_\ell$, then $f \otimes g \in \mathbb{Z}\mathrm{Poly}_{k+\ell+1}$. The construction is effective.

As a consequence, if $L \subseteq A^*$ is regular and $f \in \mathbb{Z}\mathrm{Poly}_k$, then $\mathbf{1}_L \otimes f \in \mathbb{Z}\mathrm{Poly}_{k+1}$. The following result states that such functions actually generate the whole space $\mathbb{Z}\mathrm{Poly}_{k+1}$.

**Proposition II.18.** Let $k \ge 0$, the following (effectively) holds:

$$ \mathbb{Z}\mathrm{Poly}_{k+1} = \mathrm{Span}_{\mathbb{Z}}(\{\mathbf{1}_L \otimes f : L \text{ regular}, f \in \mathbb{Z}\mathrm{Poly}_k\}). $$

**Example II.19.** The map $w \mapsto (-1)^{|w|}|w|$ is in $\mathbb{Z}\mathrm{Poly}_1$ as it equals $\mathbf{1}_{\mathrm{odd}} \otimes \mathbf{1}_{\mathrm{odd}} + \mathbf{1}_{\mathrm{even}} \otimes \mathbf{1}_{\mathrm{even}} - \mathbf{1}_{\mathrm{even}} \otimes \mathbf{1}_{\mathrm{odd}} - \mathbf{1}_{\mathrm{odd}} \otimes \mathbf{1}_{\mathrm{even}} - \mathbf{1}_{\mathrm{odd}} + \mathbf{1}_{\mathrm{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^* \to \mathbb{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 $\Rightarrow$ Item 1, observe that $\mathbb{Z}\mathrm{Poly}$ 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 $\Rightarrow$ Item 2, we obtain for all $k \ge 0$ as an immediate consequence of Proposition II.18:

$$ \mathbb{Z}\mathrm{Poly}_k = \mathrm{Span}_{\mathbb{Z}}(\{\mathbf{1}_{L_0} \otimes \cdots \otimes \mathbf{1}_{L_k} : L_0, \dots, L_k \text{ regular languages}\}) \quad (1) $$

and the result follows.

The equivalence between Item 2 and Item 3 follows (in a non effective way) from [13, 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 $\Rightarrow$ 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 \times g(w) := f(w) \times g(w)$). This can be obtained by generalising Example II.4. Moreover, $f \times g \in \mathbb{Z}\mathrm{Poly}_{k+\ell}$ whenever $f \in \mathbb{Z}\mathrm{Poly}_k$ and $g \in \mathbb{Z}\mathrm{Poly}_\ell$.

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.

### 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}(\mathbb{Z})$ be the set of all $n \times m$ matrices with coefficients in $\mathbb{Z}$. We equip $M^{n,m}(\mathbb{Z})$ with the usual matrix multiplication.

**Definition II.25 (Linear representation).** We say that a triple $(I, \mu, F)$ where $\mu: A^* \to M^{n,n}(\mathbb{Z})$ is a monoid morphism, $I \in M^{1,n}(\mathbb{Z})$ and $F \in M^{n,1}(\mathbb{Z})$, is a Z-linear representation of a function $f: A^* \to \mathbb{Z}$ if $f(w) = I\mu(w)F$ for all $w \in 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 \mapsto (-1)^{|w|} |w|$ from Example II.19 is a Z-polyregular function, hence it is a Z-rational series. It has the following Z-linear representation:

$$ \left( \begin{pmatrix} -1 & 0 \\ 0 & 1 \end{pmatrix}, w \mapsto \begin{pmatrix} -1 & 1 \\ 0 & -1 \end{pmatrix}^{|w|} \begin{pmatrix} 0 \\ 1 \end{pmatrix} \right). $$

Note that the eigenvalues of any matrix in $\mu(A^*)$ are 1 or -1.

**Example II.27.** The function $w \mapsto (-2)^{|w|}$ from Example II.16 is a Z-rational series that is not a Z-polyregular function. It can be represented via $((1), \mu, (1))$ where $\mu(w) = ((-2)^{|w|})$ for all $w \in A^*$. Observe that for all $n \ge 1$, there exists a matrix in $\mu(A^*)$ whose eigenvalue has modulus $2^n > 1$.

A Z-linear representation $(I, \mu, 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 \in \mathcal{M}^{n,n}(\mathbb{Z})$, we let $\text{Spec}(M) \subseteq \mathbb{C}$ be its spectrum, which is the set of all its (complex) eigenvalues. If $S \subseteq \mathcal{M}^{n,n}(\mathbb{Z})$, we let $\text{Spec}(S) := \bigcup_{M \in S} \text{Spec}(M)$ be the union of the spectrums. Finally, let $B(0, 1) := \{x \in \mathbb{C} : |x| \le 1\}$ be the unit disc and $\mathbb{U} := \{x \in \mathbb{C} : \exists n \ge 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 $\mu(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^* \to \mathbb{Z}$ be a Z-rational series and $(I, \mu, F)$ be a minimal Z-linear representation of $f$. Let $w \in A^*$ and $\lambda \in \text{Spec}(\mu(w))$. There exist coefficients $\alpha_{i,j} \in \mathbb{C}$ for $1 \le i, j \le n$, and words $u_1, v_1, \dots, u_n, v_n \in A^*$ such that $\lambda^X = \sum_{i,j=1}^n \alpha_{i,j} f(v_i w^X u_j)$ for all $X \ge 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^* \to \mathbb{Z}$ is ultimately N-polynomial whenever there exists $M \ge 0$ such that for all $\ell \ge 0$, for all $\alpha_0, w_1, \alpha_1, \dots, w_\ell, \alpha_\ell \in A^*$, there exists $P \in \mathbb{Q}[X_1, \dots, X_\ell]$, such that $f(\alpha_0 w_1^{NX_1} \alpha_1 \cdots w_\ell^{NX_\ell} \alpha_\ell) = P(X_1, \dots, X_\ell)$, whenever $X_1, \dots, X_\ell \ge M$.

In this section we only need to have $\ell = 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^* \to \mathbb{Z}$ be (respectively) ultimately $N_1$-polynomial and ultimately $N_2$-polynomial, then:

* $f+g$ and $f \otimes g$ are ultimately $(N_1 \times N_2)$-polynomial;

* $\delta f$ is ultimately $N_1$-polynomial for $\delta \in \mathbb{Z}$.

Furthermore, for every regular language $L$, there exists $N > 0$ such that $\mathbf{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^* \to \mathbb{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 representations $(I, \mu, F)$ of $f$, $\text{Spec}(\mu(A^*)) \subseteq \mathbb{U} \cup \{0\}$.

4) $f$ is a Z-rational series and for some minimal Z-linear representation $(I, \mu, F)$ of $f$, $\text{Spec}(\mu(A^*)) \subseteq B(0, 1)$;

*Proof.* Item 4 $\Rightarrow$ Item 1 is a direct consequence of [22, Theorem 2.6] and Theorem II.20. Item 1 $\Rightarrow$ Item 2 follows from Lemma II.30 and Theorem II.20.

For Item 2 $\Rightarrow$ Item 3, let $(I, \mu, F)$ be a minimal representation of $f$ in $\mathbb{Z}$, of dimension $n \ge 0$. Let $w \in A^*$ and $\lambda \in \text{Spec}(\mu(w))$. Thanks to Lemma II.28, there exists $\alpha_{i,j}, u_i, v_j$ for $1 \le i, j \le n$, such that $\lambda^X = \sum_{1 \le i,j \le n} \alpha_{i,j} f(v_i w^X u_j)$ for $X$ large enough. By assumption, for all $1 \le i, j \le n$, there exists $N_{i,j} > 0$ such that $X \mapsto f(v_i w^{N_{i,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 \mapsto \lambda^{N X} = (\lambda^N)^X$ is a polynomial for $X$ large enough, which therefore must be a constant polynomial. Hence $\lambda^N \in \{0, 1\}$, which implies that $\lambda \in \{0\} \cup \mathbb{U}$. Item 3 $\Rightarrow$ Item 4 is obvious. $\square$

**Remark II.32.** Item 3 of Theorem II.31 is optimal, in the sense that for all $\lambda \in \mathbb{U} \cup \{0\}$, there exists a Z-rational series of polynomial growth having a minimal representation $(I, \mu, F)$ with $\lambda \in \text{Spec}(\mu(A^*))$ (if $\lambda \in \mathbb{U}$, we let $\mu(a)$ be the companion matrix of the cyclotomic polynomial associated to $\lambda$).

**Remark II.33.** Leveraging the proof scheme used for the implication Item 2 $\Rightarrow$ 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 \in A^*$, there exists $P \in \mathbb{Q}[X]$, such that $|f(uw^X v)| \le P(X)$, for $X$ large enough.

**Remark II.34.** Beware that $\text{Spec}(\mu(A)) \subseteq \{0\} \cup \mathbb{U}$ has no reason to imply $\text{Spec}(\mu(A^*)) \subseteq \{0\} \cup \mathbb{U}$.

### III. FREE VARIABLE MINIMIZATION AND GROWTH RATE

In this section, we study the membership problem from $\mathbb{Z}$Poly to $\mathbb{Z}$Poly$_k$ for a given $k \ge 0$. As observed in Claim II.15, if $f \in \mathbb{Z}$Poly$_k$ then $|f(w)| = O(|w|^k)$. We show that this asymptotic behavior completely characterizes $\mathbb{Z}$Poly$_k$ inside $\mathbb{Z}$Poly. 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 \in \mathbb{Z}\text{Poly}$, which is done in Section IV.

This can be understood as a result that “minimizes” the
number of free variables needed to describe a $\mathbb{Z}$-polyregular
function. As such, it is tightly connected with the “pebble
minimization” results that exists for (word-to-word) polyregu-
lar functions [17] and $\mathbb{N}$-polyregular functions [14]. However,
these results cannot be used as black box theorems to mini-
mize the number of free variables of $\mathbb{Z}$-polyregular functions
because the negative coefficients of the latter induce non-trivial
behaviors.

To capture the growth rate of $\mathbb{Z}$-polyregular functions,
we shall introduce a quantitative variant of the traditional
pumping lemmas. Before that, let us extend the $\mathcal{O}$ notation
to multivariate functions $f,g: \mathbb{N}^n \to \mathbb{Z}$ as follows: we say
that $f = \mathcal{O}(g)$ whenever there exist $N,C \ge 0$ such that
$|f(x_1, \dots, x_n)| \le C|g(x_1, \dots, x_n)|$ for every $x_1, \dots, x_n \ge N$. We similarly extend the notation $f(x) = \Omega(g(x))$ to
multivariate functions.

**Definition III.1.** A function $f: A^* \to \mathbb{Z}$ is $k$-pumpable whenever there exist $\alpha_0, \dots, \alpha_k \in A^*, w_1, \dots, w_k \in A^*, $ such that $|f(\alpha_0 \prod_{i=1}^k w_i^{\alpha_i})| = \Omega(|X_1 + \dots + X_k|^k)$.

**Example III.2.** For all $k \ge 0$, for all $f \in \mathbb{Z}\text{Poly}_k$, $f$ is not $(k+1)$-pumpable because $|f(w)| = \mathcal{O}(|w|^k)$.

The equivalence between Item 1 and Item 2 in
Theorem III.3 is known since [12]. However, the equivalence
with Item 3 and the effectivity of the result are novel.

**Theorem III.3** (Free Variable Minimization). Let $f \in \mathbb{Z}\text{Poly}$ and $k \ge 0$. The following conditions are equivalent:

1) $f \in \mathbb{Z}\text{Poly}_k$;

2) $|f(w)| = \mathcal{O}(|w|^k)$;

3) $f$ is not $(k+1)$-pumpable.

Furthermore, the minimal $k$ such that $f \in \mathbb{Z}\text{Poly}_k$ is com-
putable, 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 \ge 1$ and $f \in \mathbb{Z}\text{Poly}_k$. The following conditions are equivalent:

1) $f \in \mathbb{Z}\text{Poly}_{k-1}$;

2) $|f(w)| = \mathcal{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^l \mapsto k \times l$ and $w \mapsto 0$ otherwise. The function $f$ is $\mathbb{Z}$-polyregular and 2-pumpable, however, $f(\alpha_0 w^X \alpha_1) = \mathcal{O}(X)$ for every triple $\alpha_0, w, \alpha_1 \in A^*$.

Our proof of Induction Step III.4 is built upon factorization
forests. Given a morphism $\mu: A^* \to M$ into a finite monoid
and $w \in A^*$, a $\mu$-forest of $w$ is a forest that can be represented
as a word over $\hat{A} := A \uplus \{(\langle, \rangle)\}$, defined as follows.

**Definition III.6** (Factorization forest [23]). Given a monoid morphism $\mu: A^* \to M$ and $w \in A^*$, we say that $F$ is a $\mu$-forest of $w$ when:

• either $F = a$, and $w = a \in A$;

• or $F = \langle F_1 \rangle \cdots \langle F_n \rangle$, $w = w_1 \cdots w_n$ and for all $1 \le i \le n$, $F_i$ is a $\mu$-forest of $w_i \in A^+$. Furthermore, if $n \ge 3$ then $\mu(w_1) = \cdots = \mu(w_n)$ is an idempotent of $M$.

We let $\mathcal{F}^\mu$ be the language of $\mu$-forests inside $(\hat{A})^*$. 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 $\mathcal{F}_d^\mu \subseteq (\hat{A})^*$ be the set of $\mu$-forests with depth at most $d$. Let word: $\mathcal{F}_d^\mu \to A^*$ be the function mapping a $\mu$-forest of $w \in A^*$ to $w$ itself.

**Example III.7.** Let $M := (\{-1, 1, 0\}, \times)$. A forest $F \in \mathcal{F}_5^\mu$ (where $\mu: M^* \to M$ maps a word to the product of its elements) such that $\text{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 [23] that any word in $A^*$ has a $\mu$-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], [24]). Given a morphism into a finite monoid $\mu: A^* \to M$, one can effectively compute some $d \ge 0$ and a regular function forest: $A^* \to \mathcal{F}_d^\mu$ such that word ◦ forest is the identity function.

In order to prove Induction Step III.4, we shall consider a
function $(f: A^* \to \mathbb{Z}) \in \mathbb{Z}\text{Poly}_k$ that is not $k$-pumpable, and
show how to compute it as a function in $\mathbb{Z}\text{Poly}_{k-1}$. To that
end, we shall construct a function $g: \hat{A}^* \to \mathbb{Z} \in \mathbb{Z}\text{Poly}_{k-1}$
such that $f = g \circ$ forest. Since forest is regular thanks
to Theorem III.8, it will follow that $f \in \mathbb{Z}\text{Poly}_{k-1}$ by
Proposition II.12. Remark that it is only needed to define $g$
on $\mathcal{F}_d^\mu$.

Following the classical connections between MSO-formulas
and regular languages [18], we prove in Claim III.11 that for
every function $f \in \mathbb{Z}\text{Poly}_k$ there exist a finite monoid $M$ and
a morphism $\mu: A^* \to M$, such that $f(w)$ can be reconstructed
using “simple” MSO-formulas which are evaluated along
bounded-depth $\mu$-factorizations of $w$.

**Claim III.9.** Given a morphism $\mu: A^* \to M$ into a finite monoid and $d \in \mathbb{N}$, the following predicates are MSO definable for words over $\hat{A}$. For all $F \in \mathcal{F}_d^\mu$, and $w = \text{word}(F)$, then:

• $F \models \text{isleaf}(x)$ if and only if $x$ is a leaf of $F$;

• $F \models \text{between}_m(x, y)$ if and only if $x$ and $y$ are leaves of $F$, $x \le y$, and $\mu(w[x] \dots w[y]) = m$;
* $F \models \text{left}_m(x)$ if and only if $x$ is a leaf of $F$, and $\mu(w[1] \dots w[x]) = m$;

* $F \models \text{right}_m(x)$ if and only if $x$ is a leaf of $F$, and $\mu(w[x] \dots w[[w]]) = m$.

Whenever $F \in \hat{A}^* \setminus \mathcal{F}_d^\mu$, the semantics are undefined.

**Definition III.10.** The fragment INV is a subset of MSO over $\hat{A}$, 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 $\text{INV}_k := \text{INV} \cap \text{MSO}_k$.

**Claim III.11** ([15], [17]). For all $f \in \mathbb{Z}\text{Poly}_k$, one can build a finite monoid $M$, a depth $d \in \mathbb{N}$, a surjective morphism $\mu: A^* \to M$, constants $n \ge 0$, $\delta_i \in \mathbb{Z}$ for $1 \le i \le n$, formulas $\psi_i \in \text{INV}_k$ for $1 \le i \le n$, such that for every word $w \in A^*$, for every factorization forest $F \in \mathcal{F}_d^\mu$ of $w$, it holds that $f(w) = \sum_{i=1}^n \delta_i \times \#\psi_i(F)$.

In the rest of this section, we focus on the number of free variables in $\mathbb{Z}$-linear combinations of $\#\psi$ where $\psi \in \text{INV}$. The crucial idea is that one can leverage the structure of the forest $F \in \mathcal{F}_d^\mu$ to compute $\#\psi$ 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 [19], [16], [17] for the study of pebble transducers.

**Definition III.12.** Let $F \in \mathcal{F}^\mu$ and $t \in \text{Nodes}(F)$, we define the skeleton of $t$ by:

* if $t = a \in A$ is a leaf, then $\text{Skel}(t) := \{t\}$;

* otherwise if $t = (F_1) \dots (F_n)$, then $\text{Skel}(t) := \{t\} \cup \text{Skel}(F_1) \cup \text{Skel}(F_n)$.

Let $w \in A^*$, $F$ be a $\mu$-forest of $w$, and $t \in \text{Nodes}(F)$. The set of nodes $\text{Skel}(t)$ defines a $\mu$-forest of a (scattered) subword $u$ of $w$: the one obtained by concatenating the leaves of $F$ that are in $\text{Skel}(t)$. See Figure 2 for an example of a skeleton. A crucial property of $\text{Skel}(t)$ seen as a forest is that it preserves the evaluation:

**Claim III.13.** For all $d \ge 0$, finite monoid $M$, morphism $\mu: A^* \to M$, forest $F \in \mathcal{F}_d^\mu$, node $t \in F$, it holds that $\mu(\text{word}(\text{Skel}(t))) = \mu(\text{word}(t))$.

<figure><img src="image_3.png" /><figcaption>Fig. 2: A forest $F$ with $\text{word}(F) = (-1)(-1)0(-1)000000$ together with a skeleton in blue.</figcaption></figure>

Let $F$ be a forest and $x$ be a leaf in $F$. Observe that $\text{Skel}(x)$ is exactly $x$ itself. There may exist several nodes $t \in F$

such that $x \in \text{Skel}(t)$, however only one of them is maximal thanks to Lemma III.14. As a consequence one can partition $\text{Leaves}(F)$ depending on the maximal skeleton (for inclusion) which contains a given leaf (Definition III.15).

**Lemma III.14.** Let $F \in \mathcal{F}_d^\mu$, $x \in \text{Leaves}(F)$. There exists $t \in \text{Nodes}(F)$ such that $x \in \text{Skel}(t)$.

Furthermore, for every $t$, $t'$ such that $x \in \text{Skel}(t) \cap \text{Skel}(t')$, $\text{Skel}(t) \subseteq \text{Skel}(t')$ or $\text{Skel}(t') \subseteq \text{Skel}(t)$.

**Definition III.15.** Let skel-root: $\text{Leaves}(F) \to \text{Nodes}(F)$ map a leaf $x$ to the $t \in \text{Nodes}(F)$ such that $x \in \text{Skel}(t)$ and $\text{Skel}(t)$ is maximal for inclusion.

Following the work of [19], we define a notion of dependency of leaves (Definition III.17) based on the relationship between their maximal skeletons (Definition III.16).

**Definition III.16 (Observation).** We say that $t' \in \text{Nodes}(F)$ observes $t \in \text{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 $\text{skel-root}(y)$ observes $\text{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.18.** Given $d \ge 0$, there exists a (computable) bound $N_d \in \mathbb{N}$ such that for all $F \in \mathcal{F}_d^\mu$ and all leaf $x \in \text{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 $\text{sym-dep}(x, y)$ in MSO over $\mathcal{F}_d^\mu$ 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 $\vec{x} := (x_1, \dots, x_k)$ via:

$$ \text{sym-dep}(\vec{x}) := \begin{cases} \top & \text{for } k=0; \\ \top & \text{if and only if } x_1 \text{ is the root} \text{ for } k=1; \\ \bigvee_{i \neq j} \text{sym-dep}(x_i, x_j) & \text{otherwise.} \end{cases} $$

Notice that the independence (or dependence) of a tuple of leaves $\vec{x}$ only depends on the tuple $\text{skel-root}(x_1), \dots, \text{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.19.

**Lemma III.19.** Let $d \ge 0$, $M$ be a finite monoid, $\mu: A^* \to M$, $k \ge 1$, and $\psi \in \text{INV}_k$. One can effectively build a function $g: (\hat{A})^* \to \mathbb{Z} \in \mathbb{Z}\text{Poly}_{k-1}$ such that for every $F \in \mathcal{F}_d^\mu$, $g(F) = \#(\psi(\vec{x}) \wedge \text{sym-dep}(\vec{x}))(F)$.

**Definition III.20.** Let $k \ge 1$ and $f \in \mathbb{Z}\text{Poly}_k$, thanks to Claim III.11 and Theorem III.8, there exists $\mu: A^* \to M$,
$d \ge 0$, $\delta_i \in \mathbb{Z}$, $\psi_i \in \text{INV}_k$ such that:

$$
\begin{align}
f &= \left( \sum_{i=1}^{n} \delta_i \# \psi_i(\vec{x}) \right) \circ \text{forest} \nonumber \\
  &= \underbrace{\left( \sum_{i=1}^{n} \delta_i \# (\psi_i(\vec{x}) \wedge \text{sym-dep}(\vec{x})) \right)}_{:= f_{\text{dep}}} \circ \text{forest} \tag{2} \\
  &\quad + \underbrace{\left( \sum_{i=1}^{n} \delta_i \# (\psi_i(\vec{x}) \wedge \neg \text{sym-dep}(\vec{x})) \right)}_{:= f_{\text{indep}}} \circ \text{forest}. \nonumber
\end{align}
$$

We say that $f_{\text{dep}}$ is the dependent part of $f$ and $f_{\text{indep}}$ is its independent part.

Thanks to Lemma III.19 and Proposition II.12, for every $k \ge 1$ and $f \in \mathbb{Z}\text{Poly}_k$, $(f_{\text{dep}} \circ \text{forest}) \in \mathbb{Z}\text{Poly}_{k-1}$ (over $\mathcal{F}_d^\mu$). Hence, whether the function $f$ belongs to $\mathbb{Z}\text{Poly}_{k-1}$ only depends on its independent part. We will actually prove that in this case, $f \in \mathbb{Z}\text{Poly}_{k-1}$ if and only if $f_{\text{indep}} = 0$. For that, we will rely on “pumping families” that respect forest.

**Definition III.21** (Pumping family). $A (\mu, d)$-pumping family of size $k \ge 1$ is given by words $\alpha_0, w_1, \alpha_2, \dots, \alpha_{k-1}, w_k, \alpha_k \in A^*$, together with a family $F^{\vec{X}}$ of forests in $\mathcal{F}_d^\mu$, such that for all $1 \le i \le k$, $w_i \ne \varepsilon$, and $F^{\vec{X}}$ is a $\mu$-forest of $w^{\vec{X}} := \alpha_0 \prod_{i=1}^k (w_i)^{X_i} \alpha_i$ for every $\vec{X} := X_1, \dots, X_k \ge 0$.

**Remark III.22.** A $(\mu, d)$-pumping family of size $k$ satisfies that $|w^{\vec{X}}| = \Theta(X_1 + \dots + X_k)$, and $|F^{\vec{X}}| = \Theta(X_1 + \dots + X_k)$ since the depth of $F^{\vec{X}}$ is bounded by $d$.

**Lemma III.23.** Let $f_{\text{indep}}$ be defined as in Equation (2). Then, $f_{\text{indep}} \ne 0$ if and only if there exists a $(\mu, d)$-pumping family of size $k$ such that $f(F^{\vec{X}})$ is ultimately a $\mathbb{Z}$-polynomial in $X_1, \dots, X_k$ with a non-zero coefficient for $X_1 \cdots X_k$.

Moreover, one can decide whether $f_{\text{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 $\mathbb{R}[X_1, \dots, X_n]$. If $|P| = O(|Q|)$, then $\text{deg}(P) \le \text{deg}(Q)$.

*Proof of Induction Step III.4.* The only non-trivial implication is Item 3 $\Rightarrow$ Item 1. Let $f \in \mathbb{Z}\text{Poly}_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_{\text{indep}} = 0$.

Consider a pumping family $(w^{\vec{X}}, F^{\vec{X}})$ of size $k$, we have: $|f_{\text{indep}}(F^{\vec{X}})| = |f(w^{\vec{X}}) - f_{\text{dep}}(F^{\vec{X}})| = O(|X_1 + \cdots + X_k|^{k-1})$.

Assume by contradiction that $f_{\text{indep}} \ne 0$, Lemma III.23 provides us with a pumping family such that $f_{\text{indep}}(F^{\vec{X}})$

is ultimately a polynomial with non-zero coefficient for $X_1 \cdots X_k$. As this polynomial is asymptotically bounded by $(X_1 + \cdots + X_k)^{k-1}$, Lemma III.24 yields a contradiction.

The constructions of forest, $f_{\text{dep}}$, and $f_{\text{indep}}$ are effective, therefore so is our procedure. Moreover, one can decide whether $f_{\text{indep}} = 0$ thanks to Lemma III.23. □

## IV. RESIDUAL TRANSDUCERS

In this section, we provide a canonical object associated to any $\mathbb{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 $\mathbb{Z}$-polyregular functions, that will extend first-order definability for regular languages (see e.g. [6] for an introduction).

### A. Residuals of a function

We first introduce the notion of residual of a function $f: A^* \to \mathbb{Z}$ under a word $u \in A^*$.

**Definition IV.1 (Residual).** Given $f: A^* \to \mathbb{Z}$ and $u \in A^*$, we define the function $u \triangleright f: A^* \to \mathbb{Z}$, $w \mapsto f(uw)$. We let $\text{Res}(f) := \{u \triangleright f : u \in A^*\}$ be the set of residuals of $f$.

**Example IV.2.** The residuals of the function $w \mapsto |w|^2$ are the functions $w \mapsto |w|^2 + 2n|w| + n^2$ for $n \ge 0$.

**Example IV.3.** The residuals of the function $w \mapsto (-2)^{|w|}$ are the functions $w \mapsto (-2)^{n+|w|}$ for $n \ge 0$.

It is easy to see that $u \mapsto u \triangleright f$ defines a monoid action of $A^*$ over $A^* \to \mathbb{Z}$. Let us observe that this action (effectively) preserves the classes of functions $\mathbb{Z}\text{Poly}_k$.

**Claim IV.4.** Let $k \ge 0$, $f \in \mathbb{Z}\text{Poly}_k$ and $u \in A^*$. Then $u \triangleright f \in \mathbb{Z}\text{Poly}_k$ and this result is effective.

**Remark IV.5 ([13, Corollary 5.4 p 14]).** Let $f: A^* \to \mathbb{Z}$, this function is a $\mathbb{Z}$-rational series if and only if $\text{Span}_{\mathbb{Z}}(\text{Res}(f))$ has finite dimension.

Note that if $L \subseteq A^*$ and $u \in A^*$, then $u \triangleright \mathbf{1}_L$ is the characteristic function of the well-known residual language $u^{-1}L := \{w \in A^* : uw \in L\}$. In particular, the set $\{u \triangleright \mathbf{1}_L : u \in A^*\}$ is finite if and only if $L$ is regular. However, given $f \in \mathbb{Z}\text{Poly}_k$ for $k \ge 1$, the set $\{u \triangleright f : u \in 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 $\mathbb{Z}\text{Poly}_{k-1}$.

**Definition IV.6 (Growth equivalence).** Given $k \ge -1$ and $f, g: A^* \to \mathbb{Z}$, we let $f \sim_k g$ if and only if $f - g \in \mathbb{Z}\text{Poly}_k$

Let us observe that $\sim_k$ is an equivalence relation, that is compatible with external $\mathbb{Z}$-products, sums, $\otimes$ and $\triangleright$.

**Claim IV.7.** For all $k \ge -1$, $\sim_k$ is an equivalence relation and the following holds for all $u \in A^*$, $\delta \in \mathbb{Z}$, and $f, g: A^* \to \mathbb{Z}$:

* if $f \sim_k g$, then $u \triangleright f \sim_k u \triangleright g$;

* $u \triangleright (\mathbf{1}_L \otimes f) \sim_k (u \triangleright \mathbf{1}_L) \otimes f$ for $L \subseteq A^*$;
• if $f \sim_k g$ and $f' \sim_k g'$ then $f+f' \sim_k g+g'$;

• if $f \sim_k g$ then $\delta \cdot f \sim_k \delta \cdot g$.

By combining these results with the characterization of $\mathbb{Z}$Poly via these combinators in Theorem II.20, we can show that a function $f \in \mathbb{Z}$Poly$_k$ has a finite number of residuals, up to $\sim_{k-1}$ identification.

**Lemma IV.8 (Finite residuals).** Let $k \ge 0$ and $f \in \mathbb{Z}$Poly$_k$, then the quotient set $\text{Res}(f)/\sim_{k-1}$ is finite.

**Remark IV.9.** *Example IV.3 exhibits a $\mathbb{Z}$-rational series $f$ such that $\text{Res}(f)/\sim_k$ is infinite for all $k \ge 0$.*

Finally, we note that $\sim_k$ is decidable in $\mathbb{Z}$Poly.

**Claim IV.10 (Decidability).** Given $k \ge -1$ and $f, g \in \mathbb{Z}$Poly, one can decide whether $f \sim_k g$ holds.

*Proof.* Let $f, g \in \mathbb{Z}$Poly. For $k \ge 0$, $f \sim_k g$ if and only if $|(f-g)(w)| = \mathcal{O}(|w|^k)$ and this property is decidable by Theorem III.3. For $k = -1$, we have $f \sim_k g$ if and only if $f = g$, which is decidable by Corollary II.24. $\square$

## B. Residual transducers

Now we intend to show that a function $f \in \mathbb{Z}$Poly$_k$ can effectively be computed by a canonical machine, whose states are based on the finite set $\text{Res}(f)/\sim_{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 [25], that call functions on prefixes).

**Definition IV.11 (H-transducer).** Let $k \ge 0$ and $\mathcal{H}$ be a fixed subset of the functions $A^* \to \mathbb{Z}$. A $\mathcal{H}$-transducer $\mathcal{T} = (A, Q, q_0, \delta, \mathcal{H}, \lambda, F)$ consists of:

• a finite input alphabet $A$;

• a finite set of states $Q$ with $q_0 \in Q$ initial;

• a transition function $\delta: Q \times A \to Q$;

• a labelling function $\lambda: Q \times A \to \mathcal{H}$;

• an output function $F: Q \to \mathbb{Z}$.

Given $q \in Q$, we define by induction on $w \in A^*$ the value $\mathcal{T}_q(w) \in \mathbb{Z}$. For $w = \varepsilon$, we let $\mathcal{T}_q(w) := F(q)$. Otherwise let $\mathcal{T}_q(aw) := \mathcal{T}_{\delta(q,a)}(w) + \lambda(q,a)(w)$. Finally, the function computed by the $\mathcal{H}$-transducer $\mathcal{T}$ is defined as $\mathcal{T}_{q_0}: A^* \to \mathbb{Z}$. Observe that all the functions $\mathcal{T}_q$ are total.

Let us recall the standard definition of $\delta^*$ via $\delta^*(q, ua) := \delta(\delta^*(q, u), a)$ and $\delta^*(q, \varepsilon) = q$. Using this notation, a simple induction shows that $\mathcal{T}_q(w) = \sum_{uav=w} \lambda(\delta^*(q, u), a)(v) + F(\delta^*(q, w))$. As a consequence, $\mathcal{H}$-transducers are closely related to Cauchy products.

**Example IV.12.** We have depicted in Figure 3 a $\mathbb{Z}$Poly$_{-1}$-transducer and a $\mathbb{Z}$Poly$_0$-transducer computing the function $\mathbf{1}_{aA^*}$ for $A = \{a, b\}$. The first one can easily be identified with the minimal automaton of $\mathbf{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 $\mathbb{Z}$Poly$_0$. One can check e.g. that $1 = \mathbf{1}_{aA^*}(aab) = (1 - \mathbf{1}_{aA^*}(ab)) + (1 - \mathbf{1}_{aA^*}(b)) - \mathbf{1}_{aA^*}(\varepsilon) + 0$.

<figure><img src="image_4.png" /><figcaption>(a) A $\mathbb{Z}$Poly$_{-1}$-transducer computing $\mathbf{1}_{aA^*}$.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>(b) A $\mathbb{Z}$Poly$_0$-transducer computing $\mathbf{1}_{aA^*}$.</figcaption></figure>

Fig. 3: Two transducers computing $\mathbf{1}_{aA^*}$.

The reader may guess that every function $f \in \mathbb{Z}$Poly$_k$ can effectively be computed by a $\mathbb{Z}$Poly$_{k-1}$-transducer. We provide a stronger result and show that $f$ can be computed by some specific $\mathbb{Z}$Poly$_{k-1}$-transducer whose transition function is uniquely defined by $\text{Res}(f)/\sim_{k-1}$.

**Definition IV.13.** Let $k \ge 0$, let $\mathcal{T} = (A, Q, q_0, \delta, \mathcal{H}, \lambda, F)$ be a $\mathbb{Z}$Poly$_{k-1}$-transducer and $f: A^* \to \mathbb{Z}$. We say that $\mathcal{T}$ is a $k$-residual transducer of $f$ if the following conditions hold:

• $\mathcal{T}$ computes $f$;

• $Q = \text{Res}(f)/\sim_{k-1}$;

• for all $w \in A^*$, $w \triangleright f \in \delta^*(q_0, w)$;

• $\lambda(Q, A) \subseteq \text{Span}_{\mathbb{Z}}(\text{Res}(f)) \cap \mathbb{Z}$Poly$_{k-1}$.

Given a regular language $L$, the 0-residual transducer of its indicator function $\mathbf{1}_L$ can easily be identified with the minimal automaton of the language $L$, like in Example IV.12. However, for $k \ge 1$, the $k$-residual transducer of $f \in \mathbb{Z}$Poly$_k$ may not be unique. More precisely, two $k$-residual transducers share the same underlying automaton $(A, Q, \delta, \lambda)$, but the labels $\lambda$ of the transitions may not be the same.

**Example IV.14.** The $\mathbb{Z}$Poly$_{-1}$-transducer (resp. $\mathbb{Z}$Poly$_0$-transducer) from Figure 3 is a 0-residual transducer (resp. 1-residual transducer) of $\mathbf{1}_{aA^*}$. Let us check it for the 1-residual transducer. First note that $b \triangleright \mathbf{1}_{aA^*} \sim_0 a \triangleright \mathbf{1}_{aA^*} \sim_0 \mathbf{1}_{aA^*}$, hence $|\text{Res}(\mathbf{1}_{aA^*})/\sim_0| = 1$. Thus a 1-residual transducer of $\mathbf{1}_{aA^*}$ has exactly one state $q_0$. Furthermore the labels of the transitions of our transducer belong to $\lambda(Q, A) \subseteq \text{Span}_{\mathbb{Z}}(\text{Res}_f(a))$ since $1 - \mathbf{1}_{aA^*} = (a \triangleright \mathbf{1}_{aA^*}) - \mathbf{1}_{aA^*}$.

**Example IV.15.** Let $A := \{a, b\}$. The function $f: w \mapsto |w|_a \times |w|_b \in \mathbb{Z}$Poly$_2$ has a single residual up to $\sim_1$-equivalence. A 2-residual transducer of $f$ is depicted in Figure 4a.

**Example IV.16.** Let $A := \{a\}$. The function $g: w \mapsto (-1)^{|w|} \times |w| \in \mathbb{Z}$Poly$_1$ has two residuals up to $\sim_0$-
equivalence. A 1-residual transducer of $g$ is depicted in Figure 4b.

<figure><img src="image_6.png" /></figure>

(a) A 2-residual transducer of $f: w \mapsto |w|_a|w|_b$.

<figure><img src="image_7.png" /></figure>

(b) A 1-residual transducer of $g: w \mapsto (-1)^{|w|}|w|$.

<figure><img src="image_8.png" /><figcaption>Fig. 5: Example of a partial execution of Algorithm 1 to build a $k$-residual transducer of a function $f: A^* \to \mathbb{Z}$ such that $aa\triangleright f \sim_k b\triangleright f$. Nodes are labelled by their creation time. At this stage, $Q = \{\varepsilon\triangleright f\}$, $O = \{a\triangleright f, b\triangleright f\}$. The red node is not created, and the blue transition is added instead, corresponding to the “else” branch line 10 of Algorithm 1.</figcaption></figure>

Now, let us describe how to build a $k$-residual transducer for any $f \in \mathbb{Z}\text{Poly}_k$. As an illustration of how Algorithm 1 works, we refer the reader to Figure 5.

**Lemma IV.17.** Let $k \ge 0$. Given $f: A^* \to \mathbb{Z}$ such that $\text{Res}(f)/\sim_{k-1}$ is finite, Algorithm 1 builds a $k$-residual transducer of $f$. Its steps are effective given $f \in \mathbb{Z}\text{Poly}_k$.

**Remark IV.18.** 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 \in \mathbb{Z}\text{Poly}_k$

1 $O := \{\varepsilon\triangleright f\}$;
2 $Q := \emptyset$;
3 **while** $O \neq \emptyset$ **do**
4 &nbsp;&nbsp;&nbsp;&nbsp;choose $w\triangleright f \in O$;
5 &nbsp;&nbsp;&nbsp;&nbsp;**for** $a \in A$ **do**
6 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $wa\triangleright f \sim_{k-1} v\triangleright f$ for all $v\triangleright f \in O \uplus Q$ **then**
7 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$O := O \uplus \{wa\triangleright f\}$;
8 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\delta(w\triangleright f, a) := wa\triangleright f$;
9 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\lambda(w\triangleright f, a) := 0$;
10 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else**
11 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;let $f\triangleright v \in O \uplus Q$ be such that
12 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$wa\triangleright f \sim_{k-1} v\triangleright f$;
13 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\delta(w\triangleright f, a) := v\triangleright f$;
14 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\lambda(w\triangleright f, a) := wa\triangleright f - v\triangleright f$;
15 &nbsp;&nbsp;&nbsp;&nbsp;**end**
16 $O := O \setminus \{w\triangleright f\}$;
17 $Q := Q \uplus \{w\triangleright f\}$;
18 $F(w\triangleright f) := f(w)$;
19 **end**

We deduce from Lemma IV.17 that $\mathbb{Z}\text{Poly}_{k-1}$-transducers describe exactly the class $\mathbb{Z}\text{Poly}_k$ (Corollary IV.19).

**Corollary IV.19.** For all $k \ge 0$, $\mathbb{Z}\text{Poly}_k$ is the class of functions which can be computed by a $\mathbb{Z}\text{Poly}_{k-1}$-transducer. Furthermore, the conversions are effective.

**Corollary IV.20** (To be compared to Remark IV.5). For all $k \ge 0$, $\mathbb{Z}\text{Poly}_k = \{f: A^* \to \mathbb{Z} : \text{Res}(f)/\sim_{k-1} \text{ is finite}\}$.

## V. STAR-FREE $\mathbb{Z}$-POLYREGULAR FUNCTIONS

In this section, we study the subclass of $\mathbb{Z}$-polyregular functions that are built by using only FO-formulas, that we call *star-free $\mathbb{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 $\mathbb{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 $\mathbb{Z}$-polyregular functions, that specialize the results of Section II.

**Definition V.1 (Star-free $\mathbb{Z}$-polyregular).** For $k \ge 0$, we let $\mathbb{Z}\text{SF}_k := \text{Span}_\mathbb{Z}(\{\#\varphi : \varphi \in \text{FO}_\ell, \ell \le k\})$. Let $\mathbb{Z}\text{SF} := \bigcup_k \mathbb{Z}\text{SF}_k$, it is the class of star-free $\mathbb{Z}$-polyregular functions.

We also let $\mathbb{Z}\text{SF}_{-1} := \{0\}$. Similarly to $\mathbb{Z}\text{Poly}_k$, $\mathbb{Z}\text{SF}_k = \text{Span}_\mathbb{Z}(\{\#\varphi : \varphi \in \text{MSO}_k\} \cup \{\mathbf{1}_{\{\varepsilon\}}\})$.

**Example V.2.** $\mathbb{Z}\text{SF}_0$ is exactly the set of functions of the form $\sum_i \delta_i \mathbf{1}_{L_i}$ where the $\delta_i \in \mathbb{Z}$ and the $\mathbf{1}_{L_i}$ are indicator functions of star-free languages (compare with Example II.8).
**Example V.3.** The function $w \mapsto |w|_a \times |w|_b$ is in $\mathbb{Z}\mathbb{S}F_1$. Indeed, the formulas given in Example II.3 are in FO.

Now, we give an analogue of Theorem II.20 that characterizes $\mathbb{Z}\mathbb{S}F$ as $\mathbb{Z}$-rational expressions based on indicators of star-free languages, forbidding the use of the Kleene star.

**Theorem V.4.** Let $f: A^* \to \mathbb{Z}$, the following are (effectively) equivalent:

1) $f$ is a star-free $\mathbb{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 $\mathbb{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

$$ \mathbb{Z}\mathbb{S}F_k = \operatorname{Span}_{\mathbb{Z}}(\{\mathbf{1}_{L_0} \otimes \cdots \otimes \mathbf{1}_{L_k} : L_0, \dots, L_k \text{ star-free languages}\}) \quad (3) $$

and the result follows. □

**Example V.5.** The function $1_{A^*a} \otimes 1_{A^*}: w \mapsto |w|_a$ belongs to $\mathbb{Z}\mathbb{S}F_1$, and the function $1_{A^*a} \otimes 1_{A^*} \otimes 1_{bA^*} + 1_{A^*b} \otimes 1_{A^*} \otimes 1_{aA^*}: w \mapsto |w|_a \times |w|_b$ belongs to $\mathbb{Z}\mathbb{S}F_2$.

### A. Deciding star-freeness

Now, we intend to show that given a $\mathbb{Z}$-polyregular function, we can decide if it is star-free. Furthermore, we provide a semantic characterization of star-free $\mathbb{Z}$-polyregular functions leveraging ultimate $N$-polynomiality. We recall (see Definition II.29) that a function $f: A^* \to \mathbb{Z}$ is ultimately 1-polynomial when, for all $\alpha_0, w_1, \alpha_1, \dots, w_\ell; \alpha_\ell \in A^*$, there exists $P \in \mathbb{Q}[X_1, \dots, X_\ell]$, such that $f(\alpha_0 w_1^{X_1} \alpha_1 \cdots w_\ell^{X_\ell} \alpha_\ell) = P(X_1, \dots, X_\ell)$, for $X_1, \dots, X_\ell$ 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 \mapsto |w|_a \times |w|_b$ is ultimately 1-polynomial. As a counterexample, recall the map $f: w \mapsto (-1)^{|w|} \times |w|$. The map $f$ is ultimately 2-polynomial because $X \mapsto (-1)^{2X+1}(2X+1)$ and $X \mapsto (-1)^{2X}2X$ are both polynomials. However, $f$ is not ultimately 1-polynomial since $X \mapsto (-1)^X X$ is not a polynomial.

Now, let us state the main theorem of this section.

**Theorem V.8.** Let $k \ge 0$ and $f \in \mathbb{Z}\mathbb{P}\mathbb{O}\mathbb{y}_k$. The following properties are (effectively) equivalent:

1) $f \in \mathbb{Z}\mathbb{S}F$;

2) $f \in \mathbb{Z}\mathbb{S}F_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 $\mathbb{Z}\mathbb{S}F_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 [26].

**Corollary V.9.** $\mathbb{Z}\mathbb{S}F_k = \mathbb{Z}\mathbb{S}F \cap \mathbb{Z}\mathbb{P}\mathbb{O}\mathbb{y}_k$.

**Corollary V.10 (FO free variable minimization).** Let $f \in \mathbb{Z}\mathbb{S}F$, then $f \in \mathbb{Z}\mathbb{S}F_k$ if and only if $|f(w)| = \mathcal{O}(|w|^k)$. This property is decidable and the construction is effective.

*Proof.* Let $f \in \mathbb{Z}\mathbb{S}F$ be such that $|f(w)| = \mathcal{O}(|w|^k)$. By Theorem III.3 we get $f \in \mathbb{Z}\mathbb{P}\mathbb{O}\mathbb{y}_k$, thus by Theorem V.8, $f \in \mathbb{Z}\mathbb{S}F_k$. All the steps are effective and decidable. □

The rest of Section V-A is devoted to sketching the proof of Theorem V.8. Given $f \in \mathbb{Z}\mathbb{P}\mathbb{O}\mathbb{y}_k$, the main idea is to use its $k$-residual transducer to decide whether $f \in \mathbb{Z}\mathbb{S}F_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.

**Definition V.11 (Counter-free).** A deterministic automaton $(A, Q, q_0, \delta)$ is counter-free if for all $q \in Q$, $u \in A^*$, $n \ge 1$, if $\delta(q, u^n) = q$ then $\delta(q, u) = q$ (see e.g. [4]). We say that a $\mathcal{H}$-transducer is counter-free if its underlying automaton is so.

**Example V.12.** The $\mathbb{Z}\mathbb{P}\mathbb{O}\mathbb{y}_0$-transducer depicted in Figure 4b is not counter-free, since $\delta(q_0, aa) = q_0$ but $\delta(q_0, a) \ne 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 \ge 0$ and $f \in \mathbb{Z}\mathbb{P}\mathbb{O}\mathbb{y}_k$, the following conditions are equivalent:

1) $f \in \mathbb{Z}\mathbb{S}F$;

2) $f$ is ultimately 1-polynomial;

3) for all $k$-residual transducer of $f$, this transducer is counter-free and has labels in $\mathbb{Z}\mathbb{S}F_{k-1}$;

4) there exists a counter-free $\mathbb{Z}\mathbb{S}F_{k-1}$-transducer that computes $f$;

5) $f \in \mathbb{Z}\mathbb{S}F_k$.

Furthermore, this property is decidable and the constructions are effective.

The proof of Theorem V.13 will be done by induction on $k \ge 0$. First, let us note that a counter-free transducer computes a star-free function (provided that the labels are star-free).

**Lemma V.14.** Let $k \ge 0$, a counter-free $\mathbb{Z}\mathbb{S}F_{k-1}$-transducer (effectively) computes a function of $\mathbb{Z}\mathbb{S}F_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 \in \mathbb{Z}\mathbb{S}F$, then $f$ is ultimately 1-polynomial.

*Proof.* From Claim V.6 we get that $1_L$ is ultimately 1-polynomial 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.16.** Let $k \ge 0$. Let $f \in \mathbb{Z}\mathbb{Poly}_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 1-polynomial.

*Proof of Theorem V.13.* The (effective) equivalences are shown by induction on $k \ge 0$. For Item 5 $\Rightarrow$ Item 1, the implication is obvious. For Item 1 $\Rightarrow$ Item 2 we apply Lemma V.15. For Item 2 $\Rightarrow$ Item 3, we use Lemma V.16 which shows that any $k$-residual transducer of $f$ is counter-free and has ultimately 1-polynomial labels. Since these labels are in $\mathbb{Z}\mathbb{Poly}_{k-1}$, then by induction hypothesis they belong to $\mathbb{Z}\mathbb{SF}_{k-1}$. For Item 3 $\Rightarrow$ Item 4, the result follows because there exists a $k$-residual transducer computing $f$. For Item 4 $\Rightarrow$ 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 \ge 0$. Given $f \in \mathbb{Z}\mathbb{Poly}_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 $\mathbb{Z}\mathbb{SF}_{k-1}$ (since they belong to $\mathbb{Z}\mathbb{Poly}_{k-1}$). □

## B. Relationship with polyregular functions and rational series

Let us now specialize the multiple characterizations of $\mathbb{Z}\mathbb{Poly}$ presented in Section II to $\mathbb{Z}\mathbb{SF}$, 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 star-free $\mathbb{Z}$-polyregular functions are obtained by post composition with sum, in a similar way as Proposition II.13.

**Proposition V.17.** The class $\mathbb{Z}\mathbb{SF}$ is (effectively) the class of functions $\text{sum} \circ f$ where $f: A^* \to \{\pm 1\}^*$ is first-order polyregular.

Now, let us provide a description of $\mathbb{Z}\mathbb{SF}$ in terms of eigenvalues in the spirit of Theorem II.31. Intuitively, it shows that a linear representation $(I, \mu, F)$ computes a function in $\mathbb{Z}\mathbb{SF}$ if and only if $\text{Spec}(\mu(A^*))$ contains no non-trivial subgroup, mimicking the notion of *aperiodicity* for monoids<fnref n="1" />.

**Theorem V.18 (Star-free).** Let $f: A^* \to \mathbb{Z}$, the following are (effectively) equivalent:

1) $f$ is a star-free $\mathbb{Z}$-polyregular function;

2) $f$ is a $\mathbb{Z}$-rational series and for all minimal linear representation $(I, \mu, F)$ of $f$, $\text{Spec}(\mu(A^*)) \subseteq \{0, 1\}$;

3) $f$ is a $\mathbb{Z}$-rational series and there exists a linear representation $(I, \mu, F)$ of $f$ such that $\text{Spec}(\mu(A^*)) \subseteq \{0, 1\}$.

*Proof.* For Item 2 $\Rightarrow$ Item 3, the result is obvious.

For Item 1 $\Rightarrow$ Item 2, consider a minimal presentation of $f$ using $(I, \mu, F)$ of dimension $n$. Then consider a word $w$, $\lambda$ a complex eigenvalue of $\mu(w)$. Thanks to Lemma II.28, there exists $w, \alpha_{i,j}, u_i, v_j \in A^*$ for $1 \le i, j \le n$ such that $\lambda^X = \sum_{i,j=1}^n \alpha_{i,j} f(v_i w^X u_j)$. Because $f \in \mathbb{Z}\mathbb{SF}$, $f$ is ultimately 1-polynomial thanks to Theorem V.13. This entails that $X \mapsto \lambda^X$ is a polynomial for $X$ large enough. Therefore, $\lambda \in \{0, 1\}$.

For Item 3 $\Rightarrow$ 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 $\mu(w) \in \mathcal{M}^{n,n}(\mathbb{Z})$ for $w \in A^*$ are all in $\{0, 1\}$, its characteristic polynomial splits over $\mathbb{Q}$, hence there exists $P \in \mathcal{M}^{n,n}(\mathbb{Q})$ such that $T := PM_w P^{-1}$ is upper triangular with diagonal values in $\{0, 1\}$. In particular, $\mu(w)^X = P^{-1}T^X P$, but a simple induction proves that the coefficients of $T^X$ are in $\mathbb{Q}[X]$ for large enough $X$, hence so does $\mu(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 $\mathbb{Z}$-polyregular. □

**Remark V.19.** When showing Item 3 $\Rightarrow$ Item 1, we have in fact shown that the following weaker form of ultimate 1-polynomiality characterizes $\mathbb{Z}\mathbb{SF}$ among $\mathbb{Z}$-rational series: for all $u, w, v \in A^*$, there exists $P \in \mathbb{Q}[X]$, such that $f(uw^Xv) = 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 \in A^*$, then $|1_{\text{odd}}(uw^Xv)| \le 1$ for every $X \ge 0$. However, $1_{\text{odd}} \notin \mathbb{Z}\mathbb{SF}$.

As a concluding example, let us observe that our notion of star-free $\mathbb{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 \mapsto (-1)^{|w|}|w|$ is definable in weighted first order logic (however, $f \notin \mathbb{Z}\mathbb{SF}$ as shown in Example V.7). Similarly, the indicator function $1_{\text{odd}}$ is also definable in weighted first order logic, even though the language of words of odd length is not star-free.

# 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

<footnote n="1">¹Beware: the spectrum of a linear representation may not be a semigroup.</footnote>
that these results together with the technical tools introduced
to prove them open the range towards a vast study of $\mathbb{Z}$- and $\mathbb{N}$
polyregular functions. Now, let us discuss a few tracks which
seem to be promising for future work.

Weaker logics: Boolean combinations of existential first-order formulas define a well-known subclass of first-order logic, often denoted $\mathcal{B}(\exists FO)$. Over finite words, $\mathcal{B}(\exists FO)$-sentences describe the celebrated class of piecewise testable languages (see e.g. [6]). In our quantitative setting, one could define for all $k \ge 0$ the class of linear combinations of the counting formulas from $\mathcal{B}(\exists FO)_k$, as we did for $\mathbb{Z}\text{Poly}_k$ (resp. $\mathbb{Z}\text{SF}_k$) with $\text{MSO}_k$ (resp. $\text{FO}_k$). While this class seems to be a good candidate for defining “piecewise testable $\mathbb{Z}$-polyregular 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 $\mathbf{1}_{aA^*} = \#\varphi$ for $\varphi(x) := a(x) \wedge \forall y. y \ge x \in \mathcal{B}(\exists FO)_1$. Even if $|\mathbf{1}_{aA^*}(w)| = \mathcal{O}(1)$, this function cannot be written as a linear combination of counting formulas from $\mathcal{B}(\exists FO)_0$. Indeed, if we assume the converse, then $\mathbf{1}_{aA^*}$ could be written $\sum_{i=1}^n \delta_i \mathbf{1}_{L_i}$ for some piecewise testable languages $L_i$, which implies that $aA^*$ would be piecewise testable, which is not the case.

Star-free $\mathbb{N}$-polyregular functions: A very natural question is, given an $\mathbb{N}$-polyregular function (recall that it is an element of $\mathbb{N}\text{Poly} := \text{Span}_{\mathbb{N}}(\#\varphi : \varphi \in \text{MSO})$) to decide whether it is in fact a star-free $\mathbb{N}$-polyregular function (i.e. an element of $\mathbb{NSF} := \text{Span}_{\mathbb{N}}(\#\varphi : \varphi \in \text{FO}))$. In this setting, we conjecture that $\mathbb{NSF} = \mathbb{N}\text{Poly} \cap \mathbb{Z}\text{SF}$. 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 $\mathbb{N}$-polyregular function may need labels which are not $\mathbb{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 $\mathbb{Z}$-rational series: In Figure 1, there is no generalization of the class $\mathbb{Z}\text{SF}$ among the whole class of $\mathbb{Z}$-rational series. We are not aware of a way to define a class of “star free $\mathbb{Z}$-rational series”, neither with logics nor with $\mathbb{Z}$-rational expressions. Indeed, allowing the use of Kleene star for series automatically builds the whole class of $\mathbb{Z}$-rational series (including the indicator functions of all regular languages).

From a logical standpoint, it is tempting to go from poly-
nomial behaviors to exponential ones by shifting from first-
order free variables to second-order free variables. While
this approach actually captures the whole class of $\mathbb{Z}$-rational
series, it fails to circumscribe star-freeness. To make the above
statement precise, let us write $\text{MSO}^X$ (resp. $\text{FO}^X$) as the set
of $\text{MSO}$ (resp. $\text{FO}$) formulas with free second-order variables,
i.e. of the shape $\varphi(X_1, \dots, X_k)$. Given $\varphi \in \text{MSO}^X$, we let
$\#\varphi(w) : A^* \to \mathbb{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 \mapsto (-2)^{|w|} \notin \mathbb{Z}\text{Poly}$.

**Example VI.1.** Let $\varphi(X) := \top$, then $\#\varphi(w) = 2^{|w|}$. Let $\psi(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 \in X$, then $x+1 \notin X$ and $x+2 \in X$. It is an easy check that $\#\psi = \mathbf{1}_{\text{odd}}$, even though $\psi \in \text{FO}^X$ (but recall that $\mathbf{1}_{\text{odd}}$ is the indicator function of a non star-free regular language). Now, $w \mapsto (-2)^{|w|}$ equals $\#\varphi \times (2\#\psi - 1)$.

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

**Proposition VI.2.** For every function $f: A^* \to \mathbb{Z}$, the following are equivalent:

1) $f$ is a $\mathbb{Z}$-rational series;

2) $f \in \operatorname{Span}_{\mathbb{Z}}(\{\#\varphi : \varphi \in \text{MSO}^X\})$;

3) $f \in \operatorname{Span}_{\mathbb{Z}}(\{\#\varphi : \varphi \in \text{FO}^X\})$.

In our setting, it seems natural to say that $w \mapsto 2^{|w|}$ should
be a star-free $\mathbb{Z}$-rational series, contrary to $w \mapsto (-2)^{|w|}$ (as
observed in Example V.21, this approach contrasts with the
weighted logics of Droste and Gastin [27], for which $(-2)^{|w|}$
is considered as “star free”). Recall that in Theorem V.18,
we have characterized $\mathbb{Z}\text{SF}$ as the class of series whose
spectrum falls in $\{0, 1\}$. Following this result, we conjecture
that a “good” notion of star-free $\mathbb{Z}$-rational series could be
those whose spectrum falls in the set $\mathbb{R}_+$ of nonnegative real
numbers. This way, exponential growth is allowed (e.g. for
$w \mapsto 2^{|w|}$) but no periodic behaviors (e.g. for $w \mapsto (-2)^{|w|}$).
REFERENCES

[1] S. C. Kleene et al., "Representation of events in nerve nets and finite automata," *Automata studies*, vol. 34, pp. 3-41, 1956.

[2] J. R. Büchi, "Weak second-order arithmetic and finite automata," *Mathematical Logic Quarterly*, vol. 6, no. 1-6, 1960.

[3] M. P. Schützenberger, "On the definition of a family of automata," *Inf. Control.*, vol. 4, no. 2-3, pp. 245-270, 1961.

[4] R. McNaughton and S. A. Papert, *Counter-Free Automata*. The MIT Press, 1971.

[5] M. P. Schützenberger, "On finite monoids having only trivial subgroups," *Information and Control*, vol. 8, no. 2, pp. 190-194, Apr. 1965.

[6] D. Perrin and J.-E. Pin, "First-order logic and star-free sets," *Journal of Computer and System Sciences*, vol. 32, no. 3, pp. 393-406, 1986.

[7] M. Bojańczyk, "Polyregular Functions," 2018. [Online]. Available: https://arxiv.org/abs/1810.08760

[8] D. Scott, "Some definitional suggestions for automata theory," *Journal of Computer and System Sciences*, vol. 1, no. 2, pp. 187-212, 1967.

[9] E. Filiot, O. Gauwin, and N. Lhote, "Aperiodicity of rational functions is pspace-complete," in *36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)*. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016.

[10] E. Filiot, O. Gauwin, N. Lhote, and A. Muscholl, "On canonical models for rational functions over infinite words," in *38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)*, vol. 122. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018.

[11] S. Kreutzer and C. Riveros, "Quantitative monadic second-order logic," in *2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science*, 2013, pp. 113-122.

[12] M. P. Schützenberger, "Finite counting automata," *Information and control*, vol. 5, no. 2, pp. 91-107, 1962.

[13] J. Berstel and C. Reutenauer, *Noncommutative rational series with applications*. Cambridge University Press, 2011, vol. 137.

[14] G. Douéneau-Tabot, "Pebble transducers with unary output," in *46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021*, 2021.

[15] M. Bojańczyk, "Transducers of polynomial growth," in *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science*, 2022, pp. 1-27.

[16] G. Douéneau-Tabot, "Pebble minimization: the last theorems," in *26th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2023*, 2023.

[17] M. Bojańczyk, "The growth rate of polyregular functions," 2022. [Online]. Available: https://arxiv.org/abs/2212.11631

[18] W. Thomas, "Languages, automata, and logic," in *Handbook of formal languages*. Springer, 1997, pp. 389-455.

[19] G. Douéneau-Tabot, "Hiding pebbles when the output alphabet is unary," in *49th International Colloquium on Automata, Languages, and Programming, ICALP 2022*, 2022.

[20] J. Engelfriet and H. J. Hoogeboom, "MSO definable string transductions and two-way finite-state transducers," *ACM Transactions on Computational Logic (TOCL)*, vol. 2, no. 2, pp. 216-254, 2001.

[21] M. Bojanczyk, S. Kiefer, and N. Lhote, "String-to-String Interpretations With Polynomial-Size Output," in *46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)*, 2019.

[22] J. P. Bell, "A gap result for the norms of semigroups of matrices," *Linear Algebra and its Applications*, vol. 402, pp. 101-110, 2005.

[23] I. Simon, "Factorization forests of finite height," *Theor. Comput. Sci.*, vol. 72, no. 1, pp. 65-94, 1990.

[24] T. Colcombet, "Green's relations and their use in automata theory," in *International Conference on Language and Automata Theory and Applications*. Springer, 2011, pp. 1-21.

[25] G. Douéneau-Tabot, E. Filiot, and P. Gastin, "Register transducers are marble transducers," in *45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020*, 2020.

[26] T. Colcombet, S. van Gool, and R. Morvan, "First-order separation over countable ordinals," in *Foundations of Software Science and Computation Structures*, ser. Lecture Notes in Computer Science, P. Bouyer and L. Schröder, Eds. Cham: Springer International Publishing, 2022, pp. 264-284.

[27] M. Droste and P. Gastin, "Aperiodic weighted automata and weighted first-order logic," in *44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019*, vol. 138, 2019.
APPENDIX A
PROOFS OF SECTION II

A. *Proof of Proposition II.12*

In this section, we show that the functions of $\mathbb{Z}\text{Poly}_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 \le j \le k$, a formula $\varphi_j^{\text{Dom}}(x) \in \text{MSO}_1$;

* for all $1 \le j \le k$ and $a \in B$, a formula $\varphi_j^a(x) \in \text{MSO}_1$;

* for all $1 \le j, j' \le k$, a formula $\varphi_{j,j'}^{<}(x, x') \in \text{MSO}_2$.

Let $w \in A^*$, we define the domain $D(w) := \{(i, j) : 1 \le i \le |w|, 1 \le j \le k, w \models \varphi_j^{\text{Dom}}(i)\}$. Using the formulas $\varphi_j^b(x)$ (resp. $\varphi_{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 \in B^*$, for all $w \in A^*$. In this case, the transduction computes the function that maps $w \in A^*$ to this $v \in B^*$.

It follows from [20] that regular functions can (effectively) be described by MSO-transductions.

**Claim A.2.** Let $\ell \ge 0$, $k \ge 1$, $\psi(x_1, \dots, x_\ell) \in \text{MSO}_\ell$ be a formula over B and $f: A^* \to B^*$ be computed by a k-copying MSO-transduction. Let us write $W := \{x_1, \dots, x_\ell\}^{\{1, \dots, k\}}$. There exists formulas $\theta_\rho \in \text{MSO}_\ell$ over A where $\rho$ ranges in $W$, such that for all $w \in A^*$, $\#\varphi(f(w)) = \sum_{\rho \in W} \#\theta_\rho(w)$.

*Proof Sketch.* Assume that the transduction is given by formulas $\varphi_j^{\text{Dom}}(x)$, $\varphi_j^a(x) \in \text{MSO}_1$ for $a \in B$ and $\varphi_{j,j'}^{<}(x, x') \in \text{MSO}_2$ as in Definition A.1. Let $\psi$ be an MSO formula over B with first order variables $x_1, \dots, x_\ell$ and second order variables $(X_1, \dots, X_k), (Y_1, \dots, Y_k), \dots$. Let $\rho$ be a mapping from $\{x_1, \dots, x_\ell\}$ to $\{1, \dots, k\}$. We define by induction on $\psi$ the formula $\psi_\rho$ as follows (it roughly translates the formula from B to A using the transduction):

$$
\begin{align*}
(\exists x. \varphi)_\rho &:= \bigvee_{j=1}^k \exists x. \varphi_j^{\text{Dom}}(x) \wedge \varphi_{\rho+[x \mapsto j]} \\
(\exists X. \varphi)_\rho &:= \exists X_1, \dots, X_k \bigwedge_{j=1}^k (\forall x \in X_j, \varphi_j^{\text{Dom}}(x)) \wedge \varphi_\rho \\
(\neg \varphi)_\rho &:= \neg (\varphi_\rho) \\
(\varphi \lor \varphi')_\rho &:= \varphi_\rho \lor \varphi'_\rho \\
(P_a(x))_\rho &:= \varphi_{\rho(x)}^a(x) \\
(x < y)_\rho &:= \varphi_{\rho(x), \rho(y)}^<(x, y). \\
(x \in X)_\rho &:= \bigvee_{j=1}^k \varphi_j^{\text{Dom}}(x) \wedge (x \in X_j)
\end{align*}
$$

It is then a mechanical check that the translation works as expected. In the following equation, we fix $w \in A^*$ and we let pos: $D(w) \to [1:|f(w)|]$ be the function that maps a tuple $(i, j)$ to the corresponding position in the word $f(w) \in B^*$. To simplify notations, given $\rho \in W$, a word $w \in A^*$, and a valuation $\tau: \{x_1, \dots, x_\ell\} \to [1:|w|]$, we write
$\mathrm{pos}[\tau \times \rho](\vec{x}) := \mathrm{pos}(\tau(x_1), \rho(x_1)), \dots, \mathrm{pos}(\tau(x_\ell), \rho(x_\ell)).$

$$
\begin{align*}
\#\varphi(f(w)) &= \#\{\nu: \{x_1, \dots, x_\ell\} \to [1:\lfloor f(w) \rfloor] : f(w) \models \psi(\nu(x_1), \dots, \nu(x_\ell))\} \\
&= \sum_{\rho \in W} \#\{\tau: \{x_1, \dots, x_\ell\} \to [1:\lfloor w \rfloor] : f(w) \models \psi(\mathrm{pos}[\tau \times \rho](\vec{x}))\} \\
&= \sum_{\rho \in W} \#\{\nu: \{x_1, \dots, x_\ell\} \to \{1, \dots, \lfloor w \rfloor\} : w \models \psi_\rho(\nu) \wedge \bigwedge_{i=1}^\ell \varphi_{\rho(\nu(x_i))}^{\mathrm{Dom}}(x_i)\}
\end{align*}
$$

We then let $\theta_\rho := \psi_\rho \wedge \bigwedge_{i=1}^\ell \varphi_{\rho(x_i)}^{\mathrm{Dom}}(x_i)$ to conclude. $\square$

<figure><img src="image_9.png" /></figure>

The result follows immediately since $\mathbb{Z}\mathrm{Poly}_\ell$ is closed under taking sums and $\mathbb{Z}$-external products.

## B. Proof of Proposition II.13

We first show that any $\mathbb{Z}$-polyregular function can be written under the form $\sum \circ g$ where $g: A^* \to \{\pm 1\}^*$ is polyregular. This is an immediate consequence of the following claims.

**Claim A.3.** For all $\varphi \in \mathrm{MSO}$, there exists a polyregular function $f: A^* \to \{\pm 1\}^*$ such that $\#\varphi = \sum \circ f$.

*Proof.* Polyregular functions are characterized in [21, Theorem 7] as the functions computed by (multidimensional) MSO-interpretations. Recall that an MSO-interpretation of dimension $k \in \mathbb{N}$ is given by a formula $\varphi_\leq(\vec{x}, \vec{y})$ defining a total ordering over $k$-tuples of positions, a formula $\varphi^{\mathrm{Dom}}(\vec{x})$ that selects valid positions, and formulas $\varphi^a(\vec{x})$ that place the letters over the output word [21, Definition 1 and 2]. In our specific situation, letting $\varphi_\leq$ 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 $\varphi^{\mathrm{Dom}}$ be defined as $\varphi$ 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. $\square$

**Claim A.4.** The set $\{\sum \circ f : f : A^* \to \{\pm 1\}^* \text{ polyregular}\}$ is closed under sums and external $\mathbb{Z}$-products.

*Proof.* Notice that $\sum \circ f + \sum \circ g = \sum \circ (f \cdot g)$ where $f \cdot g(w) := f(w) \cdot g(w)$. As polyregular functions are closed under concatenation [7], the set of interest is closed under sums. To prove that it is closed under external $\mathbb{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). $\square$

Let us consider a polyregular function $g: A^* \to \{\pm 1\}^*$. The maps $g_+: w \mapsto |g(w)|_1$ and $g_-: w \mapsto |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 [7]). Hence $g_-$ and $g_+$ are polyregular functions with unary output, a.k.a. $\mathbb{N}$-polyregular functions. As a consequence, $\sum \circ g = g_+ - g_-$ lies in $\mathbb{Z}\mathrm{Poly}$.

# APPENDIX B

## PROOFS OF SECTION II-C

### A. Proof of Claim II.17

Let $f \in \mathbb{Z}\mathrm{Poly}_k$ and $g \in \mathbb{Z}\mathrm{Poly}_\ell$, we (effectively) show that $f \otimes g \in \mathbb{Z}\mathrm{Poly}_{k+\ell+1}$.
First, observe that if $f, g, h: A^* \to \mathbb{Z}$ and $\gamma, \delta \in \mathbb{Z}$, then $(\gamma f + \delta g) \otimes h = \gamma (f \otimes g) + \delta (g \otimes h)$. Thus it is sufficient to show the result for $f = \#\varphi$ and $g = \#\psi$ with $\varphi(x_1, \dots, x_k) \in \mathrm{MSO}_k$ and $\psi(y_1, \dots, y_\ell) \in \mathrm{MSO}_\ell$. For all $w \in A^*$ we have:

$$ \begin{aligned} (\#\varphi \otimes \#\psi)(w) &= \sum_{0 \le i \le |w|} \sum_{i_1, \dots, i_k \le i} \sum_{j_1, \dots, j_\ell > i} \mathbf{1}_{w[1:i]=\varphi(i_1, \dots, i_k)} \times \mathbf{1}_{w[i+1:|w|]=\psi'(j_1, \dots, j_\ell)} \\ &= \#\varphi(\varepsilon) \cdot \#\psi(w) \\ &\quad + \sum_{1 \le i \le |w|} \sum_{i_1, \dots, i_k \le i} \sum_{j_1, \dots, j_\ell > i} \mathbf{1}_{w[1:i]=\varphi(i_1, \dots, i_k)} \times \mathbf{1}_{w[i+1:|w|]=\psi'(j_1, \dots, j_\ell)} \\ &= \#\varphi(\varepsilon) \cdot \#\psi(w) + \#(\varphi'(z, x_1, \dots, x_k) \wedge \psi'(z, y_1, \dots, y_\ell))(w) \end{aligned} $$

where $\varphi'(z, x_1, \dots, x_k) \in \mathrm{MSO}_{k+1}$ is a formula such that $w \models \varphi'(i, i_1, \dots, i_k)$ if and only if $i_1, \dots, i_k \le i$ and $w[1:i] \models \varphi(i_1, \dots, i_k)$ (this is a regular property which is MSO definable), and similarly for $\psi'$.

## B. Proof of Proposition II.18

Let $k \ge 0$, we want to show that $\mathbb{Z}\mathrm{Poly}_{k+1} = \mathrm{Span}_{\mathbb{Z}}(\{\mathbf{1}_L \otimes f : L \text{ regular}, f \in \mathbb{Z}\mathrm{Poly}_k\})$. Observe that for all $f: A^* \to \mathbb{Z}$, $\mathbf{1}_{\{\varepsilon\}} \otimes f$ equals $f$, therefore $\mathbb{Z}\mathrm{Poly}_k \subseteq \mathrm{Span}_{\mathbb{Z}}(\{\mathbf{1}_L \otimes f : L \text{ regular}, f \in \mathbb{Z}\mathrm{Poly}_k\})$. As in the proof of Claim II.17, it is sufficient to show that $\#\varphi$ for $\varphi(x_1, \dots, x_{k+1}) \in \mathrm{MSO}_{k+1}$, can be written as a linear combination of $\mathbf{1}_L \otimes f$ where $L$ is a regular language. Observe that for all $w \in A^+$, for all valuation $i_1, \dots, i_k$ of $x_1, \dots, x_k$, we can define $P := \{1 \le j \le k : i_j = \min\{i_1, \dots, i_k\}\}$ (i.e. the $x_j$ for $j \in P$ are the variables with minimal value). Therefore, for all $w \in A^+$:

$$ \#\varphi(w) = \sum_{\emptyset \subsetneq P \subseteq [1:k]} \sum_{w=uv, u \neq v} \#(\varphi \wedge \bigwedge_{j \in P} x_j = |u| \wedge \bigwedge_{j \notin P} x_j > |u|)(w). $$

It is an easy check that one can (effectively) build a regular language $L^P \subseteq A^+$ and a formula $\psi^P$ such that for all $u \in A^+$, $v \in A^*$, $uv \models \varphi \wedge \bigwedge_{j \in P} (x_j = |u|) \wedge (\bigwedge_{j \notin P} x_j > |u|)$ if and only if $u \in L^P$ and $v \models \psi^P((x_j)_{j \notin P})$. Thus, for all $w \in A^+$:

$$ \begin{aligned} \#\varphi(w) &= \sum_{\emptyset \subsetneq P \subseteq [1:k]} \sum_{w=uv} \mathbf{1}_{L^P}(u) \times \#\psi^P(v) \\ &= \sum_{\emptyset \subsetneq P \subseteq [1:k]} (\mathbf{1}_{L^P} \otimes \#\psi^P)(w) . \end{aligned} $$

Notice that $\psi^P$ has exactly $k - |P| \le k - 1$ free-variables, thus $g$ belongs to $\mathrm{Span}_{\mathbb{Z}}(\{\mathbf{1}_L \otimes f : L \text{ regular}, f \in \mathbb{Z}\mathrm{Poly}_k\})$. Observe moreover that $g(\varepsilon) = 0 = \#\varphi(\varepsilon)$ because $k+1 > 0$.

# APPENDIX C

## PROOFS OF SECTION II-D

### A. Proof of Lemma II.28

Let $f: A^* \to \mathbb{Z}$ be a $\mathbb{Z}$-rational series and $(I, \mu, F)$ be a minimal $\mathbb{Z}$-linear representation of $f$ of dimension $n$. First note that $(I, \mu, F)$ is also a minimal $\mathbb{Q}$-linear representation of $f$ by [13, Theorem 1.1 p 121] ($\mathbb{Q}$-linear representations are defined by allowing rational coefficients within the matrices and vectors, instead of integers). Let $w \in A^*$, $\lambda \in \mathrm{Spec}(\mu(w))$ and consider a complex eigenvector $V \in \mathcal{M}^{n,1}(\mathbb{C})$ associated to $\lambda$. We let $||V|| := {}^tVV$, observe that it is a positive real number. Because $(I, \mu, F)$ is a minimal $\mathbb{Q}$-linear representation of $f$, then $\mathrm{Span}_{\mathbb{Q}}(\{\mu(u)F : u \in A^*\}) = \mathbb{Q}^n$ by [13, Proposition 2.1 p 32]. Hence there exists numbers $\alpha_j \in \mathbb{C}$ and words $u_j \in A^*$ such that $V = \sum_{j=1}^n \alpha_j \mu(u_j)F$. Symmetrically by [13, Proposition 2.1 p 32], there exists numbers $\beta_i \in \mathbb{C}$ and words $v_i \in A^*$ such that ${}^tV = \sum_{i=1}^n \beta_i I \mu(v_i)$. Therefore:

$$ \lambda^X ||V|| = {}^tV \mu(w)^X V = \sum_{i,j=1}^{n} \alpha_i \beta_j I \mu(v_i w^X u_j) F = \sum_{i,j=1}^{n} \alpha_i \beta_j f(v_i w^X u_j). $$
The result follows since $||V|| \neq 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 \geq 0$ follows from the traditional pumping lemmas. Now let $f, g: A^* \to \mathbb{Z}$ be respectively ultimately $N_1$-polynomial and ultimately $N_2$-polynomial. The fact that $f+g$ and $\delta f$ for $\delta \in \mathbb{Z}$ are ultimately $(N_1 \times 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 \in \mathbb{N}$, $\sum_{i=0}^{X} i^p$ is a polynomial in $X$.

*Proof.* It is a folklore result, but let us prove it using finite differences. If $f: \mathbb{N} \to \mathbb{Q}$, let $\Delta f: n \mapsto f(n+1) - f(n)$. Let us now prove by induction that every function $f: \mathbb{N} \to \mathbb{Q}$ such that $\Delta^p f = 0$ for some $p \geq 1$ is a polynomial. For $p = 1$, this holds because $f$ must be constant. For $p+1 > 1$, if we assume that $\Delta^{p+1} f = 0$, then $\Delta^p f$ is a constant $C$. Let $g := f - C \frac{n^p}{p!}$, and remark that $\Delta^p g = 0$. By induction hypothesis $g$ is a polynomial, hence so is $f$.

Finally, a simple induction proves that $\Delta^{p+2}(X \mapsto \sum_{i=0}^{X} i^p) = 0$. □

**Claim C.2.** Let $P, Q \in \mathbb{Q}[X, Y_1, \dots, Y_\ell]$ be two multivariate polynomials, then their Cauchy product $P \otimes Q(X, Y_1, \dots, Y_\ell) := \sum_{i=0}^X P(i, Y_1, \dots, Y_\ell)Q(Y - i, Y_1, \dots, Y_\ell)$ belongs to $\mathbb{Q}[X, Y_1, \dots, Y_\ell]$.

*Proof.* By linearity of the Cauchy product, it suffices to check that the result holds for products of the form $(X^p Y_1^{p_1} \cdots Y_\ell^{p_\ell}) \otimes (X^q Y_1^{q_1} \cdots Y_\ell^{q_\ell}) = (X^p \otimes X^q) \times Y_1^{p_1} \cdots Y_\ell^{p_\ell} Y_1^{q_1} \cdots Y_\ell^{q_\ell}$. Hence, the only thing left to check is that $X^p \otimes X^q$ is a polynomial in $X$.

$$ 
\begin{align*}
X^p \otimes X^q(Y) &= \sum_{i=0}^{Y} i^p (Y - i)^q \\
&= \sum_{i=0}^{Y} i^p \sum_{k=0}^{q} \binom{q}{k} Y^k (-i)^{q-k} \\
&= \sum_{k=0}^{q} \binom{q}{k} Y^k \sum_{i=0}^{Y} i^p (-i)^{q-k} \\
&= \sum_{k=0}^{q} \binom{q}{k} (-1)^{q-k} Y^k \sum_{i=0}^{Y} i^{p+q-k}
\end{align*}
$$

Which is a polynomial thanks to Claim C.1. □

Let us now prove that $f \otimes g$ is ultimately $N := (N_1 \times N_2)$-polynomial. For that, let us consider $\alpha_0, u_1, \alpha_1, \dots, u_\ell, \alpha_\ell \in A^*$ and prove that $(f \otimes g)(\alpha_0 u_1^{NX_1} \alpha_1 \cdots u_\ell^{NX_\ell} \alpha_\ell)$ is a polynomial for $X_1, \dots, X_\ell$ large enough.

$$ 
\begin{align*}
(f \otimes g)(\alpha_0 u_1^{NX_1} \alpha_1 \cdots u_\ell^{NX_\ell} \alpha_\ell) &= f(\alpha_0 u_1^{NX_1} \alpha_1 \cdots u_\ell^{NX_\ell} \alpha_\ell)g(\varepsilon) \\
&\quad + \sum_{j=0}^{\ell} \sum_{i=0}^{|\alpha_j|-1} f(\alpha_0 u_1^{NX_1} \alpha_1 \cdots u_j^{NX_j} (\alpha_j[1:i])) \\
&\quad \times g((\alpha_j[i+1:\alpha_j])) u_{j+1}^{NX_{j+1}} \cdots \alpha_\ell \\
&\quad + \sum_{j=1}^{\ell} \sum_{i=0}^{|u_j^N|-1} \sum_{Y=0}^{X_j-1} f(\alpha_0 u_1^{NX_1} \alpha_1 \cdots u_j^{NY} (u_j^N[1:i])) \times \\
&\quad g((u_j^N[i+1:\alpha_j])) u_j^{N(X_j-Y-1)} \cdots \alpha_\ell
\end{align*}
$$

From the hypothesis on $f$, we deduce that the first term of this sum is ultimately $N_1$-polynomial, 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, \dots, \hat{X}_j, \dots, X_\ell)$ denotes the tuple obtained by removing the $j$-th element from $(X_1, \dots, X_\ell)$:

$$f(\alpha_0 u_1^{NX_1} \alpha_1 \cdots u_j^{NY} (u_j^N[1:i])) = P_{j,i}(Y, X_1, \dots, \hat{X}_j, \dots, X_\ell)$$
$$g((u_j^N[i+1:\ell|u_j^N|]) u_j^{N(X_j-Y-1)} \cdots \alpha_\ell) = Q_{j,i}(Y, X_1, \dots, \hat{X}_j, \dots, X_\ell)$$

As a consequence, we can rewrite the third term as a Cauchy product of polynomials for large enough values of $X_1, \dots, X_\ell$:

$$\sum_{j=1}^{\ell} \sum_{i=0}^{|u_j^N|-1} \sum_{Y=0}^{X_j-1} f(\alpha_0 u_1^{NX_1} \alpha_1 \cdots u_j^{NY} (u_j^N[1:i])) g((u_j^N[i+1:\ell|u_j^N|]) u_j^{N(X_j-Y-1)} \cdots \alpha_\ell) \\
= \sum_{j=1}^{\ell} \sum_{i=0}^{|u_j^N|-1} \sum_{Y=0}^{X_j-1} P_{j,i}(Y, X_1, \dots, \hat{X}_j, \dots, X_\ell) Q_{j,i}(X_j - Y - 1, X_1, \dots, \hat{X}_j, \dots, X_\ell) \\
= \sum_{j=1}^{\ell} \sum_{i=0}^{|u_j^N|-1} P_{i,j} \otimes 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 \in \text{Leaves}(F)$, $\text{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 \in \text{Skel}(t)$ and $x \in \text{Skel}(t')$, then $\text{Skel}(t) \subseteq \text{Skel}(t')$ or the converse holds.

As $\text{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 $\text{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' \in \text{Skel}(t)$, we have $\text{Skel}(t') \subseteq \text{Skel}(t)$.

### B. Proof of Claim III.18

Let $x \in \text{Leaves}(F)$, we show that the number of $x'$ such that $x'$ depends-on $x$ is bounded (independently from $x$ and $F \in \mathcal{F}_d^\mu$). Observe that $\text{skel-root}(x')$ is either an ancestor or the sibling of an ancestor of $\text{skel-root}(x)$. Observe that for all $t \in \text{Nodes}(F)$, $\text{Skel}(t)$ is a binary tree of height at most $d$, thus is has at most $2^d$ leaves. Moreover, $\text{skel-root}(x)$ has at most $d$ ancestors and $2d$ immediate siblings of its ancestors. As a consequence, there are at most $3d \times 2^d$ leaves that depend on $x$.

### C. Proof of Lemma III.19

Let $d \ge 0$, $M$ be a finite monoid, $\mu: A^* \to M$, $k \ge 1$, and $\psi \in \text{INV}_k$. We want to build a function $g \in \mathbb{Z}\text{Poly}_{k-1}$ such that for every $F \in \mathcal{F}_d^\mu$, $g(F) = \#(\psi(\tilde{x}) \wedge \text{sym-dep}(\tilde{x}))(F)$ (since $\mathcal{F}_d^\mu$ is a regular language of $\hat{A}^*$, it does not matter how $g$ is defined on inputs $F \notin \mathcal{F}_d^\mu$).
First, we use the lexicographic order to find the first pair $(x_i, x_j)$ that is dependent in the tuple $\vec{x}$. This allows to partition our set of valuations as follows:

$$
\begin{align*}
& \{\vec{x} \in \text{Leaves}(F) : F, \vec{x} \models \psi \wedge \text{sym-dep}(\vec{x})\} \\
&= \bigcup_{1 \le i < j \le n} \{\vec{x} \in \text{Leaves}(F) : F, \vec{x} \models \psi \wedge \text{sym-dep}(x_i, x_j) \wedge \bigwedge_{(k, \ell) <_{\text{lex}} (i, j)} \neg \text{sym-dep}(x_k, x_\ell)\} \\
&= \bigcup_{1 \le i < j \le n} \{\vec{x} \in \text{Leaves}(F) : F, \vec{x} \models \psi \wedge x_j \text{ depends-on } x_i \wedge \bigwedge_{(k, \ell) <_{\text{lex}} (i, j)} \neg \text{sym-dep}(x_k, x_\ell)\} \\
& \phantom{=} \quad \underbrace{\phantom{\bigcup_{1 \le i < j \le n} \{\vec{x} \in \text{Leaves}(F) : F, \vec{x} \models \psi \wedge x_j \text{ depends-on } x_i \wedge \bigwedge_{(k, \ell) <_{\text{lex}} (i, j)} \neg \text{sym-dep}(x_k, x_\ell)\}}_{:= \psi_{i \to j}(\vec{x})} \\
& \phantom{=} \quad \underbrace{\phantom{\bigcup_{1 \le i < j \le n} \{\vec{x} \in \text{Leaves}(F) : F, \vec{x} \models \psi \wedge x_i \text{ depends-on } x_j \wedge \bigwedge_{(k, \ell) <_{\text{lex}} (i, j)} \neg \text{sym-dep}(x_k, x_\ell)\}}_{:= \psi_{i \leftarrow j}(\vec{x})}
\end{align*}
$$

As a consequence, $\#(\psi \wedge \text{sym-dep}) = \sum_{1 \le i < j \le n} \#\psi_{i \to j} + \#\psi_{i \leftarrow j} - \#\psi_{i \to j} \wedge \psi_{i \leftarrow 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 $\exists^{=\ell} x_j.\psi$ to denote the fact that there exists exactly $\ell$ different values for $x$ so that $\psi(\dots, x_j, \dots)$ holds (this quantifier is expressible in MSO at every fixed $\ell$). 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:

$$
\begin{align*}
\#(\psi \wedge \text{sym-dep}) &= \sum_{1 \le i < j \le n} \#\psi_{i \to j} + \#\psi_{i \leftarrow j} - \#\psi_{i \to j} \wedge \psi_{i \leftarrow j} \\
&= \sum_{1 \le i < j \le n} \sum_{0 \le \ell \le N_d} \ell \cdot \#\exists^{=\ell} x_j.\psi_{i \to j} \\
&\quad + \sum_{1 \le i < j \le n} \sum_{0 \le \ell \le N_d} \ell \cdot \#\exists^{=\ell} x_i.\psi_{i \leftarrow j} \\
&\quad - \sum_{1 \le i < j \le n} \sum_{0 \le \ell \le N_d} \ell \cdot \#\exists^{=\ell} x_i.\psi_{i \to j} \wedge \psi_{i \leftarrow j}
\end{align*}
$$

D. *Proof of Lemma III.23*

In order to prove Lemma III.23, we consider $f$ such that $f_{\text{indep}} \neq 0$. Our goal is to construct a pumping family to exhibit a growth rate of $f_{\text{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 $\text{start}(t) := \min\{y \in \text{Leaves}(F) \cap \text{Skel}(t)\}$ and $\text{end}(t) := \max\{y \in \text{Leaves}(F) \cap \text{Skel}(t)\}$.

**Claim D.1.** Let $x_1, \dots, x_k$ be an independent tuple of $k \ge 1$ leaves in a forest $F \in \mathcal{F}_d^\mu$ factorizing a word $w$. Let $\vec{t}$ be the vector of nodes such that $t_i := \text{skel-root}(x_i)$ for all $1 \le i \le k$. One can order the $t_i$ according to their position in the word $w$ so that $1 < \text{start}(t_1) \le \text{end}(t_1) < \dots < \text{start}(t_k) \le \text{start}(t_k) < |w|$.

*Proof.* Assume by contradiction that there exists a pair $i < j$ such that $\text{start}(t_j) \ge \text{end}(t_i)$. We then know that $\text{start}(t_i) \le \text{start}(t_j) \le \text{end}(t_i)$. In particular, $\text{skel-root}(\text{start}(t_i)) = t_i$ is an ancestor of $\text{start}(t_j)$, hence $t_i$ is an ancestor of $t_j$. This contradicts the independence of $\vec{x}$.

Assume by contradiction that there exists $i$ such that $\text{start}(t_i) = 1$ (resp. $\text{end}(t_i) = |w|$). Then $\text{skel-root}(x_i)$ must be the root of $F$, but then $\vec{x}$ cannot be an independent tuple. $\square$

Given an independent tuple $x_1, \dots, x_k \in \text{Leaves}(F)$, with $\text{skel-root}(\vec{x}) = \vec{t}$, ordered by their position in the word, let us define $m_0 := \mu(w[1:\text{start}(t_1)-1])$, $m_k := \mu(w[\text{end}(t_k)+1:w|_w])$ and $m_i := \mu(w[\text{end}(t_k)+1:\text{start}(t_{i+1})-1])$ for $1 \le i \le k-1$.

**Definition D.2** (Type of a tuple of skel-root). Let $F \in \mathcal{F}_d^\mu$ factorizing a word $w$, $\vec{x}$ be an independent tuple of leaves in $F$, and $\vec{t} = \text{skel-root}(\vec{x})$. Without loss of generality assume that the nodes are ordered by start. The type s-type($\vec{t}$) in the forest $F$ is defined as the tuple $(m_0, \text{Skel}(t_1), \dots, m_{k-1}, \text{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 $\text{Types}_{d,k}$. Moreover, given a type $T \in \text{Types}_{d,k}$, one can build the MSO formula has-s-type$_T(\vec{t})$ over $\mathcal{F}_d^\mu$ that tests whether a tuple of nodes $\vec{t}$ is of type $T$, and can be obtained as skel-root($\vec{x}$) for some tuple $\vec{x}$ of independent leaves. The key property of types is that counting types is enough to count independent valuations for a formula $\psi \in \text{INV}$.

**Claim D.3.** Let $k \ge 1$, $d \ge 0$, $M$ be a finite monoid, $\mu: A^* \to M$ be a morphism. Let $T \in \text{Types}_{d,k}$, $F \in \mathcal{F}_d^\mu$, $\vec{x}$ and $\vec{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 $\sigma: L_1 \to L_2$, where $L_1 := \text{Leaves}(F) \cap \bigcup_{i=1}^k \text{Skel}(\text{skel-root}(x_i))$ and $L_2 := \text{Leaves}(F) \cap \bigcup_{i=1}^k \text{Skel}(\text{skel-root}(y_i))$, such that for every $z \in L_1^k$, for every formula $\psi \in \text{INV}_k$, $F \models \psi(z)$ if and only if $F \models \psi(\sigma(z))$.

*Proof Sketch.* Because of the type equality, we know that $\text{Skel}(\text{skel-root}(x_i))$ and $\text{Skel}(\text{skel-root}(y_i))$ are isomorphic for $1 \le i \le k$. As the skeletons are disjoint in an independent tuple, this automatically provides the desired bijection $\sigma$.

Let us now prove that $\sigma$ 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$_m(x)$. For isleaf, the result is the consequence of the fact that $\sigma$ 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) \in L_1^2$. By definition of $L_1$, there exists $1 \le i, j \le k$ such that $y \in \text{Leaves}(F) \cap \text{Skel}(\text{skel-root}(x_i))$ and $z \in \text{Leaves}(F) \cap \text{Skel}(\text{skel-root}(x_j))$. To simplify the argument, let us assume that $y < z$ and $i + 1 = j$. Let $w := \text{forest}(F)$, and $m_{y,z} := \mu(w[y:z])$. One can decompose the computation of $m_{y,z}$ as follows:

$$ 
\begin{align*}
m_{y,z} &= \mu(w[y:z]) \\
&= \mu(w[y:\text{end}(x_i)]w[\text{end}(x_i) + 1:\text{start}(x_{i+1}) - 1]w[\text{start}(x_{i+1}):z]) \\
&= \mu(w[y:\text{end}(x_i)])m_i\mu(w[\text{start}(x_i):z])
\end{align*}
$$

Therefore, $\mu(w[y:z])$ only depends on $\text{Skel}(\text{skel-root}(y)) = \text{Skel}(\text{skel-root}(x_i))$, the position of $y$ in $\text{Skel}(\text{skel-root}(y))$, $\text{Skel}(\text{skel-root}(z)) = \text{Skel}(\text{skel-root}(x_{i+1}))$, the position of $z$ in $\text{Skel}(\text{skel-root}(z))$, and $m_i$, all of which are preserved by the bijection $\sigma$. Hence, $\mu(w[y:z]) = \mu(w[\sigma(y):\sigma(z)])$. Therefore, $F \models \text{between}_m(y, z)$ if and only if $F \models \text{between}_m(\sigma(y), \sigma(z))$.

It is an easy check that a similar argument works when $j \ne i + 1$. $\square$

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 \ge 1$, $d \ge 0$, $M$ be a finite monoid, $\mu: A^* \to M$ be a morphism. For every $\psi \in \text{INV}_k$, there exists computable coefficients $\lambda_T \ge 0$, such that the following functions from $\mathcal{F}_d^\mu$ to $\mathbb{N}$ are equal:

$$ \#\psi_{\text{indep}} := \#(\psi \wedge \neg\text{sym-dep}) = \sum_{T \in \text{Types}_{d,k}} \lambda_T \cdot \#\text{has-s-type}_T $$
*Proof.* Using the claim, we can now proceed to prove Lemma D.4.

$$
\begin{align*}
\#\psi \wedge \neg \text{sym-dep}(F) &= \sum_{\vec{x} \text{ indep}} \mathbf{1}_{F|=\psi(\vec{x})} \\
&= \sum_{T \in \text{Types}_{d,k}} \sum_{\vec{t} \in \text{Nodes}(F)} \sum_{\vec{x} \text{ indep}} \mathbf{1}_{F|=\psi(\vec{x})} \mathbf{1}_{\vec{t}=\text{skel-root}(\vec{x})} \mathbf{1}_{\text{has-s-type}_T(\vec{t})} \\
&= \sum_{T \in \text{Types}_{d,k}} \sum_{\vec{t} \in \text{Nodes}(F)} \mathbf{1}_{\text{has-s-type}_T(\vec{t})} \left( \sum_{\vec{x} \text{ indep}} \mathbf{1}_{F|=\psi(\vec{x})} \mathbf{1}_{\vec{t}=\text{skel-root}(\vec{x})} \right) \\
&= \sum_{T \in \text{Types}_{d,k}} \sum_{\vec{t} \in \text{Nodes}(F)} \mathbf{1}_{\text{has-s-type}_T(\vec{t})} \lambda_T \\
&= \sum_{T \in \text{Types}_{d,k}} \lambda_T \#(\text{has-s-type}_T(\vec{t}))
\end{align*}
$$

The coefficient $\lambda_T$ does not depend on the specific $\vec{t}$ such that $\text{s-type}(\vec{t}) = T$ thanks to Claim D.3 and the fact that $\psi \in \text{INV}$. $\square$

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 \ge 1$, $d \ge 0$, a finite monoid $M$, and a morphism $\mu: A^* \to M$, $\{\#\text{has-s-type}_T : T \in \text{Types}_{d,k}\}$ is a $\mathbb{Z}$-linearly independent family of functions from $F_d^\mu$ to $\mathbb{Z}$.

**Lemma D.5 (Pumping Lemma).** For all $T \in \text{Types}_{d,k}$, there exists a pumping family $(w^{\vec{X}}, F^{\vec{X}})$ such that for every type $T' \in \text{Types}_{d,k}$, $\#(\text{has-s-type}_{T'})(F^{\vec{X}})$ is ultimately a $\mathbb{Z}$-polynomial in $\vec{X}$ that has non-zero coefficient for $X_1 \cdots X_n$ if and only if $T = T'$.

*Proof.* Let $T \in \text{Types}_{d,k}$ be a type, it is obtained as the type of some tuple $\vec{x}$ of independent leaves in some $F \in F_d^\mu$ factorizing a word $w$. Let $t_i := \text{skel-root}(x_i)$ and $S_i := \text{Skel}(t_i)$ for $1 \le i \le k$. Recall that $\mu(\text{word}(S_i)) = \mu(\text{word}(t_i))$ thanks to Claim III.13. As a consequence, $S_i$ is a subforest of $t_i$ that provides a valid $\mu$-forest of a subword of $\text{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, $\mu(\text{word}(S_i)) = \mu(\text{word}(t_i))$ is an idempotent. Therefore, for ever $X_i \in \mathbb{N}$, the tree obtained by replacing $t_i$ with $X_i$ copies of $S_i$ in $F$ is a valid $\mu$-forest. We write $F^{\vec{X}}$ for the forest $F$ where $t_i$ is replaced by $X_i$ copies of $S_i$. This is possible because the tuple $\vec{x}$ is composed of independent leaves, hence $t_i$ and $t_j$ are disjoint subtrees of $F$ whenever $1 \le i \ne j \le k$.

Hence, $F^{\vec{X}}$ is the factorization forest of the word $w^{\vec{X}} := \alpha_0(w_1)^{X_1} \alpha_1 \cdots \alpha_{k-1}(w_k)^{X_k} \alpha_k$ where $w_i = \text{word}(S_i)$, $\alpha_i = w[\text{end}(t_i)+1:\text{start}(t_i)-1]$ for $2 \le i \le k-1$, $\alpha_0 = w[1:\text{start}(t_1)-1]$, and $\alpha_k = w[\text{end}(t_k)+1:\vert w \vert]$ are non-empty factors of $w$.

We now have to understand the behavior of $\text{has-s-type}_{T'}$ over $F^{\vec{X}}$, for every $T' \in \text{Types}_{d,k}$. To that end, let us consider $T' \in \text{Types}_{d,k}$. Let us write $E$ for the set of nodes in $F^{\vec{X}}$ that are not appearing in any of the $X_i$ repetitions of $S_i$, for $1 \le i \le k$. The set $E$ has a size bounded independently of $X_1, \dots, X_k$. To a tuple $\vec{s}$ such that $F^{\vec{X}} \models \text{has-s-type}_{T'}(\vec{s})$, one can associate the mapping $\rho_{\vec{s}}: \{1, \dots, k\} \to \{1, \dots, k\} \uplus E$, so that $\rho_{\vec{s}}(i) = \vec{s}_i$ when $\vec{s}_i \in E$, and $\rho_{\vec{s}}(i) = j$ when $\vec{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 $\text{s-type}(\vec{s}) = T'$, and $\rho_{\vec{s}}(i) = j$, then $\vec{s}_i$ must be the root of one of the $X_j$ copies of $S_j$ in $F^{\vec{X}}$. Indeed, $\vec{t}$ is obtained as $\text{skel-root}(\vec{y})$ for some independent tuple $\vec{y}$ of leaves. Hence, $\vec{s}_i = \text{skel-root}(y_i)$ which belong to some copy of $S_j$, hence $\vec{s}_i$ must be the root of this copy of $S_j$, because $S_j$ is a binary tree.
Given a map $\rho: \{1, \dots, k\} \to \{1, \dots, k\} \cup E$ and a tuple $\vec{X} \in \mathbb{N}^k$, we let $C_\rho(\vec{X})$ be the set of tuples $\vec{s}$ of nodes of $F^{\vec{X}}$ such that s-type($\vec{s}$) = $T'$, and such that $\rho_{\vec{s}} = \rho$. This allows us to rewrite the number of such vectors as a finite sum:

$$ \#(\text{has-s-type}_{T'}(\vec{t}))(F^{\vec{X}}) = \sum_{\rho: \{1, \dots, k\} \to \{1, \dots, k\} \cup E} \#C_{\rho}(\vec{X}) $$

**Claim D.7.** For every $\rho: \{1, \dots, k\} \to \{1, \dots, k\} \cup E$, $\#C_\rho(\vec{X})$ is ultimately a $\mathbb{Z}$-polynomial in $\vec{X}$. Moreover, its coefficient for $X_1 \cdots X_k$ is non-zero if and only if $\rho(i) = i$ for $1 \le i \le k$.

*Proof.* Assume that $C_\rho(\vec{X})$ is non-empty. Then choosing a vector $\vec{s} \in C_\rho(\vec{X})$ is done by fixing the image of $s_i$ to $\rho(i)$ when $\rho(i) \in E$, and selecting $p_j := |\rho^{-1}(\{j\})|$ non consecutive copies of $S_j$ 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 $\vec{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 $\binom{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_\rho(\vec{X})$ is ultimately a product of $\binom{X_j-p_j+1}{p_j}$ for the non-zero $p_j$, which is a $\mathbb{Z}$-polynomial in $X_1, \dots, X_k$. Moreover, it has a non-zero coefficient for $X_1 \dots X_k$ if and only if $p_j \neq 0$ for $1 \le j \le k$, which is precisely when $\rho(i) = i$. $\square$

We have proven that $\#(\text{has-s-type}_{T'})(F^{\vec{X}})$ is a $\mathbb{Z}$-polynomial in $X_1, \dots, X_k$, and that the only term possibly having a non-zero coefficient for $X_1 \cdots X_k$ is $\#C_{\text{id}}(\vec{X})$. Notice that if $\#C_{\text{id}}(\vec{X})$ is non-zero, we immediately conclude that $T = T'$. $\square$

**Claim D.8.** Let $P \in \mathbb{R}[X_1, \dots, X_n]$ which evaluates to 0 over $\mathbb{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|_{\mathbb{N}} = 0$, then $P$ has infinitely many roots and $P = 0$. Now, let $P$ having $n+1$ variables, and such that $P(x_1, \dots, x_n, x_{n+1}) = 0$ for all $(x_1, \dots, x_{n+1}) \in \mathbb{N}^{n+1}$. By induction hypothesis, $P(X_1, \dots, X_n, x_{n+1}) = 0$ for all $x_{n+1} \in \mathbb{N}$. Hence for all $x_1, \dots, x_n \in \mathbb{R}$, $P(x_1, \dots, x_n, X_{n+1})$ is a polynomial with one free variable having infinitely many roots, hence $P(x_1, \dots, x_n, x_{n+1}) = 0$ for every $x_{n+1} \in \mathbb{R}$. We have proven that $P = 0$. $\square$

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 \ge 1$, and $f_{\text{indep}}$ be a linear combination of $\#\psi_i \wedge \neg \text{sym-dep}$, where $\psi_i \in \text{INV}_k$. Assume moreover that $f_{\text{indep}} \neq 0$. Thanks to Lemma D.4, every $\#\psi_i \wedge \neg \text{sym-dep}$ can be written as a linear combination of $\#\text{has-s-type}_T(\vec{t})$, hence $f_{\text{indep}} = \sum_{T \in \text{Types}_{d,k}} \lambda_T \#\text{has-s-type}_T$, and the coefficients $\lambda_T$ (now in $\mathbb{Z}$) are computable.

Since $f_{\text{indep}} \neq 0$, there exists $T \in \text{Types}_{d,k}$ such that $\lambda_T \neq 0$. Using Lemma D.5, there exists a pumping family $(w^{\vec{X}}, F^{\vec{X}})$ adapted to $T$. In particular, $f(F^{\vec{X}})$ is ultimately a $\mathbb{Z}$-polynomial in $\vec{X}$, and its coefficient in $X_1 \cdots X_k$ is the sum of the coefficients in $X_1 \cdots X_k$ of the polynomials $\#\text{has-s-type}_{T'}(F^{\vec{X}})$ multiplied by $\lambda_{T'}$. This coefficient is non-zero if and only if $T = T'$. Hence, $f(F^{\vec{X}})$ is ultimately a $\mathbb{Z}$-polynomial with a non-zero coefficient for $X_1 \cdots X_k$.

As a side result, we have proven that a linear combination of $\#\text{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 $\text{Types}_{d,k}$. For the converse implication, one leverages Claim D.8: if one coefficient is non-zero, then the polynomial $f(F^{\vec{X}})$ must be non-zero.

### E. Proof of Lemma III.24

Let $P, Q \in \mathbb{R}[X_1, \dots, X_n]$ be such that $|P| = O(|Q|)$. We show that $\deg(P) \le \deg(Q)$.

If $P = 0$, then $\deg(P) \le \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 \ge 0$ and $C \ge 0$ such that $|P(x_1, \dots, x_n)| \le C|Q(x_1, \dots, x_n)|$ for all $x_1, \dots, x_n \in \mathbb{N}$ such that $x_1, \dots, x_n \ge N$.
Because $P_1$ is a non-zero polynomial, there exists a tuple $(x_1, \dots, x_n) \in \mathbb{N} \setminus \{0\}$ such that $\alpha := P_1(x_1, \dots, x_n) \neq 0$ (Claim D.8). Let us now consider $R(Y) := P(Yx_1, \dots, Yx_n) \in \mathbb{R}[Y]$, and $S(Y) := Q(Yx_1, \dots, Yx_n) \in \mathbb{R}[Y]$. Notice that $R(Y)$ has degree exactly $\deg(P)$ and its term of degree $\deg(P)$ is $\alpha Y^{\deg(P)}$. Furthermore, $S(Y)$ is a polynomial in $Y$ of degree at most $\deg(Q)$, with dominant coefficient $\beta \neq 0$. We know that for $Y$ large enough, $|R(Y)| \leq C|S(Y)|$. Since $|R(Y)| \sim_{+\infty} |\alpha|Y^{\deg(P)}$, and $|S(Y)| \sim_{+\infty} |\beta|Y^{\deg(S)} \leq |\beta|Y^{\deg(Q)}$, we conclude that $\deg(P) \leq \deg(Q)$.

# APPENDIX E
## PROOFS OF SECTION IV

### A. Proof of Claim IV.4

Let $k \geq 0$, $f \in \mathbb{Z}\text{Poly}_k$ and $u \in A^*$. We want to show that $u \triangleright f \in \mathbb{Z}\text{Poly}_k$. Notice that for every $u$, the map $u \Box: w \mapsto uw$ is regular, hence $u \triangleright f = f \circ (u \Box)$ belongs to $\mathbb{Z}\text{Poly}_k$ thanks to Proposition II.12.

### B. Proof of Claim IV.7

The fact that $\sim_k$ is an equivalence relation is obvious from the properties of $\mathbb{Z}\text{Poly}$. Furthermore if $f \sim_k g$, then $f-g \in \mathbb{Z}\text{Poly}_k$, thus $u \triangleright (f-g) = u \triangleright f - u \triangleright g \in \mathbb{Z}\text{Poly}_k$ by Claim IV.4. Furthermore it is obvious that $\delta \cdot f \sim_k \delta \cdot g$, and if $f' \sim_k g'$ then $f+f' \sim_k g+g'$.

It remains to show that $u \triangleright (\mathbf{1}_L \otimes f) \sim_k (u \triangleright \mathbf{1}_L) \otimes f$ for $L \subseteq A^*$ and for this we proceed by induction on $|u|$. By expanding the definitions we note that $a \triangleright (\mathbf{1}_L \otimes g) = (a \triangleright \mathbf{1}_L) \otimes g + \mathbf{1}_L(\varepsilon) \times (a \triangleright g)$ for all $a \in A$. By Claim IV.4 we get $a \triangleright g \in \mathbb{Z}\text{Poly}_k$, hence $a \triangleright (\mathbf{1}_L \otimes g) \sim_k (a \triangleright \mathbf{1}_L) \otimes g$. The result follows since $a \triangleright \mathbf{1}_L = \mathbf{1}_{a^{-1}L}$ and by Theorem II.20.

### C. Proof of Lemma IV.8

We first note that $u \triangleright (\delta f + \eta g) = \delta(u \triangleright f) + \eta(u \triangleright g)$, for all $f,g: A^* \to \mathbb{Z}$, $\delta, \eta \in \mathbb{Z}$ and $u \in A^*$. Hence it suffices to show that Lemma IV.8 holds on a set $S$ of functions such that $\text{Span}_{\mathbb{Z}}(S) = \mathbb{Z}\text{Poly}_k$. For $k=0$, we can chose $S := \{\mathbf{1}_L : L \text{ regular}\}$. As observed above, we have $u \triangleright \mathbf{1}_L = \mathbf{1}_{u^{-1}L}$ and the result holds since regular languages have finitely many residual languages. For $k \geq 1$, we can choose $S := \{\mathbf{1}_L \otimes g : g \in \mathbb{Z}\text{Poly}_{k-1}, L \text{ regular}\}$ by Proposition II.18. Let $\mathbf{1}_L \otimes g \in S$. Then by Claim IV.7 we get $u \triangleright (\mathbf{1}_L \otimes g) \sim_{k-1} (u \triangleright \mathbf{1}_L) \otimes g = \mathbf{1}_{u^{-1}L} \otimes g$. Since a regular language has finitely many residual languages, there are finitely many $\sim_{k-1}$-equivalence classes for the (function) residuals of $\mathbf{1}_L \otimes g$.

### D. Proof of Lemma IV.17

Let $f: A^* \to \mathbb{Z}$ be a function such that $\text{Res}(f)/ \sim_{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 $\text{Res}(f)/ \sim_{k-1}$, but directly by some elements of $\text{Res}(f)$. Remark that the labels on the transitions are of the form $w \triangleright f - v \triangleright f$ when $w \triangleright f \sim_{k-1} v \triangleright f$, hence are in $\text{Span}_{\mathbb{Z}}(\text{Res}(f)) \cap \mathbb{Z}\text{Poly}_{k-1}$ by definition of $\sim_{k-1}$ (observe that the construction of these labels is effective and that equivalence of residuals is decidable if we start from $f \in \mathbb{Z}\text{Poly}_k$). Now, let us justify the correctness and termination of Algorithm 1.

First, we note that it maintains two sets $O$ and $Q$ such that $O \uplus Q \subseteq \text{Res}(f)$ and for all $f,g \in O \uplus Q$ we have $f \neq g \Rightarrow f \not\sim_{k-1} g$. Hence the algorithm terminates since $\text{Res}(f)/ \sim_{k-1}$ is finite and $Q$ increases at every loop. At the end of its execution, we have for all $q \in Q$ and $a \in A$, that $\delta(q,a) \sim_{k-1} a \triangleright q$ and $\lambda(q,a) = a \triangleright q - \delta(q,a)$.

Let us show by induction on $n \geq 0$ that for all $a_1 \cdots a_n \in A^*$, if $q_0 \to^{a_1} q_1 \to^{a_2} \cdots \to^{a_n} q_n$ is the run labelled by $a_1 \cdots a_n$ in the underlying automaton, and $g_1 \cdots g_n$ are the functions which label the transitions, we have $q_n \sim_{k-1} a_1 \cdots a_n \triangleright f$ and for all $w \in A^*$, $f(a_1 \cdots a_n w) = \sum_{i=2}^n g_i(a_i \cdots a_n w) + q_n(w)$. For $n=0$ the result is obvious because $q_0 = f$. Now, assume that the result holds for some $n \geq 0$ and let $a_1 \cdots a_n a_{n+1} \in A^*$. Let $q_0 \to^{a_1} q_1 \to^{a_2} \cdots \to^{a_{n+1}} q_{n+1}$ be the run and $g_1 \cdots g_{n+1}$ be the labels of the transitions. Since $q_n \sim_{k-1} a_1 \cdots a_n \triangleright f$ (by induction) we get $a_{n+1} \triangleright q_n \sim_{k-1} a_1 \cdots a_n a_{n+1} \triangleright f$ by Claim IV.7. Because $q_{n+1} = \delta(q_n, a_{n+1}) \sim_{k-1} a_{n+1} \triangleright q_n$, then $q_{n+1} \sim_{k-1} a_1 \cdots a_n a_{n+1} \triangleright f$. Now, let us fix $w \in A^*$. We have $f(a_1 \cdots a_n a_{n+1} w) = \sum_{i=2}^n g_i(a_i \cdots a_n a_{n+1} u) + q_n(a_{n+1} w)$ by induction
hypothesis. But since $g_{n+1} = \lambda(q_n, a_{n+1}) = a_{n+1} \triangleright q_n - \delta(q_n, a_{n+1}) = a_{n+1} \triangleright 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 = \varepsilon$ and the definition of $F$.

### E. Proof of Corollary IV.19

Lemma IV.17 shows that any function from $\mathbb{Z}\text{Poly}_k$ is computed by its $k$-residual transducer (which is in particular a $\mathbb{Z}\text{Poly}_{k-1}$-transducer). Conversely, given a $\mathbb{Z}\text{Poly}_{k-1}$-transducer computing $f$, it is easy to write $f$ as a linear combination of elements of the form $\mathbf{1}_L \otimes g$ (see e.g. Section F-B), where $g$ is the label of a transition, thus $f \in \mathbb{Z}\text{Poly}_{k-1}$.

### F. Proof of Corollary IV.20

Every map in $\mathbb{Z}\text{Poly}_k$ has finitely many residuals up to $\sim_{k-1}$ thanks to Lemma IV.8. We now prove the converse implication. Let $f$ such that $\text{Res}(f)/\sim_{k-1}$ is finite. By Lemma IV.17 there exists a $k$-residual transducer of $f$ (which is in particular a $\mathbb{Z}\text{Poly}_{k-1}$-transducer). Thanks to Corollary IV.19, it follows that $f \in \mathbb{Z}\text{Poly}_k$.

# APPENDIX F

## PROOFS OF SECTION V

### A. Proof of Claim V.6

Let $L$ be a regular language such that $\mathbf{1}_L$ is ultimately 1-polynomial. Then, for every $u, w, v \in A^*$, there exists a polynomial $P \in \mathbb{Q}[X]$, such that $\mathbf{1}_L(uw^Xv) = P(X)$ for $X$ large enough. This implies that $P$ is a constant polynomial, and in particular $\mathbf{1}_L(uw^{X+1}v) = \mathbf{1}_L(uw^Xv)$ for $X$ large enough. As a consequence, the syntactic monoid of $L$ is aperiodic, thus $L$ is star-free [5]. Conversely, assume that $L$ is star-free. It is recognized by a morphism $\mu$ into an aperiodic finite monoid $M$. Because $M$ is aperiodic, for every $x \in M$, $x^{|M|+1} = x^{|M|}$. Hence, for all $\alpha_0, w_1, \alpha_1, \dots, w_\ell, \alpha_\ell \in A^*$, $\mathbf{1}_L(\alpha_0 w_1^{X_1} \alpha_1 \cdots w_\ell^{X_\ell} \alpha_\ell)$ is constant for $X_1, \dots, X_\ell \ge |M|$ since it only depends on the image $\mu(\alpha_0 w_1^{X_1} \alpha_1 \cdots w_\ell^{X_\ell} \alpha_\ell)$.

### B. Proof of Lemma V.14

Let $\mathcal{T} = (A, Q, q_0, \delta, \lambda)$ be a counter-free $\mathbb{Z}\text{SF}_{k-1}$-transducer computing a function $f: A^* \to \mathbb{Z}$. Since the deterministic automaton $(A, Q, q_0, \delta)$ is counter-free, then by [4] for all $q \in Q$ the language $L_q := \{u : \delta(q_0, u) = q\}$ is star-free. So is $L_q a$ for all $a \in A$. Now observe that:

$$f = \sum_{\substack{q \in Q \\ a \in A}} \mathbf{1}_{L_q a} \otimes \lambda(q, a).$$

We conclude thanks to Equation (3).

### C. Proof of Lemma V.16

Let $k \ge 0$. Let $f \in \mathbb{Z}\text{Poly}_k$ which is ultimately 1-polynomial and $\mathcal{T} = (A, Q, q_0, \delta, \mathcal{H}, \lambda, F)$ be a $k$-residual transducer of $f$. Since ultimate 1-polynomiality is preserved under taking linear combinations and residuals, the function labels of $\mathcal{T}$ are ultimately 1-polynomial (by definition of a $k$-residual transducer). It remains to show that $\mathcal{T}$ is counter-free.

Let $\alpha, w \in A^*$ and suppose that $\delta(q_0, \alpha) = \delta(q_0, \alpha w^n)$ for some $n \ge 1$. We want to show that $\delta(q_0, \alpha w) = \delta(q_0, \alpha)$. Since $\delta(q_0, \alpha) = \delta(q_0, \alpha w^{nX})$ and $\delta(q_0, \alpha w) = \delta(q_0, \alpha \alpha w^{nX+1})$ for all $X \ge 1$, it is sufficient to show that we have $\delta(q_0, \alpha w^{nX+1}) = \delta(q_0, \alpha w^{nX})$ for some $X \ge 1$.

Let $M \ge 1$ given by Definition II.29 for the ultimate 1-polynomiality of $f$. We want to show that $(\alpha w^{nM+1} \triangleright f) \sim_{k-1} (\alpha w^{nM} \triangleright f)$, i.e. $|(\alpha w^{nM+1} \triangleright f)(w) - (\alpha w^{nM} \triangleright f)(w)| = \mathcal{O}(|w|^{k-1})$ since the residuals belong to $\mathbb{Z}\text{Poly}$. For this, let us pick any $\alpha_0, w_1, \alpha_1, \dots, w_k, \alpha_k \in A^*$. By Theorem III.3, it is sufficient to show that:

$$|(\alpha w^{nM} \triangleright f - \alpha w^{nM+1} \triangleright f)(\alpha_0 w_1^{X_1} \cdots w_k^{X_k} \alpha_k)| = \mathcal{O}((X_1 + \cdots + X_k)^{k-1})$$

Because $f$ is ultimately 1-polynomial, for all $X, X_1, \dots, X_k \ge M$, $f(\alpha w^X \alpha_0 w_1^{X_1} \cdots w_k^{X_k} \alpha_k)$ is a polynomial $P(X, X_1, \dots, X_k)$. Our goal is to show that $|P(nM, X_1, \dots, X_k) - P(nM + 1, X_1, \dots, X_k)| = \mathcal{O}(|X_1 + \cdots + X_k|^{k-1})$. Since $f \in \mathbb{Z}\text{Poly}_k$, we have $|P(X, X_1, \dots, X_k)| =$
$O(|X + X_1 + \cdots + X_k|^k)$. Thus by Lemma III.24, $P$ has degree at most $k$, hence it can be rewritten under the form $P_0 + XP_1 + \cdots + X^k P_k$ where $P_i(X_1, \ldots, X_k)$ has degree at most $k-i$. Therefore:

$$ 
\begin{aligned}
& |P(nM, X_1, \ldots, X_k) - P(nM + 1, X_1, \ldots, X_k)| \\
& = \left| \sum_{i=1}^{k} P_i(X_1, \ldots, X_k) ((nM)^i - (nM + 1)^i) \right| \\
& \le \sum_{i=1}^{k} |P_i(X_1, \ldots, X_k)| (nM + 1)^i
\end{aligned}
$$

since the term $P_0$ vanishes when doing the subtraction. The result follows since the polynomials $P_i$ for $1 \le i \le 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** $\mathbb{Z}$-polyregular function can be written under the form $\sum \circ g$ where $g: A^* \to \{\pm 1\}^*$ is **star-free** polyregular. This is a consequence of the following claims.

**Claim F.1.** For all $\varphi \in \mathbb{FO}$, there exists a **star-free** polyregular function $f: A^* \to \{\pm 1\}^*$ such that $\#\varphi = \sum \circ f$.

**Proof.** **Star-free** polyregular functions are characterized in [21, Theorem 7] as the functions computed by (multidimensional) FO-interpretations. Recall that an FO-interpretation of dimension $k \in \mathbb{N}$ is given by a FO formula $\varphi_{\le}(\vec{x}, \vec{y})$ defining a total ordering over $k$-tuples of positions, a FO formula $\varphi^{\text{Dom}}(\vec{x})$ that selects valid positions, and FO formulas $\varphi^a(\vec{x})$ that place the letters over the output word [21, Definition 1 and 2]. In our specific situation, letting $\varphi_{\le}$ 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 $\varphi^{\text{Dom}}$ be defined as $\varphi$ 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. $\square$

**Claim F.2.** The set $\{\sum \circ f: f: A^* \to \{\pm 1\}^* \text{ star-free polyregular}\}$ is closed under sums and external $\mathbb{Z}$-products.

**Proof.** Notice that $\sum \circ f + \sum \circ g = \sum \circ (f \cdot g)$ where $f \cdot g(w) := f(w) \cdot g(w)$. As **star-free** polyregular functions are closed under concatenation [7], the set of interest is closed under sums. To prove that it is closed under external $\mathbb{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 [7, Theorem 2.6]). $\square$

Let us consider a **star-free** polyregular function $g: A^* \to \{\pm 1\}^*$. The maps $g_+: w \mapsto |g(w)|_1$ and $g_-: w \mapsto |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 [7]). Hence $g_-$ and $g_+$ are star-free polyregular functions with unary output, a.k.a. **star-free** $\mathbb{N}$-polyregular functions. As a consequence, $\sum \circ g = g_+ - g_-$ lies in $\mathbb{Z}$SF.

### E. Proof of Proposition VI.2

Item 3 $\Rightarrow$ Item 2 is obvious. For Item 2 $\Rightarrow$ Item 1, it is sufficient to show that if $\varphi(X_1, \ldots, X_n)$ is an $\text{MSO}^X$ formula, then $\#\varphi$ is a $\mathbb{Z}$-polyregular function. We show the result for $n=1$, i.e. for a formula $\varphi(X)$. Let us define the language $L \subseteq (A \times \{0, 1\})^*$ such that $(w, v) \in L$ if and only if $w \models \varphi(S)$ where $S := \{1 \le i \le |w| : v[i] = 1\}$. Using the classical correspondence between $\text{MSO}$ logic and automata (see e.g. [18]), the language $L$ is regular, hence it is computed by a finite deterministic automaton $A$. Given a fixed $w \in A^*$, there exists a bijection between the accepting runs of $A$ whose first component is $w$ and the sets $S$ such that $w \models \varphi(S)$. Consider the (nondeterministic) $\mathbb{Z}$-weighted automaton $A'$ (this notion is equivalent to $\mathbb{Z}$-linear representations, see e.g. [13]) 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 \in A^*$, it is easy to see that $A'$ has exactly $\#\varphi(w)$ runs labelled by $w$ whose product of the output values is 1 (and the others have product 0). Thus $A$ computes $\#\varphi$. This proof scheme adapts naturally to the case where $n \ge 1$.

For Item 1 $\Rightarrow$ Item 3, let us consider a linear representation $(I, \mu, F)$ of a Z-rational series.

**Claim F.3.** *Without loss of generality, one can assume that $\mu(A^*) \subseteq \mathcal{M}^{n,n}(\{0,1\})$, at the cost of increasing the dimension of the matrices.*

*Proof Sketch.* Let $N := \min(1, \max\{|\mu(a)_{i,j}| : a \in A, 1 \le i, j \le n\})$, we define the new dimension of our system to be $m := n \times N \times 2$. As a notation, we assume that matrices in $\mathcal{M}^{m,m}$ have their rows and columns indexed by $\{1, \dots, n\} \times \{1, \dots, N\} \times \{\pm\}$. For all $a \in A$, let us define $\nu(a) \in \mathcal{M}^{m,m}$ as follows: for all $1 \le i, j \le n, 1 \le v, v' \le N$

$$ \nu(a)_{(i,v,+),(j,v',+)} = \begin{cases} 1 & \text{if } |\mu(a)_{i,j}| \ge v' \land 0 < \mu(a)_{i,j} \\ 0 & \text{otherwise} \end{cases} $$

$$ \nu(a)_{(i,v,+),(j,v',-)} = \begin{cases} 1 & \text{if } |\mu(a)_{i,j}| \ge v' \land 0 > \mu(a)_{i,j} \\ 0 & \text{otherwise} \end{cases} $$

$$ \nu(a)_{(i,v,-),(j,v',-)} = \begin{cases} 1 & \text{if } |\mu(a)_{i,j}| \ge v' \land 0 < \mu(a)_{i,j} \\ 0 & \text{otherwise} \end{cases} $$

$$ \nu(a)_{(i,v,-),(j,v',+)} = \begin{cases} 1 & \text{if } |\mu(a)_{i,j}| \ge v' \land 0 > \mu(a)_{i,j} \\ 0 & \text{otherwise} \end{cases} $$

Let us now adapt the final vector by defining for every $1 \le i \le n, 1 \le v \le 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 \le i \le 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', \nu, F')$ computes the same function as $(I, \mu, F)$. $\square$

As a consequence, $I\mu(w)F = \sum_{i,j} I_i\mu(w)_{i,j}F_j$, let us now rewrite this sum as a counting MSO formula with set free variables.

For all $1 \le i, j \le n$, one can write an MSO formula $\psi_{i,j}(x)$ such that for all $1 \le p \le |w|$, $w \models \psi_{i,j}(p)$ if and only if $\mu(w[p])_{i,j} = 1$. Furthermore, for all $1 \le i, j \le n$, one can write an MSO formula $\theta_{i,j}$ with variables $X_p^{\text{in}}, X_p^{\text{out}}$ for $1 \le p \le n$ such that a word $w$ satisfies $\theta_{i,j}$ whenever for every position $x$ of $w$ there exists a unique pair $1 \le p, q \le n$ such that $x \in X_p^{\text{in}}$ and $x \in X_q^{\text{out}}$, if $x \in X_p^{\text{out}}$ then $(x+1) \in X_p^{\text{in}}$, the first position of $w$ belongs to $X_i^{\text{in}}$ and $X_i^{\text{out}}$, and the last position of $w$ belongs to $X_j^{\text{in}}$ and $X_j^{\text{out}}$.

$$ \mu(w)_{i,j} = \sum_{s: \{1, \dots, k-1\} \to \{1, \dots, n\}} \mu(w[1])_{i,s(1)} \mu(w[|w|])_{s(k-1),j} \prod_{k=2}^{|w|-1} \mu(w[k])_{s(k),s(k+1)} \\ = \# \left( \bigwedge_{1 \le i,j \le n} (x \in X_i^{\text{in}} \land x \in X_j^{\text{out}}) \Rightarrow \psi_{i,j}(x) \right) (w) \\ \stackrel{:=\tau_{i,j}}{=} $$

We have proven that $I\mu(w)F$ is a Z-linear combination of the counting formulas $\tau_{i,j}$ via $I\mu(w)F = \sum_{i,j} I_i F_j \cdot \#\tau_{i,j}(w)$. Notice that all the formulas used never introduced set quantifiers, hence the formulas belong to FO and have MSO free variables.