Université libre de Bruxelles, Belgium and
http://www.sarahwinter.nethttps://orcid.org/0000-0002-3499-1995 S. Winter
[500]Theory of computation Logic and verification [500]Theory of computation
Transducers This research was supported by the DFG grant LO 1174/3.

###### Acknowledgements.

The author wants to thank Emmanuel Filiot for valuable feedback on the
presentation.John Q. Open and Joan R. Access 2 42 23

# Decision problems for origin-close top-down tree transducers (full version)

Sarah Winter

###### Abstract

Tree transductions are binary relations of finite trees. For tree
transductions defined by non-deterministic top-down tree transducers,
inclusion, equivalence and synthesis problems are known to be undecidable.
Adding origin semantics to tree transductions, i.e., tagging each output node
with the input node it originates from, is a known way to recover decidability
for inclusion and equivalence. The origin semantics is rather rigid, in this
work, we introduce a similarity measure for transducers with origin semantics
and show that we can decide inclusion, equivalence and synthesis problems for
origin-close non-deterministic top-down tree transducers.

###### keywords:

tree tranducers, equivalence, uniformization, synthesis, origin semantics

###### category:

##  1 Introduction

In this paper we study decision problems for top-down tree transducers over
finite trees with origin semantics. Rounds [30] and Thatcher [31]
independently invented tree transducers (their model is known today as top-
down tree transducer) as a generalization of finite state word transducers in
the context of natural language processing and compilers in the beginning of
the 1970s. Nowadays, there is a rich landscape of various tree transducer
models used in many fields, for example, syntax-directed translation [18],
databases [29, 20], linguistics [27, 5], programming languages [33, 28], and
security analysis [23].

Unlike tree automata, tree transducers have undecidable inclusion and
equivalence problems [13]. This is already the case for word transducers [19,
17]. The intractability of, e.g., the equivalence problem for transducers
(whether two given transducers recognize the same transduction, that is, the
same relation) mainly stems from the fact that two transducers recognizing the
same transduction may produce their outputs very differently. One transducer
may produce its output fast and be ahead of the other. In general, there is an
infinite number of transducers for a single transduction. To overcome this
difficulty Bojanczyk [1] has introduced origin semantics, that is,
additionally, there is an origin function that maps output positions to their
originating input positions. The main result of [1] is a machine-independent
characterization of transductions defined by deterministic two-way transducers
with origin semantics. Word transducers with origin semantics where further
investigated in [2], and properties of subclasses of transductions with origin
semantics definable by one-way word transducers have been studied in [14, 9].
Under origin semantics, many interesting problems become decidable, e.g.,
equivalence of one-way word transducers. This is not surprising as a
transduction now incorporates _how_ it translates an input word into an output
word providing much more information.

In [16], the authors have initiated a study of several decision problems for
different tree transducer models on finite trees with origin semantics. More
concretely, they studied inclusion, equivalence, injectivity and query
determinacy problems for top-down tree transducers, tree transducers definable
in monadic second order logic, and top-down tree-to-word transducers. They
showed (amongst other results) that inclusion and equivalence become decidable
for all models except tree-to-string transducers with origin semantics.

In general, there has been an interest to incorporate some kind of origin
information (i.e., _how_ a transduction works) into tree transductions, in
order to gain more insight on different tree transductions, see, e.g., [32,
11, 26].

However, the origin semantics is rather rigid. To mitigate this, in [15], the
authors have introduced a similarity measure between (one-way) word
transducers with origin semantics which amounts to a measure that compares the
difference between produced outputs on the same input prefix, in short, the
measure compares their output delays. They show that inclusion, equivalence,
and sequential uniformization (see next paragraph) problems become decidable
for transducers that have bounded output delay. These problem are undecidable
for word transducers in general, see [19, 17, 7]. The introduction of this
similarity measure has triggered similar works on two-way word transducers,
see [4, 3].

In order to obtain decidability results (in a less rigid setting than origin
semantics), we initiate the study of inclusion, equivalence, and
uniformization problems for top-down tree transducers under similarity
measures which are based on the behavior of the transducers.

A uniformization of a binary relation is a function that selects for each
element of the domain of the relation an element in its image. Synthesis
problems are closely related to _effective_ uniformization problems;
algorithmic synthesis of specifications (i.e., relations) asks for effective
uniformization by functions that can be implemented in a specific way. The
classical setting is Church’s synthesis problem [8], where logical
specifications over infinite words are considered. Büchi and Landweber [6]
showed that for specifications in monadic second order logic, that is,
specifications that can be translated into synchronous finite automata, it is
decidable whether they can be realized by a synchronous sequential transducer.
Later, decidability has been extended to asynchronous sequential transducers
[22, 21]. Detailed studies of the synthesis of sequential transducers from
synchronous and asynchronous finite automata on finite words are provided in
[15, 34], for an overview see [7].

Uniformization questions in this spirit have been first studied for relations
over finite trees in [25, 24]. The authors have considered tree-automatic
relations, that is, relations definable by tree automata over a product
alphabet. They have shown that for tree-automatic relations definable by
deterministic top-down tree automata uniformization by deterministic top-down
tree transducers (which are a natural extension of sequential transducer on
words) is decidable. However, for non-deterministic top-down tree automata it
becomes undecidable.

Our contribution is the introduction of two similarity measures for top-down
tree transducers. The first measure is an extension of the output delay
measure introduced for word transducers in [15] to tree transducers. Comparing
top-down tree transducers based on their output delay has also been done in
e.g., [12], we use the same notion of delay to define our measure.
Unfortunately, while decidability for major decision problems is regained in
the setting of word transducers, we show that it is not in the setting of tree
transducers. The second similarity measure is more closely connected to the
origin semantics. We define two transducers as origin-close if there is a
bound on the distance of two positions which are origins of the same output
node by the two transducers. Our main result is that inclusion, equivalence
and uniformization by deterministic top-down tree transducers is decidable for
origin-close top-down tree transducers.

The paper is structured as follows. In Section 2 we provide definitions and
terminology used throughout the paper. In Section 3 we present two similarity
measures for (top-down tree) transducers and provide a comparison of their
expressiveness, and in Section 4 we consider decision problems for origin-
close top-down tree transducers.

##  2 Preliminaries

###### Words, trees, and contexts.

An _alphabet_ $\Sigma$ is a finite non-empty set of _letters_ or _symbols_. A
finite _word_ is a finite sequence of letters. The set of all finite words
over $\Sigma$ is denoted by $\Sigma^{*}$. The length of a word
$w\in\Sigma^{*}$ is denoted by $|w|$, the empty word is denoted by
$\varepsilon$. We write $u\sqsubseteq w$ if there is some $v$ such that $w=uv$
for $u,v\in\Sigma^{*}$. A subset $L\subseteq\Sigma^{*}$ is called _language_
over $\Sigma$. A _ranked alphabet_ $\Sigma$ is an alphabet where each letter
$f\in\Sigma$ has a rank $rk(f)\in\mathbbm{N}$. The set of letters of rank $i$
is denoted by $\Sigma_{i}$. A tree domain $\mathit{dom}$ is a non-empty finite
subset of $(\mathbbm{N}\setminus\\{0\\})^{*}$ such that $\mathit{dom}$ is
prefix-closed and for each $u\in(\mathbbm{N}\setminus\\{0\\})^{*}$ and
$i\in\mathbbm{N}\setminus\\{0\\}$ if $ui\in\mathit{dom}$, then
$uj\in\mathit{dom}$ for all $1\leq j<i$. We speak of $ui$ as successor of $u$
for each $u\in\mathit{dom}$ and $i\in\mathbbm{N}\setminus\\{0\\}$, and the
$\sqsubseteq$-maximal elements of $\mathit{dom}$ are called _leaves_.

A (finite $\Sigma$-labeled) _tree_ is a mapping
$t:\mathit{dom}_{t}\rightarrow\Sigma$ such that for each node
$u\in\mathit{dom}_{t}$ the number of successors of $u$ is a rank of $t(u)$.
The height $h$ of a tree $t$ is the length of its longest path, i.e.,
$h(t)=max\\{|u|\mid u\in\mathit{dom}_{t}\\}$. The set of all $\Sigma$-labeled
trees is denoted by $T_{\Sigma}$. A subset $T\subseteq T_{\Sigma}$ is called
_tree language_ over $\Sigma$.

A _subtree_ $t|_{u}$ of a tree $t$ at node $u$ is defined by
$\mathit{dom}_{t|_{u}}=\\{v\in\mathbbm{N}^{*}\mid uv\in\mathit{dom}_{t}\\}$
and $t|_{u}(v)=t(uv)$ for all $v\in\mathit{dom}_{t|_{u}}$. In order to
formalize concatenation of trees, we introduce the notion of special trees. A
_special tree_ over $\Sigma$ is a tree over
$\Sigma\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\\{\circ\\}$
such that $\circ$ has rank zero and occurs exactly once at a leaf. Given $t\in
T_{\Sigma}$ and $u\in\mathit{dom}_{t}$, we write $t[\circ/u]$ for the special
tree that is obtained by deleting the subtree at $u$ and replacing it by
$\circ$. Let $S_{\Sigma}$ be the set of special trees over $\Sigma$. For $t\in
S_{\Sigma}$ and $s\in T_{\Sigma}$ or $s\in S_{\Sigma}$ let the _concatenation_
$t\cdot s$ be the tree that is obtained from $t$ by replacing $\circ$ with
$s$.

Let $X_{n}$ be a set of $n$ variables $\\{x_{1},\dots,x_{n}\\}$ and $\Sigma$
be a ranked alphabet. We denote by $T_{\Sigma}(X_{n})$ the set of all trees
over $\Sigma$ which additionally can have variables from $X_{n}$ at their
leaves. We define $X_{0}$ to be the empty set, the set $T_{\Sigma}(\emptyset)$
is equal to $T_{\Sigma}$. Let $X=\bigcup_{n>0}X_{n}$. A tree from
$T_{\Sigma}(X)$ is called _linear_ if each variable occurs at most once. For
$t\in T_{\Sigma}(X_{n})$ let $t[x_{1}\leftarrow t_{1},\dots,x_{n}\leftarrow
t_{n}]$ be the tree that is obtained by substituting each occurrence of
$x_{i}\in X_{n}$ by $t_{i}\in T_{\Sigma}(X)$ for every $1\leq i\leq n$.

A tree from $T_{\Sigma}(X_{n})$ such that all variables from $X_{n}$ occur
exactly once and in the order $x_{1},\dots,x_{n}$ when reading the leaf nodes
from left to right, is called $n$-_context_ over $\Sigma$. Given an
$n$-context, the node labeled by $x_{i}$ is referred to as $i$th hole for
every $1\leq i\leq n$. A special tree can be seen as a $1$-context, a tree
without variables can be seen a $0$-context. If $C$ is an $n$-context and
$t_{1},\dots,t_{n}\in T_{\Sigma}(X)$ we write $C[t_{1},\dots,t_{n}]$ instead
of $C[x_{1}\leftarrow t_{1},\dots,x_{n}\leftarrow t_{n}]$.

###### Tree transductions, origin mappings, and uniformizations.

Let $\Sigma,\Gamma$ be ranked alphabets. A _tree transduction (from
$T_{\Sigma}$ to $T_{\Gamma}$)_ is a relation $R\subseteq T_{\Sigma}\times
T_{\Gamma}$. Its _domain_ , denoted $\mathrm{dom}(R)$, is the projection of
$R$ on its first component. Given trees $t_{1},t_{2}$, an _origin mapping_ of
$t_{2}$ in $t_{1}$ is a function
$o\colon\mathit{dom}_{t_{2}}\to\mathit{dom}_{t_{1}}$. Given
$v\in\mathit{dom}_{t_{2}}$, $u\in\mathit{dom}_{t_{1}}$, we say $v$ has origin
$u$ if $o(v)=u$. Examples are depicted in Figures 1(g) and 2. A
_uniformization_ of a tree transduction $R\subseteq T_{\Sigma}\times
T_{\Gamma}$ is a function $f\colon\mathrm{dom}(R)\to T_{\Gamma}$ such that
$(t,f(t))\in R$ for all $t\in\mathrm{dom}(R)$.

###### Top-down tree transducers.

We consider top-down tree transducers, which read the tree from the root to
the leaves in a parallel fashion and produce finite output trees in each step
that are attached to the already produced output.

A _top-down tree transducer_ (a tdtt) is of the form
$\mathcal{T}=(Q,\Sigma,\Gamma,q_{0},\Delta)$ consisting of a finite set of
states $Q$, a finite input alphabet $\Sigma$, a finite output alphabet
$\Gamma$, an initial state $q_{0}\in Q$, and $\Delta$ is a finite set of
transition rules of the form

$q(f(x_{1},\dots,x_{i}))\rightarrow
w[q_{1}(x_{j_{1}}),\dots,q_{n}(x_{j_{n}})],$

where $f\in\Sigma_{i}$, $w$ is an $n$-context over $\Gamma$,
$q,q_{1},\dots,q_{n}\in Q$ and variables $x_{j_{1}},\dots,x_{j_{n}}\in X_{i}$.
A _deterministic_ tdtt (a dtdtt) has no two rules with the same left-hand
side.

We now introduce a non-standard notion of configurations which is more
suitable to prove our results. Usually, a configuration is a partially
transformed input tree; the upper part is the already produced output, the
lower parts are remainders of the input tree. Here, we keep the input and
output tree separate and introduce a mapping from nodes of the output tree to
nodes of the input tree from where the transducer continues to read. A
visualization of several configurations is given in Figure 1.

A _configuration_ of a top-down tree transducer is a triple
$c=(t,t^{\prime},\varphi)$ of an input tree $t\in T_{\Sigma}$, an output tree
$t^{\prime}\in T_{\Gamma\cup Q}$ and a function
$\varphi:D_{t^{\prime}}\rightarrow\mathit{dom}_{t}$, where

  * •

$t^{\prime}(u)\in\Gamma_{i}$ for each $u\in\mathit{dom}_{t^{\prime}}$ with
$i>0$ successors, and

  * •

$t^{\prime}(u)\in\Gamma_{0}$ or $t^{\prime}(u)\in Q$ for each leaf
$u\in\mathit{dom}_{t^{\prime}}$, and

  * •

$D_{t^{\prime}}\subseteq\mathit{dom}_{t^{\prime}}$ with
$D_{t^{\prime}}=\\{u\in\mathit{dom}_{t^{\prime}}\mid t^{\prime}(u)\in Q\\}$,
i.e., $\varphi$ maps every node from the output tree $t^{\prime}$ that has a
state-label to a node of the input tree $t$.

Let $c_{1}=(t,t_{1},\varphi_{1})$ and $c_{2}=(t,t_{2},\varphi_{2})$ be
configurations of a top-down tree transducer over the same input tree. We
define a _successor relation_ $\rightarrow_{\mathcal{T}}$ on configurations as
usual by applying one rule. Figure 1 illustrates a configuration sequence
explained in Example 2.1 below. Formally, for the application of a rule, we
define $c_{1}\rightarrow_{\mathcal{T}}c_{2}:\Leftrightarrow$

  * •

There is a state-labeled node $u\in D_{t^{\prime}}$ of the output tree $t_{1}$
that is mapped to a node $v\in\mathit{dom}_{t}$ of the input tree $t$, i.e.,
$\varphi_{1}(u)=v$, and

  * •

there is a rule $t_{1}(u)\left(t(v)(x_{1},\dots,x_{i})\right)\rightarrow
w[q_{1}(x_{j_{1}}),\dots,q_{n}(x_{j_{n}})]\in\Delta$ such that the output tree
is correctly updated, i.e., $t_{2}=t_{1}[\circ/u]\cdot w[q_{1},\dots,q_{n}]$,
and

  * •

the mapping $\varphi_{2}$ is correctly updated, i.e.,
$\varphi_{2}(u^{\prime})=\varphi_{1}(u^{\prime})$ if $u^{\prime}\in
D_{t_{1}}\setminus\\{u\\}$ and $\varphi_{2}(u^{\prime})=v.j_{i}$ if
$u^{\prime}=u.u_{i}$ with $u_{i}$ is the $i$th hole in $w$.

Furthermore, let $\rightarrow_{\mathcal{T}}^{*}$ be the reflexive and
transitive closure of $\rightarrow_{\mathcal{T}}$. From here on, let
$\varphi_{0}$ always denote the mapping
$\varphi_{0}(\varepsilon)=\varepsilon$. A configuration
$(t,q_{0},\varphi_{0})$ is called _initial configuration_ of $\mathcal{T}$ on
$t$. A configuration sequence starting with an initial configuration where
each configuration is a successor of the previous one is called a _run_. For a
tree $t\in T_{\Sigma}$ let $\mathcal{T}(t)\subseteq T_{\Gamma\cup Q}$ be the
set of _final transformed outputs_ of a computation of $\mathcal{T}$ on $t$,
that is the set
$\\{t^{\prime}\mid(t,q_{0},\varphi_{0})\rightarrow_{\mathcal{T}}^{*}(t,t^{\prime},\varphi)\text{
s.t.\ there is no successor configuration of }(t,t^{\prime},\varphi)\\}.$
Note, we explicitly do not require that the final transformed output is a tree
over $\Gamma$. In the special case that $\mathcal{T}(t)$ is a singleton set
$\\{t^{\prime}\\}$, we also write $\mathcal{T}(t)=t^{\prime}$. The
_transduction_ $R(\mathcal{T})$ induced by a tdtt $\mathcal{T}$ is
$R(\mathcal{T})=\\{(t,t^{\prime})\mid t^{\prime}\in\mathcal{T}(t)\cap
T_{\Gamma}\\}.$ The class of relations definable by tdtts is called the class
of _top-down tree transductions_ , conveniently denoted by tdtt.

Let $\mathcal{T}$ be a tdtt, and let $\rho=c_{0}\dots c_{n}$ be a run of
$\mathcal{T}$ on an input tree $t\in T_{\Sigma}$ that results in an output
tree $s\in T_{\Gamma}$. The _origin function $o$_ of $\rho$ maps a node $u$ of
the output tree to the node $v$ of the input tree that was read while
producing $u$, formally $o:\mathit{dom}_{s}\rightarrow\mathit{dom}_{t}$ with
$o(u)=v$ if there is some $i$, such that $c_{i}=(t,t_{i},\varphi_{i})$,
$c_{i+1}=(t,t_{i+1},\varphi_{i+1})$ and $\varphi_{i}(u)=v$ and
$t_{i+1}(u)=s(u)$, see Figure 1. We define $R_{o}(\mathcal{T})$ to be the set

$\\{(t,s,o)\mid t\in T_{\Sigma},s\in T_{\Gamma}\text{ and
}\exists\thinspace\rho:(t,q_{0},\varphi)\rightarrow_{\mathcal{T}}^{*}(t,s,\varphi^{\prime})\text{
with origin }o\\}.$

######  Example 2.1.

Let $\Sigma$ be a ranked alphabet given by $\Sigma_{2}=\\{f\\}$,
$\Sigma_{1}=\\{g,h\\}$, and $\Sigma_{0}=\\{a\\}$. Consider the tdtt
$\mathcal{T}$ given by $(\\{q\\},\Sigma,\Sigma,\\{q\\},\Delta)$ with $\Delta$
$=$ $\\{$ $q(a)\rightarrow a$, $q(g(x_{1}))\rightarrow q(x_{1})$,
$q(h(x_{1}))\rightarrow h(q(x_{1}))$, $q(f(x_{1},x_{2}))\rightarrow
f(q(x_{1}),q(x_{2}))$ $\\}$. For each $t\in T_{\Sigma}$ the transducer deletes
all occurrences of $g$ in $t$. Consider $t:=f(g(h(a)),a)$. A possible sequence
of configurations of $\mathcal{T}$ on $t$ is
$c_{0}\rightarrow_{\mathcal{T}}^{5}c_{5}$ such that $c_{0}:=(t,q,\varphi_{0})$
with $\varphi_{0}(\varepsilon)=\varepsilon$, $c_{1}:=(t,f(q,q),\varphi_{1})$
with $\varphi_{1}(1)=1$, $\varphi_{1}(2)=2$, $c_{2}:=(t,f(q,q),\varphi_{2})$
with $\varphi_{2}(1)=11$, $\varphi_{2}(2)=2$, $c_{3}:=(t,f(q,a),\varphi_{3})$
with $\varphi_{3}(1)=11$, $c_{4}:=(t,f(h(q),a),\varphi_{4})$ with
$\varphi_{4}(11)=111$, and $c_{5}:=(t,f(h(a),a),\varphi_{5})$. A visualization
of this sequence and resulting origin mapping is shown in Figure 1.

$f$$g$$h$$a$$a$$q$$\varphi_{0}$ (a) $c_{0}$

$f$$g$$h$$a$$a$$f$$q$$q$$\varphi_{1}$$\varphi_{1}$ (b) $c_{1}$

$f$$g$$h$$a$$a$$f$$q$$q$$\varphi_{2}$$\varphi_{2}$ (c) $c_{2}$

$f$$g$$h$$a$$a$$f$$q$$a$$\varphi_{3}$ (d) $c_{3}$

$f$$g$$h$$a$$a$$f$$h$$q$$a$$\varphi_{4}$ (e) $c_{4}$

$f$$g$$h$$a$$a$$f$$h$$a$$a$ (f) $c_{5}$

$f$$g$$h$$a$$a$$f$$h$$a$$a$ (g) origin mapping

Figure 1: The configuration sequence $c_{0}$ to $c_{5}$ of $\mathcal{T}$ on
$f(g(h(a)),a)$ and resulting origin mapping from Example 2.1.

######  Example 2.2.

Let $\Sigma,\Gamma$ be given by $\Sigma_{2}=\\{f\\}$, $\Sigma_{0}=\\{a\\}$,
$\Gamma_{1}=\\{h\\}$, and $\Gamma_{0}=\\{b\\}$. Consider the tdtt
$\mathcal{T}$ given by $(\\{q\\},\Sigma,\Gamma,\\{q\\},\Delta)$ with $\Delta$
$=$ $\\{$ $q(a)\rightarrow b$, $q(f(x_{1},x_{2}))\rightarrow h(q(x_{1}))$,
$q(f(x_{1},x_{2}))\rightarrow h(q(x_{2}))$ $\\}$. Basically, when reading an
$f$-labeled node, the tdtt can non-deterministically decide whether to
continue reading in left or the right subtree. In Figure 2 two origin mappings
$o\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$ and
$o^{\prime}\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$ are given that are
result of runs of $\mathcal{T}$ on $t=f(f(f(a,a),a),a),f(f(a,a),a),a))$ with
final output $s=h(h(h(b)))$.

$f$$f$$f$$a$$a$$a$$f$$f$$a$$a$$a$$h$$h$$h$$b$ (a)
$o\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$

$f$$f$$f$$a$$a$$a$$f$$f$$a$$a$$a$$h$$h$$h$$b$ (b)
$o^{\prime}\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$

Figure 2: Origin mappings $o,o^{\prime}$. We have that
$\mathit{dist}(o(111),o^{\prime}(111))$, that is, the distance of the origins
of the leaf node, is the length of the shortest path from node $111$ to node
$211$ which is $6$.

In this work, we focus on decision problems for transducers with origin
semantics. To begin with, we introduce some notations and state relevant known
results in this context.

###### Shorthand notations.

Let $\mathcal{C}$ denote a class of transducers with origin semantics, e.g.,
tdtt or dtdtt. Given a class $\mathcal{C}$ and
$\mathcal{T}_{1},\mathcal{T}_{2}\in\mathcal{C}$, if
$R(\mathcal{T}_{1})\subseteq R(\mathcal{T}_{2})$ (resp.
$R_{o}(\mathcal{T}_{1})\subseteq R_{o}(\mathcal{T}_{2})$), we write
$\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$ (resp.
$\mathcal{T}_{1}\subseteq_{o}\mathcal{T}_{2}$). Furthermore, if
$R(\mathcal{T}_{1})=R(\mathcal{T}_{2})$ (resp.
$R_{o}(\mathcal{T}_{1})=R_{o}(\mathcal{T}_{2})$), we write
$\mathcal{T}_{1}=\mathcal{T}_{2}$ (resp.
$\mathcal{T}_{1}=_{o}\mathcal{T}_{2}$). Given classes
$\mathcal{C}_{1},\mathcal{C}_{2}$, $\mathcal{T}_{1}\in\mathcal{C}_{1}$, and
$\mathcal{T}_{2}\in\mathcal{C}_{2}$, if $\mathcal{T}_{1}$ defines a function
$f$ that is a uniformization of $R(\mathcal{T}_{2})$, we say $\mathcal{T}_{1}$
uniformizes $\mathcal{T}_{2}$, if additionally
$\mathcal{T}_{1}\subseteq_{o}\mathcal{T}_{2}$, we say $\mathcal{T}_{1}$ origin
uniformizes $\mathcal{T}_{2}$.

###### Decision problems.

The _inclusion_ resp.  _origin inclusion problem_ for a class $\mathcal{C}$
asks, given $\mathcal{T}_{1},\mathcal{T}_{2}\in\mathcal{C}$, whether
$\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$ resp.
$\mathcal{T}_{1}\subseteq_{o}\mathcal{T}_{2}$. The _equivalence_ resp.
_origin equivalence problem_ for a class $\mathcal{C}$ asks, given
$\mathcal{T}_{1},\mathcal{T}_{2}\in\mathcal{C}$, whether
$\mathcal{T}_{1}=\mathcal{T}_{2}$ resp. $\mathcal{T}_{1}=_{o}\mathcal{T}_{2}$.
Lastly, the _uniformization_ resp.  _origin uniformization problem_ for
classes $\mathcal{C}_{1},\mathcal{C}_{2}$ asks, given
$\mathcal{T}_{2}\in\mathcal{C}_{2}$, whether there exists
$\mathcal{T}_{1}\in\mathcal{C}_{1}$ such that $\mathcal{T}_{1}$ uniformizes
(resp. origin uniformizes) $\mathcal{T}_{2}$.

As mentioned in the introduction, generally, a transduction can be defined by
several transducers behaving very differently, making many problems
intractable. Adding origin semantics to transducers, i.e., seeing the
transducer behavior as part of the transduction, allows to recover
decidability. The following is known for the class tdtt.

######  Theorem 2.3 ([13]).

Inclusion and equivalence are undecidable for the class tdtt.

######  Theorem 2.4 ([16]).

Origin inclusion and origin equivalence are decidable for the class tdtt.

Turning to uniformization problems, it is known that every tdtt is
uniformizable by a dtdtt with regular lookahead (a
$\textup{{dtdtt}}^{\textup{R}}$), that is, the transducer can check membership
of the subtrees of a node in regular tree-languages before processing the
node.

######  Theorem 2.5 ([10]).

Every tdtt has a $\textup{{dtdtt}}^{\textup{R}}$-uniformization.

However, when requiring that the input should be transformed on-the-fly
(without regular lookahead), the uniformization problem becomes undecidable.
In [7], it was shown that it is undecidable whether a one-way (non-
deterministic) word transducer has a uniformization by a sequential transducer
(that is, basically, a one-way deterministic transducer). So, we get
undecidability in the tree setting for free (as stated in Theorem 2.6). This
problem has not been investigated with origin semantics so far. We show
decidability (also for more relaxed versions), see Theorem 4.8.

######  Theorem 2.6.

dtdtt-uniformization is undecidable for the class tdtt.

Since the origin semantics is rather rigid, in the next section, we introduce
two similarity measures between transducers which are based on their behavior
and re-investigate the introduced decision problems for transducers with
‘similar’ behavior.

##  3 Similarity measures for transducers

An idea that naturally comes to mind is to say that two transducers behave
similarly if for two computations over the same input that yield the same
output their respective origin mappings are ‘similar’.

The other idea is to say that two computations are similar if their output
delay is small, roughly meaning that for the same prefix (for an adequate
notion of prefix for trees) of the input the so-far produced output is of
similar size. Decision problems using this measure have already been
investigated for (one-way) word transducers [15], we lift the measure to top-
down tree transducers.

###### Origin distance.

Given a tree $t$, let the distance between two nodes $u,v\in\mathit{dom}_{t}$,
written $\mathit{dist}(u,v)$, be the shortest path between $u$ and $v$
(ignoring the edge directions), an example is given in Figure 2.

Given $\mathcal{T},\mathcal{T}_{1},\mathcal{T}_{2}\in\mathcal{C}$, where
$\mathcal{C}$ is a class of transducers with origin semantics. We say
$(t,s,o)$ is _$k$ -origin included_ in $R_{o}(\mathcal{T})$, written
$(t,s,o)\in_{k}R_{o}(\mathcal{T})$, if there is $(t,s,o^{\prime})\in
R_{o}(\mathcal{T})$ such that $\mathit{dist}(o(i),o^{\prime}(i))\leq k$ for
all $i\in\mathit{dom}_{s}$. We say $\mathcal{T}_{1}$ is _$k$ -origin included_
in $\mathcal{T}_{2}$, written $\mathcal{T}_{1}\subseteq_{k}\mathcal{T}_{2}$,
if $(s,t,o)\in_{k}R_{o}(\mathcal{T}_{2})$ for all $(s,t,o)\in
R_{o}(\mathcal{T}_{1})$. We say $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are
_$k$ -origin equivalent_, written $\mathcal{T}_{1}=_{k}\mathcal{T}_{2}$, if
$\mathcal{T}_{1}\subseteq_{k}\mathcal{T}_{2}$ and
$\mathcal{T}_{2}\subseteq_{k}\mathcal{T}_{1}$. We say $\mathcal{T}_{1}$ _$k$
-origin uniformizes_ $\mathcal{T}_{2}$ if
$\mathcal{T}_{1}\subseteq_{k}\mathcal{T}_{2}$ and $\mathcal{T}_{1}$
uniformizes $\mathcal{T}_{2}$. The $k$-origin decision problems are defined as
expected.

We need some additional notations, before we can introduce the concept of
delay.

###### Partial and prefix trees.

Let $N_{\Sigma}$ be the set of all trees over $\Sigma$ which can have symbols
from $\Sigma$, that is, symbols with rank $\geq 0$, at their leaves. The set
$N_{\Sigma}$ is the set of all _partial trees_ over $\Sigma$. Note that
$N_{\Sigma}$ includes $T_{\Sigma}$. We say a tree $t^{\prime}\in N_{\Sigma}$
is a _prefix tree_ of a tree $t\in N_{\Sigma}$, written $t^{\prime}\sqsubseteq
t$, if $\mathit{dom}_{t^{\prime}}\subseteq\mathit{dom}_{t}$, and
$t^{\prime}(u)=t(u)\text{ for all }u\in\mathit{dom}_{t^{\prime}}.$ Given
$t_{1},t_{2}\in N_{\Sigma}$, its _greatest common prefix_ , written
$t_{1}\wedge t_{2}$, is the tree $t\in N_{\Sigma}$ such that
$\mathit{dom}_{t}$ is the largest subset of
$\mathit{dom}_{t_{1}}\cap\mathit{dom}_{t_{2}}$ such that $t\sqsubseteq t_{1}$
and $t\sqsubseteq t_{2}$. Removing $t_{1}\wedge t_{2}$ from $t_{1}$ and
$t_{2}$ naturally yields a set of partial trees (we omit a formal definition)
called _difference trees_. These notions are visualized in Figure 3.

###### Delay.

Given words $w_{1},w_{2}$, to compute their delay, we remove their greatest
common prefix $w=w_{1}\wedge w_{2}$, say $w_{1}=wv_{1}$ and $w_{2}=wv_{2}$,
and their delay is the maximum of the length of their respective reminders,
i.e., $\mathrm{max}\\{|v_{1}|,|v_{2}|\\}$. We lift this to trees, given
(partial) trees $t_{1},t_{2}$, we remove their greatest common prefix
$t_{1}\wedge t_{2}$ from $t_{1}$ and $t_{2}$ which yields a set $S$ of partial
trees, we define their delay as
$\mathit{delay}(t_{1},t_{2})=\mathrm{max}\\{h(t)+1\mid t\in S\\}$. An example
is given in Figure 3. Note that for trees over unary and leaf symbols (a way
to see words) the definitions for words and trees are equal. Recall that the
length of the word $a$ is one, but the height of the tree $a$ is zero.

In order to define a similarity measure between transducers using delay, we
take two transducer runs on the same input and compute the delay between their
produced outputs throughout their runs. Although we have defined delay between
words and trees, we only provide a formal definition for top-down tree
transducers. However, for word transducers, examples are given in Example A.1,
and a formal definition can be found in [15].

Now, let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be tdtts, and $\rho_{1}$ and
$\rho_{2}$ be runs of $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, respectively,
over the same input tree $t\in T_{\Sigma}$ such that
$\rho_{1}\colon(t,q_{0}^{\mathcal{T}_{1}},\varphi_{0})\rightarrow_{\mathcal{T}_{1}}^{*}(t,t_{1},\varphi)\text{
with }t_{1}\in T_{\Gamma}$, and
$\rho_{2}\colon(t,q_{0}^{\mathcal{T}_{2}},\varphi_{0})\rightarrow_{\mathcal{T}_{2}}^{*}(t,t_{2},\varphi^{\prime})\text{
with }t_{2}\in T_{\Gamma}$.

Basically, we take a look at all configurations that occur in the runs and
compute the delay between the output trees of compatible configurations where
compatible means in both configurations the same prefix (level-wise, see
below) of the input tree has been processed.

Let us be a bit more clear what we mean with compatible. Note that when
comparing two configuration sequences (i.e., runs) of word transducers the
notion of ‘have processed the same input so far’ is clear. For tree
transducers, in one configuration sequence, a left-hand subtree might be
processed before the right-hand subtree, and in another configuration sequence
vice versa. Since these computation steps are done in a parallel fashion (just
written down in an arbitrary order in the configuration sequence), we need to
make sure to compare configurations where the subtrees have been processed
equally far (we call this level-wise). Also, a tree transducer might not even
read the whole input tree, as, e.g., in Example 2.2. We also (implicitly) take
care of this in our definition.

The result is the maximum of the delay between output trees of compatible
configurations. Given $t\in T_{\Sigma}$, let
$\mathit{Prefs}_{\mathit{level}}(t)$ denote the set of all prefix trees of $t$
such that if a node at level $i$ is kept, then all other nodes at level $i$
are kept, i.e., for $t=f(h(a),h(a))$, $\mathit{Prefs}_{\mathit{level}}(t)$
contains $f(h,h)$, but not $f(h(a),h)$. Given an intermediate configuration
$(t,t^{\prime}_{i},\varphi^{\prime})$ of the run $\rho_{i}$, we recall that
$t^{\prime}_{i}\in T_{\Gamma\cup Q_{\mathcal{T}_{i}}}$ meaning
$t^{\prime}_{i}$ contains states of $\mathcal{T}_{i}$ as leaves. Let
$t^{\prime}_{i}|\Gamma$ denote the partial tree obtained from $t_{i}$ by
removing all non-$\Gamma$-labelled nodes. We define
$\mathit{delay}(\rho_{1},\rho_{2})$ as

$\displaystyle\max\\{\mathit{delay}(t^{\prime}_{1}|\Gamma,t^{\prime}_{2}|\Gamma)\mid\
$ $\displaystyle\text{there is
}t^{\prime}\in\mathit{Prefs}_{\mathit{level}}(t),\text{ there is
}(t,t_{1}^{\prime},\varphi^{\prime})\text{ in }\rho_{1}\text{ with
}t_{1}^{\prime}\in\mathcal{T}_{1}(t^{\prime}),$ $\displaystyle\text{and, there
is }(t,t_{2}^{\prime},\varphi^{\prime\prime})\text{ in }\rho_{2}\text{ with
}t_{2}^{\prime}\in\mathcal{T}_{2}(t^{\prime})\ \\}.$

The conditions $t_{1}^{\prime}\in\mathcal{T}_{1}(t^{\prime})$ and
$t_{2}^{\prime}\in\mathcal{T}_{2}(t^{\prime})$ are introduced to make sure
that all input nodes that can be processed from $t^{\prime}$ are processed in
the selected configurations.

$g$$f$$a$$f$$b$$h$$a$$f$ (a) partial tree $t_{1}$

$g$$f$$a$$f$$f$$a$$b$ (b) partial tree $t_{2}$

$b$$h$$a$$a$$b$ (c) partial trees resulting from removing $t_{1}\wedge t_{2}$
from $t_{1}$ and $t_{2}$

Figure 3: The greatest common prefix of the partial trees $t_{1}$ and $t_{2}$,
$t_{1}\wedge t_{2}$, is marked with circles in $t_{1}$ and $t_{2}$. The delay
between $t_{1}$ and $t_{2}$ is computed from their non-common parts as
$\mathit{delay}(t_{1},t_{2})=\mathrm{max}\\{h(t)+1\mid
t\in\\{b,h(a),a\\}\\}=2$.

We introduce (shorthand) notations. Let
$\mathcal{T}_{1},\mathcal{T}_{2}\in\mathcal{C}$, where $\mathcal{C}$ is a
class of transducers. Given $(t,s)\in R(\mathcal{T}_{1})$, we say $(t,s)$ is
_$k$ -delay included_ in $R(\mathcal{T}_{2})$, written
$(t,s)\in_{\mathbb{D}_{k}}R(\mathcal{T}_{2})$, if there are runs $\rho$ and
$\rho^{\prime}$ of $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, respectively, with
input $t$ and output $s$ such that $\mathit{delay}(\rho,\rho^{\prime})\leq k$.
We say $\mathcal{T}_{1}$ is _$k$ -delay included_ in $\mathcal{T}_{2}$,
written $\mathcal{T}_{1}\subseteq_{\mathbb{D}_{k}}\mathcal{T}_{2}$, if
$(t,s)\in_{\mathbb{D}_{k}}R(\mathcal{T}_{2})$ for all $(t,s)\in
R(\mathcal{T}_{1})$. We say $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are _$k$
-delay equivalent_, written
$\mathcal{T}_{1}=_{\mathbb{D}_{k}}\mathcal{T}_{2}$, if
$\mathcal{T}_{1}\subseteq_{\mathbb{D}_{k}}\mathcal{T}_{2}$ and
$\mathcal{T}_{2}\subseteq_{\mathbb{D}_{k}}\mathcal{T}_{1}$. We say
$\mathcal{T}_{1}$ _$k$ -delay uniformizes_ $\mathcal{T}_{2}$ if
$\mathcal{T}_{1}\subseteq_{\mathbb{D}_{k}}\mathcal{T}_{2}$ and
$\mathcal{T}_{1}$ uniformizes $\mathcal{T}_{2}$. The $k$-delay decision
problems are defined as expected.

In order to get a better understanding of the expressiveness and differences
between the two similarity measures, we first explore their properties on word
transductions since words are a particular case of trees (i.e., monadic
trees).

###### Word transducers.

We denote by fst a _finite state transducer_ , the class of word transductions
recognized by fsts is the class of _rational transductions_ , conveniently
also denoted by fst. We omit a formal definition of fsts, because they are not
considered outside of this section. An fst is _sequential_ if its transitions
are input-deterministic, more formally, a dtdtt over ranked alphabets with
only unary and leaf symbols can be seen as an fst.

The results below concern origin distance, the same results were proven for
delay in [15].

######  Proposition 3.1.

  1. 1.

There exist fsts $\mathcal{T}_{1}$, $\mathcal{T}_{2}$ such that
$\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$, but
$\mathcal{T}_{1}\not\subseteq_{k}\mathcal{T}_{2}$ for all $k\geq 0$.

  2. 2.

There exist fsts $\mathcal{T}_{1}$, $\mathcal{T}_{2}$ such that
$\mathcal{T}_{1}=\mathcal{T}_{2}$, but
$\mathcal{T}_{1}\neq_{k}\mathcal{T}_{2}$ for all $k\geq 0$.

  3. 3.

There exists an fst $\mathcal{T}$ such that $\mathcal{T}$ is sequentially
uniformizable, but $\mathcal{T}$ is not $k$-origin sequentially uniformizable
for all $k\geq 0$.

######  Proof 3.2.

First, consider the fsts $\mathcal{T}_{1},\mathcal{T}_{2}$ depicted in Figure
4(a). Both recognize the same function $f\colon\\{a,b,c\\}^{*}\to\\{a\\}^{*}$
defined as $f(ab^{*}c)=a$. Clearly, $\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$
and $\mathcal{T}_{1}=\mathcal{T}_{2}$. However, the origin distance between
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ is unbounded. In $\mathcal{T}_{1}$,
the origin of the single output letter $a$ is always the first input letter.
In contrast, in $\mathcal{T}_{2}$, the origin of the output letter $a$ is
always the last input letter. Secondly, consider the fsts
$\mathcal{T},\mathcal{T}^{\prime}$ depicted in Figure 4(a). The recognized
relation
$\mathcal{R}(\mathcal{T})\subseteq\\{a,b,A,B\\}^{*}\times\\{a,b\\}^{*}$
consists of $\\{(ab^{n}A,ab^{n})\mid n\in\mathbbm{N}\\}$ and
$\\{(ab^{n}B,ab^{m})\mid 0\leq m\leq 2n-1,n\in\mathbbm{N}\\}$. The sequential
transducer $\mathcal{T}^{\prime}$ recognizes the function
$f\colon\\{a,b,A,B\\}^{*}\to\\{a,b\\}^{*}$ defined by $f(ab^{n}X)=ab^{n}$ for
$X\in\\{A,B\\}$ and all $n\in\mathbbm{N}$. Clearly, $\mathcal{T}^{\prime}$ is
a sequential uniformization of $\mathcal{T}$. However, no sequential
uniformization with bounded origin distance exists, see Appendix B.

$\mathcal{T}_{1}$$a|a$$b|\varepsilon$$c|\varepsilon$$\mathcal{T}_{2}$$a|\varepsilon$$b|\varepsilon$$c|a$$\mathcal{T}$$a|a$$b|b$$A|\varepsilon$$a|a$$b|b$$b|\varepsilon$$b|\varepsilon$$b|bb$$B|\varepsilon$$\mathcal{T}^{\prime}$$a|a$$b|b$$A|\varepsilon$$B|\varepsilon$
(a) We have $\mathcal{T}_{1}=\mathcal{T}_{2}$, and
$\mathcal{T}_{1}=_{\mathbb{D}_{1}}\mathcal{T}_{2}$, but
$\mathcal{T}_{1}\neq_{k}\mathcal{T}_{2}$ for all $k\geq 0$;
$\mathcal{T}^{\prime}$ is a sequential uniformizer of $\mathcal{T}$.

$\mathcal{T}_{3}$$a|a$$\varepsilon|c$$b|\varepsilon$$\mathcal{T}_{4}$$a|a$$\varepsilon|c$$b|\varepsilon$
(b) We have $\mathcal{T}_{3}=\mathcal{T}_{4}$, and
$\mathcal{T}_{3}=_{1}\mathcal{T}_{4}$, but
$\mathcal{T}_{3}\neq_{\mathbb{D}_{k}}\mathcal{T}_{4}$ for all $k\geq 0$.

Figure 4: Comparing origin distance and delay for word transducers, see the
proof of Proposition 3.1 and Example A.1.

We give an example (depicted in Figure 4 and described in detail in Example
A.1) that shows that the two notions are orthogonal to each other. However, if
we restrict the class fst to _real-time_ 111$\varepsilon$-transitions (as,
e.g., the loop in $\mathcal{T}_{3}$ from Figure 4, not be confused with non-
producing transitions) are standard for fst, and non-standard for tdtt in the
literature. We consider ‘real-time’ tdtt by default.  fst, that is, word
transducers such that in every transition exactly one input symbol is read,
the notion of delay is more powerful than origin distance, see below. It is
important to note that we have proven Proposition 3.1 for real-time fsts which
are equivalent to tdtts on monadic trees, i.e., Proposition 3.1 is true for
the class tdtt.

######  Proposition 3.3.

Let $\mathcal{T}_{1},\mathcal{T}_{2}$ be real-time fsts, if
$\mathcal{T}_{1}\subseteq_{i}\mathcal{T}_{2}$ for some $i\geq 0$, then
$\mathcal{T}_{1}\subseteq_{\mathbb{D}_{j}}\mathcal{T}_{2}$ for some $j\geq 0$.

The notion of bounded delay is suitable to regain decidability.

######  Theorem 3.4 ([15]).

Given $k\geq 0$, $k$-delay inclusion, $k$-delay equivalence and $k$-delay
sequential uniformization are decidable for the class fst.

Ideally, we would like to lift Theorem 3.4 from word to tree transducers, but
it turns out that the notion of delay is too expressive to yield decidability
results for tree transducers as shown in the next paragraph.

###### Tree transducers.

It is undecidable whether a given tree-automatic relation has a uniformization
by a synchronous dtdtt [24]. A tdtt is called synchronous if for one processed
input node one output node is produced as, e.g., in Example 2.2. Tree-
automatic relations are a subclass of the relations that are recognizable by
synchronous tdtt. To prove the result, the authors showed that

######  Lemma 3.5 ([24]).

There exists a synchronous tdtt $\mathcal{T}_{M}$, based on a Turing machine
$M$, that is 0-delay dtdtt-uniformizable iff $M$ halts on the empty input.

In the proof, for a TM $M$, a dtdtt $\mathcal{T}_{M}^{\prime}$ is constructed
such that $\mathcal{T}_{M}^{\prime}$ $0$-delay uniformizes $\mathcal{T}_{M}$
iff $M$ halts on the empty input. Recall that this implies that
$\mathcal{T}_{M}^{\prime}\subseteq_{\mathbb{D}_{0}}\mathcal{T}_{M}$ iff $M$
halts on the empty input. Consequently, we obtain that

######  Theorem 3.6.

Given $k\geq 0$, $k$-delay inclusion and $k$-delay dtdtt-uniformization are
undecidable for the class tdtt (even for $k=0$).

We do not know whether $k$-equivalence is decidable for a given $k\geq 0$.
Note that Theorem 3.6 does not imply that $0$-origin inclusion and $0$-origin
dtdtt-uniformization is undecidable for the class tdtt. For the class fst, the
notions of $0$-origin and $0$-delay fall together, but for tdtt this is no
longer the case. Recall the tdtt given in Example 2.2 and its unique runs that
yield the origin mappings depicted in Figure 2. The delay between these runs
is zero, but their origin mappings are different. An analysis of the
(un)decidability proof(s) in [24] pins the problems down to the fact that in
the specification and in the possible implementations the origins for the same
output node lie on different paths in the input tree. For trees, this fact has
no influence when measuring the delay between computations (as seen in Example
2.2). However, it is recognizable using the origin distance as measure. Since
the notion of delay is so powerful that the decision problems under bounded
delay become undecidable for tree transducers (see Theorem 3.6) in contrast to
word transducers (see Theorem 3.4), in the next section, we focus on bounded
origin distance.

##  4 Decision problems for origin-close transducers

We show that the decision problems become decidable for top-down tree
transducers with bounded origin distance, see Theorem 4.8. The next part is
devoted to explaining our proof ideas and introducing our main technical lemma
(Lemma 4.2) which is used in all proofs.

###### Origin-close transductions are representable as regular tree languages.

$\varepsilon$$f$pt$h$$(x_{1})$$1$$f$$\iddots\ddots$$a$$b$$2$$f$$\iddots\ddots$$a$$b$pt$h$$(x_{2})$$1$$f$pt$h$$(x_{1})$$\iddots\ddots$pt$h$$(x_{2})$$\iddots\ddots$$b$$1$$f$$\iddots\ddots$$a$$b$$2$$f$$\iddots\ddots$$a$$b$$a$$b$$2$$f$$\iddots\ddots$$a$$b$$b$$1$$f$$\iddots\ddots$$a$$b$$2$$f$$\iddots\ddots$$a$$b$$a$$b$
(a)
${\mathsf{H}_{\mathcal{T},0}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$

$f$$f$$a$$a$$a$$h$$b$ (b) $(t,s,o)$

Figure 5: Infinite tree ${\mathsf{H}_{\mathcal{T},0}}$ based on $\mathcal{T}$
from Example 2.2. On red nodes In must make a choice, on green nodes Out must
make a choice. Their respective strategies $\mathsf{t}$ and $\mathsf{s}$ which
define their choices are highlighted on the edges in red and green,
respectively. Together, $\mathsf{t}$ and $\mathsf{s}$ encode the input tree
$t=f(f(a,a),a)$, the output tree $s=h(b)$ and origin mapping
$o\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$ as depicted. Note that since
$\mathsf{t}$ and $\mathsf{s}$ are strategies, choices are made whatever the
other player does, that is why in
${\mathsf{H}_{\mathcal{T},0}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$,
we also have, e.g., a green annotation at node 1112 even though In picked node
1111.

Given $k\geq 0$, and a tdtt $\mathcal{T}$, we construct an infinite tree
${\mathsf{H}_{\mathcal{T},k}}$, given as the unfolding of a finite graph
${\mathsf{G}_{\mathcal{T},k}}$, such that a node in this infinite tree
represents an input sequence from a finite input tree and an output sequence
(where the intuition is that this output sequence was produced while
processing this input sequence). The idea is that in
${\mathsf{H}_{\mathcal{T},k}}$, we define choices (aka. strategies) of two so-
called players In and Out, where a strategy $\mathsf{t}$ of In together with a
strategy $\mathsf{s}$ of Out defines an input tree $t$, an output tree $s$,
and an origin mapping $o\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$ of $s$ in
$t$. We can annotate the tree ${\mathsf{H}_{\mathcal{T},k}}$ with the
strategies $\mathsf{t}$ and $\mathsf{s}$ which yields a tree
${\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$.
We use this game-like view for all considered decision problems. We illustrate
this view.

######  Example 4.1.

Recall the tdtt $\mathcal{T}$ over $\Sigma$ and $\Gamma$ given in Example 2.2.
First, we explain how the graph ${\mathsf{G}_{\mathcal{T},0}}$ looks like. Its
unfolding is the infinite tree ${\mathsf{H}_{\mathcal{T},0}}$ (with
annotations $\mathsf{t}$ and $\mathsf{s}$) depicted in Figure 5. We have three
types of nodes: $\\{\varepsilon,1,2\\}$ to indicate that the current node is
the root, a first or a second child. The maximum rank of $\Sigma$ is two,
hence $\\{\varepsilon,1,2\\}$. These nodes belong to In who can choose the
input label, represented by nodes $\\{f,a\\}$. Then Out chooses which output
(from $T_{\Gamma}(X)$) should be produced while processing a node. Since
$k=0$, and all right-hand sides of rules in $\mathcal{T}$ have height at most
one, only outputs of height at most one are suitable to maintain origin
distance $k=0$. For input $f$ possible choices are $h(x_{1})$ and $h(x_{2})$,
indicating whether to continue to process the left or the right subtree, or
$b$. For input $a$ only output $b$ is possible. After the output, edges to
$\\{1,\cdots,\mathit{rk}(\sigma)\\}$ exist, where $\sigma$ is the last seen
input letter. Further explanation is given in Figure 5.

We present our main technical lemma which states that origin-close
transductions are representable as tree language recognizable by a parity tree
automaton (a pta).

######  Lemma 4.2.

Given $k\geq 0$ and a tdtt $\mathcal{T}$, there exists a pta that recognizes
the tree language
$\\{{\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\mid(t,s,o)\in_{k}R_{o}(\mathcal{T})\\}$.

######  Proof 4.3 (Proof sketch.).

The infinite tree
${\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
encodes a triple $(t,s,o)$. We construct a pta (which has in fact a safety
acceptance condition) that guesses a run of $\mathcal{T}$ over the input tree
$t$ with output tree $s$ that yields an origin mapping $o^{\prime}$ such that
$(t,s,o^{\prime})\in R_{o}(\mathcal{T})$ and
$\mathit{dist}(o(i),o^{\prime}(i))\leq k$ which implies that
$(t,s,o)\in_{k}R_{o}(\mathcal{T})$.

Checking whether $\mathit{dist}(o(i),o^{\prime}(i))\leq k$ can be done on-the-
fly because the origin distance is bounded which implies that the difference
trees of so-far produced output by the guessed run and the productions encoded
by the annotations are of bounded size. Thus, they can be stored in the state
space of the pta. Even tough the construction idea is rather simple, the
implementation and correctness proof are non-trivial. We face two
difficulties. Firstly, we have to account for the fact that in $o$ and
$o^{\prime}$ origins for the same output node can lie on different paths of
the input tree. However, since their distance is bounded, the amount of shared
information that the pta has to check on different paths is also bounded.
Secondly, it is possible to have non-linear transformation rules (that is,
rules with copy, e.g., $q(f(x_{1},x_{2}))\to f(q_{1}(x_{2}),q_{2}(x_{2})))$
which adds another layer of complication. This causes that an unbounded number
of output nodes can have the same input node as origin. We require that
${\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
is a tree over a ranked alphabet, hence we have to bound the number of output
choices that can be made at an input node. We show that it suffices to only
make a bounded number of output choices for each input node. The main insight
is that when two continuations of the output tree depend on the same
continuation of the input tree, then it suffices to only consider one of them
(because the other one can be continued in the same way) if they share the
same relevant information where relevant basically means that the state that
$\mathcal{T}$ has reached (guessed by the pta) at these two output nodes and
the output difference trees compared to Out’s choices (given by $\mathsf{s}$)
are the same.

###### Solving decision problems for origin-close transducers.

We show that deciding $k$-origin inclusion and equivalence for tdtts reduces
to deciding language inclusion for ptas.

######  Proposition 4.4.

Given $k\geq 0$, $k$-origin inclusion and $k$-origin equivalence are decidable
for the class tdtt.

######  Proof 4.5.

Let $\mathcal{T}_{1},\mathcal{T}_{2}$ be tdtts over the same input and output
alphabet. If $\mathcal{T}_{1}\subseteq_{k}\mathcal{T}_{2}$, then $(t,s,o)\in
R_{o}(\mathcal{T}_{1})$ implies that $(t,s,o)\in_{k}R_{o}(\mathcal{T}_{1})$
for all $(t,s,o)\in R_{o}(\mathcal{T}_{1})$. Lemma 4.2 yields that there are
ptas $\mathcal{A}_{1},\mathcal{A}_{2}$ that recognize
$\\{{\mathsf{H}_{\mathcal{T}_{1},0}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\mid(t,s,o)\in
R_{o}(\mathcal{T})\\}$ and
$\\{{\mathsf{H}_{\mathcal{T}_{2},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\mid(t,s,o)\in_{k}R_{o}(\mathcal{T}_{2})\\}$,
respectively. Basically, we want to check that $L(\mathcal{A}_{1})\subseteq
L(\mathcal{A}_{2})$. However, we have to overcome a slight technical
difficulty. If there are trees
${\mathsf{H}_{\mathcal{T}_{1},0}}^{\mathsf{\frown}}{\mathsf{t}_{1}}^{\mathsf{\frown}}{\mathsf{s}_{1}}\in
L(\mathcal{A}_{1})$ and
${\mathsf{H}_{\mathcal{T}_{2},k}}^{\mathsf{\frown}}{\mathsf{t}_{2}}^{\mathsf{\frown}}{\mathsf{s}_{2}}\in
L(\mathcal{A}_{2})$ such that for their encoded triples $(t_{1},s_{1},o_{1})$
and $(t_{2},s_{2},o_{2})$ holds that $t_{1}=t_{2}$, $s_{1}=s_{2}$ and $o_{1}$
and $o_{2}$ have an origin difference of at most $k$, i.e.,
$(t_{1},s_{1},o_{1})\in_{k}\mathcal{R}_{0}(\mathcal{T}_{2})$, it not
necessarily holds that
${\mathsf{H}_{\mathcal{T}_{1},0}}^{\mathsf{\frown}}{\mathsf{t}_{1}}^{\mathsf{\frown}}{\mathsf{s}_{1}}\in
L(\mathcal{A}_{2})$. This is due to the fact that the base trees
${\mathsf{H}_{\mathcal{T}_{1},0}}$ and ${\mathsf{H}_{\mathcal{T}_{2},k}}$ look
different in general because choices for Out in the first tree are based on
the rules of $\mathcal{T}_{1}$ and without origin distance and in the latter
tree based on the rules of $\mathcal{T}_{2}$ with $k$-origin distance. We only
care whether the paths reachable by following the annotations $\mathsf{t_{1}}$
and $\mathsf{s_{1}}$ through ${\mathsf{H}_{\mathcal{T}_{1},0}}$ and the paths
reachability by following the annotations $\mathsf{t_{2}}$ and
$\mathsf{s_{2}}$ through ${\mathsf{H}_{\mathcal{T}_{2},k}}$ are the same.
Thus, we introduce the operation $\mathit{purge}$ which applied to a tree
annotated with strategies of In and Out removes all non-strategy paths. It is
not difficulty to see that the sets
$L_{1}:=\\{\mathit{purge}\left({\mathsf{H}_{\mathcal{T}_{1},0}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\right)\mid(t,s,o)\in
R_{o}(\mathcal{T})\\}$ and
$L_{2}:=\\{\mathit{purge}\left({\mathsf{H}_{\mathcal{T}_{2},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\right)\mid(t,s,o)\in_{k}R_{o}(\mathcal{T}_{2})\\}$
are also pta-recognizable. Hence, in order to check whether
$\mathcal{T}_{1}\subseteq_{k}\mathcal{T}_{2}$, we have to check whether
$L_{1}\subseteq L_{2}$, which is decidable. We have shown that $k$-origin
inclusion for tdtts is decidable, consequently, $k$-origin equivalence for
tdtts is decidable for all $k\geq 0$.

We show that checking whether a tdtt is $k$-origin dtdtt-uniformizable reduces
to deciding emptiness of ptas.

######  Proposition 4.6.

Given $k\geq 0$, $k$-origin dtdtt-uniformization is decidable for the class
tdtt.

######  Proof 4.7.

Given a tdtt $\mathcal{T}$, by Lemma 4.2, there is a pta that recognizes

$\\{{\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\mid(t,s,o)\in_{k}R_{o}(\mathcal{T})\\}.$

By closure under complementation and intersection, there is a pta that
recognizes

$\\{{\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\mid(t,s,o)\notin_{k}R_{o}(\mathcal{T})\\}.$

By closure under projection, there is a pta that recognizes

$\\{{\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{s}}\mid\exists\thinspace\mathsf{t}:(t,s,o)\notin_{k}R_{o}(\mathcal{T})\\}.$

By closure under complementation and intersection, there is a pta that
recognizes

$\\{{\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{s}}\mid\forall\thinspace\mathsf{t}:(t,s,o)\in_{k}R_{o}(\mathcal{T})\\}.$

By closure under projection, there is a pta that recognizes

$\\{{\mathsf{H}_{\mathcal{T},k}}\mid\exists\thinspace\mathsf{s}:\forall\thinspace\mathsf{t}:(t,s,o)\in_{k}R_{o}(\mathcal{T})\\}.$

Let $\mathcal{A}$ denote the pta obtained in the last construction step. We
show that $\mathcal{T}$ is $k$-origin dtdtt-uniformizable iff
$L(\mathcal{A})\neq\emptyset$. We have that
$L(\mathcal{A})=\\{{\mathsf{H}_{\mathcal{T},k}}\mid\exists\thinspace\mathsf{s}:\forall\thinspace\mathsf{t}:(t,s,o)\in_{k}R_{o}(\mathcal{T})\\}.$
Colloquially, this means that we can fix output choices that only depend on
the previously seen input choices, which exactly describes dtdtt-
uniformizability.

Assume $\mathcal{T}$ is $k$-origin dtdtt-uniformizable, say by a dtdtt
$\mathcal{T}^{\prime}$. There exists a strategy of Out in
${\mathsf{H}_{\mathcal{T},k}}$ that copies the computations of
$\mathcal{T}^{\prime}$. Clearly, since $\mathcal{T}^{\prime}$ is
deterministic, we obtain that
$\exists\thinspace\mathsf{s}:\forall\thinspace\mathsf{t}:(t,s,o)\in_{k}R_{o}(\mathcal{T})$,
$\mathsf{s}$ can be chosen to be the strategy that copies
$\mathcal{T}^{\prime}$. Thus, $L(\mathcal{A})\neq\emptyset$.

For the other direction, assume that $L(\mathcal{A})\neq\emptyset$. This
implies that also the set
$\\{{\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{s}}\mid\forall\thinspace\mathsf{t}:(t,s,o)\in_{k}R_{o}(\mathcal{T})\\}$
is non-empty and pta recognizable. Since the set is pta recognizable, it
contains a regular infinite tree (meaning the tree has a finite
representation). This tree implicitly contains a finite representation of some
strategy $\mathsf{s}$ such that
$\forall\thinspace\mathsf{t}:(t,s,o)\in_{k}R_{o}(\mathcal{T})$. Hence, the
strategy $\mathsf{s}$ can be translated into a finite-state dtdtt that
$k$-origin uniformizes $\mathcal{T}$.

Finally, combining Propositions 4.4 and 4.6, we obtain our main result.

######  Theorem 4.8.

Given $k\geq 0$, $k$-origin inclusion, $k$-origin equivalence, and $k$-origin
dtdtt-uniformization are decidable for the class tdtt.

##  5 Conclusion

We introduced two similarity measures for tdtts based on their behavior and
studied decision problems for similar tdtts. For tdtts with bounded delay, the
decision problems remain undecidable. For origin-close tdtts they become
decidable. For future work, we plan to consider other tree transducer models.
In [16], it was shown that origin inclusion and origin equivalence are
decidable for MSO tree transducers and macro tree transducers.

## References

  * [1] Mikolaj Bojanczyk.  Transducers with origin information.  In ICALP (2), volume 8573 of Lecture Notes in Computer Science, pages 26–37. Springer, 2014.
  * [2] Mikolaj Bojanczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle.  Which classes of origin graphs are generated by transducers.  In ICALP, volume 80 of LIPIcs, pages 114:1–114:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [3] Sougata Bose, Shankara Narayanan Krishna, Anca Muscholl, Vincent Penelle, and Gabriele Puppis.  On synthesis of resynchronizers for transducers.  In MFCS, volume 138 of LIPIcs, pages 69:1–69:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [4] Sougata Bose, Anca Muscholl, Vincent Penelle, and Gabriele Puppis.  Origin-equivalence of two-way word transducers is in PSPACE.  In FSTTCS, volume 122 of LIPIcs, pages 22:1–22:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  * [5] Fabienne Braune, Nina Seemann, Daniel Quernheim, and Andreas Maletti.  Shallow local multi-bottom-up tree transducers in statistical machine translation.  In Proceedings of the 51st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 811–821, 2013.
  * [6] J. Richard Büchi and Lawrence H. Landweber.  Solving sequential conditions by finite-state strategies.  Transactions of the American Mathematical Society, 138:295–311, 1969.  doi:10.1090/S0002-9947-1969-0280205-0.
  * [7] Arnaud Carayol and Christof Löding.  Uniformization in Automata Theory.  In Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science Nancy, July 19-26, 2011, pages 153–178. London: College Publications, 2014.
  * [8] Alonzo Church.  Logic, arithmetic and automata.  In Proceedings of the International Congress of Mathematicians, pages 23–35, 1962.
  * [9] María Emilia Descotte, Diego Figueira, and Santiago Figueira.  Closure properties of synchronized relations.  In STACS, volume 126 of LIPIcs, pages 22:1–22:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [10] Joost Engelfriet.  Top-down tree transducers with regular look-ahead.  Math. Syst. Theory, 10:289–303, 1977.
  * [11] Joost Engelfriet and Sebastian Maneth.  Macro tree translations of linear size increase are mso definable.  SIAM Journal on Computing, 32(4):950–1006, 2003.
  * [12] Joost Engelfriet, Sebastian Maneth, and Helmut Seidl.  Look-ahead removal for total deterministic top-down tree transducers.  Theor. Comput. Sci., 616:18–58, 2016.
  * [13] Zoltán Ésik.  Decidability results concerning tree transducers i.  Acta Cybernetica, 5(1):1–20, 1980.
  * [14] Diego Figueira and Leonid Libkin.  Synchronizing relations on words.  Theory Comput. Syst., 57(2):287–318, 2015.
  * [15] Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter.  On equivalence and uniformisation problems for finite transducers.  In ICALP, volume 55 of LIPIcs, pages 125:1–125:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [16] Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier, and Jean-Marc Talbot.  Decision problems of tree transducers with origin.  Inf. Comput., 261:311–335, 2018.
  * [17] Patrick C. Fischer and Arnold L. Rosenberg.  Multitape one-way nonwriting automata.  Journal of Computer and System Sciences, 2(1):88–101, 1968.  URL: http://www.sciencedirect.com/science/article/pii/S0022000068800066, doi:http://dx.doi.org/10.1016/S0022-0000(68)80006-6.
  * [18] Zoltán Fülöp and Heiko Vogler.  Syntax-directed semantics: Formal models based on tree transducers.  Springer Science & Business Media, 2012.
  * [19] Timothy V. Griffiths.  The unsolvability of the equivalence problem for lambda-free nondeterministic generalized machines.  Journal of the ACM, 15(3):409–413, 1968.
  * [20] Shizuya Hakuta, Sebastian Maneth, Keisuke Nakano, and Hideya Iwasaki.  Xquery streaming by forest transducers.  In 2014 IEEE 30th International Conference on Data Engineering, pages 952–963. IEEE, 2014.
  * [21] Michael Holtmann, Łukasz Kaiser, and Wolfgang Thomas.  Degrees of lookahead in regular infinite games.  In Foundations of Software Science and Computational Structures, volume 6014 of Lecture Notes in Computer Science, pages 252–266. Springer, 2010.  doi:/10.1007/978-3-642-12032-9_18.
  * [22] Frederick A. Hosch and Lawrence H. Landweber.  Finite delay solutions for sequential conditions.  In ICALP, pages 45–60, 1972.
  * [23] Ralf Küsters and Thomas Wilke.  Transducer-based analysis of cryptographic protocols.  Information and Computation, 205(12):1741–1776, 2007.
  * [24] Christof Löding and Sarah Winter.  Uniformization problems for tree-automatic relations and top-down tree transducers.  In MFCS, volume 58 of LIPIcs, pages 65:1–65:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [25] Christof Löding and Sarah Winter.  Synthesis of deterministic top-down tree transducers from automatic tree relations.  Inf. Comput., 253:336–354, 2017.
  * [26] Andreas Maletti.  Tree transformations and dependencies.  In Conference on Mathematics of Language, pages 1–20. Springer, 2011.
  * [27] Andreas Maletti, Jonathan Graehl, Mark Hopkins, and Kevin Knight.  The power of extended top-down tree transducers.  SIAM Journal on Computing, 39(2):410–430, 2009.
  * [28] Kazutaka Matsuda, Kazuhiro Inaba, and Keisuke Nakano.  Polynomial-time inverse computation for accumulative functions with multiple data traversals.  Higher-Order and Symbolic Computation, 25(1):3–38, 2012.
  * [29] Tova Milo, Dan Suciu, and Victor Vianu.  Typechecking for xml transformers.  J. Comput. Syst. Sci., 66(1):66–97, 2003.  doi:10.1016/S0022-0000(02)00030-2.
  * [30] William C Rounds.  Mappings and grammars on trees.  Mathematical systems theory, 4(3):257–287, 1970.
  * [31] James W. Thatcher.  Generalized² sequential machine maps.  Journal of Computer and System Sciences, 4(4):339–367, 1970.
  * [32] Arie Van Deursen, Paul Klint, and Frank Tip.  Origin tracking.  Journal of Symbolic Computation, 15(5-6):523–545, 1993.
  * [33] Janis Voigtländer and Armin Kühnemann.  Composition of functions with accumulating parameters.  Journal of functional programming, 14(3):317, 2004.
  * [34] Sarah Winter.  Uniformization problems for synchronizations of automatic relations on words.  In ICALP, volume 107 of LIPIcs, pages 142:1–142:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.

##  Appendix A Missing example

######  Example A.1.

To begin with, consider the fsts $\mathcal{T}_{1},\mathcal{T}_{2}$ depicted in
Figure 4(a), we already explained in the proof of Proposition 3.1 that
$\mathcal{T}_{1}=\mathcal{T}_{2}$, but
$\mathcal{T}_{1}\neq_{k}\mathcal{T}_{2}$ for all $k\geq 0$, i.e., their origin
distance is unbounded. However, their delay is bounded by 1. It is easy to see
that $\mathcal{T}_{1}=_{\mathbb{D}_{1}}\mathcal{T}_{2}$, because their
difference in the length of their outputs for the same input is at most one
letter. Now, consider the fsts $\mathcal{T}_{3},\mathcal{T}_{4}$ depicted in
Figure 4(b). Both recognize the relation $\\{(ab,c^{n})\mid
n\in\mathbbm{N}\\}$, hence, $\mathcal{T}_{3}=\mathcal{T}_{4}$. Clearly, their
origin distance is bounded by 1. The whole output either has the first or the
second letter as origin. However,
$\mathcal{T}_{3}\neq_{\mathbb{D}_{k}}\mathcal{T}_{4}$ for all $k\geq 0$, i.e.,
their delay is unbounded. For any $k$, take the consider the unique runs that
admit output $c^{k+1}$ in $\mathcal{T}_{3}$ and $\mathcal{T}_{4}$,
respectively. We compare these runs for the input prefix $a$,
$\mathcal{T}_{3}$, already has produced $c^{k+1}$, and $\mathcal{T}_{4}$ no
output so far. Their delay is $k+1$.

##  Appendix B Missing proofs of Propositions 3.1 and 3.3

See 3.1

######  Proof B.1.

Secondly, consider the fsts $\mathcal{T},\mathcal{T}^{\prime}$ depicted in
Figure 4(a). The recognized relation
$\mathcal{R}(\mathcal{T})\subseteq\\{a,b,A,B\\}^{*}\times\\{a,b\\}^{*}$
consists of $\\{(ab^{n}A,ab^{n})\mid n\in\mathbbm{N}\\}$ and
$\\{(ab^{n}B,ab^{m})\mid 0\leq m\leq 2n-1,n\in\mathbbm{N}\\}$. The sequential
transducer $\mathcal{T}^{\prime}$ recognizes the function
$f\colon\\{a,b,A,B\\}^{*}\to\\{a,b\\}^{*}$ defined by $f(ab^{n}X)=ab^{n}$ for
$X\in\\{A,B\\}$ and all $n\in\mathbbm{N}$. Clearly, $\mathcal{T}^{\prime}$ is
a sequential uniformization of $\mathcal{T}$. However, no sequential
uniformization with bounded origin distance exists. Towards a contradiction,
assume there is sequential transducer $\mathcal{T}^{\prime\prime}$ that
uniformizes $\mathcal{T}$ such that
$\mathcal{T}^{\prime\prime}\subseteq_{k}\mathcal{T}$ for some $k\geq 0$.
Consider the input word $ab^{2k}A$, in $\mathcal{T}$ there is only one run
with the input which yields the output $ab^{2k}$ and the origin of the $i$th
output letter is the $i$th input letter for all $i$. Since
$\mathcal{T}^{\prime\prime}\subseteq_{k}\mathcal{T}$ there exists a run of
$\mathcal{T}^{\prime\prime}$ on $ab^{2k}A$ that yields $ab^{2k}$ and the
origin of the first $b$ in the output is at latest the $k$th $b$ in the input.
Now, consider the input $ab^{6k}B$, the output of $\mathcal{T}^{\prime\prime}$
on $ab^{6k}B$ is $ab^{6k}$. Since $\mathcal{T}^{\prime\prime}$ is sequential,
the the runs of $\mathcal{T}^{\prime\prime}$ on $ab^{2k}A$ and $ab^{6k}B$ are
the same up to the input $ab^{2k}$, thus, also for the output $ab^{6k}$ the
origin first output $b$ is at latest the $k$th $b$ in the input. Now we
compare this with all possible runs in $\mathcal{T}$ on $ab^{6k}B$ that also
yield $ab^{6k}$. Note that $\mathcal{T}$ (after producing the first $b$) must
always produce two $b$ at once, thus in order to produce $ab^{6k}$ for the
input $ab^{6k}B$, the production of $b$ can only start after while reading the
second half of the input. This implies that the first output has an origin in
the second half of input which has a distance of more than $k$ (at least $2k$)
to the $k$th $b$ in the input.

See 3.3

######  Proof B.2.

Let $\mathcal{T}_{1},\mathcal{T}_{2}$ be real-time fsts such that
$\mathcal{T}_{1}\subseteq_{i}\mathcal{T}_{2}$ for some $i\geq 0$. Let $\ell$
be the maximum number of output letters that $\mathcal{T}_{1}$ produces in a
computation step. Consider any $(u,v,o_{1})\in R_{o}(\mathcal{T}_{1})$, since
$\mathcal{T}_{1}\subseteq_{i}\mathcal{T}_{2}$, there is $(u,v,o_{2})\in
R_{o}(\mathcal{T}_{2})$ such that $\mathit{dist}(o_{1}(d),o_{2}(d))\leq i$ for
all $d\in\mathit{dom}_{v}$. Let $\rho_{1}$ and $\rho_{2}$ be the corresponding
runs of $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, respectively. We show that
$\mathit{delay}(\rho_{1},\rho_{2})\leq\ell\cdot i$ which implies that
$\mathcal{T}_{1}\subseteq_{\mathbb{D}_{\ell\cdot i}}\mathcal{T}_{2}$. Let
$u=a_{1}\cdots a_{n}$ and $v=b_{1}\cdots b_{m}$. Pick any prefix of $u$, say
$a_{1}\cdots a_{k}$, and consider the prefixes of the runs $\rho_{1}$ and
$\rho_{2}$ such that the input $a_{1}\cdots a_{k}$ has been processed. Let
$b_{1}\cdots b_{k_{1}}$ and $b_{1}\cdots b_{k_{2}}$ be the respective produced
outputs. Wlog., let $k_{1}\leq k_{2}$. If $k_{1}=k_{1}$, then the output delay
for the prefix $a_{1}\cdots a_{k}$ is zero. So assume $k_{1}<k_{2}$. We have
to show that $|b_{k_{1}+1}\cdots b_{k_{2}}|$ is less than $\ell\cdot i$. Since
the origin mappings of $\rho_{1}$ and $\rho_{2}$, that is, $o_{1}$ and
$o_{2}$, have a distance of at most $i$, we know that the origin of
$b_{k_{1}+1}\cdots b_{k_{2}}$ in $\rho_{1}$ is no later than at the letter
$a_{k+i}$. On $a_{k+1}\cdots a_{k+1}$, $\mathcal{T}_{1}$ can produce at most
$\ell\cdot i$ output letters. Consequently, $|b_{k_{1}+1}\cdots
b_{k_{2}}|\leq\ell\cdot i$.

##  Appendix C Organization of the appendix

The remainder of the appendix is devoted to the proof of Lemma 4.2.

We first prove a simpler variant, Lemma D.5, for linear top-down tree
transductions. We present the formal setup in Appendix D. In Appendix E, we
introduce several auxiliary notations and definitions. Subsequently, we
construct the desired pta in Appendix F and prove Lemma D.5 in Appendix G.
Finally, in Appendix H, we lift the construction and proof to the full set of
top-down tree transductions, i.e., we prove Lemma 4.2.

##  Appendix D Linear top-down tree transductions

We fix a linear tdtt and some values.

######  Assumption D.1.

  * •

Let $\Sigma,\Gamma$ be ranked alphabets, and let $m$ be the maximal rank of
$\Sigma$.

  * •

Let $\mathcal{T}$ be a _linear_ tdtt of the form
$(Q,\Sigma,\Gamma,q_{0},\Delta)$.

  * •

Let $M$ be the maximal height of a tree appearing on the right-hand side of a
transition rule in $\Delta$.

As mentioned in Section 4, given $k\geq 0$, and a tdtt $\mathcal{T}$, we
construct an infinite tree ${\mathsf{H}_{\mathcal{T},k}}$, given as the
unfolding of a finite graph ${\mathsf{G}_{\mathcal{T},k}}$, such that a node
in this infinite tree represents an input sequence from a finite input tree
and an output sequence (where the intuition is that this output sequence was
produced while processing this input sequence). The idea is that in
${\mathsf{H}_{\mathcal{T},k}}$, we define choices (aka. strategies) of two so-
called players In and Out, where a strategy $\mathsf{t}$ of In together with a
strategy $\mathsf{s}$ of Out defines an input tree $t$, an output tree $s$,
and an origin mapping $o\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$ of $s$ in
$t$. We can annotate the tree ${\mathsf{H}_{\mathcal{T},k}}$ with the
strategies $\mathsf{t}$ and $\mathsf{s}$ which yields a tree
${\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$.

Recall the given example in Example 4.1 and its visualization depicted in
Figure 5.

######  Definition D.2 ($\mathcal{G}_{\mathcal{T}}^{k}$).

Given $k\geq 0$, we define the graph $\mathcal{G}_{\mathcal{T}}^{k}$ with
edges

  * •

$(\varepsilon\times\Sigma)\cup(\\{1,\dots,m\\}\times\Sigma)$, Edges of Player
In

  * •

$\bigcup_{i=0}^{m}(\Sigma_{i}\times T_{out,i}$), Edges of Player Out

where $T_{out,i}=\\{t\in T_{\Gamma}(X_{i})\mid t\text{ is \emph{linear} and
}h(t)\leq M+2kM\\}$,

  * •

$\bigcup_{i=0}^{m}(T_{out,i}\times\\{1,\dots,i\\})$, and Edges to all
directions

  * •

$\varepsilon$ is the initial vertex.

The height of the output choices depends on $\mathcal{T}$ and the given
parameter $k$; their height is bounded by $M+2kM$, where the summand $M$
covers the case $k=0$. The intuition behind this is that the output choices
made by Out have to mimic the outputs in the transitions of $\mathcal{T}$
which are of height at most $M$. Since we are interested in $k$-origin close
computations, the output produced by Out can be made up to $k$ computation
steps earlier (or later) compared to the computation of $\mathcal{T}$, meaning
the height of the output difference is at most $kM$. Then, the next choice of
Out might be such that the situation reverses. Hence, output choices with a
height of at most $2\cdot kM$ suffice.

Our desired infinite tree is the following regular tree.

######  Definition D.3 (${\mathsf{H}_{\mathcal{T},k}}$).

Given $k\geq 0$, let ${\mathsf{H}_{\mathcal{T},k}}$ be the unfolding of the
graph $\mathsf{G}_{\mathcal{T}}^{k}$ with root node $\varepsilon$.

We need the notion of strategy annotations and resulting encoding.

######  Definition D.4 (Strategy annotations).

Given $k\geq 0$ and ${\mathsf{H}_{\mathcal{T},k}}$, let $\mathsf{t}$ be an
encoding of a strategy for In, let $\mathsf{s}$ be an encoding of a positional
strategy for Out. Note that the strategies are positional by default, because
${\mathsf{H}_{\mathcal{T},k}}$ is a tree. We denote by
${\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
the tree ${\mathsf{H}_{\mathcal{T},k}}$ with annotated strategies $\mathsf{s}$
and $\mathsf{t}$.

An annotated tree
${\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
uniquely identifies an input tree $t$, an output tree $s$ and an origin
function $o\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$.

See Examples 4.1 and 5 for an example of the above definition.

The next lemma is our key lemma for linear top-down tree transductions, it
states that the set of origin-close linear top-down tree transductions is a
regular tree language recognizable by a parity tree automaton.

######  Lemma D.5.

Given $k\geq 0$ and a linear tdtt $\mathcal{T}$, there exists a pta that
recognizes the tree language
$\\{{\mathsf{H}_{\mathcal{T},k}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\mid(t,s,o)\in_{k}R_{o}(\mathcal{T})\text{
and }o\text{ is a linear transduction}\\}$.

For ease of presentation, in the next sections, we leave out the subscripts
$\mathcal{T}$ and $k$ and simply write ${\mathsf{H}}$ instead of
${\mathsf{H}_{\mathcal{T},k}}$.

##  Appendix E Notations and definitions

Towards the construction of our desired parity tree automaton we need further
notations and definitions.

######  Definition E.1 ($k$-neighborhood).

For $k\geq 0$, let $N_{\Sigma}^{k}$ be the subset of trees from $N_{\Sigma}$
that have at most height $k$.

######  Definition E.2 (Annotations).

For a set $A$ and $k\geq 0$, let ${A}^{(k)}$ be the set that is $A$ extended
by $a^{(1)},\dots,a^{(k)}$ for each $a\in A$.

For $t\in T_{A}$, let $t^{(j)}$ denote the tree that results from $t$ by
replacing each occurrence of some $a\in A$ by $a^{(j)}$ for
$j\in\\{1,\dots,k\\}$.

For $t\in T_{A^{(j)}}$, $\mathit{strip}(t)$ is $t$ without its annotations.

For $f^{(j)}\in A^{(k)}$, $\mathit{ann}(f^{(j)})$ is its annotation $j$.

The introduced annotations will be used to mark symbols from the output
alphabet $\Gamma$ and states $Q$ of $\mathcal{T}$ that are used as labels in
trees.

Now, for the construction of the parity tree automaton, we compare
computations of $\mathcal{T}$ and Out on an input tree (given by the strategy
annotations in $\mathsf{H}$). Since the origins of these computations can have
a distance of at most $k$, we are going to represent the difference in the
state space of our parity tree automaton.

Towards this, we introduce two types of output information trees, one for
representing the situation where $\mathcal{T}$ is ahead (see Definition E.3),
and the other one where Out is ahead (see Definition E.7).

We begin with a representation for the case where $\mathcal{T}$ is ahead (or
on par) compared to Out.

######  Definition E.3 (Output information tree wrt. $\mathcal{T}$).

A tree $s\in N_{\Gamma^{(k)}\cup\Sigma\cup Q^{(k)}\cup Q}$ is said to be an
_output information tree_ if there is some $n$ such that $s$ is of the form
$C[s_{1},\dots,s_{n}]$, where

  * •

$C\in T_{\Gamma^{(k)}\setminus\Gamma}(X_{n})$ is an $n$-context,

  * •

$s_{1},\dots,s_{n}\in N_{Q^{(k)}\cup\Sigma}$ are trees such that for each
$s_{i}$ either $s_{i}\in Q$ or $s_{i}=q^{(j)}(t)$ for some $q^{(j)}\in
Q^{(k)}$ and some $t\in N_{\Sigma}$, and

  * •

there is at most one such $s_{i}\in Q$.

Consider $\Sigma$ given by $\Sigma_{2}=\\{f\\}$ and $\Sigma_{0}=\\{a,b\\}$,
and $\Gamma$ given by $\Gamma_{2}=\\{g\\}$, $\Gamma_{1}=\\{h\\}$ and
$\Gamma_{0}=\\{c\\}$. Examples of output information trees over $\Sigma$ and
$\Gamma$ are

$g^{(7)}$$q$$c^{(7)}$

, $g^{(7)}$$h^{(5)}$$c^{(3)}$$c^{(7)}$, $g^{(7)}$$q$$q_{1}^{(2)}$$f$$f$$a$,
and $g^{(7)}$$g^{(4)}$$q_{2}^{(6)}$$b$$c^{(4)}$$q_{1}^{(2)}$$f$$f$$a$ .

We explain the intuition between (the annotations of) output information trees
wrt. $\mathcal{T}$. The upper part of such a tree with labels from
${\Gamma^{(k)}\setminus\Gamma}$ describes the part of the output that
$\mathcal{T}$ is currently ahead of Out. The annotation $a$ of an output
symbol $g^{(a)}\in\Gamma^{(k)}$ indicates that Out has to produce this output
in at most $a$ computation steps, otherwise the bound on the origin distance
will be violated. The occurrence of a $q\in Q$, i.e., a state without
annotation, indicates that Out and $\mathcal{T}$ currently read the same node
of the input tree and $\mathcal{T}$ is in $q$. Furthermore, the annotation $a$
of a state symbol $p^{(a)}\in Q^{(k)}$ indicates that the current input node
of Out has a distance of $a$ to a node of the input tree that $\mathcal{T}$
processes while in $p$; it is assumed that these vertices lie on divergent
paths. The subtree below $p^{(a)}$ indicates the (partial) input tree that
$\mathcal{T}$ processes from this divergent vertex.

Now, given such an output information tree our goal is to define an update of
the tree according to transitions of $\mathcal{T}$. We give two auxiliary
definitions first.

For the first auxiliary definition, consider the case that $\mathcal{T}$ and
Out process the same node of the input tree. We define the application of a
transition from $\mathcal{T}$ assuming $\mathcal{T}$ is in the state $q$ and
the next input symbol is $f$.

An intuition is given in Figure 8.

$q(f):$$q$$f$$s\in\mathrm{ext}(q(f)):$$g$$q_{1}$$x_{1}$$q_{2}$$x_{2}$

Figure 6: An example of the extension for $q$ and $f$ wrt. the rule
$q(f(x_{1},x_{2}))\to g(q_{1}(x_{2}),q_{2}(x_{1}))$ according to Definition
E.4.

$q^{(2)}(t):$$q^{(2)}$$f$$f$$a$$b$$a$$s\in\mathrm{ext_{k}}(q^{(2)}(t)):$$g^{(k-2)}$$q_{1}^{(4)}$$a$$q_{2}^{(4)}$$f$$a$$b$

Figure 7: An example of the extension for $q^{(2)}$ and $t=f(f(a,b),a)$ with
distance update wrt. the rule $q(f(x_{1},x_{2}))\to
g(q_{1}(x_{2}),q_{2}(x_{1}))$ according to Definition E.5.

$s(f^{\prime}):$$g^{(7)}$$q$$f^{\prime}$$q_{1}^{(4)}$$f$$a$$b$$s^{\prime}\in\mathrm{EXT}_{k}(s(f^{\prime})):$$g^{(7)}$$h^{(k)}$$q_{1}$$x_{1}$$g^{(k-4)}$$q_{2}^{(6)}$$a$$q_{3}^{(6)}$$b$

Figure 8: An example of an extension for the output information tree
$s=f^{(7)}(q,q_{1}^{(4)}(g(a,b))$ and input symbol $f^{\prime}$ to Definition
E.6. To compute the extension the rules $q(f^{\prime}(x_{1},x_{2}))\to
h(q_{1}(x_{1}))$ and $q_{1}(f(x_{1},x_{2}))\to g(q_{2}(x_{1}),q_{3}(x_{2}))$
were used.

######  Definition E.4 (Extension).

For $f\in\Sigma$ and $q\in Q$, let $\mathrm{ext}(q(f))\subseteq
N_{\Sigma\cup\Gamma\cup Q}(X)$ be the _set of extensions_ such that an
_extension_

$s\in\mathrm{ext}(q(f):\Leftrightarrow\left\\{\begin{aligned}
&\exists\thinspace q\big{(}f(x_{1},\dots,x_{i})\big{)}\rightarrow
w[q_{1}(x_{j_{1}}),\dots,q_{n}(x_{j_{n}})]\in\Delta\\\
&s=w[q_{1}(x_{j_{1}}),\dots,q_{n}(x_{j_{n}})].\end{aligned}\right.$

For the second auxiliary definition, consider the case that $\mathcal{T}$ and
Out process different nodes of the input tree and the distance between these
nodes is given. Assume Out is currently at a node $u$ of the input tree and
$\mathcal{T}$ is at another node $u^{\prime}$ of the input tree such that $u$
and $u^{\prime}$ lie on divergent paths. Recall that the idea is that, given a
state $q\in Q^{(k)}$ with annotation $a$, it should denote that $u$ has
distance of $a$ to $u^{\prime}$. The result of an application of a rule is
then defined under the assumption that Out advances to a successor of $u$ and
$\mathcal{T}$ advances to a successor of $u^{\prime}$ which results in an
increase of the distance by two, because $u$ and $u^{\prime}$ lie on divergent
paths. Since the origin of the extended output is $u^{\prime}$ with a distance
of $a$ to $u$ it is implied that Out has to recover the produced output at
most $k-a$ steps later. We define the application of a transition from
$\mathcal{T}$ assuming $\mathcal{T}$ is in the state $q$, the distance between
the nodes $u$ and $u^{\prime}$ that $\mathcal{T}$ and Out read, respectively,
is $a$, and the next input(s) for $\mathcal{T}$ are given by a partial tree
$t$. For an intuition see Figure 8.

######  Definition E.5 (Extension with distance update).

For $q^{(a)}\in Q^{(k)}$ and a partial input tree $t\in N_{\Sigma}$, let
$\mathrm{ext_{k}}(q^{(a)}(t))$ be the _set of extensions with distance update_
such that an extension

$s\in\mathrm{ext_{k}}(q^{(a)}(t)):\Leftrightarrow\left\\{\begin{aligned}
&\exists\thinspace q\big{(}t(\varepsilon)(x_{1},\dots,x_{i})\big{)}\rightarrow
w[q_{1}(x_{j_{1}}),\dots,q_{n}(x_{j_{n}})]\in\Delta\\\
&s=w^{(k-a)}[q_{1}^{(a+2)}(t|_{j_{1}}),\dots,q_{n}^{(a+2)}(t|_{j_{n}})].\end{aligned}\right.$

Now, we are ready to define an update of an output information tree according
to the transitions of $\mathcal{T}$, called extension. The extension of an
output information tree is obtained by extending all positions where states
occur according to Definition E.4 and Definition E.5. See Figure 8 for an
intuition.

######  Definition E.6 (Extension of an OIT wrt. $\mathcal{T}$).

Let $s\in N_{\Gamma^{(k)}\cup\Sigma\cup Q^{(k)}}$ be an output information
tree wrt. $\mathcal{T}$ and $f\in\Sigma$. By definition of output information
trees wrt. $\mathcal{T}$, $s$ contains at most one node whose label is in $Q$.

If $s$ contains a node whose label is in $Q$, say $q$, we let
$\mathrm{EXT}_{k}(s(f))\subseteq N_{\Gamma^{(k)}\cup\Sigma\cup Q^{(k)}}(X)$ be
the set such that $s^{\prime}\in\mathrm{EXT}_{k}(s(f))$

$:\Leftrightarrow$ $\left\\{\begin{aligned} &\exists\thinspace
u,u_{1},\ldots,u_{n}\in\mathit{dom}_{s}\text{ with
}s(u)=q,s(u_{1})=q_{1}^{(a_{1})},\ldots,s(u_{n})=q_{n}^{(a_{n})}\\\
&\exists\thinspace
s_{0}\in\mathrm{ext}(q(f)),s_{1}\in\mathrm{ext_{k}}\left(q_{1}^{(a_{1})}(s|_{u_{1}1})\right),\ldots,s_{n}\in\mathrm{ext_{k}}\left(q_{n}^{(a_{n})}(s|_{u_{n}1})\right)\\\
&\forall\thinspace
u^{\prime}\in\mathit{dom}_{s}\setminus\\{u,u_{1},\ldots,u_{n}\\}:s(u^{\prime})\notin
Q^{(k)}\\\ &s^{\prime}=s[u\leftarrow s_{0},u_{1}\leftarrow
s_{1},\ldots,u_{n}\leftarrow s_{n}].\end{aligned}\right.$

Otherwise, $\mathrm{EXT}_{k}(s(f))$ is similarly defined; the parameter $f$ is
ignored and we extend all positions that have labels in $Q^{(k)}\setminus Q$.

Secondly, we define a representation for the case that Out is ahead (or on
par) compared to $\mathcal{T}$.

######  Definition E.7 (Output information tree wrt. Out).

Recall $S_{\Gamma^{(k)}\setminus\Gamma}$ are special trees over
$T_{\Gamma^{(k)}\setminus\Gamma}$. The special tree $s\in
S_{\Gamma^{(k)}\setminus\Gamma}$ is said to be an _output information tree_ ,
if removing the $\circ$-labeled node yields a tree in
$N_{\Gamma^{(k)}\setminus\Gamma}(X)$, or if $s=\circ$. Furthermore, a tree
$s\in T_{\Gamma^{(k)}\setminus\Gamma}$ is also an _output information tree_.

Examples of output information trees wrt. Out are $g^{(7)}$$x_{2}$$\circ$,
$g^{(4)}$$\circ$$a^{(2)}$, and $b^{(3)}$. As before, the intuition behind an
annotation $a$ is that the other party has to recover the output in at most
$a$ computation steps. Since output information trees wrt. Out represent by
how much Out is ahead, here, the annotations bound the number of computation
steps $\mathcal{T}$ can use to recover the output.

Also, we define the update of such a tree for a new output choice of Out
(which has been annotated).

######  Definition E.8 (Extension of an OIT wrt. Out).

For an output information tree $s\in S_{\Gamma^{(k)}\setminus\Gamma}$ and an
annotated (partial) output tree $s^{\prime}\in
N_{\Gamma^{(k)}\setminus\Gamma}(X)$, we define the extension of $s$ by
$s^{\prime}$ as $s\cdot s^{\prime}$. For an output information tree $s\in
T_{\Gamma^{(k)}\setminus\Gamma}$, we define the extension of $s$ by an
annotated (partial) output tree $s^{\prime}\in
N_{\Gamma^{(k)}\setminus\Gamma}(X)$ to be $s$ (ignoring the parameter
$s^{\prime}$), because $s$ can not be extended as it is already a (completely
transformed) tree which only consists of (annotated) output symbols.

Examples of extended output information trees are depicted in Figure 9(a) and
Figure 9(b) on the left-hand side, e.g., the extended tree
$g^{(7)}$$h^{(7)}$$x_{1}$$x_{2}$ could be obtained from concatenating the
output information tree $g^{(7)}$$\circ$$x_{2}$ with the (annotated partial)
output tree $h^{(7)}$$x_{1}$.

Now that we have constructed ways to represent output information trees wrt.
Out and $\mathcal{T}$ and how to extend this information wrt. a computation
step, we need a way to compare extensions of output information trees. Assume
$s$ is an extended output information tree wrt. Out and $s^{\prime}$ is an
extended output information tree wrt. $\mathcal{T}$, then we want to ensure
that it is either possible to extend $s$ to $s^{\prime}$ or the other way
around. The function _sync_ can be seen as a function that removes the
greatest common prefix of the outputs in $s$ and $s^{\prime}$ from both trees,
if one output can be extended to the other output and otherwise fails, see
Figure 9 for an intuition.

$s:$$g^{(7)}$$h^{(7)}$$x_{1}$$x_{2}$$s^{\prime}:$$g^{(5)}$$h^{(5)}$$q_{1}$$x_{1}$$f^{(5)}$$q_{2}$$x_{2}$$b^{(5)}$$x_{1}\mapsto$$q_{1}$$x_{1}$$x_{2}\mapsto$$f^{(5)}$$q_{2}$$x_{2}$$b^{(5)}$
(a) Let $s$ resp. $s^{\prime}$ be extended output information trees wrt. Out
resp. $\mathcal{T}$. Consider the result of $sync(s,s^{\prime})$. Following
Out in direction 1, Out and $\mathcal{T}$ are now on par; following Out in
direction 2, $\mathcal{T}$ is now ahead.

$s:$$g^{(3)}$$x_{1}$$f^{(3)}$$x_{2}$$x_{3}$$s^{\prime}:$$g^{(7)}$$q_{1}$$x_{3}$$q_{2}$$x_{2}$$x_{1}\mapsto$$q_{1}$$x_{3}$$f^{(3)}$$x_{2}$$x_{3}$$\mapsto$$q_{2}$$x_{2}$
(b) Let $s$ resp. $s^{\prime}$ be extended output information tree wrt. Out
resp. $\mathcal{T}$. Consider the result of $sync(s,s^{\prime})$. Following
Out in direction 1, Out and $\mathcal{T}$ are now on par; following Out in
direction 2 and 3, Out is now ahead.

Figure 9: Two examples of the application of the $\mathit{sync}$ function
according to Definition E.9.

######  Definition E.9 (Synchronization).

Let $s\in T_{\Gamma^{(k)}}(X)$ and $s^{\prime}\in
N_{\Gamma^{(k)}\cup\Sigma\cup Q^{(k)}}(X)$ be extensions of output information
trees of Out and $\mathcal{T}$, respectively. The result of
$sync(s,s^{\prime})$ is defined if for all
$u\in\mathit{dom}_{s}\cap\mathit{dom}_{s^{\prime}}$ with $s(u)\in\Gamma^{(k)}$
and $s^{\prime}(u)\in\Gamma^{(k)}$ holds that
$strip(s(u))=strip(s^{\prime}(u))$. Otherwise, the result of
$sync(s,s^{\prime})$ is undefined.

If defined, the result is a mapping $\lambda:T_{\Gamma^{(k)}}(X)\rightarrow
N_{\Gamma^{(k)}\cup\Sigma\cup Q^{(k)}}(X)$ which is computed as follows. We
define a partition of $\mathit{dom}_{s}$ into $D_{1}$ and $D_{2}$, where
$D_{1}$ contains each node $u$ with $s(u)\in\Gamma^{(k)}$ and
$strip(s(u))=strip(s^{\prime}(u))$. The set $D_{1}$ are the nodes from the
greatest common prefix of $s$ and $s^{\prime}$. From the set $D_{2}$ select
those nodes that do not have a predecessor in $D_{2}$, say these are the nodes
$u_{1},\dots,u_{n}$. Note that $u_{1},\dots,u_{n}$ are also part of
$\mathit{dom}_{s^{\prime}}$, because all parent nodes of $u_{1},\dots,u_{n}$
are in $D_{1}$ which is a subset of
$\mathit{dom}_{s}\cap\mathit{dom}_{s^{\prime}}$ and their labels have the same
arity in both $s$ and $s^{\prime}$. We define the result of
$sync(s,s^{\prime})$ to be the function $\lambda$ that maps $s|_{u_{i}}$ to
$s^{\prime}|_{u_{i}}$ for each $i$.

Note that the mapping $\lambda$ is always of the form $x\mapsto s^{\prime}$
for some $x\in X$ and $s^{\prime}\in N_{\Gamma^{(k)}\cup\Sigma\cup
Q^{(k)}}(X)$, or $s\mapsto q(x)$ for some $s\in T_{\Gamma^{(k)}}(X)$, $q\in Q$
and $x\in X$. The former case means that $\mathcal{T}$ is ahead (or on par)
compared to Out and the latter case means that $\mathcal{T}$ is behind. See
the mappings given on the right-hand side in Figure 9 for examples.

The next two definitions are used in the construction of the parity tree
automaton according to Lemma D.5. The parity tree automaton we construct is
nondeterministic; sometimes, we need to guess an output tree $s$ that we
require both Out and $\mathcal{T}$ to produce in the future with certain
distance conditions. The idea behind the definition is that $\mathcal{T}$ and
Out continue in divergent directions to produce the same output. The distance
of the origins of the output should be inside the given bound $k$. Thus, we
guess how much computation steps $\mathcal{T}$ and Out take, respectively, to
produce the output. This information is given by the annotations. If the sum
of the annotations (for each output node) is below $k$, the distance of the
origins is inside the origin bound $k$.

######  Definition E.10 (Duplicate with annotations).

For $k\geq 0$ and $s\in T_{\Gamma}$, let

$\displaystyle(s_{1},s_{2})\in\mathrm{DUP}_{k}(s)\Longleftrightarrow$
$\displaystyle\ strip(s_{1})=strip(s_{2})=s,\text{ and}$ $\displaystyle\
\forall\thinspace
u\in\mathit{dom}_{s}:\mathit{ann}(s_{1}(u))+\mathit{ann}(s_{2}(u))\leq k.$

Finally, after a computation step, the number of computation steps that a
party can wait to catch up the output decreases by one.

######  Definition E.11 (Decrease).

For an annotated tree $s$ let $\mathrm{dec}(s)$ be the tree $s$ where every
annotation $(a)$ has been replaced by $(a-1)$ if $a>1$, otherwise the result
is not defined.

##  Appendix F Construction

Let $\mathcal{A}$ denote the parity tree automata we construct for the proof
of Lemma D.5. The idea behind a run of $\mathcal{A}$ on
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
(which encodes $(t,s,o\colon\mathit{dom}_{s}\to\mathit{dom}_{t})$) is to guess
a run of $\mathcal{T}$ on $t$ that produces $s$ with origin function
$o^{\prime}\colon\mathit{dom}_{s}\to\mathit{dom}_{t}$, such that the distance
bound of $k$ between origins mappings $o$ and $o^{\prime}$ is respected, and
the correctness of the guess is verified while reading
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$. To
achieve this, $\mathcal{A}$ simulates a run of $\mathcal{T}$ on $t$ and in
each step compares the outputs of both Out and $\mathcal{T}$. Furthermore,
$\mathcal{A}$ keeps track of the parts of the output that have not yet been
produced by the other party together with distance information (in terms of
output annotations) to indicate the number of steps the other party can take
to catch up again. If at some point the outputs are not the same or either Out
or $\mathcal{T}$ fails to catch up, then the tree
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$ is
rejected.

###  F.1 Parity tree automaton

We now present the construction of the above described parity tree automaton
$\mathcal{A}$ parameterized by $\mathcal{T}$ and a given $k\geq 0$.

####  F.1.1 States

The state set $Q_{\mathcal{A}}$ consists of sets of states made up from

$\underbrace{\mathcal{S}}_{\begin{subarray}{c}\text{Set of states that store
information,}\\\ \text{implicitly defined further below}\end{subarray}}$
$\cup$ $\underbrace{Q_{O}}_{\text{Validate output component}}$ $\cup$
$\underbrace{Q_{I}}_{\text{Validate input component}}$ $\cup$

$\\{q_{acc}\\}\cup\\{q_{err}\\}$,

where $Q_{O}:=\\{q_{out=t}\mid t\in T_{\Gamma^{(k)}}\text{ and }h(t)\leq
Mk\\}$ and $Q_{I}:=\\{q_{in=t}\mid t\in N_{\Sigma}^{k}\\}$.

The intuition behind the size of the trees used as states in $Q_{I}$ and
$Q_{O}$ is that these states are used when origins diverge. If origins
diverge, say $v$ is their last common ancestor, then their distance grows with
each computation step, meaning the knowledge of a $k$-neighborhood of the
input tree around $v$ is sufficient to compute the remaining output, thus the
height of the trees in $Q_{I}$ is bounded by the given origin bound $k$. Also,
since the remaining output has to be computed in at most $k$ steps, its height
can be at most $Mk$, thus the height of the trees in $Q_{O}$ is bounded by
$Mk$.

####  F.1.2 Priorities

If a set of states contains $q_{err}$, its priority is $1$, otherwise its
priority is $0$.

####  F.1.3 The next relation

Before we are able to define the transitions, we need to further describe the
state set wrt. $\mathcal{S}$. The states of $\mathcal{S}$ store information of
the form $(f,o,S_{O},S_{\mathcal{T}})$, where

  * •

$f\in T_{\Sigma_{i}}$ is the current input symbol,

  * •

$o\in T_{out,i}$ is the current output choice ,

  * •

$S_{O}\in S_{\Gamma^{(k)}}$ is the current output information tree wrt. Out,
and

  * •

$S_{\mathcal{T}}\in N_{\Gamma^{(k)}\cup\Sigma\cup Q^{(k)}\cup Q}$ is the
current output information tree wrt. $\mathcal{T}$.

In the following, we use $/$ as a tuple entry to indicate that there is
currently no information.

We define the $\mathrm{next}$ relation that sets a state with information
$(f,o,S_{O},S_{\mathcal{T}})$ in relation to possible successor states which
is the heart of the construction. To ease the understanding, we recall that an
annotation at a $\Gamma$-labeled node indicates how much steps a party can
take to produce this output, and an annotation at a $Q$-labeled node indicates
the distance between two input nodes.

First, we give an informal step-by-step construction how to compute from
$(f,o,S_{O},S_{\mathcal{T}})$ with $f\in\Sigma_{i}$ successor states
$P_{1},\dots,P_{i}$ such that
$(f,o,S_{O},S_{\mathcal{T}})\rightarrow_{\mathrm{next}}(P_{1},\dots,P_{i})$.

  * •

Extend the stored output $S_{O}$ of Out by the current output $o$ and set new
annotations.

  * •

Extend the stored output $S_{\mathcal{T}}$ of $\mathcal{T}$ by choosing an
extension $e$ according to the current input symbol $f$ and set new
annotations.

  * •

Remove the greatest common prefix of $S_{O}\cdot o$ and $e$ by applying the
sync function.

  * •

From the result $\lambda$ of sync obtain the information for Out resp.
$\mathcal{T}$ that is passed to the children.

  * •

In case that Out and $\mathcal{T}$ follow divergent directions, guess and
verify (partial) input trees (resp. output trees with annotations) for these
divergent directions. Example F.2 will make this clear.

  * •

Update annotations by applying the dec function to indicate that one
computation step has been made.

It is helpful to consider the following examples before reading the formal
definition.

######  Example F.1.

Consider $(f,o,S_{O},S_{\mathcal{T}})$ and let the extension $S_{O}\cdot
o^{(k)}$ be $s$ from Figure 9(a) and the chosen extension of $S_{\mathcal{T}}$
and $f$ from $\mathrm{EXT}_{(k)}$ be $s^{\prime}$ from Figure 9(a). The result
$\lambda$ of $\mathit{sync}(s,s^{\prime})$ is also given in the same figure.

Assume that $f$ was binary, we have to compute states $P_{1}$ and $P_{2}$
which are passed to the children of the current node in
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$.

Following Out in dir. 1, we see that Out and $\mathcal{T}$ are on par, and
$\mathcal{T}$ also continues to read in dir. 1., thus we let
$P_{1}=\\{(/,/,S_{O}^{1},S_{\mathcal{T}}^{1}))\\}$ with $S_{O}^{1}=\circ$ and
$S_{\mathcal{T}}^{1}=dec(q_{1})=q_{1}$.

Following Out in dir. 2, we see that $\mathcal{T}$ is ahead, and $\mathcal{T}$
also continues to read in dir. 2., thus we let
$P_{2}=\\{(/,/,S_{O}^{2},S_{\mathcal{T}}^{2}))\\}$ with $S_{O}^{2}=\circ$ and

$S_{\mathcal{T}}^{2}=dec\left(\leavevmode\hbox to44.65pt{\vbox
to45.14pt{\pgfpicture\makeatletter\hbox{\hskip
21.37083pt\lower-36.30798pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ } \par{{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.5639pt}{-3.55pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f^{(5)}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.03783pt}{-29.63332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$q_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}\pgfsys@moveto{-4.6126pt}{-9.22745pt}\pgfsys@lineto{-10.3506pt}{-20.7004pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{8.50278pt}{-32.97498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b^{(5)}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}\pgfsys@moveto{4.61287pt}{-9.22745pt}\pgfsys@lineto{9.6521pt}{-19.30316pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\right)=$
$f^{(4)}$$q_{2}$$b^{(4)}$.

Consider an example that is more involved.

######  Example F.2.

Consider $(f,o,S_{O},S_{\mathcal{T}})$ and let the extension $S_{O}\cdot
o^{(k)}$ be $s$ from Figure 10(b) and the chosen extension of
$S_{\mathcal{T}}$ and $f$ from $\mathrm{EXT}_{(k)}$ be $s^{\prime}$ from
Figure 10(b). The result $\lambda$ of $\mathit{sync}(s,s^{\prime})$ is also
given in the same figure.

Assume that $f$ was ternary, we have to compute states $P_{1}$, $P_{2}$ and
$P_{3}$ which are passed to the children of the current node in
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$.

Following Out in dir. 1, we see that Out and $\mathcal{T}$ are on par, but
$\mathcal{T}$ continues to read in dir. 3. Since the construction is such that
we follow Out in dir. 1, we have to guess how the input looks in dir. 3., thus
we pick some $t_{3}\in N_{\Sigma}^{k}$. As explained before, choosing some
tree from $N_{\Sigma}^{k}$ suffices, because the distances of the origins of
the eventually produced outputs will only increase.

Thus, in dir. 1, we go to a state
$P_{1}=\\{(/,/,S_{O}^{1},S_{\mathcal{T}}^{1})\\}$ with $S_{O}^{1}=\circ$ and
$S_{\mathcal{T}}^{1}=dec\left(q_{1}^{(2+1)}(t_{3})\right)=q_{1}^{(2)}(t_{3})$,
where the annotation indicates that Out and $\mathcal{T}$ are now on divergent
positions with distance 2. Furthermore, we have to verify that the guess of
$t_{3}$ was correct, thus the state $P_{3}$ at dir. 3 contains $q_{in=t_{3}}$.

Following Out in dir. 2, we see that Out is ahead and that $\mathcal{T}$ also
continues in dir. 2. Further we note that Out, while ahead, also conditions
from dir. 3. This means that $\mathcal{T}$ eventually produces both outputs
that Out chooses to produce from dir. 2 and dir. 3 solely from dir. 2. A
consequence of this is that the outputs that Out eventually produces from dir.
3 will have divergent origins when produced by $\mathcal{T}$ from dir. 2.
Thus, we guess an output tree $s_{3}\in T_{\Gamma}$ with height at most $Mk$,
since the origins diverge. Since both parties have to produce this output as
of yet, we pick some $(s_{3}^{a},s_{3}^{b})\in\mathrm{DUP}_{k}$ . Combining
all these information, in dir. 2, we go to a state
$P_{2}=\\{(/,/,S_{O}^{2},S_{\mathcal{T}}^{2})\\}$ with
$S_{\mathcal{T}}^{2}=q_{2}$ and

$S_{O}^{2}=dec\left(\leavevmode\hbox to41.36pt{\vbox
to44.27pt{\pgfpicture\makeatletter\hbox{\hskip
20.05939pt\lower-35.44353pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ } \par{{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.5639pt}{-3.55pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f^{(3)}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.72638pt}{-30.67497pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\circ$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}\pgfsys@moveto{-4.61386pt}{-9.22745pt}\pgfsys@lineto{-10.802pt}{-21.60312pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.48264pt}{-30.30608pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$s_{3}^{a}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}\pgfsys@moveto{4.613pt}{-9.22745pt}\pgfsys@lineto{10.08427pt}{-20.1676pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\right)=$
$f^{(2)}$$\circ$$dec(s_{3}^{a})$. The annotations in $dec(s_{3}^{a})$ indicate
the number of computations steps that $\mathcal{T}$ may use to produce
$s_{3}$.

Also, we have to verify that Out indeed produces $s_{3}$ from dir. 3 according
to the annotations from $dec(s_{3}^{b})$. Thus, in dir. 3, the state $P_{3}$
contains $q_{out=dec(s_{3}^{b})}$.

Note that for dir. 3 we have defined that $P_{3}$ contains both $q_{in=t_{3}}$
and $q_{out=dec(s_{3}^{b})}$, so we set
$P_{3}=\\{q_{in=t_{3}},q_{out=dec(s_{3}^{b})}\\}$.

Recall that the result of the sync function, cf. Definition E.9, is a mapping
$\lambda$ which is always of the form $x\mapsto s^{\prime}$ for some $x\in X$
and $s^{\prime}\in N_{\Gamma^{(k)}\cup\Sigma\cup Q^{(k)}}(X)$, or $s\mapsto
q(x)$ for some $s\in T_{\Gamma^{(k)}}(X)$, $q\in Q$ and $x\in X$. The former
case means that $\mathcal{T}$ is ahead (or on par) compared to Out and the
latter case means that $\mathcal{T}$ is behind. With this in mind, we formally
define the _next relation $\rightarrow_{\mathrm{next}}$_ in Definition F.3 on
Definition F.3. We make the assumption that all operations that were applied
in the construction given in Definition F.3 had defined results.

######  Definition F.3 ($\rightarrow_{\mathrm{next}}$).

Let
$(f,o,S_{O},S_{\mathcal{T}})\rightarrow_{\mathrm{next}}(P_{1},\dots,P_{i})$
for $f\in\Sigma_{i}$ if

  * •

there exists an extension $e\in\mathrm{EXT}_{(k)}(S_{\mathcal{T}}(f))$ of the
OIT $S_{\mathcal{T}}$ according to the current input symbol $f$,

  * •

there exists $\lambda$ as a result of $sync(S_{O}\cdot o^{(k)},e)$, where
$S_{O}\cdot o^{(k)}$ is the extension of the OIT $S_{O}$ by $o^{(k)}$
according to the current output choice $o$, and

  * •

the states $P_{1},\dots,P_{i}$ passed to the children of the current input
node are build up from $P_{1}=\emptyset,\dots,P_{i}=\emptyset$ according to
$\lambda$ as specified in $(\dagger)$, where $(\dagger):=$

$\left\lmoustache\begin{aligned}
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ deal with the children where $\mathcal{T}$ is ahead (or on par)
compared to {{Out}}}\phantom{\Big{(}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ both {{Out}} and $\mathcal{T}$ continue to read at the $j$th
child}\\\ &\exists\thinspace j\thinspace\big{(}\lambda:x_{j}\mapsto
w[q_{1}(x_{j_{1}}),\dots,q_{m}(x_{j_{m}}),\dots,q_{n}(x_{j_{n}})]\text{ with
}j_{m}=j\big{)}\rightarrow\phantom{\Big{(}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ chose and verify input neighborhoods for all other ($\neq j$)}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>children that $\mathcal{T}$ also reads}\\\
&\phantom{t}\bigg{(}\exists\thinspace
t_{1},\dots,t_{m-1},t_{m+1},\dots,t_{n}\in N_{\Sigma}^{k}:\bigwedge_{\ell\neq
m}P_{j_{\ell}}\ni q_{in=t_{\ell}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ set new OITs for the $j$th child}\\\ &\phantom{text}\wedge
P_{j}\ni(/,/,S_{O}^{j},S_{\mathcal{T}}^{j})\text{ with }S_{O}^{j}=\circ,\text{
and }S_{\mathcal{T}}^{j}=\phantom{\Big{(}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ at a child only it's own input is followed, use chosen}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>input neighborhoods in the OIT for the other children to}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>be able to further select $\mathcal{T}$s computation}\\\
&\phantom{text}\mathrm{dec}\big{(}w[q_{1}^{(2+1)}(t_{1}),\dots,q_{m-1}^{(2+1)}(t_{m-1}),q_{m},q_{m+1}^{(2+1)}(t_{m+1}),\dots,q_{n}^{(2+1)}(t_{n})]\big{)}\bigg{)}\\\
&\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ only {{Out}} continues to read at the $j$th child
}\quad\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>(similar to above)}\\\ &\exists\thinspace
j\thinspace\big{(}\lambda:x_{j}\mapsto
w[q_{1}(x_{j_{1}}),\dots,q_{n}(x_{j_{n}})]\text{ with no
}j_{m}=j\big{)}\rightarrow\\\ &\phantom{t}\bigg{(}\exists\thinspace
t_{1},\dots,t_{n}\in N_{\Sigma}^{k}:\bigwedge_{\ell}P_{j_{\ell}}\ni
q_{in=t_{\ell}}\thinspace\wedge P_{j}\ni(/,/,S_{O}^{j},S_{\mathcal{T}}^{j})\\\
&\phantom{text}\text{with }S_{O}^{j}=\circ,\text{ and
}S_{\mathcal{T}}^{j}=\mathrm{dec}\big{(}w[q_{1}^{(2+1)}(t_{1}),\dots,q_{n}^{(2+1)}(t_{n})]\big{)}\bigg{)}\\\
&\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ deal with the children where {{Out}} is ahead compared to
$\mathcal{T}$}\\\ \end{aligned}\right.$

Def. is continued at Section F.1.3

$\left\rmoustache\begin{aligned} &\phantom{texttext}\text{ {Def.\ continued
from \lx@cref{creftype~refnum}{def:next}}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ deal with the children where {{Out}} is ahead compared to
$\mathcal{T}$}\phantom{\Big{(}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ {{Out}} and $\mathcal{T}$ continue to read at the same child}\\\
&\exists\thinspace
j\thinspace\big{(}\lambda:w[x_{j_{1}},\dots,x_{j_{n}}]\mapsto q(x_{j})\text{
with }j_{m}=j\big{)}\rightarrow\phantom{\Big{(}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ chose output trees for all other ($\neq j$) children that {{Out}}
also reads}\\\ &\phantom{t}\bigg{(}\exists\thinspace
s_{1},\dots,s_{m-1},s_{m+1},\dots,s_{n}\in T_{\Gamma}:\bigwedge_{\ell\neq
m}h(s_{\ell})\leq Mk\thinspace\wedge\phantom{\big{(}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ both {{Out}} and $\mathcal{T}$ have to produce these, chose
annotations that}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>indicate how much steps each party can use}\\\
&\phantom{text}\exists\thinspace(s_{1}^{a},s_{1}^{b})\in\mathrm{DUP}_{(k)}(s_{1}),\dots,(s_{m-1}^{a},s_{m-1}^{b})\in\mathrm{DUP}_{(k)}(s_{m-1}),\\\
&\phantom{texttext}(s_{m+1}^{a},s_{m+1}^{b})\in\mathrm{DUP}_{(k)}(s_{m+1}),\dots,(s_{n}^{a},s_{n}^{b})\in\mathrm{DUP}_{(k)}(s_{n}):\\\
&\phantom{texttext}\bigwedge_{\ell\neq m}P_{j_{\ell}}\ni
q_{out=\mathrm{dec}(s_{\ell}^{b})}\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ verify that {{Out}} produces the chosen}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>output trees (annotations wrt.\ {{Out}})}\\\ &\phantom{texttext}\wedge
P_{j}\ni(/,/,S_{O}^{j},S_{\mathcal{T}}^{j})\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ set new OITs for the $j_{1}$th child\ }\phantom{\Big{(}}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ use chosen output trees (annotations wrt.\ $\mathcal{T}$) in the
OIT to be}\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>able to further synchronize this with $\mathcal{T}$s computation}\\\
&\phantom{texttextte}\text{with }S_{\mathcal{T}}^{j}=q\text{ and
}S_{O}^{j}=\mathrm{dec}\big{(}w[s_{1}^{a},\dots,s_{m-1}^{a},\circ,s_{m+1}^{a},s_{n}^{a}]\big{)}\bigg{)}\\\
&\\\
&\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>$//\\!\\!$ {{Out}} and $\mathcal{T}$ share no read
direction}\quad\texttt{\small\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color<EMAIL_ADDRESS>(similar to above)}\\\ &\exists\thinspace
j\thinspace\big{(}\lambda:w[x_{j_{1}},\dots,x_{j_{n}}]\mapsto q(x_{j})\text{
with no }j_{m}=j\\\ &\phantom{t}\bigg{(}\exists\thinspace s_{1},\dots,s_{n}\in
T_{\Gamma}:\bigwedge_{\ell}h(s_{\ell})\leq Mk\thinspace\wedge\\\
&\phantom{text}\exists\thinspace(s_{1}^{a},s_{1}^{b})\in\mathrm{DUP}_{(k)}(s_{1}),\dots,(s_{n}^{a},s_{n}^{b})\in\mathrm{DUP}_{(k)}(s_{n}):\\\
&\phantom{textte}\bigwedge_{\ell}P_{j_{\ell}}\ni
q_{out=\mathrm{dec}(s_{\ell}^{b})}\wedge
P_{j}\ni(/,/,S_{O}^{j_{1}},S_{\mathcal{T}}^{j_{1}})\text{ with }\\\
&\phantom{texttextte}S_{\mathcal{T}}^{j}=q\text{ and
}S_{O}^{j}=\mathrm{dec}\big{(}w[s_{1}^{a},\dots,s_{n}^{a}]\big{)}\bigg{)}\end{aligned}\right.$

We define the following auxiliary relation.

######  Definition F.4 ($\mathrm{NEXT}$).

For $S\in\mathcal{S}$, let

$\mathrm{NEXT}(S)=\\{(P_{1},\dots,P_{i})\mid
S\rightarrow_{\mathrm{next}}(P_{1},\dots,P_{i})\\}\cup\\{(\\{q_{err}\\})^{i}\\}$

be the set of possible successor states.

The idea of the construction for the parity automaton is that the automaton
guesses an application of the next relation (which means guessing an
application of a rule from $\mathcal{T}$ and comparing the information with
the output choice of Out defined in
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$)
such that the origins obtained from computations of $\mathcal{T}$ and Out
never have a distance of more than $k$.

With all definitions in place, we are ready to present the construction of
$\Delta_{\mathcal{A}}$ that implements the idea described in the paragraph
before. The automaton only checks properties on the part of
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
that are relevant for $t$ and $s$, and collect the needed information along
the way. However, before we do so, we take a closer look at one special case
that can occur.

######  Example F.5.

In order to compute a pair such that
$(f,o,S_{O},S_{\mathcal{T}})\rightarrow_{\mathrm{next}}(P_{1},\dots,P_{i})$,
assume that the result of the sync function used to compute this pair contains
$g^{(6)}$$x_{2}$$c^{(3)}$$\mapsto$$q$$x_{1}$. We see that Out is ahead
compared to $\mathcal{T}$, and that they do not share a read direction. The
construction given in Definition F.3 for last case is applied. That means we
follow $\mathcal{T}$ in dir. 1 and guess an output tree that Out has to
produce from dir. 2 and verify that both Out and $\mathcal{T}$ will eventually
produce the chosen output tree. Therefore, an output tree is chosen, for
example $b\in T_{\Gamma}$, and a pair from $\mathrm{DUP}_{(k)}(b)$, for
example $(b^{(2)},b^{(3)})$. Then, in dir. 2, the state $P_{2}$ that contains
$q_{out=dec(b^{(3)})}=q_{out=b^{(2)}}$ is reached, and in dir. 1 the state
$P_{1}$ that contains $(/,/,S_{O}^{1},S_{\mathcal{T}}^{1})$ is reached with
$S_{\mathcal{T}}^{1}=q$ and $S_{O}^{1}=dec\left(\leavevmode\hbox
to46.58pt{\vbox to43.82pt{\pgfpicture\makeatletter\hbox{\hskip
23.28299pt\lower-36.30798pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.14201pt}{-2.23056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$g^{(6)}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.94998pt}{-32.97498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b^{(2)}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}\pgfsys@moveto{-3.95326pt}{-7.90799pt}\pgfsys@lineto{-9.65211pt}{-19.30315pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{8.48482pt}{-31.65553pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$c^{(3)}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}\pgfsys@moveto{3.95314pt}{-7.90799pt}\pgfsys@lineto{10.31174pt}{-20.62259pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\right)=$
$g^{(5)}$$b^{(1)}$$c^{(2)}$.

According to the construction of the transitions of $\mathcal{A}$ presented
below, the following can happen. Recall that
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$ is
identified with some input tree $t$, output tree $s$, and corresponding origin
mapping $o$. Consider a run of $\mathcal{A}$ on
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$,
and assume that a node will be reached that corresponds to some
$v\in\mathit{dom}_{t}$ and $\mathcal{A}$ is in a state that contains
$(f,o,S_{O},S_{\mathcal{T}})$. Assume that in order to continue the run, the
successor states $P_{1},\dots,P_{i}$ from this example are used. From this
node, following the strategy annotations of In, $\mathcal{A}$ will reach a
node in
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
that corresponds to $v1\in\mathit{dom}_{t}$. This node will have a strategy
annotation for Out, however this strategy annotation has no relevance for the
the output tree $s$, because only strategy annotations for Out that are
reachable from nodes in
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
that corresponds to (descendants of) $v2\in\mathit{dom}_{t}$ contribute
further to $s$. The described node that corresponds to $v1\in\mathit{dom}_{t}$
will be reached with a state that contains some
$(f^{\prime},o^{\prime},S_{O}^{1},S_{\mathcal{T}}^{1})$ with $S_{O}^{1}$ and
$S_{\mathcal{T}}^{1}$ as above and $o^{\prime}$ is the new strategy annotation
for Out. To continue the run of $\mathcal{A}$, we chose successor states
according to the next relation. To compute these, as formally defined,
$S_{O}^{1}\cdot o^{\prime(k)}$ is used. Recall that $S_{O}^{1}\cdot
o^{\prime(k)}$ is $S_{O}^{1}$, because $S_{O}^{1}=g^{(5)}(b^{(1)},c^{(2)})\in
T_{\Gamma^{(k)}}$. We see that the irrelevant strategy annotation plays no
role in the computation of the successor states. Since this case is rather
hidden below, as it is covered as a special case of the statements in the
upcoming correctness proof, we explicitly showed this example here.

The situation that $\mathcal{A}$ reaches a node of
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
(with a meaningful state), in which the strategy annotation of Out is
irrelevant, happens because for the special case where Out is ahead compared
to $\mathcal{T}$ and they do not share a read direction, we follow
$\mathcal{T}$ (instead of Out which we follow otherwise). This is only done
because it simplifies the correctness proof of the following construction in
this section.

####  F.1.4 Transitions

As we have seen in Example F.2, it can happen that more than one state is
passed to a direction, then we follow each state as described below in the
construction of $\Delta_{\mathcal{A}}$ and implicitly assume that we go into a
set of states.

Recall that the parity tree automaton reads nodes of
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$.
Hence, as alphabet of the parity tree automaton, we use triples. The first
entry is the label from $\mathsf{H}$, the second and third entry are the
strategy annotations for In and Out, respectively. We assume the strategy
annotations are the number of the child that is chosen. We use $\\#$ in the
second resp. third entry to indicate that there is no annotation for either In
or Out.

##### Construction of Delta wrt. stored output information trees

  * •

We define $q_{in}:=(/,/,\circ,q_{0})$ to be the initial state.

  * •

For $(/,/,S_{O},S_{\mathcal{T}})\in\mathcal{S}$, $f\in\Sigma_{i}$ and
$j\in\\{1,\dots,|T_{out,i}|\\}$, we add

$\bigg{(}(/,/,S_{O},S_{\mathcal{T}}),(f,\\#,j),q_{acc},\dots,q_{acc},\underbrace{(f,/,S_{O},S_{\mathcal{T}})}_{j\text{th
child}},q_{acc},\dots,\underbrace{q_{acc}}_{|T_{out,i}|\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}.$

_We collect the current input symbol and follow the choice of Out._

  * •

For $(f,/,S_{O},S_{\mathcal{T}})\in S$, $f\in\Sigma_{i}$ and $o\in T_{out,i}$,
we add

$\bigg{(}(f,/,S_{O},S_{\mathcal{T}}),(o,\\#,\\#),p_{1},\dots,p_{i}\bigg{)}\text{
to }\Delta_{\mathcal{A}}\text{ for each
}(p_{1},\dots,p_{i})\in\mathrm{NEXT}(f,o,S_{O},S_{\mathcal{T}}).$

_We collect the current output choice and compute the successor states
according to the next relation which guesses an application of rule from
$\mathcal{T}$ as defined above._

  * •

For $(/,/,S_{O},S_{\mathcal{T}})\in\mathcal{S}$,
$\ell\in(\\{\varepsilon\\}\cup\\{1,\dots,m\\})$ and
$j\in\\{1,\dots,|\Sigma|\\}$, we add

$\bigg{(}(/,/,S_{O},S_{\mathcal{T}}),(\ell,j,\\#),q_{acc},\dots,q_{acc},\underbrace{(/,/,S_{O},S_{\mathcal{T}})}_{j\text{th
child}},q_{acc},\dots,\underbrace{q_{acc}}_{|\Sigma|\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}.$

_We follow the choice of In._

For ease of presentation, we speak of collecting (input and output)
information along the tree and choosing successor states as “one step” of
$\mathcal{A}_{k}$.

The next two parts are the constructions used to verify the input resp. the
output guesses.

##### Construction of Delta wrt. input guesses

  * •

For $q_{in=t}\in Q_{I}$, $f\in\Sigma_{i}$ and $j\in\\{1,\dots,|T_{out,i}|\\}$,
we add

$\bigg{(}q_{in=t},(f,j,\\#),q_{acc},\dots,q_{acc},\underbrace{q_{in=t}}_{j\text{th
child}},q_{acc},\dots,\underbrace{q_{acc}}_{|T_{out,i}|\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}\text{ if }t(\varepsilon)=f.$

_We check the correctness of (the root node of) the guess._

  * •

For $q_{in=f}\in Q_{I}$, $f\in\Sigma_{i}$ and $j\in\\{1,\dots,|T_{out,i}|\\}$,
we add

$\bigg{(}q_{in=f},(f,\\#,j),q_{acc},\dots,\underbrace{q_{acc}}_{|T_{out,i}|\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}.$

_We follow the choice of Out._

  * •

For $q_{in=t}\in Q_{I}$ with $t(\varepsilon)\in\Sigma_{i}$ and $o\in
T_{out,i}$, we add

$\bigg{(}q_{in=t},(o,\\#,\\#),q_{in=t|_{1}},\dots,q_{in=t|_{i}}\bigg{)}\text{
to }\Delta_{\mathcal{A}}.$

_We pass on the remainder of the guess._

  * •

For $q_{in=t}\in Q_{I}$, $\ell\in(\\{\varepsilon\\}\cup\\{1,\dots,m\\})$ and
$j\in\\{1,\dots,|\Sigma|\\}$, we add

$\bigg{(}q_{in=t},(\ell,j,\\#),q_{acc},\dots,q_{acc},\underbrace{q_{in=t}}_{j\text{th
child}},q_{acc},\dots,\underbrace{q_{acc}}_{|\Sigma|\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}.$

_We follow the choice of In._

##### Construction of Delta wrt. output guesses

  * •

For $q_{out=t}\in Q_{O}$, $f\in\Sigma_{i}$ and
$j\in\\{1,\dots,|T_{out,i}|\\}$, we add

$\bigg{(}q_{out=t},(f,\\#,j),q_{acc},\dots,q_{acc},\underbrace{q_{out=t}}_{j\text{th
child}},q_{acc},\dots,\underbrace{q_{acc}}_{|T_{out,i}|\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}.$

_We follow the choice of Out._

  * •

For $q_{out=t}\in Q_{O}$ and $o\in T_{out,i}$ such that $sync(o,t)$ is defined
and $dom(\lambda)\neq\emptyset$, we add

$\bigg{(}q_{out=t},(o,\\#,\\#),q_{1},\dots,q_{i}\bigg{)}\text{ to
}\Delta_{\mathcal{A}},\text{ where }q_{j}\text{ is }q_{out=dec(w)},$

if $\lambda:w\mapsto x_{j}$ and $dec(w)$ is valid, otherwise $q_{j}=q_{err}$
for all $1\leq j\leq i.$

_We check the correctness of a part of the guess._

  * •

For $q_{out=t}\in Q_{O}$ and $o\in T_{out,i}$ such that $sync(o,t)$ is defined
and $dom(\lambda)=\emptyset$, we add

$\bigg{(}q_{out=t},(o,\\#,\\#),q_{acc},\dots,\underbrace{q_{acc}}_{i\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}.$

_We have successfully verified the guess._

  * •

For $q_{out=t}\in Q_{O}$, $\ell\in(\\{\varepsilon\\}\cup\\{1,\dots,m\\})$ and
$j\in\\{1,\dots,|\Sigma|\\}$, we add

$\bigg{(}q_{out=t},(\ell,j,\\#),q_{acc},\dots,q_{acc},\underbrace{q_{out=t}}_{j\text{th
child}},q_{acc},\dots,\underbrace{q_{acc}}_{|\Sigma|\text{th
child}}\bigg{)}\text{ to }\Delta_{\mathcal{A}}.$

_We follow the choice of In._

##  Appendix G Correctness of the construction

We prove our key lemma for linear top-down tree transductions, that is, Lemma
D.5. First, we prove the direction from left to right.

input tree $t$$S_{\mathcal{T}}$output tree $s$(output tree $s_{\rho}$
embedded)for the unique $x$with $S_{\mathcal{T}}(x)\in Q$:$\varphi(vx)=u$ in
$\rho$$\varphi(v\bar{x})=\bar{u}$ in $\rho$ for $\bar{x}$with
$S_{\mathcal{T}}(\bar{x})\in Q^{(k)}\setminus Q$$u$$\bar{u}$$v$$vx$$v\bar{x}$
(a) Situation where $S_{O}$ is $\circ$ and $S_{\mathcal{T}}$ is of the form
$w[q_{1}^{(a_{1})}(t_{1}),\dots,q,\dots,q_{n}^{(a_{n})}(t_{n})]$, where $w$ is
a context over $\Gamma^{(k)}\setminus\Gamma$, $q\in Q$, $q_{i}^{(a_{i})}\in
Q^{(k)}\setminus Q$, and $t_{i}\in N_{\Sigma}$ is an input neighborhood for
all $i$. This indicates that $\mathcal{T}$ is ahead compared to Out. The tree
$strip(w)[q_{1},\dots,q,\dots,q_{n}]$ is located at $v$ in $s_{\rho}$. For the
$x\in\mathit{dom}_{S_{\mathcal{T}}}$ with $S_{\mathcal{T}}(x)=q$ holds
$\varphi(vx)=u$, for an $\bar{x}\in\mathit{dom}_{S_{\mathcal{T}}}$ with
$S_{\mathcal{T}}(\bar{x})\in Q^{(k)}\setminus Q$, say $q_{i}^{(a_{i})}$, and
$\varphi(v\bar{x})=\bar{u}$ holds that the distance between $u$ and $\bar{u}$
is $a_{i}$ and $t_{i}$ is located at $\bar{u}$ in $t$.

input tree $t$$S_{O}$output tree $s$(output tree $s_{\rho}$
embedded)$\varphi(v)=u$ in $\rho$$u$$v$ (b) Situation where $S_{O}$ is a
(special) tree (which is not $\circ$) over $\Gamma^{(k)}$ and
$S_{\mathcal{T}}\in Q$. This indicates that Out is ahead compared to
$\mathcal{T}$. The tree $S_{O}$, without annotations and without $\circ$, is
located at $v$ in $s$. The tree $S_{\mathcal{T}}$ is located in $s_{\rho}$ at
$v$.

Figure 10: Visualization of the proof of Lemma G.1. In the run of
$\mathcal{A}$ on
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$, a
node corresponding to some $u\in\mathit{dom}_{t}$ with information
$(f,o,S_{O},S_{\mathcal{T}})$ is reached. There is a (partial) run $\rho$ of
$\mathcal{T}$ on $t$ with (partial output tree) $s_{\rho}$ such that
$s_{\rho}$ (partially) defines the output tree $s$ (this is drawn as the green
part of $s$) and there exists a unique $v\in\mathit{dom}_{s}$ such that the
current configuration of $\mathcal{T}$ satisfies Items 1, 2, 3, 4, 5 and 6;
some of these conditions are visualized.

######  Lemma G.1.

${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}\in
L(\mathcal{A})\Rightarrow(t,s,o)\in_{k}R_{o}(\mathcal{T})\text{ and }o\text{
is a linear transduction}$

######  Proof G.2.

Each reachable (according to the strategies of In and Out) node of
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$ is
identified with a node of the input tree $t$. We show by induction on the
height of a level of the input tree $t$ that the following statement holds:

Fix an accepting run of $\mathcal{A}$ on
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$.
For each level of the input tree $t$, there exists a sequence of
configurations $\rho:\leavevmode\nobreak\
(t,q_{0},\varphi_{0})\leavevmode\nobreak\ \rightarrow_{*}\leavevmode\nobreak\
(t,s_{\rho},\varphi)$ of $\mathcal{T}$ with associated origin function
$o_{\rho}$ that extends the sequence of configurations from the previous level
such that the following conditions are satisfied:

Refer to Figure 10 for a graphical representation of the relation between some
of the mentioned components below. For a reachable (according to the
strategies of In and Out) node of
${\mathsf{H}}^{\mathsf{\frown}}{\mathsf{t}}^{\mathsf{\frown}}{\mathsf{s}}$
that corresponds to a node $u\in\mathit{dom}_{t}$ on that level, that was