11institutetext: LaBRI, University of Bordeaux, France22institutetext: Dept.
of Computer Science & Engineering IIT Bombay, India 33institutetext: Dept. of
Mathematics, Computer Science, and Physics, Udine University, Italy

# One-way Resynchronizability
of Word Transducers

Sougata Bose 11 S.N. Krishna 22 Anca Muscholl 11 Gabriele Puppis 33

###### Abstract

The origin semantics for transducers was proposed in 2014, and it led to
various characterizations and decidability results that are in contrast with
the classical semantics. In this paper we add a further decidability result
for characterizing transducers that are close to one-way transducers in the
origin semantics. We show that it is decidable whether a non-deterministic
two-way word transducer can be resynchronized by a bounded, regular
resynchronizer into an origin-equivalent one-way transducer. The result is in
contrast with the usual semantics, where it is undecidable to know if a non-
deterministic two-way transducer is equivalent to some one-way transducer.

###### Keywords:

String transducers Resynchronizers One-way transducers

##  1 Introduction

Regular word-to-word functions form a robust and expressive class of
transformations, as they correspond to deterministic two-way transducers, to
deterministic streaming string transducers [1], and to monadic second-order
logical transductions [11]. However, the transition from word languages to
functions over words is often quite tricky. One of the challenges is to come
up with effective characterizations of restricted transformations. A first
example is the characterization of functions computed by one-way transducers
(known as  _rational functions_). It turns out that it is decidable whether a
regular function is rational [14], but the algorithm is quite involved [3]. In
addition, non-determinism makes the problem intractable: it is undecidable
whether the relation computed by a non-deterministic two-way transducer can be
also computed by a one-way transducer, [2]. A second example is the problem of
knowing whether a regular word function can be described by a first-order
logical transduction. This question is still open in general [16], and it is
only known how to decide if a _rational_ function is definable in first-order
logic [13].

Word transducers with origin semantics were introduced by Bojańczyk [4] and
shown to provide a machine-independent characterization of regular word-to-
word functions. The origin semantics, as the name suggests, means tagging the
output by the positions of the input that generated that output.

A nice phenomenon is that origins can restore decidability for some
interesting problems. For example, the equivalence of word relations computed
by one-way transducers, which is undecidable in the classical semantics [18,
19], is PSPACE-complete for two-way non-deterministic transducers in the
origin semantics [7]. Another, deeper, observation is that the origin
semantics provides an algebraic approach that can be used to decide fragments.
For example, [4] provides an effective characterization of first-order
definable word functions under the origin semantics. As for the problem of
knowing whether a regular word function is rational, it becomes almost trivial
in the origin semantics.

Ag$b$Ag$a$Ag$c$Ag$a$Ag$a$Ag$b$Ag$a$Ag$c$input:output:origins:Ag$b$Ag$a$Ag$c$Ag$a$Ag$a$Ag$b$Ag$a$Ag$c$input:output:resynchronizedorigins:
Figure 1: On the left, an input-output pair for a transducer $T$ that reads
$wd$ and outputs $dw$, $d\in\Sigma$, $w\in\Sigma^{*}$, the arrows denoting
origins. On the right, the same input-output pair, but with origins modified
by a resynchronizer $\mathcal{R}$. The resynchronized relation
$\mathcal{R}(T)$ is order-preserving, and $T$ is one-way resynchronizable.

A possible objection against the origin semantics is that the comparison of
two transducers in the origin semantics is too strict. Resynchronizations were
proposed in order to overcome this issue. A resynchronization is a binary
relation between input-output pairs with origins, that preserves the input and
the output, changing only the origins. Resynchronizations were introduced for
one-way transducers [15], and later for two-way transducers [7]. For one-way
transducers _rational_ resynchronizations are transducers acting on the
synchronization languages, whereas for two-way transducers, _regular_
resynchronizations are described by regular properties over the input that
restrict the change of origins. The class of bounded111“Bounded” refers here
to the number of source positions that are mapped to the same target position.
It rules out resynchronizations such as the universal one. regular
resynchronizations was shown to behave very nicely, preserving the class of
transductions defined by non-deterministic, two-way transducers: for any
bounded regular resynchronization $\mathcal{R}$ and any two-way transducer
$T$, the resynchronized relation $\mathcal{R}(T)$ can be computed by another
two-way transducer [7]. In particular, non-deterministic, two-way transducers
can be effectively compared modulo bounded regular resynchronizations.

As mentioned above, it is easy to know if a two-way transducer is equivalent
under the origin semantics to some one-way transducer [4], since this is
equivalent to being order-preserving. But what happens if this is not the
case? Still, the given transducer $T$ can be “close” to some order-preserving
transducer. What we mean here by “close” is that there exists some bounded
regular resynchronizer $\mathcal{R}$ such that $\mathcal{R}(T)$ is order-
preserving and all input-output pairs with origins produced by $T$ are in the
domain of $\mathcal{R}$. We call such transducers _one-way resynchronizable_.
Figure 1 gives an example.

In this paper we show that it is decidable if a two-way transducer is one-way
resynchronizable. We first solve the problem for bounded-visit two-way
transducers. A bounded-visit transducer is one for which there is a uniform
bound for the number of visits of any input position. Then, we use the
previous result to show that one-way resynchronizability is decidable for
arbitrary two-way transducers, so without the bounded-visit restriction. This
is done by constructing, if possible, a bounded, regular resynchronization
from the given transducer to a bounded-visit transducer with regular language
outputs. Finally, we show that bounded regular resynchronizations are closed
under composition, and this allows to combine the previous construction with
our decidability result for bounded-visit transducers.

_Related work and paper overview._ The synthesis problem for resynchronizers
asks to compute a resynchronizer from one transducer to another one, when the
two transducers are given as input. The problem was studied in [6] and shown
to be decidable for unambiguous two-way transducers (it is open for
unrestricted transducers). The paper [21] shows that the containment version
of the above problem is undecidable for unrestricted one-way transducers.

The origin semantics for streaming string transducers (SST) [1] has been
studied in [5], providing a machine-independent characterization of the sets
of origin graphs generated by SSTs. An open problem here is to characterize
origin graphs generated by aperiodic streaming string transducers [10, 16].
Going beyond words, [17] investigates decision problems of tree transducers
with origin, and regains the decidability of the equivalence problem for non-
deterministic top-down and MSO transducers by considering the origin
semantics. An open problem for tree transducers with origin is that of
synthesizing resynchronizers as in the word case.

We will recall regular resynchronizations in Section 3. Section 4 provides the
proof ingredients for the bounded-visit case, and the proof of decidability of
one-way resynchronizability in the bounded-visit case can be found in Section
5. Finally, in Section 6 we sketch the proof in the general case. Missing
proofs can be found in the appendix.

##  2 Preliminaries

Let $\Sigma$ be a finite input alphabet. Given a word $w\in\Sigma^{*}$ of
length $|w|=n$, a _position_ is an element of its domain
$\mathsf{dom}(w)=\\{1,\dots,n\\}$. For every position $i$, $w(i)$ denotes the
letter at that position. A _cut_ of $w$ is any number from $1$ to $|w|+1$, so
a cut identifies a position _between_ two consecutive letters of the input.
The cut $i=1$ represents the position just before the first input letter, and
$i=|w|+1$ the position just after the last letter of $w$.

#### Two-way transducers.

We use two-way transducers as defined in [3, 6], with a slightly different
presentation than in classical papers such as [22]. As usual for two-way
machines, for any input $w\in\Sigma^{*}$, $w(0)=\mathop{\vdash}$ and
$w(|w|+1)=\mathop{\dashv}$, where
$\mathop{\vdash},\mathop{\dashv}\notin\Sigma$ are special markers used as
delimiters.

A _two-way transducer_ (or just _transducer_ from now on) is a tuple
$T=(Q,\Sigma,\Gamma,\Delta,I,F)$, where $\Sigma,\Gamma$ are respectively the
input and output alphabets, $Q=Q_{\prec}\uplus Q_{\succ}$ is the set of
states, partitioned into left-reading states from $Q_{\prec}$ and right-
reading states from $Q_{\succ}$, $I\subseteq Q_{\succ}$ is the set of initial
states, $F\subseteq Q$ is the set of final states, and $\Delta\subseteq
Q\times(\Sigma\uplus\\{\mathop{\vdash},\mathop{\dashv}\\})\times\Gamma^{*}\times
Q$ is the finite transition relation. Left-reading states read the letter to
the left, whereas right-reading states read the letter to the right. This
partitioning will also determine the head movement during a transition, as
explained below.

As usual, to define runs of transducers we first define configurations. Given
a transducer $T$ and a word $w\in\Sigma^{*}$, a _configuration_ of $T$ on $w$
is a state-cut pair $(q,i)$, with $q\in Q$ and $1\leq i\leq|w|+1$. A
configuration $(q,i)$, $1\leq i\leq|w|+1$ means that the automaton is in state
$q$ and its head is between the $(i-1)$-th and the $i$-th letter of $w$. The
transitions that depart from a configuration $(q,i)$ and read $a$ are denoted
$(q,i)\stackrel{{\scriptstyle a}}{{\longrightarrow}}(q^{\prime},i^{\prime})$,
and must satisfy one of the following:
(1) $q\in Q_{\succ}$, $q^{\prime}\in Q_{\succ}$, $a=w(i)$,
$(q,a,v,q^{\prime})\in\Delta$, and $i^{\prime}=i+1$,
(2) $q\in Q_{\succ}$, $q^{\prime}\in Q_{\prec}$, $a=w(i)$,
$(q,a,v,q^{\prime})\in\Delta$, and $i^{\prime}=i$,
(3) $q\in Q_{\prec}$, $q^{\prime}\in Q_{\succ}$, $a=w(i-1)$,
$(q,a,v,q^{\prime})\in\Delta$, and $i^{\prime}=i$,
(4) $q\in Q_{\prec}$, $q^{\prime}\in Q_{\prec}$, $a=w(i-1)$,
$(q,a,v,q^{\prime})\in\Delta$, and $i^{\prime}=i-1$. When $T$ has only right-
reading states (i.e. $Q_{\prec}=\emptyset$), its head can only move rightward.
In this case we call $T$ a _one-way transducer_.

A _run_ of $T$ on $w$ is a sequence $\rho=(q_{1},i_{1})\stackrel{{\scriptstyle
a_{j_{1}}\mid v_{1}}}{{\longrightarrow}}(q_{2},i_{2})\stackrel{{\scriptstyle
a_{j_{2}}\mid v_{2}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle
a_{j_{m}}\mid v_{m}}}{{\longrightarrow}}(q_{m+1},i_{m+1})$ of configurations
connected by transitions. Note that the positions $j_{1},j_{2},\dots,j_{m}$ of
letters do not need to be ordered from smaller to bigger, and can differ
slightly (by $+1$ or $-1$) from the cuts $i_{1},i_{2},\dots,i_{m+1}$, since
cuts take values in between consecutive letters.

A configuration $(q,i)$ on $w$ is _initial_ (resp.  _final_) if $q\in I$ and
$i=1$ (resp. $q\in F$ and $i=|w|+1$). A run is _successful_ if it starts with
an initial configuration and ends with a final configuration. The _output_
associated with a successful run $\rho$ as above is the word $v_{1}v_{2}\cdots
v_{m}\in\Gamma^{*}$. A transducer $T$ defines a relation
${[\\![T]\\!]}\subseteq\Sigma^{*}\times\Gamma^{*}$ consisting of all the pairs
$(u,v)$ such that $v$ is the output of some successful run $\rho$ of $T$ on
$u$.

#### Origin semantics.

In the origin semantics for transducers [4] the output is tagged with
information about the position of the input where it was produced. If reading
the $i$-th letter of the input we output $v$, then all letters of $v$ are
tagged with $i$, and we say they have _origin_ $i$. We use the notation
$(v,i)$ for $v\in\Gamma^{*}$ to denote that all positions in the output word
$v$ have origin $i$, and we view $(v,i)$ as word over the alphabet
$\Gamma\times\mathbb{N}$. The outputs associated with a successful run
$\rho=(q_{1},i_{1})\stackrel{{\scriptstyle b_{1}\mid
v_{1}}}{{\longrightarrow}}(q_{2},i_{2})\stackrel{{\scriptstyle b_{2}\mid
v_{2}}}{{\longrightarrow}}(q_{3},i_{3})\cdots\stackrel{{\scriptstyle b_{m}\mid
v_{m}}}{{\longrightarrow}}(q_{m+1},i_{m+1})$ in the origin semantics are the
words of the form $\nu=(v_{1},j_{1})(v_{2},j_{2})\cdots(v_{m},j_{m})$ over
$\Gamma\times\mathbb{N}$ where, for all $1\leq k\leq m$, $j_{k}=i_{k}$ if
$q_{k}\in Q_{\succ}$, and $j_{k}=i_{k}-1$ if $q_{k}\in Q_{\prec}$. Under the
origin semantics, the relation defined by $T$, denoted ${[\\![T]\\!]}_{o}$, is
the set of pairs $\sigma=(u,\nu)$ —called _synchronized pairs_ — such that
$u\in\Sigma^{*}$ and $\nu\in(\Gamma\times\mathbb{N})^{*}$ is the output of
some successful run on $u$.

Equivalently, a synchronized pair $(u,\nu)$ can be described as a triple
$(u,v,\mathit{orig})$, where $v$ is the projection of $\nu$ on $\Gamma$, and
$\mathit{orig}:\mathsf{dom}(v)\to\mathsf{dom}(u)$ associates with each
position of $v$ its origin in $u$. So for
$\nu=(v_{1},j_{1})(v_{2},j_{2})\cdots(v_{m},j_{m})$ as above, $v=v_{1}\dots
v_{m}$, and, for all positions $i$ s.t. $|v_{1}\dots v_{k-1}|<i\leq|v_{1}\dots
v_{k}|$, we have $\mathit{orig}(i)=j_{k}$. Given two transducers
$T_{1},T_{2}$, we say they are _origin-equivalent_ if
${[\\![T_{1}]\\!]}_{o}={[\\![T_{2}]\\!]}_{o}$. Note that two transducers
$T_{1},T_{2}$ can be equivalent in the classical semantics,
${[\\![T_{1}]\\!]}={[\\![T_{2}]\\!]}$, while they can have different origin
semantics, so ${[\\![T_{1}]\\!]}_{o}\neq{[\\![T_{2}]\\!]}_{o}$.

#### Bounded-visit transducers.

Let $k>0$ be some integer, and $\rho$ some run of a two-way transducer $T$. We
say that $\rho$ is _$k$ -visit_ if for every $i\geq 0$, it has at most $k$
occurrences of configurations from $Q\times\\{i\\}$. We call a transducer $T$
_$k$ -visit_ if for every $\sigma\in{[\\![T]\\!]}_{o}$ there is some
successful, $k$-visit run $\rho$ of $T$ with output $\sigma$ (actually we
should call the transducer $k$-visit _in the origin semantics_ , but for
simplicity we omit this). For example, the relation $\\{(w,\overline{w})\mid
w\in\Sigma^{*}\\}$, where $\overline{w}$ denotes the reverse of $w$, can be
computed by a $3$-visit transducer. A transducer is called _bounded-visit_ if
it is $k$-visit for some $k$.

#### Common guess.

It is often useful to work with a variant of two-way transducers that can
guess beforehand some annotation on the input and inspect it consistently when
visiting portions of the input multiple times. This feature is called _common
guess_ [5], and strictly increases the expressive power of two-way
transducers, including bounded-visit ones.

##  3 One-way resynchronizability

###  3.1 Regular resynchronizers

Resynchronizations are used to compare transductions in the origin semantics.
A _resynchronization_ is a binary relation
$\mathcal{R}\subseteq(\Sigma^{*}\times(\Gamma\times\mathbb{N})^{*})^{2}$ over
synchronized pairs such that $(\sigma,\sigma^{\prime})\in\mathcal{R}$ implies
that $\sigma=(u,v,\mathit{orig})$ and
$\sigma^{\prime}=(u,v,\mathit{orig}^{\prime})$ for some origin mappings
$\mathit{orig},\mathit{orig}^{\prime}:\mathsf{dom}(v)\to\mathsf{dom}(u)$. In
other words, a resynchronization will only change the origin mapping, but
neither the input, nor the output. Given a relation
$S\subseteq\Sigma^{*}\times(\Gamma\times\mathbb{N})^{*}$ with origins, the
_resynchronized relation_ $\mathcal{R}(S)$ is defined as
$\mathcal{R}(S)=\\{\sigma^{\prime}\mid(\sigma,\sigma^{\prime})\in\mathcal{R},\;\sigma\in
S\\}$. For a transducer $T$ we abbreviate $\mathcal{R}({[\\![T]\\!]}_{o})$ by
$\mathcal{R}(T)$. The typical use of a resynchronization $\mathcal{R}$ is to
ask, given two transducers $T,T^{\prime}$, whether $\mathcal{R}(T)$ and
$T^{\prime}$ are origin-equivalent.

Regular resynchronizers (originally called MSO resynchronizers) were
introduced in [7] as a resynchronization mechanism that preserves definability
by two-way transducers. They were inspired by MSO (monadic second-order)
transductions [9, 12] and they are formally defined as follows. A _regular
resynchronizer_ is a tuple
$\mathcal{R}=(\overline{I},\overline{O},\mathsf{ipar},\mathsf{opar},(\mathsf{move}_{\tau})_{\tau},(\mathsf{next}_{\tau,\tau^{\prime}})_{\tau,\tau^{\prime}})$
consisting of

  * •

some monadic parameters (colors) $\overline{I}=(I_{1},\dots,I_{m})$ and
$\overline{O}=(O_{1},\dots,O_{n})$,

  * •

MSO sentences $\mathsf{ipar},\mathsf{opar}$, defining languages over expanded
input and output alphabets, i.e. over $\Sigma^{\prime}=\Sigma\times
2^{\\{1,\dots,m\\}}$ and $\Gamma^{\prime}=\Gamma\times 2^{\\{1,\dots,n\\}}$,
respectively,

  * •

MSO formulas $\mathsf{move}_{\tau}(y,z)$,
$\mathsf{next}_{\tau,\tau^{\prime}}(z,z^{\prime})$ with two free first-order
variables and parametrized by expanded output letters $\tau,\tau^{\prime}$
(called types, see below).

To apply a regular resynchronizer as above, one first guesses the valuation of
all the predicates $I_{j},O_{k}$, and uses it to interpret the parameters
$\overline{I}$ and $\overline{O}$. Based on the chosen valuation of the
parameters $\overline{O}$, each position $x$ of the output $v$ gets an
associated _type_
$\tau_{x}=(v(x),b_{1},\dots,b_{n})\in\Gamma\times\\{0,1\\}^{n}$, where $b_{j}$
is $1$ or $0$ depending on whether $x\in O_{j}$ or not. We refer to the output
word together with the valuation of the output parameters as _annotated
output_ , so a word over $\Gamma\times\\{0,1\\}^{n}$. Similarly, the
_annotated input_ is a word over $\Sigma\times\\{0,1\\}^{m}$. The annotated
input and output word must satisfy the formulas $\mathsf{ipar}$ and
$\mathsf{opar}$, respectively.

The origins of output positions are constrained using the formulas
$\mathsf{move}_{\tau}$ and $\mathsf{next}_{\tau,\tau^{\prime}}$, which are
_parametrized by output types and evaluated over the annotated input_.
Intuitively, the formula $\mathsf{move}_{\tau}(y,z)$ states how the origin of
every output position of type $\tau$ changes from $y$ to $z$. We refer to $y$
and $z$ as _source_ and _target_ origin, respectively. The formula
$\mathsf{next}_{\tau,\tau^{\prime}}(z,z^{\prime})$ instead constrains the
target origins $z,z^{\prime}$ of any two consecutive output positions with
types $\tau$ and $\tau^{\prime}$, respectively.

Formally,
$\mathcal{R}=(\overline{I},\overline{O},\mathsf{ipar},\mathsf{opar},(\mathsf{move}_{\tau}),(\mathsf{next}_{\tau,\tau^{\prime}}))$
defines the resynchronization consisting of all pairs
$(\sigma,\sigma^{\prime})$, with $\sigma=(u,v,\mathit{orig})$,
$\sigma^{\prime}=(u,v,\mathit{orig}^{\prime})$, $u\in\Sigma^{*}$, and
$v\in\Gamma^{*}$, for which there exist $u^{\prime}\in{\Sigma^{\prime}}^{*}$
and $v^{\prime}\in{\Gamma^{\prime}}^{*}$ such that

  * •

$\pi_{\Sigma}(u^{\prime})=u$ and $\pi_{\Gamma}(v^{\prime})=v$

  * •

$u^{\prime}$ satisfies $\mathsf{ipar}$ and $v^{\prime}$ satisfies
$\mathsf{opar}$,

  * •

$(u^{\prime},\mathit{orig}(x),\mathit{orig}^{\prime}(x))$ satisfies
$\mathsf{move}_{\tau}$ for all $\tau$-labeled output positions
$x\in\mathsf{dom}(v^{\prime})$, and

  * •

$(u^{\prime},\mathit{orig}^{\prime}(x),\mathit{orig}^{\prime}(x+1))$ satisfies
$\mathsf{next}_{\tau,\tau^{\prime}}$ for all
$x,x+1\in\mathsf{dom}(v^{\prime})$ such that $x$ and $x+1$ have label $\tau$
and $\tau^{\prime}$, respectively.

###### Example 1

Consider the following resynchronization $\mathcal{R}$. A pair
$(\sigma,\sigma^{\prime})$ belongs to $\mathcal{R}$ if
$\sigma=(uv,uwv,\mathit{orig})$,
$\sigma^{\prime}=(uv,uwv,\mathit{orig}^{\prime})$, with $u,v,w\in\Sigma^{+}$.
The origins $\mathit{orig}$ and $\mathit{orig}^{\prime}$ are both the identity
over $u$ and $v$. The origin of every position of $w$ in $\sigma$ (hence a
source origin) is either the first or the last position of $v$. The origin of
every position of $w$ in $\sigma^{\prime}$ (a target origin) is the first
position of $v$.

This resynchronization is described by a regular resynchronizer that uses two
input parameters $I_{1},I_{2}$ to mark the last and the first positions of $v$
in the input, and one output parameter $O$ to mark the factor $w$ in the
output. The formula $\mathsf{move}_{\tau}(y,z)$ is either $(I_{1}(y)\vee
I_{2}(y))\wedge I_{2}(z)$ or $(y=z)$, depending on whether the type $\tau$
describes a position inside $w$ or a position outside $w$.

We now turn to describing some important restrictions on (regular)
resynchronizers. Let
$\mathcal{R}=(\overline{I},\overline{O},\mathsf{ipar},\mathsf{opar},(\mathsf{move}_{\tau}),(\mathsf{next}_{\tau,\tau^{\prime}}))$
be a resynchronizer.

  * •

$\mathcal{R}$ is _$k$ -bounded_ (or just _bounded_) if for every annotated
input $u^{\prime}\in{\Sigma^{\prime}}^{*}$, every output type
$\tau\in\Gamma^{\prime}$, and every position $z$, there are at most $k$
positions $y$ such that $(u^{\prime},y,z)$ satisfies $\mathsf{move}_{\tau}$.
Recall that $y,z$ are input positions.

  * •

$\mathcal{R}$ is _$T$ -preserving_ for a given transducer $T$, if every
$\sigma\in{[\\![T]\\!]}_{o}$ belongs to the domain of $\mathcal{R}$.

  * •

$\mathcal{R}$ is _partially bijective_ if each $\mathsf{move}_{\tau}$ formula
defines a partial, bijective function from source origins to target origins.
Observe that this property implies that $\mathcal{R}$ is 1-bounded.

The boundedness restriction rules out resynchronizations such as the universal
one, that imposes no restriction on the change of origins. It is a decidable
restriction [7], and it guarantees that definability by two-way transducers is
effectively preserved under regular resynchronizations, modulo common guess.
More precisely, Theorem 16 in [7] shows that, given a bounded regular
resynchronizer $\mathcal{R}$ and a transducer $T$, one can construct a
transducer $T^{\prime}$ with common guess that is origin-equivalent to
$\mathcal{R}(T)$.

######  Example 1 (continued)

Consider again the regular resynchronizer $\mathcal{R}$ described in the
previous example. Note that $\mathcal{R}$ is $2$-bounded, since at most two
source origins are redirected to the same target origin. If we used an
additional output parameter to distinguish, among the positions of $w$, those
that have source origin in the first position of $v$ and those that have
source origin in the last position of $v$, we would get a $1$-bounded, regular
resynchronizer.

We state below two crucial properties of regular resynchronizers (the second
lemma is reminiscent of Lemma 11 from [21], which proves closure of bounded
resynchronizers with vacuous $\mathsf{next}_{\tau,\tau^{\prime}}$ relations).

######  Lemma 1 ()

Every bounded, regular resynchronizer is effectively equivalent to some
$1$-bounded, regular resynchronizer.

######  Lemma 2 ()

The class of bounded, regular resynchronizers is effectively closed under
composition.

###  3.2 Main result

Given a two-way transducer $T$ one can ask if it is origin-equivalent to some
one-way transducer. It was observed in [4] that this property holds if and
only if all synchronized pairs defined by $T$ are _order-preserving_ , namely,
for all $\sigma=(u,v,\mathit{orig})\in{[\\![T]\\!]}_{o}$ and all
$y,y^{\prime}\in\mathsf{dom}(v)$, with $y<y^{\prime}$, we have
$\mathit{orig}(y)\leq\mathit{orig}(y^{\prime})$. The decidability of the above
question should be contrasted to the analogous question in the classical
semantics: “is a given two-way transducer classically equivalent to some one-
way transducer?” The latter problem turns out to be decidable for functional
transducers [14, 3], but is undecidable for arbitrary two-way transducers [2].

Here we are interested in a different, more relaxed notion:

###### Definition 1

A transducer $T$ is called _one-way resynchronizable_ if there exists a
bounded, regular resynchronizer $\mathcal{R}$ that is $T$-preserving and such
that $\mathcal{R}(T)$ is order-preserving.

Note that if $T^{\prime}$ is an order-preserving transducer, then one can
construct rather easily a one-way transducer $T^{\prime\prime}$ such that
$T^{\prime}=_{o}T^{\prime\prime}$, by eliminating non-productive U-turns from
accepting runs.

Moreover, note that without the condition of being $T$-preserving every
transducer $T$ would be one-way resynchronizable, using the empty
resynchronization.

###### Example 2

Consider the transducer $T_{1}$ that moves the last letter of the input $wa$
to the front by a first left-to-right pass that outputs the last letter $a$,
followed by a right-to-left pass without output, and finally by a left-to-
right pass that produces the remaining $w$. Let $\mathcal{R}$ be the bounded
regular resynchronizer that redirects the origin of the last $a$ to the first
position. Assuming an output parameter $O$ with an interpretation constrained
by $\mathsf{opar}$ that marks the last position of the output, the formula
$\mathsf{move}_{(a,1)}(y,z)$ says that target origin $z$ (source origin $y$,
resp.) of the last $a$ is the first (last, resp.) position of the input. It is
easy to see that $\mathcal{R}(T_{1})$ is origin-equivalent to the one-way
transducer that on input $wa$, guesses $a$ and outputs $aw$. Thus, $T_{1}$ is
one-way resynchronizable. See also Figure 1.

###### Example 3

Consider the transducer $T_{2}$ that reads inputs of the form $u\\#v$ and
outputs $vu$ in the obvious way, by a first left-to-right pass that outputs
$v$, followed by a right-to-left pass, and a finally a left-to-right pass that
outputs $u$. Using the characterization with the notion of cross-width that we
introduce below, it can be shown that $T_{2}$ is not one-way resynchronizable.

In order to give a flavor of our results, we anticipate here the two main
theorems, before introducing the key technical concepts of cross-width and
inversion (these will be defined further below).

###### Theorem 3.1

For every bounded-visit transducer $T$, the following are equivalent:

  * (1)

$T$ is one-way resynchronizable,

  * (2)

the cross-width of $T$ is finite,

  * (3)

no successful run of $T$ has inversions,

  * (4)

there is a partially bijective, regular resynchronizer $\mathcal{R}$ that is
$T$-preserving and such that $\mathcal{R}(T)$ is order-preserving.

Moreover, condition (3) is decidable.

We will use Theorem 3.1 to show that one-way resynchronizability is decidable
for arbitrary two-way transducers (not just bounded-visit ones).

###### Theorem 3.2

It is decidable whether a given two-way transducer $T$ is one-way
resynchronizable.

Let us now introduce the first key concept, that of cross-width:

######  Definition 2 (cross-width)

Let $\sigma=(u,v,\mathit{orig})$ be a synchronized pair and let
$X_{1},X_{2}\subseteq\mathsf{dom}(v)$ be sets of output positions such that,
for all $x_{1}\in X_{1}$ and $x_{2}\in X_{2}$, $x_{1}<x_{2}$ and
$\mathit{orig}(x_{1})>\mathit{orig}(x_{2})$. We call such a pair
$(X_{1},X_{2})$ a _cross_ and define its _width_ as
$\min(|\mathit{orig}(X_{1})|,|\mathit{orig}(X_{2})|)$, where
$\mathit{orig}(X)=\\{\mathit{orig}(x)\mid x\in X\\}$ is the set of origins
corresponding to a set $X$ of output positions.

The _cross-width_ of a synchronized pair $\sigma$ is the maximal width of the
crosses in $\sigma$. A transducer has _bounded cross-width_ if for some
integer $k$, all synchronized pairs associated with successful runs of $T$
have cross-width at most $k$.

For instance, the transducer $T_{2}$ in Example 3 has unbounded cross-width.
In contrast, the transducer $T_{1}$ in Example 2 has cross-width one.

The other key notion of _inversion_ will be introduced formally in the next
section (page 3), as it requires a few technical definitions. The notion
however is very similar in spirit to that of cross, with the difference that a
single inversion is sufficient for witnessing a family of crosses with
arbitrarily large cross-width.

##  4 Proof overview for Theorem 3.1

This section provides an overview of the proof of Theorem 3.1, and introduces
the main ingredients.

We will use flows (a concept inspired from crossing sequences [22, 3] and
revised in Section 4.1) in order to derive the key notion of inversion.
Roughly speaking, an inversion in a run involves two loops that produce
outputs in an order that is reversed compared to the order on origins.
Inversions were also used in the characterization of one-way definability of
two-way transducers under the classical semantics [3]. There, they were used
for deriving some combinatorial properties of outputs. Here we are only
interested in detecting inversions, and this is a simple task.

Flows will also be used to associate factorization trees with runs (the
existence of factorization trees of bounded height was established by the
celebrated Simon’s factorization theorem [23]). We will use a structural
induction on these factorization trees and the assumption that there is no
inversion in every run to construct a regular resynchronization witnessing
one-way resynchronizability of the transducer at hand.

Another important ingredient underlying the main characterization is given by
the notion of dominant output interval (Section 4.2), which is used to
formalize the invariant of our inductive construction.

###  4.1 Flows and inversions

#### Intervals.

An _interval_ of a word is a set of consecutive positions in it. An interval
is often denoted by $I=[i,i^{\prime})$, with $i=\min(I)$ and
$i^{\prime}=\max(I)+1$. Given two intervals $I=[i,i^{\prime})$ and
$J=[j,j^{\prime})$, we write $I<J$ if $i^{\prime}\leq j$, and we say that
$I,J$ are adjacent if $i^{\prime}=j$. The union of two adjacent intervals
$I=[i,i^{\prime})$, $J=[j,j^{\prime})$, denoted $I\cdot J$, is the interval
$[i,j^{\prime})$ (if $I,J$ are not adjacent, then $I\cdot J$ is undefined).

#### Subruns.

Given a run $\rho$ of a transducer, a _subrun_ is a factor of $\rho$. Note
that a subrun of a two-way transducer may visit a position of the input
several times. For an input interval $I=[i,j)$ and a run $\rho$, we say that a
subrun $\rho^{\prime}$ of $\rho$ _spans over $I$_ if $i$ (resp. $j$) is the
smallest (resp. greatest) input position labeling some transition of
$\rho^{\prime}$. The left hand-side of the figure at page 4.1 gives an example
of an interval $I$ of an input word together with the subruns
$\alpha_{1},\alpha_{2},\alpha_{3},\beta_{1},\beta_{2},\beta_{3}$, $\gamma_{1}$
that span over it. Subruns spanning over an interval can be left-to-right,
left-to-left, right-to-left, or right-to-right depending on where the starting
and ending positions are w.r.t. the endpoints of the interval.

#### Flows.

Flows are used to summarize subruns of a two-way transducer that span over a
given interval. The definition below is essentially taken from [3], except for
replacing “functional” by “$K$-visit”. Formally, a _flow_ of a transducer $T$
is a graph with vertices divided into two groups, $\mathsf{L}$-vertices and
$\mathsf{R}$-vertices, labeled by states of $T$, and with directed edges also
divided into two groups, productive and non-productive edges. The graph
satisfies the following requirements. Edge sources are either an
$\mathsf{L}$-vertex labeled by a right-reading state, or an
$\mathsf{R}$-vertex labeled by a left-reading state, and symmetrically for
edge destinations; moreover, edges are of one of the following types:
$\mathsf{L}\mathsf{L}$, $\mathsf{L}\mathsf{R}$, $\mathsf{R}\mathsf{L}$,
$\mathsf{R}\mathsf{R}$. Second, each node is the endpoint of exactly one edge.
Finally, $\mathsf{L}$ ($\mathsf{R}$, resp.) vertices are totally ordered, in
such a way that for every $\mathsf{L}\mathsf{L}$ ($\mathsf{R}\mathsf{R}$,
resp.) edge $(v,v^{\prime})$, we have $v<v^{\prime}$. We will only consider
flows of $K$-visiting transducers, so flows with at most $2K$ vertices. For
example, the flow in the left-hand side of the figure at page 4.1 has six
$\mathsf{L}$-vertices on the left, and six $\mathsf{R}$-vertices on the right.
The edges $\alpha_{1}$, $\alpha_{2}$, $\alpha_{3}$ are $\mathsf{L}\mathsf{L}$,
$\mathsf{L}\mathsf{R}$, and $\mathsf{R}\mathsf{R}$, respectively.

Given a run $\rho$ of $T$ and an interval $I=[i,i^{\prime})$ on the input,
_the flow of $\rho$ on $I$_, denoted $\mathit{flow}_{\rho}(I)$, is obtained by
identifying every configuration at position $i$ (resp. $i^{\prime}$) with an
$\mathsf{L}$ (resp. $\mathsf{R}$) vertex, labeled by the state of the
configuration, and every subrun spanning over $I$ with an edge connecting the
appropriate vertices (this subrun is called the _witnessing subrun_ of the
edge of the flow). An edge is said to be _productive_ if its witnessing subrun
produces non-empty output.

#### Flow monoid.

The composition of two flows $F$ and $G$ is defined when the
$\mathsf{R}$-vertices of $F$ induce the same sequence of labels as the
$\mathsf{L}$-vertices of $G$. In this case, the composition results in the
flow $F\cdot G$ that has as vertices the $\mathsf{L}$-vertices of $F$ and the
$\mathsf{R}$-vertices of $G$, and for edges the directed paths in the graph
obtained by glueing the $\mathsf{R}$-vertices of $F$ with the
$\mathsf{L}$-vertices of $G$ so that states are matched. Productiveness of
edges is inherited by paths, implying that an edge of $F\cdot G$ is productive
if and only if the corresponding path contains at least one edge (from $F$ or
$G$) that is productive. When the composition is undefined, we simply write
$F\cdot G=\bot$. The above definitions naturally give rise to a _flow monoid_
associated with the transducer $T$, where elements are the flows of $T$,
extended with a dummy element $\bot$, and the product operation is given by
the composition of flows, with the convention that $\bot$ is absorbing. It is
easy to verify that for any two adjacent intervals $I<J$ of a run $\rho$,
$\mathit{flow}_{\rho}(I)\cdot\mathit{flow}_{\rho}(J)=\mathit{flow}_{\rho}(I\cdot
J)$. We denote by $M_{T}$ the _flow monoid_ of a $K$-visiting transducer $T$.

Let us estimate the size of $M_{T}$. If $Q$ is the set of states of $T$, there
are at most $|Q|^{2K}$ possible sequences of $\mathsf{L}$ and
$\mathsf{R}$-vertices; and the number of edges (marked as productive or not)
is bounded by ${2K\choose K}\cdot(2K)^{K}\cdot 2^{K}\leq(2K+1)^{2K}$.
Including the dummy element $\bot$ in the flow monoid, we get
$|M_{T}|\leq(|Q|\cdot(2K+1))^{2K}+1=:\mathbf{M}$.

#### Loops.

A loop of a run $\rho$ over input $w$ is an interval $I=[i,j)$ with a flow
$F=$ $\mathit{flow}_{\rho}(I)$ such that $F\cdot F=F$ (call $F$ _idempotent_).
The run $\rho$ can be pumped on a loop $I=[i,j)$ as expected: given $n>0$, we
let $\mathit{pump}^{n}_{I}(\rho)$ be the run obtained from $\rho$ by glueing
the subruns that span over the intervals $[1,i)$ and $[j,|w|+1)$ with $n$
copies of the subruns spanning over $I$ (see figure to the right). X
$I$$\boldsymbol{\alpha_{1}}$$~{}\boldsymbol{\alpha_{2}}$$\boldsymbol{\alpha_{3}}$$\boldsymbol{\beta_{1}}$$\boldsymbol{\beta_{2}}$$\boldsymbol{\beta_{3}}$$~{}\boldsymbol{\gamma_{1}}$01234560123456$I$$2$
more copies of
$I$$\boldsymbol{\alpha_{1}}$$~{}\boldsymbol{\alpha_{2}}$$\boldsymbol{\alpha_{1}}$$\boldsymbol{\alpha_{3}}$$~{}\boldsymbol{\alpha_{2}}$$\boldsymbol{\alpha_{1}}$$\boldsymbol{\alpha_{3}}$$~{}\boldsymbol{\alpha_{2}}$$\boldsymbol{\alpha_{3}}$$\boldsymbol{\beta_{1}}$$\boldsymbol{\beta_{2}}$$\boldsymbol{\beta_{1}}$$\boldsymbol{\beta_{3}}$$\boldsymbol{\beta_{2}}$$\boldsymbol{\beta_{1}}$$\boldsymbol{\beta_{3}}$$\boldsymbol{\beta_{2}}$$\boldsymbol{\beta_{3}}$$~{}\boldsymbol{\gamma_{1}}$$~{}\boldsymbol{\gamma_{1}}$$~{}\boldsymbol{\gamma_{1}}$

The lemma below shows that the occurrence order relative to subruns witnessing
$\mathsf{L}\mathsf{R}$ or $\mathsf{R}\mathsf{L}$ edges of a loop (called
_straight edges_ , for short) is preserved when pumping the loop. This
seemingly straightforward lemma is needed for detecting inversions and its
proof is surprisingly non-trivial. For example, the external edge connecting
the two $\mathsf{L}$-vertices $1,2$ in the figure above appears before edge
$\alpha_{2}$, and also before every copy of $\alpha_{2}$ in the run where loop
$I$ is pumped.

######  Lemma 3 ()

Let $\rho$ be a run of $T$ on $u$, let $J<I<K$ be a partition of the domain of
$u$ into intervals, with $I$ loop of $\rho$, and let
$F=\mathit{flow}_{\rho}(J)$, $E=\mathit{flow}_{\rho}(I)$, and
$G=\mathit{flow}_{\rho}(K)$ be the corresponding flows. Consider an arbitrary
edge $f$ of either $F$ or $G$, and a straight edge $e$ of the idempotent flow
$E$. Let $\rho_{f}$ and $\rho_{e}$ be the witnessing subruns of $f$ and $e$,
respectively. Then the occurrence order of $\rho_{f}$ and $\rho_{e}$ in $\rho$
is the same as the occurrence order of $\rho_{f}$ and any copy of $\rho_{e}$
in $\mathit{pump}^{n}_{I}(\rho)$.

We can now formalize the key notion of inversion:

######  Definition 3 (inversion)

An _inversion_ of $\rho$ is a tuple $(I,e,I^{\prime},e^{\prime})$ such that  •
$I,I^{\prime}$ are loops of $\rho$ and $I<I^{\prime}$, • $e,e^{\prime}$ are
productive straight edges in $\mathit{flow}_{\rho}(I)$ and
$\mathit{flow}_{\rho}(I^{\prime})$ respectively, • the subrun witnessing
$e^{\prime}$ precedes the subrun witnessing $e$ in the run order (see the
figure to the right). X
$I$$\boldsymbol{\alpha_{1}}$$~{}\boldsymbol{\alpha_{2}}$$\boldsymbol{\alpha_{3}}$$\boldsymbol{\beta_{1}}$$\boldsymbol{\beta_{2}}$$\boldsymbol{\beta_{3}}$$~{}\boldsymbol{\gamma_{1}}$$I$$I^{\prime}$$\boldsymbol{e^{\prime}}\
\ \ $$\ \ \ \boldsymbol{e}$

###  4.2 Dominant output intervals

In this section we identify some particular intervals of the output that play
an important role in the inductive construction of the resynchronizer for a
one-way resynchronizable transducer.

Given $n\in\mathbb{N}$, we say that a set $B$ of output positions is _$n$
-large_ if $|\mathit{orig}(B)|>n$; otherwise, we say that $B$ is _$n$ -small_.
Recall that here we work with a $K$-visiting transducer $T$, for some constant
$K$, and that $\mathbf{M}=(|Q|\cdot(2K+1))^{2K}+1$ is an upper bound to the
size of the flow monoid $M_{T}$. We will extensively use the derived constant
$\mathbf{C}=\mathbf{M}^{2K}$ to distinguish between large and small sets of
output positions. The intuition behind this constant is that any set of output
positions that is $\mathbf{C}$-large must traverse a loop of $\rho$. This is
formalized in the lemma below. The proof uses algebraic properties of the flow
monoid $M_{T}$ [20] (see also Theorem 7.2 in [3], which proves a similar
result, but with a larger constant derived from Simon’s factorization
theorem):

######  Lemma 4 ()

Let $I$ be an input interval and $B$ a set of output positions with origins
inside $I$. If $B$ is $\mathbf{C}$-large, then there is a loop $J\subseteq I$
of $\rho$ such that $\mathit{flow}_{\rho}(J)$ contains a productive straight
edge witnessed by a subrun that intersects $B$ (in particular,
$\mathit{out}(J)\cap B\neq\emptyset$).

We need some more notations for outputs. Given an input interval $I$ we denote
by $\mathit{out}_{\rho}(I)$ the set of output positions whose origins belong
to $I$ (note that this might not be an output interval). An _output block_ of
$I$ is a maximal interval contained in $\mathit{out}_{\rho}(I)$.

The _dominant output interval_ of $I$, denoted $\mathit{bigout}_{\rho}(I)$, is
the smallest output interval that contains all $\mathbf{C}$-large output
blocks of $I$. In particular, $\mathit{bigout}_{\rho}(I)$ either is empty or
begins with the first $\mathbf{C}$-large output block of $I$ and ends with the
last $\mathbf{C}$-large outblock block of $I$. We will often omit the
subscript $\rho$ from the notations $\mathit{flow}_{\rho}(I)$,
$\mathit{out}_{\rho}(I),\mathit{bigout}_{\rho}(I)$, etc., when no confusion
arises.

We now fix a successful run $\rho$ of the $K$-visiting transducer $T$. The
rest of the section presents some technical lemmas that will be used in the
inductive constructions for the proof of the main theorem. _In the lemmas
below, we assume that all successful runs of $T$ (in particular, $\rho$) avoid
inversions._

######  Lemma 5 ()

Let $I_{1}<I_{2}$ be two input intervals and $B_{1},B_{2}$ output blocks of
$I_{1}$, $I_{2}$, respectively. If both $B_{1},B_{2}$ are $\mathbf{C}$-large,
then $B_{1}<B_{2}$.

######  Proof (sketch)

If the claim would not hold, then Lemma 4 would provide some loops
$J_{1}\subseteq I_{1}$ and $J_{2}\subseteq I_{2}$, together with some
productive edges in them, witnessing an inversion. ∎

######  Lemma 6 ()

Let $I=I_{1}\cdot I_{2}$, $B=\mathit{bigout}(I)$, and
$B_{i}=\mathit{bigout}(I_{i})$ for $i=1,2$. Then $B\setminus(B_{1}\cup B_{2})$
is $4K\mathbf{C}$-small.

######  Proof (sketch)

By Lemma 5, $B_{1}<B_{2}$. Moreover, all $\mathbf{C}$-large output blocks of
$I_{1}$ or $I_{2}$ are also $\mathbf{C}$-large output blocks of $I$, so $B$
contains both $B_{1}$ and $B_{2}$. Suppose, by way of contradiction, that
$B\setminus(B_{1}\cup B_{2})$ is $4K\mathbf{C}$-large. This means that there
is a $2K\mathbf{C}$-large set $S\subseteq B\setminus(B_{1}\cup B_{2})$ with
origins entirely to the left of $I_{2}$, or entirely to the right of $I_{1}$.
Suppose, w.l.o.g., that the former case holds, and decompose $S$ as a union of
maximal output blocks $B^{\prime}_{1},B^{\prime}_{2},\dots,B^{\prime}_{n}$
with origins either entirely inside $I_{1}$, or entirely outside. Since $S\cap
B_{1}=\emptyset$, every block $B^{\prime}_{i}$ with origins inside $I_{1}$ is
$\mathbf{C}$-small. Similarly, by Lemma 0.C.1 in Appendix 0.C, every block
$B^{\prime}_{i}$ with origins outside $I_{1}$ is $\mathbf{C}$-small too.
Moreover, since $\rho$ is $K$-visiting, we get $n\leq 2K$. Altogether, this
contradicts the assumption that $S$ is $2K\mathbf{C}$-large. ∎

######  Lemma 7 ()

Let $I=I_{1}\cdot I_{2}\cdots I_{n}$, such that $I$ is a loop and
$\mathit{flow}(I)=\mathit{flow}(I_{k})$ for all $k$. Then $\mathit{bigout}(I)$
can be decomposed as $B_{1}\cdot J_{1}\cdot B_{2}\cdot J_{2}\cdot\dots\cdot
J_{n-1}\cdot B_{n}$, where

  1. 1.

for all $1\leq k\leq n$, $B_{k}=\mathit{bigout}(I_{k})$ (with $B_{k}$ possibly
empty);

  2. 2.

for all $1\leq k<n$, the positions in $J_{k}$ have origins inside $I_{k}\cup
I_{k+1}$ and $J_{k}$ is $2K\mathbf{C}$-small.

######  Proof (sketch)

The proof idea is similar to the previous lemma. First, using properties of
idempotent flows, one shows that all output positions strictly between $B_{k}$
and $B_{k+1}$, for any $k=1,\dots,n-1$, have origin in $I_{k}\cup I_{k+1}$.
Then, one observes that every output block of $I_{k}$ disjoint from $B_{k}$ is
$\mathbf{C}$-small, and since  $T$ is $K$-visiting there are at most $K$ such
blocks. This shows that every output interval $J_{k}$ between $B_{k}$ and
$B_{k+1}$ is $2K\mathbf{C}$-small. For an illustration see the figure to the
right. The $\mathbf{C}$-large blocks in $I_{1}$ are shown in red; in blue
those for $I_{2}$, in purple those for $I_{3}$. So $\mathit{bigout}(I_{1})$ is
the entire output between the two red dots, $\mathit{bigout}(I_{2})$ between
the two blue dots, and $\mathit{bigout}(I_{3})$ between the purple dots. All
three blocks are non-empty, and $\mathit{bigout}(I_{1}\cdot I_{2}\cdot I_{3})$
goes from the first red to the second purple dot. Black non-dashed arrows
stand for $\mathbf{C}$-small blocks. ∎ X
$I$$\boldsymbol{\alpha_{1}}$$~{}\boldsymbol{\alpha_{2}}$$\boldsymbol{\alpha_{3}}$$\boldsymbol{\beta_{1}}$$\boldsymbol{\beta_{2}}$$\boldsymbol{\beta_{3}}$$~{}\boldsymbol{\gamma_{1}}$$I_{1}$$I_{2}$$I_{3}$

##  5 Proof of Theorem 3.1

This section is devoted to proving the characterization of one-way
resynchronizability in the bounded-visit case. We will use the notion of
_bounded-traversal_ from [21], that was shown to characterize the class of
bounded regular resynchronizers, in as much as bounded-delay characterizes
rational resynchronizers [15].

######  Definition 4 (traversal [21])

Let $\sigma=(u,v,\mathit{orig})$ and
$\sigma^{\prime}=(u,v,\mathit{orig}^{\prime})$ be two synchronized pairs with
the same input and output words.

Given two input positions $y,y^{\prime}\in\mathsf{dom}(u)$, we say that _$y$
traverses $y^{\prime}$_ if there is a pair $(y,z)$ of source and target
origins associated with the same output position such that $y^{\prime}$ is
between $y$ and $z$, with $y^{\prime}\neq z$ and possibly $y^{\prime}=y$. More
precisely:

  * •

$(y,y^{\prime})$ is a _left-to-right traversal_ if $y\leq y^{\prime}$ and for
some output position $x$, $\mathit{orig}(x)=y$ and
$z=\mathit{orig}^{\prime}(x)>y^{\prime}$;

  * •

$(y,y^{\prime})$ is a _right-to-left traversal_ if $y\geq y^{\prime}$ and for
some output position $x$, $\mathit{orig}(x)=y$ and
$z=\mathit{orig}^{\prime}(x)<y^{\prime}$.

A pair $(\sigma,\sigma^{\prime})$ of synchronized pairs with input $u$ and
output $v$ is said to have _$k$ -bounded traversal_, with $k\in\mathbb{N}$, if
every $y^{\prime}\in\mathsf{dom}(u)$ is traversed by at most $k$ distinct
positions of $\mathsf{dom}(u)$.

A resynchronizer $\mathcal{R}$ has _bounded traversal_ if there is some
$k\in\mathbb{N}$ such that every $(\sigma,\sigma^{\prime})\in\mathcal{R}$ has
$k$-bounded traversal.

######  Lemma 8 ([21])

A regular resynchronizer is bounded if and only if it has bounded traversal.

######  Proof (of Theorem 3.1)

First of all, observe that the implication $4\rightarrow 1$ is
straightforward. To prove the implication $1\rightarrow 2$, assume that there
is a $k$-bounded, regular resynchronizer $\mathcal{R}$ that is $T$-preserving
and such that $\mathcal{R}(T)$ is order-preserving. Lemma 8 implies that
$\mathcal{R}$ has $t$-bounded traversal, for some constant $t$. We head
towards proving that $T$ has cross-width bounded by $t+k$. Consider two
synchronized pairs $\sigma=(u,v,\mathit{orig})$ and
$\sigma^{\prime}=(u,v,\mathit{orig}^{\prime})$ such that
$\sigma\in{[\\![T]\\!]}_{o}$ and $(\sigma,\sigma^{\prime})\in\mathcal{R}$, and
consider a cross $(X_{1},X_{2})$ of $\sigma$. We claim that
$|\mathit{orig}(X_{1})|$ or $|\mathit{orig}(X_{2})|$ is at most $t+k$. Let
$x_{1}=\min(\mathit{orig}(X_{1}))$,
$x^{\prime}_{1}=\max(\mathit{orig}^{\prime}(X_{1}))$,
$x_{2}=\max(\mathit{orig}(X_{1}))$, and
$x^{\prime}_{2}=\min(\mathit{orig}^{\prime}(X_{2}))$. Since $(X_{1},X_{2})$ is
a cross, we have $x_{1}>x_{2}$, and since $\sigma^{\prime}$ is order-
preserving, we have $x^{\prime}_{1}\leq x^{\prime}_{2}$. Now, if
$x^{\prime}_{1}>x_{2}$, then at least $|\mathit{orig}(X_{2})|-k$ input
positions from $X_{2}$ traverse $x^{\prime}_{1}$ to the right (the $-k$ term
is due to the fact that at most $k$ input positions can be resynchronized to
$x^{\prime}_{1}$). Symmetrically, if $x^{\prime}_{1}\leq x_{2}$, then at least
$|\mathit{orig}(X_{1})|-k$ input positions from $X_{1}$ traverse $x_{2}$ to
the left (the $-k$ term accounts for the case where some positions are
resynchronized to $x^{\prime}_{1}$ and $x^{\prime}_{1}=x_{2}$). This implies
$\min(|\mathit{orig}(X_{1})|,|\mathit{orig}(X_{2})|)\leq t+k$, as claimed.

The remaining implications rely on the assumption that $T$ is bounded-visit.

The implication $2\rightarrow 3$ is shown by contraposition: one considers a
successful run $\rho$ with an inversion, and shows that crosses of arbitrary
width emerge after pumping the loops of the inversion (here Lemma 3 is
crucial).

The proof of $3\rightarrow 4$ is more involved, we only sketch it here.
Assuming that no successful run of $T$ has inversions we build a partially
bijective, regular resynchronizer $\mathcal{R}$ that is $T$-preserving and
$\mathcal{R}(T)$ is order-preserving. The resynchronizer $\mathcal{R}$ uses
some parameters to guess a successful run $\rho$ of $T$ on $u$ and a
factorization tree of bounded height for $\rho$. Formally, a _factorization
tree_ for a sequence $\alpha$ of monoid elements (e.g. the flows
$\mathit{flow}_{\rho}([y,y])$ for all input positions $y$) is an ordered,
unranked tree whose yield is the sequence $\alpha$. The leaves of the
factorization tree are labeled with the elements of $\alpha$. All other nodes
have at least two children and are labeled by the monoid product of the child
labels (in our case by the flows of $\rho$ induced by the covered factors in
the input). In addition, if a node has more than two children, then all its
children must have the same label, representing an idempotent element of the
monoid. By Simon’s factorization theorem [23], every sequence of monoid
elements has some factorization tree of height at most linear in the size of
the monoid (in our case, at most $3|M_{T}|$, see e.g. [8]).

_Parameters._ We use input parameters to encode the successful run $\rho$ and
a factorization tree for $\rho$ of height at most $H=3|M_{T}|$. These
parameters specify, for each input interval corresponding to a subtree, the
start and end positions of the interval and the label of the root of the
subtree. Correctness of these annotations can be enforced by an MSO sentence
$\mathsf{ipar}$. The run and the factorization tree also need to be encoded
over the output, using output parameters. More precisely, given a level in the
tree and an output position, we need to be able to determine the flow and the
productive edge that generated that position. The technical details for
checking correctness of the output annotation using the formulas
$\mathsf{opar}$, $\mathsf{move}_{\tau}$ and
$\mathsf{next}_{\tau,\tau^{\prime}}$ can be found in Appendix 0.D.

_Moving origins._ For each level $\ell$ of the factorization tree, a partial
resynchronization relation $\mathcal{R}_{\ell}$ is defined. The relation is
partial in the sense that some output positions may not have a source-target
origin pair defined at a given level. But once a source-target pair is defined
for some output position at a given level, it remains defined for all higher
levels.

In the following we write $\mathit{bigout}(p)$ for the dominant output
interval associated with the input interval $I(p)$ corresponding to a node $p$
in the tree. For every level $\ell$ of the factorization tree, the
resynchronizer $\mathcal{R}_{\ell}$ will be a partial function from source
origins to target origins, and will satisfy the following:

  * •

the set of output positions for which $\mathcal{R}_{\ell}$ defines target
origins is the union of the intervals $\mathit{bigout}(p)$ for all nodes $p$
at level $\ell$;

  * •

$\mathcal{R}_{\ell}$ only moves origins within the same interval at level
$\ell$, that is, $\mathcal{R}_{\ell}$ defines only pairs $(y,z)$ of source-
target origins such that $y,z\in I(p)$ for some node $p$ at level $\ell$;

  * •

the target origins defined by $\mathcal{R}_{\ell}$ are order-preserving within
every interval at level $\ell$, that is, for all output positions
$x<x^{\prime}$, if $\mathcal{R}_{\ell}$ defines the target origins of
$x,x^{\prime}$ to be $z,z^{\prime}$, respectively, and if $z,z^{\prime}\in
I(p)$ for some node $p$ at level $\ell$, then $z\leq z^{\prime}$;

  * •

$\mathcal{R}_{\ell}$ is $\ell\cdot 4K\mathbf{C}$-bounded, namely, there are at
most $\ell\cdot 4K\mathbf{C}$ distinct source origins that are moved by
$\mathcal{R}_{\ell}$ to the same target origin.

The construction of $\mathcal{R}_{\ell}$ is by induction on $\ell$. For a
binary node $p$ at level $\ell$ with children $p_{1},p_{2}$, the
resynchronizer $\mathcal{R}_{\ell}$ inherits the source-origin pairs from
level $\ell-1$ for output positions that belong to
$\mathit{bigout}(p_{1})\cup\mathit{bigout}(p_{2})$. Note that
$\mathit{bigout}(p_{1})<\mathit{bigout}(p_{2})$ by Lemma 5, so
$\mathcal{R}_{\ell}$ is order-preserving inside
$\mathit{bigout}(p_{1})\cup\mathit{bigout}(p_{2})$. Output positions inside
$\mathit{bigout}(p)\setminus(\mathit{bigout}(p_{1})\cup\mathit{bigout}(p_{2}))$
are moved in an order-preserving manner to one of the extremities of $I(p)$,
or to the last position of $I(p_{1})$. Boundedness of $\mathcal{R}_{\ell}$ is
guaranteed by Lemma 6.

The case where $p$ is an idempotent node at level $\ell$ with children
$p_{1},p_{2},\dots,p_{n}$ follows a similar approach. For brevity, let
$I_{i}=I(p_{i})$ and $B_{i}=\mathit{bigout}(p_{i})$, and observe that, by
Lemma 5, $B_{1}<B_{2}<\dots<B_{n}$. Lemma 7 provides a decomposition of
$\mathit{bigout}(p)$ as $B_{1}\cdot J_{1}\cdot B_{2}\cdot J_{2}\cdot\dots\cdot
J_{n-1}\cdot B_{n}$, for some $2K\mathbf{C}$-small output intervals $J_{k}$
with origins inside $I_{k}\cup I_{k+1}$, for $k=1,\dots,n-1$. As before, the
resynchronizer $\mathcal{R}_{\ell}$ behaves exactly as $\mathcal{R}_{\ell-1}$
for the output positions inside the $B_{k}$’s. For any other output position,
say $x\in J_{k}$, the resynchronizer $\mathcal{R}_{\ell}$ will move the origin
either to the last position of $I_{k}$ or to the first position of $I_{k+1}$,
depending on whether the source origin of $x$ belongs to $I_{k}$ or $I_{k+1}$.
∎

##  6 Proof overview of Theorem 3.2

The main obstacle towards dropping the bounded-visit restriction from Theorem
3.1, while maintaining the effectiveness of the characterization, is the lack
of a bound on the number of flows. Indeed, for a transducer $T$ that is not
necessarily bounded-visit, there is no bound on the number of flows that
encode successful runs of $T$, and thus the proofs of the implications
$2\rightarrow 3\rightarrow 4$ are not applicable anymore. However, the proofs
of the implications $1\rightarrow 2$ and $4\rightarrow 1$ remain valid, even
for a transducer $T$ that is not bounded-visit.

The idea for proving Theorem 3.2 is to transform $T$ into an equivalent
bounded-visit transducer $\mathit{low}(T)$, so that the property of one-way
resynchronizability is preserved. More precisely, given a two-way transducer
$T$, we construct:

  1. 1.

a bounded-visit transducer $\mathit{low}(T)$ that is classically equivalent to
$T$,

  2. 2.

a $1$-bounded, regular resynchronizer $\mathcal{R}$ that is $T$-preserving and
such that $\mathcal{R}(T)=_{o}\mathit{low}(T)$.

We can apply our characterization of one-way resynchronizability in the
bounded-visit case to the transducer $\mathit{low}(T)$. If $\mathit{low}(T)$
is one-way resynchronizable, then by Theorem 3.1 we obtain another partially
bijective, regular resynchronizer $\mathcal{R}^{\prime}$ that is
$\mathit{low}(T)$-preserving and such that
$\mathcal{R}^{\prime}(\mathit{low}(T)))$ is order-preserving. Thanks to Lemma
2, the resynchronizers $\mathcal{R}$ and $\mathcal{R}^{\prime}$ can be
composed, so we conclude that the original transducer $T$ is one-way
resynchronizable. Otherwise, if $\mathit{low}(T)$ is not one-way
resynchronizable, we show that neither is $T$. This is precisely shown in the
lemma below.

######  Lemma 9 ()

For all transducers $T,T^{\prime}$, with $T^{\prime}$ bounded-visit, and for
every partially bijective, regular resynchronizer $\mathcal{R}$ that is
$T$-preserving and such that $\mathcal{R}(T)=_{o}T^{\prime}$, $T$ is one-way
resynchronizable if and only if $T^{\prime}$ is one-way resynchronizable.

There are however some challenges in the approach described above. First, as
$T$ may output arbitrarily many symbols with origin in the same input
position, and $\mathit{low}(T)$ is bounded-visit, we need $\mathit{low}(T)$ to
be able to produce arbitrarily long outputs within a single transition. For
this reason, we allow $\mathit{low}(T)$ to be a transducer with _regular
outputs_. The transition relation of such a transducer consists of finitely
many tuples of the form $(q,a,L,q^{\prime})$, with $q,q^{\prime}\in Q$,
$a\in\Sigma$, and $L\subseteq\Gamma^{*}$ a regular language over the output
alphabet. The semantics of a transition rule $(q,a,L,q^{\prime})$ is that,
upon reading $a$, the transducer can switch from state $q$ to state
$q^{\prime}$, and move its head accordingly, while outputting any word from
$L$. We also need to use transducers with common guess. Both extensions,
regular outputs and common guess, already appeared in prior works (cf. [5,
7]), and the proof of Theorem 3.1 in the bounded-visit case can be easily
adapted to these features.

There is still another problem: we cannot always expect that there exists a
bounded-visit transducer $\mathit{low}(T)$ classically equivalent to $T$.
Consider, for instance, the transducer that performs several passes on the
input, and on each left-to-right pass, at an arbitrary input position, it
copies as output the letter under its head. It is easy to see that the Parikh
image of the output is an exact multiple of the Parikh image of the input, and
standard pumping arguments show that no bounded-visit transducer can realize
such a relation.

A solution to this second problem is as follows. Before trying to construct
$\mathit{low}(T)$, we test whether $T$ satisfies the following condition on
vertical loops (these are runs starting and ending at the same position and at
the same state). There should exist some $K$ such that $T$ is _$K$ -sparse_,
meaning that the number of different origins of outputs generated inside some
vertical loop is at most $K$. If this condition is not met, then we show that
$T$ has unbounded cross-width, and hence, by the implication $1\rightarrow 2$
of Theorem 3.1, $T$ is not one-way resynchronizable. Otherwise, if the
condition holds, then we show that a bounded-visit transducer
$\mathit{low}(T)$ equivalent to $T$ can indeed be constructed.

##  7 Complexity

We discuss the effectiveness and complexity of our characterization. For a
$k$-visit transducer $T$, the effectiveness of the characterization relies on
detecting inversions in successful runs of $T$. It is not difficult to see
that this can be decided in space that is polynomial in the size of $T$ and
the bound $k$. We can also show that one-way resynchronizability is Pspace-
hard. For this we recall that the emptiness problem for two-way finite
automata is Pspace-complete. Let $A$ be a two-way automaton accepting some
language $L$, and let $\Sigma$ be a binary alphabet disjoint from that of $L$.
The function $\\{(w\cdot a_{1}\dots a_{n},a_{n}\dots a_{1})\mid w\in
L,a_{1}\dots a_{n}\in\Sigma^{*},n\geq 0\\}$ can be realized by a two-way
transducer $T$ of size polynomial in $|A|$, and $T$ is one-way
resynchronizable if and only if $L$ is empty.

In the unrestricted case, we showed that one-way resynchronizability is
decidable (Theorem 3.2). We briefly outline the complexity of the decision
procedure:

  1. 1.

First one checks that $T$ is $K$-sparse for some $K$. To do this, we construct
from $T$ the regular language $L$ of all inputs with some positions marked
that correspond to origins produced within the same vertical loop. Bounded
sparsity is equivalent to having a uniform bound on the number of marked
positions in every input from $L$. Standard techniques for two-way automata
allow to decide this in space that is polynomial in the size of $T$. Moreover,
this also gives us a computable exponential bound to the largest constant $K$
for which $T$ can be $K$-sparse.

  2. 2.

Next, we construct from the $K$-sparse transducer $T$ a bounded-visit
transducer $T^{\prime}$ that is classically equivalent to $T$ and has
exponential size.

  3. 3.

Finally, we decide one-way resynchronizability of $T^{\prime}$ by detecting
inversions in successful runs of $T^{\prime}$ (Theorem 3.1).

Summing up, one can decide one-way resynchronizability of unrestricted two-way
transducers in exponential space. It is open if this bound is optimal. We also
do not have any interesting bound on the size of the resynchronizer that
witnesses one-way resynchronizability, both in the bounded-visit case and in
the unrestricted case. Similarly, we lack upper and lower bounds on the size
of the resynchronized one-way transducers, when these exist.

##  8 Conclusions

As the main contribution of this paper, we provided a characterization for the
subclass of two-way transducers that are one-way resynchronizable, namely,
that can be transformed by some bounded, regular resynchronizer, into an
origin-equivalent one-way transducer.

There are similar definability problems that emerge in the origin semantics.
For instance, one could ask whether a given two-way transducer can be
resynchronized, through some bounded, regular resynchronization, to a relation
that is origin-equivalent to a first-order transduction. This can be seen as a
relaxation of the first-order definability problem in the origin semantics,
namely, the problem of telling whether a two-way transducer is origin-
equivalent to some first-order transduction, shown decidable in [4]. It is
worth contrasting the latter problem with the challenging open problem whether
a given transduction is equivalent to a first-order transduction in the
classical setting.

#### Acknowledgments.

We thank the FoSSaCS reviewers for their constructive and useful comments.

## References

  * [1] Rajeev Alur and Pavel Cerný.  Expressiveness of streaming string transducer.  In IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS’10), volume 8 of LIPIcs, pages 1–12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010.
  * [2] Félix Baschenis, Olivier Gauwin, Anca Muscholl, and Gabriele Puppis.  One-way definability of sweeping transducers.  In IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS’15), volume 45 of LIPIcs, pages 178–191. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
  * [3] Félix Baschenis, Olivier Gauwin, Anca Muscholl, and Gabriele Puppis.  One-way definability of two-way word transducers.  Logical Methods in Computer Science, 14(4):1–54, 2018.
  * [4] Mikolaj Bojańczyk.  Transducers with origin information.  In International Colloquium on Automata, Languages and Programming (ICALP’14), number 8572 in LNCS, pages 26–37. Springer, 2014.
  * [5] Mikolaj Bojańczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle.  Which classes of origin graphs are generated by transducers?  In International Colloquium on Automata, Languages and Programming (ICALP’17), volume 80 of LIPIcs, pages 114:1–114:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [6] Sougata Bose, Shankara Narayanan Krishna, Anca Muscholl, Vincent Penelle, and Gabriele Puppis.  On synthesis of resynchronizers for transducers.  In International Symposium on Mathematical Foundations of Computer Science (MFCS’19), volume 138 of LIPIcs, pages 69:1–69:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [7] Sougata Bose, Anca Muscholl, Vincent Penelle, and Gabriele Puppis.  Origin-equivalence of two-way word transducers is in PSPACE.  In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’18), volume 122 of LIPIcs, pages 1–18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  * [8] Thomas Colcombet.  Factorisation forests for infinite words.  In Fundamentals of Computation Theory (FCT), volume 4639 of LNCS, pages 226–237. Springer, 2007.
  * [9] 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.
  * [10] Luc Dartois, Ismaël Jecker, and Pierre-Alain Reynier.  Aperiodic string transducers.  Int. J. Found. Comput. Sci., 29(5):801–824, 2018.
  * [11] 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.
  * [12] Joost Engelfriet and Hendrik Jan Hoogeboom.  Finitary compositions of two-way finite-state transductions.  Fundamenta Informaticae, 80:111–123, 2007.
  * [13] Emmanuel Filiot, Olivier Gauwin, and Nathan Lhote.  Logical and algebraic characterizations of rational transductions.  Logical Methods in Computer Science, 15(4), 2019.
  * [14] Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier, and Frédéric Servais.  From two-way to one-way finite state transducers.  In ACM/IEEE Symposium on Logic in Computer Science (LICS’13), pages 468–477, 2013.
  * [15] Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter.  On equivalence and uniformisation problems for finite transducers.  In Proc. of nternational Colloquium on Automata, Languages, and Programming (ICALP’16), number 125 in LIPIcs, pages 1–14. Schloss Dagstuhl \- Leibniz-Zentrum für Informatik, 2016.
  * [16] Emmanuel Filiot, Shankara Narayanan Krishna, and Ashutosh Trivedi.  First-order definable string transformations.  In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’14), LIPIcs, pages 147–159. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.
  * [17] Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier, and Jean-Marc Talbot.  Decision problems of tree transducers with origin.  Inf. Comput., 261(Part):311–335, 2018.
  * [18] T. V. Griffiths.  The unsolvability of the equivalence problem for lambda-free nondeterministic generalized machines.  J. ACM, 15(3):409–413, 1968.
  * [19] 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.
  * [20] Ismael Jecker.  Personal communication.
  * [21] Denis Kuperberg and Jan Martens.  Regular resynchronizability of origin transducers is undecidable.  In International Symposium on Mathematical Foundations of Computer Science (MFCS’20), volume 170 of LIPIcs, pages 1–14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [22] John C. Shepherdson.  The reduction of two-way automata to one-way automata.  IBM Journal of Research and Development, 3(2):198–200, 1959.
  * [23] Imre Simon.  Factorization forests of finite height.  Theoretical Computer Science, 72(1):65–94, 1990.

Appendix

##  Appendix 0.A Proofs from Section 3.1

See 1

###### Proof

Let
$R=(\overline{I},\overline{O},\mathsf{ipar},\mathsf{opar},(\mathsf{move}_{\tau})_{\tau},(\mathsf{next}_{\tau,\tau^{\prime}})_{\tau,\tau^{\prime}})$
be a $k$-bounded, regular resynchronizer. Let $\hat{u}$ and $\hat{v}$ be a
pair of annotated input and output satisfying $\mathsf{ipar}$ and
$\mathsf{opar}$ respectively. To construct an equivalent $1$-bounded regular
resynchronizer $R^{\prime}$ we introduce additional output parameters.
Specifically, each output position will be annotated with an output type
$\tau$ from $R$ and an additional index in $\\{1,\dots,k\\}$. The intended
meaning of the index is as follows: if $(y,z)$ is the source/target origin
pair associated with an output position labeled by $(\tau,i)$,
$i\in\\{1,\dots,k\\}$, then then there are exactly $(i-1)$ positions
$y^{\prime}<y$ such that $(\hat{u},y^{\prime},z)\models\mathsf{move}_{\tau}$.

Note that this indexing depends on the choice of the target origin $z$.
Therefore, different indexing are possible for different choice of the target
origin $z$.

Based on the resynchronizer $R$, we define the new resynchronizer as
$R^{\prime}=(\overline{I},\overline{O}^{\prime},\mathsf{ipar},\mathsf{opar}^{\prime},(\mathsf{move}^{\prime}_{(\tau,i)})_{\tau,i},(\mathsf{next}_{(\tau,i),(\tau^{\prime},i^{\prime})})_{\tau,i,\tau^{\prime},i^{\prime}})$,
where

  * •

$\overline{O}^{\prime}=\overline{O}\uplus\\{O^{\prime}_{1},\dots,O^{\prime}_{k}\\}$
consists of the old output parameters $\overline{O}$ of $R$ plus some new
parameters $O^{\prime}_{1},\dots,O^{\prime}_{k}$ for representing indices in
$\\{1,\dots,k\\}$;

  * •

$\mathsf{opar}^{\prime}$ defines language of all output annotations whose
projections over $\Gamma^{\prime}$ (the output alphabet extended with the
parameters of $R$) satisfy $\mathsf{opar}$ and each position is marked by
exactly one index;

  * •

given a type $\tau^{\prime}$ that encodes a type $\tau$ of $R$ and an index
$i\in\\{1,\dots,k\\}$, $\mathsf{move}^{\prime}_{\tau^{\prime}}(y,z)$ states
that $y$ is the $i$-th position $y^{\prime}$ satisfying
$\mathsf{move}_{\tau}(y^{\prime},z)$; This property can be expressed by the
MSO-formula

$\displaystyle\exists~{}y_{1}<\dots<y_{i}=y~{}\bigwedge\nolimits_{j}\mathsf{move}_{\tau}(y_{j},z)$
$\displaystyle~{}\wedge~{}\forall y^{\prime}\leq
y~{}\big{(}\mathsf{move}_{\tau}(y^{\prime},z)\rightarrow\bigvee\nolimits_{j}y^{\prime}=y_{j}\big{)};$

  * •

$\mathsf{next}^{\prime}_{(\tau,i),(\tau^{\prime},i^{\prime})}(z,z^{\prime})$
enforces the same property as
$\mathsf{next}_{\tau,\tau^{\prime}}(z,z^{\prime})$.

The resynchronizer $R^{\prime}$ is $1$-bounded by definition of
$\mathsf{move}^{\prime}_{(\tau,i)}$. If for positions $y<y^{\prime}$,
$(\hat{u},y,z)\models\mathsf{move}^{\prime}_{(\tau,i)}$ and
$(\hat{u},y^{\prime},z)\models\mathsf{move}^{\prime}_{(\tau,i)}$, then $y$ and
$y^{\prime}$ are both the $i$-th source position in $\hat{u}$ satisfying
$\mathsf{move}_{\tau}$ with target $z$, which is a contradiction.

We now prove that $R$ and $R^{\prime}$ define the same relation between
synchronized pairs. First we show $R^{\prime}\subseteq R$. Consider
$((u,v),(u,v^{\prime}))\in R^{\prime}$. Therefore, there exists
$\hat{u}\models\mathsf{ipar}$ and $\hat{v}\models\mathsf{opar}^{\prime}$ such
that $\mathsf{move}^{\prime}$ applied to positions of $\hat{v}$ give the
$v^{\prime}$ witnessing $((u,v),(u,v^{\prime}))\in R^{\prime}$. By definition
of $\mathsf{opar}^{\prime}$, $\hat{v}_{\Gamma^{\prime}}\models\mathsf{opar}$.
Suppose, a position $x$ of output type $(\tau,i)$ is moved from origin $y$ in
$v$ to $z$ in $v^{\prime}$. This means
$(\hat{u},y,z)\models\mathsf{move}^{\prime}_{(\tau,i)}$. Then, by definition
of $\mathsf{move}^{\prime}_{(\tau,i)}$,
$(\hat{u},y,z)\models\mathsf{move}_{\tau}$. This shows $R^{\prime}\subseteq
R$.

For the containment $R\subseteq R^{\prime}$, consider
$((u,v),(u,v^{\prime}))\in R$. Therefore, there exists
$\hat{u}\models\mathsf{ipar}$ and $\hat{v}\models\mathsf{opar}$ such that
$\mathsf{move}$ applied to each position in $\hat{v}$ witnesses
$((u,v),(u,v^{\prime}))\in R$. This means for every position
$x\in\mathsf{dom}(\hat{v})$ with output-type $\tau$, there exist $y,z$, such
that $(\hat{u},y,z)\models\mathsf{move}_{\tau}$, $y=\mathit{orig}(v(x))$ and
$z=\mathit{orig}(v^{\prime}(x))$. For such a position
$x\in\mathsf{dom}(\hat{v})$ of output type $\tau$, let $i\in\\{1,\dots,k\\}$
be such that there are exactly $i-1$ positions $y_{1}<y_{2}<\dots y_{i-1}<y$
such that $(\hat{u},y_{j},z)\models\mathsf{move}_{\tau}$. Let
$\hat{v}^{\prime}$ be the annotation of $\hat{v}$ where every position $x$ is
annotated with the index $i$ as above. Clearly
$\hat{v}^{\prime}\models\mathsf{opar}^{\prime}$ and therefore,
$((u,v),(u,v^{\prime}))\in R^{\prime}$. We conclude $R=R^{\prime}$. ∎

See 2

###### Proof

Let
$R=(\overline{I},\overline{O},\mathsf{ipar},\mathsf{opar},(\mathsf{move}_{\tau})_{\tau},(\mathsf{next}_{\tau,\tau^{\prime}})_{\tau,\tau^{\prime}})$
and
$R^{\prime}=(\overline{I}^{\prime},\overline{O}^{\prime},\mathsf{ipar}^{\prime},\mathsf{opar}^{\prime}$,
$(\mathsf{move}^{\prime}_{\lambda})_{\lambda},(\mathsf{next}^{\prime}_{\lambda,\lambda^{\prime}})_{\lambda,\lambda^{\prime}})$
be two bounded, regular resynchronizers. In view of Lemma 1, we can assume
that both resynchronizers are $1$-bounded. The composition $R\circ R^{\prime}$
can be defined by combining the effects of $R$ and $R^{\prime}$ almost
component-wise. Some care should be taken, however, in combining the formulas
$\mathsf{next}$ and $\mathsf{next}^{\prime}$. Formally, we define the composed
resynchronizer
$R^{\prime\prime}=(\overline{I}^{\prime\prime},\overline{O}^{\prime\prime},\mathsf{ipar}^{\prime\prime},\mathsf{opar}^{\prime\prime},(\mathsf{move}^{\prime\prime}_{(\tau,\lambda)})_{\tau,\lambda},(\mathsf{next}^{\prime\prime}_{(\tau,\lambda),(\tau^{\prime},\lambda^{\prime})})_{\tau,\lambda,\tau^{\prime},\lambda^{\prime}})$,
where

  * •

$\overline{I}^{\prime\prime}$ is the union of the parameters $\overline{I}$
and $\overline{I}^{\prime}$,

  * •

$\overline{O}^{\prime\prime}$ is the union of the parameters $\overline{O}$
and $\overline{O}^{\prime}$,

  * •

$\mathsf{ipar}^{\prime\prime}$ is the conjunction of the formulas
$\mathsf{ipar}$ and $\mathsf{ipar}^{\prime}$;

  * •

$\mathsf{opar}^{\prime\prime}$ is the conjunction of the formulas
$\mathsf{opar}$ and $\mathsf{opar}^{\prime}$;

  * •

$\mathsf{move}^{\prime\prime}_{(\tau,\lambda)}(y,z)$ states the existence of
some position $t$ satisfying both formulas $\mathsf{move}_{\tau}(t,z)$ and
$\mathsf{move}^{\prime}_{\lambda}(y,t)$;

  * •

$\mathsf{next}_{(\tau,\lambda),(\tau^{\prime},\lambda^{\prime})}(z,z^{\prime})$
requires that $\mathsf{next}_{\tau,\tau^{\prime}}(z,z^{\prime})$ holds and,
moreover, that there exist some positions $t,t^{\prime}$ satisfying
$\mathsf{move}_{\tau}(t,z)$,
$\mathsf{move}_{\tau^{\prime}}(t^{\prime},z^{\prime})$, and
$\mathsf{next}_{\lambda,\lambda^{\prime}}(t,t^{\prime})$; note that these
positions $t,t^{\prime}$ are uniquely determined from $z,z^{\prime}$ since $R$
is $1$-bounded, and they act, at the same time, as source origins for $R$ and
as target origins for $R^{\prime}$.

By definition, $\mathsf{move}^{\prime\prime}_{(\tau,\lambda)}$ is $1$-bounded,
thus $z$ and $\tau$ determine a unique $t$, which together with $\lambda$
determines a unique $y$. It is also easy to see that $R^{\prime\prime}$ is
equivalent to $R\circ R^{\prime}$ as the positions corresponding to $t$ in
formulas $\mathsf{move}^{\prime\prime}_{(\tau,\lambda)}$ and
$\mathsf{next}^{\prime\prime}_{(\tau,\lambda),(\tau^{\prime},\lambda^{\prime})}$
correspond to the source origin of $R$ and target origin of $R^{\prime}$. ∎

##  Appendix 0.B Proofs from Section 4.1

See 3

###### Proof

It is convenient to rephrase the claim of the lemma in terms of a
juxtaposition operation on flows and in terms of an induced accessibility
relation on edges. Formally, given two flows $F,G$, we define the
juxtaposition $FG$ in a way similar to concatenation, with the only exception
that in the result we maintain as an additional group of vertices the
$\mathsf{R}$ vertices of $F$, glued with the state-matching $\mathsf{L}$
vertices of $G$ (strictly speaking, the result of a juxtaposition of two flows
is not a flow, since it has three distinguished groups of vertices). We denote
by $E\dots E$ the $n$-fold juxtaposition of the flow $E$ with itself (this
must not be confused with the $n$-fold concatenation $E\cdot\ldots\cdot E$).

Let $F,E,G$, $f,e$, $\rho_{f},\rho_{e}$ be as stated in the lemma, and let
$\preceq$ denote the accessibility order between edges in a juxtaposition of
flows, e.g. $FEG$ (note that, due to the type of flows considered here,
$\preceq$ turns out to always be a total order on $FEG$). Observe that the
relative occurrence order of $\rho_{f}$ and $\rho_{e}$ inside $\rho$ is the
same as the accessibility order $\preceq$ of the edges $f$ and $e$ on the
graph $FEG$. A similar claim holds for the occurrence order of $\rho_{f}$ and
any copy of $\rho_{e}$ inside the pumped run $\mathit{pump}^{n}_{I}(\rho)$,
which corresponds to the accessibility order of $f$ and any copy of $e$ in the
graph $FE\dots EG$. Thanks to these correspondences, to prove the lemma it
suffices to consider any copy $e^{\prime}$ of $e$ in $FE\dots EG$, and show
that

$f\preceq e\text{ in }FEG\qquad\text{iff}\qquad f\preceq e^{\prime}\text{ in
}FE\dots EG.$

We thus prove the above claim. Consider the maximal path $\pi$ inside $E\dots
E$ that contains the edge $e^{\prime}$. Note that this path starts and ends at
some extremal vertices of $E\dots E$ (otherwise the path could be extended
while remaining inside $E\dots E$). Also recall that concatenation can be
defined from juxtaposition by removing the intermediate groups of vertices,
leaving only the extremal ones, and by shortcutting paths into edges. We call
this operation _flattening_ , for short. In particular, since $E$ is
idempotent, we have that $E=E\cdot\ldots\cdot E$ can be obtained from the
flattening of $E\dots E$, and this operation transforms the path $\pi$ into an
edge $e^{\prime\prime}$. By construction, we have that $f\preceq e^{\prime}$
in $FE\dots EG$ if and only if $f\preceq e^{\prime\prime}$ in $FEG$. So it
remains to prove that

$f\preceq e\text{ in }FEG\qquad\text{iff}\qquad f\preceq
e^{\prime\prime}\text{ in }FEG.$

Clearly, this latter claim holds if the edges $e$ and $e^{\prime\prime}$
coincide. This is indeed the case when $e$ is a straight edge and $E$ is
idempotent. The formal proof that this holds is rather tedious, but follows
quite easily from a series of results we have already proven in [3]. Roughly
speaking, one proves that:

  * •

the edges of an idempotent flow $E$ can be grouped into _components_ (cf.
Definition 6.4 from [3]), so that each component contains exactly one straight
edge (cf. Lemma 6.6 from [3], see also the figure at page 4.1, where
components are represented by colors);

  * •

every path inside the juxtaposition $EE$, with $E$ idempotent, consists of
edges from the same component, say $C$; moreover, after the flattening from
$EE$ to $E$, this path becomes an edge of $E$ that belongs again to the
component $C$ (cf. Claims 7.3 and 7.4 in the proof of Theorem 7.2 from [3]);

  * •

every maximal path in $E\dots E$ that contains a straight edge starts and end
at opposite sides of $E\dots E$ (simple observation based on the definition of
concatenation and Lemma 6.6 from [3]).

To conclude, recall that $\pi$ is a path inside $E\dots E$ that contains a
copy $e^{\prime}$ of the straight edge $e$, and that becomes the edge
$e^{\prime\prime}$ after the flattening into $E$. The previous properties
immediately imply that $e=e^{\prime\prime}$.

##  Appendix 0.C Proofs from Section 4.2

As explained in the body, the technical lemmas involving output blocks are
only applicable to transducers that avoid inversions. _Hereafter we assume
that $T$ is a transducer that avoids inversions, and we denote by $\rho$ an
arbitrary successful run of $T$._

See 5

###### Proof

$B_{1}$ and $B_{2}$ are clearly disjoint. By way of contradiction, assume that
$B_{1}$ and $B_{2}$ are $\mathbf{C}$-large, but $B_{1}>B_{2}$. By Lemma 4, we
can find for both $i=1$ and $i=2$ a loop $J_{i}\subseteq I_{i}$ and a
productive straight edge $e_{i}\in\mathit{flow}(J_{i})$ that is witnessed by a
subrun intersecting $B_{i}$. Clearly, we have $J_{1}<J_{2}$, and since
$B_{1}>B_{2}$, the subrun witnessing $e_{1}$ follows the subrun witnessing
$e_{2}$. Thus, $(J_{1},e_{1},J_{2},e_{2})$ is an inversion of $\rho$, which
contradicts the assumption that $T$ avoids inversions.

We now turn to the proofs of Lemmas 6 and 7, which both require auxiliary
lemmas relying again on the assumption that $T$ avoids inversion.

######  Lemma 0.C.1 ()

Let $I$ be an input interval, $B_{1}<B_{2}$ two output blocks of $I$, and $S$
the set of output positions strictly between $B_{1}$ and $B_{2}$ and with
origins outside $I$. If $B_{1},B_{2}$ are $\mathbf{C}$-large, then $S$ is
$2\mathbf{C}$-small.

###### Proof

By way of contradiction, suppose that $S$ is $2\mathbf{C}$-large. This means
that $|\mathit{orig}(S)\cap I^{\prime}|>\mathbf{C}$ for some interval
$I^{\prime}$ disjoint from $I$, say $I^{\prime}<I$ (the case of $I^{\prime}>I$
is treated similarly). By Lemma 4, we can find two loops $J\subseteq I$ and
$J^{\prime}\subseteq I^{\prime}$ and some productive straight edges
$e\in\mathit{flow}(J)$ and $e^{\prime}\in\mathit{flow}(J^{\prime})$ that are
witnessed by subruns intersecting $B_{1}$ and $S$, respectively. Since
$S>B_{1}$, we know that the subrun witnessing $e$ follows the subrun
witnessing $e^{\prime}$. As in the previous proof, this shows the inversion
$(J,e,J^{\prime},e^{\prime})$, which contradicts the assumption that $T$
avoids inversions.

See 6

###### Proof

By Lemma 5, we have $B_{1}<B_{2}$. Moreover, all $\mathbf{C}$-large output
blocks of $I_{1}$ or $I_{2}$ are also $\mathbf{C}$-large output blocks of $I$,
so $B$ contains both $B_{1}$ and $B_{2}$. Let $I_{0}$ be the maximal interval
to the left of $I_{1}$, and thus adjacent to it, and, similarly, let $I_{3}$
be the maximal interval to the right of $I_{2}$, and thus adjacent to it.

Suppose, by way of contradiction, that $B\setminus(B_{1}\cup B_{2})$ is
$4K\mathbf{C}$-large. This means that there is a $2K\mathbf{C}$-large set
$S\subseteq B\setminus(B_{1}\cup B_{2})$ with origins entirely inside
$I_{0}\cdot I_{1}$ or entirely inside $I_{2}\cdot I_{3}$. Suppose, w.l.o.g.,
that the former case holds, and decompose $S$ as a union of maximal output
blocks $B^{\prime}_{1},B^{\prime}_{2},\dots,B^{\prime}_{n}$ of either $I_{0}$
or $I_{1}$. Since $S\cap B_{1}=\emptyset$, we have that every block
$B^{\prime}_{i}$ with origins inside $I_{1}$ is $\mathbf{C}$-small. Similarly,
by Lemma 0.C.1, every block $B^{\prime}_{i}$ with origins inside $I_{0}$ is
$\mathbf{C}$-small too. Moreover, since $\rho$ is $K$-visiting, we have that
the number $n$ of maximal output blocks of either $I_{0}$ or $I_{1}$ that are
contained in $S$ is at most $2K$. All together, this contradicts the
assumption that $S$ is $2K\mathbf{C}$-large.

######  Lemma 0.C.2 ()

Let $I$ be a loop of $\rho$. Then $\mathit{flow}(I)$ has at most one
productive straight edge, and this edge must be $\mathsf{L}\mathsf{R}$.

###### Proof

Suppose, by way of contradiction, that there are two productive straight edges
in $\mathit{flow}(I)$, say $e$ and $f$, with $e$ before $f$ in $\rho$ (the
reader may refer again to the figure at page 4.1, and think of $e$ and $f$,
for instance, as the edges labeled by $\alpha_{2}$ and $\gamma_{1}$,
respectively). Suppose that we pump $I$ twice, and let $I_{1}<I_{2}$ be the
copies of $I$ in the pumped run $\rho^{\prime}$. Let also $e_{1},e_{2}$ (resp.
$f_{1},f_{2}$) be the corresponding copies of $e$ (resp. $f$), so that
$e_{j},f_{j}$ belong to the flow $\mathit{flow}_{\rho^{\prime}}(I_{j})$. It is
easy to check the following properties:

  * •

if $e$ is an $\mathsf{L}\mathsf{R}$ edge, then the subrun witnessed by $e_{1}$
occurs in $\rho^{\prime}$ before the subrun witnessed by $e_{2}$ (and the
other way around if $e$ is $\mathsf{R}\mathsf{L}$);

  * •

the subruns witnessed by $e_{1}$ and $e_{2}$ occur in $\rho^{\prime}$ before
the subruns witnessed by $f_{1},f_{2}$ (this property follows easily from the
observation that when building the product
$\mathit{flow}(I)\cdot\mathit{flow}(I)$, the edges $e_{1},e_{2}$ will be
“part” of the edge $e$ in the product, whereas $f_{1},f_{2}$ will be “part” of
the edge $f$).

Let us assume first that $e$ is an $\mathsf{R}\mathsf{L}$ edge. Then observe
that $(I_{1},e_{1},I_{2},e_{2})$ is an inversion in $\rho^{\prime}$. But this
contradicts $T$ being inversion-free. Therefore, both $e,f$ are
$\mathsf{L}\mathsf{R}$ edges. But then, $(I_{1},f_{1},I_{2},e_{2})$ is an
inversion in $\rho^{\prime}$, and we have again a contradiction.

###### Remark 0.C.1

The statement of Lemma 0.C.2 can be strengthened by observing the following
property of productive edges in an idempotent flow. Assume that $I$ is a loop
and $e$ is the unique productive straight edge in $\mathit{flow}(I)$. Let $f$
be some productive (non-straight) edge of $\mathit{flow}(I)$ with $f\not=e$.
When $I$ is pumped then the subruns witnessing the copies of $f$ are part of
the subrun witnessing $e$ in the product flow. This means for example, that in
the figure on page 4.1 the productive edges are either all among the blue
edges, or all among the gray edges (none of the red edges can be productive,
because the straight edge is $\mathsf{R}\mathsf{L}$, and would result in a
productive $\mathsf{R}\mathsf{L}$ edge on pumping).

See 7

###### Proof

By Lemma 0.C.2, we can assume that $\mathit{flow}(I)=\mathit{flow}(I_{k})$ has
a unique productive straight edge $e$, which is an $\mathsf{L}\mathsf{R}$
edge. Let $B^{\prime}_{k}$ be the output block corresponding to $e$ in
$\mathit{flow}(I_{k})$. Since $\mathit{flow}(I)$ is idempotent, any output
block of $I$ has one of the following shapes (see also Remark 0.C.1):

  * (a)

A block $B=B^{\prime}_{1}\cdot J^{\prime}_{1}\cdot\dots J^{\prime}_{n-1}\cdot
B^{\prime}_{n}$, for some intervals $J^{\prime}_{1},\dots,J^{\prime}_{n-1}$
such that $\mathit{out}(I_{k})$ is included in $J^{\prime}_{k-1}\cdot
B^{\prime}_{k}\cdot J^{\prime}_{k}$ for all $1<k<n$,

  * (b)

At most $2K$ output blocks $L_{1},\dots,L_{p},R_{1},\dots,R_{s}$, where each
$L_{i}$ and $R_{j}$ corresponds to an edge of $\mathit{flow}(I_{1})$ and
$\mathit{flow}(I_{n})$, respectively: the blocks $L_{i},R_{j}$ appear before,
respectively after the straight edge.

Moreover, the order of the output blocks of $I$ is
$L_{1},\dots,L_{p},B,R_{1},\dots,R_{s}$. To illustrate the statement (a)
above, the reader can take as example $p=s=2$, $L_{1}=\alpha$, $L_{2}=\beta$,
$R_{1}=\kappa$, $R_{2}=\zeta$,
$J^{\prime}_{1}=\cdots=J^{\prime}_{n-1}=\alpha\kappa\beta\zeta$ in Figure 2.
For statement (b), notice that in $I_{1}\cdot I_{2}\cdot I_{3}$, we have the
output blocks $L_{1}=\alpha,L_{2}=\beta$ of $I_{1}$, the straight edge
$(\gamma\alpha\kappa\beta\zeta)^{2}\gamma$ (the purple zigzag) followed by
$R_{1}=\kappa,R_{2}=\zeta$ of $I_{3}$.

Note that $B_{k}=\mathit{bigout}(I_{k})$ is contained in
$J^{\prime}_{k-1}\cdot B^{\prime}_{k}\cdot J^{\prime}_{k}$ for all $1<k<n$.
Moreover, $B_{1}=\mathit{bigout}(I_{1})$ is contained in $L_{1}\cdots
L_{p}\cdot B^{\prime}_{1}\cdot J^{\prime}_{1}$, and
$B_{n}=\mathit{bigout}(I_{n})$ is contained in $J^{\prime}_{n-1}\cdot
B^{\prime}_{n}\cdot R_{1}\cdots R_{s}$. Also by Lemma 5, $B_{j}$ precedes
$B_{j+1}$ for all $j$.

$I$$\boldsymbol{\alpha_{1}}$$~{}\boldsymbol{\alpha_{2}}$$\boldsymbol{\alpha_{3}}$$\boldsymbol{\beta_{1}}$$\boldsymbol{\beta_{2}}$$\boldsymbol{\beta_{3}}$$~{}\boldsymbol{\gamma_{1}}$$I_{1}$$I_{2}$$I_{3}$$\boldsymbol{\alpha}$$\boldsymbol{\beta}$$\boldsymbol{\gamma}$$\boldsymbol{\alpha}$$\boldsymbol{\kappa}$$\boldsymbol{\beta}$$\boldsymbol{\zeta}$$\boldsymbol{\gamma}$$\boldsymbol{\alpha}$$\boldsymbol{\kappa}$$\boldsymbol{\beta}$$\boldsymbol{\zeta}$$\boldsymbol{\zeta}$$\boldsymbol{\gamma}$$\boldsymbol{\kappa}$

Figure 2: Illustration for Lemma 7.

If one of the $L_{k}$ is $\mathbf{C}$-large, then $B_{1}$ is non-empty, hence
$\mathit{bigout}(I)$ is non-empty and starts at the first position of $B_{1}$.
Similarly, if one of the $R_{k}$ is $\mathbf{C}$-large then $B_{n}$ is non-
empty, hence $\mathit{bigout}(I)$ is non-empty and ends with the last position
of $B_{n}$. Otherwise, if all $L_{j},R_{j}$ are $\mathbf{C}$-small then
$\mathit{bigout}(I)$ is either empty or equal to $B$. In all cases we can
write $\mathit{bigout}(I)=B_{1}\cdot J_{1}\cdot B_{2}\cdot
J_{2}\cdot\dots\cdot J_{n-1}\cdot B_{n}$, with each $J_{k}$ consisting of at
most $K$ $\mathbf{C}$-small blocks of $I_{k}$ and $K$ $\mathbf{C}$-small
blocks of $I_{k+1}$, namely those left over after gathering the
$\mathbf{C}$-large blocks into $\mathit{bigout}(I_{k})$ and
$\mathit{bigout}(I_{k+1})$, respectively. Therefore, each $J_{k}$ is
$2K\mathbf{C}$-small.

##  Appendix 0.D Proof of Theorem 3.1.

Recall that the implication $4\rightarrow 1$ is straightforward, and the
implication $1\rightarrow 2$ was already proven in full detail in the main
body. Below, we provide detailed proofs of the implications $2\rightarrow
3\rightarrow 4$.

The implication $2\rightarrow 3$ is shown by contradiction. Consider a
successful run $\rho$ of $T$ on some input $u$ and suppose there is an
inversion: $\rho$ has disjoint loops $I<I^{\prime}$, whose flows contain
productive straight edges, say $e$ in $\mathit{flow}_{\rho}(I)$ and
$e^{\prime}$ in $\mathit{flow}_{\rho}(I^{\prime})$, such that $e^{\prime}$
precedes $e$ in the run order. Let $u=u_{1}\,w\,u_{2}\,w^{\prime}\,u_{3}$ so
that $w$ and $w^{\prime}$ are the factors of the input delimited by the loops
$I$ and $I^{\prime}$, respectively. Further let $v$ and $v^{\prime}$ be the
outputs produced along the edges $e$ and $e^{\prime}$, respectively. Consider
now the run $\rho_{k}$ obtained from $\rho$ by pumping the input an arbitrary
number $k$ of times on the loops $I$ and $I^{\prime}$. This run is over the
input $u_{1}\,(w)^{k}\,u_{2}\,(w^{\prime})^{k}\,u_{3}$, and in the output
produced by $\rho_{k}$ there are $k$ (possibly non-consecutive) occurrences of
$v$ and $v^{\prime}$. By Lemma 3 all occurrences of $v^{\prime}$ precede all
occurrences of $v$. In particular, if $X_{1}$ (resp. $X_{2}$) is the set of
positions corresponding to all the occurrences of $v$ (resp. $v^{\prime}$) in
the output produced by $\rho_{k}$, then $(X_{1},X_{2})$ is a cross of width at
least $k$.

Now we prove the implication $3\rightarrow 4$. We assume that no run of $T$
has any inversion. We want to build a partially bijective, regular
resynchronizer $\mathcal{R}$ that is $T$-preserving and such that
$\mathcal{R}(T)$ is order-preserving. The resynchronizer $\mathcal{R}$ will
use input and output parameters to guess a successful run $\rho$ of $T$ on the
input $u$ and a corresponding _factorization tree_ for $\rho$ of height at
most $H=3|M_{T}|$ (see page 5 for the formal definition and the existence of a
factorization tree).

The resynchronizer $\mathcal{R}$ that we will define is _functional_ , which
means here that every source origin is mapped by each $\mathsf{move}_{\tau}$
formula to at most one target position.

#### Notations.

For a node $p$ of a factorization tree we write $I(p)$ for the input interval
which is the yield of the subtree of $p$. Recall that the leaves of the
factorization tree correspond to singleton intervals on the input. The set of
output positions with origins in $I(p)$ is denoted by $\mathit{out}(p)$ (note
that this might not be an interval).

Recall that an output block $B$ of $\mathit{out}(p)$ is a maximal interval of
output positions with origins in $I(p)$, and hence the position just before
and the position just after $B$ have origins outside $I(p)$. We also write
$\mathit{bigout}(p)$, instead of $\mathit{bigout}(I(p))$, for the dominant
output interval of $I(p)$ (see page 4 for the definition). Finally, given a
position $x$ in the output and a level $\ell$ of the factorization tree of
$\rho$, we denote by $p_{x,\ell}$ the unique node at level $\ell$ such that
$I(p_{x,\ell})$ contains the source origin of $x$.

#### Input Parameters.

The successful run $\rho$ together with its factorization tree of height at
most $H=3|M_{T}|$ can be easily encoded over the input using input parameters
$\mathsf{ipar}$. The parameters describe each input interval $I(p)$ and the
label $\mathit{flow}(I(p))$ of each node $p$ in the factorization tree.
Formally, an input interval $I(p)$ is described by marking the begin and end
with two distinguished parameters for the specific level. The label
$\mathit{flow}(I(p))$ annotates every position inside $I(p)$. This accounts
for $H(2+|M_{T}|)$ input parameters. Correctness of the annotations with the
above input parameters can be expressed by a formula $\mathsf{ipar}$. In
particular, on the leaves, $\mathsf{ipar}$ checks that every interval is a
singleton of the form $\\{y\\}$ and its flow is the one induced by the letter
$u(y)$. On the internal nodes, $\mathsf{ipar}$ checks that the label of a node
coincides with the monoid product of the labels of its children, which is a
composition of flows. It also checks that for every node with more than two
children, the node and the children are labelled by the same idempotent flow.

#### Output Parameters.

We also need to encode the run $\rho$ on the output, because the
resynchronizer will determine the target origin of an output position, not
only on the basis of the flow at the source origin, but also on the basis of
the productive transition that generated that particular position. The
annotation that encodes the run $\rho$ on the output is done using output
parameters (one for each transition in $\Delta$), and its correctness will be
enforced by a suitable combination of the formulas $\mathsf{opar}$,
$\mathsf{move}_{\tau}$, and $\mathsf{next}_{\tau,\tau^{\prime}}$. This will
take a significant amount of technical details and will rely on specific
properties of formulas $\mathsf{move}_{\tau}$, so we prefer to temporarily
postpone those details.

Below, we explain how the origins are transformed by a series of partial
resynchronizers $\mathcal{R}_{\ell}$ that “converge” in finitely many steps to
a desired resynchronization, under the assumption that the output annotation
correctly encodes the same run $\rho$ that is represented in the input
annotation.

#### Moving origins.

Here we will work with a fixed successful run $\rho$ and a factorization tree
for it, that we assume are correctly encoded by the input and output
annotations. For every level $\ell$ of the factorization tree, we will define
a functional, bounded, regular resynchronizer $\mathcal{R}_{\ell}$. Each
resynchronizer $\mathcal{R}_{\ell}$ will be _partial_ , in the sense that for
some output positions it will not define source-target origin pairs. However,
the set of output positions with associated source-target origin pairs
increases with the level $\ell$, and the top level resynchronizer
$\mathcal{R}_{*}$ will specify source-target origin pairs for all output
positions. The latter resynchronizer will almost define the resynchronization
that is needed to prove item (4) of the theorem; we will only need to modify
it slightly in order to make it $1$-bounded and to check that the output
annotation is correct.

To enable the inductive construction, we need the resynchronizer
$\mathcal{R}_{\ell}$ to satisfy the following properties, for every level
$\ell$ of the factorization tree:

  * •

the set of output positions for which $\mathcal{R}_{\ell}$ defines target
origins is the union of the dominant output intervals $\mathit{bigout}(p)$ of
all nodes $p$ at level $\ell$;

  * •

$\mathcal{R}_{\ell}$ only moves origins within the same interval at level
$\ell$, that is, $\mathcal{R}_{\ell}$ defines only pairs $(y,z)$ of source-
target origins such that $y,z\in I(p)$ for some node $p$ at level $\ell$;

  * •

the target origins defined by $\mathcal{R}_{\ell}$ are order-preserving within
the same interval at level $\ell$, that is, for all output positions
$x<x^{\prime}$, if $\mathcal{R}_{\ell}$ defines the target origins of
$x,x^{\prime}$ to be $z,z^{\prime}$, respectively, and if $z,z^{\prime}\in
I(p)$ for some node $p$ at level $\ell$, then $z\leq z^{\prime}$.

  * •

$\mathcal{R}_{\ell}$ is $\ell\cdot 4K\mathbf{C}$-bounded, namely, there are at
most $\ell\cdot 4K\mathbf{C}$ distinct source origins that are moved by
$\mathcal{R}_{\ell}$ to the same target origin.

The inductive construction of $\mathcal{R}_{\ell}$ will basically amount to
defining appropriate formulas $\mathsf{move}_{\tau}(y,z)$.

Base Case. The base case is $\ell=0$, namely, when the resynchronization is
acting at the leaves of the factorization tree. In this case, the regular
resynchronizer $\mathcal{R}_{\ell}$ is vacuous, as the input intervals $I(p)$
associated with the leaves $p$ are singletons, and hence all dominant output
intervals $\mathit{bigout}(p)$ are empty. Formally, for this resynchronizer
$\mathcal{R}_{\ell}$, we simply let $\mathsf{move}_{\tau}(y,z)$ be false,
independently of the underlying output type $\tau$ and of the source and
target origins. This resynchronization is clearly functional, $0$-bounded, and
order-preserving.

Inductive Step. For the inductive step, we explain how the origins of an
output position $x\in\mathit{bigout}(p)$ are moved within the interval $I(p)$,
where $p=p_{x,\ell}$ is the node at level $\ell$ that “generates” $x$. Even
though we explain this by mentioning the node $p_{x,\ell}$, the definition of
the resynchronization will not depend on it, but only on the level $\ell$ and
the underlying input and output parameters. In particular, to describe how the
origin of a $\tau$-labeled output position $x$ is moved, the formula
$\mathsf{move}_{\tau}(y,z)$ has to determine the productive edge that
generated $x$ in the flow that labels the node $p_{x,\ell}$. This can be done
by first determining from the output type $\tau$ the productive transition
$t_{x}$ that generated $x$, and then inspecting the annotation at the source
origin $y$ to “track” $t_{x}$ inside the productive edges of the flow
$\mathit{flow}(I_{p^{\prime}})$, for each node $p^{\prime}$ along the unique
path from the leaf $p_{x,0}$ to node $p_{x,\ell}$. In the case distinction
below, we implicitly rely on this type of computation, which can be easily
implemented in MSO.

  1. 1.

$\boldsymbol{p_{x,\ell}}$ is a binary node. We first consider the case where
$p=p_{x,\ell}$ is a binary node (the annotation on the source origin $y$ will
tell us whether this is the case). Let $p_{1},p_{2}$ be the left and right
children of $p$. If $x$ belongs to one of the dominant output blocks
$\mathit{bigout}(p_{1})$ and $\mathit{bigout}(p_{2})$ (again, this information
is available at the input annotation), then the resynchronizer
$\mathcal{R}_{\ell}$ will inherit the source-target origin pairs associated
with $x$ from the lower level resynchronization $\mathcal{R}_{\ell-1}$. Note
that $\mathit{bigout}(p_{1})<\mathit{bigout}(p_{2})$ by Lemma 5, so
$\mathcal{R}_{\ell}$ is order-preserving at least for the output positions
inside $\mathit{bigout}(p_{1})\cup\mathit{bigout}(p_{2})$.

We now describe the source-target origin pairs when
$x\in\mathit{bigout}(p)\setminus(\mathit{bigout}(p_{1})\cup\mathit{bigout}(p_{2}))$.
The idea is to move the origin of $x$ to one of the following three input
positions, depending on the relative order between $x$ and the positions in
$\mathit{bigout}(p_{1})$ and in $\mathit{bigout}(p_{2})$:

     * •

the first position of $I(p_{1})$, if $x<\mathit{bigout}(p_{1})$;

     * •

the last position of $I(p_{1})$, if
$\mathit{bigout}(p_{1})<x<\mathit{bigout}(p_{2})$;

     * •

the last position of $I(p_{2})$, if $x>\mathit{bigout}(p_{2})$.

Which of the above cases holds can be determined, again, by inspecting the
output type $\tau$ and the annotation of the source origin $y$, in a way
similar to the computation of the productive edge that generated $x$ at level
$\ell$. So the described resynchronization can be implemented by an MSO
formula $\mathsf{move}_{\tau}(y,z)$.

The resulting resynchronization $\mathcal{R}_{\ell}$ is functional and order-
preserving inside every interval at level $\ell$. It remains to argue that
$\mathcal{R}_{\ell}$ is $\ell\cdot 4K\mathbf{C}$-bounded. To see why this
holds, assume, by the inductive hypothesis, that $\mathcal{R}_{\ell-1}$ is
$(\ell-1)\cdot 4K\mathbf{C}$-bounded. Recall that the new source-target origin
pairs that are added to $\mathcal{R}_{\ell}$ are those associated with output
positions in
$\mathit{bigout}(p)\setminus(\mathit{bigout}(p_{1})\cup\mathit{bigout}(p_{2}))$.
Lemma 6 tells us that there are at most $4K\mathbf{C}$ distinct positions that
are source origins of such positions. So, in the worst case, at most
$(\ell-1)\cdot 4K\mathbf{C}$ source origins from $\mathcal{R}_{\ell-1}$ and at
most $4K\mathbf{C}$ new source origins from $\mathcal{R}_{\ell}$ are moved to
the same target origin. This shows that $\mathcal{R}_{\ell}$ is $\ell\cdot
4K\mathbf{C}$-bounded.

  2. 2.

$\boldsymbol{p_{x,\ell}}$ is an idempotent node. The case where $p=p_{x,\ell}$
is an idempotent node with children $p_{1},p_{2},\dots,p_{n}$ follows a
similar approach. For brevity, let $I_{i}=I(p_{i})$ and
$B_{i}=\mathit{bigout}(p_{i})$. By Lemma 5, we have $B_{1}<B_{2}<\dots<B_{n}$.
Lemma 7 then provides a decomposition of $\mathit{bigout}(p)$ as $B_{1}\cdot
J_{1}\cdot B_{2}\cdot J_{2}\cdot\dots\cdot J_{n-1}\cdot B_{n}$, for some
$2K\mathbf{C}$-small output intervals $J_{k}$, for $k=1,\dots,n-1$, that have
origins inside $I_{k}\cup I_{k+1}$.

As before, the resynchronizer $\mathcal{R}_{\ell}$ behaves exactly as
$\mathcal{R}_{\ell-1}$ for the output positions inside the $B_{k}$’s. For any
other output position, say $x\in J_{k}$ for some $k=1,2,\dots,n-1$, we first
recall that the source origin $y$ of $x$ is either inside $I_{k}$ or inside
$I_{k+1}$. Depending on which of the two intervals contains $y$, the
resynchronizer $\mathcal{R}_{\ell}$ will define the target origin $z$ to be
either the last position of $I_{k}$ or the first position of $I_{k+1}$.
However, since we cannot determine using MSO the index $k$ of the interval
$J_{k}$ that contains $x$, we proceed as follows.

First observe that any block $B_{i}$ can be identified by some flow edge at
level $\ell-1$, and the latter edge can represented in MSO by suitable monadic
predicates over the input. Let $B,B^{\prime}$ be the two consecutive blocks
among $B_{1},\dots,B_{n}$ such that $B<x<B^{\prime}$. Note that these blocks
can be determined in MSO once the productive edge that generated $x$ is
identified. Further let $I$ be the interval among $I_{1},\dots,I_{n}$ that
contains the origin $y$ of $x$. By the previous arguments, we have that the
interval $I$ contains either all the origins of $B$ or all the origins
$B^{\prime}$. Moreover, which of the two sub-cases holds can again be
determined in MSO by inspecting the annotations. The formula
$\mathsf{move}_{\tau}(y,z)$ can thus define the target origin $z$ to be

     * •

the last position of $I$, if $I$ contains the origins of $B$;

     * •

the first position of $I$, if $I$ contains the origins of $B^{\prime}$.

The above construction yields a functional regular resynchronization
$\mathcal{R}_{\ell}$ that associates with any two output positions
$x<x^{\prime}$ with source origins in the same interval $I(p)$, some target
origins $z\leq z^{\prime}$. In other words, the resynchronization
$\mathcal{R}_{\ell}$ is order-preserving in each interval at level $\ell$.

It remains to show that $\mathcal{R}_{\ell}$ is $\ell\cdot
4K\mathbf{C}$-bounded, under the inductive hypothesis that
$\mathcal{R}_{\ell-1}$ is $(\ell-1)\cdot 4K\mathbf{C}$-bounded. This is done
using a similar argument as before, that is, by observing that the output
positions in $\mathit{bigout}(p)\setminus\big{(}\bigcup_{1\leq k\leq
n}\mathit{bigout}(p_{i})\big{)}$ belong to some $J_{k}$, and in the worst case
all source origins $y$ of positions from $J_{k}$ are moved to the last
position of $I_{k}$. By Lemma 7, there are at most $2K\mathbf{C}$ such
positions $y$.

#### Top level resynchronizer.

Let $\mathcal{R}_{*}$ be the the resynchronizer $\mathcal{R}_{\ell}$ obtained
at the top level $\ell$ of the factorization tree. Based on the above
constructions, $\mathcal{R}_{*}$ defines target origins for all output
positions, unless the dominant output interval $\mathit{bigout}(p)$ associated
with the root $p$ is empty (this can indeed happen when the number of
different origins in the output is at most $\mathbf{C}$, so not sufficient for
having at least one $\mathbf{C}$-large output factor). In particular, if
$\mathit{bigout}(p)\neq\emptyset$, then $\mathit{bigout}(p)$ is the whole
output, and $\mathcal{R}_{\ell}$ is basically the desired resynchronization,
assuming that the output annotations are correct.

Let us now discuss briefly the degenerate case where
$\mathit{bigout}(p)=\emptyset$, which of course can be detected in MSO. In
this case, the appropriate resynchronizer $\mathcal{R}_{*}$ should be
redefined so that it moves all source origins to the same target origin, say
the first input position. Clearly, this gives a functional, regular
resynchronizer that is order-preserving and $\mathbf{C}$-bounded.

#### Correctness of output annotation.

Recall that the properties of the top level resynchronizer $\mathcal{R}_{*}$,
in particular, the claim that $\mathcal{R}_{*}$ is bounded, were crucially
relying on the assumption that every output position $x$ is correctly
annotated with the productive transition that generated it. This assumption
cannot be guaranteed by the MSO sentence $\mathsf{opar}$ alone (the property
intrinsically talks about a relation between input and output annotations).
Below, we explain how to check correctness of the output annotation with the
additional help of the formulas $\mathsf{move}_{\tau}(y,z)$ (that will be
modified for this purpose) and
$\mathsf{next}_{\tau,\tau^{\prime}}(z,z^{\prime})$.

Let $\rho$ be the successful run as encoded by the input annotation. The idea
is to check that the sequence of productive transitions $t_{x}$ that annotate
the positions $x$ in the output is the maximal sub-sequence of $\rho$
consisting only of productive transitions. Besides the straightforward
conditions (concerning, for instance, the first and last productive
transitions of $\rho$, or the possible multiple symbols that could be produced
within a single transition), the important condition to be verified is the
following:

($\dagger$)

The above property is easily expressible by an MSO formula
$\varphi^{\dagger}_{\tau,\tau^{\prime}}(y,y^{\prime})$, assuming that
$\tau,\tau^{\prime}$ are the output types of $x,x+1$ and the free variables
$y$ and $y^{\prime}$ are interpreted by the _source origins_ of $x$ and $x+1$,
with $x$ ranging over all output positions. This is very close to the type of
constraints that can be enforced by the formula
$\mathsf{next}_{\tau,\tau^{\prime}}$ of a regular resynchronizer, with the
only difference that the latter formula can only access the _target origins_
$z,z^{\prime}$ of $x,x+1$.

We thus need a way to uniquely determine from the target origins
$z,z^{\prime}$ of $x$ the source origins $y,y^{\prime}$ of $x$. For this, we
could rely on the formulas $\mathsf{move}_{\tau}(y,z)$, if only they were
defining partial bijections between $y$ and $z$. Those formulas are in fact
close to define partial bijections, as they are functional and $k$-bounded,
for $k=H\cdot 4K\mathbf{C}$. The latter boundedness property, however, depends
again on the assumption that the output annotation is correct. We overcome
this problem by gradually modifying the resynchronizer $\mathcal{R}_{*}$ so as
to make it functional and $1$-bounded (i.e., partially bijective),
independently of the output annotations.

We start by modifying the formulas $\mathsf{move}_{\tau}(y,z)$ to make them
“syntactically” $k$-bounded. Formally, we construct from
$\mathsf{move}_{\tau}(y,z)$ the formula

$\displaystyle\mathsf{move}^{\prime}_{\tau}(y,z)$
$\displaystyle~{}=~{}\mathsf{move}_{\tau}(y,z)$
$\displaystyle\>~{}\wedge~{}\>\forall
y_{1},\dots,y_{k},y_{k+1}~{}\Big{(}\bigwedge\nolimits_{i}\mathsf{move}_{\tau}(y_{i},z)\Big{)}\rightarrow\Big{(}\bigvee\nolimits_{i\neq
j}y_{i}=y_{j}\Big{)}.$

Intuitively, the above formula is semantically equivalent to
$\mathsf{move}_{\tau}(y,z)$ when there are at most $k$ input positions
$y^{\prime}$ that can be paired with $z$ via the same formula
$\mathsf{move}_{\tau}$, and it is false otherwise.

Let $\mathcal{R}^{\prime}_{*}$ be the regular resynchronizer obtained from
$\mathcal{R}_{*}$ by replacing the formulas $\mathsf{move}_{\tau}$ by
$\mathsf{move}^{\prime}_{\tau}$, for every output type $\tau$. By
construction, $\mathcal{R}^{\prime}_{*}$ is functional and $k$-bounded,
independently of any assumption on the output annotations. We can then apply
Lemma 1 and obtain from $\mathcal{R}^{\prime}_{*}$ an equivalent regular
resynchronizer
$\mathcal{R}^{\prime\prime}_{*}=(\overline{I}^{\prime\prime},\overline{O}^{\prime\prime},\mathsf{ipar}^{\prime\prime},\mathsf{opar}^{\prime\prime},(\mathsf{move}^{\prime\prime}_{\tau})_{\tau},(\mathsf{next}^{\prime\prime}_{\tau,\tau^{\prime}})_{\tau,\tau^{\prime}})$
that is $1$-bounded. So each $\mathsf{move}^{\prime\prime}_{\tau}$ is a
partial bijection.

We are now ready to verify the correctness of the output annotation. Recall
that the idea is to enforce the property $(\dagger)$ by exploiting the
previously defined formula
$\varphi^{\dagger}_{\tau,\tau^{\prime}}(y,y^{\prime})$ and the partial
bijection between the source origings $y,y^{\prime}$ and the target origins
$z,z^{\prime}$, as defined by $\mathsf{move}^{\prime\prime}_{\tau}(y,z)$ and
$\mathsf{move}^{\prime\prime}_{\tau^{\prime}}(y^{\prime},z^{\prime})$.
Formally, we define

$\mathsf{next}^{\prime\prime\prime}_{\tau,\tau^{\prime}}(z,z^{\prime})~{}=~{}\mathsf{next}^{\prime\prime}_{\tau,\tau^{\prime}}(z,z^{\prime})~{}\wedge~{}\exists
y,y^{\prime}~{}\mathsf{move}^{\prime\prime}_{\tau}(y,z)~{}\wedge~{}\mathsf{move}^{\prime\prime}_{\tau^{\prime}}(y^{\prime},z^{\prime})~{}\wedge~{}\varphi^{\dagger}_{\tau,\tau^{\prime}}(y,y^{\prime}).$

To conclude, by replacing in $\mathcal{R}^{\prime\prime}$ the formulas
$\mathsf{next}^{\prime\prime}_{\tau,\tau^{\prime}}$ with
$\mathsf{next}^{\prime\prime\prime}_{\tau,\tau^{\prime}}$, we obtain a regular
resynchronizer $\mathcal{R}$ that is partially bijective, $T$-preserving and
such that $\mathcal{R}(T)$ is order-preserving. This completes the proof of
the implication $3\rightarrow 4$ of our main theorem. ∎

##  Appendix 0.E Proof of Theorem 3.2

We provide here the missing details of the proof of Theorem 3.2, as sketched
in Section 6. We recall that the goal is to construct, from a given arbitrary
two-way transducer $T$:

  1. 1.

a bounded-visit transducer $\mathit{low}(T)$ that is classically equivalent to
$T$,

  2. 2.

partially bijective, regular resynchronizer $\mathcal{R}$ that is
$T$-preserving and such that $\mathcal{R}(T)=_{o}\mathit{low}(T)$.

We will reason with a fixed input $u$ at hand and with an induced
accessibility relation on productive transitions of $T$, tagged with origins.
Formally, a _tagged transition_ is any pair $(t,y)$ consisting of a transition
$t\in\Delta$ and a position $y$ on the input $u$, such that $t$ occurs at
position $y$ in some successful run on $u$. The accessibility preorder on
tagged transitions is such that $(t,y)\preceq_{u}(t^{\prime},y^{\prime})$
whenever $T$ has a run on $u$ starting with transition $t$ at position $y$ and
ending with transition $t^{\prime}$ at position $y^{\prime}$. This preorder
induces an equivalence relation, denoted $\sim_{u}$. Intuitively,
$(t,y)\sim_{u}(t^{\prime},y^{\prime})$ means that $T$ can cycle an arbitrary
number of times between these two tagged transitions (possibly
$(t,y)=(t^{\prime},y^{\prime})$). A $\sim_{u}$-equivalence class $C$ is called
_realizable on $u$_ if there is a successful run on $u$ that uses at least
once a tagged transition from the class $C$.

We say that $T$ is _$K$ -sparse_ if for every input $u$ and every realizable
$\sim_{u}$-equivalence class $C$, there are at most $K$ _productive_ tagged
transitions in $C$ (recall that a productive transition is one that produces
non-empty output). Intuitively, bounded sparsity means that the number of
origins of outputs produced by vertical loops in successful runs of $T$ is
uniformly bounded. If $T$ is not $K$-sparse for any $K$, then we say that $T$
has _unbounded sparsity_.

When $T$ is $K$-sparse, the productive tagged transitions from the same
realizable $\sim_{u}$-equivalence class can be lexicographically ordered and
distinguished by means of numbers from a fixed finite range, say
$\\{1,\dots,K\\}$. An important observation is that the equivalence $\sim_{u}$
is a regular property, in the sense that one can construct, for instance, an
MSO formula $\varphi^{\sim_{u}}_{t,t^{\prime}}(y,y^{\prime})$ that holds on
input $u$ if and only if $(t,y)\sim_{u}(t^{\prime},y^{\prime})$. In
particular, this implies that unbounded sparsity can be effectively tested: it
suffices to construct the regular language consisting of every possible input
$u$ with a distinguished realizable $\sim_{u}$-equivalence class marked on it,
and check whether this language contains words with arbitrarily many marked
positions that correspond to productive tagged transitions (this boils down to
detecting special loops in a classical finite-state automaton).

###### Lemma 0.E.1

If $T$ has unbounded sparsity, then $T$ is not one-way definable.

###### Proof

The assumption that $T$ has unbounded sparsity and the definition of
$\sim_{u}$ imply that, for every $n\in\mathbb{N}$, there exist an input $u$, a
successful run $\rho$ on $u$, and $2n$ tagged transitions
$(t_{1},y_{1}),\dots,(t_{n},y_{n})$,
$(t^{\prime}_{1},y^{\prime}_{1}),\dots,(t^{\prime}_{n},y^{\prime}_{n})$ such
that the $t_{i}$’s occur before the $t^{\prime}_{j}$ in $\rho$ and the
$y^{\prime}_{i}$ are to the right of the $y^{\prime}_{j}$. Since $n$ can grow
arbitrarily, this witnesses precisely the fact that $T$ has unbounded cross-
width. Thus, by the implication $1\rightarrow 2$ of Theorem 3.1, which is
independent of $T$ being bounded-visit, we know that $T$ is not one-way
resynchronizable. ∎

Let us now show how to construct a bounded-visit transducer $\mathit{low}(T)$
with regular outputs and common guess that is equivalent to $T$, under the
assumption that $T$ is $K$-sparse for some constant $K$. Intuitively,
$\mathit{low}(T)$ simulates successful runs of $T$ on input $u$ by
shortcutting maximal vertical loops. Formally, for an input $u$ and a tagged
transition $(t,y)$, a _vertical loop_ at $(t,y)$ is any run on $u$ that starts
and ends with transition $t$ at position $y$. We will tacitly focus on
vertical loops that are realizable on $u$, exactly as we did for
$\sim_{u}$-equivalence classes. The output of a vertical loop is the word
spelled out by the productive transitions in it.

Of course, all tagged transitions in a vertical loop at $(t,y)$ are
$\sim_{u}$-equivalent to $(t,y)$. In particular, as $T$ is $K$-sparse, there
are at most $K$ productive tagged transitions in a (realizable) vertical loop,
and hence the language $L_{t,y}$ of outputs of vertical loops at $(t,y)$ is
regular. In addition, there are only finitely many languages $L_{t,y}$ for
varying $(t,y)$. This can be seen as follows: we can assume an order on the
elements of the $\sim_{u}$-class $C$ of $(t,y)$, and a strongly connected
graph with nodes corresponding to $C$ and edges reflecting the accessibility
preorder. The correctness of the graph can be checked with regular annotations
on the input, and the graph itself can be turned into an automaton accepting
$L_{t,y}$. Therefore, using common guess in $\mathit{low}(T)$, we can assume
that every position $y$ carries as annotation the language $L_{t,y}$ for each
transition $t$. By definition, $L_{t,y}$ is non-empty if and only if there is
some productive vertical loop at $(t,y)$.

Consider an arbitrary successful run $\rho$ of $T$ on $u$. Let
$\mathit{low}(\rho)$ be the run obtained by replacing, from left to right,
every maximal vertical loop at $(t,y)$ by the single transition $t$. Here,
maximality refers to the subrun relation. We call $\mathit{low}(\rho)$ the
_normalization of $\rho$_ and we observe that this is a successful,
$|\Delta|$-visit run. This means that (i) $\mathit{low}(\rho)$ can be finitely
encoded on the input as a sequence of flows of height at most $|\Delta|$, and
(ii) the language consisting of inputs annotated with such encodings is
regular.

The transducer $\mathit{low}(T)$ guesses the encoding of a normalization
$\mathit{low}(\rho)$ and uses it to simulate a possible run $\rho$ of $T$. In
particular, every time $\mathit{low}(T)$ traverses a transition $t$ from the
flow of $\mathit{low}(\rho)$ at position $y$, it outputs a word from the
language $L_{t,y}$. However, in order to simplify later the construction of a
resynchronizer $\mathcal{R}$ such that $\mathcal{R}(T)=_{o}\mathit{low}(T)$,
it is convenient that $\mathit{low}(T)$ outputs the word from $L_{t,y}$ in a
possibly different origin, which is uniquely determined by the
$\sim_{u}$-equivalence class of $(t,y)$. Formally, we define the _anchor_ of a
$\sim_{u}$-equivalence class $C$, denoted $\mathit{an}(C)$, to be the leftmost
input position $z$ such that $(t^{\prime},z)\in C$ for some transition
$t^{\prime}$. After traversing a transition $t$ from the flow at position $y$,
and before outputting a word from $L_{t,y}$, the transducer $\mathit{low}(T)$
moves to the anchor $\mathit{an}([(t,y)]_{\sim_{u}})$. Then it outputs the
appropriate word and moves back to position $y$, where it can resume the
simulation of the normalized run $\mathit{low}(\rho)$. Note that the position
$y$ can be recovered from the anchor $\mathit{an}([(t,y)]_{\sim_{u}})$ since
the elements inside the equivalence class $[(t,y)]_{\sim_{u}}$ can be
identified by numbers from $\\{1,\dots,K\\}$ (recall that $T$ is $K$-sparse),
and since the relationship between any two such elements is a regular
property. It is routine to verify that the described transducer
$\mathit{low}(T)$ is equivalent to $T$ and bounded-visit.

Let us now explain how to construct a partially bijective, regular
resynchronizer $\mathcal{R}$ that is $T$-preserving and such that
$\mathcal{R}(T)=_{o}\mathit{low}(T)$. We proceed as in the construction of
$\mathit{low}(T)$ by annotating the input word $u$ with flows that encode the
normalization $\mathit{low}(\rho)$ of a successful run $\rho$ of $T$ on $u$.
As for the output word $v$, we annotate every position $x$ of $v$ with the
productive transition $t=(q,a,v,q^{\prime})$ of $\rho$ that generated $x$. For
short, we call $t$ _the transition of $x$_. In addition, we fix an MSO-
definable total ordering on tagged transitions (e.g. the lexicographic
ordering). Then, we determine from each output position $x$ the
$\sim_{u}$-equivalence class $C=[(t,y)]_{\sim_{u}}$, where $u$ is the
underlying input, $t$ is the productive transition that generated $x$, and $y$
is its origin, and we extend the annotation of $x$ with the index of the
element $(t,y)$ inside the equivalence class $C$, according to the fixed total
ordering on tagged transitions. This number $i$ is called _the index of $x$_.

The resynchronizer $\mathcal{R}$ needs to redirect the source origin $y$ of
any output position generated by a transition $t$ to a target origin $z$ that
is the anchor of the $\sim_{u}$-equivalence class of $(t,y)$. To simplify the
explanation, we temporarily assume that the input and output are correctly
annotated as described above. By inspecting the type $\tau$ of an output
position $x$, the formula $\mathsf{move}_{\tau}(y,z)$ of $\mathcal{R}$ can
determine the transition $t$ of $x$, and enforce that
$(t,y)\sim_{u}(t^{\prime},z)$, for some transition $t^{\prime}$, and that
$(t,y)\not\sim_{u}(t^{\prime\prime},z^{\prime})$, for all $z^{\prime}<z$ and
all transitions $t^{\prime\prime}$. _Under the assumption that the input and
output annotations are correct_ , this would result in a bounded
resynchronizer $\mathcal{R}$. Indeed, for every position $z$, there exist at
most $K\cdot|\Delta|$ positions $y$ that, paired with some productive
transition, turn out to be $\sim_{u}$-equivalent to $(t^{\prime},z)$ for some
transition $t^{\prime}$. Once again, we need to further constrain the relation
$\mathsf{move}_{\tau}(y,z)$ so that it describes a partial bijection between
source and target origins (this will be useful later). For this, it suffices
to additionally enforce that $(t,y)$ is the $i$-th element in its
$\sim_{u}$-equivalence class, accordingly to the fixed total ordering on
tagged transitions, where $i$ is the index specified in the output type $\tau$
of $x$. This latter modification also guarantees that $i$ is the correct index
of $x$.

Unless we further refine our constructions, we cannot claim that they always
result in a $1$-bounded resynchronizer $\mathcal{R}$, since the above
arguments crucially rely on the assumption that the input and output
annotations are correct. However, we can apply the same trick that we used in
the proof of Theorem 3.1, to make the resynchronizer $\mathcal{R}$
“syntactically” $1$-bounded, even in the presence of badly-formed annotations.
Formally, let $\mathsf{move}_{\tau}(y,z)$ be the formula that transforms the
origins in the way described above, and define

$\mathsf{move}^{\prime}_{\tau}(y,z)~{}=~{}\mathsf{move}_{\tau}(y,z)~{}\wedge~{}\forall
y^{\prime}~{}\big{(}\mathsf{move}_{\tau}(y^{\prime},z)\rightarrow
y^{\prime}=y\big{)}.$

By construction, the above formula defines a partial bijection entailing the
old relation $\mathsf{move}_{\tau}$ (in the worst case, when the annotations
are not correct, the above formula may not hold for some pairs of source and
target origins). In addition, if the annotations are correct, then
$\mathsf{move}^{\prime}_{\tau}(y,z)$ is semantically equivalent to
$\mathsf{move}_{\tau}(y,z)$, as desired. In this way, we obtain a regular
resynchronizer
$\mathcal{R}=(\overline{I},\overline{O},\mathsf{ipar},\mathsf{opar},\mathsf{move}^{\prime}_{\tau},\mathsf{next})$
that is always $1$-bounded, no matter how we define $\mathsf{ipar}$,
$\mathsf{opar}$, and $\mathsf{next}$.

We now explain how to check that the annotations are correct. The input
annotation does not pose any particular problem, since the language of inputs
annotated with normalized runs is regular, and can be checked using the first
formula $\mathsf{ipar}$ of the resynchronizer. As for the output annotation,
correctness of the indices was already enforced by the
$\mathsf{move}^{\prime}_{\tau}$ relation. It remains to enforce correctness of
the transitions. Once again, this boils down to verifying the following
property ($\dagger$):

($\dagger$)

From here we proceed exactly as in the proof of Theorem 3.1. We observe that
Property ($\dagger$) is expressible by an MSO formula
$\varphi_{\tau,\tau^{\prime}}^{\dagger}(y,y^{\prime})$, assuming that
$\tau,\tau^{\prime}$ are the output types of $x,x+1$, that $y,y^{\prime}$ are
interpreted by the source origins of $x,x+1$, and that $x$ ranges over all
output positions. We then recall that $\mathsf{move}_{\tau}(y,z)$ and
$\mathsf{move}_{\tau}(y^{\prime},z^{\prime})$ describe partial bijections
between source and target origins, and exploit this enforce ($\dagger$) by
means of the last formula of $\mathcal{R}$:

$\mathsf{next}_{\tau,\tau^{\prime}}(z,z^{\prime})~{}=~{}\exists
y,y^{\prime}~{}\mathsf{move}_{\tau}(y,z)~{}\wedge~{}\mathsf{move}_{\tau^{\prime}}(y^{\prime},z^{\prime})~{}\wedge~{}\varphi_{\tau,\tau^{\prime}}^{\dagger}(y,y^{\prime}).$

This guarantees that all annotations are correct, and proves that
$\mathcal{R}$ is a partially bijective, regular resynchronizer satisfying
$\mathcal{R}(T)=_{o}\mathit{low}(T)$. It is also immediate to see that
$\mathcal{R}$ is $T$-preserving.

We finally prove that one-way resynchronizability of $T$ reduces to one-way
resynchronizability of $\mathit{low}(T)$, which can be effectively tested
using Theorem 3.1 since $\mathit{low}(T)$ is bounded-visit:

See 9

###### Proof

For the right-to-left implication, suppose that
$T^{\prime}=_{o}\mathcal{R}(T)$ is bounded-visit and one-way resynchronizable.
Since $T^{\prime}$ is bounded-visit, we can use the implications $1\rightarrow
2\rightarrow 3\rightarrow 4$ in Theorem 3.1 to get the existence of a
partially bijective, regular resynchronizer $\mathcal{R}^{\prime}$ that is
$T^{\prime}$-preserving and such that $\mathcal{R}^{\prime}(T^{\prime})$ is
order-preserving. By Lemma 2, there is a bounded, regular resynchronizer
$\mathcal{R}^{\prime\prime}$ that is equivalent to
$\mathcal{R}^{\prime}\circ\mathcal{R}$. In particular,
$\mathcal{R}^{\prime\prime}(T)$ is order-preserving. It remains to verify that
$\mathcal{R}^{\prime\prime}$ is also $T$-preserving. Consider any synchronized
pair $\sigma\in{[\\![T]\\!]}_{o}$. Since $\mathcal{R}$ is $T$-preserving,
$\sigma$ belongs to the domain of $\mathcal{R}^{\prime}$, and hence
$(\sigma,\sigma^{\prime})\in\mathcal{R}$ for some synchronized pair
$\sigma^{\prime}\in{[\\![T^{\prime}]\\!]}_{o}$. Since $\mathcal{R}$ is
$T^{\prime}$-preserving, $\sigma^{\prime}$ belongs to the domain of
$\mathcal{R}$, and hence there is
$(\sigma,\sigma^{\prime\prime})\in(\mathcal{R}^{\prime}\circ\mathcal{R})=\mathcal{R}^{\prime\prime}$.
This shows that $\mathcal{R}^{\prime\prime}$ is $T$-preserving, and hence $T$
is one-way resynchronizable.

For the converse direction, suppose that $T^{\prime}$ is bounded-visit, but
not one-way resynchronizable. We apply again Theorem 3.1, but now we use the
contrapositives of the implications $2\rightarrow 3\rightarrow 4\rightarrow
1$, and obtain that $T^{\prime}$ has unbounded cross-width (see Definition 2).

We also recall that
$\mathcal{R}=(\overline{I},\overline{O},\mathsf{ipar},(\mathsf{move}_{\tau})_{\tau},(\mathsf{next}_{\tau,\tau^{\prime}})_{\tau,\tau})$
is partially bijective. This means that every formula
$\mathsf{move}_{\tau}(y,z)$ defines a partial bijection from source to target
positions. A useful property of every MSO-definable partial bijection is that,
for every position $t$, it can only define boundedly many pairs $(y,z)$ with
either $y\leq t<z$ or $z\leq t<y$ — for short, we say call such a pair $(y,z)$
_$t$ -separated_. This follows from compositional properties of regular
languages. Indeed, let $\mathcal{A}$ be a deterministic automaton equivalent
to the formula that defines the partial bijection. For every pair $(y,z)$ in
the partial bijection, let $q_{y,z}$ be the state visited at position $t$ by
the successful run of $\mathcal{A}$ on the input annotated with the pair
$(y,z)$. If $\mathcal{A}$ accepted more than $|Q|$ pairs that are
$t$-separated, where $Q$ is the state space of $\mathcal{A}$, then at least
two of them, say $(y,z)$ and $(y^{\prime},z^{\prime})$, would satisfy
$q_{y,z}=q_{y^{\prime},z^{\prime}}$. But this would imply that the pair
$(y,z^{\prime})$ is also accepted by $\mathcal{A}$, which contradicts the
assumption that $\mathcal{A}$ defines a partial bijection.

We now exploit the above result to prove that the property of having unbounded
cross-width transfers from $T^{\prime}$ to $T$. Consider a cross
$(X_{1},X_{2})$ of arbitrarily large width $h$ in some synchronized pair
$\sigma=(u,v,\mathit{orig})$ of $T^{\prime}$. Without loss of generality,
assume that all positions in $X_{1}\cup X_{2}$ have the same type $\tau$. Let
$Z_{i}=\mathit{orig}(X_{i})$, for $i=1,2$, and $t=\max(Z_{2})$. By definition
of cross, we have $X_{1}<X_{2}$ and $Z_{2}\leq t<Z_{1}$. Recall that
$\mathsf{move}_{\tau}$ defines a partial bijection, and that this implies that
there are only boundedly many pairs of source-target origins that are
$t$-separated, say $(y_{1},z_{1}),\dots,(y_{k},z_{k})$ for a constant $k$ that
only depends on $\mathcal{R}$. Moreover, since
$\mathcal{R}(T)=_{o}T^{\prime}$, the positions in $Z_{i}$ can be seen as
target origins of the formula $\mathsf{move}_{\tau}$ of $\mathcal{R}$. Now,
let $X^{\prime}_{i}=X_{i}\setminus\mathit{orig}^{-1}(\\{z_{1},\dots,z_{k}\\}$
and $Y^{\prime}_{i}=\mathit{orig}^{\prime}(X^{\prime}_{i})$, for any
synchronized pair $\sigma^{\prime}=(u,v,\mathit{orig}^{\prime})$ such that
$(\sigma,\sigma^{\prime})\in\mathcal{R}$. By construction, we have
$X^{\prime}_{1}<X^{\prime}_{2}$ and $Y^{\prime}_{2}\leq t<Y^{\prime}_{1}$ (the
latter condition follows from the fact that the source origins from
$Y^{\prime}_{i}$ can only be moved to target origins on the same side w.r.t.
$t$). This means that $(X^{\prime}_{1},X^{\prime}_{2})$ is a cross of width
$h-k$. As $h$ can be taken arbitrarily large and $k$ is constant, this proves
that $T$ has unbounded cross-width as well.

Finally, by the contrapositive of the implication $1\rightarrow 2$ of Theorem
3.1 (which does not need the assumption that $T$ is bounded-visit), we
conclude that $T$ is not one-way resynchronizable. ∎

Summing up, the algorithm that decides whether a given two-way transducer $T$
is one-way resynchronizable first verifies that $T$ is $K$-sparse for some $K$