# Resynchronized Uniformization and Definability Problems for Rational
Relations††thanks: This work was supported by the DFG grant LO 1174/3.

Christof Löding1  Sarah Winter2 This work is supported by the MIS project
F451019F (F.R.S.-FNRS). Sarah Winter is a postdoctoral researcher at
F.R.S.-FNRS.  RWTH Aachen University, Germany
Université libre de Bruxelles, Belgium

(yyyy-mm-dd; yyyy-mm-dd; yyyy-mm-dd)

###### Abstract

Regular synchronization languages can be used to define rational relations of
finite words, and to characterize subclasses of rational relations, like
automatic or recognizable relations. We provide a systematic study of the
decidability of uniformization and definability problems for subclasses of
rational relations defined in terms of such synchronization languages. We
rephrase known results in this setting and complete the picture by adding
several new decidability and undecidability results.

###### keywords:

rational relations, transducer, synchronization languages, uniformization,
definability

##  1 Introduction

In this paper we study uniformization and definability problems for subclasses
of rational relations over finite words. The class of (binary) rational
relations is defined by transducers, that is, nondeterministic finite state
automata in which each transition is annotated with a pair of an input and an
output word (see Berstel (1979); Sakarovitch (2009)). One can also view such a
transducer as a two-tape automaton that processes two given words with two
reading heads. The two heads can process their word at different speeds (for
example, in each transition one can read only one letter on the first tape and
two letters on the second tape). While the class of rational relations is
rather expressive, it does not have good algorithmic and closure properties
(see Berstel (1979)). For example, the class is not closed under intersection
and complement, and the universality problem (whether a given transducer
accepts all pairs of words) is undecidable.

One obtains subclasses of rational relations by restricting the way the two
heads can move on their tapes. An important such subclass of rational
relations are synchronous rational relations, often called automatic
relations, see Frougny and Sakarovitch (1993); Khoussainov and Nerode (1994);
Blumensath and Grädel (2000). These are obtained when restricting the
transducers to move synchronously on the two tapes, that is, reading in each
transition one letter from each word (that has not yet been fully read).
Automatic relations enjoy many closure and algorithmic properties that make
them, for example, a suitable tool in decision procedures for logic, see
Blumensath and Grädel (2000).

The class of recognizable relations is obtained when processing the two words
completely asynchronously, that is, the transducer completely reads the word
on the first tape, and then it reads the word on the second tape. It is not
hard to see that recognizable relations are finite unions of products of
regular languages, see (Berstel, 1979, Chapter III, Theorem 1.5).

The definability problem for two classes $C_{1},C_{2}$ of word relations is
the problem of deciding for a given relation in $C_{1}$ whether it is in
$C_{2}$. For example, if $C_{1}$ is the class of rational relations, and
$C_{2}$ the class of automatic relations, then the problem is to decide
whether a given rational relation can be defined by a synchronous transducer.
This problem was shown undecidable by (Frougny and Sakarovitch, 1993,
Proposition 5.5), and also the definability problem for rational and
recognizable relations was shown undecidable by (Berstel, 1979, Chapter III,
Theorem 8.4). A systematic study of definability problem for some important
subclasses of rational relations is given by Carton et al. (2006).

In this paper, we consider a more general version of the definability problem,
where the subclasses of rational relations are defined by synchronization
languages, a formalism that has been introduced and studied by Figueira and
Libkin (2015); Descotte et al. (2019). In that setting, a synchronization
language is a language over the alphabet $\\{1,2\\}$, specifying how the two
heads of a transducer are allowed to move on the two tapes. For example, the
word $1121222$ indicates that two symbols from the first tape are read, then
one symbol from the second tape, then one symbol from the first tape, and then
three symbols from the second tape. Each run of a transducer defines such a
synchronization word. Therefore, a regular synchronization language $L$
defines a subclass of the rational relations, namely all relations that can be
defined by a transducer whose runs have synchronization words in $L$. For
example, the class of automatic relations is defined by the synchronization
language $(12)^{*}(1^{*}+2^{*})$, and the class of recognizable relations by
$1^{*}2^{*}$, see Figueira and Libkin (2015).

We consider here a more general version of synchronization languages. Assuming
that the input (first tape) alphabet $\Sigma$, and the output (second tape)
alphabet $\Gamma$ of the relation are disjoint, we consider synchronization
languages that are regular subsets of $(\Sigma\cup\Gamma)^{*}$. A word over
$(\Sigma\cup\Gamma)^{*}$ does not just specify in which order the heads move
along the tape, but also which symbols have to be read in each step. This way,
it is possible to capture subclasses of rational relations that cannot be
captured with the synchronization languages over $\\{1,2\\}$, as for example
the class of prefix-recognizable relations (see Section 4.2.3). Another
motivation for studying this more general formalism of synchronization
languages is its tight connection to origin semantics.

Origin semantics is motivated by the intractability of, e.g., the equivalence
problem for rational relations (whether two given transducers recognize the
same relation), which stems from the fact that two transducers recognizing the
same relation may produce their outputs very differently. This is witnessed by
their different synchronization languages. To overcome this difficulty
Bojańczyk (2014); Bojańczyk et al. (2017) have introduced and studied
transducers with origin semantics, that is, additionally, there is an origin
function that maps output positions to their originating input positions. The
main result of Bojańczyk (2014) is a machine-independent characterization of
relations defined by two-way transducers with origin semantics (Bojańczyk,
2014, Theorem 1). Using the origin semantics, many interesting problems become
decidable, e.g., deciding whether two given (one-way) transducers are
equivalent reduces to deciding whether their synchronization languages are
equal. However, the origin semantic is rather rigid. To mitigate this, Filiot
et al. (2016) have introduced a similarity measure between (one-way111The
introduction of this measure has triggered similar work on two-way
transducers, see Bose et al. (2018, 2019).) transducers with origin semantics
which amounts to a similarity measure between their synchronization languages.
Restricting, for example, the equivalence problem to transducers that have
‘similar’ synchronization languages allows to regain decidability. Since
origin semantics of transducers cannot be captured by synchronization
languages over $\\{1,2\\}$, this is another motivation for studying the
formalism of synchronization languages over $\Sigma\cup\Gamma$. For example, a
synchronization language over $\Sigma\cup\Gamma$ can capture all transducers
that behave similarly to a given one in the above mentioned measure.

We study here the decidability of the definability problem, whether a given
rational, automatic, or recognizable relation can be defined inside a given
synchronization language $T$ for different classes of synchronization
languages. The results are summarized in Table 2 on Table 2. An explanation of
the results is given in Section 4.1. We note here that another kind of
definability problem in the context of synchronization languages has been
studied by Descotte et al. (2018): Given two synchronization languages (over
$\\{1,2\\}$), are all relations that are definable with the first
synchronization language also definable with the second synchronization
language? So the definability problem considered by Descotte et al. (2018) is
on the level of classes of relations, while we study definability for
individual relations.

Furthermore, we also study the uniformization problem for subsequential
transducers. A uniformization of a binary relation $R$ is a subset of $R$ that
defines a function and that has the same domain as $R$, so the function
selects precisely one image for each element in the domain. In our setting, we
are given a relation over finite words, and ask whether this relation has a
uniformization that can be computed by a subsequential transducer. A
subsequential transducer is a transducer that is deterministic on the input
symbols, and produces in each step a finite sequence of output symbols (the
prefix “sub” refers to the fact that the transducer can make a final output at
the end of the word). The uniformization problem by synchronous sequential
transducers (that read in each step one input symbol and produce one output
symbol) has first been studied for automatic relations over infinite words in
the context of synthesizing sequential functions from a logic specification by
Büchi and Landweber (1969). The setting in which the sequential transducer
needs not be synchronous has been considered by Hosch and Landweber (1972);
Holtmann et al. (2010).

While the decidability results for uniformization of automatic relations by
synchronous sequential transducers can easily be transferred from infinite to
finite words, the problem becomes different when the sequential transducer
needs not be synchronous. Decidability for uniformization of automatic
relations by subsequential transducers has been shown by (Carayol and Löding,
2014, Theorem 18), and for other subclasses of rational relations (finite
valued and deterministic rational relations) by Filiot et al. (2016). For
rational relations, the problem becomes undecidable, see (Carayol and Löding,
2014, Theorem 17) (however, each rational relation has a uniformization by a
rational function, see Sakarovitch (2009), which needs not be subsequential).

The problem of uniformization by subsequential transducers does not impose any
restrictions on how the subsequential transducer produces its output. If one
is, for example, interested in uniformization by subsequential transducers
that have a bound $k$ on the delay between input and output (the difference of
the length of the processed input and the produced output), then this can be
captured by using a regular synchronization language as another parameter to
the problem. The subsequential transducer then has to produce its output in
such a way that the resulting interleaving of input and output is inside the
given synchronization language. As an example (of unbounded delay between
input and output), transducers that produce exactly two output symbols for
each input symbol are captured by the synchronization language
$(\Sigma\Gamma\Gamma)^{*}$.

Uniformization of automatic relations by subsequential transducers with a
synchronization language of finite shiftlag (which roughly corresponds to the
bounded delay case mentioned in the previous paragraph) has been shown to be
decidable by Winter (2018). Uniformization of rational relations by
subsequential transducers with a synchronization language ‘similar’ to the one
of the given transducer has been studied in Filiot et al. (2016).

Our contribution is a systematic overview and some new results of
uniformization problems for rational, automatic, and recognizable relations by
subsequential transducers for different classes of synchronization languages.
An overview is given in Table 1 on Table 1, and the results are explained in
more detail in Section 3.1.

The paper is structured as follows. In Section 2 we provide definitions and
terminology used throughout the paper. In Section 3 we present results on
uniformization, and in Section 4 we consider definability problems.

##  2 Preliminaries

In this section, we introduce our terminology and recall some results that are
used throughout the paper. Let $\mathbbm{N}$ denote the set of non-negative
integers.

##### Words, languages, relations, and uniformizations.

An _alphabet_ is a finite non-empty set of _symbols_ , also called _letters_.
We denote alphabets by $\Sigma$ and $\Gamma$. A _word_ over $\Sigma$ is a
possibly empty finite sequence $a_{1}\cdots a_{n}$ of symbols from $\Sigma$.
The empty word is denoted by $\varepsilon$. Given a word $w$, we denote by
$|w|$ its length, that is, the number of symbols in $w$, by $|w|_{a}$ the
number of occurrences of letter $a$ in $w$, by $w[i]$ its $i$th symbol, and by
$w[i:j]$ its infix $w[i]\cdots w[j]$ for $i\leq j$.

We denote by $\Sigma^{-1}$ the set of symbols $a^{-1}$ for all $a\in\Sigma$.
Any word $w$ over $\Sigma\cup\Sigma^{-1}$ can be reduced into a unique
irreducible word using the free group equations $aa^{-1}=a^{-1}a=\varepsilon$
for all $a\in\Sigma$, e.g., $c^{-1}abb^{-1}a^{-1}a=c^{-1}a$.

Let $\Sigma^{*}$, and $\Sigma^{+}$ denote the set of finite and non-empty
finite words over $\Sigma$, respectively. We write $\Sigma^{k}$ for
$\underbrace{\Sigma\cdots\Sigma}_{k\text{ times}}$, and $\Sigma^{\leq k}$ for
$\bigcup_{i=0}^{k}\Sigma^{i}$. A _language_ $L$ is a subset of $\Sigma^{*}$,
its set of prefixes is denoted by $\mathrm{Prefs}(L)$, and $u^{-1}L$ is the
set $\\{v\mid uv\in L\\}$.

A (binary) _relation_ $R$ is a subset of $\Sigma^{*}\times\Gamma^{*}$, its
domain $\mathrm{dom}(R)$ is the set $\\{u\mid(u,v)\in R\\}$, and $(u,v)^{-1}R$
is the relation $\\{(x,y)\mid(ux,vy)\in R\\}$.

A _uniformization_ of a relation $R\subseteq\Sigma^{*}\times\Gamma^{*}$ is a
total function $f\colon\mathrm{dom}(R)\to\Gamma^{*}$ such that $(u,f(u))\in R$
for all $u\in\mathrm{dom}(R)$.

##### Synchronization languages.

We consider relations over $\Sigma^{*}\times\Gamma^{*}$, and refer to $\Sigma$
as input alphabet and to $\Gamma$ as output alphabet. We assume that $\Sigma$
and $\Gamma$ are disjoint, if not, we annotate every symbol in $\Sigma$ with
$1$ and every symbol in $\Gamma$ with $2$ to make them disjoint. A language
over $\Sigma\cup\Gamma$ then encodes a relation over
$\Sigma^{*}\times\Gamma^{*}$, as explained in the following. For
$c\in\\{\mathbbmtt{i},\mathbbmtt{o}\\}$, referring to input and output,
respectively, we define two functions
$\pi_{c}\colon(\Sigma\cup\Gamma)\rightarrow(\Sigma\cup\Gamma\cup\\{\varepsilon\\})$
by $\pi_{\mathbbmtt{i}}(a)=a$, $\pi_{\mathbbmtt{o}}(a)=\varepsilon$ if
$a\in\Sigma$, and $\pi_{\mathbbmtt{i}}(a)=\varepsilon$,
$\pi_{\mathbbmtt{o}}(a)=a$ if $a\in\Gamma$. These functions are lifted to
words over $\Sigma\cup\Gamma$ by applying them to each letter. A word
$w\in(\Sigma\cup\Gamma)^{*}$ is a _synchronization_ of the uniquely determined
pair $(u,v)\in\Sigma^{*}\times\Gamma^{*}$ with $u=\pi_{\mathbbmtt{i}}(w)$ and
$v=\pi_{\mathbbmtt{o}}(w)$. We write $\llbracket w\rrbracket$ to denote
$(u,v)$. Then a language $S\subseteq(\Sigma\cup\Gamma)^{*}$ of
synchronizations defines the relation $\llbracket S\rrbracket=\\{\llbracket
w\rrbracket\mid w\in S\\}$. Such languages over $\Sigma\cup\Gamma$ are called
_synchronization languages_.

Given a synchronization language $S\subseteq(\Sigma\cup\Gamma)^{*}$, we say a
word $w\in(\Sigma\cup\Gamma)^{*}$ is _$S$ -controlled_ if $w\in S$. A language
$T\subseteq(\Sigma\cup\Gamma)^{*}$ is _$S$ -controlled_ if all its words are,
namely, if $T\subseteq S$.

##### Lag, shift, and shiftlag.

Different classes of automaton definable relations can be defined in terms of
the interleaving of input and output symbols in synchronization languages, see
Figueira and Libkin (2015). These characterizations make use of the notions
lag, shift, and shiftlag, as defined below. For the examples illustrating
these definitions, consider $\Sigma=\\{a\\}$ and $\Gamma=\\{b\\}$. Given a
word $w\in(\Sigma\cup\Gamma)^{*}$, a position $i\leq|w|$, and
$\gamma\in\mathbbm{N}$, we say $i$ is _$\gamma$ -lagged_ if the absolute value
of the difference between the number of input and output symbols in $w[1:i]$
is $\gamma$, e.g., the last position $5$ in the word $abaaa$ is $3$-lagged.
Likewise, we define the notions _$ >\\!\\!\gamma$-lagged_ and _$
<\\!\\!\gamma$-lagged_.

Given a word $w\in(\Sigma\cup\Gamma)^{*}$, a _shift_ of $w$ is a position
$i\in\\{1,\dots,|w|-1\\}$ such that $w[i]\in\Sigma\leftrightarrow
w[i+1]\notin\Sigma$. Two shifts $i<j$ are _consecutive_ if there is no shift
$\ell$ such that $i<\ell<j$.

Given a word $w\in(\Sigma\cup\Gamma)^{*}$, let $\mathit{shift}(w)$ be the
number of shifts in $w$, let $\mathit{lag}(w)$ be the maximum lag of a
position in $w$, and let $\mathit{shiftlag}(w)$ be the maximum
$n\in\mathbbm{N}$ such that $w$ contains $n$ consecutive shifts which are
$>\\!\\!n$-lagged.

As an example consider the word $w=aabaabbbbbbbaaab$: $\mathit{lag}(w)$ is
$4$, because position twelve (at the end of the $b$-block) is $4$-lagged;
$\mathit{shift}(w)$ is $5$; $\mathit{shiftlag}(w)$ is $2$, because the two
consecutive shifts at positions five and twelve are $>\\!\\!2$-lagged.

We lift these notions to languages by taking the supremum in
$\mathbbm{N}\cup\\{\infty\\}$, e.g.,
$\mathit{shift}(S)=\mathrm{sup}\\{\mathit{shift}(w)\mid w\in S\\}$, and
likewise for $\mathit{lag}(S)$ and $\mathit{shiftlag}(S)$. For example, the
language $a^{*}b^{*}a^{*}$ has infinite lag and shiftlag of $2$, the language
$a^{*}b^{*}a^{*}b^{*}$ has shiftlag of $3$.

######  Theorem 1 ((Figueira and Libkin, 2015, Theorem 2)).

Let $S\subseteq(\Sigma\cup\Gamma)^{*}$ be a regular language. It is decidable
whether

  1. 1.

$\mathit{lag}(S)$ is finite,

  2. 2.

$\mathit{shift}(S)$ is finite, and

  3. 3.

$\mathit{shiftlag}(S)$ is finite.

##### Automata.

A _non-deterministic finite state automaton (NFA)_ is a tuple
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F)$, where $Q$ is a finite set of _states_
, $\Sigma$ is an alphabet, $q_{0}\in Q$ is an _initial state_ ,
$\Delta\subseteq Q\times\Sigma\times Q$ is a _transition relation_ , and
$F\subseteq Q$ is a set of _final states_. A _run_ $\rho$ of $\mathcal{A}$
from a state $p_{0}$ to a state $p_{n}$ on a non-empty word $w=a_{1}\cdots
a_{n}$ is a non-empty sequence of transitions
$(p_{0},a_{1},p_{1})(p_{1},a_{2},p_{2})\cdots(p_{n-1},a_{n},p_{n})\in\Delta^{*}$.
We write $\mathcal{A}\colon p_{0}\xrightarrow{w}p_{n}$ if such a run exists. A
_run_ on the empty word is a single state, we write $\mathcal{A}\colon
p\xrightarrow{\varepsilon}p$. A run is _accepting_ if it starts in the initial
state and ends in a final state. For each state $q\in Q$, we denote by
$\mathcal{A}_{q}$ the NFA that is obtained from $\mathcal{A}$ by setting the
initial state to $q$.

The language _recognized_ by $\mathcal{A}$ is
$L(\mathcal{A})=\\{w\in\Sigma^{*}\mid\mathcal{A}\colon
q_{0}\xrightarrow{w}q\in F\\}$. The class of languages recognized by NFAs is
the class of _regular_ languages.

An NFA is _deterministic_ (a DFA) if for each state $q\in Q$ and $a\in\Sigma$
there is at most one outgoing transition. In this case, it is more convenient
to express $\Delta$ as a (partial) function $\delta:Q\times\Sigma\rightarrow
Q$. Furthermore, let $\delta^{*}$ denote the usual extension of $\delta$ from
symbols to words.

##### Transducers.

A _non-deterministic finite state transducer (NFT)_ , _transducer_ for short,
is a tuple $\mathcal{T}=(Q,\Sigma,\Gamma,q_{0},\Delta,F,f)$, where $Q$ is
finite set of states, $\Sigma$ and $\Gamma$ are alphabets, $q_{0}\in Q$ is an
initial state, $\Delta\subseteq Q\times\Sigma^{*}\times\Gamma^{*}\times Q$ is
a finite set of transitions, $F\subseteq Q$ is set of final states, and
$f\colon F\to\Gamma^{*}$ is a _final output function_. A _non-empty run_
$\rho$ is a non-empty sequence of transitions
$(p_{0},u_{1},v_{1},p_{1})(p_{1},u_{2},v_{2},p_{2})\cdots(p_{n-1},u_{n},v_{n},p_{n})\in\Delta^{*}$.
The _input_ (resp.  _output_) of $\rho$ is $u=u_{0}\cdots u_{n}$ (resp.
$v=v_{0}\cdots v_{n}$). Shorthand, we write $\mathcal{T}\colon
p_{0}\xrightarrow{u|v}p_{n}$. An _empty run_ is a single state, we write
$\mathcal{T}\colon p\xrightarrow{\varepsilon|\varepsilon}p$. A run is
_accepting_ if it starts in the initial state and ends in a final state.

The relation _recognized_ by $\mathcal{T}$ is $R(\mathcal{T})=\\{(u,v\cdot
f(q))\in\Sigma^{*}\times\Gamma^{*}\mid\mathcal{T}\colon
q_{0}\xrightarrow{u|v}q\in F\\}$. The class of relations recognized by NFTs is
the class of _rational_ relations. The transducer is _subsequential_ if each
transition reads exactly one input symbol and the transitions are
deterministic on the input, in other words, if $\Delta$ corresponds to a
(partial) function $Q\times\Sigma\to\Gamma^{*}\times Q$. Then it defines a
_subsequential function_.

A transducer induces a synchronization language in a natural way. A
synchronization of a pair of words can be seen as a representation of how a
transducer consumes the input and output word of a pair. We denote the
synchronization language of a transducer $\mathcal{T}$ by $S(\mathcal{T})$
which is formally defined as the set

$\begin{array}[]{l}\\{u_{1}v_{1}u_{2}v_{2}\cdots
u_{n}v_{n}f(p_{n})\in(\Sigma\cup\Gamma)^{*}\mid\\\
\qquad\qquad\qquad(q_{0},u_{1},v_{1},p_{1})(p_{1},u_{2},v_{2},p_{2})\cdots(p_{n-1},u_{n},v_{n},p_{n})\in\Delta^{*}\text{
and }p_{n}\in F\\}.\end{array}$

It is easy to see that an NFA for $S(\mathcal{T})$ can be obtained from
$\mathcal{T}$. Note that this directly implies that $S(\mathcal{T})$ is
regular. Given a regular language $S\subseteq(\Sigma\cup\Gamma)^{*}$, we say
that $\mathcal{T}$ is _$S$ -controlled_ if $S(\mathcal{T})$ is $S$-controlled.
We say that $\mathcal{T}$ has _finite lag_ (_shift_ resp.  _shiftlag_) if
$S(\mathcal{T})$ has finite lag (shift resp. shiftlag).

Conversely, for a regular synchronization language $S$ one can easily
construct a transducer $\mathcal{T}$ such that $S(\mathcal{T})=S$.

##### Characterization of relation classes via synchronization languages.

In this work, we consider classes of relations that can be defined by regular
synchronization languages, that is, subclasses of rational relations. Two
standard subclasses of rational relations are automatic relations which are
relations that can be defined in terms of automata that synchronously read
input and output symbols, and recognizable relations which are relations that
can be expressed as finite unions of products of regular languages (see, e.g.,
Carton et al. (2006)). We do not formalize these definitions here because we
are working with a different characterization of these relation classes, as
explained below. We denote by Rec, Aut, and Rat the classes of recognizable,
automatic, and rational relations, respectively. It is well-known that
$\textsc{Rec}\subsetneq\textsc{Aut}\subsetneq\textsc{Rat}$.

We recall the connection between these classes of relations and
synchronization languages as established by Figueira and Libkin (2015). For a
regular synchronization language $S\subseteq(\Sigma\cup\Gamma)^{*}$, let

$\textsc{Rel}(S)=\\{\llbracket
T\rrbracket\\!\mid\\!T\subseteq(\Sigma\cup\Gamma)^{*}\text{ is a regular
$S$-controlled language}\\}$

be the set of relations that can be given by regular $S$-controlled
synchronization languages.

######  Proposition 2 (Figueira and Libkin (2015)).

The following properties hold.

  1. 1.

$\textsc{Rel}(\Sigma^{*}\Gamma^{*})=\textsc{Rec}$.

  2. 2.

$\textsc{Rel}((\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*}))=\textsc{Aut}$.

  3. 3.

$\textsc{Rel}((\Sigma+\Gamma)^{*})=\textsc{Rat}$.

Let $\textsc{Reg}_{\mathsf{all}}$ be the class of all regular synchronization
languages, $\textsc{Reg}_{\mathsf{FSL}}$ and $\textsc{Reg}_{\mathsf{FS}}$ be
the class of regular synchronization languages with finite shiftlag and finite
shift, respectively. Clearly,
$\textsc{Reg}_{\mathsf{FS}}\subsetneq\textsc{Reg}_{\mathsf{FSL}}\subsetneq\textsc{Reg}_{\mathsf{all}}$.
We have the following result.

######  Theorem 3 (Figueira and Libkin (2015)).

Let $S\subseteq(\Sigma\cup\Gamma)^{*}$ be a regular language, then:

  1. 1.

$\textsc{Rel}(S)\subseteq\textsc{Rec}$ iff $S\in\textsc{Reg}_{\mathsf{FS}}$,

  2. 2.

$\textsc{Rel}(S)\subseteq\textsc{Aut}$ iff $S\in\textsc{Reg}_{\mathsf{FSL}}$,

  3. 3.

$\textsc{Rel}(S)\subseteq\textsc{Rat}$ iff $S\in\textsc{Reg}_{\mathsf{all}}$.

Note that the previous theorem is a statement about the class of relations
$\textsc{Rel}(S)$ defined by all regular subsets of $S$. In particular, if
$S\in\textsc{Reg}_{\mathsf{FS}}$ then $\llbracket S\rrbracket\in\textsc{Rec}$,
if $S\in\textsc{Reg}_{\mathsf{FSL}}$ then $\llbracket
S\rrbracket\in\textsc{Aut}$. However, the converse generally does not hold,
e.g., consider $S=(\Sigma\cup\Gamma)^{*}$, clearly $\llbracket
S\rrbracket=(\Sigma^{*}\times\Gamma^{*})\in\textsc{Rec}$ but
$S\notin\textsc{Reg}_{\mathsf{FS}}$.

Given a class $\mathcal{C}$ of regular languages over $\Sigma\cup\Gamma$, we
say that a regular language $S_{0}\subseteq(\Sigma\cup\Gamma)^{*}$ is a
_canonical representative_ of $\mathcal{C}$ if
$\textsc{Rel}(S_{0})=\bigcup_{S\in\mathcal{C}}\textsc{Rel}(S)$. A canonical
representative is called _effective_ if for each regular $S$-controlled
$T\subseteq(\Sigma\cup\Gamma)^{*}$ for some $S\in\mathcal{C}$ there is a
regular $S_{0}$-controlled $T^{\prime}\subseteq(\Sigma\cup\Gamma)^{*}$ such
that $\llbracket T\rrbracket=\llbracket T^{\prime}\rrbracket$ and $T^{\prime}$
can be constructed in finite time.

######  Theorem 4 (Figueira and Libkin (2015)).

The following properties hold.

  1. 1.

$\Sigma^{*}\Gamma^{*}$ is an effective canonical representative of
$\textsc{Reg}_{\mathsf{FS}}$.

  2. 2.

$(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$ is an effective canonical
representative of $\textsc{Reg}_{\mathsf{FSL}}$.

  3. 3.

$(\Sigma+\Gamma)^{*}$ is an effective canonical representative of
$\textsc{Reg}_{\mathsf{all}}$.

##  3 Uniformization problems

In this section, we take a systematic look at uniformization problems defined
by synchronization languages in the classes
$\textsc{Reg}_{\mathsf{all}},\textsc{Reg}_{\mathsf{FSL}}$, and
$\textsc{Reg}_{\mathsf{FS}}$. Roughly speaking, these problems are about
deciding whether a given relation (given by a synchronization language $S$),
has a uniformization by a subsequential transducer whose synchronization
language is contained in a given synchronization language $T$.

We begin with an example of a rational relation that is uniformizable by a
subsequential transducer. Afterwards, we formally define our problem settings.

######  Example 5.

Consider the rational relation over the input alphabet $\Sigma=\\{a,b\\}$ and
the output alphabet $\Gamma=\\{c\\}$

$R_{1}=\\{(aw,c^{|w|_{a}})\mid w\in\Sigma^{*}\\}\cup\\{(wb,c^{|w|_{b}})\mid
w\in\Sigma^{*}\\}$

defined by the synchronization language $ac(ac+b)^{*}+(a+bc)^{*}bc$. The
relation is uniformized by the subsequential transducer depicted in Figure 1
on the left-hand side. If the input starts with $a$, then the transducer
produces output $c$ for each input $a$ and no output for an input $b$, and
vice versa otherwise.

$a|c$$b|c$$a|c,b|\varepsilon$$b|c$$a|\varepsilon$$b|c$$a|\varepsilon$$\varepsilon$$\varepsilon$$a|\varepsilon$$b|d,c|e$$a|d$$\varepsilon$
Figure 1:  The subsequential transducer on the left uniformizes the relation
$R_{1}$ from Example 5, the subsequential transducer on the right uniformizes
the relation $R_{2}$ from Example 7.

The general problem whether a rational relation has a uniformization by a
subsequential transducer is undecidable, see (Carayol and Löding, 2014,
Theorem 17). We consider the decision problem that introduces a parameter $T$
for the synchronizations that the subsequential transducer can use:

######  Definition 6 (Resynchronized uniformization problem).

The _resynchronized uniformization problem_ asks, given a regular source
language $S\subseteq(\Sigma\cup\Gamma)^{*}$ and a regular target language
$T\subseteq(\Sigma\cup\Gamma)^{*}$, whether there exists a $T$-controlled
subsequential transducer that uniformizes $\llbracket S\rrbracket$.

We start by giving an example.

######  Example 7.

Consider the rational relation over the input alphabet $\Sigma=\\{a,b,c\\}$
and output alphabet $\Gamma=\\{d,e\\}$

$R_{2}=\\{(a^{i}ba^{j},d(d+e)^{k})\mid i,j,k\geq
0\\}\cup\\{(a^{i}ca^{j},e(d+e)^{k})\mid i,j,k\geq 0\\}$

defined by the synchronization language
$S=da^{*}ba^{*}(d+e)^{*}+ea^{*}ca^{*}(d+e)^{*}$. Furthermore, consider
$T=\Sigma^{*}(\Sigma\Gamma)^{+}$. The relation is uniformized by the
$T$-controlled subsequential transducer depicted in Figure 1 on the right-hand
side. The uniformization realized by the transducer maps inputs of the form
$a^{i}ba^{j}$ to $d^{j+1}$ and inputs of form $a^{i}ca^{j}$ to $ed^{j}$ for
all $i,j\geq 0$.

$R_{2}$ can also be uniformized by a subsequential transducer that is
$(\Sigma^{*}\Gamma^{*})$-controlled. To be more specific, $R_{2}$ can be
uniformized by a subsequential transducer that is
$(\Sigma^{*}\Gamma)$-controlled. Such a transducer can first read the whole
input, and then output $d$ if the input is of the form $a^{*}ba^{*}$, and
output $e$ if the input is of the form $a^{*}ca^{*}$.

But $R_{2}$ cannot be uniformized by a subsequential transducer that is
$(\Sigma\Gamma)^{*}$-controlled. Such a transducer would have to make the
first output after reading the first input symbol. If this input symbol is
$a$, then it is not yet decided if the output has to start with $d$ or with
$e$.

###  3.1 Overview of the results

target source |  rational $S\in\textsc{Reg}_{\mathsf{all}}$ |  automatic $S\in\textsc{Reg}_{\mathsf{FSL}}$ |  recognizable $S\in\textsc{Reg}_{\mathsf{FS}}$
---|---|---|---
unrestricted $T=(\Sigma\cup\Gamma)^{*}\in\textsc{Reg}_{\mathsf{all}}$ |  undec. (Carayol and Löding, 2014, Theorem 17) |  dec. (Carayol and Löding, 2014, Theorem 18) | always
synchronous $T\\!=\\!(\Sigma\Gamma)^{*}(\Sigma^{*}\\!+\\!\Gamma^{*})\\!\in\\!\textsc{Reg}_{\mathsf{FSL}}$ |  undec. (Corollary 12) |  dec. Büchi and Landweber (1969) | dec.
input before output $T=\Sigma^{*}\Gamma^{*}\in\textsc{Reg}_{\mathsf{FS}}$ |  dec. (Theorem 9) |  dec. (Carayol and Löding, 2014, Proposition 20) | always
$T\in\textsc{Reg}_{\mathsf{all}}$ | undec. |  undec. (Corollary 15) |  dec. (Winter, 2018, Theorem 25)
$T\in\textsc{Reg}_{\mathsf{FSL}}$ | undec. |  dec. (Winter, 2018, Theorem 10) | dec.
$T\in\textsc{Reg}_{\mathsf{FS}}$ | open | dec. | dec.
$\exists T\in\textsc{Reg}_{\mathsf{all}}$ | reduces to $T=(\Sigma\cup\Gamma)^{*}$
$\exists T\in\textsc{Reg}_{\mathsf{FSL}}$ | undec. (Corollary 13) | dec. (Theorem 8) | always
$\exists T\in\textsc{Reg}_{\mathsf{FS}}$ | dec. (Corollary 10) | dec. | always
Table 1: Overview of results for instances of the resynchronized
uniformization problem (upper and middle rows) and variants (lower rows). The
results are described in Section 3.1.

Table 1 provides an overview of known and new (un)decidability results for the
resynchronized uniformization problem for different types of source relations
and target synchronization relations. The entries for the new results contain
references to the corresponding statement in this paper, which are proved in
Section 3.2 and Section 3.3. Some entries contain a reference to the
literature. The results by Winter (2018) (see (Winter, 2018, Theorems 10 and
25)) use the same terminology as in this paper, so they do not need further
explanation. Some other results from the literature are not stated in terms of
synchronization languages, so we explain their connection to our setting
below, and we also briefly explain the table entries without a further
reference, which are either trivial or are direct consequences of other
entries in the table.

As classes for source relations we consider rational, automatic, and
recognizable relations, represented by the columns in the table. Formally,
these relations are specified by regular languages from the classes
$\textsc{Reg}_{\mathsf{all}}$, $\textsc{Reg}_{\mathsf{FSL}}$, and
$\textsc{Reg}_{\mathsf{FS}}$. But note that precise representations of the
source relations are not important because according to Theorem 4 we can
always assume that the source relation is encoded using the canonical
synchronizations for rational, automatic, and recognizable relations.

The rows of the table correspond to different variations concerning the target
synchronization language $T$ in the problem. The upper three rows show the
cases where $T$ is fixed to the canonical synchronizations for rational,
automatic, and recognizable relations, respectively.

The first row is about the problem whether a given relation has a
$(\Sigma\cup\Gamma)^{*}$-controlled subsequential uniformization, which is
equivalent to asking whether it has a uniformization by an arbitrary
subsequential transducer. This problem has been considered by Carayol and
Löding (2014): For rational source relations the problem is undecidable
(Carayol and Löding, 2014, Theorem 17) and for automatic source relations it
is decidable (Carayol and Löding, 2014, Theorem 18). The same authors have
also shown that it is decidable whether an automatic relation has a
uniformization by a recognizable relation, which corresponds to a
$\Sigma^{*}\Gamma^{*}$-controlled subsequential uniformization in our table
(third row, middle column), see (Carayol and Löding, 2014, Proposition 20).

The question whether an automatic relation has a uniformization by a
synchronous subsequential transducer (second row, middle column) is a
classical problem of reactive synthesis that has been studied intensively over
infinite words and was first solved by Büchi and Landweber (1969). The result
can easily be adapted from infinite to finite words.

Let us now look at first three rows and the rightmost column (recognizable
relations). First, we explain why a recognizable relation always has a
uniformization by a $\Sigma^{*}\Gamma^{*}$-controlled subsequential
transducer, and thus also a by $(\Sigma\cup\Gamma)^{*}$-controlled one. Recall
that a recognizable relation $R$ can be effectively represented as
$\bigcup_{i=0}^{n}U_{i}\times V_{i}$ where $U_{i}\subseteq\Sigma^{*}$ and
$V_{i}\subseteq\Gamma^{*}$ are regular languages for each $i$. Since regular
languages are closed under all Boolean operations, one can find such a
representation in which all the $U_{i}$ are pairwise disjoint. Now it suffices
to pick some $v_{i}\in V_{i}$ for each $i$, then the relation
$R_{f}=\bigcup_{i=0}^{n}U_{i}\times\\{v_{i}\\}$ is functional and uniformizes
$R$. Clearly, $R_{f}$ is realizable by a $\Sigma^{*}\Gamma^{*}$-controlled
subsequential transducer based on a product DFA for the $U_{i}$. Secondly, the
result that it is decidable whether a recognizable relation has a
uniformization by a synchronous subsequential transducer follows directly from
the fact that it is decidable whether an automatic relation has a
uniformization by a synchronous sequential transducer because every
recognizable relation is also automatic (in general, decidability results
propagate to the right in each row of the table).

As already mentioned, the first three rows deal with the fixed target
synchronization languages that are the canonical representatives for the
classes $\textsc{Reg}_{\mathsf{all}}$, $\textsc{Reg}_{\mathsf{FSL}}$,
$\textsc{Reg}_{\mathsf{FS}}$. The three rows in the middle are about the
problem where a regular target synchronization language from one of these
classes is given as input to the problem. The two undecidability results for
rational source relations in this part of the table directly follow for the
choices of $T=(\Sigma\cup\Gamma)^{*}$ resp.
$T=(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$ from the results in the upper
rows. The decidability results in this part of the table follow directly from
the decidability results by Winter (2018) since
$\textsc{Reg}_{\mathsf{FS}}\subseteq\textsc{Reg}_{\mathsf{FSL}}\subseteq\textsc{Reg}_{\mathsf{all}}$.
We conjecture that the case of rational source relations and target
synchronization languages of finite shift is decidable, but we were not able
to prove it, so this case is still open.

The last three rows consider the version of the problem where the target
synchronization language is not fixed or given, but we ask for the existence
of a uniformization by a subsequential transducer whose synchronization
language is in $\textsc{Reg}_{\mathsf{all}}$, $\textsc{Reg}_{\mathsf{FSL}}$,
resp. $\textsc{Reg}_{\mathsf{FS}}$. Clearly, for the class
$\textsc{Reg}_{\mathsf{all}}$ this reduces to the first row because both
problems do not impose any restriction on the synchronization language of the
subsequential transducer. Concerning recognizable source relations, we have
seen above that a recognizable relation always has
$\Sigma^{*}\Gamma^{*}$-controlled sequential uniformization, thus, every entry
is “always”. The decidability result for automatic source relations in the
last row is a direct consequence of the decidability result one column to the
left.

We now show the remainder of the results, first the decidability results in
Section 3.2, then the undecidability results in Section 3.3.

###  3.2 Decidability results

To begin with, we show the following:

######  Theorem 8.

It is decidable whether a given automatic relation has a uniformization by a
subsequential transducer with finite shiftlag.

###### Proof.

This is consequence of the proof that it is decidable whether an automatic
relation has a uniformization by a subsequential transducer presented by
Carayol and Löding (2014). It turns out that if an automatic relation has a
uniformization by a subsequential transducer, then the relation also has a
uniformization by a subsequential transducer with finite shiftlag. A bit more
formally, Carayol and Löding (2014) have reduced the problem to deciding the
existence of a winning strategy in a safety game. Such a winning strategy can
be translated into a
$(\Sigma^{k}\Gamma^{k})^{*}\Sigma^{*}\Gamma^{*}$-controlled subsequential
transducer for a computable $k$. In other words, as long as the needed
lookahead on the input to produce the next output is at most $k$, the
subsequential transducer for the uniformization alternates between reading
input words of length $k$ and producing output words of length $k$. Once the
transducer needs a lookahead of more than $k$, it can read the remainder of
the input and produce one final output word. The language
$(\Sigma^{k}\Gamma^{k})^{*}\Sigma^{*}\Gamma^{*}$ has finite shiftlag. ∎

Now we show that it is decidable whether a given rational relation has a
uniformization by a $\Sigma^{*}\Gamma^{*}$-controlled subsequential
transducer. The functions computed by $\Sigma^{*}\Gamma^{*}$-controlled
subsequential transducers are clearly recognizable relations, and conversely,
each functional recognizable relation can be computed by a
$\Sigma^{*}\Gamma^{*}$-controlled subsequential transducer (as already
explained in Section 3.1).

We prove that it is decidable whether a given rational relation has a
uniformization by a recognizable relation by a reduction from the boundedness
problem for distance automata. A distance automaton is a finite state
automaton that additionally maps transitions to distances of $0$, $1$, or
$\infty$. Then a run is associated with the sum of distances seen along the
run. Such an automaton is said to be bounded if there exists a bound such that
each accepted word has a run with a distance less or equal to this bound. We
define this formally.

A _finite state automaton with a distance function_ (_distance automaton_)
$\mathcal{A}$ is a tuple $(Q,\Sigma,q_{0},\Delta,F,d)$, where the first five
components are the same as for finite state automata, and
$d\colon\Delta\rightarrow\\{0,1,\infty\\}$ is a distance function that assigns
a value to each transition. The concepts of run, accepting run, and recognized
language are defined as for finite state automata. The _distance_ $d(\rho)$ of
a run $\rho=(p_{0},a_{1},p_{1})\dots(p_{n-1},a_{n},p_{n})$ of $\mathcal{A}$ on
$w=a_{1}\dots a_{n}$ is defined as $\sum_{i=1}^{n}d((p_{i-1},a_{i},p_{i}))$,
where for any integer $i$, $i<\infty$, and $i+\infty=\infty+i=\infty$. The
_distance_ $d(w)$ of a word $w$ is defined as $\infty$ if $w\notin
L(\mathcal{A})$ and otherwise as the minimal distance of an accepting run of
$\mathcal{A}$ on $w$, that is, $\mathrm{min}\\{d(\rho)\mid\rho\text{ is an
accepting run of $\mathcal{A}$ on $w$}\\}$. Let $D(\mathcal{A})$ denote the
supremum of distances associated with $L(\mathcal{A})$, that is, the supremum
of $\\{d(w)\mid w\in L(\mathcal{A})\\}$. A distance automaton $\mathcal{A}$ is
_bounded_ if $D(\mathcal{A})$ is finite. Hashiguchi has shown that the
boundedness problem for distance automata is decidable, see Hashiguchi (1982,
1990), see also Kirsten (2005).

Now that we have introduced distance automata, we are ready to prove the
result.

######  Theorem 9.

It is decidable whether a given rational relation has a uniformization by a
recognizable relation.

###### Proof.

We give a reduction to the boundedness problem for distance automata.

Let $R\subseteq\Sigma^{*}\times\Gamma^{*}$ be a rational relation given by an
NFA $\mathcal{A}$ over $\Sigma\cup\Gamma$ that defines $R$, that is,
$\llbracket L(\mathcal{A})\rrbracket=R$. Our goal is to construct a distance
automaton $\mathcal{B}$ such that such that
$\mathrm{dom}(\mathcal{B})=\mathrm{dom}(R)$ and $D(\mathcal{B})$ is bounded
iff $R$ has a uniformization by a recognizable relation.

Note that a uniformization of $R$ by a recognizable relation only produces
finitely many different possible output words. Hence, there is a bound on the
length on these output words. And vice versa, if there is a bound $n$ such
that for each word $u$ in the domain of $R$ there is an output word $v$ such
that $|v|\leq n$ and $(u,v)\in R$, then the relation assigning to each input
the smallest output in length-lexicographic order is a recognizable
uniformization of $R$.

So we use the reduction to boundedness of distance automata to check such a
bound on the length of shortest output words for each input exists. The idea
behind the construction is to replace transitions labeled with output symbols
with transitions that increase the distance value of a run. Formally, we take
all input transitions of $\mathcal{A}$ with distance value $0$, and insert
transitions with distance value $1$ that correspond to runs consuming one
input symbol and a non-empty sequence of output symbols, as described below.

Let
$\mathcal{B}=(Q_{\mathcal{A}},\Sigma,q_{0}^{\mathcal{A}},\Delta,F_{\mathcal{A}},d)$
be a distance automaton, where $\Delta$ and $d$ are defined such that

$(p,a,q)\in\Delta\text{ and }d((p,a,q))=0\text{ iff }\mathcal{A}\colon
p\xrightarrow{a}q\text{ and}$ $(p,a,q)\in\Delta\text{ and }d((p,a,q))=1\text{
iff }\mathcal{A}\colon p\xrightarrow{a}q^{\prime}\xrightarrow{w}q\text{ for
}q^{\prime}\in Q_{\mathcal{A}},w\in\Gamma^{+},\text{ and not
}\mathcal{A}\colon p\xrightarrow{a}q.$

It is easy to see that $L(\mathcal{B})=\mathrm{dom}(R)$. We show that $R$ has
a uniformization by a recognizable relation iff $D(\mathcal{B})$ is bounded.

Assume $R$ is uniformized by a recognizable relation
$\bigcup_{i=1}^{n}U_{i}\times\\{v_{i}\\}$. Let $\ell$ be the length of the
longest $v_{i}$. Then, for each $u\in\mathrm{dom}(R)$ there exists a
$v\in\Gamma^{\leq\ell}$ such that there is synchronization $w$ of $(u,v)$ that
is accepted by $\mathcal{A}$. A run of $\mathcal{A}$ on $w$ can be easily
translated into a run of $\mathcal{B}$ on $u$. It directly follows that $d(u)$
is at most $\ell$. Thus, $d(\mathcal{B})$ is bounded.

Assume $d(\mathcal{B})$ is bounded by $n$. Thus, for each
$u\in\mathrm{dom}(R)$ we can pick a $v\in\Gamma^{*}$ of length at most
$|\Delta|\cdot n$ such that there exists a synchronization $w$ of $(u,v)$ that
is accepted by $\mathcal{A}$. The factor $|\Delta|$ was introduced because a
number of consecutive transitions with output labels that occur in
$\mathcal{A}$ increase the distance of a corresponding run in $\mathcal{B}$
only by one. Since there are only finitely many words of a fixed length it
follows directly that $R$ can be uniformized by recognizable relation.

From the decidability of the boundedness problem for distance automata we
obtain decidability of the problem whether a rational relation is
uniformizable by a recognizable relation. ∎

Turning to the question whether a rational relation has a subsequential
uniformization inside the class of languages with finite shift, we obtain the
following.

######  Corollary 10.

It is decidable whether a given rational relation has a uniformization by a
subsequential transducer with finite shift.

###### Proof.

We show that if a rational relation is uniformizable by a subsequential
transducer whose synchronization language has finite shift, then it is
uniformizable by a recognizable relation which is decidable by Theorem 9.

Given a rational relation $R$ and a subsequential transducer $\mathcal{T}$
that uniformizes $R$ such that $S(\mathcal{T})\in\textsc{Reg}_{\mathsf{FS}}$.
Recall that $\Sigma^{*}\Gamma^{*}$ is an effective canonical representation of
$\textsc{Reg}_{\mathsf{FS}}$. Clearly, the $\Sigma^{*}\Gamma^{*}$-controlled
representation of $S(\mathcal{T})$ describes a functional recognizable
relation, and as explained earlier, functional recognizable relation can be
computed by $\Sigma^{*}\Gamma^{*}$-controlled subsequential transducers. ∎

###  3.3 Undecidability results

First, we introduce a technical result by Carayol and Löding (2014) of which
Corollaries 12 and 13 are easy consequences. There, it is shown that is
undecidable whether a given rational relation has a uniformization by a
subsequential transducer by showing the following stronger statement.

######  Lemma 11 (Carayol and Löding (2014)).

There exists a rational relation $R_{M}$, constructed from a Turing machine
$M$, such that $R_{M}$ has a uniformization by the identity function if $M$
does not halt for the empty input, and $R_{M}$ has no uniformization by any
subsequential transducer if $M$ halts for the empty input.

Clearly, the identity function can be realized by a
$(\Sigma\Gamma)^{*}$-controlled subsequential transducer. Since
$(\Sigma\Gamma)^{*}\subseteq(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})\in\textsc{Reg}_{\mathsf{FSL}}$,
it is now easy to see that

######  Corollary 12.

It is undecidable whether a given rational relation has a uniformization by a
synchronous subsequential transducer, that is, a
$(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$-controlled subsequential
transducer.

######  Corollary 13.

It is undecidable whether a given rational relation has a uniformization by a
subsequential transducer with finite shiftlag.

In the remainder of this section, we show that for a given automatic relation
and a given regular synchronization language it is undecidable whether the
relation has a subsequential uniformization according to the synchronization
language.

First, we show a stronger result. Recall that a regular synchronization
language $S\subseteq(\Sigma\cup\Gamma)^{*}$ is a fine-grained way to describe
the possible behavior of a transducer. A little less fine-grained is a so-
called regular _control language_ , that is a regular language
$L\subseteq\\{1,2\\}$. Such a language describes how a transducer may process
input and output symbols, but does not specify which input and output symbols
occur, e.g., $12211$ means that a transducer reads one input symbol,
subsequently produces two output symbols, and then reads two input symbols.
This notion of control language is the one used by Figueira and Libkin (2015).
Each control language $L$ naturally corresponds to a synchronization language
by substituting $1$ with $\Sigma$ and $2$ with $\Gamma$, and to each
synchronization language we can associate the control language obtained by the
projection that replaces symbols from $\Sigma$ with $1$, and symbols from
$\Gamma$ with $2$. So the definitions and notations introduced in Section 2
regarding synchronization languages can be applied in a natural way to control
languages (in fact, these notions have originally been defined for control
languages by Figueira and Libkin (2015)).

We show that for a given automatic relation and a given control language it is
undecidable whether the relation has uniformization according to the control
language.

######  Theorem 14.

It is undecidable whether a given automatic relation has a uniformization by
an $L$-controlled subsequential transducer for a given regular control
language $L\subseteq\\{1,2\\}^{*}$.

###### Proof.

We give a reduction from the halting problem for Turing machines (TMs). Given
a TM $M$ with a right-infinite tape, our goal is to describe an automatic
relation $R_{M}$ and a regular control language $L_{M}$ such that $R_{M}$ can
only be uniformized by an $L_{M}$-controlled subsequential transducer if $M$
does not halt for the empty input.

Let $Q_{M}$ denote the state set of $M$, $q_{0}^{M}$ denotes the initial state
of $M$, $\Gamma_{M}$ denotes the tape alphabet of $M$ including the blank
symbol $\underbracket{\hskip 4.30554pt}$, $\delta_{M}$ denotes the transition
function of $M$, and $\vdash$ denotes the tape delimiter. We represent a
configuration $c$ of $M$ in the usual way as $\vdash\\!a_{1}\cdots
a_{k}qb_{1}\cdots b_{k}$, where
$a_{1},\dots,a_{k},b_{1},\dots,b_{\ell}\in\Gamma_{M}$, $a_{1}\cdots
a_{k}b_{1}\cdots b_{\ell}$ is the content of the tape of $M$, $q\in Q_{M}$ is
the current control state of $M$, and the head of $M$ is on $b_{1}$. We assume
that a configuration is represented without additional blanks, meaning a
configuration representation does not start nor end with a blank. Let
$\mathcal{C}^{M}$ denote the set of all configurations of $M$. For a
configuration $c\in\mathcal{C}^{M}$ let $\mathit{succ}(c)$ denote its
successor configuration. Without loss of generality, we assume that
$\mathit{succ}(c)$ is at least as long as $c$, we call this non-erasing. Every
TM can be made non-erasing by introducing a new tape symbol $B$ that is
written instead of $\underbracket{\hskip 4.30554pt}$ and the TM behaves on $B$
the same as on $\underbracket{\hskip 4.30554pt}$. Furthermore, we call a
configuration $c\in\mathcal{C}^{M}$ whose last letter is some $q\in Q_{M}$ and
there is a transition of the form
$\delta_{M}(q,\mbox{\raisebox{2.79857pt}{$\underbracket{\hskip
4.30554pt}$}})=(q^{\prime},a,R)$ extending configuration, because
$|\mathit{succ}(c)|=|c|+1$. We denote by $\mathcal{C}^{M}_{E}$ the set of
extending configurations.

Let
$\Sigma=Q_{M}\mathop{\vphantom{\cup}\mathchoice{\ooalign{\hfil$\displaystyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}{\ooalign{\hfil$\textstyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}{\ooalign{\hfil$\scriptstyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}{\ooalign{\hfil$\scriptscriptstyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}}\displaylimits\Gamma_{M}\mathop{\vphantom{\cup}\mathchoice{\ooalign{\hfil$\displaystyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}{\ooalign{\hfil$\textstyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}{\ooalign{\hfil$\scriptstyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}{\ooalign{\hfil$\scriptscriptstyle\cup$\hfil\cr\hfil$\cdot$\hfil\crcr}}}\displaylimits\\{\$,\\#\\}$.
We define an automatic relation $R_{M}\subseteq\Sigma^{*}\times\Sigma^{*}$
whose domain consists of words of the form $\$c_{1}\$\cdots\$c_{m}\\#$ where
$c_{1},\dots,c_{m-1}$ are configurations of $M$ and $c_{m}$ is a (prefix of a)
configuration of $M$. The idea is that we want to force a uniformizer to
produce an output sequence that begins with
$\$\vdash\\!q_{0}^{M}\$\mathit{succ}(c_{1})\$\dots\$\mathit{succ}(c_{m-1})$
for such an input. The control language is defined in such a way that this is
indeed possible (the subsequential transducer can produce
$\mathit{succ}(c_{i})$ while reading $c_{i}$). And this should define a
uniformization iff there is no halting computation of $M$ for the empty input.
That is, we have to define $R_{M}$ in such a way that the pair $(u,v)\in
R_{M}$, where $u=\$c_{1}\$\cdots\$c_{m}\\#$ and $v$ starts with
$\$\vdash\\!q_{0}^{M}\$\mathit{succ}(c_{1})\$\cdots\$\mathit{succ}(c_{m-1})$
iff $c_{1}\$\dots\$c_{m}$ is not a halting computation of $M$.

We describe a function $f^{M}_{\mathit{succ}}$ defined over all four-letter
infixes of words from the domain of $R_{M}$ which defines how a subsequential
transducer should build successor configurations. First, given a configuration
$c\in\mathcal{C}^{M}$, note that in order to output
$\mathit{succ}(c)[1]\dots\mathit{succ}(c)[j]$, it suffices to have read
$c[1]\cdots c[j+2]$. Furthermore, in order to determine the letter
$\mathit{succ}(c)[j]$, it suffices to remember $c[j-1]c[j]c[j+1]c[j+2]$. For
example, consider the configuration $c$ of the form $a_{1}a_{2}qb_{1}b_{2}$
and the transition $\delta_{M}(q,b_{1})=(q^{\prime},c,L)$, then the successor
configuration $\mathit{succ}(c)$ is $a_{1}q^{\prime}a_{2}cb_{2}$. To determine
$\mathit{succ}(c)[2]$, $c[3]c[4]$ is needed. To determine
$\mathit{succ}(c)[3]$, $c[2]$ is needed, because the applied transition moves
the head to the left.

The function $f^{M}_{\mathit{succ}}$ extends this idea to infixes from words
of the domain of $R_{M}$. Formally, the type of the partial function
$f^{M}_{\mathit{succ}}$ is
$\Sigma\Sigma\Sigma\Sigma\to\Sigma\cup\Sigma\Sigma$. We omit a formal
definition of the mapping, instead, we provide some examples:

  * •

$a_{1}a_{2}qb_{1}$ maps to $q^{\prime}$ if
$\delta_{M}(q,b_{1})=(q^{\prime},c,L)$

  * •

$a_{2}qb_{1}b_{2}$ maps to $c$ if $\delta_{M}(q,b_{1})=(q^{\prime},c,L)$

  * •

$b_{2}b_{3}\$a_{1}$ maps to $b_{3}$  _configuration suffix is connected via
$\$$ with configuration prefix_

  * •

$b_{3}\$a_{1}q$ maps to $\$$

  * •

$a_{1}a_{2}q\$$ maps to $a_{2}c$ if
$\delta_{M}(q,\mbox{\raisebox{2.79857pt}{$\underbracket{\hskip
4.30554pt}$}})=(q^{\prime},c,R)$  _suffix of an extending configuration and
$\$$ is seen, this is the only case the function has a two-letter target_

  * •

$a_{2}q\$a_{1}$ maps to $q^{\prime}$ if
$\delta_{M}(q,\mbox{\raisebox{2.79857pt}{$\underbracket{\hskip
4.30554pt}$}})=(q^{\prime},c,R)$

To ensure that $f^{M}_{\mathit{succ}}$ is totally defined, we define
$\mathit{succ}(c)=c$ for halting configurations $c$.

We design the relation $R_{M}$ and the control language $L_{M}$ such that a
potential uniformizer is forced to behave according to
$f^{M}_{\mathit{succ}}$. To ensure this, we introduce two constraints
(formally below). The output must end according to $f^{M}_{\mathit{succ}}$
applied to the suffix of the input, and we have to enforce that the potential
uniformizer produces two letters only if the delimiter $\$$ after an extending
configuration is seen. The latter condition can not directly be enforced by
$R_{M}$ nor $L_{M}$, but in $R_{M}$ it suffices to compare the length of the
last configuration in the input and the last configuration of the output
modulo two to detect deviations (explained in the correctness proof).

Before we define the relation, we introduce one shorthand notation. Given
$w\in\Sigma^{*}$, let $\mathit{last}_{i}(w)$ denote the letter $w[|w|-i]$ for
$i\in\mathbbm{N}$, that is, the $i$th to last letter of $w$, and let
$\mathit{last}_{i:j}(w)$ denote $w[|w|-i]\cdots w[|w|-j]$ for
$i,j\in\mathbbm{N}$ with $i\geq j$.

Formally, the relation $R_{M}\subseteq\Sigma^{*}\times\Sigma^{*}$ contains a
pair $(u,v)$ iff

  1. 1.

$u=\$c_{1}\$\dots\$c_{m}\\#$, where $c_{1},\dots,c_{m-1}\in\mathcal{C}^{M}$,
$c_{m}\in\mathrm{Prefs}(\mathcal{C}^{M})$, $m>1$,

  2. 2.

$v=\$c^{\prime}_{1}\$\dots\$c^{\prime}_{\ell}\\#$, where
$c^{\prime}_{1},\dots,c^{\prime}_{\ell-1}\in\mathcal{C}^{M}$,
$c_{\ell}\in\mathrm{Prefs}(\mathcal{C}^{M})$, $\ell>1$,

  3. 3.

$c^{\prime}_{1}:=\ \vdash\\!q_{0}^{M}$ is the initial configuration of $M$ on
the empty tape,

  4. 4.

$c_{1}\$\dots\$c_{m-1}\neq c^{\prime}_{1}\$\dots\$c^{\prime}_{\ell-2}$ or
$c^{\prime}_{\ell-1}$ is not a halting configuration of $M$,

  5. 5.

$f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))=\begin{cases}\mathit{last}_{1}(v)&\text{if
}f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))\in\Sigma\\\
\mathit{last}_{2:1}(v)&\text{if
}f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))\in\Sigma\Sigma,\end{cases}$

_Items 6 and 7 are designed under the assumption that if $|c_{m}|\leq 1$, then
a uniformizer has not finished to produce $\mathit{succ(c_{m-1})}$. If
$|c_{m}|=2$, then $\$$ – the delimiter after $\mathit{succ(c_{m-1})}$ – is
produced, and if $|c_{m}|\geq 3$, then the production of
$\mathit{succ(c_{m})}$ has started._

  1. 6.

     * •

if $|c_{m}|>3$, then $|c^{\prime}_{\ell}|>1$,  _$c^{\prime}_{\ell}$ refers to
a prefix of $\mathit{succ(c_{m})}$ of length at least $2$_

     * •

if $|c_{m}|=3$, then $|c^{\prime}_{\ell}|=1$,  _$c^{\prime}_{\ell}$ refers to
the first letter of $\mathit{succ(c_{m})}$_

     * •

if $|c_{m}|=2$, then $|c^{\prime}_{\ell}|=0$,  _delimiter $\$$ after
$\mathit{succ(c_{m-1})}$ is produced, thus, $c^{\prime}_{\ell}=\varepsilon$_

     * •

if $|c_{m}|\leq 1$, then $|c^{\prime}_{\ell}|>1$,  _$c^{\prime}_{\ell}$ refers
to $\mathit{succ(c_{m-1})}$ which has length at least $2$_

  2. 7.

     * •

if $|c_{m}|\geq 3$, then $(|c_{m}|-|c^{\prime}_{\ell}|)\\!\mod{2}=0$,

     * •

if $|c_{m}|=2$, then
$(|c_{m-1}|-|c^{\prime}_{\ell-1}|)\\!\mod{2}=\begin{cases}1&\text{if
}c_{m-1}\in\mathcal{C}^{M}_{E}\\\ 0&\text{otherwise},\end{cases}$

     * •

if $|c_{m}|\leq 1$, then
$(|c_{m-1}|-|c^{\prime}_{\ell}|)\\!\mod{2}=\begin{cases}1&\text{if
}c_{m-1}\in\mathcal{C}^{M}_{E}\\\ 0&\text{otherwise}.\end{cases}$

In combination with the control language $L_{M}$ defined below, Items 5, 6 and
7 ensure that an $L_{M}$-controlled subsequential uniformizer of $R_{M}$ has
to output $\mathit{succ}(c_{i})$ while reading $c_{i}$ according to
$f^{M}_{\mathit{succ}}$ (as will be explained later). It is not hard to see
that $R_{M}$ is an automatic relation. For Item 7 note that
$(x-y)\mod{2}=\mathit{sign}((x\\!\mod{2})-(y\\!\mod{2}))$. Replacing Items 5,
6 and 7 by $c^{\prime}_{i+1}=\mathit{succ}(c_{i})$ would make the relation
non-automatic, in general.

The control language $L_{M}$ is defined by the regular expression
$1222211(1(2+22))^{*}12$, we explain its use further below.

We claim that $R_{M}$ can be uniformized by an $L_{M}$-controlled
subsequential transducer iff $M$ does not halt on the empty tape.

If $M$ does not halt, then an $L_{M}$-controlled subsequential transducer that
produces

$\$\underbrace{\vdash\\!q_{0}^{M}}_{c_{1}^{\prime}}\$f^{M}_{\mathit{succ}}(u[1:4])f^{M}_{\mathit{succ}}(u[2:5])\cdots
f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))\\#$

for input $u$ of the form $\$c_{1}\$\dots\$c_{m}\\#$ uniformizes $R_{M}$:
First, note that this output guarantees that
$c^{\prime}_{i+1}=\mathit{succ}(c_{i})$ for all $i\leq m-1$, and
$c_{\ell-1}=\mathit{succ}(c_{m-1})$. We show that the conditions of $R_{M}$
are satisfied: We begin with Items 5, 6 and 7.

Clearly, $f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))$ has the correct
value.

The next statements are easy consequences of the definition of
$f^{M}_{\mathit{succ}}$: If $|c_{m}|\leq 1$, then the delimiter $\$$ after
$\mathit{succ}(c_{m-1})$ is not included in the output, and
$c^{\prime}_{\ell}$ refers to $\mathit{succ}(c_{m-1})$. Every configuration
has length at least 2, thus, $|c^{\prime}_{\ell}|\geq 2$. If $|c_{m}|=2$, then
the output ends with $\$\\#$, i.e., $c^{\prime}_{\ell}=\varepsilon$. If
$|c_{m}|=3$, then $|c^{\prime}_{\ell}|=1$ and $c^{\prime}_{\ell}$ is the first
letter of $\mathit{succ}(c_{m})$. Lastly, if $|c_{m}|>3$, then
$|c^{\prime}_{\ell}|>1$ and $c^{\prime}_{\ell}$ is a prefix of
$\mathit{succ}(c_{m})$. Hence, it is easy to see that all length constraints
regarding $c^{\prime}_{\ell}$ are satisfied.

We turn to the modulo constraints. After $c_{m-1}$, $\$$ follows, thus,
$f^{M}_{\mathit{succ}}$ at the end of $c_{m-1}\$$ yields two letters iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$. Hence, $\mathit{succ}(c_{m-1})$ is one letter
longer than $c_{m-1}$ iff $c_{m-1}\in\mathcal{C}^{M}_{E}$. We have explained
in the above paragraph that if $|c_{m}|\leq 1$, then $c^{\prime}_{\ell}$
refers to $\mathit{succ}(c_{m-1})$ and if $|c_{m}|=2$, then
$c^{\prime}_{\ell-1}$ refers to $\mathit{succ}(c_{m-1})$. Thus, the condition
if $|c_{m}|\leq 1$, then $(|c_{m-1}|-|c^{\prime}_{\ell}|)\\!\mod{2}=1$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$ is satisfied. Also, the condition if
$|c_{m}|=2$, then $(|c_{m-1}|-|c^{\prime}_{\ell-1}|)\\!\mod{2}=1$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$ is satisfied. After $c_{m}$, no $\$$ follows,
thus $f^{M}_{\mathit{succ}}$ applied to shifting four-letter windows of
$c_{m}$ (with three letters known of $c_{m}$ when the first letter of
$c^{\prime}_{\ell}$ is produced) yields that $|c_{m}|$ and
$|c^{\prime}_{\ell}|$ are either both even or both odd. Thus, the condition if
$|c_{m}|\geq 3$, then $(|c_{m}|-|c^{\prime}_{\ell}|)\\!\mod{2}=0$ is
satisfied.

We turn to Items 1, 2, 3 and 4. If $c_{1}$ is not equal to the initial
configuration $q_{0}^{M}$, then clearly $c_{1}\$\dots\$c_{m-1}\neq
c^{\prime}_{1}\$\dots\$c^{\prime}_{\ell-2}$. Thus, assume $c_{1}$ is the
initial configuration. Then either there exists an $i\leq m-1$ such that
$\mathit{succ}(c_{i})\neq c_{i+1}$ or if no such $i$ exists then
$\mathit{succ}(c_{i})$ cannot be a halting configuration for all $i$ because
$M$ does not halt. In the former case we have that
$c_{i+1}\neq\mathit{succ}(c_{i})=c^{\prime}_{i+1}$ which implies
$c_{1}\$\dots\$c_{m-1}\neq c^{\prime}_{1}\$\dots\$c^{\prime}_{\ell-2}$. In the
latter case we have that $c^{\prime}_{\ell-1}=\mathit{succ}(c_{m-1})$ is not a
halting configuration.

We argue that it is possible for a subsequential transducer to realize

$\$\vdash\\!q_{0}^{M}\$f^{M}_{\mathit{succ}}(u[1:4])f^{M}_{\mathit{succ}}(u[2:5])\cdots
f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))\\#$

in an $L_{M}$-controlled fashion. The idea is that the transducer, after
producing $\$c_{1}^{\prime}\$:=\$\vdash\\!q_{0}^{M}\$$, behaves according to
$f^{M}_{\mathit{succ}}$ shifting the considered four-letter window letter-by-
letter. Let us break down the intended use of $L_{M}$:

$\underbrace{12222}_{\begin{subarray}{c}\text{read first $\$$ and}\\\
\text{output
$\$\vdash\\!q_{0}^{M}\$$}\end{subarray}}\overbrace{11}^{\begin{subarray}{c}\text{lookahead
for computing}\\\ \text{succ.\ config.\
correctly}\end{subarray}}\underbrace{(1(2+22))^{*}}_{\begin{subarray}{c}\text{produce
succ.\ config.\ with $(12)^{*}$}\\\ \text{use $122$ at \$ if tape}\\\
\text{content becomes longer}\end{subarray}}\overbrace{1}^{\text{final
}\\#}\phantom{\quad}\underbrace{2}_{\text{final }\\#}$

With this in mind it is easy to see that it is possible to realize the desired
sequence in an $L_{M}$-controlled fashion such that all conditions of $R_{M}$
are satisfied.

Now assume that $M$ does halt for the empty input, and let
$c_{1},\ldots,c_{m}$ be the sequence of configurations corresponding to a
halting computation. Clearly, an $L_{M}$-controlled subsequential transducer
that produces for the input $u$ of the form $\$c_{1}\$\cdots\$c_{m}\\#$ the
output

$\$\vdash\\!q_{0}^{M}\$f^{M}_{\mathit{succ}}(u[1:4])f^{M}_{\mathit{succ}}(u[2:5])\cdots
f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))\\#$

is not a uniformizer:
$c_{1}\$\cdots\$c_{m-1}=c^{\prime}_{1}\$\cdots\$c^{\prime}_{\ell-2}$, and
$c_{\ell-1}$ is a halting configuration of $M$.

We now show that any $L_{M}$-controlled subsequential uniformizer of $R_{M}$
behaves according to $f^{M}_{\mathit{succ}}$ (after producing
$\$c_{1}^{\prime}\$:=\$\vdash\\!q_{0}^{M}\$$) which implies that if $R_{M}$ is
uniformizable by an $L_{M}$-controlled subsequential transducer then $M$ does
not halt on the empty input. Assume such a uniformizer has so far behaved
according to $f^{M}_{\mathit{succ}}$, and now produces something different.
Let $u^{\prime}$ denote the current input sequence. We distinguish two cases.

First, assume that the uniformizer in its last computation step has produced
output $o$ such that $o\neq
f^{M}_{\mathit{succ}}(\mathit{last}_{3:0}(u^{\prime}))$, but
$|o|=|f^{M}_{\mathit{succ}}(\mathit{last}_{3:0}(u^{\prime}))|$. Then, the next
and last input symbol is $\\#$. The whole input sequence is $u=u^{\prime}\\#$.
Clearly, the condition $f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))$ of
$R_{M}$ is violated.

Secondly, assume that the uniformizer in its last computation step has
produced output $o$ such that
$|o|\neq|f^{M}_{\mathit{succ}}(\mathit{last}_{3:0}(u^{\prime}))|$. As in the
previous case, the next and last input symbol is $\\#$. The whole input
sequence is $u=u^{\prime}\\#$. The uniformizer must make one last single-
letter output to be $L_{M}$-controlled, this output must be $\\#$, otherwise
the output is clearly not according to $R_{M}$.

To start, we assume that $\mathit{last}_{1}(u)=\$$. Then $c_{m}=\varepsilon$.
Furthermore, $|f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))|=2$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$. The relation $R_{M}$ requires that
$|c^{\prime}_{\ell}|>1$ if $|c_{m}|<1$, hence, the output $o$ of the
uniformizer does not contain $\$$. Since $o$ was the first output not
according to $f^{M}_{\mathit{succ}}$, we obtain that
$|c_{m-1}|-|c^{\prime}_{\ell}|$ is even iff $c_{m-1}\in\mathcal{C}^{M}_{E}$.
This violates the constraint if $|c_{m}|\leq 3$, then
$(|c_{m-1}|-|c^{\prime}_{\ell}|)\\!\mod{2}=1$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$.

We now assume that $\mathit{last}_{1}(u)\neq\$$. Then
$|f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))|=1$, and $|o|=2$, because
$L_{M}$ ensures that an output is either one or two letters. Depending on the
length of $c_{m}$, different conditions of $R_{M}$ must be satisfied.

Assume that $|c_{m}|>3$, then $o$ can not include $\$$, because that would
start a new configuration prefix $c^{\prime}_{\ell}$ which violates the length
constraints of $c^{\prime}_{\ell}$. Thus, since $|o|=2$, we obtain that
$c_{m}$ is even iff $c^{\prime}_{\ell}$ is odd, which violates that
$(|c_{m}|-|c^{\prime}_{\ell}|)\\!\mod{2}=0$ if $|c_{m}|\geq 3$.

Assume that $|c_{m}|=3$. This implies that the output produced before $o$ was
$\$$, otherwise the subsequential transducer would have not behaved according
to $f^{M}_{\mathit{succ}}$ in the computation step before $o$. Hence, $o$ can
not be of the form $\$\$$ or begin with $\$$, because $\$\$$ is not part of a
valid output according to $R_{M}$. If $o$ ends with $\$$, then
$|c^{\prime}_{\ell}|=0$ which violates the length constraint. Thus, $o$
contains no $\$$, meaning that $|c^{\prime}_{\ell}|=2$ which violates the
length constraint.

Assume that $|c_{m}|=2$. The uniformizer must ensure that
$|c^{\prime}_{\ell}|=0$, the only way to achieve this with an output of length
two is either $\$\$$ or $o$ ends with $\$$ (and begins with some other
letter). However, $\$\$$ is not part of a valid output sequence. In the other
case, since all previous outputs were according to $f^{M}_{\mathit{succ}}$, we
obtain that $(|c_{m-1}|-|c^{\prime}_{\ell-1}|)\\!\mod{2}=0$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$, which violates that
$(|c_{m-1}|-|c^{\prime}_{\ell-1}|)\\!\mod{2}=1$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$.

Assume that $|c_{m}|\leq 1$. The uniformizer must ensure that
$|c^{\prime}_{\ell}|>1$, thus, $o$ can not contain $\$$. Thus, since $|o|=2$
and all previous outputs were according to $f^{M}_{\mathit{succ}}$, we obtain
that $(|c_{m-1}|-|c^{\prime}_{\ell}|)\\!\mod{2}=0$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$, which violates that
$(|c_{m-1}|-|c^{\prime}_{\ell}|)\\!\mod{2}=1$ iff
$c_{m-1}\in\mathcal{C}^{M}_{E}$.

We have proven that every $L_{M}$-controlled uniformizer of $R_{M}$ behaves
according to $f^{M}_{\mathit{succ}}$ after the output
$\$\vdash\\!q_{0}^{M}\$$. Together with $(u,v)\in R_{M}$ iff $M$ halts on the
empty input, where

$u=\$c_{1}\$\cdots\$c_{m}\\#\in\mathrm{dom}(R_{M}),\text{ and}$
$v=\$\vdash\\!q_{0}^{M}\$f^{M}_{\mathit{succ}}(u[1:4])f^{M}_{\mathit{succ}}(u[2:5])\cdots
f^{M}_{\mathit{succ}}(\mathit{last}_{4:1}(u))\\#$

we obtain that $R_{M}$ is uniformizable by an $L_{M}$-controlled subsequential
transducer iff $M$ halts on the empty input. ∎

We have seen that the problem whether an automatic relation has a uniformizer
that behaves according to a given control language is undecidable, thus, it is
also undecidable if we specify a synchronization language.

######  Corollary 15.

It is undecidable whether a given automatic relation has a uniformization by
an $S$-controlled subsequential transducer for a given regular synchronization
language $S\subseteq(\Sigma\cup\Gamma)^{*}$.

###### Proof.

Consider the automatic relation $R_{M}$, based on a Turing machine $M$, and
$L_{M}\subseteq\\{1,2\\}^{*}$ as in the proof of Theorem 14. Let
$S=\\{w\in(\Sigma\cup\Gamma)^{*}\mid w\text{ is $L_{M}$-controlled}\\}$. It
follows directly that it is undecidable whether $R_{M}$ has an $S$-controlled
uniformization. ∎

##  4 Definability problems

In the previous section we considered uniformization problems in the context
of synchronization languages. We now turn to the definability problem, so the
question whether a given relation can be defined inside a given target
language of synchronizations.

More formally, we are interested in the following problem.

######  Definition 16 (Resynchronized definability problem).

The _resynchronized definability problem_ asks, given a regular source
language $S\subseteq(\Sigma\cup\Gamma)^{*}$ and a regular target language
$T\subseteq(\Sigma\cup\Gamma)^{*}$, whether $\llbracket
S\rrbracket\in\textsc{Rel}(T)$.

We say that $T^{\prime}\subseteq T$ is a definition of $\llbracket
S\rrbracket$ in $T$ if $T^{\prime}$ is regular and $\llbracket
S\rrbracket=\llbracket T^{\prime}\rrbracket$, so if $T^{\prime}$ is a witness
for $\llbracket S\rrbracket\in\textsc{Rel}(T)$.

We assume all source and target languages to be regular without explicitly
mentioning it in the remainder.

We start by giving an example.

######  Example 17.

Let $\Sigma=\\{a\\}$ and $\Gamma=\\{b\\}$. Consider

$S=(ab)^{*}+(ab)^{*}(aa^{+}+bb^{+}),\text{ and}$
$T=a^{*}b^{*}+\underbrace{(ab)^{*}(aa^{+}+bb^{+})}_{U}.$

The relation $\llbracket S\rrbracket$ contains pairs of words where the words
have the same length, or the difference between the length of the words is at
least two. The target synchronization language contains all pairs of words
with difference at least two in the synchronous encoding (denoted by the set
$U$). The difference with $S$ is that the pairs of words of same length are
contained in $T$ in the completely asynchronous encoding $a^{*}b^{*}$.
Clearly, this set of words $a^{n}b^{n}$ for all $n$ is not a regular subset of
$a^{*}b^{*}$. However, in order to define $\llbracket S\rrbracket$ in $T$, we
can also select a larger subset of $a^{*}b^{*}$ that also contains pairs of
words that are already covered by $U$. We illustrate below that this is indeed
possible, that is, $\llbracket S\rrbracket\in\textsc{Rel}(T)$. We define the
set

$T^{\prime}=\underbrace{\\{uv\in a^{*}b^{*}\mid u\in a^{*},v\in
b^{*},(|u|-|v|)\ \mathrm{mod}\ 2=0\\}}_{M\subseteq a^{*}b^{*}}\ \cup\ U.$

Clearly, $T^{\prime}$ is regular and $T^{\prime}\subseteq T$. The relation
$\llbracket M\rrbracket$ captures all pairs of words where the difference
between the length of the words is even which implies that
$\llbracket(ab)^{*}\rrbracket\subseteq\llbracket M\rrbracket$. Note that
$\llbracket M\rrbracket\cap\llbracket U\rrbracket$ contains pairs of words
where the difference between the length of the words is at least two and even.
Moreover, $(\llbracket
M\rrbracket\setminus\llbracket(ab)^{*}\rrbracket)\subseteq\llbracket
U\rrbracket$. Consequently, $\llbracket T^{\prime}\rrbracket=\llbracket
S\rrbracket$.

###  4.1 Overview and simple results

target source |  rational $S\in\textsc{Reg}_{\mathsf{all}}$ |  automatic $S\in\textsc{Reg}_{\mathsf{FSL}}$ |  recognizable $S\in\textsc{Reg}_{\mathsf{FS}}$
---|---|---|---
unrestricted $T=(\Sigma\cup\Gamma)^{*}\in\textsc{Reg}_{\mathsf{all}}$ | always | always | always
synchronous $T\\!=\\!(\Sigma\Gamma)^{*}(\Sigma^{*}\\!+\\!\Gamma^{*})\\!\in\\!\textsc{Reg}_{\mathsf{FSL}}$ |  undec. Frougny and Sakarovitch (1993) | always | always
input before output $T=\Sigma^{*}\Gamma^{*}\in\textsc{Reg}_{\mathsf{FS}}$ |  undec. Berstel (1979) | dec. Carton et al. (2006) | always
$T\in\textsc{Reg}_{\mathsf{all}}$ |  undec. (Proposition 18) |  undec. (Proposition 18) |  undec. (Proposition 18)
$T\in\textsc{Reg}_{\mathsf{FSL}}$ | undec. |  open (dec. if target is unambiguous (Theorem 41)) |  dec. (Proposition 20) ($\llbracket S\rrbracket\in\textsc{Rel}(T)$ iff $\llbracket S\rrbracket\subseteq\llbracket T\rrbracket$)
$T\in\textsc{Reg}_{\mathsf{FS}}$ | undec. |  dec. (Proposition 21) |  dec. (Proposition 20) ($\llbracket S\rrbracket\in\textsc{Rel}(T)$ iff $\llbracket S\rrbracket\subseteq\llbracket T\rrbracket$)
$\exists T\in\textsc{Reg}_{\mathsf{all}}$ | reduces to $T=(\Sigma\cup\Gamma)^{*}$
$\exists T\in\textsc{Reg}_{\mathsf{FSL}}$ | reduces to $T=(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$
$\exists T\in\textsc{Reg}_{\mathsf{FS}}$ | reduces to $T=\Sigma^{*}\Gamma^{*}$
Table 2:  Overview of results for instances of the resynchronized definability
problem (upper and middle rows) and variants (lower rows). The results are
described in Section 4.1.

In Table 2 we give an overview of known and new results. The table is
organized in the same way as Table 1 for the uniformization problems. As
classes for source relations we consider rational, automatic, and recognizable
relations. The upper three rows correspond to the question whether a relation
is rational, automatic, and recognizable, respectively, because the target
languages are effective canonical representations of their respective relation
classes, see Theorem 4. In the context of definability, the lower three rows
correspond to the same problems as in the upper three rows, respectively
(while in the context of uniformization by subsequential transducers there are
differences, see Table 1).

The three middle rows describe the instances of the resynchronized
definability problem where a target synchronization language is given as part
of the input. The undecidability and decidability results shown in the table
are not very difficult to obtain, and are explained below. The most
interesting case, whether given automatic relation is definable inside a given
target language of finite shiftlag, is considered in Section 4.2. The general
case remains open, however, we solve some special cases of the problem.

Let us now turn to the undecidability results in the middle three rows. For
the first column and the second and third middle row, undecidability follows
directly for the choices of $T=(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$ and
$\Sigma^{*}\Gamma^{*}$, respectively.

The undecidability results for the first row in the middle part are a direct
consequence of the undecidability of the universality problem for rational
relations, see e.g., Berstel (1979).

######  Proposition 18.

For every fixed source language $S$ with $\llbracket
S\rrbracket=\Sigma^{*}\times\Gamma^{*}$ the resynchronized definability
problem for given $T\in\textsc{Reg}_{\mathsf{all}}$ is undecidable.

###### Proof.

If $\llbracket S\rrbracket=\Sigma^{*}\times\Gamma^{*}$, then the question if
$S$ can be defined in $T$ is equivalent to asking whether $\llbracket
T\rrbracket$ is universal. This corresponds to the universality problem for
rational relations because there is a one-to-one correspondence between finite
state transducers and regular synchronization languages (as explained in
Section 2). ∎

The decidability results in the middle rows of Table 2 are based on the
following simple lemma.

######  Lemma 19.

Given a recognizable relation $R$ and $T\in\textsc{Reg}_{\mathsf{FS}}$, the
set $\\{w\in T\mid\llbracket w\rrbracket\in R\\}$ is regular.

###### Proof.

Since $R$ is recognizable it can be effectively expressed as a finite union of
products of regular languages, say $R=\bigcup_{i=0}^{n}U_{i}\times V_{i}$ with
regular languages $U_{i}\subseteq\Sigma^{*}$ and $V_{i}\subseteq\Gamma^{*}$.
An NFA for $\\{w\in S\mid\llbracket w\rrbracket\in R\\}$ has to accept some
$w\in(\Sigma\cup\Gamma)^{*}$ if $w\in T$, $\pi_{\mathbbmtt{i}}(w)\in U_{i}$
and $\pi_{\mathbbmtt{o}}(w)\in V_{i}$ for some $i$. It is routine to construct
such an NFA from NFAs for $T$ and the $U_{i},V_{i}$. ∎

######  Proposition 20.

The resynchronized definability problem is decidable if the given source
language has finite shift and the given target language has finite shiftlag.

###### Proof.

Let $S\in\textsc{Reg}_{\mathsf{FS}}$ and $T\in\textsc{Reg}_{\mathsf{FSL}}$. We
show that $\llbracket S\rrbracket\in\textsc{Rel}(T)$ iff $\llbracket
S\rrbracket\subseteq\llbracket T\rrbracket$. Clearly, if $\llbracket
S\rrbracket\not\subseteq\llbracket T\rrbracket$, then $\llbracket
S\rrbracket\not\in\textsc{Rel}(T)$. For the other direction, let $U:=\\{w\in
T\mid\llbracket w\rrbracket\in\llbracket S\rrbracket\\}$ be the set of all
synchronizations in $T$ that synchronize a pair in $\llbracket S\rrbracket$.
The relation $\llbracket S\rrbracket$ is recognizable, because $S$ is regular
and has finite shift. Hence, $U$ is regular according to Lemma 19. If
$\llbracket S\rrbracket\subseteq\llbracket T\rrbracket$, then each pair in
$\llbracket S\rrbracket$ has at least one synchronization in $T$, and
therefore $\llbracket U\rrbracket=\llbracket S\rrbracket$, which means that
$\llbracket S\rrbracket\in\textsc{Rel}(T)$.

Since $\llbracket S\rrbracket$ and $\llbracket T\rrbracket$ are automatic
relations, the inclusion $\llbracket S\rrbracket\subseteq\llbracket
T\rrbracket$ is decidable. ∎

######  Proposition 21.

The resynchronized definability problem is decidable if the given source
language has finite shiftlag and the given target language has finite shift.

###### Proof.

Given $S\in\textsc{Reg}_{\mathsf{FSL}}$ and $T\in\textsc{Reg}_{\mathsf{FS}}$.
The relation $\llbracket S\rrbracket$ is automatic, and for automatic
relations it is decidable whether they are recognizable, see Carton et al.
(2006). If $\llbracket S\rrbracket$ is not recognizable, then $\llbracket
S\rrbracket\notin\textsc{Rel}(T)\subseteq\textsc{Rec}$. If $\llbracket
S\rrbracket$ is recognizable, it can be effectively represented as a
recognizable relation, i.e., as some
$S^{\prime}\in\textsc{Reg}_{\mathsf{FS}}$. Then, the problem reduces to the
resynchronized definability problem for regular source and target languages
with finite shift, which is decidable according to Proposition 20. ∎

###  4.2 Automatic source relations and targets with finite shiftlag

We do not know whether the resynchronized definability problem for a given
automatic relation and a given regular synchronization language with finite
shiftlag is decidable. However, we provide some partial answers and show
decidability for some special cases in Sections 4.2.1, 4.2.2 and 4.2.3. We
start by explaining how the problem is related to another open problem, namely
the problem whether two given disjoint automatic relations $R_{1}$ and $R_{2}$
can be separated by a recognizable relation, that is, asking whether there
exists a recognizable relation $R$ such that $R_{1}\subseteq R$ and $R\cap
R_{2}=\emptyset$, see Proposition 22.

This problem seems to lie on the border between decidability and
undecidability, we give a brief, rather informal, explanation. The following
problem was recently shown to be undecidable by Kopczynski (2016): Given two
visibly pushdown languages $L_{1}$ and $L_{2}$ that are disjoint, does there
exist a regular language $L$ that separates $L_{1}$ and $L_{2}$, that is,
$L_{1}\subseteq L$ and $L_{2}\cap L=\emptyset$? Although this is an
undecidable problem in general, we explain how to reduce the problem whether
two disjoint automatic relations are separable by a recognizable relation to a
more restricted variant.

An automatic relation can be translated into a so-called one-turn visibly
pushdown language. Think of a one-turn visibly pushdown language obtained from
an automatic relation $R$ as a $\Sigma^{*}\Gamma^{*}$-controlled language of
the form $\\{u^{r}v\mid(u,v)\text{ is in the relation }R\\}$. The idea is that
in a visibly pushdown automaton, after reading $u^{r}$, the stack content is
$u$, then while reading $v$ the stack is emptied and membership of $(u,v)$ in
the relation is verified as follows: Let $S$ be the
$(\Sigma\Gamma)^{*}(\Sigma^{*}\cup\Gamma^{*})$-controlled representation of
$R$. The visibly pushdown automaton repeats these steps: a letter from the
input $u$ is read, and a letter from the stack content $v$ is read (and
popped). The pair of letters is used to simulate two steps in a DFA that
recognizes the set $S$.

Turning to the separability problem, if there is a regular language separating
two such one-turn visibly pushdown languages obtained from two disjoint
automatic relations, then there is such a regular language that is
$\Sigma^{*}\Gamma^{*}$-controlled (since all relevant words are in
$\Sigma^{*}\Gamma^{*}$). Consequently, the automatic relations that served as
a starting point are separable by a recognizable relation of the form
$\\{(u^{r},v)\mid uv\text{ is in the separating language with
}u\in\Sigma^{*}\text{ and }v\in\Gamma^{*}\\}$.

######  Proposition 22.

The problem whether two automatic relations are separable by a recognizable
relation can be reduced to the resynchronized definability problem for given
source and target languages with finite shiftlag.

###### Proof.

Let $R_{1}\subseteq\Sigma^{*}\times\Gamma^{*}$ and
$R_{2}\subseteq\Sigma^{*}\times\Gamma^{*}$ be two automatic relations with
$R_{1}\cap R_{2}=\emptyset$. For the reduction, we define a source language
$S$ and a target language $T$, both with finite shiftlag, such that
$\llbracket S\rrbracket\in\textsc{Rel}(T)$ iff there is a recognizable
relation that contains $R_{1}$ and has empty intersection with $R_{2}$.

Let $S$ be the $(\Sigma\Gamma)^{*}(\Sigma^{*}\cup\Gamma^{*})$-controlled
representation of $\overline{R_{2}}$, that is, of the complement of $R_{2}$.
The set $S$ can be obtained starting from a
$(\Sigma\Gamma)^{*}(\Sigma^{*}\cup\Gamma^{*})$-controlled representation of
$R_{2}$ via complementation and intersection. The target language $T$ is
defined such that a definition of $\llbracket S\rrbracket$ as a subset of $T$
must contain all pairs from $R_{1}$ in the recognizable synchronization
$\Sigma^{*}\Gamma^{*}$. The pairs that are neither in $R_{1}$ nor in $R_{2}$
can be contained using the recognizable or the automatic synchronization (or
both). This is achieved by choosing $T:=\Sigma^{*}\Gamma^{*}\cup M$, where $M$
is the $(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$-controlled representation
of $\overline{R_{1}}\cap\overline{R_{2}}$. We show that $\llbracket
S\rrbracket\in\textsc{Rel}(T)$ iff $R_{1}$ and $R_{2}$ are separable by a
recognizable relation.

Assume $\llbracket S\rrbracket\in\textsc{Rel}(T)$, and let $U\subseteq T$ be
regular with $\llbracket U\rrbracket=\llbracket S\rrbracket=\overline{R_{2}}$.
Let $U^{\prime}=U\cap\Sigma^{*}\Gamma^{*}$. Then $\llbracket
U^{\prime}\rrbracket$ is a recognizable relation. Because $\llbracket
U^{\prime}\rrbracket\subseteq\llbracket U\rrbracket=\overline{R_{2}}$, we
obtain that $R_{2}\cap\llbracket U^{\prime}\rrbracket=\emptyset$. Further,
$R_{1}\subseteq\overline{R_{2}}=\llbracket U\rrbracket$. Since $\llbracket
M\rrbracket\subseteq\overline{R_{1}}$, synchronizations in $M$ cannot
contribute anything from $R_{1}$. From
$U^{\prime}=U\cap\Sigma^{*}\Gamma^{*}=U\setminus M$, we thus obtain that
$R_{1}\subseteq\llbracket U^{\prime}\rrbracket$. Hence, $\llbracket
U^{\prime}\rrbracket$ is a recognizable relation that separates $R_{1}$ and
$R_{2}$.

Assume $R$ is a recognizable relation that separates $R_{1}$ and $R_{2}$. We
have $\overline{R_{2}}=R\cup\llbracket M\rrbracket$, thus we can define $S$ in
$T$ by $M\cup N$, where $N$ is the $\Sigma^{*}\Gamma^{*}$-controlled
representation of $R$. ∎

####  4.2.1 Special types of definitions

The reduction in the proof of Proposition 22 suggests that the difficulty of
the problem is coming from the fact that for certain pairs in the source
relation, there are different synchronizations available in $T$. In the
reduction, the pairs that are neither in $R_{1}$ nor in $R_{2}$ are contained
in $T$ with their $(\Sigma\Gamma)^{*}(\Sigma^{*}\cup\Gamma^{*})$-controlled
representation and their $\Sigma^{*}\Gamma^{*}$-controlled representation.
These two representations are the two extreme cases in the sense that one
representation is completely asynchronous (input before output), and the other
representation is as synchronous as possible (alternating between input and
output as long as possible). The definition of $\llbracket S\rrbracket$ in $T$
has to select some of the asynchronous representations but, in general, not
all of them. This is also illustrated in Example 17.

In this section we show that this is indeed the main source of the difficulty
of the problem. We define special types of definitions of $\llbracket
S\rrbracket$ in $T$ that correspond to the selection of, roughly speaking, the
most asynchronous representation of $\llbracket S\rrbracket$ in $T$ (called
$\mathit{minsync}(S,T)$), the most synchronous representations of $\llbracket
S\rrbracket$ in $T$ (called $\mathit{maxsync}(S,T)$), and the full
representation of $\llbracket S\rrbracket$ in $T$ (called
$\mathit{allsync}(S,T)$). We show that regularity of these representations of
$\llbracket S\rrbracket$ in $T$ is decidable. In Sections 4.2.2 and 4.2.3 we
then give applications of these results.

For the formal definitions we need a measure of how “(a)synchronous” a word
$w$ is in a synchronization language $T$ of finite shiftlag. A
characterization for regular synchronization languages of finite shiftlag by
Figueira and Libkin (2015) (formally stated in Lemma 23 below) shows that such
languages can be expressed as a finite union of concatenations of a regular
language with finite lag and a regular language with finite shift.

Given $\gamma\in\mathbbm{N}$, we denote by $L_{\leq\gamma}$ the regular set of
words over $\Sigma\cup\Gamma$ with $\leq\\!\\!\gamma$-lagged positions, i.e.,
$L_{\leq\gamma}=\\{u\in(\Sigma\cup\Gamma)^{*}\mid\mathit{lag}(u)\leq\gamma\\}$.

######  Lemma 23 (Figueira and Libkin (2015)).

Given a regular language $S\subseteq(\Sigma\cup\Gamma)^{*}$ with
$\mathit{shiftlag}(S)<n$. It holds that $S\subseteq
L_{\leq\gamma}\cdot(\Sigma^{*}+\Gamma^{*})^{n}$ with $\gamma$ chosen as
$2\left(n(|Q|+1)+1\right)$, where $Q$ is the state set of an NFA recognizing
$S$.

Intuitively, the finite lag part of this representation of $T$ corresponds to
the synchronous part. So the idea is that we consider for $w\in T$ the longest
prefix $x$ of $w$ such that $x^{-1}T$ is not of finite shift. The longer such
a prefix, the “more synchronous” the word $w$ is inside $T$. Formally, these
ideas are captured by a partial order on words in $T$, as defined below.

Given a synchronization language $T\in\textsc{Reg}_{\mathsf{FSL}}$, we define
a partial order on $T$. Given $w,w^{\prime}\in T$ such that $\llbracket
w\rrbracket=\llbracket w^{\prime}\rrbracket$, we let $w\preceq_{T}w^{\prime}$
if $(w^{\prime}[1,i])^{-1}T\in\textsc{Reg}_{\mathsf{FS}}$ implies
$(w[1,i])^{-1}T\in\textsc{Reg}_{\mathsf{FS}}$ for all $i$. As usual, we let
$w\approx_{T}w^{\prime}$ if $w\preceq_{T}w^{\prime}$ and
$w^{\prime}\preceq_{T}w$, and $w\prec_{T}w^{\prime}$ if
$w\preceq_{T}w^{\prime}$ and $w\not\approx_{T}w^{\prime}$. We omit the index
$T$ if it is clear from the context.

Given two synchronization languages $S,T\in\textsc{Reg}_{\mathsf{FSL}}$, we
define three sets of synchronizations, namely,

$\displaystyle\mathit{minsync}(S,T)=$ $\displaystyle\quad\\{w\in
T\mid\llbracket w\rrbracket\in\llbracket S\rrbracket\text{ and
}w\preceq_{T}w^{\prime}\text{ for all }w^{\prime}\in T\text{ such that
}\llbracket w\rrbracket=\llbracket w^{\prime}\rrbracket\\},$
$\displaystyle\mathit{maxsync}(S,T)=$ $\displaystyle\quad\\{w\in
T\mid\llbracket w\rrbracket\in\llbracket S\rrbracket\text{ and
}w\succeq_{T}w^{\prime}\text{ for all }w^{\prime}\in T\text{ such that
}\llbracket w\rrbracket=\llbracket w^{\prime}\rrbracket\\},\text{ and}$
$\displaystyle\mathit{allsync}(S,T)=\\{w\in T\mid\llbracket
w\rrbracket\in\llbracket S\rrbracket\\}.$

If one of the above sets is regular, and $\llbracket
S\rrbracket\subseteq\llbracket T\rrbracket$, then this gives a $T$-controlled
definition of $\llbracket S\rrbracket$ because $\mathit{minsync}(S,T)$ and
$\mathit{maxsync}(S,T)$ contain exactly one representation of every element in
$\llbracket S\rrbracket$, and $\mathit{allsync}(S,T)$ contains all
representations of $\llbracket S\rrbracket$-elements that are in $T$. Our main
goal is to show that it is decidable whether these sets are regular, see Lemma
31. Towards that we introduce some additional notations, definitions, and
lemmas.

##### Additional notations.

Given a DFA $\mathcal{A}$ over $\Sigma\cup\Gamma$, we denote by
$Q_{\mathcal{A}}^{\mathsf{FS}}\subseteq Q_{\mathcal{A}}$ the set that contains
a state $q$ if $L(\mathcal{A}_{q})\in\textsc{Reg}_{\mathsf{FS}}$, where
$\mathcal{A}_{q}$ denotes $\mathcal{A}$ with initial state $q$. The following
lemma is a simple consequence of this definition.

######  Lemma 24.

Let $T\in\textsc{Reg}_{\mathsf{FSL}}$ and $\mathcal{A}$ be a DFA with
$L(\mathcal{A})=T$. For all $w\in(\Sigma\cup\Gamma)^{*}$ we have that
$w^{-1}T\in\textsc{Reg}_{\mathsf{FS}}$ iff $\delta_{\mathcal{A}}^{*}(w)\in
Q_{\mathcal{A}}^{\mathsf{FS}}$.

We say that two words $x,y\in(\Sigma\cup\Gamma)^{*}$ are _compatible_ if they
are of same length and there exist $u,v\in(\Sigma\cup\Gamma)^{*}$ such that
$\llbracket xu\rrbracket=\llbracket yv\rrbracket$. So two words of same length
are compatible if they can be extended such that they synchronize the same
pair. For example, with $\Sigma=\\{a,b\\}$ and $\Gamma=\\{c,d\\}$, the words
$acab$ and $cadc$ are compatible because $\llbracket acab\cdot
dc\rrbracket=\llbracket cadc\cdot ab\rrbracket=(aab,cdc)$. Furthermore, we
define $\mathit{diff}(x,y)=(u,v)$ if $x$ and $y$ are compatible and $u,v$ are
the shortest words such that $\llbracket xu\rrbracket=\llbracket
yv\rrbracket$, and let $|\mathit{diff}(x,y)|=|uv|$. Note that $u$ and $v$ are
unique because $|x|=|y|$ implies that one of $u,v$ consists only of input
symbols, and the other one only of output symbols. Taking the previous
example, we have $\mathit{diff}(acab,cadc)=(dc,ab)$

As a tool in our proofs we use an automaton that synchronously reads pairs of
words $x,y$ that have bounded lag and, if $x,y$ are compatible, it reaches the
state $(u,v)$ for $\mathit{diff}(x,y)=(u,v)$. This is explained in more detail
below.

First note that for compatible words of bounded lag, the length of their
difference is bounded.

######  Remark 25.

Let $x,y$ be compatible with $\mathit{diff}(x,y)=(u,v)$. If
$\mathit{lag}(x),\mathit{lag}(y)\leq k$, then $|u|,|v|\leq k$.

Given $k\in\mathbbm{N}$, we define the relation
$\mathbb{D}_{k}\subseteq(\Sigma\cup\Gamma)^{*}\times(\Sigma\cup\Gamma)^{*}$ as

$\mathbb{D}_{k}:=\\{(x,y)\mid\text{$x$ and $y$ are compatible and
$\mathit{lag}(x),\mathit{lag}(y)\leq k$}\\}.$

The relation $\mathbb{D}_{k}$ is automatic, that is, the set $\\{x\otimes
y\mid(x,y)\in\mathbb{D}_{k}\\}$ is regular, where $x\otimes y$ denotes the
_convolution_ of $x$ and $y$ defined as the word
$(x[1],y[1])\cdots(x[n],y[n])\in(\Sigma\times\Gamma)^{*}$, where $n=|x|=|y|$
(if $|x|\neq|y|$ the convolution is not defined). Due to Remark 25, the set of
convolutions of pairs in $\mathbb{D}_{k}$ is recognized by a DFA
$\mathcal{D}_{k}$ that keeps track of the difference of the words. Formally,
$\mathcal{D}_{k}=(Q,(\Sigma\cup\Gamma)\times(\Sigma\cup\Gamma),(\varepsilon,\varepsilon),\Delta,Q)$,
where $Q=\\{(w_{0},w_{1})\mid
w_{0},w_{1}\in\Sigma^{*}\cup\Gamma^{*},|w_{0}|=|w_{1}|,|w_{0}|,|w_{1}|\leq
k\\}$ and the transitions in $\Delta$ update the difference for the next input
$(a_{0},a_{1})$, which can formally be defined by
$\bigl{(}(w_{0},w_{1}),(a_{0},a_{1}),(y_{0}z_{0},y_{1}z_{1})\bigr{)}\in\Delta$
with

$y_{i}=\begin{cases}a_{i}^{-1}w_{i}&\text{if
}a_{i}\in\Sigma,w_{i}\in\Sigma^{+}\text{ or
}a_{i}\in\Gamma,w_{i}\in\Gamma^{+}\\\ w_{i}&\text{if
}a_{i}\in\Sigma,w_{i}\in\Gamma^{+}\text{ or
}a_{i}\in\Gamma,w_{i}\in\Sigma^{+}\\\ \varepsilon&\text{if
}w_{i}=\varepsilon,a_{i}=a_{1-i}\\\ a_{1-i}&\text{if
}w_{i}=\varepsilon,a_{i}\neq a_{1-i},\text{ and}\end{cases}$
$z_{i}=\begin{cases}\varepsilon&\text{if
}a_{1-i}\in\Sigma,w_{1-i}\in\Sigma^{+}\text{ or
}a_{1-i}\in\Gamma,w_{1-i}\in\Gamma^{+}\\\ a_{1-i}&\text{if
}a_{1-i}\in\Sigma,w_{1-i}\in\Gamma^{+}\text{ or
}a_{1-i}\in\Gamma,w_{1-i}\in\Sigma^{+}\\\ \varepsilon&\text{if
}w_{i}=\varepsilon,a_{i}=a_{1-i}\\\ a_{1-i}&\text{if
}w_{i}=\varepsilon,a_{i}\neq a_{1-i}\end{cases}$

for $i=0,1$. Note that if the operation $a_{i}^{-1}w_{i}$ does not yield an
element from $(\Sigma\cup\Gamma)^{*}$ then there exists no transition from
$(w_{0},w_{1})$ with label $(a_{0},a_{1})$, because this indicates
incompatibility.

By an easy but cumbersome induction one can show that the above definition of
$\mathcal{D}_{k}$ is such that the automaton indeed computes the difference of
two compatible string with lag at most $k$, as stated in the following lemma.

######  Lemma 26.

Given $x,y$ compatible with $\mathit{lag}(x),\mathit{lag}(y)\leq k$ and
$\mathit{diff}(x,y)=(u,v)$, then
$\mathcal{D}_{k}\colon(\varepsilon,\varepsilon)\xrightarrow{x\otimes y}(u,v)$.

Lastly, given $T\in\textsc{Reg}_{\mathsf{FSL}}$, we define the set
$\mathit{fse}(T)$ – finite shift entry – as

$\mathit{fse}(T):=\\{x\in\mathit{Prefs}(T)\mid
x^{-1}T\in\textsc{Reg}_{\mathsf{FS}}\text{ and
}(x^{\prime})^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\text{ for all $x^{\prime}$
proper prefix of $x$}\\},$

that is, the set of all prefixes of $T$ that induce an entry point into some
finite shift remainder of $T$. It is easy to see that this set is regular
because by Lemma 24 it is sufficient to accept those words that enter a state
from $Q_{\mathcal{A}}^{\mathsf{FS}}$ in a DFA $\mathcal{A}$ for $T$ for the
first time. Furthermore, $\mathit{lag}(\mathit{fse}(T))\leq\gamma$, where
$\gamma$ is chosen according to Lemma 23.

##### Main lemmas.

We are ready to show our key lemmas. The decidability of regularity of the
sets $\mathit{minsync}(S,T)$, $\mathit{maxsync}(S,T)$, and
$\mathit{allsync}(S,T)$ is stated in Lemma 31.

We start with a helpful lemma about the regularity of sets of non-minimal
synchronizations, and then consider the sets $\mathit{minsync}(T,T)$,
$\mathit{maxsync}(T,T)$ without the additional parameter $S$ in Lemma 28 and
Lemma 30.

######  Lemma 27.

For $T\in\textsc{Reg}_{\mathsf{FSL}}$ and a regular $T^{\prime}\subseteq T$,
the set $\\{w\in T\mid\text{ there is }w^{\prime}\in T^{\prime}\text{ such
that }w\succ w^{\prime}\\}$ is regular.

###### Proof.

Let $U:=\\{w\in T\mid\text{ there is }w^{\prime}\in T^{\prime}\text{ such that
}w\succ_{T}w^{\prime}\\}$.

A synchronization $w\in T$ is in $U$ if $w=xz$ such that
$x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}$ and there exists some
$y\in\mathit{fse}(T)$ such that $x,y$ are compatible and $\llbracket
w\rrbracket\in\llbracket y(y^{-1}T^{\prime})\rrbracket$. The last condition
ensures that $y$ can be extended to some $w^{\prime}=yz^{\prime}\in
T^{\prime}$ with $\llbracket w\rrbracket=\llbracket w^{\prime}\rrbracket$.

This description allows us to represent $U$ as

$\displaystyle\bigcup_{\mathclap{\begin{subarray}{c}x\text{ s.t.\
}x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\\\
y\in\mathit{fse}(T)\end{subarray}}}\ \\{xz\in T\mid\llbracket
xz\rrbracket\in\llbracket
y(y^{-1}T^{\prime})\rrbracket\\}=\bigcup_{\mathclap{\begin{subarray}{c}x\text{
s.t.\ }x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\\\
y\in\mathit{fse}(T)\end{subarray}}}\ x\cdot\\{z\in x^{-1}T\mid\llbracket
z\rrbracket\in\llbracket x\rrbracket^{-1}(\llbracket y\rrbracket\llbracket
y^{-1}T^{\prime}\rrbracket)\\}$ $\displaystyle=$
$\displaystyle\bigcup_{\mathclap{\begin{subarray}{c}x\text{ s.t.\
}x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\\\
y\in\mathit{fse}(T)\end{subarray}}}\ x\cdot\\{z\in x^{-1}T\mid\llbracket
z\rrbracket\in\llbracket v\rrbracket^{-1}(\llbracket u\rrbracket\llbracket
y^{-1}T^{\prime}\rrbracket)\\},\text{where $\mathit{diff}(x,y)=(u,v)$.}$

Using this representation, our goal is to show that $U$ is regular by
rewriting it it terms of automata for $T,T^{\prime}$. Let
$\mathcal{A},\mathcal{A}^{\prime}$ denote DFAs for $T,T^{\prime}$
respectively. For simplicity, we assume that $\mathcal{A}$ and
$\mathcal{A}^{\prime}$ use the same transition structure, and only differ in
their sets of final states (this can be achieved by taking the product of the
two transition structures). Recall that $x$ and $y$ (chosen as above) have a
lag of at most $\gamma$, where $\gamma$ is chosen according to Lemma 23.
According to Lemma 26, the run of $\mathcal{D}_{\gamma}$ on $x\otimes y$ ends
in the state $\mathit{diff}(x,y)$, say $(u,v)$, which indicates that
$\llbracket xu\rrbracket=\llbracket yv\rrbracket$. So we can write the
representation of $U$ as

$\bigcup_{\mathclap{\begin{subarray}{c}p\in Q_{\mathcal{A}}\setminus
Q_{\mathcal{A}}^{\mathsf{FS}}\\\ q\in Q_{\mathcal{A}}^{\mathsf{FS}}\\\
u,v\in\Sigma^{\leq\gamma}\cup\Gamma^{\leq\gamma}\end{subarray}}}\
M_{p,q,u,v}\cdot\overbrace{\\{z\in L(\mathcal{A}_{p})\mid\llbracket
z\rrbracket\in\underbrace{\llbracket u\rrbracket^{-1}\bigl{(}\llbracket
v\rrbracket\llbracket
L(\mathcal{A}_{q}^{\prime})\rrbracket\bigr{)}}_{R_{q,u,v}}\\}}^{L_{p,q,u,v}},$

where

$\begin{array}[]{ll}M_{p,q,u,v}=\\{x\in(\Sigma\cup\Gamma)^{*}\mid&\text{there
is }y\in\mathit{fse}(T)\text{ such that }\mathcal{A}\colon
q_{0}^{\mathcal{A}}\xrightarrow{x}p,\\\ &\mathcal{A}\colon
q_{0}^{\mathcal{A}}\xrightarrow{y}q,\text{ and
}\mathcal{D}_{\gamma}\colon(\varepsilon,\varepsilon)\xrightarrow{x\otimes
y}(u,v)\\}.\end{array}$

The set $M_{p,q,u,v}$ is easily seen to be regular. Since $L(\mathcal{A}_{q})$
is regular and has finite shift, the relation $R_{q,u,v}$ is recognizable.
Hence, the set $L_{p,q,u,v}$ is regular according to Lemma 19.

In conclusion, the set $U$ is representable as a finite union of regular sets,
thus, it is regular. ∎

######  Lemma 28.

For each $T\in\textsc{Reg}_{\mathsf{FSL}}$ the set $\mathit{minsync}(T,T)$ is
regular.

###### Proof.

The set $\mathit{minsync}(T,T)$ is equal to $T\setminus\\{w\in T\mid\text{
there is }w^{\prime}\in T\text{ such that }w\succ w^{\prime}\\},$ that is, $T$
without all synchronizations that are not minimal. An application of Lemma 27
with $T^{\prime}=T$ yields that the set of non-minimal synchronizations in $T$
is regular, and hence also its complement $\mathit{minsync}(T,T)$. ∎

In contrast to Lemma 28, given $T\in\textsc{Reg}_{\mathsf{FSL}}$, the set
$\mathit{maxsync}(T,T)$ is not regular in general.

######  Example 29.

Consider $T=(\Sigma\Gamma)^{*}+\Sigma^{*}\Gamma^{*}$. The set
$\mathit{maxsync}(T,T)$ is of the form

$T\setminus\\{xy\in\Sigma^{*}\Gamma^{*}\mid
x\in\Sigma^{*},y\in\Gamma^{*},|x|=|y|\\}.$

It is easy to see that the set to be removed is not regular, thus,
$\mathit{maxsync}(T,T)$ is not regular.

In fact, regularity of $\mathit{maxsync}(T,T)$ turns out to be a strong
property because then the resynchronized definability problem reduces to the
question of regularity of $\mathit{maxsync}(S,T)$, as stated in the following
lemma.

######  Lemma 30.

Let $S,T\in\textsc{Reg}_{\mathsf{FSL}}$ such that $\mathit{maxsync}(T,T)$ is
regular. Then $\llbracket S\rrbracket\in\textsc{Rel}(T)$ iff
$\mathit{maxsync}(S,T)$ is regular and $\llbracket
S\rrbracket\subseteq\llbracket T\rrbracket$.

###### Proof.

If $\mathit{maxsync}(S,T)$ is regular and $\llbracket
S\rrbracket\subseteq\llbracket T\rrbracket$, then $\llbracket
S\rrbracket=\llbracket\mathit{maxsync}(S,T)\rrbracket\in\textsc{Rel}(T)$.

Now assume that $\llbracket S\rrbracket\in\textsc{Rel}(T)$, and let
$T^{\prime}\subseteq T$ be a regular set such that $\llbracket
T^{\prime}\rrbracket=\llbracket S\rrbracket$. Then
$\mathit{maxsync}(S,T)=\mathit{maxsync}(T^{\prime},T)$, and we have

$\mathit{maxsync}(T^{\prime},T)=\mathit{maxsync}(T,T)\cap(T^{\prime}\cup\underbrace{\\{w\in
T\mid\text{ there is }w^{\prime}\in T^{\prime}\text{ with }w\succ
w^{\prime}\\}}_{U}).$

The set $U$ is regular according to Lemma 27, and hence
$\mathit{maxsync}(T^{\prime},T)$ is a Boolean combination of regular sets. ∎

Note that Lemma 30 fails without the assumption that $\mathit{maxsync}(T,T)$
is regular: If $\mathit{maxsync}(T,T)$ is not regular, we can choose $S=T$ and
obtain that $\llbracket S\rrbracket=\llbracket T\rrbracket\in\textsc{Rel}(T)$,
and $\mathit{maxsync}(S,T)=\mathit{maxsync}(T,T)$ is not regular (and Example
29 shows that there are regular sets $T$ such that $\mathit{maxsync}(T,T)$ is
not regular).

We now prove our main lemma on the decidability of the regularity of the
different sets of synchronizations.

######  Lemma 31.

Given two synchronization languages $S,T\in\textsc{Reg}_{\mathsf{FSL}}$. The
regularity of the followings sets is effectively decidable.

  1. 1.

$\mathit{minsync}(S,T)$,

  2. 2.

$\mathit{maxsync}(S,T)$, and

  3. 3.

$\mathit{allsync}(S,T)$.

###### Proof.

First note that the definition of the sets $\mathit{minsync}(S,T)$,
$\mathit{maxsync}(S,T)$, and $\mathit{allsync}(S,T)$ does not depend on the
precise representation of $S$, but only on the relation $\llbracket
S\rrbracket$. Hence, we can choose a representation of $\llbracket
S\rrbracket$ inside $\textsc{Reg}_{\mathsf{FSL}}$ that is most convenient for
our purposes.

According to Lemma 23, $T\subseteq
L_{\leq\gamma}\cdot(\Sigma^{*}+\Gamma^{*})^{m}$ for some $\gamma$ and $m$.
This means the synchronizations in $T$ have lag at most $\gamma$ before
entering the finite shift part. We choose for $S$ what we call the full
$\gamma$-lagged representation, which means that $S$ satisfies $S=\\{w\in
L_{\leq\gamma}\cdot(\Sigma^{*}+\Gamma^{*})\mid\llbracket
w\rrbracket\in\llbracket S\rrbracket\\}$. We can obtain such a representation
of $\llbracket S\rrbracket$ as follows: Let $S^{\prime}$ be the canonical
$(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$-controlled representation of
$\llbracket S\rrbracket$. Then $\\{y\mid\text{exists }x\in S^{\prime}\text{
and }\mathcal{D}_{\gamma}:(\varepsilon,\varepsilon)\xrightarrow{x\otimes
y}(\varepsilon,\varepsilon)\\}$ is the full $\gamma$-lagged representation of
$\llbracket S\rrbracket$, which is clearly regular.

So in the following, we assume that $S$ is the full $\gamma$-lagged
representation of $\llbracket S\rrbracket$, and let $\mathcal{A}$ be a DFA for
$S$. The advantage of this representation is the following. Let
$y\in(\Sigma\cup\Gamma)^{*}$ with $\mathit{lag}(y)\leq\gamma$. Then
$\llbracket y\rrbracket^{-1}\llbracket S\rrbracket=\llbracket
y^{-1}S\rrbracket$, that is, if there is a pair in $\llbracket S\rrbracket$
that starts with $\llbracket y\rrbracket$, then there is a synchronization of
that pair in $S$ that starts with $y$.

Let $\mathcal{B}$ be a DFA for $T$.

######  Claim 32.

It is decidable whether $\mathit{minsync}(S,T)$ is regular.

###### Proof.

Note that $\mathit{minsync}(S,T)=\mathit{allsync}(S,\mathit{minsync}(T,T))$.
Lemma 28 yields that $\mathit{minsync}(T,T)$ is regular. Together with the
next claim, decidability follows. ∎

In the proofs of the next claims we use that it is decidable whether an
automatic relation is recognizable, see Carton et al. (2006).

######  Claim 33.

It is decidable whether $\mathit{allsync}(S,T)$ is regular.

###### Proof.

We show that $\mathit{allsync}(S,T)$ is not regular iff there exists some
$y\in\mathit{fse}(T)$ such that the relation $\llbracket
y^{-1}S\rrbracket\cap\llbracket y^{-1}T\rrbracket$ is not recognizable.

Assume that $\llbracket y^{-1}S\rrbracket\cap\llbracket y^{-1}T\rrbracket$ is
not recognizable for some $y\in\mathit{fse}(T)$. Hence, the relation
$\llbracket y^{-1}\mathit{allsync}(S,T)\rrbracket=\llbracket
y^{-1}S\rrbracket\cap\llbracket y^{-1}T\rrbracket$ is not recognizable. Since
$y^{-1}T\in\textsc{Reg}_{\mathsf{FS}}$, the set
$y^{-1}\mathit{allsync}(S,T)\subseteq y^{-1}T$ has finite shift. However, it
is not regular, because every regular set with finite shift describes a
recognizable relation. Thus, $y^{-1}\mathit{allsync}(S,T)$ is not regular
which implies that $\mathit{allsync}(S,T)$ is not regular.

Conversely, assume that $\llbracket y^{-1}S\rrbracket\cap\llbracket
y^{-1}T\rrbracket$ is recognizable for all $y\in\mathit{fse}(T)$. We partition
the set $\mathit{allsync}(S,T)$ into $\\{w\mid
w^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\\}\cap\mathit{allsync}(S,T)$ and
$\\{w\mid w^{-1}T\in\textsc{Reg}_{\mathsf{FS}}\\}\cap\mathit{allsync}(S,T)$
and show that both sets are regular.

The first set is regular, because if
$w^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}$, then $\mathit{lag}(w)\leq\gamma$,
thus, we can rewrite first set as $\\{w\in S\cap T\mid
w^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\\}$.

The second set is described as

$\displaystyle\bigcup_{\mathclap{\begin{subarray}{c}y\in\mathit{fse}(T)\end{subarray}}}\
y\cdot(y^{-1}\mathit{allsync}(S,T))=\bigcup_{\mathclap{\begin{subarray}{c}y\in\mathit{fse}(T)\end{subarray}}}\
y\cdot\\{z\in y^{-1}T\mid\llbracket z\rrbracket\in\llbracket
y^{-1}S\rrbracket\cap\llbracket y^{-1}T\rrbracket\\}$ $\displaystyle=$
$\displaystyle\bigcup_{\mathclap{\begin{subarray}{c}p\in Q_{\mathcal{A}}\\\
q\in Q_{\mathcal{B}}\end{subarray}}}\ M_{p,q}\cdot\\{z\in
L(\mathcal{B}_{q})\mid\llbracket z\rrbracket\in\llbracket
L(\mathcal{A}_{p})\rrbracket\cap\llbracket L(\mathcal{B}_{q})\rrbracket\\},$

where $M_{p,q}=\\{y\in\mathit{fse}(T)\mid\mathcal{A}\colon
q_{0}^{\mathcal{A}}\xrightarrow{y}p,\mathcal{B}\colon
q_{0}^{\mathcal{B}}\xrightarrow{y}q\\}$. The set $M_{p,q}$ is clearly regular.
If $M_{p,q}$ is non-empty then $\llbracket
L(\mathcal{A}_{p})\rrbracket\cap\llbracket L(\mathcal{B}_{q})\rrbracket$ is
recognizable because then $\llbracket L(\mathcal{A}_{p})\rrbracket=\llbracket
y^{-1}S\rrbracket$, $\llbracket L(\mathcal{B}_{q})\rrbracket=\llbracket
y^{-1}T\rrbracket$ for some $y\in\mathit{fse}(T)$, and $\llbracket
y^{-1}S\rrbracket\cap\llbracket y^{-1}T\rrbracket$ is recognizable by
assumption. Thus, the set $\\{z\in L(\mathcal{B}_{q})\mid\llbracket
z\rrbracket\in\llbracket L(\mathcal{A}_{p})\rrbracket\cap\llbracket
L(\mathcal{B}_{q})\rrbracket\\}$ is regular according to Lemma 19.

We have shown $\mathit{allsync}(S,T)$ is regular iff $\llbracket
y^{-1}S\rrbracket\cap\llbracket y^{-1}T\rrbracket$ is recognizable for all
$y\in\mathit{fse}(T)$. With $p,q$ as above, $\llbracket
y^{-1}S\rrbracket\cap\llbracket y^{-1}T\rrbracket=\llbracket
L(\mathcal{A}_{p})\rrbracket\cap\llbracket L(\mathcal{B}_{q})\rrbracket$, and
hence there are only finitely many such relations. Further, $\llbracket
L(\mathcal{A}_{p})\rrbracket\cap\llbracket L(\mathcal{B}_{q})\rrbracket$ is an
automatic relation because $\llbracket L(\mathcal{A}_{p})\rrbracket$ and
$\llbracket L(\mathcal{B}_{q})\rrbracket$ are automatic. Hence, it is
decidable whether $\llbracket L(\mathcal{A}_{p})\rrbracket\cap\llbracket
L(\mathcal{B}_{q})\rrbracket$ is recognizable. ∎

The proof of the next claim is similar to the proof of the previous claim but
more involved.

######  Claim 34.

It is decidable whether $\mathit{maxsync}(S,T)$ is regular.

###### Proof.

Our goal is to show that $\mathit{maxsync}(S,T)$ is regular iff $\llbracket
y^{-1}\mathit{maxsync}(S,T)\rrbracket$ is recognizable for all
$y\in\mathit{fse}(T)$. The proof of this also provides a way to decide this
property.

To begin with, assume that $\mathit{maxsync}(S,T)$ is regular. Consider some
$y\in\mathit{fse}(T)$. Clearly, $y^{-1}\mathit{maxsync}(S,T)$ is regular.
Consequently, $\llbracket y^{-1}\mathit{maxsync}(S,T)\rrbracket$ is
recognizable, because $y^{-1}\mathit{maxsync}(S,T)\subseteq
y^{-1}T\in\textsc{Reg}_{\mathsf{FS}}$ is regular and has finite shift.

Conversely, assume that $\llbracket y^{-1}\mathit{maxsync}(S,T)\rrbracket$ is
recognizable for all $y\in\mathit{fse}(T)$, and consider some
$y\in\mathit{fse}(T)$. We describe $\llbracket
y^{-1}\mathit{maxsync}(S,T)\rrbracket$ as an intermediate step to showing that
$\mathit{maxsync}(S,T)$ is regular. First, we have that $z\in
y^{-1}(\mathit{maxsync}(S,T))$ if $z\in y^{-1}T$ and $\llbracket
z\rrbracket\in\llbracket y^{-1}S\rrbracket$, and there is no $x$ compatible to
$y$ such that $x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}$ and $\llbracket
yz\rrbracket\in\llbracket x(x^{-1}T)\rrbracket$ because this would mean that
$yz$ is not a maximal synchronization. We obtain that

$\displaystyle\llbracket y^{-1}\mathit{maxsync}(S,T)\rrbracket=$
$\displaystyle\left(\llbracket y^{-1}S\rrbracket\cap\llbracket
y^{-1}T\rrbracket\right)\setminus\Bigl{(}\bigcup_{\mathclap{\begin{subarray}{c}x\text{
compatible to }y\\\ x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\end{subarray}}}\
\llbracket y\rrbracket^{-1}\llbracket x(x^{-1}T)\rrbracket\Bigr{)}$
$\displaystyle=$ $\displaystyle\left(\llbracket
y^{-1}S\rrbracket\cap\llbracket
y^{-1}T\rrbracket\right)\setminus\Bigl{(}\bigcup_{\mathclap{\begin{subarray}{c}x\text{
compatible to }y\\\ x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\end{subarray}}}\
\llbracket u\rrbracket^{-1}\bigl{(}\llbracket v\rrbracket\llbracket
x^{-1}T\rrbracket\bigr{)}\Bigr{)}\text{ with }\mathit{diff}(x,y)=(u,v).$

We now rewrite this representation of $\llbracket
y^{-1}\mathit{maxsync}(S,T)\rrbracket$ based on the automata
$\mathcal{A},\mathcal{B},\mathcal{D}_{\gamma}$. Let $\mathcal{A}\colon
q_{0}^{\mathcal{A}}\xrightarrow{y}p$, and $\mathcal{B}\colon
q_{0}^{\mathcal{B}}\xrightarrow{y}q$. Then $\llbracket
L(\mathcal{A}_{p})\rrbracket=\llbracket y^{-1}S\rrbracket$, and $\llbracket
L(\mathcal{B}_{q})\rrbracket=\llbracket y^{-1}T\rrbracket$. Further, consider
some $x$ compatible to $y$ such that
$x^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}$, and let $B\colon
q_{0}^{\mathcal{B}}\xrightarrow{x}r$. Then $\llbracket
L(\mathcal{B}_{r})\rrbracket=\llbracket x^{-1}T\rrbracket$. The lags of $x$
and of $y$ are at most $\gamma$, hence
$\mathcal{D}_{\gamma}\colon(\varepsilon,\varepsilon)\xrightarrow{x\otimes
y}(u,v)$ with $\mathit{diff}(x,y)=(u,v)$ according to Lemma 26. Thus, we
obtain

$\displaystyle\llbracket
y^{-1}\mathit{maxsync}(S,T)\rrbracket=\overbrace{\bigl{(}\llbracket
L(\mathcal{A}_{p})\rrbracket\cap\llbracket
L(\mathcal{B}_{q})\rrbracket\bigr{)}\setminus\Bigl{(}\bigcup_{\mathclap{\begin{subarray}{c}(r,u,v)\in
G\end{subarray}}}\ \llbracket u\rrbracket^{-1}\bigl{(}\llbracket
v\rrbracket\llbracket
L(\mathcal{B}_{r})\rrbracket\bigr{)}\Bigr{)}}^{R_{p,q,G}},$

where $G=\\{(r,u,v)\mid\text{there is }x\text{ with }\mathcal{B}\colon
q_{0}^{\mathcal{B}}\xrightarrow{x}r\in Q_{\mathcal{B}}\setminus
Q_{\mathcal{B}}^{\mathsf{FS}}\text{ and
}\mathcal{D}_{\gamma}\colon(\varepsilon,\varepsilon)\xrightarrow{x\otimes
y}(u,v)\\}$. Note that $G$ is finite because $|u|,|v|\leq\gamma$ for all
$(r,u,v)\in G$. Furthermore, we define the transition profile $P(y)$ of $y$ as
the triple $(p,q,G)$. The profile $P(y)$ contains all necessary information to
express $\llbracket y^{-1}\mathit{maxsync}(S,T)\rrbracket=R_{P(y)}$. Let
$\mathcal{P}=\\{P(y)\mid y\in\mathit{fse}(T)\\}$ be the set of all relevant
profiles, and note that the set is finite.

We are ready to show that $\mathit{maxsync}(S,T)$ is regular. Towards that we
partition it into $\\{w\mid
w^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\\}\cap\mathit{maxsync}(S,T)$ and
$\\{w\mid w^{-1}T\in\textsc{Reg}_{\mathsf{FS}}\\}\cap\mathit{maxsync}(S,T)$
and show that both sets are regular. The first set contains only
synchronizations that do not have some $y\in\mathit{fse}(T)$ as prefix, and
the second set contains only synchronizations that have some
$y\in\mathit{fse}(T)$ as prefix.

The first set is regular, because if
$w^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}$, then $\mathit{lag}(w)\leq\gamma$,
thus, we can rewrite first set as $\\{w\in S\cap T\mid
w^{-1}T\notin\textsc{Reg}_{\mathsf{FS}}\\}$.

The second set is described as

$\bigcup_{\mathclap{y\in\mathit{fse}(T)}}\
y\cdot\bigl{(}y^{-1}\mathit{maxsync}(S,T)\bigr{)}=\bigcup_{\mathclap{y\in\mathit{fse}(T)}}\
y\cdot\\{z\in y^{-1}T\mid\llbracket z\rrbracket\in\llbracket
y^{-1}\mathit{maxsync}(S,T)\rrbracket\\}.$

Using the definition of $\llbracket y^{-1}\mathit{maxsync}(S,T)\rrbracket$
from above we can express this as

$\bigcup_{\mathclap{(p,q,G)\in\mathcal{P}}}\ M_{p,q,G}\cdot\\{z\in
L(\mathcal{B}_{q})\mid\llbracket z\rrbracket\in R_{p,q,G}\\},$

where $M_{p,q,G}=\\{y\in\mathit{fse}(T)\mid P(y)=(p,q,G)\\}$. The set
$M_{p,q,G}$ is regular because one can build an automaton that checks for in
input $y$ whether $y\in\mathit{fse}(T)$ and whether $P(y)=(p,q,G)$ by standard
automaton constructions. If $M_{p,q,G}$ is non-empty, then there is some
$y\in\mathit{fse}(T)$ with $R_{p,q,G}=\llbracket
y^{-1}\mathit{maxsync}(S,T)\rrbracket$, which is recognizable by assumption.
Thus, the set $\\{z\in L(\mathcal{B}_{q})\mid\llbracket z\rrbracket\in
R_{p,q,G}\\}$ is regular according to Lemma 19.

Hence, $\mathit{maxsync}(S,T)$ is a finite union of regular sets.

We have shown that $\mathit{maxsync}(S,T)$ is regular iff $\llbracket
y^{-1}\mathit{maxsync}(S,T)\rrbracket$ is recognizable for all
$y\in\mathit{fse}(T)$. We have seen that
$y^{-1}\mathit{maxsync}(S,T)\rrbracket=R_{(p,q,G)}$ for $P(y)=(p,q,G)$ only
depends on the profile of $y$, so there are only finitely many such relations.
The relations used in the description of $R_{(p,q,G)}$ are all automatic, and
hence $R_{(p,q,G)}$ is also automatic. Thus, it is decidable whether
$R_{(p,q,G)}$ is recognizable. ∎

This completes the proof Lemma 31. ∎

The decidability results presented next follow easily from the above lemma.

######  Theorem 35.

It is decidable, given $S,T\in\textsc{Reg}_{\mathsf{FSL}}$, whether
$\mathit{minsync}(S,T)$, $\mathit{maxsync}(S,T)$, or $\mathit{allsync}(S,T)$
is a definition of $\llbracket S\rrbracket$ in $T$.

###### Proof.

The regularity of $\mathit{minsync}(S,T)$, $\mathit{maxsync}(S,T)$, and
$\mathit{allsync}(S,T)$ is decidable by Lemma 31. It is decidable whether
$\llbracket S\rrbracket\subseteq\llbracket T\rrbracket$, because
$S,T\in\textsc{Reg}_{\mathsf{FSL}}$ and
$(\Sigma\Gamma)^{*}(\Sigma^{*}+\Gamma^{*})$ is an effective canonical
representation of $\textsc{Reg}_{\mathsf{FSL}}$. So, deciding whether
$\llbracket S\rrbracket\subseteq\llbracket T\rrbracket$ can be reduced to
deciding inclusion of regular languages. ∎

In combination with Lemma 30 we obtain the following theorem.

######  Theorem 36.

The resynchronized definability problem is decidable for given
$S,T\in\textsc{Reg}_{\mathsf{FSL}}$ with $\mathit{maxsync}(T,T)$ regular.

In Section 4.2.3 we give an example for a class of languages $T$ such that
$\mathit{maxsync}(T,T)$ is regular.

We finish this section with some relations between the regularity of the sets
$\mathit{minsync}(S,T)$, $\mathit{maxsync}(S,T)$ and $\mathit{allsync}(S,T)$
for $S,T\in\textsc{Reg}_{\mathsf{FSL}}$. In the next examples we show that the
regularity of $\mathit{allsync}(S,T)$ does not imply the regularity of
$\mathit{maxsync}(S,T)$ and vice versa.

In Example 29, we have given an example where $\mathit{allsync}(T,T)$ is
regular and $\mathit{maxsync}(T,T)$ is not regular. Recall that
$\mathit{allsync}(T,T)=T$.

######  Example 37.

Consider $S=(\Sigma\Gamma)^{*}$ describing all pairs of words where the input
and output component have the same length. Consider
$T=(\Sigma\Gamma)^{*}+\Sigma^{*}\Gamma^{*}$. Clearly,
$\mathit{maxsync}(S,T)=(\Sigma\Gamma)^{*}$ is regular. However,
$\mathit{allsync}(S,T)$ is not regular, because it is of the form

$(\Sigma\Gamma)^{*}\cup\\{xy\in\Sigma^{*}\Gamma^{*}\mid
x\in\Sigma^{*},y\in\Gamma^{*},|x|=|y|\\},$

and the latter set is not regular.

We show that the regularity of $\mathit{minsync}(S,T)$ implies the regularity
of $\mathit{allsync}(S,T)$ and vice versa.

######  Lemma 38.

Given $S,T\in\textsc{Reg}_{\mathsf{FSL}}$, $\mathit{minsync}(S,T)$ is regular
iff $\mathit{allsync}(S,T)$ is regular.

###### Proof.

Assume $\mathit{allsync}(S,T)$ is regular. Clearly, $\mathit{minsync}(S,T)$
can be expressed as

$\mathit{minsync}(\mathit{allsync}(S,T),\mathit{allsync}(S,T)).$

Thus, $\mathit{minsync}(S,T)$ is regular according to Lemma 28.

Assume $T^{\prime}:=\mathit{minsync}(S,T)$ is regular and note that
$T^{\prime}\subseteq T$. We have

$\mathit{allsync}(S,T)=T^{\prime}\cup\underbrace{\\{w\in T\mid\text{there is
}w^{\prime}\in T^{\prime}\text{ such that }w\succ_{T}w^{\prime}\\}}_{U}$

The set $U$ is regular by Lemma 27. ∎

####  4.2.2 Unambiguous targets

Based on the results in Section 4.2.1 we can now show that the resychronized
definability problem for automatic source relations and target languages of
finite shiftlag is decidable if the target language is additionally
unambiguous.

A regular language $T\subseteq(\Sigma\cup\Gamma)^{*}$ is called _unambiguous_
if $w_{1}\neq w_{2}$ implies that $\llbracket w_{1}\rrbracket\neq\llbracket
w_{2}\rrbracket$ for all $w_{1},w_{2}\in T$.

In general, unambiguity is undecidable for regular synchronization languages.
We obtain this by a simple reduction from a known result as follows. As
mentioned in Section 2, for a regular synchronization language $S$ one can
easily construct a transducer $\mathcal{T}$ such that $S(\mathcal{T})=S$ and
vice versa. Hence, it is not difficult to see that $S$ is unambiguous iff
$\mathcal{T}$ is unambiguous222Note that in the literature unambiguous is
sometimes defined only with respect to the input., that is, for each
$(u,v)\in\llbracket S\rrbracket=R(\mathcal{T})$ there exists exactly one
accepting run in $\mathcal{T}$ whose input is $u$ and output is $v$. Allauzen
et al. (2011) have shown that it is undecidable whether a transducer is
unambiguous. As a direct consequence we obtain that

######  Lemma 39.

It is undecidable whether a given regular language
$S\subseteq(\Sigma\cup\Gamma)^{*}$ is unambiguous.

However, unambiguity becomes decidable for regular synchronization languages
with finite shiftlag. Allauzen et al. (2011) have shown that it is decidable
whether a transducer with finite lag is unambiguous which yields that it is
decidable whether a regular synchronization language with finite lag is
unambiguous. We slightly generalize this.

######  Lemma 40.

It is decidable whether a given regular language
$S\subseteq(\Sigma\cup\Gamma)^{*}$ with finite shiftlag is unambiguous.

###### Proof.

Let $\mathcal{A}$ be a DFA for $S$. We consider an automatic relation over the
input and output alphabets $\Sigma\times Q_{\mathcal{A}}$ and $\Gamma\times
Q_{\mathcal{A}}$, respectively. This relation is defined by the regular
synchronization language $S^{\prime}\subseteq((\Sigma\cup\Gamma)\times
Q_{\mathcal{A}})^{*}$ with finite shiftlag as

$\displaystyle
S^{\prime}:=\\{(a_{1},q_{0})(a_{2},q_{1})\dots(a_{n},q_{n-1})\mid$
$\displaystyle\ a_{1}\dots a_{n}\in L(\mathcal{A})\text{ and }$
$\displaystyle\ q_{0}\cdots q_{n-1}\delta_{\mathcal{A}}(q_{n-1},a_{n})\text{
is the run of $\mathcal{A}$ on }a_{1}\dots a_{n}\\}.$

Let $S^{\prime\prime}\subseteq((\Sigma\times Q_{\mathcal{A}})(\Gamma\times
Q_{\mathcal{A}}))^{*}((\Sigma\times Q_{\mathcal{A}})^{*}+(\Gamma\times
Q_{\mathcal{A}})^{*})$ be the canonical representation of $S^{\prime}$. We
show that the regular language $S$ is unambiguous iff
$w_{1}=(\sigma_{1},r_{0})\dots(\sigma_{i},r_{i-1})$ and
$w_{2}=(\bar{\sigma}_{1},s_{0})\dots(\bar{\sigma}_{j},s_{j-1})$ with
$\sigma_{1}\cdots\sigma_{i}=\bar{\sigma}_{1}\cdots\bar{\sigma}_{j}$ implies
that $r_{0}\cdots r_{i-1}=s_{0}\cdots s_{j-1}$ for all $w_{1},w_{2}\in
S^{\prime\prime}$. This property can be checked given an NFA for
$S^{\prime\prime}$. If $S^{\prime\prime}$ does not satisfy the property one
can guess letter-by-letter some word $u$ over $\Sigma\cup\Gamma$ and two
different words $v,v^{\prime}$ over $Q_{\mathcal{A}}$ and check that $u\otimes
v\in S^{\prime\prime}$ and $u\otimes v^{\prime}\in S^{\prime\prime}$ using an
NFA for $S^{\prime\prime}$.

If $S$ is unambiguous, then
$w_{1}=(\sigma_{1},r_{0})\dots(\sigma_{i},r_{i-1})$ and
$w_{2}=(\bar{\sigma}_{1},s_{0})\dots(\bar{\sigma}_{j},s_{j-1})$ with
$\sigma_{1}\cdots\sigma_{i}=\bar{\sigma}_{1}\cdots\bar{\sigma}_{j}$ implies
that $r_{0}\cdots r_{i-1}=s_{0}\cdots s_{j-1}$ for all $w_{1},w_{2}\in
S^{\prime\prime}$ since the automaton $\mathcal{A}$ is deterministic.

For the other direction, we show that if $S$ is not unambiguous, then there
exist $w_{1},w_{2}\in S^{\prime\prime}$ with
$w_{1}=(\sigma_{1},r_{0})\dots(\sigma_{i},r_{i-1})$ and
$w_{2}=(\bar{\sigma}_{1},s_{0})\dots(\bar{\sigma}_{j},s_{j-1})$ such that
$\sigma_{1}\cdots\sigma_{i}=\bar{\sigma}_{1}\cdots\bar{\sigma}_{j}$ and
$r_{0}\cdots r_{i-1}\neq s_{0}\cdots s_{j-1}$. Assume that $S$ is not
unambiguous, then there are $x,y\in S$ with $x\neq y$ and $\llbracket
x\rrbracket=\llbracket y\rrbracket$, that is, two different synchronizations
describe the same pair. Let $w_{1},w_{2}\in S^{\prime\prime}$ with
$w_{1}=(\sigma_{1},r_{0})\dots(\sigma_{n},r_{n-1})$ and
$w_{2}=(\bar{\sigma}_{1},s_{0})\dots(\bar{\sigma}_{n},s_{n-1})$ denote their
respective representations. Since $x$ and $y$ encode the same pair, it is easy
to see that
$\sigma_{1}\cdots\sigma_{n}=\bar{\sigma}_{1}\cdots\bar{\sigma}_{n}$. We show
that $x\neq y$ implies $r_{0}\cdots r_{n-1}\neq s_{0}\cdots s_{n-1}$.

Towards a contradiction, assume that $r_{0}\cdots r_{n-1}=s_{0}\cdots s_{n-1}$
which implies that $w_{1}=w_{2}$. Let
$(p_{0},a_{1},p_{1})(p_{1},a_{2},p_{2})\cdots(p_{n-1},a_{n},p_{n})$ be the run
of $\mathcal{A}$ on $x$ and
$(q_{0},b_{1},q_{1})(q_{1},b_{2},q_{2})\cdots(q_{n-1},b_{n},q_{n})$ be the run
of $\mathcal{A}$ on $y$. Pick the first $i$ such that $a_{i}\neq b_{i}$,
without loss of generalization, assume that $a_{i}\in\Sigma$ and
$b_{i}\in\Gamma$. Let $j$ be the smallest $j>i$ such that $j$ is a shift of
$x$. Let $u=a_{i}\cdots a_{j}$, clearly, $u\in\Sigma^{*}$. Analogously, let
$k$ be the smallest $k>i$ such that $k$ is a shift of $y$. Let $v=b_{i}\cdots
b_{k}$, clearly, $v\in\Gamma^{*}$. Note that this implies that $a_{j+1}=b_{i}$
and $b_{k+1}=a_{i}$. Furthermore, since $w_{1}=w_{2}$, this also implies that
$p_{i-1}=q_{k}$ and $q_{i-1}=p_{j}$. Moreover, since $a_{1}\cdots
a_{i-1}=b_{1}\cdots b_{i-1}$, we have that
$\delta_{\mathcal{A}}(p_{0},a_{1}\cdots
a_{i-1})=p_{i-1}=q_{i-1}=\delta_{\mathcal{A}}(q_{0},b_{1}\cdots b_{i-1})$.
Thus, we can conclude that $p_{i-1}=q_{i-1}=q_{k}=p_{j}$. Since
$\delta_{\mathcal{A}}(p_{i-1},u)=p_{j}$ and
$\delta_{\mathcal{A}}(q_{i-1},v)=q_{k}$, we obtain that $a_{1}\cdots
a_{i-1}(u+v)^{*}a_{j+1}\cdots a_{n}\subseteq S$. Clearly, this subset does not
have finite shiftlag, thus, $S$ does not have finite shiftlag, which is a
contradiction. ∎

Using the results from the previous section we obtain that

######  Theorem 41.

The resynchronized definability problem is decidable for source languages with
finite shiftlag and unambiguous target language with finite shiftlag.

###### Proof.

Let $S,T\in\textsc{Reg}_{\mathsf{FSL}}$ and let $T$ be unambiguous. Our goal
is to decide whether $\llbracket S\rrbracket\in\textsc{Rel}(T)$, i.e., whether
there is a regular language $U\subseteq T$ such that $\llbracket
U\rrbracket=\llbracket S\rrbracket$. Assume, such a $U$ exists, then
$U=\mathit{minsync}(S,T)=\mathit{maxsync}(S,T)=\mathit{allsync}(S,T)$, because
$T$ is unambiguous. Thus, $\llbracket S\rrbracket\in\textsc{Rel}(T)$ iff
$\mathit{minsync}(S,T)$ is regular and $\llbracket
S\rrbracket=\llbracket\mathit{minsync}(S,T)\rrbracket$. The first condition is
decidable according to Lemma 31, the second condition is decidable because
$S,T\in\textsc{Reg}_{\mathsf{FSL}}$. ∎

####  4.2.3 Prefix-recognizable targets

In this section we describe a class of target synchronization languages $T$
that have the property that $\mathit{maxsync}(T,T)$ is regular. According to
Theorem 36, the resynchronized definability problem is decidable for such
targets (and source languages $S$ of finite shiftlag).

Based on that we then give an alternative proof for decidability of the
problem whether a given (binary) automatic relation is prefix-recognizable
(the decidability of this problem has already been shown by Choffrut (2014)
for relations of arbitrary arity).

A set $U\subseteq(\Sigma\Gamma)^{*}$ is called _$(\Sigma\Gamma)^{*}$ -prefix
closed_ if $uab\in U$ implies $u\in U$ for all $u\in(\Sigma\Gamma)^{*}$ and
all $a\in\Sigma$, $b\in\Gamma$.

The class of target languages that we consider contains the synchronization
languages that are of the form $T=U\Sigma^{*}\Gamma^{*}$ for a regular
$(\Sigma\Gamma)^{*}$-prefix closed set $U$.

######  Lemma 42.

Let $T=U\Sigma^{*}\Gamma^{*}$ for a regular $(\Sigma\Gamma)^{*}$-prefix closed
set $U$. Then $\mathit{maxsync}(T,T)$ is regular.

###### Proof.

Let $w\in T$. Then $w=uxy$ with $u\in U$, $x\in\Sigma^{*}$, and
$y\in\Gamma^{*}$. Because $U$ is $(\Sigma\Gamma)^{*}$-prefix closed, we have
that $w\in\mathit{maxsync}(T,T)$ iff

  * •

$x=\varepsilon$, or $y=\varepsilon$, or

  * •

$x=ax^{\prime}$, $y=by^{\prime}$, and $uab\notin U$.

An automaton that accepts the words $w$ with this property can easily be built
from an automaton for $U$. ∎

A direct consequence of Lemma 42 and Theorem 36 is:

######  Theorem 43.

The resynchronized definability problem is decidable for given
$S,T\in\textsc{Reg}_{\mathsf{FSL}}$ where $T=U\Sigma^{*}\Gamma^{*}$ for a
regular $(\Sigma\Gamma)^{*}$-prefix closed set $U$.

We now turn to prefix-recognizable relations. The standard definition of this
class of relations uses a single alphabet $A$ as input and output alphabet. A
relation over $A^{*}\times A^{*}$ is called _prefix-recognizable_ if it can be
written in the form

$\bigcup_{i=1}^{n}U_{i}(V_{i}\times W_{i}):=\\{(uv,uw)\mid\text{$u\in U_{i}$,
$v\in V_{i}$, and $w\in W_{i}$}\\},$

for regular languages $U_{i},V_{i},W_{i}\subseteq A^{*}$ for each $i$.

A simple example of a prefix-recognizable relation is the lexicographical
ordering on words over an ordered alphabet.

Prefix-recognizable relations where first studied by Angluin and Hoover (1984)
and Läuchli and Savioz (1987). The class of prefix-recognizable relations is a
natural class that enjoys many nice properties. An overview over these
properties (for prefix-recognizable graphs) is given by (Blumensath, 2001,
Theorem 1). Furthermore, the graphs of prefix-recognizable relations have a
decidable MSO theory which was shown by Caucal (2003).

In order to capture prefix-recognizable relations in our setting, we we make
the input and output alphabets disjoint by annotating input letters by $1$ and
output letters by $2$, that is, $\Sigma=\\{1\\}\times A$ and
$\Gamma=\\{2\\}\times A$. And we say that a relation over
$\Sigma^{*}\times\Gamma^{*}$ is prefix-recognizable if the relation over
$A^{*}\times A^{*}$ that is obtained by removing the annotations $1$ and $2$
is prefix-recognizable.

Let $\mathit{Id_{A}}=\\{(1,a)(2,a)\mid a\in
A\\}^{*}\subseteq(\Sigma\Gamma)^{*}$. Then it is not hard to see that the
prefix-recognizable relations are precisely those that can be defined by
regular subsets of $T_{\mathit{pr}}:=\mathit{Id_{A}}\Sigma^{*}\Gamma^{*}$.

######  Remark 44.

A relation over $\Sigma^{*}\times\Gamma^{*}$ is prefix recognizable iff it is
in $\textsc{Rel}(T_{\mathit{pr}})$.

Since $\mathit{Id_{A}}$ is $(\Sigma\Gamma)^{*}$-prefix closed, we obtain the
following corollary of Theorem 43: