*intro notioncolor=nicecyan, emphasize *notioncolor=darkblue *unknowncolor=nicered notion — skeleton — skeletons notion — skeleton monoid notion — skeleton-idempotent — idempotent — idempotency — skeleton idempotency notion — loop — loops notion — empty@loop notion — pump — pumped — pumping notion — flow-normalized notion — period — periods notion — cut — cuts — $C$-cut — $C$-cuts — first $C$-cut — $i$-th $C$-cut — $(i+1)$-th $C$-cut notion — set of $C$-cuts — set of cuts notion — weight — weights notion — delay — delays notion — lag — lags notion — root — roots — primitive root — primitive roots notion — word inequality — word inequalities — inequality — inequalities notion — system — systems — system of inequalities — systems of inequalities — system of word inequalities — systems of word inequalities notion — solution — solutions notion — satisfiable — satisfiability — satisfied notion — variable order notion — pointwise order notion — pointwise product — pointwise products notion — variant of pointwise order notion — variant of pointwise product notion — convolution — convolutions notion — length-preserving notion — automatic notion — rational relation — rational relations — rational notion — $k$-valued — $k$-valuedness — $2$-valued — valuedness — single-valued — single-valuedness — functional notion — finite-valued — Finite-valued — finite valuedness notion — copyless update — copyless updates — update — updates notion — initial@update — initial update notion — final@update — final update notion — deterministic — determinism — Deterministic notion — unambiguous — unambiguity notion — $k$-ambiguous — ambiguity — finitely ambiguous — finitely-ambiguous — finite ambiguity — Finite ambiguity notion — streaming string transducer — streaming string transducers — SST — SSTs notion — run — runs notion — input consumed by — inputs consumed by — consumed input — consumed inputs — input — inputs notion — update induced by — induced update notion — accepting notion — output produced by — outputs produced by — produced output — produced outputs — output — outputs notion — relation realized by — relations realized by — realized relation — realized relations — relation — relations notion — equivalent — equivalence — equivalences — equivalence problem — Equivalence notion — dumbbell from $q_{1}$ to $q_{2}$ — dumbbell — dumbbells notion — plain dumbbell from $q_{1}$ to $q_{2}$ — plain dumbbell — plain dumbbells notion — multiset finite state automaton — multiset finite state automata — multiset automaton — multiset automata notion — W-pattern — W-patterns notion — left run — left runs notion — mid run — mid runs notion — right run — right runs notion — W-run — W-runs notion — divergent — divergence notion — simply divergent — simple divergence notion — marked sequence — marked sequences notion — unmarked sequence notion — cover notion — reversible notion — size — sizes notion — separation

# Finite-valued Streaming String Transducers

Emmanuel Filiot (Université libre de Bruxelles, Brussels, Belgium)
Ismaël Jecker (Université de Besançon, Besançon, France)
Gabriele Puppis (University of Udine, Udine, Italy)
Christof Löding (RWTH Aachen University, Aachen, Germany)
Anca Muscholl (LaBRI, Université Bordeaux, Bordeaux, France)
Sarah Winter (IRIF, Université Paris Cité, Paris, France)

###### Abstract

A transducer is finite-valued if for some bound $k$, it maps any given input
to at most $k$ outputs. For classical, one-way transducers, it is known since
the 80s that finite valuedness entails decidability of the equivalence
problem. This decidability result is in contrast to the general case, which
makes finite-valued transducers very attractive. For classical transducers it
is also known that finite valuedness is decidable and that any $k$-valued
finite transducer can be decomposed as a union of $k$ single-valued finite
transducers.

In this paper, we extend the above results to copyless streaming string
transducers (SSTs), answering questions raised by Alur and Deshmukh in 2011.
SSTs strictly extend the expressiveness of one-way transducers via additional
variables that store partial outputs. We prove that any $k$-valued SST can be
effectively decomposed as a union of $k$ (single-valued) deterministic SSTs.
As a corollary, we obtain equivalence of SSTs and two-way transducers in the
finite-valued case (those two models are incomparable in general). Another
corollary is an elementary upper bound for checking equivalence of finite-
valued SSTs. The latter problem was already known to be decidable, but the
proof complexity was unknown (it relied on Ehrenfeucht’s conjecture). Finally,
our main result is that finite valuedness of SSTs is decidable. The complexity
is PSpace, and even PTime when the number of variables is fixed.

##  1 Introduction

Finite-state word transducers are simple devices that allow to reason about
data transformations in an effective, and even efficient way. In their most
basic form they transform words using finite control. Unlike automata, their
power heavily depends on various parameters, like non-determinism, the
capability of scanning the input several times, or the kind of storage they
may use. The oldest transducer model, known as generalized sequential machine,
extends finite automata by outputs. Inspired by an approach that applies to
arbitrary relational structures [13], logic-based transductions were
considered by Engelfriet and Hoogeboom [19] and shown to be ”equivalent” to
”functional” (a.k.a. ”single-valued”) _two-way transducers_. Ten years later
Alur and Cerný [2] proposed _”streaming string transducers”_ (”SST”), a one-
way model that uses write-only registers as additional storage. Registers can
be updated by appending or prepending strings, or concatenated, but not
duplicated (they are copyless). They showed that ”SSTs” are ”equivalent” to
the model studied by [19] in the ”functional” case. These ”equivalences”
support thus the notion of “regular” word functions, in the spirit of
classical results on regular word languages from automata theory and logics
due to Büchi, Elgot, Trakhtenbrot, Rabin, and others.

In the non-”functional” case the picture is less satisfactory, as
”equivalence” only holds between ”SSTs” and non-deterministic MSO
transductions [5], which extend the original MSO transductions by
existentially quantified monadic parameters. On the other hand, two-way
transducers and ”SSTs” become incomparable. Moreover, the ”equivalence
problem” for the non-deterministic models is undecidable, even for one-way
transducers [22, 28]. There is however a class of relations that is almost as
nice as (regular) word functions: this is the class of _”finite-valued”_
relations, namely, relations that associate a uniformly bounded number of
”outputs” with each ”input”.

######  Example 1.

Let $n\in\mathbb{N}$ and consider the relation

$R_{n}~{}=~{}\big{\\{}(\bar{v}_{1}\dots\bar{v}_{k},\bar{v}_{i})~{}|~{}k\in\mathbb{N},~{}1\leq
i\leq k,~{}\forall 1\leq j\leq k,~{}\bar{v}_{j}\in\\{0,1\\}^{n}\big{\\}}.$

E.g. $(001011,00),(001011,10),(001011,11)\in R_{2}$. For all $n$, the relation
$R_{n}$ is $2^{n}$-valued and realizable by a (one-way) finite transducer
$T_{n}$, which uses non-determinism to guess an index $i\in\\{1,\dots,k\\}$.
It keeps on reading its ”input” (in successive rounds of length $n$ to read
the bit-vectors $\bar{v}_{1},\dots,\bar{v}_{i-1}$) while outputting nothing,
until it non-deterministically decides to output $\bar{v}_{i}$ in $n$
successive steps, and then keeps on reading the remaining
$\bar{v}_{i+1},\dots,\bar{v}_{k}$ while outputting nothing, and accepts. The
transducer $T_{n}$ has $O(n)$ states and the number of ”accepting” ”runs” per
”input” is unbounded because $k$ is arbitrary and if $\bar{v}_{x}=\bar{v}_{y}$
for some $x<y$, then this accounts for two ”accepting” ”runs” and a single
”output”. The ”ambiguity” can be bounded, but at the cost of an exponential
blow-up, for instance by making the transducer initially guess a word
$\overline{v}\in\\{0,1\\}^{n}$ (stored in memory), output it, and then verify
$\overline{v}=\overline{v_{i}}$ for some $1\leq i\leq k$.

”Finite-valued” transductions were intensively studied in the setting of one-
way transducers. In addition to the fact that finite-valued one-way
transducers are exponentially more succinct than their ”finitely-ambiguous”
counterpart, as illustrated by Example 1, one of the main advantages of this
class is the decidability of the ”equivalence problem” [14].111[14] states
that their proof works for two-way transducers as well. Inspired by [14] the
”equivalence problem” for ”$k$-valued” ”SSTs” was shown to be decidable in
[35]. However both results rely on the Ehrenfeucht conjecture [1, 23] and
therefore provide no elementary upper bounds.

For one-way transducers and for a fixed $k$, being ”$k$-valued” can be checked
in PTime [26]. It is also known that every ”$k$-valued” one-way transducer can
be effectively decomposed into a union of $k$ ”unambiguous” one-way
transducers of exponential size [43, 44, 40]. For both two-way transducers and
”SSTs”, checking ”$k$-valuedness” for fixed $k$ is a PSpace problem (see e.g.
[5] for ”SSTs”). Decomposing ”finite-valued” ”SSTs” and deciding finite-
valuedness for ”SSTs” were listed as open problems in [5], more than 10 years
back. Compared to one-way finite transducers, new challenges arise with SSTs,
due to the extra power they enjoy to produce ”outputs”. For example over the
alphabet $\Sigma=\\{0,1\\}$, consider the set of pairs
$(w,0^{n_{0}}1^{n_{1}})$ and $(w,1^{n_{1}}0^{n_{0}})$, where $w\in\Sigma^{*}$
and $n_{b}$ is the number of bits $b\in\\{0,1\\}$ in $w$. The ”outputs” are
essentially the concatenated numbers of $0$ and $1$, in unary, and in any
order. This transduction is ”$2$-valued”, but not realizable by any one-way
finite transducer. However, the following single-state ”SST” $T$ with 2
registers $X_{0},X_{1}$ (both initially empty) realizes it: whenever it reads
$b\in\\{0,1\\}$, it non-deterministically does the ”update” $X_{b}:=bX_{b}$ or
$X_{b}:=X_{b}b$ (while $X_{1-b}$ is unchanged), and eventually ”outputs”
either $X_{0}X_{1}$ or $X_{1}X_{0}$. The ability of ”SSTs” to generate
”outputs” non-linearly makes their study challenging. To illustrate this,
consider the following slight modification of $T$: $X_{0}$ is initialized with
$1$ instead of the empty word. The resulting SST is not finite-valued anymore,
because on reading $0^{n}$, it would output $0^{\ell}10^{m}$ for all $\ell,m$
such that $\ell+m=n$.

Another open problem was the relationship between ”SSTs” and two-way
transducers in the finite-valued case. It is not hard to see that the standard
translation from deterministic two-way transducers to ”deterministic” ”SSTs”
also applies to the ”finite-valued” case, see the proof of Theorem 2 below.
The converse translation however is far more complicated and relies on a
decomposition theorem for ”SSTs”, which we establish here.

##### Contributions.

The results presented in this paper draw a rather complete picture about
”finite-valued” ”SSTs”, answering several open problems from [5]. First, we
show that ”$k$-valued” ”SSTs” enjoy the same decomposition property as one-way
transducers:

######  Theorem 1 (name=, restate=Decomposition).

For all $k\in\mathbb{N}$, every $k$-valued ”SST” can be decomposed into a
union of $k$ ”single-valued” (or even ”deterministic”) ”SSTs”. The complexity
of the construction is elementary.

An important consequence of the above theorem is the ”equivalence” of ”SSTs”
and two-way transducers in the ”finite-valued” setting:

######  Theorem 2 (name=, restate=EquivalentTwoWay).

Let $R\subseteq\Sigma^{*}\times\Sigma^{*}$ be a ”finite-valued” relation. If
$R$ can be realized by an ”SST”, then an ”equivalent” two-way transducer can
be effectively constructed, and vice-versa.

A second consequence of Theorem 1 is an elementary upper bound for the
”equivalence problem” of ”finite-valued” ”SSTs” [35]:

######  Theorem 3 (name=, restate=EquivalenceProblem).

The ”equivalence problem” for ”$k$-valued” ”SSTs” can be solved with
elementary complexity.

###### Proof.

Given two ”$k$-valued” ”SSTs” $T,T^{\prime}$, we first decompose them into
unions of $k$ ”single-valued” ”SSTs” $T_{1},\dots,T_{k}$ and
$T^{\prime}_{1},\dots,T^{\prime}_{k}$, respectively. By [2] we can even assume
that every $T_{i}$ and $T^{\prime}_{j}$ is a ”deterministic” ”SST”. Finally,
[5, Theorem 4.4] shows how to check the ”equivalence” of
$\bigcup_{i=1}^{k}T_{i}$ and $\bigcup_{i=1}^{k}T^{\prime}_{i}$ in PSpace. ∎

Our last, and main, contribution is to establish the decidability of ”finite
valuedness” for ”SSTs”:

######  Theorem 4 (name=, restate=Effectiveness).

Given any ”SST” $T$, we can decide in PSpace if $T$ is ”finite-valued”, and in
PTime if the number of variables is fixed. Moreover, this problem is at least
as hard as the ”equivalence problem” for ”deterministic” ”SSTs”.

This last result is the most technical one, and requires to reason on
particular substructures (”W-patterns”) of ”SSTs”. Such substructures have
been already used for one-way transducers, but for ”SSTs” genuine challenges
arise. The starting point of our proof is a recent result allowing to
determine if two runs of an ”SST” are far apart [20]. The proof then relies on
identifying suitable patterns and extending techniques from word combinatorics
to more involved word inequalities.

Based on the ”equivalence” between ”SSTs” and two-way transducers in the
”finite-valued” setting (Theorem 2), and the decidability of ”finite
valuedness” for ”SST” (Theorem 4), we exhibit an alternative proof for the
following (known) result:

######  Corollary 1 (name=[46],restate=Yen).

Finite-valuedness of two-way transducers is decidable in PSpace.

Observe also that without the results in this paper, the result of [46] could
not help to show Theorem 4, because only the conversion of ”finite-valued”
two-way transducers into ”finite-valued” ”SSTs” was known (under the
assumption that any input positions is visited a bounded number of times), but
not the other way around. Finally note that Theorem 1 (and Theorem 2) also
provides a decomposition result for ”finite-valued” two-way transducers.

We also observe that since ”SSTs” and non-deterministic MSO transductions are
equivalent [5], Theorem 4 entails decidability of ”finite valuedness” for non-
deterministic MSO transductions as well. Moreover, since in the ”single-
valued” case, ”deterministic” ”SSTs” and MSO transductions are also equivalent
[2], Theorem 1 implies a decomposition result for MSO transductions: any
”$k$-valued” non-deterministic MSO transduction can be decomposed as a union
of $k$ (deterministic) MSO transductions. Finally, from Theorem 2, we also get
that under the assumption of ”finite valuedness”, non-deterministic MSO
transductions, two-way transducers and ”SST” are equally expressive.

##  2 Preliminaries

For convenience, technical terms and notations in the electronic version of
this manuscript are hyper-linked to their definitions (cf.
https://ctan.org/pkg/knowledge).

Hereafter, $\mathbb{N}$ (resp. $\mathbb{N}_{+}$) denotes the set of non-
negative (resp. strictly positive) integers, and $\Sigma$ denotes a generic
alphabet.

##### Words and relations.

We denote by $\varepsilon$ the empty word, by $|u|$ the length of a word
$u\in\Sigma^{*}$, and by $u[i]$ its $i$-th letter, for $1\leq i\leq|u|$. We
introduce a ”convolution” operation on words, which is particularly useful to
identify robust and well-behaved classes of relations, as it is done for
instance in the theory of automatic structures [8]. For simplicity, we only
consider ”convolutions” of words of the same length. Given $u,v\in\Sigma^{*}$,
with $|u|=|v|$, the convolution $""u\mathbin{\otimes}v@convolution""$ is a
word over $(\Sigma^{2})^{*}$ of length $|u|=|v|$ such that
$(u\mathbin{"\otimes@convolution"}v)[i]=(u[i],v[i])$ for all $1\leq i\leq|u|$.
For example, $(aba)\mathbin{"\otimes@convolution"}(bcc)=(a,b)(b,c)(a,c)$. As
$\mathbin{"\otimes@convolution"}$ is associative, we may write
$u\mathbin{"\otimes@convolution"}v\mathbin{"\otimes@convolution"}w$ for any
words $u,v,w$.

A relation $R\subseteq(\Sigma^{*})^{k}$ is ””length-preserving”” if
$|u_{1}|=\dots=|u_{k}|$ for all $(u_{1},\dots,u_{k})\in R$. A ”length-
preserving” relation is ””automatic”” if the language
$\\{u_{1}\mathbin{"\otimes@convolution"}\dots\mathbin{"\otimes@convolution"}u_{k}\mid(u_{1},\dots,u_{k})\in
R\\}$ is recognized by a finite state automaton. A binary relation
$R\subseteq\Sigma^{*}\times\Sigma^{*}$ (not necessarily ”length-preserving”)
is ””$k$-valued””, for $k\in\mathbb{N}$, if for all $u\in\Sigma^{*}$, there
are at most $k$ words $v$ such that $(u,v)\in R$. It is ””finite-valued”” if
it is ”$k$-valued” for some $k$.

##### Variable updates.

Fix a finite set of variables $\mathcal{X}=\\{X_{1},\dots,X_{m}\\}$, disjoint
from the alphabet $\Sigma$. A (copyless) ””update”” is any mapping
$\alpha:\mathcal{X}\rightarrow(\Sigma\uplus\mathcal{X})^{*}$ such that each
variable $X\in\mathcal{X}$ appears _at most once_ in the word
$\alpha(X_{1})\dots\alpha(X_{m})$. Such an ”update” can be morphically
extended to words over $\Sigma\uplus\mathcal{X}$, by simply letting
$\alpha(a)=a$ for all $a\in\Sigma$. Using this, we can compose any two
”updates” $\alpha,\beta$ to form a new ”update”
$\alpha\,\beta:\mathcal{X}\rightarrow(\Sigma\uplus\mathcal{X})^{*}$, defined
by $(\alpha\,\beta)(X)=\beta(\alpha(X))$ for all $X\in\mathcal{X}$. An
”update” is called ””initial@@update”” (resp. ””final@@update””) if all
variables in $\mathcal{X}$ (resp. $\mathcal{X}\setminus\\{X_{1}\\}$) are
mapped to the empty word. The designated variable $X_{1}$ is used to store the
final ”output” produced by an ”SST”, as defined in the next paragraph.

##### Streaming string transducers.

A (non-deterministic, copyless) ””streaming string transducer”” (SST for
short) is a tuple $T=(\Sigma,\mathcal{X},Q,Q_{\mathrm{init}},$
$Q_{\mathrm{final}},\Omega,\Delta)$, where $\Sigma$ is an alphabet, $Q$ is a
finite set of states, $Q_{\mathrm{init}},Q_{\mathrm{final}}\subseteq Q$ are
the sets of initial and final states, $\Omega$ is a function from final states
to ”final@@update” ”updates”, and $\Delta$ is a finite transition relation
consisting of tuples of the form $(q,a,\alpha,q^{\prime})$, where
$q,q^{\prime}\in Q$ are the source and target states, $a\in\Sigma$ is an input
symbol, and $\alpha$ is an ”update”. We often denote a transition
$(q,a,\alpha,q^{\prime})\in\Delta$ by the annotated arrow:

$q\xrightarrow{a/\alpha}q^{\prime}.$

The ””size”” $|T|$ of an ”SST” $T$ is defined as the number of states plus the
size of its transition relation.

A ””run”” of $T$ is a sequence of transitions from $\Delta$ of the form

$\rho=q_{0}\xrightarrow{a_{1}/\alpha_{1}}q_{1}\xrightarrow{a_{2}/\alpha_{2}}q_{2}\dots
q_{n-1}\xrightarrow{a_{n}/\alpha_{n}}q_{n}.$

The input consumed by $\rho$ is the word
$""\operatorname{in}(\rho)@input""=a_{1}\dots a_{n}$. The ””update induced
by”” $\rho$ is the composition $\beta=\alpha_{1}\dots\alpha_{n}$. We write
$\rho:\>u/\beta$ to mean that $\rho$ is a ”run” with $u$ as ”consumed input”
and $\beta$ as ”induced update”. A ”run” $\rho$ as above is ””accepting”” if
the first state is initial and the last state is final, namely, if $q_{0}\in
Q_{\mathrm{init}}$ and $q_{n}\in Q_{\mathrm{final}}$. In this case, the
”induced update”, extended to the left with the ”initial update” denoted by
$"\iota@initialupdate"$ and to the right with the ”final update”
$\Omega(q_{n})$, gives rise to an ”update”
$"\iota@initialupdate"\,\beta\,\Omega(q_{n})$ that maps $X_{1}$ to a word over
$\Sigma$ and all remaining variables to the empty word. In particular, the
latter ”update” determines the output produced by $\rho$, defined as the word
$""\operatorname{out}(\rho)@output""=("\iota@initialupdate"\,\beta\,\Omega(q_{n}))(X_{1})$.

The relation realized by an ”SST” $T$ is

$""\mathscr{R}(T)@relation""~{}=~{}\big{\\{}\big{(}"\operatorname{in}(\rho)@input","\operatorname{out}(\rho)@output"\big{)}\in\Sigma^{*}\times\Sigma^{*}~{}\big{|}~{}\rho\text{
"accepting" "run" of }T\big{\\}}$

An ”SST” is $k$-valued (resp. finite-valued) if its ”realized relation” is so.
It is ””deterministic”” if it has a single initial state and the transition
relation is a partial function (from pairs of states and input letters to
pairs of ”updates” and states). It is ””unambiguous”” if it admits at most one
”accepting” ”run” on each ”input”. Similarly, it is called ””$k$-ambiguous””
if it admits at most $k$ ”accepting” ”runs” on each ”input”. Of course, every
”deterministic” ”SST” is ”unambiguous”, and every ”unambiguous” ”SST” is
”single-valued” (i.e. $1$-valued). Two ”SSTs” $T_{1},T_{2}$ are ””equivalent””
if $"\mathscr{R}(T_{1})@relation"="\mathscr{R}(T_{2})@relation"$. The
”equivalence problem” for ”SSTs” is undecidable in general, and it is so even
for one-way transducers [22, 28]. However, decidability is recovered for
”finite-valued” ”SSTs”:

######  Theorem 5 ([35]).

”Equivalence” of ”finite-valued” ”SSTs” is decidable.

Note that checking equivalence is known to be in PSpace for _”deterministic”_
”SSTs”. This easily generalizes to unions of ”deterministic” (hence ”single-
valued”) ”SSTs”, because the ”equivalence” checking algorithm is exponential
only in the number of variables:

######  Theorem 6 ([5]).

The following problem is in PSpace: given $n+m$ ”deterministic” ”SSTs”
$T_{1},\dots,T_{n},T^{\prime}_{1},\dots,T^{\prime}_{m}$, decide whether
$\bigcup_{i=1}^{n}"\mathscr{R}(T_{i})@relation"=\bigcup_{j=1}^{m}"\mathscr{R}(T^{\prime}_{j})@relation"$.

For any fixed $k$, the ”$k$-valuedness” property is decidable in PSpace:

######  Theorem 7 ([5]).

For any fixed $k\in\mathbb{N}$, the following problem is in222In [5], no
complexity result is provided, but the decidability procedure relies on a
reduction to the emptiness of a $1$-reversal $k(k+1)$-counter machine, based
on the proof for equivalence of deterministic SST [3]. The counter machine is
exponential in the number of variables only, and the result follows since
emptiness of counter machines with fixed number of reversals and fixed number
of counters is in NLogSpace [24]. PSpace: given an ”SST” $T$, decide whether
$T$ is ”$k$-valued”. It is in PTime if one further restricts to ”SSTs” with a
fixed number of variables.

The decidability status of ”finite valuedness” for ”SSTs”, that is, for
unknown $k$, was an open problem. Part of our contribution is to show that
this problem is also decidable.

###  2.1 Pumping and word combinatorics

When reasoning with automata, it is common practice to use pumping arguments.
This section introduces pumping for ”SSTs”, as well as combinatorial results
for reasoning about (in)equalities between pumped ”outputs” of ”SSTs”.

In order to have adequate properties for pumped runs of ”SSTs”, the notion of
loop needs to be defined so as to take into account how the content of
variables “flows” into other variables when performing an ”update”. We define
the ””skeleton”” of an ”update”
$\alpha:\mathcal{X}\rightarrow(\Sigma\uplus\mathcal{X})^{*}$ as the ”update”
$\hat{\alpha}:\mathcal{X}\rightarrow\mathcal{X}^{*}$ obtained from $\alpha$ by
removing all the letters from $\Sigma$. Note that there are only finitely many
”skeletons”, and their composition forms a finite monoid, called the
””skeleton monoid”” (this is very similar to the flow monoid from [35], but
does not rely on any normalization).

A ””loop”” of a ”run” $\rho$ of an ”SST” is any factor $L$ of $\rho$ that
starts and ends in the same state and ”induces@induced update” a ””skeleton-
idempotent”” ”update”, namely, an ”update” $\alpha$ such that $\alpha$ and
$\alpha\,\alpha$ have the same ”skeleton”. For example, the ”update”
$\alpha:\>X_{1}\mapsto a\,X_{1}\,b\,X_{2}\,c,\>X_{2}\mapsto a$ is ”skeleton-
idempotent” and thus can be part of a ”loop”. We will often denote a ”loop” in
a ”run” by an interval $[i,j]$. In this case, it is convenient to assume that
the indices $i,j$ represent “positions” in-between the transitions, thus
identifying occurrences of states; in this way, adjacent ”loops” can be
denoted by intervals of the form $[i_{1},i_{2}]$, $[i_{2},i_{3}]$, etc. In
particular, if the run consists of $n$ transitions, then the largest possible
interval on it is $[0,n]$. For technical reasons, we do allow ””empty@@loop””
”loops”, that is, ”loops” of the form $[i,j]$, with $i=j$ and with the
”induced update” being the identity function on $\mathcal{X}$.

The run obtained from $\rho$ by pumping $n$ times a ”loop” $L$ is denoted
$""\operatorname{pump}^{n}_{L}(\rho)@pumping""$. If we are given an $m$-tuple
of _pairwise disjoint_ ”loops” $\bar{L}=(L_{1},\dots,L_{m})$ and an $m$-tuple
of (positive) numbers $\bar{n}=(n_{1},\dots,n_{m})$, then we write
$\reintro[pumping]{\operatorname{pump}^{\bar{n}}_{\bar{L}}(\rho)}$ for the
”run” obtained by pumping simultaneously $n_{i}$ times $L_{i}$, for each
$1\leq i\leq m$.

The next lemma is a Ramsey-type argument that, based on the number of states
of the ”SST”, the size of the ”skeleton monoid”, and a number $n$, derives a
minimum length for a ”run” to witness $n+1$ points and ”loops” between pairs
of any of these points. The reader can refer to [30] to get good estimates of
the values of $E,H$.

######  Lemma 1 (name=, restate=RamseyLemma).

Given an ”SST”, one can compute two numbers $E,H$ such that for every run
$\rho$, every $n\in\mathbb{N}$, and every set $I\subseteq\\{0,\dots,|\rho|\\}$
of cardinality $En^{H}+1$, there is a subset $I^{\prime}\subseteq I$ of
cardinality $n+1$ such that for all $i<j\in I^{\prime}$ the interval $[i,j]$
is a ”loop” of $\rho$. The values of $E,H$ are elementary in the size of the
”SST”.

Below, we describe the effect on the ”output” of ”pumping” ”loops” in a ”run”
of an ”SST”. We start with the following simple combinatorial result:

######  Lemma 2 (name=, restate=LoopPumpingLemma).

Let $\alpha$ be a ”skeleton-idempotent” ”update”. For every variable $X$,
there exist two words $u,v\in\Sigma^{*}$ such that, for all positive natural
numbers $n\in\mathbb{N}_{+}$, $\alpha^{n}(X)=u^{n-1}\,\alpha(X)\,v^{n-1}$.

It follows that ”pumping” ”loops” in a ”run” corresponds to introducing
repeated copies of factors in the ”output”. Similar results can be found in
[35] for ”SSTs” and in [36, 18] for two-way transducers:

######  Corollary 2.

Let $\rho$ be an ”accepting” ”run” of an ”SST” and let
$\bar{L}=(L_{1},\dots,L_{m})$ be a tuple of pairwise disjoint ”loops” in
$\rho$. Then, for some $r\leq 2m|\mathcal{X}|$ there exist words
$w_{0},\dots,w_{r},u_{1},\dots,u_{r}$ and indices $1\leq i_{1},\dots,i_{r}\leq
m$, not necessarily distinct, such that for every tuple
$\bar{n}=(n_{1},\dots,n_{m})\in\mathbb{N}^{m}_{+}$ of positive natural
numbers,

$"\operatorname{out}("\operatorname{pump}^{\bar{n}}_{\bar{L}}(\rho)@pump")@output"~{}=~{}w_{0}\,u_{1}^{n_{i_{1}}-1}\,w_{1}\,\dots\,u_{r}^{n_{i_{r}}-1}\,w_{r}.$

###### Proof.

This follows immediately from Lemma 2. Note that the content of any variable
$X$ just after ”pumping” a ”loop” either appears as infix of the final output,
or is erased by some later ”update”. In both cases, each ”pumped” ”loop”
$L_{i}$ induces in the ”output” $(n_{i}-1)$-folded repetitions of $2k$
(possibly empty) factors, where $k$ is the number of variables of the ”SST”.
Since the ”loops” are pairwise disjoint, they contribute such factors without
any interference. The final output
$"\operatorname{out}("\operatorname{pump}^{\bar{n}}_{\bar{L}}(\rho)@pump")@output"$
thus features repetitions of $r=2km$ (possibly empty) factors. ∎

The rest of the section analyses properties of words with repeated factors
like the one in Corollary 2.

######  Definition 1.

A ””word inequality”” with repetitions parametrized in $\mathtt{X}$ is a pair
$e=(w,w^{\prime})$ of terms of the form

$\displaystyle w$
$\displaystyle~{}=~{}s_{0}~{}t_{1}^{\mathtt{x}_{1}}~{}s_{1}~{}\dots~{}t_{m}^{\mathtt{x}_{m}}~{}s_{m}$
$\displaystyle w^{\prime}$
$\displaystyle~{}=~{}s^{\prime}_{0}~{}{t^{\prime}_{1}}^{\mathtt{y}_{1}}~{}s^{\prime}_{1}~{}\dots~{}{t^{\prime}_{n}}^{\mathtt{y}_{n}}~{}{s^{\prime}_{n}}$

where $s_{i},t_{i},s^{\prime}_{j},t^{\prime}_{j}\in\Sigma^{*}$ and
$\mathtt{x}_{i},\mathtt{y}_{j}\in\mathtt{X}$ for all $i,j$. The set of
””solutions”” of $e=(w,w^{\prime})$, denoted
$\reintro[solutions]{\operatorname{Sols}(e)}$, consists of the mappings
$f:\mathtt{X}\rightarrow\mathbb{N}$ such that $f(w)\neq f(w^{\prime})$, where
$f(w)$ is the word obtained from $w$ by substituting every formal parameter
$\mathtt{x}\in\mathtt{X}$ by $f(\mathtt{x})$, and similarly for
$f(w^{\prime})$. A ””system of word inequalities”” is a non-empty finite set
$E$ of ”inequalities” as above, and its set of ”solutions” is given by
$\reintro[solutions]{\operatorname{Sols}(E)}=\bigcap_{e\in
E}"\operatorname{Sols}(e)@solutions"$.

The next theorem states that if there exists a solution to a system of
inequalities parameterized by a single variable $\mathtt{x}$, then the set of
solutions is co-finite.

######  Theorem 8 (name=[37, Theorem 4.3]).

Given a ”word inequality” $e$ with repetitions parameterized by single
variable $\mathtt{x}$, $"\operatorname{Sols}(e)@solutions"$ is either empty or
co-finite; more precisely, if the left (resp. right) hand-side of $e$ contains
$m$ (resp. $n$) repeating patterns (as in Definition 1), then either
$"\operatorname{Sols}(e)@solutions"=\emptyset$ or
$|\mathbb{N}\setminus"\operatorname{Sols}(e)@solutions"|\leq m+n$.

Finally, we present two corollaries of the above theorem, that will be used
later. The first corollary concerns ”satisfiability” of a ”system of
inequalities”. Formally, we say that a ”word inequality” $e$ (resp. a ”system
of inequalities” $E$) is ””satisfiable”” if its set of ”solutions” is non-
empty.

######  Corollary 3 (name=, restate=SaarelaA).

Let $E$ be a ”system of word inequalities”. If every ”inequality” $e\in E$ is
”satisfiable”, then so is the ”system” $E$.

The second corollary is related to the existence of large sets of solutions
for a ”satisfiable” ”word inequality” that avoid any correlation between
variables. To formalize the statement, it is convenient to fix a total order
on the variables of the ”inequality”, say
$\mathtt{x}_{1},\dots,\mathtt{x}_{k}$, and then identify every function
$f:\mathtt{X}\rightarrow\mathbb{N}$ with the $k$-tuple of values
$\bar{x}=(x_{1},\dots,x_{k})$, where $x_{i}=f(\mathtt{x}_{i})$ for all
$i=1,\dots,k$. According to this correspondence, the corollary states the
existence of sets of solutions that look like Cartesian products of finite
intervals of values, each with arbitrarily large cardinality. The statement of
the corollary is in fact slightly more complicated than this, as it discloses
dependencies between the intervals. We also observe that the order in which we
list the variables is arbitrary, but different orders will induce different
dependencies between intervals.

######  Corollary 4 (name=, restate=SaarelaB).

Let $e$ be a ”word inequality” with repetitions parametrized in
$\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$. If $e$ is
”satisfiable”, then

$\exists\ell_{1}~{}\forall h_{1}~{}\dots~{}\exists\ell_{k}~{}\forall
h_{k}\quad\\!\\!\\!\\!\underbrace{[\ell_{1},h_{1}]}_{\text{values for
}\mathtt{x}_{1}}\\!\\!\\!\\!\times\,\dots\,\times\\!\\!\\!\\!\underbrace{[\ell_{k},h_{k}]}_{\text{values
for
<EMAIL_ADDRESS>
###  2.2 Delay between accepting runs

We briefly recall the definitions from [20] and introduce a measure of
similarity (called ”delay”) between ”accepting” ”runs” of an ”SST” that have
the same ”input” and the same ”output”.

We first give some intuition, followed by definitions and an example.
Naturally, the difference between the amount of output symbols produced during
a run should be an indicator of (dis)similarity. However, as ”SSTs” do not
necessarily build their output from left to right, one must also take into
account the position where an output symbol is placed. For example, compare
two ”runs” $\rho$ and $\rho^{\prime}$ on the same ”input” that produce the
same ”output” $aaabbb$. After consuming a prefix of the input, $\rho$ may have
produced $aaa\\_\ \\_\ \\_$ and $\rho^{\prime}$ may have produced $\\_\ \\_\
\\_bbb$. The amount of produced output symbols is the same, but the ”runs” are
delayed because $\rho$ built the ”output” from the left, whereas
$\rho^{\prime}$ did it from the right. This idea of ”delay” comes with an
important caveat. As another example, consider two runs $\rho$ and
$\rho^{\prime}$ on the same ”input” that produce the same ”output” $aaaaaa$,
and assume that, after consuming the same prefix of the ”input”, $\rho$ and
$\rho^{\prime}$ produced $aaa\\_\ \\_\ \\_$ and $\\_\ \\_\ \\_aaa$,
respectively. Note that the ”output” $aaaaaa$ is a periodic word. Hence, it
does not matter if $aaa$ is appended or prepended to a word with period $a$.
In general, one copes with this phenomenon by dividing the ”output” into
periodic parts, where all periods are bounded by a well-chosen parameter $C$.
So, intuitively, the ”delay” measures the difference between the numbers of
output symbols that have been produced by the two ”runs”, up to the end of
each of periodic factor. The number of produced output symbols is formally
captured by a ”weight” function, defined below, and the ”delay” aggregates the
”weight” differences.

For an ”accepting” ”run” $\rho$, a position $t$ of $\rho$, and a position $j$
in the output $"\operatorname{out}(\rho)@output"$, we denote by
$""\operatorname{weight}^{t}_{j}(\rho)@weight""$ the number of output
positions $j^{\prime}\leq j$ that are produced by the prefix of $\rho$ up to
position $t$. We use the above notation when $j$ witnesses a change in a
repeating pattern of the output. These changes in repeating patterns are
called cuts, as formalized below.

Let $w$ be any non-empty word (e.g. the output of $\rho$ or a factor of it).
The primitive root of $w$, denoted $""\operatorname{root}(w)@root""$, is the
shortest word $r$ such that $w\in\\{r\\}^{*}$. For a fixed integer $C>0$ we
define a factorization $w[1,j_{1}],w[j_{1}+1,j_{2}],\dots,w[j_{n}+1,j_{n+1}]$
of $w$ in which every $j_{i}$ is chosen as the rightmost position for which
$w[j_{i-1}+1,j_{i}]$ has ”primitive root” of length not exceeding $C$. These
positions $j_{1},\dots,j_{n}$ are called ””$C$-cuts””. More precisely:

  * •

the [$C$-cuts]first $C$-cut of $w$ is the largest position $j\leq|w|$, such
that $|"\operatorname{root}(w[1,j])@root"|\leq C$;

  * •

if $j$ is the ”$i$-th $C$-cut” of $w$, then the [$C$-cuts]$(i+1)$-th $C$-cut
of $w$ is the largest position $j^{\prime}>j$ such that
$|"\operatorname{root}(w[j+1,j^{\prime}])@root"|\leq C$.

We denote by $""{C}\mspace{-3.0mu}\operatorname{-cuts}(w)@setofcuts""$ the set
of all ”$C$-cuts” of $w$.

We are now ready to define the notion of ”delay”. Consider two ”accepting”
”runs” $\rho,\rho^{\prime}$ of an ”SST” with the same ”input”
$u="\operatorname{in}(\rho)@input"="\operatorname{in}(\rho^{\prime})@input"$
and the same ”output”
$w="\operatorname{out}(\rho)@output"="\operatorname{out}(\rho^{\prime})@output"$,
and define:

$""{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay""~{}=\max\limits_{\begin{subarray}{c}t\leq|u|,\\\
j\,\in\,"{C}\mspace{-3.0mu}\operatorname{-cuts}(w)@setofcuts"\end{subarray}}~{}\big{|}"\operatorname{weight}^{t}_{j}(\rho)@weight"-"\operatorname{weight}^{t}_{j}(\rho^{\prime})@weight"\big{|}$

that is, the maximum, over all prefixes of the ”runs” and all $C$-cuts of the
”output”, of the absolute values of the differences of the corresponding
weights in $\rho$ and $\rho^{\prime}$. Note that the ”delay” is only defined
for ”accepting” ”runs” with same ”input” and ”output”. So whenever we write
$"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"$, we
implicitly mean that $\rho,\rho^{\prime}$ have _same ”input” and same
”output”_.

######  Example 2.

Let $w=abcccbb$ be the ”output” of runs $\rho,\rho^{\prime}$ on the same
”input” of length $2$. Assume $\rho$ produces $abc\\_\ \\_bb$ and then
$abcccbb$, whereas $\rho^{\prime}$ produces $\\_\ \\_\ \\_c\\_bb$ and then
$abcccbb$. For $C=2$, we obtain
$"{2}\mspace{-3.0mu}\operatorname{-cuts}(w)@setofcuts"=\\{2,5,7\\}$, i.e., $w$
is divided into $ab|ccc|bb$. To compute the
$"{2}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"$, we need
to calculate ”weights” at ”cuts”. For $t=0$,
$"\operatorname{weight}^{0}_{j}(\rho)@weight"="\operatorname{weight}^{0}_{j}(\rho^{\prime})@weight"=0$
for all $j\in"{2}\mspace{-3.0mu}\operatorname{-cuts}(w)@setofcuts"$ because
nothing has been produced. For $t=2$,
$"\operatorname{weight}^{2}_{j}(\rho)@weight"="\operatorname{weight}^{2}_{j}(\rho^{\prime})@weight"=j$
for all $j\in"{2}\mspace{-3.0mu}\operatorname{-cuts}(w)@setofcuts"$ because
the whole output has been produced. Only the case $t=1$ has an impact on the
delay. We have $"\operatorname{weight}^{1}_{2}(\rho)@weight"=2$,
$"\operatorname{weight}^{1}_{5}(\rho)@weight"=3$, and
$"\operatorname{weight}^{1}_{7}(\rho)@weight"=5$. Also, we have
$"\operatorname{weight}^{1}_{2}(\rho^{\prime})@weight"=0$,
$"\operatorname{weight}^{1}_{5}(\rho)@weight"=1$, and
$"\operatorname{weight}^{1}_{7}(\rho)@weight"=3$. Hence, we obtain
$"{2}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"=2$.

We recall below a few crucial results from [20]. A first result shows that the
relation of pairs of ”runs” having bounded ”delay” (for a fixed bound) is
”automatic” — for this to make sense, we view a ”run” of an ”SST” as a finite
word, with letters representing transitions, and we recall that a relation is
”automatic” if its ”convolution” language is regular.

######  Lemma 3 ([20, Theorem 5]).

Given an ”SST” and some numbers $C,D$, the relation consisting of pairs of
”accepting” ”runs” $(\rho,\rho^{\prime})$ such that
$"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"\leq D$ is
”automatic”.

###### Proof.

The statement in [20, Theorem 5] is not for ”runs” of ”SSTs”, but for
sequences of ”updates”. One can easily build an automaton that checks if two
sequences of transitions, encoded by their ”convolution”, form ”accepting”
”runs” $\rho,\rho^{\prime}$ of the given ”SST” on the same ”input”. The
remaining condition
$"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"\leq D$
only depends on the underlying sequences of ”updates” determined by $\rho$ and
$\rho^{\prime}$, and can be checked using [20, Theorem 5]. ∎

A second result shows that given two ”runs” with large ”delay”, one can find a
set of positions on the ”input” (the cardinality of which depends on how large
the ”delay” is) in such a way that any interval starting just before any of
these positions and ending just after any other of these positions is a ”loop”
on both ”runs” such that, when ”pumped”, produces different ”outputs”. By this
last result, large ”delay” intuitively means “potentially different
”outputs””.

######  Lemma 4 (name=[20, Lemma 6]).

Given an ”SST”, one can compute333We remark that the notation and the actual
bounds here differ from the original presentation of [20], mainly due to the
fact that here we manipulate ”runs” with explicit states and ”loops” with
”idempotent” ”skeletons”. In particular, the parameters $C,D,m$ here
correspond respectively to the values $kE^{2},\ell E^{4},CE^{2}$ with
$k,\ell,C$ as in [20, Lemma 6], and $E$ as in our Lemma 1.  some numbers $C,D$
such that, for all $m\geq 1$ and all runs $\rho,\rho^{\prime}$: if
$"{Cm}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay">Dm^{2}$,
then there exist $m$ positions $0\leq\ell_{1}<\dots<\ell_{m}\leq|\rho|$ such
that, for every $1\leq i<j\leq m$, the interval $L_{i,j}=[\ell_{i},\ell_{j}]$
is a ”loop” on both $\rho$ and $\rho^{\prime}$ and satisfies

$"\operatorname{out}("\operatorname{pump}^{2}_{L_{i,j}}(\rho)@pump")@output"\>\neq\>"\operatorname{out}("\operatorname{pump}^{2}_{L_{i,j}}(\rho^{\prime}<EMAIL_ADDRESS>
To reason about ”finite valuedness” we will often consider several ”accepting”
”runs” on the same ”input” that have pairwise large ”delays”. By Lemma 4,
every two such ”runs” can be pumped so as to witness different ”outputs”. The
crux however is to show that these runs can be pumped _simultaneously_ so as
to get pairwise different ”outputs”. This is indeed possible thanks to:

######  Lemma 5.

Let $C,D$ be computed as in Lemma 4, and $k$ be an arbitrary number. Then one
can compute a number $m$ such that, for all runs $\rho_{0},\dots,\rho_{k}$ on
the same ”input” and with $\displaystyle\bigwedge\nolimits_{0\leq i<j\leq
k}\big{(}"\operatorname{out}(\rho_{i})@output"\neq"\operatorname{out}(\rho_{j})@output"~{}\vee~{}"{Cm}\mspace{-3.0mu}\operatorname{-delay}(\rho_{i},\rho_{j})@delay">Dm^{2}\big{)}$,
there is a tuple $\bar{L}=(L_{i,j})_{0\leq i<j\leq k}$ of disjoint intervals
that are ”loops” on all ”runs” $\rho_{0},\dots,\rho_{k}$, and there is a tuple
$\bar{n}=(n_{i,j})_{0\leq i<j\leq k}$ of positive numbers such that

$\text{for all }0\leq i<j\leq
k\,,\quad"\operatorname{out}("\operatorname{pump}^{\bar{n}}_{\bar{L}}(\rho_{i})@pump")@output"\>\neq\>"\operatorname{out}("\operatorname{pump}^{\bar{n}}_{\bar{L}}(\rho_{j})@pump")@output"\,.$

###### Proof.

We first define $m$. Let $E,H$ be as in Lemma 1, and set $m:=m_{0}+1$ for the
sequence $m_{0},\ldots,m_{k-1}$ defined inductively by $m_{k-1}:=k(k+1)$, and
$m_{h}:=Em_{h+1}^{H}$.

We show how to ”pump” the ”runs” in such a way that all pairs of indices $i<j$
witnessing
$"{Cm}\mspace{-3.0mu}\operatorname{-delay}(\rho_{i},\rho_{j})@delay">Dm^{2}$
before ”pumping”, will witness different ”outputs” after ”pumping”. Consider
one such pair $(i,j)$, with $i<j$, such that
$"{Cm}\mspace{-3.0mu}\operatorname{-delay}(\rho_{i},\rho_{j})@delay">Dm^{2}$,
so in particular,
$"\operatorname{out}(\rho_{i})@output"="\operatorname{out}(\rho_{j})@output"$
(if there is no such pair, then all ”runs” have pairwise different ”outputs”,
and so we are already done). We apply Lemma 4 and obtain a set $I_{i,j,0}$ of
$m=m_{0}+1$ positions such that each interval $L=[\ell,\ell^{\prime}]$ with
$\ell,\ell^{\prime}\in I_{i,j,0}$ is a loop on both $\rho_{i}$ and $\rho_{j}$,
and:

$"\operatorname{out}("\operatorname{pump}^{2}_{L}(\rho_{i})@pump")@output"\neq"\operatorname{out}("\operatorname{pump}^{2}_{L}(\rho_{j}<EMAIL_ADDRESS>(1)

Then, by repeatedly using Lemma 1, we derive the existence of sets
$I_{i,j,k-1}\subseteq\cdots\subseteq I_{i,j,1}\subseteq I_{i,j,0}$ with
$|I_{i,j,h}|=m_{h}+1$ such that each interval $L=[\ell,\ell^{\prime}]$ with
$\ell,\ell^{\prime}\in I_{i,j,h}$ is a loop on $\rho_{i},\rho_{j}$, and $h$
further runs from $\rho_{0},\ldots,\rho_{k}$ (our definition of $m$ from the
beginning of the proof is tailored to this repeated application of Lemma 1,
because $|I_{i,j,h}|=m_{h}+1=Em_{h+1}^{H}+1$). In particular, all intervals
with endpoints in $I_{i,j,k-1}$ are loops on all the
$\rho_{0},\ldots,\rho_{k}$.

In this way, for each pair $i<j$ such that $\rho_{i}$ and $\rho_{j}$ have
large ”delay”, we obtain $k(k+1)$ adjacent intervals that are loops on all
runs and that satisfy the pumping property (1) from above.

As there are at most $k(k+1)$ pairs of runs, we can now choose from the sets
of intervals that we have prepared one interval $L_{i,j}$ for each pair $i<j$
with
$"{Cm}\mspace{-3.0mu}\operatorname{-delay}(\rho_{i},\rho_{j})@delay">Dm^{2}$,
in such a way that all the chosen intervals are pairwise disjoint (for
example, we could do so by always picking among the remaining intervals the
one with the left-most right border, and then removing all intervals that
intersect this one). The selected intervals $L_{i,j}$ thus have the following
properties:

  1. 1.

$L_{i,j}$ is a ”loop” on all ”runs” $\rho_{0},\dots,\rho_{k}$,

  2. 2.

$L_{i,j}$ is disjoint from every other interval $L_{i^{\prime},j^{\prime}}$,

  3. 3.

$"\operatorname{out}("\operatorname{pump}^{2}_{L_{i,j}}(\rho_{i})@pump")@output"\neq"\operatorname{out}("\operatorname{pump}^{2}_{L_{i,j}}(\rho_{j})@pump")@output"$.

If a pair $i<j$ of ”runs” is such that
$"\operatorname{out}(\rho_{i})@output"\neq"\operatorname{out}(\rho_{j})@output"$,
then we set $L_{i,j}$ as an empty ”loop”.

Now, let $\bar{L}=(L_{i,j})_{0\leq i<j\leq k}$ be the tuple of chosen
intervals, and consider the following system of word ”inequalities” with
formal parameters $(\mathtt{x}_{i,j})_{0\leq i<j\leq k}=:\bar{\mathtt{x}}$:

$\text{for all }0\leq i<j\leq
k\,,\quad"\operatorname{out}("\operatorname{pump}^{\bar{\mathtt{x}}}_{\bar{L}}(\rho_{i})@pump")@output"\>\neq\>"\operatorname{out}("\operatorname{pump}^{\bar{\mathtt{x}}}_{\bar{L}}(\rho_{j})@pump")@output"\,.$

Here, the value of the formal parameter $\mathtt{x}_{i,j}$ determines how
often the loop $L_{i,j}$ is pumped. By Corollary 2, this corresponds to a word
”inequality” in the parameters $\mathtt{x}_{i,j}$.

Note that there is one such ”inequality” for each pair of ”runs”
$\rho_{i},\rho_{j}$ with $0\leq i<j\leq k$. By the choice of the intervals in
$\bar{L}$, each of the ”inequalities” is ”satisfiable”: indeed, the
”inequality” for $\rho_{i},\rho_{j}$ is ”satisfied” by letting
$\mathtt{x}_{i^{\prime},j^{\prime}}=1$ if $i^{\prime}\not=i$ or
$j^{\prime}\not=j$, and $\mathtt{x}_{i,j}=2$ otherwise.

By Corollary 3, the system of ”inequalities” is also ”satisfiable” with a
tuple $\bar{n}=(n_{i,j})_{0\leq i<j\leq k}$ of numbers, as claimed in the
lemma. ∎

##  3 The Decomposition Theorem

This section is devoted to the proof of the Decomposition Theorem:

*

Our proof relies on the notion of _”cover”_ of an ”SST”, which is reminiscent
of the so-called “lag-separation covering” construction [17, 39]. Intuitively,
given an SST $T$ and two integers $C,D\in\mathbb{N}$, we construct an ”SST”
$"\operatorname{Cover}_{C,D}(T)@cover"$ that is ”equivalent” to $T$, yet for
each ”input” $u$ it only admits pairs of ”accepting” ”runs” with different
”outputs” or $C$-”delay” larger than $D$.

######  Proposition 1 (name=, restate=SeparationCovering).

Given an ”SST” $T$ and two numbers $C,D$, one can compute an ”SST” called
$""\operatorname{Cover}_{C,D}(T)@cover""$ such that

  1. 1.

$"\operatorname{Cover}_{C,D}(T)@cover"$ is ”equivalent” to $T$;

  2. 2.

for every two ”accepting” ”runs” $\rho\neq\rho^{\prime}$ of
$"\operatorname{Cover}_{C,D}(T)@cover"$ having the same ”input”, either
$"\operatorname{out}(\rho)@output"\neq"\operatorname{out}(\rho^{\prime})@output"$
or $"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay">~{}D$;

  3. 3.

every ”accepting” ”run” of $"\operatorname{Cover}_{C,D}(T)@cover"$ can be
projected onto an ”accepting” ”run” of $T$.

###### Proof.

We order the set of ”accepting” ”runs” of $T$ lexicographically, and we get
rid of all the ”runs” for which there exists a lexicographically smaller ”run”
with the same ”input”, the same ”output”, and small ”delay”. Since all these
conditions are encoded by regular languages, the remaining set of ”runs” is
also regular, and this can be used to construct an ”SST”
$"\operatorname{Cover}_{C,D}(T)@cover"$ that satisfies the required
properties.

We now give more details about this construction. Let $R$ denote the set of
all ”accepting” ”runs” of $T$. Remark that $R$ is a language over the alphabet
consisting of transitions of $T$, and it is recognised by the underlying
automaton of $T$, so it is regular. Let

$""\operatorname{Sep}_{C,D}(R)@separation""~{}=~{}\big{\\{}\rho\in
R~{}\big{|}~{}\nexists\rho^{\prime}\in
R\;.\,\rho^{\prime}\\!<\\!\rho~{}\wedge~{}"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"\leq
D\big{\\}}.$

Recall that the delay is only defined for ”accepting” ”runs” with same ”input”
and same ”output”, so
$"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"\leq D$
implies that
$"\operatorname{in}(\rho)@input"="\operatorname{in}(\rho^{\prime})@input"$ and
$"\operatorname{out}(\rho)@output"="\operatorname{out}(\rho^{\prime})@output"$.
We show that

  1. a)

$"\operatorname{Sep}_{C,D}(R)@separation"$ is a regular subset of $R$;

  2. b)

$\\{("\operatorname{in}(\rho)@input","\operatorname{out}(\rho)@output")\>\mid\>\rho\in"\operatorname{Sep}_{C,D}(R)@separation"\\}=\\{("\operatorname{in}(\rho)@input","\operatorname{out}(\rho)@output")\>\mid\>\rho\in
R\\}$;

  3. c)

for every pair of ”runs”
$\rho,\rho^{\prime}\in"\operatorname{Sep}_{C,D}(R)@separation"$ over the same
”input”, either
$"\operatorname{out}(\rho)@output"\neq"\operatorname{out}(\rho^{\prime})@output"$
or $"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay">D$.

Before proving these properties, let us show how to use them to conclude the
proof of the proposition:

We start with a DFA $A$ recognizing
$"\operatorname{Sep}_{C,D}(R)@separation"$, whose existence is guaranteed by
Property a). Note that the transitions of $A$ are of the form
$\big{(}q,(s,a,\alpha,s^{\prime}),q^{\prime}\big{)}$, where
$(s,a,\alpha,s^{\prime})$ is a transition of $T$. Without loss of generality,
we assume that the source state $q$ of an $A$-transition determines the source
state $s$ of the corresponding $T$-transition, and similarly for the target
states $q^{\prime}$ and $s^{\prime}$. Thanks to this, we can turn $A$ into the
desired ”SST” $"\operatorname{Cover}_{C,D}(T)@cover"$ by simply projecting
away the $T$-states from the $T$-transitions, namely, by replacing every
transition $\big{(}q,(s,a,\alpha,s^{\prime}),q^{\prime}\big{)}$ with
$(q,a,\alpha,q^{\prime})$. To complete the construction, we observe that if
the state $q^{\prime}$ is final in $A$, then the corresponding state
$s^{\prime}$ is also final in $T$ (this is because $A$ recognizes only
”accepting” ”runs” of $T$). Accordingly, we can define the ”final@@update”
”update” of $"\operatorname{Cover}_{C,D}(T)@cover"$ so that it maps any final
state $q^{\prime}$ of $A$ to the ”final@@update” ”update”
$\Omega(s^{\prime})$, as determined by the corresponding final state
$s^{\prime}$ in $T$. Finally, thanks to Properties b) and c), the ”SST”
$"\operatorname{Cover}_{C,D}(T)@cover"$ constructed in this way clearly
satisfies the properties claimed in the proposition.

Let us now prove Properties a)–c).

Proof of Property a). Note that $"\operatorname{Sep}_{C,D}(R)@separation"$ is
obtained by combining the relations $R$,
$\\{(\rho,\rho^{\prime})~{}|~{}\rho^{\prime}<\rho\\}$, and
$\\{(\rho,\rho^{\prime})~{}|~{}"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"\leq~{}D\\}$
using the operations of intersection, projection, and complement. Also recall
that $R$ can be regarded a regular language, and that
$\\{(\rho,\rho^{\prime})~{}|~{}\rho^{\prime}<\rho\\}$ and
$\\{(\rho,\rho^{\prime})~{}|~{}"{C}\mspace{-3.0mu}\operatorname{-delay}(\rho,\rho^{\prime})@delay"~{}\leq~{}D\\}$
are ”automatic” relations (for the latter one uses Lemma 3). It is also a
standard result (cf. [27, 32, 8]) that ”automatic” relations are closed under
intersection, projection, and complement. From this it follows that
$"\operatorname{Sep}_{C,D}(R)@separation"$ is a regular language.

Proof of Property b). As $"\operatorname{Sep}_{C,D}(R)@separation"\subseteq
R$, the left-to-right inclusion is immediate. To prove the converse inclusion,
consider an ”input”-”output” pair $(u,v)$ in the right hand-side of the
equation, namely, $(u,v)$ is a pair in the relation realised by $T$. Let
$\rho$ be the lexicographically least ”accepting” ”run” of $T$ such that
$"\operatorname{in}(\rho)@input"=u$ and $"\operatorname{out}(\rho)@output"=v$.
By construction, $\rho\in"\operatorname{Sep}_{C,D}(R)@separation"$ and hence
$(u,v)$ also belongs to the left hand-side of the equation.

Proof of Property c). This holds trivially by the definition of
$"\operatorname{Sep}_{C,D}(R)@separation"$. ∎

We can now present the missing ingredients of the decomposition result.
Proposition 2 below shows that, for suitable choices of $C$ and $D$ that
depend on the ”valuedness” of $T$, $"\operatorname{Cover}_{C,D}(T)@cover"$
turns out to be ”$k$-ambiguous”.

This will enable the decomposition result via a classical technique that
decomposes any ”$k$-ambiguous” automaton/transducer into a union of $k$
”unambiguous” ones (see Proposition 3 further below).

######  Proposition 2.

Let $T$ be a ”$k$-valued” ”SST” and let $C,D,m$ be as in Lemma 5 (note that
$m$ depends on $k$). The ”SST” $"\operatorname{Cover}_{Cm,Dm^{2}}(T)@cover"$
is ”$k$-ambiguous”.

###### Proof.

We prove the contrapositive of the statement. Assume that
$"\operatorname{Cover}_{Cm,Dm^{2}}(T)@cover"$ is not ”$k$-ambiguous”, that is,
it admits $k+1$ ”accepting” ”runs” $\rho_{0},\dots,\rho_{k}$ on the same
”input”. Recall from Proposition 1 that for all $0\leq i<j\leq k$, either
$"\operatorname{out}(\rho_{i})@output"\neq"\operatorname{out}(\rho_{j})@output"$
or
$"{Cm}\mspace{-3.0mu}\operatorname{-delay}(\rho_{i},\rho_{j})@delay">Dm^{2}$.
By Lemma 5 we can find pumped versions of the ”runs” $\rho_{0},\dots,\rho_{k}$
that have all the same ”input” but have pairwise different ”outputs”, and thus
$T$ is not ”$k$-valued”. ∎

######  Proposition 3.

For all $k\in\mathbb{N}$, every ”$k$-ambiguous” ”SST” can be decomposed into a
union of $k$ ”unambiguous” ”SSTs”.

###### Proof.

The decomposition is done via a classical technique applicable to
”$k$-ambiguous” NFA and, by extension, to all variants of automata and
transducers (see [31, 38]). More precisely, decomposing a ”$k$-ambiguous” NFA
into a union of $k$ ”unambiguous” NFA is done by ordering runs
lexicographically and by letting the $i$-th NFA in the decomposition guess the
$i$-th accepting run on a given input (if it exists). Since the lexicographic
order is a regular property of pairs of runs, it is easy to track all smaller
runs. ∎

#### Proof of Theorem 1

We now have all the ingredients to prove Theorem 1, which directly follows
from Propositions 2 and 3, and the fact that ”unambiguous” ”SSTs” can be
determinized [5].

As a consequence of Theorem 1, we can now prove the correspondence between
”finite-valued” ”SSTs” and ”finite-valued” two-way transducers stated in the
introduction as the following theorem:

*

###### Proof.

If $R$ is realized by an ”SST” $T$ then we can apply Theorem 1 in order to
obtain $k$ ”unambiguous” ”SSTs” $T_{i}$, such that $T$ and the union of
$T_{1},\dots,T_{k}$ are ”equivalent”. From [2] we know that in the functional
case, ”SSTs” and two-way transducers are ”equivalent”. Thus, every $T_{i}$ can
be transformed effectively into an ”equivalent”, even deterministic, two-way
transducer. From this we obtain an ”equivalent” ”$k$-ambiguous” two-way
transducer.

For the converse we start with a ”$k$-valued” two-way transducer $T$ and first
observe that we can normalise $T$ in such a way that the crossing
sequences444A crossing sequence is a standard notion in the theory of finite-
state two-way machines [42], and is defined as the sequence of states in which
a given input position is visited by a run of the machine of accepting runs of
$T$ are bounded by a constant linear in the size of $T$. Once we work with
runs with bounded crossing sequences we can construct an ”equivalent” ”SST” in
the same way as we do for deterministic two-way transducers. The idea is that
during the run of the ”SST” the variables record the ”outputs” generated by
the pieces of runs at the left of the current input position (see e.g. [33,
16] for self-contained proofs). ∎

##  4 Finite valuedness

We characterize ”finite valuedness” of ”SSTs” by excluding certain types of
substructures. Our characterization has strong analogies with the
characterization of ”finite valuedness” for one-way transducers, where the
excluded substructures have the shape of a “W” and are therefore called _W-
patterns_ (cf. [17]).555In [17] there were also other substructures excluded,
which however can be seen as degenerate cases of ”W-patterns”.

######  Definition 2.

A ””W-pattern”” is a substructure of an ”SST” consisting of states
$q_{1},q_{2},r_{1},r_{2},r_{3}$, and some initial and final states, that are
connected by ”runs” as in the diagram

Ag$q_{1}$Ag$q_{2}$Ag$r_{1}$Ag$r_{2}$Ag$r_{3}$Ag$\begin{subarray}{c}\text{initial}\\\
\text{state}\end{subarray}$Ag$\begin{subarray}{c}\text{final}\\\
\text{state}\end{subarray}$Ag$\rho_{0}:\,u/\alpha~{}$Ag$~{}\rho_{4}:\,w/\omega$Ag$\rho^{\prime}_{1}:\,v^{\prime}/\beta^{\prime}~{}~{}$Ag$\rho^{\prime\prime}_{1}:\,v^{\prime\prime}/\beta^{\prime\prime}$Ag$~{}\rho^{\prime\prime\prime}_{1}:\,v^{\prime\prime\prime}/\beta^{\prime\prime\prime}$Ag$\rho^{\prime}_{2}:\,v^{\prime}/\gamma^{\prime}\phantom{x}$Ag$\rho^{\prime\prime}_{2}:\,v^{\prime\prime}/\gamma^{\prime\prime}$Ag$\phantom{x}\rho^{\prime\prime\prime}_{2}:\,v^{\prime\prime\prime}/\gamma^{\prime\prime\prime}$Ag$\rho^{\prime}_{3}:\,v^{\prime}/\eta^{\prime}~{}~{}$Ag$\rho^{\prime\prime}_{3}:\,v^{\prime\prime}/\eta^{\prime\prime}$Ag$~{}~{}~{}\rho^{\prime\prime\prime}_{3}:\,v^{\prime\prime\prime}/\eta^{\prime\prime\prime}$

where a notation like $\rho:u^{\prime}/\mu$ describes a run named $\rho$ that
consumes an ”input” $u^{\prime}$ and produces an ”update” $\mu$. Moreover, the
cyclic ”runs” $\rho^{\prime\prime}_{1}$, $\rho^{\prime\prime}_{2}$,
$\rho^{\prime\prime}_{3}$,
$\rho^{\prime}_{1}\rho^{\prime\prime}_{1}\rho^{\prime\prime\prime}_{1}$,
$\rho^{\prime}_{2}\rho^{\prime\prime}_{2}\rho^{\prime\prime\prime}_{2}$, and
$\rho^{\prime}_{3}\rho^{\prime\prime}_{3}\rho^{\prime\prime\prime}_{3}$ are
required to be ”loops”, namely, their ”updates” must have ”idempotent”
”skeletons”.

An important constraint of the above definition is that the small ”loops” at
states $r_{1},r_{2},r_{3}$ consume the same ”input”, i.e. $v^{\prime\prime}$,
and, similarly, the big ”loops” at $q_{1}$ and $q_{2}$, as well as the runs
from $q_{1}$ to $q_{2}$, consume the same set of ”inputs”, i.e.
$v^{\prime}\,(v^{\prime\prime})^{*}\,v^{\prime\prime\prime}$.

Given a ”W-pattern” $P$ and a positive natural number $x$, we construct the
following ”runs” by composing together copies of the ”runs” of the diagram of
Definition 2:

$\displaystyle""\operatorname{lft}\nolimits_{P}^{x}@leftrun""$
$\displaystyle~{}=~{}\rho^{\prime}_{1}(\rho^{\prime\prime}_{1})^{x}\,\rho^{\prime\prime\prime}_{1}$
$\displaystyle""\operatorname{mid}\nolimits_{P}^{x}@midrun""$
$\displaystyle~{}=~{}\rho^{\prime}_{2}\,(\rho^{\prime\prime}_{2})^{x}\,\rho^{\prime\prime\prime}_{2}$
$\displaystyle""\operatorname{rgt}\nolimits_{P}^{x}@rightrun""$
$\displaystyle~{}=~{}\rho^{\prime}_{3}\,(\rho^{\prime\prime}_{3})^{x}\,\rho^{\prime\prime\prime}_{3}.$

Similarly, given a sequence
$s=(x_{1},x_{2},\dots,x_{i-1},\underline{x_{i}},x_{i+1},\dots,x_{n})$ of
positive numbers with exactly one element underlined (we call such a sequence
a ””marked sequence””), we define the ”accepting” ”run”

$\displaystyle""\operatorname{run}\nolimits_{P}({s})@W-run""~{}=~{}$
$\displaystyle\hfill\rho_{0}~{}~{}\underbrace{"\operatorname{lft}\nolimits_{P}^{x_{1}}@leftrun"~{}"\operatorname{lft}\nolimits_{P}^{x_{2}}@leftrun"~{}\ldots~{}"\operatorname{lft}\nolimits_{P}^{x_{i-1}}@leftrun"}_{\text{loops
at
$q_{1}$}}~{}~{}"\operatorname{mid}\nolimits_{P}^{x_{i}}@midrun"~{}~{}\underbrace{"\operatorname{rgt}\nolimits_{P}^{x_{i+1}}@rightrun"~{}"\operatorname{rgt}\nolimits_{P}^{x_{i+2}}@rightrun"~{}\ldots~{}"\operatorname{rgt}\nolimits_{P}^{x_{n}}@rightrun"}_{\text{loops
at $q_{2}$}}~{}~{}\rho_{4}.$

For each ”marked sequence”
$s=(x_{1},\dots,x_{i-1},\underline{x_{i}},x_{i+1},\dots,x_{n})$,
$"\operatorname{run}\nolimits_{P}({s})@W-run"$ consumes the ”input”
$u\,v^{\prime}(v^{\prime\prime})^{x_{1}}v^{\prime\prime\prime}\,\dots\,v^{\prime}(v^{\prime\prime})^{x_{n}}v^{\prime\prime\prime}\,w$
and produces an ”output” of the form

$\displaystyle"\operatorname{out}("\operatorname{run}\nolimits_{P}({s})@W-run")@output"~{}=~{}\big{(}"\iota@initialupdate"\,\alpha{}$
$\displaystyle\beta^{\prime}(\beta^{\prime\prime})^{x_{1}}\beta^{\prime\prime\prime}\,\dots\,\beta^{\prime}(\beta^{\prime\prime})^{x_{i-1}}\beta^{\prime\prime\prime}\,~{}$
$\displaystyle\gamma^{\prime}(\gamma^{\prime\prime})^{x_{i}}\gamma^{\prime\prime\prime}\,~{}$
$\displaystyle\eta^{\prime}(\eta^{\prime\prime})^{x_{i+1}}\eta^{\prime\prime\prime}\,\dots\,\eta^{\prime}(\eta^{\prime\prime})^{x_{n}}\eta^{\prime\prime\prime}~{}\omega\,\omega^{\prime}\big{)}(X_{1})$

where $"\iota@initialupdate"$ is the ”initial@@update” ”update” and
$\omega^{\prime}$ is the ”final@@update” ”update” determined by the final
state of $"\operatorname{run}\nolimits_{P}({s})@W-run"$. Note that,
differently from the output, the ”input” only depends on the [marked
sequence]unmarked sequence, and thus a ”W-pattern” can have ”accepting” ”runs”
that consume the same ”input” and produce arbitrarily many different
”outputs”. As an example, consider a ”W-pattern” as in Definition 2, where
$\gamma^{\prime\prime}$ is the only update that produces output symbols – say
$\gamma^{\prime\prime}$ appends letter $c$ to the right of the unique
variable. Further suppose that $u=w=\varepsilon$,
$v^{\prime}=v^{\prime\prime\prime}=a$, and $v^{\prime\prime}=b$. So, on
”input” $(aba)\,(ab^{2}a)\,\dots\,(ab^{n}a)$, this ”W-pattern” produces $n$
different ”outputs”: $c$, $c^{2}$, …, $c^{n}$. The definition and the lemma
below generalize this example.

######  Definition 3.

A ”W-pattern” $P$ is called ””divergent”” if there exists a $5$-tuple of
numbers $n_{1},n_{2},n_{3},n_{4},n_{5}\in\mathbb{N}_{+}$ for which the two
”runs”
$"\operatorname{run}\nolimits_{P}({(n_{1},n_{2},n_{3},\underline{n_{4}},n_{5})})@W-run"$
and
$"\operatorname{run}\nolimits_{P}({(n_{1},\underline{n_{2}},n_{3},n_{4},n_{5})})@W-run"$
produce different outputs (remark that the ”runs” consume the same ”input”).
It is called ””simply divergent”” if in addition
$n_{1},n_{2},n_{3},n_{4},n_{5}\in\\{1,2\\}$.

######  Theorem 9.

An ”SST” is ”finite-valued” iff it does not admit a ”simply divergent”
”W-pattern”.

The two implications of the theorem are shown in Sections 4.2 and 4.3;
effectiveness of the characterization is shown in the next section.

###  4.1 Effectiveness of finite valuedness

We prove that the characterization of ”finite valuedness” in terms of absence
of ”simply divergent” ”W-patterns” (Theorem 9) is effective, and yields a
PSpace decision procedure. We also prove that the ”equivalence problem” for
”deterministic” ”SSTs”, known to be in PSpace, is polynomially reducible to
the ”finite valuedness” problem. Despite recent efforts by the community to
better understand the complexity of the ”equivalence problem”, it is unknown
whether the PSpace upper bound for ”equivalence” (and hence for ”finite
valuedness”) can be improved, as no non-trivial lower bound is known. On the
other hand, ”equivalence” (as well as ”finite valuedness”) turns out to be in
PTime when the number of variables is fixed [5].

The effectiveness procedure uses the following complexity result on the
composition of deterministic ”SSTs”, which is of independent interest. It is
known that deterministic ”SSTs” are closed under composition because of their
equivalence to MSO transductions [2]. A precise complexity analysis of this
closure property can be found in [6], but it is triply exponential. We show
how to do composition with a single exponential, using results from [15].

######  Proposition 4.

Let $T_{1}$ and $T_{2}$ be two ”deterministic” ”SSTs” realizing the functions
$f_{1}:\Sigma_{1}^{*}\rightarrow\Sigma_{2}^{*}$ and
$f_{2}:\Sigma_{2}^{*}\rightarrow\Sigma_{3}^{*}$. Let $n_{i}$ (resp. $m_{i}$)
be the number of states (resp. variables) of $T_{i}$, and
$M=n_{1}+n_{2}+m_{1}+m_{2}$ One can construct in time exponential in $M$ and
polynomial in $|\Sigma_{1}|+|\Sigma_{2}|+|\Sigma_{3}|$ a ”deterministic” ”SST”
realizing $f_{1}\circ f_{2}$, with exponentially many states and polynomially
many variables in $M$.

###### Proof.

Each $T_{i}$ can be converted in polynomial time into an ”equivalent” two-way
transducer that is ””reversible””, namely, both deterministic and co-
deterministic [15]. Again by [15], reversible two-way transducers can be
composed in polynomial time, yielding a reversible two-way transducer $S$
realizing $f_{1}\circ f_{2}$, and having polynomially many states in $M$.
Finally, it suffices to convert $S$ back to a ”deterministic” ”SST”, which can
be done in time exponential in the number of states of $S$ and polynomial in
the size of the alphabets. This yields a ”deterministic” ”SST” with
exponentially many states and polynomially many variables in $M$ (see e.g.
[33, 16]). ∎

*

###### Proof.

We start with an overview of the proof. By Theorem 9, it suffices to decide
whether a given ”SST” $T$ admits a ”simply divergent” ”W-pattern”. Let us fix
some tuple $\overline{x}=(x_{1},\dots,x_{5})\in\\{1,2\\}^{5}$. We construct an
”SST” $T_{\overline{x}}$ which is _not_ ”single-valued” iff $T$ has a
”W-pattern” which is ”simply divergent” for $\overline{x}$. Since checking
”single-valuedness” of ”SST” is decidable [5], we can decide ”finite
valuedness” of $T$ by solving ”single-valuedness” problems for all ”SST”
$T_{\overline{x}}$, for all tuples $\overline{x}\in\\{1,2\\}^{5}$.
Intuitively, we exhibit an encoding of ”W-patterns” $P$ as words $u_{P}$, and
show that such words form a regular language. The encoding $u_{P}$ informally
consists of the ”runs” that form the ”W-pattern” $P$, and some of these ”runs”
are overlapped to ensure that they are on the same ”input”. Accordingly, the
”SST” $T_{\overline{x}}$ will take as ”input” such an encoding $u_{P}$ and
produce as ”outputs” the two words
$"\operatorname{out}("\operatorname{run}\nolimits_{P}({s})@W-run")@output"$
and
$"\operatorname{out}("\operatorname{run}\nolimits_{P}({s^{\prime}})@W-run")@output"$,
where $s=(x_{1},x_{2},x_{3},\underline{x_{4}},x_{5})$ and
$s^{\prime}=(x_{1},\underline{x_{2}},x_{3},x_{4},x_{5})$. To achieve this,
$T_{\overline{x}}$ can consume the ”input” $u_{P}$ while iterating the encoded
”runs” as prescribed by $s$ or $s^{\prime}$ and simulating the transitions to
construct the appropriate outputs. Finally, an analysis of the size of
$T_{\overline{x}}$ and of the algorithm from [5] for checking ”single-
valuedness” gives the PSpace upper bound.

#### Detailed reduction

We now explain in detail the reduction to the ”single-valuedness” problem. We
will then show how to derive the PSpace upper bound by inspecting the
decidability proof for ”single-valuedness”.

Let
$T=(\Sigma,\mathcal{X},Q,Q_{\mathrm{init}},Q_{\mathrm{final}},\Omega,\Delta)$
be the given ”SST” and let $\mathcal{P}$ be the set of all ”W-patterns” of
$T$. We first show that $\mathcal{P}$ is a regular set, modulo some well-
chosen encodings of ”W-patterns” as words. Recall that a ”W-pattern” consists
of a tuple of runs
$P=(\rho_{0},\rho^{\prime}_{1},\rho^{\prime\prime}_{1},\rho^{\prime\prime\prime}_{1},\rho^{\prime}_{2},\rho^{\prime\prime}_{2},\rho^{\prime\prime\prime}_{2},\rho^{\prime}_{3},\rho^{\prime\prime}_{3},\rho^{\prime\prime\prime}_{3},\rho_{4})$,
connected as in the diagram of Definition 2. Note that some of those runs
share a common ”input” (e.g.
$\rho^{\prime\prime}_{1},\rho^{\prime\prime}_{2},\rho^{\prime\prime}_{3}$
share the ”input” $v^{\prime\prime}$). Therefore, we cannot simply encode $P$
as a the sequence of ”runs” $\rho_{0},\rho^{\prime}_{1},\dots$, as otherwise
regularity would be lost. Instead, in the encoding we overlap groups of ”runs”
over the same ”input”, precisely, the group
$\\{\rho^{\prime}_{1},\rho^{\prime}_{2},\rho^{\prime}_{3}\\}$ on ”input”
$v^{\prime}$, the group
$\\{\rho^{\prime\prime}_{1},\rho^{\prime\prime}_{2},\rho^{\prime\prime}_{3}\\}$
on ”input” $v^{\prime\prime}$, and the group
$\\{\rho^{\prime\prime\prime}_{1},\rho^{\prime\prime\prime}_{2},\rho^{\prime\prime\prime}_{3}\\}$
on ”input” $v^{\prime\prime\prime}$. Formally, this is done by taking the
”convolution” of the ”runs” in each group, which results in a word over the
alphabet $\Delta^{3}$. Accordingly, $P$ is encoded as the word

$u_{P}~{}=~{}\rho_{0}\>\\#\>(\rho^{\prime}_{1}\mathbin{"\otimes@convolution"}\rho^{\prime}_{2}\mathbin{"\otimes@convolution"}\rho^{\prime}_{3})\>\\#\>(\rho^{\prime\prime}_{1}\mathbin{"\otimes@convolution"}\rho^{\prime\prime}_{2}\mathbin{"\otimes@convolution"}\rho^{\prime\prime}_{3})\>\\#\>(\rho^{\prime\prime\prime}_{1}\mathbin{"\otimes@convolution"}\rho^{\prime\prime\prime}_{2}\mathbin{"\otimes@convolution"}\rho^{\prime\prime\prime}_{3})\>\\#\>\rho_{4}$

where $\\#$ is a fresh separator. The language $L_{\mathcal{P}}=\\{u_{P}\mid
P\in\mathcal{P}\\}$, consisting of all encodings of ”W-patterns”, is easily
seen to be regular, recognizable by some automaton $A_{\mathcal{P}}$ which
checks that runs forming each ”convolution” share the same ”input” and verify
”skeleton idempotency” (recall that ”skeletons” form a finite monoid). The
number of states of the automaton $A_{\mathcal{P}}$ turns out to be polynomial
in the number of states of $T$ and in the size of the ”skeleton monoid”, which
in turn is exponential in the number of variables.

Next, we construct the ”SST” $T_{\overline{x}}$ as the disjoint union of two
deterministic ”SSTs” $T_{s}$ and $T_{s^{\prime}}$, where
$s=(x_{1},x_{2},x_{3},\underline{x_{4}},x_{5})$ and
$s^{\prime}=(x_{1},\underline{x_{2}},x_{3},x_{4},x_{5})$. We only describe
$T_{s}$, as the construction of $T_{s^{\prime}}$ is similar. The ”SST” $T_{s}$
is obtained as a suitable restriction of the composition of two
”deterministic” ”SSTs” $T_{\mathrm{iter}}^{s}$ and $T_{\mathrm{exec}}$, which
respectively iterate the ”runs” as prescribed by $s$ and execute the
transitions read as ”input”. When fed with the encoding $u_{P}$ of a
”W-pattern”, $T_{\mathrm{iter}}^{s}$ needs to output
$"\operatorname{run}\nolimits_{P}({s})@W-run"\in\Delta^{*}$. More precisely,
it takes as ”input” a word of the form
$\rho_{0}\>\\#\>(\rho^{\prime}_{1}\mathbin{"\otimes@convolution"}\rho^{\prime}_{2}\mathbin{"\otimes@convolution"}\rho^{\prime}_{3})\>\\#\>(\rho^{\prime\prime}_{1}\mathbin{"\otimes@convolution"}\rho^{\prime\prime}_{2}\mathbin{"\otimes@convolution"}\rho^{\prime\prime}_{3})\>\\#\>(\rho^{\prime\prime\prime}_{1}\mathbin{"\otimes@convolution"}\rho^{\prime\prime\prime}_{2}\mathbin{"\otimes@convolution"}\rho^{\prime\prime\prime}_{3})\>\\#\>\rho_{4}$
and produces as ”output”

$\displaystyle\rho_{0}{}{}$
$\displaystyle\rho^{\prime}_{1}\,(\rho^{\prime\prime}_{1})^{x_{1}}\,\rho^{\prime\prime\prime}_{1}~{}~{}\rho^{\prime}_{1}\,(\rho^{\prime\prime}_{1})^{x_{2}}\,\rho^{\prime\prime\prime}_{1}~{}~{}\rho^{\prime}_{1}\,(\rho^{\prime\prime}_{1})^{x_{3}}\,\rho^{\prime\prime\prime}_{1}~{}~{}$
$\displaystyle\rho^{\prime}_{2}\,(\rho^{\prime\prime}_{2})^{x_{4}}\,\rho^{\prime\prime\prime}_{2}~{}~{}$
$\displaystyle\rho^{\prime}_{3}\,(\rho^{\prime\prime}_{3})^{x_{5}}\,\rho^{\prime\prime\prime}_{3}~{}~{}\rho_{4}.$

The SST $T_{\mathrm{iter}}^{s}$ uses one variable for each non-iterated run
(e.g. for $\rho_{0}$ and $\rho^{\prime}_{1}$), $x_{1}+x_{2}+x_{3}$ variables
to store copies of $\rho^{\prime\prime}_{1}$, $x_{4}$ variables to store
copies of $\rho^{\prime\prime}_{2}$, and $x_{5}$ variables to store copies of
$\rho^{\prime\prime}_{3}$, and eventually outputs the concatenation of all
these variables to obtain $"\operatorname{run}\nolimits_{P}({s})@W-run"$. Note
that $T_{\mathrm{iter}}^{s}$ does not need to check that the ”input” is a
well-formed encoding, so the number of its states and variables is bounded by
a constant; on the other hand, the input alphabet, consisting of transitions
of $T$, is polynomial in the size of $T$.

The construction of $T_{\mathrm{exec}}$ is straightforward: it just executes
the transitions it reads along the ”input”, thus simulating a run of $T$.
Hence $T_{\mathrm{exec}}$ has a single state and the same number of variables
as $T$. Its alphabet is linear in the size of $T$.

Now, $T_{s}$ is obtained from the composition $T_{\mathrm{exec}}\circ
T_{\mathrm{iter}}^{s}$ by restricting the ”input” domain to $\mathcal{P}$. It
is well-known that ”deterministic” ”SST” are closed under composition and
regular domain restriction [2]. By the above constructions, we have

$T_{\bar{x}}(u_{P})~{}=~{}T_{s}(u_{P})~{}\cup~{}T_{s^{\prime}}(u_{P})~{}=~{}"\operatorname{out}("\operatorname{run}\nolimits_{P}({s})@W-run")@output"~{}\cup~{}"\operatorname{out}("\operatorname{run}\nolimits_{P}({s^{\prime}})@W-run")@output"$

and hence $T$ contains a ”W-pattern” that is ”simply divergent” for $\bar{x}$
iff $T_{\bar{x}}$ is not ”single-valued”. This already implies the
decidability of the existence of a ”simply divergent” ”W-pattern” in $T$, and
hence by Theorem 9, of ”finite valuedness”.

#### Complexity analysis

Let us now analyse the complexity in detail. This requires first estimating
the size of $T_{\bar{x}}$. Let $n_{T}$ resp. $m_{T}$ be the number of states
of $T$, resp. its number of variables. From the previous bounds on the sizes
of $T_{\mathrm{exec}}$ and $T^{s}_{\mathrm{iter}}$ and Proposition 4, we
derive that the number of states and variables of $T_{\mathrm{exec}}\circ
T^{s}_{\mathrm{iter}}$ is polynomial in both $n_{T}$ and $m_{T}$. Further,
restricting the domain to $\mathcal{P}$ is done via a product with the
automaton $A_{\mathcal{P}}$, whose size is polynomial in $n_{T}$ and
exponential in $m_{T}$. Summing up, the number of states of $T_{s}$ is
exponential in $m_{T}$, and polynomial in $n_{T}$. Its number of variables is
polynomial in both $n_{T}$ and $m_{T}$. And so do $T_{s^{\prime}}$ and
$T_{\bar{x}}$.

As explained in [5], checking ”single-valuedness” of ”SST” reduces to checking
non-emptiness of a 1-reversal 2-counter machine of size exponential in the
number of variables and polynomial in the number of states. This is fortunate,
since it allows us to conclude that checking ”single-valuedness” of
$T_{\bar{x}}$ reduces to checking non-emptiness of a 1-reversal 2-counter
machine of size just exponential in the number of variables of $T$. The PSpace
upper bound (and the PTime upper bound for a fixed number of variables) now
follow by recalling that non-emptiness of bounded reversal counter machines is
in NLogSpace [25].

#### Lower bound

For the lower bound, consider two ”deterministic” ”SST” $T_{1},T_{2}$ over
some alphabet $\Sigma$ with same domain $D$. Domain equivalence can be tested
in PTime because $T_{1},T_{2}$ are ”deterministic”. Consider a fresh symbol
$\\#\not\in\Sigma$, and the relation

$R~{}=~{}\Big{\\{}\big{(}u_{1}\\#\dots\\#u_{n},\>T_{i_{1}}(u_{1})\\#\dots\\#T_{i_{n}}(u_{n})\big{)}~{}\Big{|}~{}\begin{smallmatrix}u_{i}\in
D,~{}n\in\mathbb{N},\\\
i_{1},\dots,i_{n}\in\\{1,2\\}\end{smallmatrix}\Big{\\}}$

It is easily seen that $R$ is realizable by a (non-deterministic) ”SST”. We
claim that $R$ is ”finite-valued” iff it is ”single-valued”, iff $T_{1}$ and
$T_{2}$ are ”equivalent”. If $T_{1}$ and $T_{2}$ are ”equivalent”, then
$T_{1}(u_{j})=T_{2}(u_{j})$ for all $1\leq j\leq n$, hence $R$ is ”single-
valued”, and so ”finite-valued”. Conversely, if $T_{1}$ and $T_{2}$ are not
”equivalent”, then $T_{1}(u)\neq T_{2}(u)$ for some $u\in D$, and the family
of ”inputs” $(u\\#)^{n}\,u$, with $n\in\mathbb{N}$, witnesses the fact that
$R$ is not ”finite-valued”. ∎

As a corollary, we obtain an alternative proof of the following known result
that was recalled in the introduction:

*

###### Proof.

Observe that a necessary condition for a two-way transducer to be finite-
valued is that crossing sequences are bounded. More precisely, if a crossing
sequence has a loop then the output of the loop must be empty, otherwise the
transducer is not finite valued. Given a bound on the length of crossing
sequences the standard conversion into an equivalent ”SST” applies, see e.g.
[33, 16]. This yields an SST with an exponential number of states and a linear
number of variables, both in the number of states of the initial two-way
transducer. Finally, we apply the algorithm of Theorem 4, and we observe that
it amounts to checking emptiness of a $1$-reversal $2$-counter machine whose
number of states is exponential in the number of states of the initial two-way
transducer. We again conclude by using the NLogSpace algorithm for checking
emptiness of such counter machines [25]. ∎

###  4.2 A necessary condition for finite valuedness

Here we prove the contrapositive of the left-to-right implication of Theorem
9: we show that in a ”divergent” ”W-pattern” there exist arbitrarily many
”outputs” produced by the same ”input”.

######  Lemma 6.

Every ”SST” that contains some ”divergent” ”W-pattern” is not ”finite-valued”.

###### Proof.

Let us fix an ”SST” with a ”divergent” ”W-pattern” $P$. In order to prove that
the ”SST” is not ”finite-valued”, we show that we can construct arbitrary
numbers of ”accepting” ”runs” of $P$ that consume the same ”input” and produce
pairwise different ”outputs”. To do this we will consider for some suitable
$M\in\mathbb{N}$ ”inequalities” in the formal parameters
$\mathtt{s}_{1},\ldots,\mathtt{s}_{M}$ (where $1\leq i<j\leq M$), and look for
arbitrary large, ”satisfiable”, subsets of such ”inequalities”:

$\displaystyle
e_{M,i,j}[\mathtt{s}_{1},\mathtt{s}_{2},\ldots,\mathtt{s}_{M}]:$
$\displaystyle\qquad\left.\begin{array}[]{ccc}&"\operatorname{out}("\operatorname{run}\nolimits_{P}({\mathtt{s}_{1},\mathtt{s}_{2},\ldots,\mathtt{s}_{i-1},\underline{\mathtt{s}_{i}},\mathtt{s}_{i+1},\ldots,\mathtt{s}_{M}})@W-run")@output"\\\
&\neq\\\
&"\operatorname{out}("\operatorname{run}\nolimits_{P}({\mathtt{s}_{1},\mathtt{s}_{2},\ldots,\mathtt{s}_{j-1},\underline{\mathtt{s}_{j}},\mathtt{s}_{j+1},\ldots,\mathtt{s}_{M}}<EMAIL_ADDRESS>
Recall that, according to the diagram of Definition 2, the number of variable
occurrences before (resp. after) the underlined parameter represents the
number of ”loops” at state $q_{1}$ (resp. $q_{2}$) in a ”run” of the
”W-pattern”. Moreover, each variable $\mathtt{s}_{i}$ before (resp. after) the
underlined parameter represents the number of repetitions of the ”loop” at
$r_{1}$ (resp. $r_{3}$) within occurrences of bigger ”loops” at $q_{1}$ (resp.
$q_{2}$); similarly, the underlined variable represents the number of
repetitions of the ”loop” at $r_{2}$ within the ”run” that connects $q_{1}$ to
$q_{2}$. In view of this, by Corollary 2, the ”outputs” of the ”runs”
considered in the above inequality have the format required for a ”word
inequality” with repetitions parametrized by
$\mathtt{s}_{1},\ldots,\mathtt{s}_{M}$.

The fact that the ”W-pattern” $P$ is ”divergent” allows to find sets of
”satisfiable” ”inequalities” $e_{M,i,j}$ of arbitrary large cardinality. This
in turn will yield together with our word combinatorics results, arbitrary
numbers of ”accepting” ”runs” over the same ”input” and with pairwise
different ”outputs”.

######  Claim.

For every $m\in\mathbb{N}$, there exist $M\in\mathbb{N}$ and a set
$I\subseteq\\{1,2,\ldots,M\\}$ of cardinality $m+1$ such that, for all $i<j\in
I$, $e_{M,i,j}$ is ”satisfiable”.

###### Proof of the claim.

Since $P$ is a ”divergent” ”W-pattern”, there exist
$n_{1},n_{2},n_{3},n_{4},n_{5}\in\mathbb{N}_{+}$ such that

$"\operatorname{out}("\operatorname{run}\nolimits_{P}({n_{1},\underline{n_{2}},n_{3},n_{4},n_{5}})@W-run")@output"~{}\neq~{}"\operatorname{out}("\operatorname{run}\nolimits_{P}({n_{1},n_{2},n_{3},\underline{n_{4}},n_{5}}<EMAIL_ADDRESS>
We fix such numbers $n_{1},n_{2},n_{3},n_{4},n_{5}\in\mathbb{N}_{+}$. Consider
now the following ”inequality” over the formal parameters
$\mathtt{x},\mathtt{y},\mathtt{z}$:

$\displaystyle e[\mathtt{x},\mathtt{y},\mathtt{z}]:$
$\displaystyle\quad\left.\begin{array}[]{ccc}&"\operatorname{out}("\operatorname{run}\nolimits_{P}({\overbrace{n_{1},n_{1},\ldots,n_{1}}^{\mathtt{x}\textup{
times}},\>\underline{n_{2}},\>\overbrace{n_{3},\ldots,n_{3}}^{\mathtt{y}\textup{
times}},\>n_{4},\>\overbrace{n_{5},\ldots,n_{5}}^{\mathtt{z}\textup{
times}}}<EMAIL_ADDRESS>&\neq\\\
&"\operatorname{out}("\operatorname{run}\nolimits_{P}({\underbrace{n_{1},n_{1},\ldots,n_{1}}_{\mathtt{x}\textup{
times}},\>n_{2},\>\underbrace{n_{3},\ldots,n_{3}}_{\mathtt{y}\textup{
times}},\>\underline{n_{4}},\>\underbrace{n_{5},\ldots,n_{5}}_{\mathtt{z}\textup{
times}}}<EMAIL_ADDRESS>
Note that every instance of $e[\mathtt{x},\mathtt{y},\mathtt{z}]$ with
concrete values $x,y,z$ is also an instance of $e_{M,i,j}$, where $M=x+y+z+2$,
$i=x+1$, $j=x+y+2$, and all parameters $\mathtt{s}_{1},\ldots,\mathtt{s}_{M}$
are instantiated with values from $\\{n_{1},\ldots,n_{5}\\}$. Moreover, as the
parameters in $e[\mathtt{x},\mathtt{y},\mathtt{z}]$ determine the number of
repetitions of $n_{1},n_{3},n_{5}$, which in their turn correspond to
”pumping” ”loops” at $q_{1}$ and $q_{2}$, by Corollary 2, the ”outputs” of the
considered ”runs” have the format required for a ”word inequality” with
repetitions parametrized by $\mathtt{x},\mathtt{y},\mathtt{z}$.

Since $e[\mathtt{x},\mathtt{y},\mathtt{z}]$ is ”satisfiable” (e.g. with
$\mathtt{x}=\mathtt{y}=\mathtt{z}=1$), Corollary 4 implies that

$\displaystyle\exists\ell_{\mathtt{y}}~{}\forall
h_{\mathtt{y}}~{}\exists\ell_{\mathtt{x}}~{}\forall
h_{\mathtt{x}}~{}\exists\ell_{\mathtt{z}}~{}\forall h_{\mathtt{z}}$
$\displaystyle\qquad\quad\underbrace{[\ell_{\mathtt{x}},h_{\mathtt{x}}]}_{\text{values
for
}\mathtt{x}}\times\underbrace{[\ell_{\mathtt{y}},h_{\mathtt{y}}]}_{\text{values
for
}\mathtt{y}}\times\underbrace{[\ell_{\mathtt{z}},h_{\mathtt{z}}]}_{\text{values
for<EMAIL_ADDRESS>
Note that we start by quantifying over $\ell_{y}$ and not $\ell_{x}$
(Corollary 4 is invariant with respect to the parameter order)666The reader
may compare this with the example given before Def. 3.. This particular order
ensures that for every $m\in\mathbb{N}$ there exist three integers
$\ell_{y},\ell_{x},\ell_{z}>0$ such that

<EMAIL_ADDRESS>(2)

Further note that $h_{y}=2m\ell_{y}$ depends only on $\ell_{y}$, while
$h_{x}=\ell_{x}+2m\ell_{y}$ depends on both $\ell_{x}$ and $\ell_{y}$.

We can now prove the claim by letting
$M=\ell_{\mathtt{x}}+2m\ell_{\mathtt{y}}+\ell_{\mathtt{z}}+1$ and
$I=\\{\ell_{\mathtt{x}}+2\lambda\ell_{\mathtt{y}}+1\mid 0\leq\lambda\leq
m\\}$. Indeed, the gap between two consecutive values of $I$ equals
$2\ell_{y}$, and for every $i<j\in I$ we get

$\begin{array}[]{lllll}i-1&\in&[\ell_{\mathtt{x}},\ell_{\mathtt{x}}+2(m-1)\ell_{\mathtt{y}}]&\subseteq&[\ell_{\mathtt{x}},\ell_{\mathtt{x}}+2m\ell_{\mathtt{y}}]\\\
j-i-1&\in&[2\ell_{\mathtt{y}}-1,2m\ell_{\mathtt{y}}-1]&\subseteq&[\ell_{\mathtt{y}},2m\ell_{\mathtt{y}}]\\\
M-j&\in&[\ell_{\mathtt{z}},\ell_{\mathtt{z}}+2(m-1)\ell_{\mathtt{y}}]&\subseteq&[\ell_{\mathtt{z}},\ell_{\mathtt{z}}+2m\ell_{\mathtt{y}}].\end{array}$

Thus, by Equation (2), $(i-1,j-i-1,M-j)\in"\operatorname{Sols}(e)@solutions"$.
This ”solution” of $e$ corresponds to the instance of $e_{M,i,j}$ with the
values for the formal parameters $\mathtt{s}_{1},\dots,\mathtt{s}_{M}$ defined
by

$\mathtt{s}_{h}=\left\\{\begin{array}[]{lll}n_{1}&\textup{ for every }1\leq
h\leq i-1,\\\ n_{2}&\textup{ for }h=i,\\\ n_{3}&\textup{ for every }i+1\leq
h\leq j-1,\\\ n_{4}&\textup{ for }h=j,\\\ n_{5}&\textup{ for every }j+1\leq
M.\end{array}\right.$

Hence, $e_{M,i,j}$ is ”satisfiable” for all $i<j\in I$, as claimed. ∎

We can now conclude the proof of the lemma using the above claim: Corollary 3
tells us that any ”system” of ”word inequalities” is ”satisfiable” when every
”word inequality” in it is so. Using this and the above claim, we derive that
for every $m$ there exist $t_{1},t_{2},\ldots,t_{M}\in\mathbb{N}_{+}$ such
that, for all $i<j\in I$ (with $I$ as in the claim),
$e_{M,i,j}[t_{1},t_{2},\ldots,t_{M}]$ holds. For every $h\in I$, let

<EMAIL_ADDRESS>
Note that all runs $\rho_{h}$, for $h\in I$, consume the same ”input”, since
they all correspond to the same unmarked sequence
$(t_{1},t_{2},\ldots,t_{M})$. However, they produce pairwise different
”outputs”, because for every $i<j\in I$, the tuple
$(t_{1},t_{2},\ldots,t_{M})$ is a ”solution” of $e_{M,i,j}$. Since $|I|=m$ can
be chosen arbitrarily, the transducer is not finitely valued. ∎

###  4.3 A sufficient condition for finite valuedness

We finally prove that an ”SST” with no ”simply divergent” ”W-pattern” is
”finite-valued”. The proof relies on two crucial results.

The first result is a characterizastion of ”finite ambiguity” for ”SSTs”,
which is easily derived from a prior characterization of ”finite ambiguity”
for finite state automata [34, 29, 45]:

######  Definition 4.

A ””dumbbell”” is a substructure of an ”SST” consisting of states
$q_{1},q_{2}$ connected by ”runs” as in the diagram

Ag$q_{1}$Ag$q_{2}$Ag$\begin{subarray}{c}\text{initial}\\\
\text{state}\end{subarray}$Ag$\begin{subarray}{c}\text{final}\\\
\text{state}\end{subarray}$Ag$\rho_{0}:~{}u/\alpha~{}$Ag$~{}\rho_{4}:~{}w/\omega$Ag$\rho_{1}:~{}v/\beta$Ag$\rho_{2}:~{}v/\gamma$Ag$\rho_{3}:~{}v/\eta$

where the ”runs” $\rho_{1}$ and $\rho_{3}$ are ”loops” (in particular, they
produce ”updates” with ”idempotent” ”skeletons”) and at least two among the
runs $\rho_{1},\rho_{2},\rho_{3}$ that consume the same ”input” $v$ are
distinct.

######  Lemma 7.

An ”SST” is ”finitely ambiguous” iff it does not contain any ”dumbbell”.

###### Proof.

Let
$T=(\Sigma,\mathcal{X},Q,Q_{\mathrm{init}},Q_{\mathrm{final}},\Omega,\Delta)$
be an ”SST”. By projecting away the ”updates” on the transitions we obtain
from $T$ a ””multiset finite state automaton”” $A$. Formally,
$A=(\Sigma,Q_{\mathrm{init}},Q_{\mathrm{final}},\Delta^{\prime})$, where
$\Delta^{\prime}$ is the _multiset_ containing one occurrence of a triple
$(q,a,q^{\prime})$ for each transition of the form $(q,a,\alpha,q^{\prime})$
in $\Delta$. Note that a ”multiset automaton” can admit several occurrences of
the same (”accepting”) ”run”. Accordingly, the notion of ”finite ambiguity”
for $A$ requires the existence of a uniform bound to the number of
_occurrences_ of ”accepting” ”runs” of $A$ on the same ”input”. We also remark
that ”multiset automata” are essentially the same as weighted automata over
the semiring of natural numbers (the weight of a transition being its number
of occurrences), with only a difference in terminology where ”finite
ambiguity” in ”multiset automata” corresponds to ”finite valuedness” in
weighted automata.

Given the above construction of $A$ from $T$, one can verify by induction on
$|u|$ that the number of occurrences of ”accepting” ”runs” of $A$ on $u$
coincides with the number of ”accepting” ”runs” of $T$ on $u$. This means that
$A$ is ”finitely ambiguous” iff $T$ is ”finitely ambiguous”.

Finally, we recall the characterizations of ”finite ambiguity” from [34, 29,
45] (see in particular Theorem 1.1 and Lemma 2.6 from [34]). For short, their
results directly imply that a ”multiset automaton” is ”finitely ambiguous” iff
it does not contain a ””plain dumbbell””, namely, a substructure of the form

Ag$q_{1}$Ag$q_{2}$Ag$\begin{subarray}{c}\text{initial}\\\
\text{state}\end{subarray}$Ag$\begin{subarray}{c}\text{final}\\\
\text{state}\end{subarray}$Ag$\rho^{\prime}_{0}:~{}u~{}$Ag$~{}\rho^{\prime}_{4}:~{}w$Ag$\rho^{\prime}_{1}:~{}v$Ag$\rho^{\prime}_{2}:~{}v$Ag$\rho^{\prime}_{3}:~{}v$

where at least two among
$\rho^{\prime}_{1},\rho^{\prime}_{2},\rho^{\prime}_{3}$ are distinct ”runs”.

This almost concludes the proof of the lemma, since any ”dumbbell” of $T$ can
be projected into a ”plain dumbbell” of $A$. The converse implication,
however, is not completely straightforward. The reason is that the cyclic
”runs” of a ”plain dumbbell” in $A$ do not necessarily correspond to ”loops”
in the ”SST” $T$, as the ”runs” need not produce ”updates” with ”idempotent”
”skeletons”. Nonetheless, we can reason as follows. Suppose that $A$ contains
a ”plain dumbbell”, with occurrences of ”runs”
$\rho^{\prime}_{0},\rho^{\prime}_{1},\rho^{\prime}_{2},\rho^{\prime}_{3},\rho^{\prime}_{4}$
as depicted above. Let $\rho_{0},\rho_{1},\rho_{2},\rho_{3},\rho_{4}$ be the
corresponding ”runs” in $T$, and let $\alpha,\beta,\gamma,\eta,\omega$ be
their induced ”updates”. Further let $n$ be a large enough number such that
$\beta^{n}$ and $\eta^{n}$ have ”idempotent” ”skeletons” (such an $n$ always
exists since the ”skeleton monoid” is finite). Now consider the substructure
in $T$ given by the ”runs” $\rho_{0}=\rho^{\prime}_{0}$,
$\rho_{1}=(\rho^{\prime}_{1})^{n}$,
$\rho_{2}=(\rho^{\prime}_{1})^{n-1}\,\rho^{\prime}_{2}$,
$\rho_{3}=(\rho^{\prime}_{3})^{n}$, and $\rho_{4}=\rho^{\prime}_{4}$. This
substructure satisfies precisely the definition of ”dumbbell” for the ”SST”
$T$. ∎

The second ingredient for the proof of the right-to-left implication of
Theorem 9 uses once more the cover construction described in Proposition 1.
More precisely, in Lemma 8 below we show that if an ”SST” $T$ has no ”simply
divergent” ”W-pattern”, then, for some well chosen values $C$, $D$, $m$, the
”SST” $\operatorname{Cover}_{Cm,Dm^{2}}(T)$ contains no ”dumbbell”. Before
proving the lemma, let us show how it can be used to establish the right-to-
left implication of Theorem 9.

#### Proof of Theorem 9

By Lemma 7, if $\operatorname{Cover}_{Cm,Dm^{2}}(T)$ has no ”dumbbell”, then
it is ”finitely ambiguous”, and hence it associates with each ”input” a
uniformly bounded number of ”outputs”. In particular,
$\operatorname{Cover}_{Cm,Dm^{2}}(T)$ is ”finite-valued”, and since it is also
”equivalent” to $T$, then $T$ is ”finite-valued” too. ∎

######  Lemma 8.

Given an SST $T$, one can compute three numbers $C$, $D$, and $m$ such that if
$\operatorname{Cover}_{Cm,Dm^{2}}(T)$ contains a ”dumbbell”, then $T$ contains
a ”simply divergent” ”W-pattern”.

###### Proof.

Intuitively, we will show that if
$"\operatorname{Cover}_{Cm,Dm^{2}}(T)@cover"$ contains a ”dumbbell”, then this
”dumbbell” must admit two distinct ”runs” $\pi,\pi^{\prime}$ that either
produce different ”outputs” or have large ”delay”. In both cases we will be
able to transform the ”dumbbell” into a ”simply divergent” ”W-pattern”. For
example, in the case of a large ”delay”, we will rely on Lemmas 4 and 1 to
identify certain ”loops” in $\pi$ and $\pi^{\prime}$ that lie entirely inside
occurrences of the ”runs” $\rho_{0},\dots,\rho_{4}$ of the ”dumbbell”, and
such that, when pumped, produce different ”outputs”. From there, we will be
able to expose a ”simply divergent” ”W-pattern” in
$"\operatorname{Cover}_{Cm,Dm^{2}}(T)@cover"$, and hence in $T$ as well.

Formally, let $T$ be an ”SST”, let $C,D$ be defined as in Lemma 4, and let
$m=7E^{H^{2}+H+1}+1$, where $E,H$ are defined as in Lemma 1. Next, suppose
that $"\operatorname{Cover}_{Cm,Dm^{2}}(T)@cover"$ contains a ”dumbbell” like
the one of Definition 4, with ”runs”
$\rho_{0},\rho_{1},\rho_{2},\rho_{3},\rho_{4}$ that produce respectively the
”updates” $\alpha,\beta,\gamma,\eta,\omega$.

Consider the following ”accepting” ”runs”, which are obtained by composing the
copies of the original ”runs” of the ”dumbbell”, and that are different
because two of $\rho_{1},\rho_{2},\rho_{3}$ have to be different:

$\displaystyle\pi$
$\displaystyle~{}=~{}\rho_{0}~{}\rho_{1}~{}\rho_{2}~{}\rho_{3}~{}\rho_{3}~{}\rho_{3}~{}\rho_{4}$
(3) $\displaystyle\pi^{\prime}$
$\displaystyle~{}=~{}\rho_{0}~{}\rho_{1}~{}\rho_{1}~{}\rho_{1}~{}\rho_{2}~{}\rho_{3}~{}\rho_{4}.$

By the properties of $"\operatorname{Cover}_{Cm,Dm^{2}}(T)@cover"$, since
$\pi$ and $\pi^{\prime}$ consume the same ”input”, they either produce
different ”outputs” or have $Cm$-”delay” larger than $Dm^{2}$.

We first consider the case where the ”outputs” are different. In this case, we
can immediately witness a ”simply divergent” ”W-pattern” $P$ by adding empty
”runs” to the ”dumbbell”; formally, for every $i=1,2,3$, we let
$\rho^{\prime}_{i}=\rho_{i}$ and
$\rho^{\prime\prime}_{i}=\rho^{\prime\prime\prime}_{i}=\varepsilon$, so as to
form a ”W-pattern” like the one in the diagram of Definition 2, but now with
$r_{1}=q_{1}$ and $r_{2}=r_{3}=q_{2}$. Using the notation introduced at the
beginning of Section 4, we observe that
$\pi="\operatorname{run}\nolimits_{P}({1,\underline{1},1,1,1})@W-run"$ and
$\pi^{\prime}="\operatorname{run}\nolimits_{P}({1,1,1,\underline{1},1})@W-run"$
— recall that the underlined number represents how many times the small ”loop”
at $r_{2}$, which is empty here, is repeated along the ”run” from $q_{1}$ to
$q_{2}$, and the other numbers represent how many times the small ”loops” at
$r_{1}$ and $r_{3}$, which are also empty here, are repeated within the
occurrences of big ”loops” at $q_{1}$ and $q_{2}$. Since, by assumption, the
”runs” $\pi$ and $\pi^{\prime}$ produce different ”outputs”, the ”W-pattern”
$P$ is ”simply divergent”, as required.

We now consider the case where $\pi$ and $\pi^{\prime}$ have large ”delay”,
namely,
$"{Cm}\mspace{-3.0mu}\operatorname{-delay}(\pi,\pi^{\prime})@delay">Dm^{2}$.
In this case Lemma 4 guarantees the existence of a set
$I\subseteq\\{0,1,\ldots,|\pi|\\}$ containing $m$ positions in between the
input letters such that, for all pairs $i<j$ in $I$, the interval $[i,j]$ is a
”loop” on both $\pi$ and $\pi^{\prime}$ and satisfies

$"\operatorname{out}("\operatorname{pump}^{2}_{[i,j]}(\pi)@pump")@output"\>\neq\>"\operatorname{out}("\operatorname{pump}^{2}_{[i,j]}(\pi^{\prime}<EMAIL_ADDRESS>(4)

Next, recall from Equation (3) that $\pi$, and similarly $\pi^{\prime}$,
consists of seven parts, representing copies of the original ”runs” of the
”dumbbell” and consuming the ”inputs” $u,v,v,v,v,v,w$. We identify these parts
with the numbers $1,\dots,7$. Since we defined $m$ as $7E^{H^{2}+H+1}+1$,
there is one of these parts in which at least $E^{H^{2}+H+1}+1$ of the
aforementioned positions of $I$ occur. Let $p\in\\{1,2,\ldots,7\\}$ denote the
number of this part, and let $I_{p}$ be a set of $E^{H^{2}+H+1}+1$ positions
from $I$ that occur entirely inside the $p$-th part. We conclude the proof by
a further case distinction, depending on whether $p\in\\{1,7\\}$ or
$p\in\\{2,\dots,6\\}$.

#### Parts $1$ and $7$

Let us suppose that $p\in\\{1,7\\}$, and let $i$ and $j$ be two distinct
positions in $I_{p}$. We let $P$ be the ”W-pattern” obtained by transforming
the ”dumbbell” as follows:

  1. 1.

First, we ”pump” either $\rho_{0}$ or $\rho_{4}$ depending on $p$:

     * •

If $p=1$, we set
$\rho_{0}^{\prime}="\operatorname{pump}^{2}_{[i,j]}(\rho_{0})@pump"$ and
$\rho_{4}^{\prime}=\rho_{4}$.

     * •

If $p=7$, we set
$\rho_{4}^{\prime}="\operatorname{pump}^{2}_{[i-|u\,v^{5}|,j-|u\,v^{5}|]}(\rho_{4})@pump"$
and $\rho_{0}^{\prime}=\rho_{0}$.

  2. 2.

Then, we add empty ”runs” to $\rho_{1}$, $\rho_{2}$, and $\rho_{3}$; formally,
for each $h\in\\{1,2,3\\}$, we set $\rho_{h}^{\prime}=\rho_{h}$ and
$\rho_{h}^{\prime\prime}=\rho_{h}^{\prime\prime\prime}=\varepsilon$.

Now that we identified a ”W-pattern” $P$ in
$"\operatorname{Cover}_{C,D}(T)@cover"$, we note that

$\displaystyle"\operatorname{pump}^{2}_{[i,j]}(\pi)@pump"$
$\displaystyle~{}=~{}"\operatorname{run}\nolimits_{P}({1,\underline{1},1,1,1})@W-run"$
$\displaystyle"\operatorname{pump}^{2}_{[i,j]}(\pi^{\prime})@pump"$
<EMAIL_ADDRESS>
We also recall Equation 4, which states that these ”runs” produce different
”outputs”. This means that the ”W-pattern” $P$ is ”simply divergent”. Finally,
since the ”runs” of $"\operatorname{Cover}_{C,D}(T)@cover"$ can be projected
into ”runs” of $T$, we conclude that $T$ contains a ”simply divergent”
”W-pattern”.

#### Parts $2-6$

Let us suppose that $p\in\\{2,\dots,6\\}$. Note that, in this case, the
elements of $I_{p}$ denote positions inside the $p$-th factor of the ”input”
$u\,v\,v\,v\,v\,v\,w$, which is a $v$. To refer directly to the positions of
$v$, we define $I^{\prime}_{p}$ as the set obtained by subtracting
$|u\,v^{p-1}|$ from each element of $I_{p}$. Since the set $|I^{\prime}_{p}|$
has cardinality $E^{H^{2}+H+1}+1$, we claim that we can find an interval with
endpoints from $I^{\prime}_{p}$ that is a ”loop” of $\rho_{1}$, $\rho_{2}$,
and $\rho_{3}$, at the same time. Specifically, we can do so via three
consecutive applications of Lemma 1:

  1. 1.

As $|I^{\prime}_{p}|=E^{H^{2}+H+1}+1=E\cdot(E^{H+1})^{H}+1$, there exists a
set $I^{\prime\prime}_{p}\subseteq I^{\prime}_{p}$ of cardinality $E^{H+1}+1$
such that for every pair $i<j$ in $I^{\prime\prime}_{p}$, the interval $[i,j]$
is a ”loop” of $\rho_{1}$;

  2. 2.

As $|I_{p}^{\prime\prime}|=E^{H+1}+1=E\cdot E^{H}+1$, there exists
$I^{\prime\prime\prime}_{p}\subseteq I^{\prime\prime}_{p}$ of cardinality
$E+1$ s.t. for every pair $i<j$ in $I^{\prime\prime\prime}_{p}$, the interval
$[i,j]$ is a ”loop” of $\rho_{2}$ (and also of $\rho_{1}$, since $i,j\in
I^{\prime\prime\prime}_{p}\subseteq I^{\prime\prime}_{p}$);

  3. 3.

As $|I^{\prime\prime\prime}_{p}|=E+1=E\cdot 1^{H}+1$, there are two positions
$i<j$ in $I^{\prime\prime\prime}_{p}$ such that the interval $[i,j]$ is a
”loop” of $\rho_{3}$ (and also of $\rho_{1}$ and $\rho_{2}$ since $i,j\in
I^{\prime\prime\prime}_{p}\subseteq I^{\prime\prime}_{p}$).

The diagram below summarizes the current situation: we have just managed to
find an interval $[i,j]$ that is a ”loop” on all $v$-labelled ”runs”
$\rho_{1},\rho_{2},\rho_{3}$ of the ”dumbbell” (the occurrences of this
interval inside $\rho_{1},\rho_{2},\rho_{3}$ are highlighted by thick
segments):

Ag$\begin{subarray}{c}\text{initial}\\\
\text{state}\end{subarray}$Ag$q_{1}$Ag$q_{2}$Ag$\begin{subarray}{c}\text{final}\\\
\text{state}\end{subarray}$Ag$\rho_{0}:~{}u/\alpha$Ag$\rho_{4}:~{}w/\omega$Ag$\rho_{1}:~{}v/\beta\phantom{xi}$AgAgAg$\phantom{x}\rho_{3}:~{}v/\eta$AgAgAg$\rho_{2}:~{}v/\gamma$AgAg

We can now expose a ”W-pattern” $P$ by merging the positions $i$ and $j$
inside each $v$-labelled ”run” $\rho_{1}$, $\rho_{2}$, and $\rho_{3}$ of the
”dumbbell”. Formally, we let $\rho^{\prime}_{0}=\rho_{0}$,
$\rho^{\prime}_{4}=\rho_{4}$, and for every $h\in\\{1,2,3\\}$, we define
$\rho^{\prime}_{h}$, $\rho^{\prime\prime}_{h}$, and
$\rho^{\prime\prime\prime}_{h}$, respectively, as the intervals $[0,i]$,
$[i,j]$, and $[j,|v|]$ of $\rho_{h}$. Now that we have identified a
”W-pattern” $P$ inside $"\operatorname{Cover}_{C,D}(T)@cover"$, we remark that
$\pi="\operatorname{run}\nolimits_{P}({1,\underline{1},1,1,1})@W-run"$ and
$\pi^{\prime}="\operatorname{run}\nolimits_{P}({1,1,1,\underline{1},1})@W-run"$.
Additionally, if we transpose $i$ and $j$ from $I_{p}^{\prime}$ back to $I$,
that is, if we set $i^{\prime}=i+|u\,v^{p-1}|$ and
$j^{\prime}=j+|u\,v^{p-1}|$, since both $i^{\prime}$ and $j^{\prime}$ occur in
the $p$-th part of $\pi$ and $\pi^{\prime}$, ”pumping” the interval
$[i^{\prime},j^{\prime}]$ in $\pi$ (resp. $\pi^{\prime}$) amounts to
incrementing the $(p-1)$-th parameter in the notation
$"\operatorname{run}\nolimits_{P}({1,\underline{1},1,1,1})@W-run"$ (resp.
$"\operatorname{run}\nolimits_{P}({1,1,1,\underline{1},1})@W-run"$). More
precisely:

$\displaystyle"\operatorname{pump}^{2}_{[i^{\prime},j^{\prime}]}(\pi)@pump"$
$\displaystyle~{}=~{}"\operatorname{run}\nolimits_{P}({n_{1},\underline{n_{2}},n_{3},n_{4},n_{5}})@W-run"$
$\displaystyle"\operatorname{pump}^{2}_{[i^{\prime},j^{\prime}]}(\pi^{\prime})@pump"$
$\displaystyle~{}=~{}"\operatorname{run}\nolimits_{P}({n_{1},n_{2},n_{3},\underline{n_{4}},n_{5}})@W-run"$

where each $n_{p^{\prime}}$ is either $2$ or $1$ depending on whether
$p^{\prime}=p-1$ or not. Since Equation 4 states that these two ”runs” produce
different ”outputs”, the ”W-pattern” $P$ is ”simply divergent”. Finally, since
the ”runs” of $"\operatorname{Cover}_{C,D}(T)@cover"$ can be projected into
”runs” of $T$, we conclude that, also in this case, $T$ contains a ”simply
divergent” ”W-pattern”. ∎

##  5 Conclusion

We have drawn a rather complete picture of finite-valued SSTs and answered
several open questions of [5]. Regarding expressiveness, they can be
decomposed as unions of deterministic SST (Theorem 1), and they are equivalent
to finite-valued two-way transducers (Theorem 2), and to ”finite-valued” non-
deterministic MSO transductions (see Section 1). On the algorithmic side,
their equivalence problem is decidable in elementary time (Theorem 3) and
”finite valuedness” of ”SSTs” is decidable in PSpace (PTime for a fixed number
of variables), see Theorem 4. As an alternative proof to the result of [46],
our results imply the PSpace decidability of ”finite valuedness” for two-way
transducers (Corollary 1). Because of the effective expressiveness equivalence
between ”SSTs” and non-deterministic MSO transductions, our result also
entails decidability of ”finite valuedness” for the latter class.

##### Further questions.

A first interesting question is how big the valuedness of an ”SST” can be. In
the classical case of one-way transducers the valuedness has been shown to be
at most exponential (if finite at all) [43]. We can obtain a bound from Lemma
8, but the value is likely to be sub-optimal.

Our ”equivalence” procedure relies on the decomposition of a $k$-valued ”SST”
into a union of $k$ ”deterministic” ”SSTs” each of elementary size. Our
construction is likely to be sub-optimal again, and so is our complexity for
checking ”equivalence”. On the other hand, only a PSpace lower bound is known
[35]. A better understanding of the complexity of the ”equivalence” problem
for (sub)classes of ”SSTs” is a challenging question. Already for
”deterministic” ”SSTs”, ”equivalence” is only known to be between NLogSpace
and PSpace [3].

However, beyond the ”finite-valued” setting there is little hope to find a
natural restriction on ”valuedness” which would preserve the decidability of
the ”equivalence” problem. Already for one-way transducers of linear
”valuedness” (i.e. where the number of outputs is linear in the ”input”
length), ”equivalence” is undecidable, as shown through a small modification
of the proof of [28].

”Deterministic” ”SSTs” have been extended, while preserving decidability of
the ”equivalence problem”, in several ways: to copyful ”SSTs” [9, 21], which
allow to copy the content of variables several times, to infinite strings [7],
and to trees [4]. Generalizations of these results to the ”finite-valued”
setting yield interesting questions. On trees, similar questions (effective
”finite valuedness”, decomposition and ”equivalence”) have been answered
positively for bottom-up tree transducers [41].

Finally, ”SSTs” have linear ”input”-to-”output” growth (in the length of the
strings). There is a recent trend in extending transducer models to allow
polynomial growth [12, 10, 11, 18], and ”finite valuedness” has not yet been
studied in this context.

## References

  * [1] M.H. Albert and J. Lawrence.  A proof of Ehrenfeucht’s conjecture.  Theor. Comput. Sci., 41(1):121–123, 1985.
  * [2] Rajeev Alur and Pavol Cerný.  Expressiveness of streaming string transducers.  In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 1–12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010.  URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1, https://doi.org/10.4230/LIPICS.FSTTCS.2010.1 doi:10.4230/LIPICS.FSTTCS.2010.1.
  * [3] Rajeev Alur and Pavol Cerný.  Streaming transducers for algorithmic verification of single-pass list-processing programs.  In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 599–610. ACM, 2011\.  https://doi.org/10.1145/1926385.1926454 doi:10.1145/1926385.1926454.
  * [4] Rajeev Alur and Loris D’Antoni.  Streaming tree transducers.  J. ACM, 64(5):31:1–31:55, 2017.  https://doi.org/10.1145/3092842 doi:10.1145/3092842.
  * [5] Rajeev Alur and Jyotirmoy V. Deshmukh.  Nondeterministic streaming string transducers.  In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 1–20. Springer, 2011.  https://doi.org/10.1007/978-3-642-22012-8_1 doi:10.1007/978-3-642-22012-8_1.
  * [6] Rajeev Alur, Taylor Dohmen, and Ashutosh Trivedi.  Composing copyless streaming string transducers.  CoRR, abs/2209.05448:1–21, 2022.  URL: https://doi.org/10.48550/arXiv.2209.05448, http://arxiv.org/abs/2209.05448 arXiv:2209.05448, https://doi.org/10.48550/ARXIV.2209.05448 doi:10.48550/ARXIV.2209.05448.
  * [7] Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi.  Regular transformations of infinite strings.  In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 65–74. IEEE Computer Society, 2012.  https://doi.org/10.1109/LICS.2012.18 doi:10.1109/LICS.2012.18.
  * [8] Achim Blumensath and Erich Grädel.  Automatic structures.  In Proceedings of the 15th IEEE Symposium on Logic in Computer Science, LICS 2000, pages 51–62. IEEE Computer Society Press, 2000.
  * [9] Mikolaj Bojanczyk.  The hilbert method for transducer equivalence.  ACM SIGLOG News, 6(1):5–17, 2019.  https://doi.org/10.1145/3313909.3313911 doi:10.1145/3313909.3313911.
  * [10] Mikolaj Bojanczyk.  Transducers of polynomial growth.  In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 1:1–1:27. ACM, 2022.  https://doi.org/10.1145/3531130.3533326 doi:10.1145/3531130.3533326.
  * [11] Mikolaj Bojanczyk.  On the growth rates of polyregular functions.  In LICS, pages 1–13. ACM, 2023.  https://doi.org/10.1109/LICS56636.2023.10175808 doi:10.1109/LICS56636.2023.10175808.
  * [12] Mikolaj Bojanczyk, Sandra Kiefer, and Nathan Lhote.  String-to-string interpretations with polynomial-size output.  In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 106:1–106:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.106, https://doi.org/10.4230/LIPICS.ICALP.2019.106 doi:10.4230/LIPICS.ICALP.2019.106.
  * [13] Bruno Courcelle and Joost Engelfriet.  Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics and its applications.  Cambridge University Press, 2012.
  * [14] Karel Culik II and Juhani Karhumäki.  The equivalence of finite valued transducers (on HDT0L languages) is decidable.  Theor. Comput. Sci., 47:71–84, 1986.
  * [15] Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote.  On reversible transducers.  In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 113:1–113:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [16] Luc Dartois, Ismaël Jecker, and Pierre-Alain Reynier.  Aperiodic string transducers.  Int. J. Found. Comput. Sci., 29(5):801–824, 2018.  https://doi.org/10.1142/S0129054118420054 doi:10.1142/S0129054118420054.
  * [17] Rodrigo De Souza.  Etude structurelle des transducteurs de norme bornée.  PhD thesis, LTCI - Laboratoire Traitement et Communication de l’Information, Paris-Saclay, 2008.  URL: http://www.theses.fr/2008ENST0023/document.
  * [18] Gaëtan Douéneau-Tabot.  Optimization of string transducers.  PhD thesis, Université Paris Cité, Paris, France, 2023.  URL: https://gdoueneau.github.io/pages/DOUENEAU-TABOT_Optimization-transducers_v2.pdf.
  * [19] Joost Engelfriet and Hendrik Jan Hoogeboom.  MSO definable string transductions and two-way finite-state transducers.  ACM Trans. Comput. Log., 2(2):216–254, 2001.
  * [20] Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter.  A regular and complete notion of delay for streaming string transducers.  In Petra Berenbrink, Patricia Bouyer, Anuj Dawar, and Mamadou Moustapha Kanté, editors, 40th International Symposium on Theoretical Aspects of Computer Science, STACS 2023, March 7-9, 2023, Hamburg, Germany, volume 254 of LIPIcs, pages 32:1–32:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  https://doi.org/10.4230/LIPIcs.STACS.2023.32 doi:10.4230/LIPIcs.STACS.2023.32.
  * [21] Emmanuel Filiot and Pierre-Alain Reynier.  Copyful streaming string transducers.  Fundam. Informaticae, 178(1-2):59–76, 2021.  https://doi.org/10.3233/FI-2021-1998 doi:10.3233/FI-2021-1998.
  * [22] Patrick C. Fischer and Arnold L. Rosenberg.  Multi-tape one-way nonwriting automata.  J. Comput. and System Sci., 2:88–101, 1968.
  * [23] Victor S. Guba.  Equivalence of infinite systems of equations in free groups and semigroups to finite subsystems.  Mat. Zametki, 40(3):688—690, 1986.
  * [24] Eitan M. Gurari and Oscar H. Ibarra.  The complexity of decision problems for finite-turn multicounter machines.  J. Comput. Syst. Sci., 22(2):220–229, 1981.  https://doi.org/10.1016/0022-0000(81)90028-3 doi:10.1016/0022-0000(81)90028-3.
  * [25] Eitan M. Gurari and Oscar H. Ibarra.  The complexity of decision problems for finite-turn multicounter machines.  In Shimon Even and Oded Kariv, editors, Automata, Languages and Programming, 8th Colloquium, Acre (Akko), Israel, July 13-17, 1981, Proceedings, volume 115 of Lecture Notes in Computer Science, pages 495–505. Springer, 1981.
  * [26] Eitan M. Gurari and Oscar H. Ibarra.  A note on finite-valued and finitely ambiguous transducers.  Math. Syst. Theory, 16(1):61–66, 1983.
  * [27] Bernard R. Hodgson.  Décidabilité par automate fini.  Ann. Sci. Math. Québec, 7(3):39–57, 1983.
  * [28] Oscar H. Ibarra.  The unsolvability of the equivalence problem for e-free NGSM’s with unary input (output) alphabet and applications.  SIAM J. of Comput., 7(4):524–532, 1978.
  * [29] Gérard Jacob.  Un algorithme calculant le cardinal, fini ou infini, des demi-groupes de matrices.  Theoretical Computer Science, 5(2):183–204, 1977.
  * [30] Ismaël Jecker.  A Ramsey theorem for finite monoids.  In Markus Bläser and Benjamin Monmege, editors, 38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, March 16-19, 2021, Saarbrücken, Germany (Virtual Conference), volume 187 of LIPIcs, pages 44:1–44:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  URL: https://doi.org/10.4230/LIPIcs.STACS.2021.44, https://doi.org/10.4230/LIPICS.STACS.2021.44 doi:10.4230/LIPICS.STACS.2021.44.
  * [31] J. Howard Johnson.  Do rational equivalence relations have regular cross-sections?  In Wilfried Brauer, editor, Automata, Languages and Programming, 12th Colloquium, Nafplion, Greece, July 15-19, 1985, Proceedings, volume 194 of Lecture Notes in Computer Science, pages 300–309. Springer, 1985.  URL: https://doi.org/10.1007/BFb0015755, https://doi.org/10.1007/BFB0015755 doi:10.1007/BFB0015755.
  * [32] Bakhadyr Khoussainov and Anil Nerode.  Automatic presentations of structures.  In Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC ’94, Indianapolis, Indiana, USA, 13-16 October 1994, volume 960 of Lecture Notes in Computer Science, pages 367–392. Springer, 1995.
  * [33] Jérémy Ledent.  Streaming string transducers (internship report).  https://perso.ens-lyon.fr/jeremy.ledent/internship_report_L3.pdf, 2013.
  * [34] Arnaldo Mandel and Imre Simon.  On finite semigroups of matrices.  Theoretical Computer Science, 5(2):101–111, 1977.
  * [35] Anca Muscholl and Gabriele Puppis.  Equivalence of finite-valued streaming string transducers is decidable.  In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 122:1–122:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  https://doi.org/10.4230/LIPIcs.ICALP.2019.122 doi:10.4230/LIPIcs.ICALP.2019.122.
  * [36] Brigitte Rozoy.  Outils et résultats pour les transducteurs boustrophédons.  RAIRO-Theoretical Informatics and Applications, 20(3):221–250, 1986\.
  * [37] Aleksi Saarela.  Systems of word equations, polynomials and linear algebra: A new approach.  Eur. J. Comb., 47:1–14, 2015.  https://doi.org/10.1016/j.ejc.2015.01.005 doi:10.1016/j.ejc.2015.01.005.
  * [38] Jacques Sakarovitch.  A construction on finite automata that has remained hidden.  Theor. Comput. Sci., 204(1-2):205–231, 1998.  https://doi.org/10.1016/S0304-3975(98)00040-1 doi:10.1016/S0304-3975(98)00040-1.
  * [39] Jacques Sakarovitch and Rodrigo de Souza.  On the decidability of bounded valuedness for transducers.  In Edward Ochmanski and Jerzy Tyszkiewicz, editors, Mathematical Foundations of Computer Science 2008, 33rd International Symposium, MFCS 2008, Torun, Poland, August 25-29, 2008, Proceedings, volume 5162 of Lecture Notes in Computer Science, pages 588–600. Springer, 2008.
  * [40] Jacques Sakarovitch and Rodrigo de Souza.  On the decomposition of k-valued rational relations.  In Susanne Albers and Pascal Weil, editors, STACS 2008, 25th Annual Symposium on Theoretical Aspects of Computer Science, Bordeaux, France, February 21-23, 2008, Proceedings, volume 1 of LIPIcs, pages 621–632. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2008\.  URL: https://doi.org/10.4230/LIPIcs.STACS.2008.1324, https://doi.org/10.4230/LIPICS.STACS.2008.1324 doi:10.4230/LIPICS.STACS.2008.1324.
  * [41] Helmut Seidl.  Equivalence of finite-valued tree transducers is decidable.  Math. Syst. Theory, 27(4):285–346, 1994.  https://doi.org/10.1007/BF01192143 doi:10.1007/BF01192143.
  * [42] John C. Shepherdson.  The reduction of two-way automata to one-way automata.  IBM J. Res. Dev., 3(2):198–200, 1959.  URL: https://doi.org/10.1147/rd.32.0198, https://doi.org/10.1147/RD.32.0198 doi:10.1147/RD.32.0198.
  * [43] Andreas Weber.  Decomposing finite-valued transducers and deciding their equivalence.  SIAM J. Comput., 22(1):175–202, 1993.  https://doi.org/10.1137/0222014 doi:10.1137/0222014.
  * [44] Andreas Weber.  Decomposing a k-valued transducer into k unambiguous ones.  RAIRO-ITA, 30(5):379–413, 1996.
  * [45] Andreas Weber and Helmut Seidl.  On the degree of ambiguity of finite automata.  Theor. Comput. Sci., 88(2):325–349, 1991.  https://doi.org/10.1016/0304-3975(91)90381-B doi:10.1016/0304-3975(91)90381-B.
  * [46] Di-De Yen and Hsu-Chun Yen.  On the decidability of the valuedness problem for two-way finite transducers.  Inf. Comput., 285(Part):104870, 2022.  URL: https://doi.org/10.1016/j.ic.2022.104870, https://doi.org/10.1016/J.IC.2022.104870 doi:10.1016/J.IC.2022.104870.

##  Appendix A Appendix

###  A.1 Pumping and word combinatorics

*

###### Proof.

The paper [30] computes for a given monoid $M$ an upper bound $R_{M}(n)$ such
that any sequence from $M^{*}$ of length larger than $R_{M}(n)$ contains $n$
consecutive infixes such for some idempotent $e$ of $M$ (i.e., satisfying
$ee=e$) each such infix multiplies out to $e$. In our case, the monoid $M$ is
the product of the monoid $((Q\times Q)\cup\\{0\\},\cdot)$ with
$(p,q)\cdot(q,r)=(p,r)$ (resp. $(p,q)\cdot(q^{\prime},r)=0$ if
$q\not=q^{\prime}$) and the ”skeleton monoid” of the ”SST”. Thus, any infix of
the run that multiplies out to an idempotent (after mapping each transition to
the corresponding monoid element) corresponds to a ”loop” of the ”SST”. The
upper bound $R_{M}(n)$ is exponential only in the size of $M$. ∎

*

###### Proof.

Let $\hat{\alpha}$ be the ”idempotent” ”skeleton” of $\alpha$. We first prove
the following claim:

######  Claim.

For all $X\in\mathcal{X}$, if $\hat{\alpha}(X)\neq\varepsilon$, then $X$
occurs in $\alpha(X)$.

###### Proof of the claim.

The proof is by induction on the number of variables $X$ such that
$\hat{\alpha}(X)\neq\varepsilon$. The base case holds vacuously. As for the
induction step, fix a variable $X_{0}$ such that
$\hat{\alpha}(X_{0})\neq\varepsilon$. We distinguish two cases:

  * •

If $X_{0}$ occurs in $\alpha(X_{0})$, then the claim clearly holds for $X_{0}$
and it reamins to prove it for all other variables
$Y\in\mathcal{X}\setminus\\{X_{0}\\}$. Since $\alpha$ is copyless, $X_{0}$
does not occur in $\alpha(Y)$, for all $Y\in\mathcal{X}\setminus\\{X_{0}\\}$.
Therefore, the restricted ”update” $\alpha|_{\mathcal{X}\setminus\\{X_{0}\\}}$
has an ”idempotent” ”skeleton”, and by the inductive hyopotehsis it satisfies
the claim. From this we immediately derive that the claim also holds for the
original ”update” $\alpha$.

  * •

If $X_{0}$ does not occur in $\alpha(X_{0})$, then $\alpha(X_{0})$ still
contains at least one occurrence of another variable, since
$\hat{\alpha}(X_{0})\neq\varepsilon$. So, suppose that $\alpha(X_{0})=h\,Y\,t$
for some $h,t\in(\mathcal{X}\cup\Sigma)^{*}$ and $Y\in\mathcal{X}$. Since
$\alpha$ is ”skeleton-idempotent”, we have
$(\alpha\alpha)(X_{0})=\alpha(h)\,\alpha(Y)\,\alpha(t)=h^{\prime}\,Y\,t^{\prime}$
for some $h^{\prime},t^{\prime}\in(\mathcal{X}\cup\Sigma^{*})$. Now, if $Y$
occurs in $\alpha(Y)$, then we can apply the inductive hypothesis on the
restriction $\alpha|_{\mathcal{X}\setminus\\{Y\\}}$, as in the previous case,
and establish the claim. Otherwise, if $Y$ does not occur in $\alpha(Y)$, we
reach a contradiction by arguing as follows. Since $Y$ occurs in
$\alpha(h)\,\alpha(Y)\,\alpha(t)$ but not in $\alpha(Y)$, then it occurs in
$\alpha(h)\,\alpha(t)$. Since $X_{0}$ is the unique variable such that $Y$
occurs in $\alpha(X_{0})$ (because $\alpha$ is copyless), necessarily $X_{0}$
occurs in $h\,t$ and hence in $\alpha(X_{0})$ as well, which contradicts the
initial assumption. ∎

We conclude the proof of the lemma. Let $X\in\mathcal{X}$. If $\alpha(X)$ does
not contain any variable, then we immediately get the result, as
$\alpha^{n}(X)=\alpha(X)$ for all $n\geq 1$. Otherwise, if $\alpha(X)$
contains some variable, then we know that $\hat{\alpha}(X)\neq\varepsilon$, so
by the above claim, $X$ occurs in $\alpha(X)$. Hence, $\alpha(X)=h\,X\,t$ for
some $h,t\in(\mathcal{X}\cup\Sigma)^{*}$. We now prove that
$\alpha(h)\,\alpha(t)\in\Sigma^{*}$. Indeed, let $Y$ be any variable in $h\,t$
(if there is no such variable then clearly $\alpha(h)\,\alpha(t)$ contains no
variable either). Since $\alpha$ is copyless, $Y$ does not occur in
$\alpha(Y)$, hence by the above claim (contrapositive),
$\hat{\alpha}(Y)=\varepsilon$, whence $\alpha(Y)\in\Sigma^{*}$. We then derive
$(\alpha\alpha)(X)=\alpha(h)\,\alpha(X)\,\alpha(t)$, where
$\alpha(h),\alpha(t)\in\Sigma^{*}$, and so we can take $u=\alpha(h)$ and
$v=\alpha(t)$. To conclude, we have $\alpha^{2}(X)=u\,\alpha(X)\,v$, so for
$n>2$,
$\alpha^{n}(X)=\alpha^{n-2}(\alpha^{2}(X))=\alpha^{n-2}(u\,\alpha(X)\,v)=u\,\alpha^{n-1}(X)\,v$,
as claimed. ∎

*

Ag$\mathtt{x}$Ag$\mathtt{y}$AgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAg$g^{\prime}_{\emptyset}$Ag$g^{\prime\prime}_{\emptyset}$Ag$\phantom{X}g^{\prime}_{\\{\mathtt{x}\\}}$Ag$g^{\prime\prime}_{\\{\mathtt{x}\\}}$Ag$g^{\prime}_{\\{\mathtt{x},\mathtt{y}\\}}=g^{\prime\prime}_{\\{\mathtt{x},\mathtt{y}\\}}$AgTh.
8AgTh. 8AgTh. 8AgTh. 8 Figure 1: Illustration of an argument for the proof of
Corollary 3

###### Proof.

We assume that all inequalities considered hereafter have parameters in
$\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$. We are going to
compare functions from $\mathtt{X}$ to $\mathbb{N}$ based on suitable partial
orders, each parametrized by a variable. Formally, given two functions
$f,g:\mathtt{X}\rightarrow\mathbb{N}$ and a variable
$\mathtt{x}\in\mathtt{X}$, we write
$f\mathrel{""\leq_{\mathtt{x}}@variableorder""}g$ iff $f(\mathtt{x})\leq
g(\mathtt{x})$ and $f(\mathtt{y})=g(\mathtt{y})$ for all
$\mathtt{y}\in\mathtt{X}\setminus\\{\mathtt{x}\\}$. We prove the following two
properties (the first property is equivalent to the claim of the lemma):

$\displaystyle\bigwedge_{e\in E}\exists
f\in"\operatorname{Sols}(e)@solutions"~{}~{}\rightarrow~{}~{}\exists
g\in"\operatorname{Sols}(E)@solutions"$ (5) $\displaystyle\forall
f\in"\operatorname{Sols}(E)@solutions"~{}~{}\forall\mathtt{x}\in\mathtt{X}~{}~{}\exists
g\mathrel{"\geq_{\mathtt{x}}@variableorder"}f~{}~{}\forall
h\mathrel{"\geq_{\mathtt{x}}@variableorder"}g~{}~{}h\in"\operatorname{Sols}(E)@solutions"$
(6)

The proof is by a double induction on the cardinality of $E$ and the number
$k$ of parameters.

The base case is when $E$ has cardinality $1$. In this case Property (5) holds
trivially. We see how Property (6) follows from Theorem 8. Let $E=\\{e\\}$,
$f\in"\operatorname{Sols}(e)@solutions"$, and fix an arbitrary variable
$\mathtt{x}\in\mathtt{X}$. We construct the ”inequality” $e^{\prime}$ with
$\mathtt{x}$ as single formal parameter, by instantiating in $e$ every other
parameter $\mathtt{y}\in\mathtt{X}\setminus\\{\mathtt{x}\\}$ with the value
$f(\mathtt{y})$. By construction, $f$ restricted to $\\{\mathtt{x}\\}$ is a
”solution” of $e^{\prime}$, and thus, by Theorem 8,
$"\operatorname{Sols}(e^{\prime})@solutions"$ is co-finite. This means that
there is a number $x_{0}\in\mathbb{N}$ such that $x_{0}\geq f(\mathtt{x})$
and, for all $x_{1}\geq x_{0}$, the mapping $\mathtt{x}\mapsto x_{1}$ is a
”solution” to $e^{\prime}$ as well. This property can be transferred to the
original ”inequality” $e$, as follows. We define $g=f[\mathtt{x}/x_{1}]$ as
the function obtained from $f$ by replacing the image of $\mathtt{x}$ with
$x_{1}$. Note that $g\geq_{\mathtt{x}}f$ and, for all
$h\mathrel{"\geq_{\mathtt{x}}@variableorder"}g$,
$h\in"\operatorname{Sols}(e)@solutions"$. This proves Property (6).

As for the inductive step, suppose that $E$ is a ”system” with at least two
”inequalities”, and divide $E$ into two sub-systems, $E^{\prime}$ and
$E^{\prime\prime}$, with cardinalities strictly smaller than that of $E$.

Let us first prove Property (5) for $E$. Suppose that every ”inequality” in
$E$ is ”satisfiable”. By the inductive hypothesis, $E^{\prime}$ and
$E^{\prime\prime}$ are also ”satisfiable”; in particular, there exist
”solutions” $g^{\prime}$ and $g^{\prime\prime}$ of $E^{\prime}$ and
$E^{\prime\prime}$, respectively. We proceed with a second induction to prove
that, for larger and larger sets of variables $\mathtt{Y}\subseteq\mathtt{X}$,
there are ”solutions” of $E^{\prime}$ and $E^{\prime\prime}$ that agree on all
the variables from $\mathtt{Y}$, namely:

$\displaystyle\exists
g^{\prime}_{\mathtt{Y}}\in"\operatorname{Sols}(E^{\prime})@solutions"~{}~{}\exists
g^{\prime\prime}_{\mathtt{Y}}\in"\operatorname{Sols}(E^{\prime\prime})@solutions"~{}~{}\forall\mathtt{y}\in\mathtt{Y}~{}~{}g^{\prime}_{\mathtt{Y}}(\mathtt{y})=g^{\prime\prime}_{\mathtt{Y}}(\mathtt{y})\
.$ ($\star$)

Of course, for $\mathtt{Y}=\mathtt{X}$, the above property will imply the
existence of a ”solution” of $E$. The reader can refer to Figure 1 as an
illustration of the arguments that follow (axes correspond to variables, and
red and blue dots represent ”solutions” of the ”systems” $E^{\prime}$ and
$E^{\prime\prime}$, respectively).

For $\mathtt{Y}=\emptyset$, the claim ($\star$) is trivial, since we can
simply let $g^{\prime}_{\emptyset}=g^{\prime}$ and
$g^{\prime\prime}_{\emptyset}=g^{\prime\prime}$. For the inductive step,
suppose that ($\star$) holds for $\mathtt{Y}$ and let us prove it also holds
for $\mathtt{Y}^{\prime}=\mathtt{Y}\uplus\\{\mathtt{x}\\}$. By inductive
hypothesis, $E^{\prime}$ and $E^{\prime\prime}$ satisfy Property (6). In
particular, by instantiating $f$ with $g^{\prime}_{\mathtt{Y}}$ (resp.
$g^{\prime\prime}_{\mathtt{Y}}$) in Property (6), we obtain the existence of
$g^{\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}g^{\prime}_{\mathtt{Y}}$
such that, for all
$h^{\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}g^{\prime}$,
$h^{\prime}\in"\operatorname{Sols}(E^{\prime})@solutions"$ (resp.
$g^{\prime\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}g^{\prime\prime}_{\mathtt{Y}}$
such that, for all
$h^{\prime\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}g^{\prime\prime}$,
$h^{\prime\prime}\in"\operatorname{Sols}(E^{\prime\prime})@solutions"$). Note
that the functions $g^{\prime}_{\mathtt{Y}}$, $g^{\prime\prime}_{\mathtt{Y}}$,
$g^{\prime}$, $g^{\prime\prime}$ all agree on the variables from $\mathtt{Y}$.
Moreover, without loss of generality, we can assume that $g^{\prime}$ and
$g^{\prime\prime}$ also agree on the variable $\mathtt{x}$: indeed, if this
were not the case, we could simply replace the $\mathtt{x}$-images of
$g^{\prime}$ and $g^{\prime\prime}$ with
$\max\\{g^{\prime}(\mathtt{x}),g^{\prime\prime}(\mathtt{x})\\}$, without
affecting the previous properties. Property ($\star$) now follows from letting
$g^{\prime}_{\mathtt{Y}^{\prime}}=g^{\prime}$ and
$g^{\prime\prime}_{\mathtt{Y}^{\prime}}=g^{\prime\prime}$. This concludes the
proof of the inductive step for Property (5).

Let us now prove the inductive step for Property (6). Let $f$ be a ”solution”
of $E$ and let $\mathtt{x}\in\mathtt{X}$. Since both $E^{\prime}$ and
$E^{\prime\prime}$ satisfy Property (6) and since
$f\in"\operatorname{Sols}(E^{\prime})@solutions"\cap"\operatorname{Sols}(E^{\prime\prime})@solutions"$,
there are
$g^{\prime},g^{\prime\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}f$ such
that, for all
$h^{\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}g^{\prime}$ and
$h^{\prime\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}g^{\prime\prime}$,
$h^{\prime}\in"\operatorname{Sols}(E^{\prime})@solutions"$ and
$h^{\prime\prime}\in"\operatorname{Sols}(E^{\prime\prime})@solutions"$. Since
$g^{\prime},g^{\prime\prime}\mathrel{"\geq_{\mathtt{x}}@variableorder"}f$,
$g^{\prime}$ and $g^{\prime\prime}$ agree on all variables, except possibly
$\mathtt{x}$. Without loss of generality, we can also assume that $g^{\prime}$
and $g^{\prime\prime}$ agree on $\mathtt{x}$: as before, if this were not the
case, we could replace the $\mathtt{x}$-images of $g^{\prime}$ and
$g^{\prime\prime}$ with
$\max\\{g^{\prime}(\mathtt{x}),g^{\prime\prime}(\mathtt{x})\\}$, while
preserving the previous properties. Now that we have
$g^{\prime}=g^{\prime\prime}$, we can use this function to witness Property
(6), since, for all $h\mathrel{"\geq_{\mathtt{x}}@variableorder"}g^{\prime}$
($=g^{\prime\prime}$), we have
$h\in"\operatorname{Sols}(E^{\prime})@solutions"\cap"\operatorname{Sols}(E^{\prime\prime})@solutions"="\operatorname{Sols}(E)@solutions"$.
∎

*

Ag$\mathtt{x}_{1}$Ag$\mathtt{x}_{2}$AgAg$\phantom{XXX}\\{x_{1}\\}\times\\{x_{2}\\}$AgAgAgAgAgAgAgAg$\exists\ell_{1}$Ag$\forall
h_{1}$Ag$[\ell_{1},h_{1}]\times\\{x_{2}\\}$AgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAgAg$\exists\ell_{2}$Ag$\forall
h_{2}$Ag$[\ell_{1},h_{1}]\times[\ell_{2},h_{2}]$AgTh. 8AgTh. 8AgTh. 8AgTh.
8AgTh. 8 Figure 2: Illustration of an argument for the proof of Corollary 4

###### Proof.

Let $e$ be a ”satisfiable” ”word inequality” parametrized in $\mathtt{X}$ and
let $\bar{x}=(x_{1},\dots,x_{k})$ be any ”solution” of $e$. We will prove the
following claim by induction on $i=0,\dots,k$:

$\displaystyle\exists\ell_{1}~{}\forall
h_{1}~{}\dots~{}\exists~{}\ell_{i}~{}\forall h_{i}$
$\displaystyle\quad[\ell_{1},h_{1}]\times\cdots\times[\ell_{i},h_{i}]\times\\{x_{i+1}\\}\times\dots\times\\{x_{k}\\}\subseteq"\operatorname{Sols}(e)@solutions"$
($\star$)

Note that for $i=k$ the above claim coincides with the statement of the
corollary. The reader can also refer to Figure 2 as an illustration of the
arguments that follow (axes correspond to variables $\mathtt{x}_{1}$ and
$\mathtt{x}_{2}$, dots represent generic ”solutions” of $e$, clusters of black
dots represent solutions in the form of Cartesian products, like those that
appear in ($\star$).