11institutetext: Universität Bremen, Germany 22institutetext: TU München,
Germany

# How to decide Functionality of Compositions of Top-Down Tree Transducers

Sebastian Maneth 11 Helmut Seidl 22 Martin Vu 11

###### Abstract

We prove that functionality of compositions of top-down tree transducers is
decidable by reducing the problem to the functionality of one top-down tree
transducer with look-ahead.

##  1 Introduction

Tree transducers are fundamental devices that were invented in the 1970’s in
the context of compilers and mathematical linguistics. Since then they have
been applied in a huge variety of contexts such as, e.g., programming
languages [13], security [10], or XML databases [9].

The perhaps most basic type of tree transducer is the top-down tree transducer
[15, 14] (for short _transducer_). One important decision problem for
transducers concerns _functionality_ : given a (nondeterministic) transducer,
does it realize a function? This problem was shown to be decidable by Ésik [8]
(even in the presence of look-ahead); note that this result also implies the
decidability of equivalence of deterministic transducers [8], see also [7,
11].

A natural and fundamental question is to ask whether functionality can also be
decided for _compositions of transducers_. It is well known that compositions
of transducers form a proper hierarchy, more precisely: compositions of $n+1$
transducers are strictly more expressive than compositions of $n$ transducers
[6]. Even though transducers are well studied, the question of deciding
functionality for compositions of transducers has remained open. In this paper
we fill this gap and show that the question can be answered affirmatively.

Deciding functionality for compositions of transducers has several
applications. For instance, if an arbitrary composition of (top-down and
bottom-up) tree transducers is functional, then an equivalent deterministic
transducer with look-ahead can be constructed [5]. Together with our result
this implies that it is decidable for such a composition whether or not it is
definable by a deterministic transducer with look-ahead; note that the
construction of such a single deterministic transducer improves efficiency,
because it removes the need of computing intermediate results of the
composition. Also other recent definability results can now be generalized to
compositions: for instance, given such a composition we can now decide whether
or not an equivalent linear transducer or an equivalent homomorphism exists
[12] (and if so, construct it).

Let us now discuss the idea of our proof in detail. Initially, we consider a
composition $\tau$ of two transducers $T_{1}$ and $T_{2}$. Given $\tau$, we
construct a ‘candidate’ transducer with look-ahead $M$ with the property that
$M$ is functional if and only if $\tau$ is functional. Our construction of $M$
is an extension of the product construction in [2, p. 195]. The latter
constructs a transducer $N$ (_without_ look-ahead) that is obtained by
translating the right-hand sides of the rules of $T_{1}$ by the transducer
$T_{2}$. It is well-known that in general, the transducer $N$ is _not_
equivalent to $\tau$ [2] and thus $N$ may not be functional even though $\tau$
is. This is due to the fact that the transducer $T_{2}$ may

  * •

copy or

  * •

delete input subtrees.

Copying of an input tree means that the tree is translated several times and
in general by different states. Deletion means that in a translation rule a
particular input subtrees is not translated at all.

Imagine that $T_{2}$ copies and translates an input subtree in two different
states $q_{1}$ and $q_{2}$, so that the domains $D_{1}$ and $D_{2}$ of these
states differ and moreover, $T_{1}$ nondeterministically produces outputs in
the union of $D_{1}$ and $D_{2}$. Now the problem that arises in the product
construction of $N$ is that $N$ needs to guess the output of $T_{1}$, however,
the two states corresponding to $q_{1}$ and $q_{2}$ _cannot_ guarantee that
the same guess is used. However, the same guess may be used. This means that
$N$ (seen as a binary relation) is a superset of $\tau$. To address this
problem we show that it suffices to change $T_{1}$ so that it only outputs
trees in the intersection of $D_{1}$ and $D_{2}$. Roughly speaking this can be
achieved by changing $T_{1}$ so that it runs several tree automata in
parallel, in order to carry out the necessary domain checks.

Imagine now a transducer $T_{1}$ that translates two input subtrees in states
$q_{1}$ and $q_{2}$, respectively, but has no rules for state $q_{2}$. This
means that the translation of $T_{1}$ (and of $\tau$) is empty. However, the
transducer $T_{2}$ deletes the position of $q_{2}$. This causes the
translation of $N$ to be non-empty. To address this problem we equip $N$ with
look-ahead. The look-ahead checks if the input tree is in the domains of all
states of $T_{1}$ translating the current input subtree.

Finally, we are able to generalize the result to arbitrary compositions of
transducers $T_{1},\dots,T_{n}$. For this, we apply the extended composition
described above to the transducers $T_{n-1}$ and $T_{n}$, giving us the
transducer with look-ahead $M$. The look-ahead of $M$ can be removed and
incorporated into the transducer $T_{n-2}$ using a composition result of [2].
The resulting composition of $n-1$ transducers is functional if and only if
the original composition is.

The details of all our proofs can be found in the Appendix.

##  2 Top-Down Tree Transducers

For $k\in\mathbb{N}$, we denote by $[k]$ the set $\\{1,\dots,k\\}$. Let
$\Sigma=\\{e_{1}^{k_{1}},\dots,e_{n}^{k_{n}}\\}$ be a _ranked alphabet_ ,
where $e_{j}^{k_{j}}$ means that the symbol $e_{j}$ has rank $k_{j}$. By
$\Sigma_{k}$ we denote the set of all symbols of $\Sigma$ which have rank $k$.
The set $T_{\Sigma}$ of trees over $\Sigma$ consists of all strings of the
form $a(t_{1},\dots,t_{k})$, where $a\in\Sigma_{k}$, $k\geq 0$, and
$t_{1},\dots,t_{k}\in T_{\Sigma}$. Instead of $a()$ we simply write $a$. We
fix the set $X$ of _variables_ as $X=\\{x_{1},x_{2},x_{3},\dots\\}$.

Let $B$ be an arbitrary set. We define $T_{\Sigma}[B]=T_{\Sigma^{\prime}}$
where $\Sigma^{\prime}$ is obtained from $\Sigma$ by
$\Sigma^{\prime}_{0}=\Sigma_{0}\cup B$ while for all $k>0$,
$\Sigma^{\prime}_{k}=\Sigma_{k}$. In the following, let $A,B$ be arbitrary
sets. We let $A(B)=\\{a(b)\mid a\in A,b\in B\\}$.

###### Definition 1

A _top-down tree transducer_ $T$ (or _transducer_ for short) is a tuple of the
form $T=(Q,\Sigma,\Delta,R,q_{0})$ where $Q$ is a finite set of _states_ ,
$\Sigma$ and $\Delta$ are the _input_ and _output ranked alphabets_ ,
respectively, disjoint with $Q$, $R$ is a _finite set of rules_ , and
$q_{0}\in Q$ is the _initial state_. The rules contained in $R$ are of the
form $q(a(x_{1},\dots,x_{k}))\to t$, where $q\in Q$, $a\in\Sigma_{k}$, $k\geq
0$ and $t$ is a tree in $T_{\Delta}[Q(X)]$.

If $q(a(x_{1},\dots,x_{k}))\to t\in R$ then we call $t$ a right-hand side of
$q$ and $a$. The rules of $R$ are used as rewrite rules in the natural way, as
illustrated by the following example.

###### Example 1

Consider the transducer $T=(\\{q_{0},q\\},\Sigma,\Delta,R,q_{0})$ where
$\Sigma_{0}=\\{e\\}$, $\Sigma_{1}=\\{a\\}$, $\Delta_{0}=\\{e\\}$,
$\Delta_{1}=\\{a\\}$ and $\Delta_{2}=\\{f\\}$ and $R$ consists the following
rules (numbered $1$ to $4$):

$\begin{array}[]{lclclcl}1:\
q_{0}(a(x_{1}))&\rightarrow&f(q(x_{1}),q_{0}(x_{1}))&&2:\
q_{0}(e)&\rightarrow&e\\\ 3:\ q(a(x_{1}))&\rightarrow&a(q(x_{1}))&&4:\
q(e)&\rightarrow&e.\end{array}$

On input $a(a(e))$, the transducer $T$ produces the output tree
$f(a(e),f(e,e))$ as follows

$q_{0}$$a$$a$$e$$1$$f$$q$$a$$e$$q_{0}$$a$$e$$1$$f$$q$$a$$e$$f$$q$$e$$q_{0}$$e$$4$$f$$q$$a$$e$$f$$e$$q_{0}$$e$$3$$f$$a$$q$$e$$f$$e$$q_{0}$$e$$4$$f$$a$$e$$f$$e$$q_{0}$$e$$2$$f$$a$$e$$f$$e$$e$

Informally, when processing a tree $s\in T_{\Sigma}$, the transducer $T$
produces a tree $t$ in which all proper subtrees of $s$ occur as disjoint
subtrees of $t$, ‘ordered’ by size. As the reader may realize, given an input
tree $s$ of size $n$, the transducer $T$ produces an output tree that is of
size $(n^{2}+n)/2$. Hence, this translation has quadratic size increase, i.e.,
the size of the output tree is a most quadratic in size of the input tree.
Note that transducers can have polynomial or exponential size increase [1].
$\hfill\squareforqed$

Let $s\in T_{\Sigma}$. Then $T(s)$ contains all trees in $T_{\Delta}$
obtainable from $q_{0}(s)$ by applying rules of $T$.

Clearly, $T$ defines a binary relation over $T_{\Sigma}$ and $T_{\Delta}$. In
the following, we denote by $\mathcal{R}(T)$ the binary relation that the
transducer $T$ defines. We say that the transducer $T$ is _functional_ if the
relation $\mathcal{R}(T)$ is a function. Let $q$ be a state of $T$. We denote
by $\text{dom}(q)$ the _domain_ of $q$, i.e., the set of all trees $s\in
T_{\Sigma}$ for which some tree $t\in T_{\Delta}$ is obtainable from $q(s)$ by
applying rules of $T$. We define the _domain_ of $T$ by
$\text{dom}(T)=\text{dom}(q_{0})$. For instance in Example 1,
$\text{dom}(T)=T_{\Sigma}$. However, if we remove the rule $1$ for instance
then the domain of $T$ shrinks to the set $\\{e\\}$. We define
$\text{dom}(q)$, the _domain_ of a state $q$ of $T$, analogously.

A transducer $T=(Q,\Sigma,\Delta,R,q)$ is a _top-down tree automaton_ (for
short _automaton_) if $\Sigma=\Delta$ and all rules of $T$ are of the form
$q(a(x_{1},\dots,x_{k}))\rightarrow a(q_{1}(x_{1}),\dots q_{k}(x_{k}))$ where
$a\in\Sigma_{k}$, $k\geq 0$.

Let $T_{1}$ and $T_{2}$ be transducers. As $\mathcal{R}(T_{1})$ and
$\mathcal{R}(T_{2})$ are relations, they can be composed. Hence,

$\mathcal{R}(T_{1})\circ\mathcal{R}(T_{2})=\\{(s,u)\mid\text{for some
}t,(s,t)\in\mathcal{R}(T_{1})\text{ and }(t,u)\in\mathcal{R}(T_{2})\\}.$

If the output alphabet of $T_{1}$ and the input alphabet of $T_{2}$ coincide
then the transducers $T_{1}$ and $T_{2}$ can be composed as well. The
composition $T_{1}\,\hat{\circ}\,T_{2}$ of the transducers $T_{1}$ and $T_{2}$
defines a tree translation as follows. On input $s$, the tree $s$ is first
translated by $T_{1}$. Afterwards, the tree produced by $T_{1}$ is translated
by $T_{2}$ which yields the output tree. Clearly, $T_{1}\,\hat{\circ}\,T_{2}$
computes the relation $\mathcal{R}(T_{1})\circ\mathcal{R}(T_{2})$. We say that
the composition $T_{1}\,\hat{\circ}\,T_{2}$ is _functional_ if the relation
$\mathcal{R}(T_{1})\circ\mathcal{R}(T_{2})$ is a function.

##  3 Functionality of Two-Fold Compositions

In this section we show that for a composition $\tau$ of two transducers, a
transducer $M$ with look-ahead can be constructed such that $M$ is functional
if and only if $\tau$ is functional. Before formally introducing the
construction for $M$ and proving its correctness, we explain how to solve the
challenges described in Section 1, i.e., we show how to handle copying and
deleting rules. In the following, we call the product construction in [2, p.
195] simply the _p-construction_.

To see how precisely we handle copying rules, consider the transducers $T_{1}$
and $T_{2}$. Let the transducer $T_{1}$ consist of the rules

$\begin{array}[]{lclclcl}q_{1}(a(x_{1}))&\rightarrow&b(q_{1}(x_{1}))&&q_{1}(e)&\rightarrow&e_{i}\mid
i=1,2,3\\\ \end{array}$

while transducer $T_{2}$ consist of the rules

$\begin{array}[]{lclclcl}q_{2}(b(x_{1}))&\rightarrow&f(q^{\prime}_{2}(x_{1}),q_{2}^{\prime\prime}(x_{1}))&&q_{2}^{\prime}(e_{j})&\rightarrow&e\mid
j=1,2\\\
q_{2}^{\prime\prime}(e_{3})&\rightarrow&e^{\prime}&&q_{2}^{\prime\prime}(e_{j})&\rightarrow&e\mid
j=1,2.\\\ \end{array}$

The composition $\tau=T_{1}\,\hat{\circ}\,T_{2}$ defines a relation that only
contains a single pair: $\tau$ only translates the tree $a(e)$ into $f(e,e)$.
Therefore, $\tau$ is functional. For $T_{1}$ and $T_{2}$, the p-construction
yields the transducer $N$ with the rules

$\begin{array}[]{lclclcl}(q_{1},q_{2})(a(x_{1}))&\rightarrow&f((q_{1},q^{\prime}_{2})(x_{1}),(q_{1},q_{2}^{\prime\prime})(x_{1}))&&(q_{1},q_{2}^{\prime})(e)&\rightarrow&e\\\
(q_{1},q_{2}^{\prime\prime})(e)&\rightarrow&e^{\prime}&&(q_{1},q_{2}^{\prime\prime})(e)&\rightarrow&e.\\\
\end{array}$

On input $a(e)$, the transducer $N$ can produce either $f(e,e)$ or
$f(e,e^{\prime})$. Therefore, $N$ and $\tau$ are clearly not equivalent.
Furthermore, the transducer $N$ is obviously not functional even though the
composition $\tau$ is.

In order to obtain a better understanding of why this phenomenon occurs, we
analyze the behavior of $N$ and $\tau$ on input $a(e)$ in the following.

In the translation of $\tau$, the states $q_{2}^{\prime}$ and
$q_{2}^{\prime\prime}$ process the same tree produced by $q_{1}$ on input $e$
due to the copying rule $q_{2}(b(x_{1}))\rightarrow
f(q^{\prime}_{2}(x_{1}),q_{2}^{\prime\prime}(x_{1}))$. Furthermore,
$q_{2}^{\prime}$ and $q_{2}^{\prime\prime}$ process a tree in
$\text{dom}(q_{2}^{\prime})\cap\text{dom}(q_{2}^{\prime\prime})$. More
precisely, $q_{2}^{\prime}$ and $q_{2}^{\prime\prime}$ both process either
$e_{1}$ or $e_{2}$.

In the translation of $N$ on the other hand, due to the rule
$(q_{1},q_{2})(a(x_{1}))\rightarrow
f((q_{1},q^{\prime}_{2})(x_{1}),(q_{1},q_{2}^{\prime\prime})(x_{1}))$, the
states $(q_{1},q_{2}^{\prime})$ and $(q_{1},q_{2}^{\prime\prime})$ process $e$
by ‘guessing independently’ from each other what $q_{1}$ might have produced
on input $e$. In particular, the problem is that
$(q_{1},q_{2}^{\prime\prime})$ can apply the rule
$(q_{1},q_{2}^{\prime\prime})(e)\rightarrow e^{\prime}$ which eventually leads
to the production of $f(e,e^{\prime})$. Applying this rule means that
$(q_{1},q_{2}^{\prime\prime})$ guesses that $e_{3}$ is produced by $q_{1}$.
While this guess is valid, i.e., $e_{3}$ is producible by $q_{1}$ on input
$e$, quite clearly $e_{3}\notin\text{dom}(q_{2}^{\prime})$.

In general, guesses performed by states of $N$ cannot be ‘synchronized’, i.e.,
we cannot guarantee that states guess the same tree. Our solution to fix this
issue is to restrict $(q_{1},q_{2}^{\prime})$ and
$(q_{1},q_{2}^{\prime\prime})$ such that either state is only allowed to guess
trees in $\text{dom}(q_{2}^{\prime})\cap\text{dom}(q_{2}^{\prime\prime})$. To
understand why this approach works in general consider the following example.

###### Example 2

Let ${T}_{1}$ and ${T}_{2}$ be arbitrary transducers. Let
${\tau}={T}_{1}\,\hat{\circ}\,{T}_{2}$ be functional. Let ${T}_{1}$ on input
$s$ produce either $b(t_{1})$ or $b(t_{2})$. Let ${T}_{2}$ contain the rule

$q_{2}(b(x_{1}))\rightarrow f(q_{2}^{1}(x_{1}),q_{2}^{2}(x_{1}))$

where $q_{2}$ is the initial state of ${T}_{2}$. The application of this rule
effectively means that the states $q_{2}^{1}$ and $q_{2}^{2}$ process the same
subtree produced by ${T}_{1}$. Let
$t_{1},t_{2}\in\text{dom}(q_{2}^{1})\cap\text{dom}(q_{2}^{2})$. Informally
speaking, it does not matter whether the state $q_{2}^{1}$ processes $t_{1}$
or $t_{2}$; for either input $q_{2}^{1}$ produces the same output tree $r$ and
nothing else, otherwise, the functionality of $\tau$ is contradicted. The same
holds for $q_{2}^{2}$. $\hfill\squareforqed$

Informally, Example 2 suggests that if $(q_{1},q_{2}^{\prime\prime})$ and
$(q_{1},q_{2}^{\prime\prime})$ only guess trees in
$\text{dom}(q_{2}^{\prime})\cap\text{dom}(q_{2}^{\prime\prime})$, then it does
not matter which tree exactly those states guess if the composition is
functional. The final result in either case is the same. Quite clearly this is
the case in our example. (In effect, $q_{2}^{\prime\prime}$ is forbidden to
guess $e_{3}$.) Thus, restricting $(q_{1},q_{2}^{\prime})$ and
$(q_{1},q_{2}^{\prime\prime})$ basically achieves the same result as
synchronizing their guesses if the composition is functional.

Now the question is how exactly do we restrict the states of $N$? Consider the
states $(q_{1},q_{2}^{\prime})$ and $(q_{1},q_{2}^{\prime\prime})$ of $N$ in
our example. The trick is to restrict $q_{1}$ such that $q_{1}$ can only
produce trees in
$\text{dom}(q_{2}^{\prime})\cap\text{dom}(q_{2}^{\prime\prime})$. Thus any
guess is guaranteed to be in
$\text{dom}(q_{2}^{\prime})\cap\text{dom}(q_{2}^{\prime\prime})$. In order to
restrict which output trees $T_{1}$ can produce, we compose $T_{1}$ with the
_domain automaton_ of $T_{2}$.

For an arbitrary transducer $T=(Q,\Sigma,\Delta,R,q)$, the _domain automaton_
$A$ of $T$ is constructed analogous to the automaton in [4, Theorem 3.1]. The
set of states of $A$ is the power set of ${Q}$ where $\\{q\\}$ is the initial
state of $A$. The idea is that if in a translation of $T$ on input $s$, the
states $q_{1}\dots,q_{n}$ process the node $v$ of $s$ then
$\\{q_{1}\dots,q_{n}\\}$ processes the node $v$ of $s$ in a computation of
$A$. The rules of $A$ are thus defined as follows.

Let $S=\\{q_{1}\dots,q_{n}\\}$, $n>0$, and $a\in\Sigma_{k}$. In the following,
we denote by $\text{rhs}_{T}(q_{j},a)$, where $j\in[n]$, the set of all right-
hand sides of $q_{j}$ and $a$. For all non-empty subsets
$\Gamma_{1}\subseteq\text{rhs}_{T}(q_{1},a),\dots,\Gamma_{n}\subseteq\text{rhs}_{T}(q_{n},a)$,
we define a rule

$S(a(x_{1},\dots,x_{k}))\rightarrow a(S_{1}(x_{1}),\dots,S_{k}(x_{k}))$

where for $i\in[k]$, $S_{i}$ is defined as the set
$\bigcup_{j=1}^{n}\Gamma_{j}\langle x_{i}\rangle$. We denote by
$\Gamma_{j}\langle x_{i}\rangle$ the set of all states $q^{\prime}$ such that
$q^{\prime}(x_{i})$ occurs in some tree $\gamma$ in $\Gamma_{j}$; e.g., for

$\Gamma_{j}=\\{a(q(x_{1}),q^{\prime}(x_{2})),\
a(a(q_{1}(x_{1}),q_{2}(x_{2})),q_{3}(x_{1}))\\},$

we have $\Gamma_{j}\langle x_{1}\rangle=\\{q,q_{1},q_{3}\\}$ and
$\Gamma_{j}\langle x_{2}\rangle=\\{q^{\prime},q_{2}\\}$. We define that the
state $\emptyset$ of $A$ realizes the identity. Hence, the rules for the state
$\emptyset$ are defined in the obvious way.

We now explain why subsets $\Gamma_{j}$ of right-hand sides are used for the
construction of rules of $A$. Recall that the idea is that if in a translation
of $T$ on input $s$, the states $q_{1}\dots,q_{n}$ process the node $v$ of $s$
then $\\{q_{1}\dots,q_{n}\\}$ processes the node $v$ of $s$ in a computation
of $A$. Due to copying rules, multiple instances of a state $q_{1}$ may access
$v$. Two instance of $q_{1}$ may process $v$ in different manners. This
necessitates the use of subsets $\Gamma_{j}$ of right-hand sides. For a better
understanding, consider the following example.

###### Example 3

Let $T=(\\{q_{0},q\\},\Sigma,\Delta,R,q_{0})$ where
$\Sigma_{0}=\Delta_{0}=\\{e\\}$, $\Sigma_{1}=\Delta_{1}=\\{a\\}$ and
$\Sigma_{2}=\Delta_{2}=\\{f\\}$. The set $R$ contains the following rules:

$\begin{array}[]{lclclcl}q_{0}(a(x_{1}))&\rightarrow&f(q_{0}(x_{1}),q_{0}(x_{1}))&&q(a(x_{1}))&\rightarrow&e^{\prime}\\\
q_{0}(f(x_{1},x_{2}))&\rightarrow&q_{0}(x_{1})&&q(f(x_{1},x_{2}))&\rightarrow&e^{\prime}\\\
q_{0}(f(x_{1},x_{2}))&\rightarrow&f(q(x_{1}),q(x_{2}))&&q(e)&\rightarrow&e^{\prime}\\\
q_{0}(e)&\rightarrow&e.\\\ \end{array}$

Consider the input tree $s=a(f(e,e))$. Clearly, on input $s$, the tree
$f(e,f(e^{\prime},e^{\prime}))$ is producible by $T$. In this translation, two
instances of the state $q_{0}$ process the subtree $f(e,e)$ of $s$, however
the instances of $q_{0}$ do not process $f(e,e)$ in the same way. The first
instance of $q_{0}$ produces $e$ on input $f(e,e)$ while the second instance
produces $f(e^{\prime},e^{\prime})$. These translations mean that the states
$q_{0}$ and $q$ process the leftmost $e$ of $s$.

Consider the domain automaton $A$ of $T$. By definition, $A$ contains the rule
$\\{q_{0}\\}(a(x_{1}))\rightarrow a(\\{q_{0}\\}(x_{1}))$ which is obtained
from the right-hand side of the rule $q_{0}(a(x_{1}))\rightarrow
f(q_{0}(x_{1}),q_{0}(x_{1}))$ of $T$. To simulate that the states $q_{0}$ and
$q$ process the leftmost $e$ of $s$ in the translation from $s$ to
$f(e,f(e^{\prime},e^{\prime}))$, we clearly require the rule
$\\{q_{0}\\}(f(x_{1},x_{2}))\rightarrow
f(\\{q_{0},q\\}(x_{1}),\\{q\\}(x_{2}))$ obtained from the right-hand sides of
the rules $q_{0}(f(x_{1},x_{2})\rightarrow q_{0}(x_{1})$ and
$q_{0}(f(x_{1},x_{2})\rightarrow f(q(x_{1}),q(x_{2}))$ of $T$.

For completeness, we list the remaining rules of $A$. The automaton $A$ also
contains the rules

$\begin{array}[]{rlclcrlcl}\\{q_{0}\\}&(f(x_{1},x_{2}))&\rightarrow&f(\\{q\\}(x_{1}),\\{q\\}(x_{2}))&&\\{q\\}&(a(x_{1}))&\rightarrow&a(\emptyset(x_{1}))\\\
\\{q_{0}\\}&(f(x_{1},x_{2}))&\rightarrow&f(\\{q_{0}\\}(x_{1}),\emptyset(x_{2}))&&\\{q\\}&(f(x_{1},x_{2}))&\rightarrow&f(\emptyset(x_{1}),\emptyset(x_{2}))\\\
\\{q_{0}\\}&(e)&\rightarrow&e&&\\{q\\}&(e)&\rightarrow&e.\\\
\emptyset&(f(x_{1},x_{2}))&\rightarrow&f(\emptyset(x_{1}),\emptyset(x_{2}))&&\emptyset&(a(x_{1}))&\rightarrow&a(\emptyset(x_{1}))\\\
\emptyset&(e)&\rightarrow&e.\\\ \end{array}$

For the rules of the state $\\{q_{0},q\\}$ consider the following. The right-
hand sides of rules of $\\{q_{0},q\\}$ are identical to the right-hand sides
of rules of $\\{q_{0}\\}$, i.e., the rules for $\\{q_{0},q\\}$ are obtained by
substituting $\\{q_{0}\\}$ on the left-hand-side of rules of $A$ by
$\\{q_{0},q\\}$. $\hfill\squareforqed$

The automaton $A$ has the following property.

###### Lemma 1

Let $S\neq\emptyset$ be a state of $A$. Then $s\in\text{dom}(S)$ if and only
if $s\in\bigcap_{q\in S}\text{dom}(q)$.

Obviously, Lemma 1 implies that $A$ recognizes the domain of $T$.

Using the domain automaton $A$ of $T_{2}$, we transform $T_{1}$ into the
transducer $\hat{T}_{1}$. Formally, the transducer $\hat{T}_{1}$ is obtained
from $T_{1}$ and $A$ using the p-construction. In our example, the transducer
$\hat{T}_{1}$ obtained from $T_{1}$ and $T_{2}$ includes the following rules

$\begin{array}[]{rlcl}(q_{1},\\{q_{2}\\})&(a(x_{1}))&\rightarrow&b((q_{1},\\{q_{2}^{\prime},q_{2}^{\prime\prime}\\})(x_{1}))\\\
(q_{1},\\{q_{2}^{\prime},q_{2}^{\prime\prime}\\})&(e)&\rightarrow&e_{j}\\\
\end{array}$

where $j=1,2$. The state $(q_{1},\\{q_{2}\\})$ is the initial state of
$\hat{T}_{1}$. Informally, the idea is that in a translation of
$\hat{\tau}=\hat{T}_{1}\,\hat{\circ}\,T_{2}$, a tree produced by a state
$(q,S)$ of $\hat{T}_{1}$ is only processed by states in $S$. The following
result complements this idea.

###### Lemma 2

If the state $(q,S)$ of $\hat{T}_{1}$ produces the tree $t$ and
$S\neq\emptyset$ then $t\in\bigcap_{q_{2}\in S}\text{dom}(q_{2})$.

We remark that if a state of the form $(q,\emptyset)$ occurs then it means
that in a translation of $\hat{\tau}$, no state of $T_{2}$ will process a tree
produced by $(q,\emptyset)$. Note that as $A$ is nondeleting and linear,
$\hat{T}_{1}$ defines the same relation as $T_{1}\,\hat{\circ}\,A$ [2, Th. 1].
Informally, the transducer $\hat{T}_{1}$ is a restriction of the transducer
$T_{1}$ such that
$\text{range}(\hat{T}_{1})=\text{range}(T_{1})\cap\text{dom}(T_{2})$.
Therefore, the following holds.

###### Lemma 3

$\mathcal{R}(T_{1})\circ\mathcal{R}(T_{2})=\mathcal{R}(\hat{T}_{1})\circ\mathcal{R}(T_{2})$.

Due to Lemma 3, we focus on $\hat{T}_{1}$ instead of $T_{1}$ in the following.

Consider the transducer $\hat{N}$ obtained from $\hat{T}_{1}$ and $T_{2}$
using the p-construction. By construction, the states of $\hat{N}$ are of the
form $((q,S),q^{\prime})$ where $(q,S)$ is a state of $\hat{T}_{1}$ and
$q^{\prime}$ is a state of $T_{2}$. In the following, we write
$(q,S,q^{\prime})$ instead for better readability. Informally, the state
$(q,S,q^{\prime})$ implies that in a translation of $\hat{\tau}$ the state
$q^{\prime}$ is supposed to process a tree produced by $(q,S)$. Because trees
produced by $(q,S)$ are only supposed to be processed by states in $S$, we
only consider states $(q,S,q^{\prime})$ where $q^{\prime}\in S$. For
$\hat{T}_{1}$ and $T_{2}$, we obtain the transducer $\hat{N}$ with the
following rules

$\begin{array}[]{rlcl}(q_{1},\\{q_{2}\\},q_{2})&(a(x_{1}))&\rightarrow&f((q_{1},S,q_{2}^{\prime})(x_{1}),(q_{1},S,q_{2}^{\prime\prime})(x_{1}))\\\
(q_{1},S,q_{2}^{\prime})&(e)&\rightarrow&e\\\
(q_{1},S,q_{2}^{\prime\prime})&(e)&\rightarrow&e\\\ \end{array}$

where $S=\\{q_{2}^{\prime},q_{2}^{\prime\prime}\\}$ and $i=1,2$. The initial
state of $\hat{N}$ is $(q_{1},\\{q_{2}\\},q_{2})$. Obviously, $\hat{N}$
computes the relation $\mathcal{R}(T_{1})\circ\mathcal{R}(T_{2})$.

In the following, we briefly explain our idea. In a translation of $\hat{N}$
on input $a(e)$, the subtree $e$ is processed by $(q_{1},S,q_{2}^{\prime})$
and $(q_{1},S,q_{2}^{\prime\prime})$. Note that in a translation of
$\hat{\tau}$ the states $q_{2}^{\prime}$ and $q_{2}^{\prime\prime}$ would
process the same tree produced by $(q_{1},S)$ on input $e$. Consider the state
$(q_{1},S,q_{2}^{\prime\prime})$. If $(q_{1},S,q_{2}^{\prime\prime})$, when
reading $e$, makes a _valid_ guess, i.e., $(q_{1},S,q_{2}^{\prime\prime})$
guesses a tree $t$ that is producible by $(q_{1},S)$ on input $e$, then
$t\in\text{dom}(q_{2}^{\prime})$ by construction of $\hat{T}_{1}$. Due to
previous considerations (cf. Example 2), it is thus sufficient to ensure that
all guesses of states of $\hat{N}$ are valid. While obviously in the case of
$\hat{N}$, all guesses are indeed valid, guesses of transducers obtained from
the p-construction are in general not always valid; in particular if _deleting
rules_ are involved.

To be more specific, consider the following transducers $T_{1}^{\prime}$ and
$T_{2}^{\prime}$. Let $T^{\prime}_{1}$ contain the rules

$\begin{array}[]{lclclcl}q_{1}(a(x_{1},x_{2}))&\rightarrow&b(q^{\prime}_{1}(x_{1}),q_{1}^{\prime\prime}(x_{2}),q_{1}^{\prime\prime\prime}(x_{2}))&&q^{\prime}_{1}(e)&\rightarrow&e\\\
\end{array}$

where $\text{dom}(q_{1}^{\prime\prime})$ consists of all trees whose left-most
leaf is labeled by $e$ while $\text{dom}(q_{1}^{\prime\prime\prime})$ consists
of all trees whose left-most leaf is labeled by $c$. Let $T^{\prime}_{2}$
contain the rules

$\begin{array}[]{lclclcl}q_{2}(b(x_{1},x_{2},x_{3}))&\rightarrow&q_{2}(x_{1})&&q_{2}(e)&\rightarrow&e_{j}\mid
j=1,2.\\\ \end{array}$

As the translation of $T^{\prime}_{1}$ is empty, obviously the translation of
$\tau^{\prime}=T^{\prime}_{1}\,\hat{\circ}\,T^{\prime}_{2}$ is empty as well.
Thus, $\tau^{\prime}$ is functional. However, the p-construction yields the
transducer $N^{\prime}$ with the rules

$\begin{array}[]{lclclcl}(q_{1},q_{2})(a(x_{1},x_{2}))&\rightarrow&(q_{1}^{\prime},q_{2})(x_{1})&&(q^{\prime}_{1},q_{2})(e)&\rightarrow&e_{j}\mid
j=1,2\\\ \end{array}$

Even though $\tau^{\prime}=T_{1}^{\prime}\,\hat{\circ}\,T_{2}^{\prime}$ is
functional, the transducer $N^{\prime}$ is not. More precisely, on input
$a(e,s)$, where $s$ is an arbitrary tree, $N^{\prime}$ can produce either
$e_{1}$ or $e_{2}$ while $\tau^{\prime}$ would produce nothing. The reason is
that in the translation of $N^{\prime}$, the tree $a(e,s)$ is processed by the
state $(q_{1},q_{2})$ by applying the deleting rule
$\eta=(q_{1},q_{2})(a(x_{1},x_{2}))\rightarrow(q_{1}^{\prime},q_{2})(x_{1})$.
Applying $\eta$ means that $(q_{1},q_{2})$ guesses that on input $a(e,s)$, the
state $q_{1}$ produces a tree of the form $b(t_{1},t_{2},t_{3})$ by applying
the rule $q_{1}(a(x_{1},x_{2}))\rightarrow
b(q^{\prime}_{1}(x_{1}),q_{1}^{\prime\prime}(x_{2}),q_{1}^{\prime\prime\prime}(x_{2}))$
of $T_{1}$. However, this guess is not valid, i.e., $q_{1}$ does not produce
such a tree on input $a(e,s)$, as by definition
$s\notin\text{dom}(q_{1}^{\prime\prime})$ or
$s\notin\text{dom}(q_{1}^{\prime\prime\prime})$. The issue is that
$N^{\prime}$ itself cannot verify the validity of this guess because, due to
the deleting rule $\eta$, $N^{\prime}$ does not read $s$.

As the reader might have guessed our idea is that the validity of each guess
is verified using look-ahead. First, we need to define look-ahead.

A _transducer with look-ahead_ (or _la-transducer_) $M^{\prime}$ is a
transducer that is equipped with an automaton called the _la-automaton_.
Formally, $M^{\prime}$ is a tuple $M^{\prime}=(Q,\Sigma,\Delta,R,q,B)$ where
$Q$, $\Sigma$, $\Delta$ and $q$ are defined as for transducers and $B$ is the
la-automaton. The rules of $R$ are of the form
$q(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\to t$ where for $i\in[k]$, $l_{i}$
is a state of $B$. Consider the input $s$. The la-transducer $M^{\prime}$
processes $s$ in two phases: First each input node of $s$ is annotated by the
states of $B$ at its children, i.e., an input node $v$ labeled by
$a\in\Sigma_{k}$ is relabeled by $\langle a,l_{1},\dots,l_{k}\rangle$ if $B$
arrives in the state $l_{i}$ when processing the $i$-th subtree of $v$.
Relabeling the nodes $s$ provides $M^{\prime}$ with additional information
about the subtrees of $s$, e.g., if the node $v$ is relabeled by $\langle
a,l_{1},\dots,l_{k}\rangle$ then the $i$-th subtree of $v$ is a tree in
$\text{dom}(l_{i})$. The relabeled tree is then processed by $M^{\prime}$. To
this end a rule $q(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\to t$ is
interpreted as $q(\langle a,l_{1},\dots,l_{k}\rangle(x_{1},\dots,x_{k}))\to
t$.

In our example, the idea is to equip $N^{\prime}$ with an la-automaton to
verify the validity of guesses. In particular, the la-automaton is the domain
automaton $A^{\prime}$ of $T_{1}^{\prime}$. Recall that a state of
$A^{\prime}$ is a set consisting of states of $T_{1}^{\prime}$. To process
relabeled trees the rules of $N^{\prime}$ are as follows

$\begin{array}[]{lclclcl}(q_{1},q_{2})(a(x_{1}\\!:\\{q_{1}^{\prime}\\},x_{2}\\!:\\{q_{1}^{\prime\prime},q_{1}^{\prime\prime}\\}))&\rightarrow&(q_{1}^{\prime},q_{2})(x_{1})&&(q^{\prime}_{1},q_{2})(e)&\rightarrow&e_{j}\mid
j=1,2\\\ \end{array}$

Consider the tree $a(e,s)$, where $s$ is an arbitrary tree. The idea is that
if the root of $a(e,s)$ is relabeled by $\langle
a,\\{q_{1}^{\prime}\\},\\{q_{1}^{\prime\prime},q_{1}^{\prime\prime\prime}\\}\rangle$,
then due to Lemma 1, $e\in\text{dom}(q_{1}^{\prime})$ and
$s\in\text{dom}(q_{1}^{\prime\prime})\cap\text{dom}(q_{1}^{\prime\prime})$ and
thus on input $a(e,s)$ a tree of the form $b(t_{1},t_{2},t_{3})$ is producible
by $q_{1}$ using the rule $q_{1}(a(x_{1},x_{2}))\rightarrow
b(q^{\prime}_{1}(x_{1}),q_{1}^{\prime\prime}(x_{2}),q_{1}^{\prime\prime\prime}(x_{2}))$.
Quite clearly, the root of $a(e,s)$ is _not_ relabeled. Thus, the translation
of $N^{\prime}$ equipped with the la-automaton $A^{\prime}$ is empty as the
translation of $\tau^{\prime}$ is.

###  3.1 Construction of the LA-Transducer $M$

Recall that for a a composition $\tau$ of two transducers $T_{1}$ and $T_{2}$,
we aim to construct an la-transducer $M$ such that $M$ is functional if and
only if $\tau$ is functional.

In the following we show that combining the ideas presented above yields the
la-transducer $M$. For $T_{1}$ and $T_{2}$, we obtain $M$ by first completing
the following steps.

  1. 1.

Construct the domain automaton $A$ of $T_{2}$

  2. 2.

Construct the transducer $\hat{T}_{1}$ from $T_{1}$ and $A$ using the
p-construction

  3. 3.

Construct the transducer $N$ from $\hat{T}_{1}$ and $T_{2}$ using the
p-construction

We then obtain $M$ by extending $N$ into a transducer with look-ahead. Note
that the states of $N$ are written as $(q,S,q^{\prime})$ instead of
$((q,S),q^{\prime})$ for better readability, where $(q,S)$ is a state of
$\hat{T}_{1}$ and $q^{\prime}$ is a state of $T_{2}$. Recall that
$(q,S,q^{\prime})$ means that $q^{\prime}$ is supposed to process a tree
generated by $(q,S)$. Furthermore, recall that $S$ is a set of states of
$T_{2}$ and that the idea is that trees produced by $(q,S)$ are only supposed
to be processed by states in $S$. Thus, we only consider states
$(q,S,q^{\prime})$ of $N$ where $q^{\prime}\in S$.

The transducer $M$ with look-ahead is constructed as follows. The set of
states of $M$ and the initial state of $M$ are the states of $N$ and the
initial state of $N$, respectively. The la-automaton of $M$ is the domain
automaton $\hat{A}$ of $\hat{T}_{1}$.

We now define the rules of $M$. First, recall that a state of $\hat{A}$ is a
set consisting of states of $\hat{T}_{1}$. Furthermore, recall that for a set
of right-hand sides $\Gamma$ and a variable $x$, we denote by $\Gamma\langle
x\rangle)$ the set of all states $q$ such that $q(x)$ occurs in some
$\gamma\in\Gamma$. For a right-hand side $\gamma$, the set $\gamma\langle
x\rangle$ is defined analogously. For all rules

$\eta=(q,S,q^{\prime})(a(x_{1},\dots,x_{k}))\rightarrow\gamma$

of $N$ we proceed as follows: If $\eta$ is obtained from the rule
$(q,S)(a(x_{1},\dots,x_{k}))\rightarrow\xi$ of $\hat{T}_{1}$ and subsequently
translating $\xi$ by the state $q^{\prime}$ of $T_{2}$ then we define the rule

$(q,S,q^{\prime})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma$

for $M$ where for $i\in[k]$, $l_{i}$ is a state of $\hat{A}$ such that
$\xi\langle x_{i}\rangle\subseteq l_{i}$. Recall that relabeling a node $v$,
that was previously labeled by $a$, by $\langle a,l_{1},\dots,l_{k}\rangle$
means that the $i$-th subtree of $v$ is a tree in $\text{dom}(l_{i})$. By
Lemma 1, $s\in\text{dom}(l_{i})$ if and only if $s\in\bigcap_{\hat{q}\in
l_{i}}\text{dom}(\hat{q})$. Thus, if the node $v$ of a tree $s$ is relabeled
by $\langle a,l_{1},\dots,l_{k}\rangle$ then it means that $(q,S)$ can process
subtree of $s$ rooted at $v$ using the rule
$(q,S)(a(x_{1},\dots,x_{k}))\rightarrow\xi$.

In the following, we present a detailed example for the construction of $M$
for two transducers $T_{1}$ and $T_{2}$.

###### Example 4

Let the transducer $T_{1}$ contain the rules

$\begin{array}[]{lclclcl}q_{0}(f(x_{1},x_{2}))&\rightarrow&f(q_{1}(x_{1}),q_{2}(x_{2}))&&q_{0}(f(x_{1},x_{2}))&\rightarrow&q_{3}(x_{2})\\\
q_{2}(f(x_{1},x_{2}))&\rightarrow&f(q_{2}(x_{1}),q_{1}(x_{2}))&&q_{1}(f(x_{1},x_{2}))&\rightarrow&f(q_{1}(x_{1}),q_{1}(x_{2}))\\\
q_{2}(f(x_{1},x_{2}))&\rightarrow&f^{\prime}(q_{2}(x_{1}),q_{1}(x_{2}))&&q_{1}(f(x_{1},x_{2}))&\rightarrow&f^{\prime}(q_{1}(x_{1}),q_{1}(x_{2}))\\\
q_{2}(e)&\rightarrow&e&&q_{1}(e)&\rightarrow&e\\\
q_{3}(d)&\rightarrow&d&&q_{1}(d)&\rightarrow&d\end{array}$

and let the initial state of $T_{1}$ be $q_{0}$. Informally, when reading the
symbol $f$, the states $q_{1}$ and $q_{2}$ nondeterministically decide whether
or not to relabel $f$ by $f^{\prime}$. However, the domain of $q_{2}$ only
consists of trees whose leftmost leaf is labeled by $e$. The state $q_{3}$
only produces the tree $d$ on input $d$. Thus, the domain of $T_{1}$ only
consists of trees of the form $f(s_{1},s_{2})$ where $s_{1}$ and $s_{2}$ are
trees and either the leftmost leaf of $s_{2}$ is $e$ or $s_{2}=d$.

The initial state of the transducer $T_{2}$ is $\hat{q}_{0}$ and $T_{2}$
contains the rules

$\begin{array}[]{lclclcl}\hat{q}_{0}(f(x_{1},x_{2}))&\rightarrow&f(\hat{q}_{1}(x_{1}),\hat{q}_{2}(x_{1}))&&\hat{q}_{1}(f(x_{1},x_{2}))&\rightarrow&f(\hat{q}_{1}(x_{1}),\hat{q}_{1}(x_{2}))\\\
\hat{q}_{0}(d)&\rightarrow&d&&\hat{q}_{1}(f^{\prime}(x_{1},x_{2}))&\rightarrow&f^{\prime}(\hat{q}_{1}(x_{1}),\hat{q}_{2}(x_{2}))\\\
\hat{q}_{2}(f(x_{1},x_{2}))&\rightarrow&f(\hat{q}_{2}(x_{1}),\hat{q}_{2}(x_{2}))&&\hat{q}_{1}(e)&\rightarrow&e\\\
\hat{q}_{2}(e)&\rightarrow&e&&\hat{q}_{1}(d)&\rightarrow&d\\\
\hat{q}_{2}(d)&\rightarrow&d.\\\ \end{array}$

Informally, on input $s$, the state $\hat{q}_{2}$ produces $s$ if the symbol
$f^{\prime}$ does not occur in $s$; otherwise $\hat{q_{2}}$ produces no
output. The state $\hat{q}_{1}$ realizes the identity. Hence, the domain of
$T_{2}$ only consists of the tree $d$ and trees $f(s_{1},s_{2})$ with no
occurrences of $f^{\prime}$ in $s_{1}$.

Consider the composition $\tau=T_{1}\,\hat{\circ}\,T_{2}$. On input $s$, the
composition $\tau$ yields $f(s_{1},s_{1})$ if $s$ is of the form
$f(s_{1},s_{2})$ and the leftmost leaf of $s_{2}$ is labeled by $e$. If the
input tree is of the form $f(s_{1},d)$, the output tree $d$ is produced.
Clearly, $\tau$ is functional. We remark that both phenomena described in
Section 3 occur in the composition $\tau$. More precisely, simply applying the
p-construction to $T_{1}$ and $T_{2}$ yields a nondeterministic transducer due
to ‘independent guessing’. Furthermore, not checking the validity of guesses
causes nondeterminism on input $f(s_{1},d)$.

In the following, we show how to construct the la-automaton $M$ from the
transducers $T_{1}$ and $T_{2}$.

Construction of the domain automaton $\mathbf{A}$. We begin by constructing
the domain automaton $A$ of $T_{2}$. The set of states of $A$ is the power set
of the set of states of $T_{2}$ and the initial state of $A$ is
$\\{\hat{q}_{0}\\}$. The rules of $A$ are

$\begin{array}[]{rlclc
rlcl}\\{\hat{q}_{0}\\}&(f(x_{1},x_{2}))&\rightarrow&f(S(x_{1}),\emptyset(x_{2}))\\\
\\{\hat{q}_{0}\\}&(d)&\rightarrow&d\\\
S&(f(x_{1},x_{2}))&\rightarrow&f(S(x_{1}),S(x_{2}))\\\ S&(e)&\rightarrow&e\\\
S&(d)&\rightarrow&d\\\ \end{array}$

where $S=\\{\hat{q}_{1},\hat{q_{2}}\\}$. The state $\emptyset$ realizes the
identity. The rules for the state $\emptyset$ are straight forward and hence
omitted here. All remaining states, such as for instance
$\\{\hat{q}_{0},\hat{q}_{1}\\}$, are unreachable and hence the corresponding
rules are irrelevant. Thus, we omit these rules as well. In the following, we
only consider rules of states that are reachable.

Construction of the transducer $\mathbf{\hat{T}_{1}}$. For $T_{1}$ and $A$,
the p-construction yields the transducer $\hat{T}_{1}$. The transducer
$\hat{T}_{1}$ contains the rules

$\begin{array}[]{rlcl c
rlcl}(q_{0},\\{\hat{q}_{0}\\})&(f(x_{1},x_{2}))&\rightarrow&f((q_{1},S)(x_{1}),q_{2}(x_{2}))\\\
(q_{0},\\{\hat{q}_{0}\\})&(f(x_{1},x_{2}))&\rightarrow&(q_{3},\\{\hat{q}_{0}\\})(x_{2})\vspace{0.12cm}\\\
q_{1}&(f(x_{1},x_{2}))&\rightarrow&f(q_{1}(x_{1}),q_{1}(x_{2}))\\\
q_{1}&(f(x_{1},x_{2}))&\rightarrow&f^{\prime}(q_{1}(x_{1}),q_{1}(x_{2}))\\\
q_{1}&(e)&\rightarrow&e\\\ q_{1}&(d)&\rightarrow&d\vspace{0.12cm}\\\
(q_{1},S)&(f(x_{1},x_{2}))&\rightarrow&f((q_{1},S)(x_{1}),(q_{1},S)(x_{2}))\\\
(q_{1},S)&(e)&\rightarrow&e\\\ (q_{1},S)&(d)&\rightarrow&d\vspace{0.12cm}\\\
q_{2}&(f(x_{1},x_{2}))&\rightarrow&f(q_{2}(x_{1}),q_{1}(x_{2}))\\\
q_{2}&(f(x_{1},x_{2}))&\rightarrow&f^{\prime}(q_{2}(x_{1}),q_{1}(x_{2}))\\\
q_{2}&(e)&\rightarrow&e\vspace{0.12cm}\\\
(q_{3},\\{\hat{q}_{0}\\})&(d)&\rightarrow&d\\\ \end{array}$

and the initial state of $\hat{T}_{1}$ is $(q_{0},\\{\hat{q}_{0}\\})$. For
better readability, we just write $q_{1}$ and $q_{2}$ instead of
$(q_{1},\emptyset)$ and $(q_{2},\emptyset)$, respectively.

Construction of the transducer $\mathbf{N}$. For $\hat{T_{1}}$ and $T_{2}$, we
construct the transducer $N$ containing the rules

$\begin{array}[]{rlclcrlcl}(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})&(f(x_{1},x_{2}))&\rightarrow&f((q_{1},S,\hat{q}_{1})(x_{1}),(q_{1},S,\hat{q}_{2})(x_{1}))\\\
(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})&(f(x_{1},x_{2}))&\rightarrow&(q_{3},\\{\hat{q}_{0}\\},\hat{q}_{0})(x_{2})\vspace{0.12cm}\\\
(q_{1},S,\hat{q}_{1})&(f(x_{1},x_{2}))&\rightarrow&f((q_{1},S,\hat{q}_{1})(x_{1}),(q_{1},S,\hat{q}_{1})(x_{2}))\\\
(q_{1},S,\hat{q}_{1})&(e)&\rightarrow&e\\\
(q_{1},S,\hat{q}_{1})&(d)&\rightarrow&d\vspace{0.12cm}\\\
(q_{1},S,\hat{q}_{2})&(f(x_{1},x_{2}))&\rightarrow&f((q_{1},S,\hat{q}_{2})(x_{1}),(q_{1},S,\hat{q}_{2})(x_{2}))\\\
(q_{1},S,\hat{q}_{2})&(e)&\rightarrow&e\\\
(q_{1},S,\hat{q}_{2})&(d)&\rightarrow&d\vspace{0.12cm}\\\
(q_{3},\\{\hat{q}_{0}\\},\\{\hat{q}_{0}\\})&(d)&\rightarrow&d\\\ \end{array}$

The initial state of $N$ is $(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})$. Note that
the states such as $(q_{1},S,\hat{q}_{0})$ are not considered as $\hat{q}_{0}$
is not contained in $S$. We remark that though no nondeterminism is caused by
‘independent guessing’, $N$ is still nondeterministic on input $f(s_{1},d)$ as
the validity of guesses cannot be checked. To perform validity checks for
guesses, we extend $N$ with look-ahead.

Construction of the look-ahead automaton $\mathbf{\hat{A}}$. Recall that the
look-ahead automaton of $M$ is the domain automaton $\hat{A}$ of
$\hat{T}_{1}$. The set of states of $\hat{A}$ is the power set of the set of
states of $\hat{T_{1}}$. The initial state of $\hat{A}$ is
$\\{(q_{0},\\{\hat{q}_{0}\\})\\}$ and $\hat{A}$ contains the following rules.

$\begin{array}[]{rlclcrlcl}\\{(q_{0},\\{\hat{q}_{0}\\})\\}&(f(x_{1},x_{2}))&\rightarrow&f(\\{(q_{1},S)\\}(x_{1}),\\{q_{2}\\})\\}(x_{2}))\\\
\\{(q_{0},\\{\hat{q}_{0}\\})\\}&(f(x_{1},x_{2}))&\rightarrow&f(\emptyset(x_{1}),\\{(q_{3},\\{\hat{q}_{0}\\})\\}(x_{2}))\vspace{0.12cm}\\\
\\{q_{1}\\}&(f(x_{1},x_{2}))&\rightarrow&f(\\{q_{1}\\}(x_{1}),\\{q_{1}\\}(x_{2}))&&\\{q_{1}\\}&(e)&\rightarrow&e\\\
\\{q_{1}\\}&(d)&\rightarrow&d\vspace{0.12cm}\\\
\\{(q_{1},S)\\}&(f(x_{1},x_{2}))&\rightarrow&f(\\{(q_{1},S)(x_{1})\\},\\{(q_{1},S)\\}(x_{2}))\\\
\\{(q_{1},S)\\}&(e)&\rightarrow&e\\\
\\{(q_{1},S)\\}&(d)&\rightarrow&d\vspace{0.12cm}\\\
\\{q_{2}\\}&(f(x_{1},x_{2}))&\rightarrow&f(\\{q_{2}\\}(x_{1}),\\{q_{1}\\}(x_{2}))\\\
\\{q_{2}\\}&(e)&\rightarrow&e\vspace{0.12cm}\\\
(q_{3},\\{\hat{q}_{0}\\},\\{\hat{q}_{0}\\})&(d)&\rightarrow&d\\\ \end{array}$

For better readability, we again just write $q_{1}$ and $q_{2}$ instead of
$(q_{1},\emptyset)$ and $(q_{2},\emptyset)$, respectively. We remark that, by
construction of the domain automaton, $\hat{A}$ also contains the rule

$\\{(q_{0},\\{\hat{q}_{0}\\})\\}(f(x_{1},x_{2}))\rightarrow
f(\\{(q_{1},S)\\}(x_{1}),\\{q_{2},(q_{3},\\{\hat{q}_{0}\\})\\}(x_{2})),$

however, since no rules are defined for the state
$\\{q_{2},(q_{3},\\{\hat{q}_{0}\\})\\}$, this rule can be omitted.

Construction of the la-transducer $\mathbf{M}$. Finally, we construct the la-
transducer $M$. The initial state of $M$ is
$(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})$ and the rules of $M$ are

$\begin{array}[]{rlclcrlcl}(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})&(f(x_{1}\\!\\!:\\!\\{(q_{1},S)\\},x_{2}\\!\\!:\\!\\{q_{2}\\}))&\rightarrow&f((q_{1},S,\hat{q}_{1})(x_{1}),(q_{1},S,\hat{q}_{2})(x_{1}))\\\
(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})&(f(x_{1}\\!\\!:\\!\emptyset,x_{2}\\!\\!:\\!\\{q_{3},\\{\hat{q}_{0}\\}\\}))&\rightarrow&(q_{3},\\{\hat{q}_{0}\\},\hat{q}_{0})(x_{2})\vspace{0.12cm}\\\
(q_{1},S,\hat{q}_{1})&(f(x_{1}\\!\\!:\\!\\{(q_{1},S)\\},x_{2}\\!\\!:\\!\\{(q_{1},S)\\}))&\rightarrow&f((q_{1},S,\hat{q}_{1})(x_{1}),(q_{1},S,\hat{q}_{1})(x_{2}))\\\
(q_{1},S,\hat{q}_{1})&(e)&\rightarrow&e\\\
(q_{1},S,\hat{q}_{1})&(d)&\rightarrow&d\vspace{0.12cm}\\\
(q_{1},S,\hat{q}_{2})&(f(x_{1}\\!\\!:\\!\\{(q_{1},S)\\},x_{2}\\!\\!:\\!\\{(q_{1},S)\\}))&\rightarrow&f((q_{1},S,\hat{q}_{2})(x_{1}),(q_{1},S,\hat{q}_{2})(x_{2}))\\\
(q_{1},S,\hat{q}_{2})&(e)&\rightarrow&e\\\
(q_{1},S,\hat{q}_{2})&(d)&\rightarrow&d\vspace{0.12cm}\\\
(q_{3},\\{\hat{q}_{0}\\},\\{\hat{q}_{0}\\})&(d)&\rightarrow&d\\\ \end{array}$

By construction, the transducer $N$ contains the rule

$\eta=(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})(f(x_{1},x_{2}))\rightarrow
f((q_{1},S,\hat{q}_{1})(x_{1}),(q_{1},S,\hat{q}_{2})(x_{1})).$

This rule is obtained from the rule
$(q_{0},\\{\hat{q}_{0}\\})(f(x_{1},x_{2}))\rightarrow
f((q_{1},S)(x_{1}),q_{2}(x_{2}))$ of $\hat{T}_{1}$.

Consider the input tree $f(s_{1},s_{2})$ where $s_{1}$ and $s_{2}$ are
arbitrary ground trees. Clearly, translating $f(s_{1},s_{2})$ with $N$ begins
with the rule $\eta$. Recall that the transducer $N$ is equipped with look-
ahead in order to guarantee that guesses performed by states of $N$ are valid.
In particular, to guarantee that the guess corresponding to $\eta$ is valid,
we need to test whether or not $s_{1}\in\text{dom}(q_{1},S)$ and
$s_{2}\in\text{dom}(q_{2})$. Therefore, $M$ contains the rule

$(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})(f(x_{1}\\!\\!:\\!\\{(q_{1},S)\\},x_{2}\\!\\!:\\!\\{q_{2}\\}))\rightarrow
f((q_{1},S,\hat{q}_{1})(x_{1}),(q_{1},S,\hat{q}_{2})(x_{1})).$

Recall that if $f$ is relabeled by $\langle
f,\\{q_{1},S\\},\\{q_{2}\\}\rangle$ via the la-automaton $\hat{A}$, this means
precisely that $s_{1}\in\text{dom}(q_{1},S)$ and $s_{2}\in\text{dom}(q_{2})$.
We remark that by definition, $M$ also contains rules of the form

$(q_{0},\\{\hat{q}_{0}\\},\hat{q}_{0})(f(x_{1}\\!\\!:\\!l_{1},x_{2}\\!\\!:\\!l_{2}))\rightarrow
f((q_{1},S,\hat{q}_{1})(x_{1}),(q_{1},S,\hat{q}_{2})(x_{1})),$

where $l_{1}$ and $l_{2}$ are states of $\hat{A}$ such that
$\\{q_{1},S\\}\subseteq l_{1}$ and $\\{q_{2}\\}\subseteq l_{2}$ and $l_{1}$ or
$l_{2}$ is a proper superset. However, as none such states $l_{1}$ and $l_{2}$
are reachable by $\hat{A}$, we have omitted rules of this form. Other rules
are omitted for the same reason.$\hfill\squareforqed$

###  3.2 Correctness of the LA-Transducer $M$

In the following we prove the correctness of our construction. More precisely,
we prove that $M$ is functional if and only if $T_{1}\,\hat{\circ}\,T_{2}$ is.
By Lemma 3, it is sufficient to show that $M$ is functional if and only if
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is.

First, we prove that the following claim: If $M$ is functional then
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional. More precisely, we show that
$\mathcal{R}(\hat{T}_{1})\circ\mathcal{R}(T_{2})\subseteq\mathcal{R}(M)$.
Obviously, this implies our claim. First of all, consider the transducers $N$
and $N^{\prime}$ obtained from the p-construction in our examples in Section
3. Notice that the relations defined by $N$ and $N^{\prime}$ are supersets of
$\mathcal{R}(T_{1})\circ\mathcal{R}(T_{2})$ and
$\mathcal{R}(T_{1}^{\prime})\circ\mathcal{R}(T_{2}^{\prime})$, respectively.

In the following, we show that this observation can be generalized. Consider
arbitrary transducers $T$ and $T^{\prime}$. We claim that the transducer
$\breve{N}$ obtained from the p-construction for $T$ and $T^{\prime}$ always
defines a superset of the composition
$\mathcal{R}(T)\circ\mathcal{R}(T^{\prime})$. To see that our claim holds,
consider a translation of $T\,\hat{\circ}\,T^{\prime}$ in which the state
$q^{\prime}$ of $T^{\prime}$ processes a tree $t$ produced by the state $q$ of
$T$ on input $s$. If the corresponding state $(q,q^{\prime})$ of $\breve{N}$
processes $s$ then $(q,q^{\prime})$ can guess that $q$ has produced $t$ and
proceed accordingly. Thus $\breve{N}$ can effectively simulate the composition
$T\,\hat{\circ}\,T^{\prime}$.

As $M$ is in essence obtained from the p-construction extended with look-
ahead, $M$ ‘inherits’ this property. Note that the addition of look-ahead does
not affect this property. Therefore our claim follows.

###### Lemma 4

$\mathcal{R}(\hat{T}_{1})\circ\mathcal{R}(T_{2})\subseteq\mathcal{R}(M)$.

In fact an even stronger result holds.

###### Lemma 5

Let $(q_{1},S)$ be a state of $\hat{T}_{1}$ and $q_{2}$ be a state of $T_{2}$.
If on input $s$, $(q_{1},S)$ can produce the tree $t$ and on input $t$,
$q_{2}$ can produce the tree $r$ then $(q_{1},S,q_{2})$ can produce $r$ on
input $s$.

Consider a translation of $\hat{T}_{1}\,\hat{\circ}\,T_{2}$ in which $T_{2}$
processes the tree $t$ produced by $T_{1}$ on input $s$. We call a translation
of $M$ _synchronized_ if the translation simulates a translation of
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$, i.e., if a state $(q,S,q^{\prime})$ of $M$
processes the subtree $s^{\prime}$ of $s$ and the corresponding state of
$q^{\prime}$ of $T_{2}$ processes the subtree $t^{\prime}$ of $t$ and
$t^{\prime}$ is produced by $(q,S)$ on input $s^{\prime}$, then
$(q,S,q^{\prime})$ guesses $t^{\prime}$.

We now show that if $\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional, then so
is $M$. Before we prove our claim consider the following auxiliary results.

###### Lemma 6

Consider an arbitrary input tree $s$. Let $\hat{s}$ be a subtree of $s$.
Assume that in an arbitrary translation of $M$ on input $s$, the state
$(q_{1},S,q_{2})$ processes $\hat{s}$. Then, a synchronized translation of $M$
on input $s$ exists in which the state $(q_{1},S,q_{2})$ processes the subtree
$\hat{s}$.

It is easy to see that the following result holds for arbitrary transducers.

###### Proposition 1

Let $\tau=T_{1}\,\hat{\circ}\,T_{2}$ where $T_{1}$ and $T_{2}$ are arbitrary
transducers. Let $s$ be a tree such that $\tau(s)=\\{r\\}$ is a singleton. Let
$t_{1}$ and $t_{2}$ be distinct trees produced by $T_{1}$ on input $s$. If
$t_{1}$ and $t_{2}$ are in the domain of $T_{2}$ then
$T_{2}(t_{1})=T_{2}(t_{2})=\\{r\\}$.

Using Lemma 6 and Proposition 1, we now show that the following holds. Note
that in the following $t/v$, where $t$ is some tree and $v$ is a node, denotes
the subtree of $t$ rooted at the node $v$.

###### Lemma 7

Consider an arbitrary input tree $s$. Let $\hat{s}$ be a subtree of $s$. Let
the state $(q_{1},S,q_{2})$ process $\hat{s}$ in a translation $M$ on input
$s$. If $\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional then $(q_{1},S,q_{2})$
can only produce a single output tree on input $\hat{s}$.

###### Proof

Assume to the contrary that $(q_{1},S,q_{2})$ can produce distinct trees
$r_{1}$ and $r_{2}$ on input $\hat{s}$. For $r_{1}$, it can be shown that a
tree $t_{1}$ exists such that

  1. 1.

on input $\hat{s}$, the state $(q_{1},S)$ of $\hat{T}_{1}$ produces $t_{1}$
and

  2. 2.

on input $t_{1}$, the state $q_{2}$ of $T_{2}$ produces $r_{1}$.

It can be shown that a tree $t_{2}$ with the same properties exists for
$r_{2}$. Informally, this means that $r_{1}$ and $r_{2}$ are producible by
$(q_{1},S,q_{2})$ by simulating the ‘composition of $(q_{1},S)$ and $q_{2}$’.

Due to Lemma 6, a synchronized translation of $M$ on input $s$ exists in which
the state $(q_{1},S,q_{2})$ processes the subtree $\hat{s}$ of $s$. Let $g$ be
the node at which $(q_{1},S,q_{2})$ processes $\hat{s}$. Let
$\hat{q}_{1},\dots,\hat{q}_{n}$ be all states of $M$ of the form
$(q_{1},S,q_{2}^{\prime})$, where $q_{2}^{\prime}$ is some state of $T_{2}$,
that occur in the synchronized translation of $M$ and that process $\hat{s}$.
Note that by definition $q_{2}^{\prime}\in S$. Due to Lemmas 2 and 5, we can
assume that in the synchronized translation, the states
$\hat{q}_{1},\dots,\hat{q}_{n}$ all guess that the tree $t_{1}$ has been
produced by the state $(q_{1},S)$ of $\hat{T}_{1}$ on input $\hat{s}$. Hence,
we can assume that at the node $g$, the output subtree $r_{1}$ is produced.
Therefore, a synchronized translation of $M$ on input $s$ exists, that yields
an output tree $\hat{r}_{1}$ such that $\hat{r}_{1}/g=r_{1}$, where
$\hat{r}_{1}/g$ denotes the subtree of $\hat{r}_{1}$ rooted at the node $g$.
Analogously, it follows that a synchronized translation of $M$ on input $s$
exists, that yields an output tree $\hat{r}_{2}$ such that
$\hat{r}_{2}/g=r_{2}$.

As both translation are synchronized, i.e., ‘simulations’ of translations of
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ on input $s$, it follows that the trees
$\hat{r}_{1}$ and $\hat{r}_{2}$ are producible by
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ on input $s$. Due to Proposition 1,
$\hat{r}_{1}=\hat{r}_{2}$ and therefore
$r_{1}=\hat{r}_{1}/g=\hat{r}_{2}/g=r_{2}$. ∎

Lemma 4 implies that if $M$ is functional then
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional as well. Lemma 7 implies that
if $\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional then so is $M$. Therefore,
we deduce that due Lemmas 4 and 7 the following holds.

###### Corollary 1

$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional if and only if $M$ is
functional.

In fact, Corollary 1 together with Lemma 4 imply that
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ and $M$ are equivalent if
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional, since it can be shown that
$\text{dom}(\hat{T}_{1}\,\hat{\circ}\,T_{2})=\text{dom}(M)$.

Since functionality for transducers with look-ahead is decidable [8],
Corollary 1 implies that it is decidable whether or not
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional. Together with Lemma 3, we
obtain:

###### Theorem 3.1

Let $T_{1}$ and $T_{2}$ be top-down tree transducers. It is decidable whether
or not $T_{1}\,\hat{\circ}\,T_{2}$ is functional.

###  3.3 Functionality of Arbitrary Compositions

In this section, we show that the question whether or not an arbitrary
composition is functional can be reduced to the question of whether or not a
two-fold composition is functional.

###### Lemma 8

Let $\tau$ be a composition of transducers. Then two transducers $T_{1},T_{2}$
can be constructed such that $T_{1}\,\hat{\circ}\,T_{2}$ is functional if and
only if $\tau$ is functional.

###### Proof

Consider a composition of $n$ transducers
$T^{\prime}_{1},\dots,T^{\prime}_{n}$. W.l.og. assume that $n>2$. For $n\leq
2$, our claim follows trivially. Let $\tau$ be the composition of
$T^{\prime}_{1},\dots,T^{\prime}_{n}$. We show that transducer
$\hat{T}_{1},\dots,\hat{T}_{n-1}$ exist such that
$\hat{T}_{1}\,\hat{\circ}\,\cdots\,\hat{\circ}\,\hat{T}_{n-1}$ is functional
if and only if $\tau$ is.

Consider an arbitrary input tree $s$. Let $t$ be a tree produced by the
composition
$T^{\prime}_{1}\,\hat{\circ}\,\cdots\,\hat{\circ}\,T^{\prime}_{n-2}$ on input
$s$. Analogously as in Proposition 1, the composition
$T^{\prime}_{n-1}\,\hat{\circ}\,T^{\prime}_{n}$, on input $t$, can only
produce a single output tree if $\tau$ is functional. For the transducers
$T^{\prime}_{n-1}$ and $T^{\prime}_{n}$, we construct the la-transducer $M$
according to our construction in Section 3.1. It can be shown that, the la-
transducer $M$ our construction yields has the following properties regardless
of whether or not $T_{n-1}\,\hat{\circ}\,T_{n}$ is functional

  1. (a)

$\text{dom}(M)=\text{dom}(T_{n-1}\,\hat{\circ}\,T_{n})$ and

  2. (b)

on input $t$, $M$ only produces a single output tree if and only if
$T_{n-1}\,\hat{\circ}\,T_{n}$ does

Therefore, $\tau(s)$ is a singleton if and only if
$T^{\prime}_{1}\,\hat{\circ}\,\cdots\,\hat{\circ}\,T^{\prime}_{n-2}\,\hat{\circ}\,M(s)$
is a singleton. Engelfriet has shown that every transducer with look-ahead can
be decomposed to a composition of a deterministic bottom-up relabeling and a
transducer (Theorem 2.6 of [4]). It is well known that (nondeterministic)
relabelings are independent of whether they are defined by bottom-up
transducers or by top-down transducers (Lemma 3.2 of [3]). Thus, any
transducer with look-ahead can be decomposed into a composition of a
nondeterministic top-down relabeling and a transducer. Let $R$ and $T$ be the
relabeling and the transducer such that $M$ and $R\,\hat{\circ}\,T$ are
equivalent. Then obviously, $\tau(s)$ is a singleton if and only if
$T^{\prime}_{1}\,\hat{\circ}\,\cdots\,\hat{\circ}\,T^{\prime}_{n-2}\,\hat{\circ}\,R\,\hat{\circ}\,T(s)$
is a singleton.

Consider arbitrary transducers $\bar{T}_{1}$ and $\bar{T}_{2}$. Baker has
shown that if $\bar{T}_{2}$ is non-deleting and linear then a transducer $T$
can be constructed such that $T$ and $\bar{T}_{1}\,\hat{\circ}\,\bar{T}_{2}$
are equivalent (Theorem 1 of [2]). By definition, any relabeling is non-
deleting and linear. Thus, we can construct a transducer $\tilde{T}$ such that
$\tilde{T}$ and $T^{\prime}_{n-2}\,\hat{\circ}\,R$ are equivalent. Therefore,
it follows that $\tau(s)$ is a singleton if and only if
$T^{\prime}_{1}\,\hat{\circ}\,\cdots\,\hat{\circ}\,T^{\prime}_{n-3}\,\hat{\circ}\,\tilde{T}\,\hat{\circ}\,T(s)$
is a singleton. This yields our claim. ∎

Lemma 8 and Theorem 3.1 yield that functionality of compositions of
transducers is decidable.

Engelfriet has shown that any la-transducer can be decomposed into a
composition of a nondeterministic top-down relabeling and a transducer [4, 3].
Recall that while la-transducers generalize transducers, bottom-up transducers
and la-transducers are incomparable [4]. Baker, however, has shown that the
composition of $n$ bottom-up-transducers can be realized by the composition of
$n+1$ top-down transducers [2]. For any functional composition of transducers
an equivalent deterministic la-transducer can be constructed [5]. Therefore we
obtain our following main result.

###### Theorem 3.2

Functionality for arbitrary compositions of top-down and bottom-up tree
transducers is decidable. In the affirmative case, an equivalent deterministic
top-down tree transducer with look-ahead can be constructed.

##  4 Conclusion

We have presented a construction of an la-transducer for a composition of
transducers which is functional if and only if the composition of the
transducers is functional — in which case it is equivalent to the composition.
This construction is remarkable since transducers are not closed under
composition in general, neither does functionality of the composition imply
that each transducer occurring therein, is functional. By Engelfriet’s
construction in [5], our construction provides the key step to an efficient
implementation (i.e., a deterministic transducer, possibly with look-ahead)
for a composition of transducers – whenever possible (i.e., when their
translation is functional). As an open question, it remains to see how large
the resulting functional transducer necessarily must be, and whether the
construction can be simplified if for instance only compositions of linear
transducers are considered.

## References

  * [1] Aho, A.V., Ullman, J.D.: Translations on a context-free grammar. Inf. Control. 19(5), 439–475 (1971)
  * [2] Baker, B.S.: Composition of top-down and bottom-up tree transductions. Inf. Control. 41(2), 186–213 (1979)
  * [3] Engelfriet, J.: Bottom-up and top-down tree transformations - A comparison. Math. Syst. Theory 9(3), 198–231 (1975)
  * [4] Engelfriet, J.: Top-down tree transducers with regular look-ahead. Math. Syst. Theory 10, 289–303 (1977)
  * [5] Engelfriet, J.: On tree transducers for partial functions. Inf. Process. Lett. 7(4), 170–172 (1978)
  * [6] Engelfriet, J.: Three hierarchies of transducers. Math. Syst. Theory 15(2), 95–125 (1982)
  * [7] Engelfriet, J., Maneth, S., Seidl, H.: Deciding equivalence of top-down XML transformations in polynomial time. J. Comput. Syst. Sci. 75(5), 271–286 (2009)
  * [8] Ésik, Z.: Decidability results concerning tree transducers I. Acta Cybern. 5(1), 1–20 (1980)
  * [9] Hakuta, S., Maneth, S., Nakano, K., Iwasaki, H.: Xquery streaming by forest transducers. In: ICDE 2014, Chicago, USA, March 31 - April 4, 2014. pp. 952–963 (2014)
  * [10] Küsters, R., Wilke, T.: Transducer-based analysis of cryptographic protocols. Inf. Comput. 205(12), 1741–1776 (2007)
  * [11] Maneth, S.: A survey on decidable equivalence problems for tree transducers. Int. J. Found. Comput. Sci. 26(8), 1069–1100 (2015)
  * [12] Maneth, S., Seidl, H., Vu, M.: Definability results for top-down tree transducers. In: DLT 2021, Porto, Portugal, August 16-20, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12811, pp. 291–303. Springer (2021)
  * [13] Matsuda, K., Inaba, K., Nakano, K.: Polynomial-time inverse computation for accumulative functions with multiple data traversals. High. Order Symb. Comput. 25(1), 3–38 (2012)
  * [14] Rounds, W.C.: Mappings and grammars on trees. Math. Syst. Theory 4(3), 257–287 (1970)
  * [15] Thatcher, J.W.: Generalized sequential machine maps. J. Comput. Syst. Sci. 4(4), 339–367 (1970)

##  Appendix 0.A Appendix

In the following, we first introduce additional notation and definitions used
in the proofs in the Appendix.

###  0.A.1 Definitions

####  0.A.1.1 Set of Nodes

Let $t$ be a tree. For $t$, its set $V(t)$ of nodes is a subset of
$V=\mathbb{N}^{*}$. More formally, $V(t)=\\{\epsilon\\}\cup\\{iu\mid
i\in[k],u\in V(t_{i})\\}$ where $t=a(t_{1},\dots,t_{k})$, $a\in\Sigma_{k}$,
$k\geq 0$ and $t_{1},\dots,t_{k}\in T_{\Sigma}$. For better readability we add
dots between numbers. E.g. for the tree $t=f(a,f(a,b))$ we have
$V(t)=\\{\epsilon,1,2,2.1,2.2\\}$. For $v\in V(t)$, $t[v]$ is the label of $v$
and $t/v$ is the subtree of $t$ rooted at $v$.

####  0.A.1.2 Substitutions

Let $t_{1},\dots t_{n}$ be trees over $\Sigma$ and $v_{1},\dots,v_{n}$ be
distinct nodes none of which is a prefix of the other, then we denote by
$[v_{i}\leftarrow t_{i}\mid i\in[n]]$ the _substitution_ that for each
$i\in[n]$, replaces the subtree rooted at $v_{i}$ with $t_{i}$.

Let $t$ be a tree, $a\in\Sigma_{0}$ and $\mathcal{T}$ be a set of trees. We
denote by $t[a\leftarrow\mathcal{T}]$ the set of all trees obtained by
substituting leaves labeled by $a$ with some tree in $\mathcal{T}$, i.e., the
set of all trees of the form $t[v\leftarrow t_{v}\mid v\in V(t),t[v]=a]$ where
for all $a$-leaves $v$, $t_{v}\in\mathcal{T}$. Note that two distinct leaves
labeled by $a$ may be replaced by distinct trees in $\mathcal{T}$. If
$\mathcal{T}=\emptyset$ then we define $t[a\leftarrow\mathcal{T}]=\emptyset$.
For simplicity, we write $t[a\leftarrow t^{\prime}]$ if
$\mathcal{T}=\\{t^{\prime}\\}$.

####  0.A.1.3 Partial Trees and Semantic of a Transducer

Recall that $T_{\Sigma}[B]=T_{\Sigma^{\prime}}$ where $\Sigma^{\prime}$ is
obtained from $\Sigma$ by $\Sigma^{\prime}_{0}=\Sigma_{0}\cup B$ while for all
$k>0$, $\Sigma^{\prime}_{k}=\Sigma_{k}$. In the following, we call a tree in
$T_{\Sigma}[B]$ a _partial tree_.

The _semantic_ of a transducer $T$, defined as in Section 2, is formally
defined as follows. Let $q\in Q$ and $v$ be an arbitrary node. We denote by
$[\\![q]\\!]^{T}_{v}$ the partial function from $T_{\Sigma}[B]$ to the power
set of $T_{\Delta}[Q(V)]$ defined as follows

  * •

for $s=a(s_{1},\dots,s_{k})$, $a\in\Sigma_{k}$, and $s_{1},\dots,s_{k}\in
T_{\Sigma}[B]$,

$[\\![q]\\!]^{T}_{v}(s)=\bigcup_{\xi\in\text{rhs}_{T}(q,a)}\xi[q(x_{i})\leftarrow[\\![q]\\!]_{v.i}(s_{i})\mid
q\in Q,i\in[k]]$

  * •

for $b\in B$, $[\\![q]\\!]^{T}_{v}(b)=\\{q(v)\\}$,

where $\text{rhs}_{T}(q,a)$ denotes the set of all right-hand sides of $q$ and
$a$. The reason why input nodes of $s$ are added to the semantic of $T$ is
that for some of our proofs we require that for states $q$ of $T$ it is
traceable which input node $q$ currently processes.

If clear from context which transducer is meant, we omit the superscript $T$
and write $[\\![q]\\!]_{v}$ instead of $[\\![q]\\!]^{T}_{v}$. In the
following, we write $[\\![q]\\!]$ instead of $[\\![q]\\!]_{\epsilon}$ for
simplicity. We write $[\\![q]\\!]^{T}_{v}(s)\Rightarrow t$ if
$t\in[\\![q]\\!]^{T}_{v}(s)$.

In the following, for trees in $T_{\Delta}[Q(X)]$ and $T_{\Delta}[Q(V)]$, we
write $t\langle x\leftarrow v\rangle$ to denote the substitution
$t[q(x)\leftarrow q(v)\mid q\in Q]$ for better readability where $x\in X$ and
$v\in V$.

Recall that for a set $\Gamma$ of right-hand sides of a transducer $T$,
$\Gamma\langle x_{i}\rangle$ denotes the set of all states $q$ of $T$ such
that $q(x_{i})$ occurs in some tree $\gamma$ in $\Gamma$. For a set $\Lambda$
of trees in $T_{\Delta}[Q(V)]$, we define $\Lambda\langle v\rangle$ where $v$
is some node analogously; e.g., for
$\Lambda=\\{f(q(v_{1}),f(q(v_{2}),q^{\prime}(v_{2}))),\
f(q_{1}(v_{1}),q_{2}(v_{2}))\\}$, we have $\Lambda\langle
v_{1}\rangle=\\{q,q_{1}\\}$ and $\Lambda\langle
x_{2}\rangle=\\{q,q^{\prime},q_{2}\\}$.

##  Appendix 0.B Properties of the Domain Automaton $A$

In the following we consider the _domain automaton_ $A$ introduced in Section
3 for a transducer $T$. In particular, we consider the properties of $A$.
Recall that a state of $A$ is a set consisting of states of $T$. In Section 3,
we have claimed that if in a translation of $T$ on input $s$, the states
$q_{1}\dots,q_{n}$ process the node $v$ of $s$ then $\\{q_{1}\dots,q_{n}\\}$
processes the node $v$ of $s$ in a computation of $A$. We now formally prove
this statement. First we prove the following auxiliary result.

###### Lemma 9

Let $s\in T_{\Sigma}[X]$. Let $v_{1},\dots v_{n}$ be the nodes of $s$ that are
labeled by a symbol in $X$. Let $S_{1}$ and $S_{2}$ be states of $A$ and let
for $j=1,2$,

$[\\![S_{j}]\\!](s)\Rightarrow s[v_{i}\leftarrow S^{i}_{j}(v_{i})\mid
i\in[n]]$

where for $i\in[n]$, $S_{j}^{i}$ is a state of $A$. Then

$[\\![S_{1}\cup S_{2}]\\!](s)\Rightarrow s[v_{i}\leftarrow S^{i}_{1}\cup
S^{i}_{2}(v_{i})\mid i\in[n]].$

###### Proof

We prove our claim by structural induction over $s$. Let
$s=a(s_{1},\dots,s_{k})$ where $a\in\Sigma_{k}$, $k\geq 0$, and for
$\iota\in[k]$, $s_{\iota}\in T_{\Sigma}[X]$. As

$[\\![S_{1}]\\!](s)\Rightarrow s[v_{i}\leftarrow S^{i}_{1}(v_{i})\mid
i\in[n]],$

a rule $S_{1}(a(x_{1},\dots,x_{k}))\rightarrow
a(\hat{S}_{1}(x_{1}),\dots,\hat{S}_{k}(x_{k}))$ exists such that for all
$\iota\in[k]$, on input $s_{\iota}$, the function
$[\\![\hat{S}_{\iota}]\\!]_{\iota}$ yields the subtree of $s[v_{i}\leftarrow
S^{i}_{1}(v_{i})\mid i\in[n]]$ that is rooted at the node $\iota$. More
formally,

$[\\![\hat{S}_{\iota}]\\!]_{\iota}(s_{\iota})\Rightarrow
s_{\iota}[v^{\prime}\leftarrow S^{i}_{1}(\iota.v^{\prime})\mid v^{\prime}\in
V(s_{\iota})\text{ and }\iota.v^{\prime}=v_{i}\text{ where }i\in[n]],$

which in turn implies

$[\\![\hat{S}_{\iota}]\\!](s_{\iota})\Rightarrow
s_{\iota}[v^{\prime}\leftarrow S^{i}_{1}(v^{\prime})\mid v^{\prime}\in
V(s_{\iota})\text{ and }\iota.v^{\prime}=v_{i}\text{ where }i\in[n]].$

Analogously, it follows that a rule $S_{2}(a(x_{1},\dots,x_{k}))\rightarrow
a(\hat{S}^{\prime}_{1}(x_{1}),\dots,\hat{S}_{k}^{\prime}(x_{k}))$ exists such
that for all $\iota\in[k]$,

$[\\![\hat{S}^{\prime}_{\iota}]\\!](s_{\iota})\Rightarrow
s_{\iota}[v^{\prime}\leftarrow S^{i}_{2}(v^{\prime})\mid v^{\prime}\in
V(s_{\iota})\text{ and }\iota.v^{\prime}=v_{i}\text{ where }i\in[n]].$

We now show that the automaton $A$ contains the rule

$S_{1}\cup S_{2}(a(x_{1},\dots,x_{k}))\rightarrow
a(\hat{S}_{1}\cup\hat{S}^{\prime}_{1}(x_{1}),\dots,\hat{S}_{k}\cup\hat{S}_{k}^{\prime}(x_{k})).$
(a)

By construction, the rule $S_{1}(a(x_{1},\dots,x_{k}))\rightarrow
a(\hat{S}_{1}(x_{1}),\dots,\hat{S}_{k}(x_{k}))$ is defined only if for all
$q\in S_{1}$ a non-empty set of right-hand sides
$\Gamma_{q}\subseteq\text{rhs}_{T}(q,a)$ exists such that for $\iota\in[k]$,
$\hat{S}_{\iota}=\bigcup_{q\in S_{1}}\Gamma_{q}\langle x_{\iota}\rangle$.
Likewise, the rule $S_{2}(a(x_{1},\dots,x_{k}))\rightarrow
a(\hat{S}^{\prime}_{1}(x_{1}),\dots,\hat{S}_{k}^{\prime}(x_{k}))$ is defined
only if for all $q^{\prime}\in S_{2}$ a non-empty set of right-hand sides
$\Gamma^{\prime}_{q^{\prime}}\subseteq\text{rhs}_{T}(q^{\prime},a)$ exists
such that for $\iota\in[k]$, $\hat{S}^{\prime}_{\iota}=\bigcup_{q^{\prime}\in
S_{2}}\Gamma^{\prime}_{q^{\prime}}\langle x_{\iota}\rangle$. For all states
$q\in S_{1}\cup S_{2}$, we define

$\breve{\Gamma}_{q}=\begin{cases}\Gamma_{q}\cup\Gamma^{\prime}_{q}&\text{ if
}q\in S_{1}\cap S_{2}\\\ \Gamma_{q}&\text{ if }q\in S_{1}\setminus S_{2}\\\
\Gamma^{\prime}_{q}&\text{ if }q\in S_{2}\setminus S_{1}\end{cases}$

Clearly, the sets $\breve{\Gamma}_{q}$ yield that the rule defined in (a)
exists.

Now, consider the following. As for $\iota\in[k]$,

$[\\![\hat{S}_{\iota}]\\!](s_{\iota})\Rightarrow
s_{\iota}[v^{\prime}\leftarrow S^{i}_{1}(v^{\prime})\mid v^{\prime}\in
V(s_{\iota})\text{ and }\iota.v^{\prime}=v_{i}\text{ where }i\in[n]]$

and

$[\\![\hat{S}^{\prime}_{\iota}]\\!](s_{\iota})\Rightarrow
s_{\iota}[v^{\prime}\leftarrow S^{i}_{2}(v^{\prime})\mid v^{\prime}\in
V(s_{\iota})\text{ and }\iota.v^{\prime}=v_{i}\text{ where }i\in[n]]$

the induction hypothesis yields

$[\\![\hat{S}_{\iota}\cup\hat{S}_{\iota}^{\prime}]\\!](s_{\iota})\Rightarrow
s_{\iota}[v^{\prime}\leftarrow S^{i}_{1}\cup S^{i}_{2}(v^{\prime})\mid
v^{\prime}\in V(s_{\iota})\text{ and }\iota.v^{\prime}=v_{i}\text{ where
}i\in[n]]$ (b)

Thus, due to (a) and (b) our claim follows. ∎

We now prove our statement.

###### Lemma 10

Let $s\in T_{\Sigma}[X]$. Let $v_{1},\dots v_{n}$ be the nodes of $s$ that are
labeled by a symbol in $X$. Let $S$ be a state of $A$. For $q\in S$, let
$[\\![q]\\!]^{T}(s)\Rightarrow t_{q}$. Then,

$[\\![S]\\!]^{A}(s)\Rightarrow s[v_{i}\leftarrow S_{i}(v_{i})\mid i\in[n]]$

where $S_{i}=\bigcup_{q\in S}t_{q}\langle v_{i}\rangle$.

###### Proof

Due to Lemma 9, it is sufficient to show that if
$[\\![q]\\!]^{T}(s)\Rightarrow t_{q}$, then

$[\\![\\{q\\}]\\!]^{A}(s)\Rightarrow s[v_{i}\leftarrow
S^{\prime}_{i}(v_{i})\mid i\in[n]]$

where $S^{\prime}_{i}=t_{q}\langle v_{i}\rangle$. We prove this claim by
structural induction over $s$. Let $s=a(s_{1},\dots,s_{k})$ where
$a\in\Sigma_{k}$, $k\geq 0$, and for $i\in[k]$, $s_{i}\in T_{\Sigma}[X]$. Due
to our premise, $\gamma\in\text{rhs}(q,a)$ exists such that

$t_{q}\in\gamma[q^{\prime}(x_{i})\leftarrow[\\![q^{\prime}]\\!]_{i}(s_{i})\mid
q^{\prime}\in Q,i\in[k]].$ (1)

By definition of $A$, $\gamma\in\text{rhs}(q,a)$ implies that the automaton
$A$ contains the rule

$\\{q\\}(a)\rightarrow a(\hat{S}_{1}(x_{1}),\dots,\hat{S}_{k}(x_{k}))$ (a)

where $\hat{S}_{i}=\gamma\langle x_{i}\rangle$ for $i\in[k]$.

Now consider $\gamma\in\text{rhs}(q,a)$ in conjunction with the variable
$x_{i}$. Let $\gamma\langle x_{i}\rangle=\\{q_{1},\dots,q_{m}\\}$. For
$j\in[m]$, we denote by $U_{j}$ the set of all nodes of $\gamma$ that are
labeled by $q_{j}(x_{i})$. For all nodes $u\in U_{j}$, Equation 1 clearly
implies $[\\![q_{j}]\\!]_{i}^{T}(s_{i})\Rightarrow t_{q}/u$. Recall that by
definition, if $\breve{q}(\breve{v})$ occurs in $t_{q}/u$, where $\breve{q}$
is a state of $T$ and $\breve{v}$ is some node then $\breve{v}$ is of the form
$i.v^{\prime}$. Clearly, $[\\![q_{j}]\\!]_{i}^{T}(s_{i})\Rightarrow t_{q}/u$
implies $[\\![q_{j}]\\!]^{T}(s_{i})\Rightarrow\eta_{u}$ where $\eta_{u}$
denotes the tree obtained from $t_{q}/u$ by substituting occurrences of
$\breve{q}(i.v^{\prime})$ by $\breve{q}(v^{\prime})$.

Recall that $\eta_{u}\langle v^{\prime}\rangle$ denotes the set of all states
$q^{\prime}$ in $Q$ such that $q^{\prime}(v^{\prime})$ occurs in $\eta_{u}$.
In the following, let $S_{u,v^{\prime}}=\eta_{u}\langle v^{\prime}\rangle$.
Due to the induction hypothesis, it follows that for all $u\in U_{j}$,

$[\\![\\{q_{j}\\}]\\!]^{A}(s_{i})\Rightarrow s_{i}[v^{\prime}\leftarrow
S_{u,v^{\prime}}(v^{\prime})\mid v^{\prime}\in V(s_{i}),s_{i}[v^{\prime}]\in
X].$ (2)

Due to Lemma 9 and Equation 2, it follows for all $j\in[m]$ that

$[\\![\\{q_{j}\\}]\\!]^{A}(s_{i})\Rightarrow
s_{i}[v^{\prime}\leftarrow\bigcup_{u\in U_{j}}S_{u,v^{\prime}}(v^{\prime})\mid
v^{\prime}\in V(s_{i}),s_{i}[v^{\prime}]\in X]$ (3)

Recall that $\hat{S}_{i}=\gamma\langle x_{i}\rangle$. Thus, Lemma 9 and
Equation 3 yield

$[\\![\hat{S}_{i}]\\!]^{A}(s_{i})\Rightarrow
s_{i}[v^{\prime}\leftarrow\bigcup_{j\in[m]}\bigcup_{u\in
U_{j}}S_{u,v^{\prime}}(v^{\prime})\mid v^{\prime}\in
V(s_{i}),s_{i}[v^{\prime}]\in X]$ (b)

Note that for $v=i.v^{\prime}$,

$\bigcup_{j\in[m]}\bigcup_{u\in U_{j}}\eta_{u}\langle
v^{\prime}\rangle=\bigcup_{j\in[m]}\bigcup_{u\in
U_{j}}S_{u,v^{\prime}}=t\langle v\rangle.$

Therefore it follows that (a) and (b) yield our claim. ∎

Additionally, the domain automaton $A$ has the following property. If in a
translation of $A$ on input $s$, the state $S$ processes the node $v$ of $s$
then a translation of $T$ on input $s$ exists such that $v$ is only processed
by states in $S$. More formally, we prove thee following result.

###### Lemma 11

Let $s\in T_{\Sigma}[X]$. Let $v_{1},\dots v_{n}$ be the nodes of $s$ that are
labeled by a symbol in $X$. Let $S,S_{1},\dots,S_{n}$ be states of $A$. Let
$[\\![S]\\!]^{A}(s)\Rightarrow\hat{s}$ where

$\hat{s}=s[v_{i}\leftarrow S_{i}(v_{i})\mid i\in[n]].$

For all $q\in S$, a tree $t$ exists such that $[\\![q]\\!]^{T}(s)\Rightarrow
t$ and for $i\in[n]$, $t\langle v_{i}\rangle\subseteq S_{i}$.

###### Proof

We prove our claim by structural induction. Obviously, our claim holds if
$s\in X$.

In the following, let $s\notin X$. Then, a node $v$ exist such that the
subtree of $s$ rooted at $v$ is of the form $a(s_{1},\dots,s_{k})$ where
$a\in\Sigma_{k}$, $k\geq 0$, and $s_{1},\dots,s_{k}\in X$. Note that by
definition $v$ can be a leaf. Consider the tree $s^{\prime}=s[v\leftarrow
x_{1}]$. Let $v_{1}^{\prime},\dots,v_{m}^{\prime}$ be the nodes of
$s^{\prime}$ that are labeled by a symbol in $X$. W.l.o.g. let
$v_{1}^{\prime}=v$.

Recall that the node $v$ is labeled by the node $a$ in $s$. As
$[\\![S]\\!]^{A}(s)\Rightarrow\hat{s}$, it follows that a tree $\tilde{s}$
exists such that $[\\![S]\\!]^{A}(s^{\prime})\Rightarrow\tilde{s}$ and the
tree $s$ can be obtained from $\tilde{s}$ by substituting $S_{1}^{\prime}(v)$
by $\xi\langle x_{i}\leftarrow v.j\mid j\in[k]\rangle$ where $\xi$ is a right-
hand side of $S_{1}^{\prime}$ and $a$. Note that by definition, states
$S_{1}^{\prime},\dots,S_{m}^{\prime}$ of $A$ exists such that the tree
$\tilde{s}$ is obtained from $s^{\prime}$ by relabeling the node
$v_{i}^{\prime}$ of $s^{\prime}$ by $S_{i}^{\prime}(v_{i})$. More formally, it
holds that

$\tilde{s}=s^{\prime}[v_{i}^{\prime}\leftarrow
S^{\prime}_{i}(v_{i}^{\prime})\mid i\in[m]],$

and that

$\hat{s}=\tilde{s}[S_{1}^{\prime}(v)\leftarrow\xi\langle x_{i}\leftarrow
v.j\mid j\in[k]\rangle].$ (1)

By induction hypothesis, as $[\\![S]\\!]^{A}(s^{\prime})\Rightarrow\tilde{s}$,
for all states $q\in S$, a tree $t^{\prime}$ exists such that

  1. 1.

$[\\![q]\\!]^{T}(s^{\prime})\Rightarrow t^{\prime}$ and

  2. 2.

for $i\in[m]$, $t^{\prime}\langle v_{i}^{\prime}\rangle\subseteq
S^{\prime}_{i}$.

In particular, it holds that $t^{\prime}\langle
v^{\prime}_{1}\rangle=t^{\prime}\langle v\rangle\subseteq S^{\prime}_{1}$.

Let $S^{\prime}_{1}=\\{q_{1},\dots,q_{n}\\}$. Recall that $\xi$ is a right-
hand side of $S_{1}^{\prime}$ and $a$. W.l.o.g. let
$\xi=a(S_{1}(x_{1}),\dots,S_{k}(x_{k}))$. Then, by definition of the rules of
$A$, it follows that for each $j\in[n]$, a tree $\gamma_{j}$ exists such that

  1. (a)

$\gamma_{j}\in\text{rhs}_{T}(q_{j},a)$ and

  2. (b)

for $\iota\in[k]$ it holds that $\bigcup_{j\in[n]}\gamma_{j}\langle
x_{\iota}\rangle\subseteq S_{\iota}$.

As $t^{\prime}\langle v\rangle\subseteq S^{\prime}_{1}$, it follows that
$[\\![q]\\!]^{T}(s)\Rightarrow t$ where

$t=t^{\prime}[q_{j}(v)\leftarrow\gamma_{j}\langle x_{i}\leftarrow v.i\mid
i\in[k]\rangle\mid j\in[n]].$ (2)

Consider the node $v.\iota$ where $\iota\in[k]$. If $\breve{S}(v.\iota)$
occurs in $\hat{s}$ then it follows due to Equation 1 that
$\breve{S}(x_{\iota})$ occurs in $\xi$. Due to Equation 2 and Statement (b),
it follows that $t\langle v.\iota\rangle\subseteq S_{\iota}$. Thus, our claim
follows. ∎

Lemmas 10 and 11 yield Lemma 1.

##  Appendix 0.C Properties of $\hat{T}_{1}$

In the following we consider the properties of the transducer $\hat{T}_{1}$.
Recall that $\hat{T}_{1}$ is obtained via the p-construction from the
transducer $T_{1}$ and the domain automaton $A$ of $T_{2}$. In particular, we
formally prove the statements we made about $\hat{T}_{1}$ in Section 3. First
we formally prove Lemma 2, that is, we prove the following.

###### Lemma 12

Let $(q,S)$ be a state of $\hat{T}_{1}$ and $S\neq\emptyset$. If the tree $t$
over $\Delta$ is producible by $(q,S)$ then $t\in_{q_{2}\in
S}\bigcap\text{dom}(q_{2})$.

###### Proof

Let $t$ be produced by $(q,S)$ on input $s$ where $s\in T_{\Sigma}$. Clearly,
it is sufficient to show that $[\\![S]\\!]^{A}(t)\Rightarrow t$ due to Lemma
1. We prove our claim by structural induction. Let $s=a(s_{1},\dots,s_{k})$
where $a\in\Sigma_{k}$, $k\geq 0$, and $s_{1},\dots,s_{k}\in T_{\Sigma}$. As
$t$ is produced by $(q,S)$ on input $s$, a right-hand side $\xi$ for $(q,S)$
and $a$ exists such that

$t\in\xi[(q^{\prime},S^{\prime})(x_{i})\leftarrow[\\![(q^{\prime},S^{\prime})]\\!]_{i}^{\hat{T}_{1}}(s_{i})\mid(q^{\prime},S^{\prime})\in\hat{Q}_{1},i\in[k]].$
(1)

This means that

$t=\xi[u\leftarrow t/u\mid u\in V(\xi),\xi[u]\text{ is of the form
}(q^{\prime},S^{\prime})(x_{i})].$

The following statements hold:

  1. 1.

By definition of $\hat{T}_{1}$, it follows that
$[\\![S]\\!]^{A}(\xi)\Rightarrow\xi^{\prime}$ where

$\xi^{\prime}=\xi[u\leftarrow S^{\prime}(u)\mid u\in V(\xi),\xi[u]\text{ is of
the form }(q^{\prime},S^{\prime})(x_{i})].$

  2. 2.

Consider the node $u$. Let $u$ be labeled by $(q^{\prime},S^{\prime})(x_{i})$
in $\xi$. This means that $u$ is labeled by $S^{\prime}(u)$ in $\xi^{\prime}$.
By Equation 1, $t/u$ can be produced by $(q^{\prime},S^{\prime})$ on input
$s_{i}$.

By induction hypothesis, $[\\![S^{\prime}]\\!]^{A}(t^{\prime})\Rightarrow
t^{\prime}$ for all trees $t^{\prime}$ producible by
$(q^{\prime},S^{\prime})$. Thus, $[\\![S^{\prime}]\\!]^{A}(t/u)\Rightarrow
t/u$. By definition $[\\![S^{\prime}]\\!]^{A}(t/u)\Rightarrow t/u$ implies

$[\\![S^{\prime}]\\!]^{A}_{u}(t/u)\Rightarrow t/u$

because $t/u$ is ground.

Statements (1) and (2) yield that $[\\![S]\\!]^{A}(t)\Rightarrow t$. ∎

We now show that the converse holds as well.

###### Lemma 13

Let $s\in T_{\Sigma}$ and $t$ be producible by the state $q_{1}$ of $T_{1}$ on
input $s$. Let $S\subseteq Q_{2}$ such that $t\in\bigcap_{q\in
S}\text{dom}(q)$. Then $t$ be producible by the state $(q_{1},S)$ of
$\hat{T}_{1}$ on input $s$.

###### Proof

We prove our claim by structural induction. Let $s=a(s_{1},\dots,s_{k})$,
$a\in\Sigma_{k}$, $k\geq 0$, and $s_{1},\dots,s_{k}\in T_{\Sigma}$. As $t$ be
producible by the state $q_{1}$ of $T_{1}$ on input $s$,
$\xi\in\text{rhs}_{T_{1}}(q_{1},a)$ exists such that

$t\in\xi[q^{\prime}(x_{i})\leftarrow[\\![q^{\prime}]\\!]^{T_{1}}_{i}(s_{i})\mid
q^{\prime}\in Q_{1},i\in[k]].$

In essence, this means that

$t=\xi[u\leftarrow t/u\mid u\in V(\xi),\xi[u]\text{ is of the form
}q^{\prime}(x_{i})].$

Hence, it follows that if a node $u$ is labeled by $q^{\prime}(x_{i})$ in
$\xi$ then

$[\\![q^{\prime}]\\!]^{T_{1}}_{i}(s_{i})\Rightarrow t/u.$ (*)

By our premise $t\in\bigcap_{q\in S}\text{dom}(q)$. Due to Lemma 1, it follows
that $[\\![S]\\!]^{A}(t)\Rightarrow t$. Therefore, for all leafs $u$ of $\xi$
that are labeled by a symbol in of the form $q_{1}(x_{i})$, a state $S_{u}$ of
$A$ exists such that

$[\\![S]\\!]^{A}(\xi)\Rightarrow\xi[u\leftarrow S_{u}(u)\mid u\in
V(\xi),\xi[u]\in Q_{1}(X)]$

and $[\\![S_{u}]\\!]^{A}_{u}(t/u)\Rightarrow t/u$. By definition of
$\hat{T}_{1}$, the former implies that

$(q_{1},S)(a(x_{1},\dots,x_{k}))\rightarrow\xi[u\leftarrow(q^{\prime},S_{u})(x_{i})\mid
u\in V(\xi),\xi[u]=q^{\prime}(x_{i})]\ (\dagger)$

is a rule of $\hat{T}_{1}$. The later implies
$[\\![S_{u}]\\!]^{A}(t/u)\Rightarrow t/u$ as $t_{u}$ is ground. Therefore,
$t/u\in\bigcap_{q\in S_{u}}\text{dom}(q)$ due to Lemma 1.

Consider an arbitrary node $\breve{u}$ of $\xi$. Let $\breve{u}$ labeled by
$\breve{q}(x_{i})$ in $\xi$. Then, $t/\breve{u}\in\bigcap_{q\in
S_{\breve{u}}}\text{dom}(q)$. Furthermore, due to (*), it follows that
$[\\![\breve{q}]\\!]^{T_{1}}_{i}(s_{i})\Rightarrow t/\breve{u}$.

Then, the induction hypothesis yields that
$[\\![(\breve{q},S_{\breve{u}})]\\!]^{\hat{T}_{1}}(s_{i})\rightarrow
t/\breve{u}$. Note that
$[\\![(\breve{q},S_{\breve{u}})]\\!]^{\hat{T}_{1}}(s_{i})\rightarrow
t/\breve{u}$ implies
$[\\![(\breve{q},S_{\breve{u}})]\\!]^{\hat{T}_{1}}_{i}(s_{i})\rightarrow
t/\breve{u}$ because $s_{i}$ is ground. Along with $(\dagger)$, this yields
our claim. ∎

Lemmas 12 and 13 allow us to prove the following statement, which implies
Lemma 3.

###### Lemma 14

$\text{dom}(\hat{T}_{1})=\text{dom}(T_{1}\,\hat{\circ}\,T_{2})$ and for $s\in
T_{\Sigma}$, $\hat{T}_{1}(s)=T_{1}(s)\cap\text{dom}(T_{2})$.

###### Proof

First we show that
$\text{dom}(\hat{T}_{1})=\text{dom}(T_{1}\,\hat{\circ}\,T_{2})$. Let
$s\in\text{dom}(\hat{T}_{1})$, i.e., a tree $t$ over $\Delta$ exists such that
$[\\![(q_{1}^{0},\\{q_{2}^{0}\\})]\\!]^{\hat{T}_{1}}(s)\Rightarrow t$, where
$(q_{1}^{0},\\{q_{2}^{0}\\})$ is the initial state of $\hat{T}_{1}$. By
construction of $\hat{T}_{1}$, it follows that
$[\\![q_{1}^{0}]\\!]^{{T}_{1}}(s)\Rightarrow t$ and by Lemma 12,
$t\in\text{dom}(q_{2}^{0})$. Hence
$s\in\text{dom}(T_{1}\,\hat{\circ}\,T_{2})$. For the converse, let
$s\in\text{dom}(T_{1}\,\hat{\circ}\,T_{2})$. Then, a tree $t$ over $\Delta$
exists such that $[\\![q_{1}^{0}]\\!]^{{T}_{1}}(s)\Rightarrow t$, where
${q_{1}^{0}}$ is the initial state of $T_{1}$, and $t\in\text{dom}(q_{2})$.
Hence, due to Lemma 13 it follows that
$[\\![(q_{1}^{0},\\{q_{2}^{0}\\})]\\!]^{\hat{T}_{1}}(s)\Rightarrow t$ and
thus, $s\in\text{dom}(\hat{T}_{1})$.

Now we show that $\hat{T}_{1}(s)=T_{1}(s)\cap\text{dom}(T_{2})$ . Let
$[\\![(q_{1}^{0},\\{q_{2}^{0}\\})]\\!]^{\hat{T}_{1}}(s)\Rightarrow t$. By
construction of $\hat{T}_{1}$, $[\\![q_{1}^{0}]\\!]^{{T}_{1}}(s)\Rightarrow t$
holds. By Lemma 12, $t\in\text{dom}(q_{2}^{0})$. Therefore, our claim follows.
Conversely, let $t\in T_{1}(s)\cap\text{dom}(T_{2})$. Then, clearly
$t\in\text{dom}(q_{2}^{0})$ and $[\\![q_{1}^{0}]\\!]^{{T}_{1}}(s)\Rightarrow
t$. By Lemma 13,
$[\\![(q_{1}^{0},\\{q_{2}^{0}\\})]\\!]^{\hat{T}_{1}}(s)\Rightarrow t$ which
yields our claim. ∎

##  Appendix 0.D Correctness of the LA-Transducer $M$

In this section, we present the formal proof of correctness for the la-
transducer $M$, i.e., we show that $M$ is functional if and only if
$T_{1}\,\hat{\circ}\,T_{2}$ is functional. Recall that due to Lemma 3, it is
sufficient to consider $\hat{T}_{1}\,\hat{\circ}\,T_{2}$.

In the following, denote by $L$ the set of states of the la-automaton of $M$.
W.l.o.g. we assume that for all states $l$ in $L$,
$\text{dom}(l)\neq\emptyset$. In the remainder of this section, our proofs
employ partial trees in $T_{\Sigma}[L]$. Consider such a tree $s$. Recall that
in a translation of $M$ input trees are first preprocessed by a relabeling
induced by the la-automaton of $M$. We demand that in a translation of $M$ the
tree $s$ is relabeled as follows: If the $i$-th child of the node $v$ of $s$
is labeled by $l\in L$ then we require that $v$ be relabeled by a symbol of
the form $\langle a,l_{1},\dots l_{i-1},l,l_{i+1},\dots.l_{k}\rangle$.

For instance, consider the la-automaton
$B=(\\{p,p^{\prime}\\},\Sigma,\Sigma,R,\\{p\\})$ where
$\Sigma=\\{f^{2},a^{0},b^{0}\\}$ and $R$ contains the rules

$\begin{array}[]{lclclcl}p(f(x_{1},x_{2}))&\rightarrow&f(p(x_{1}),p(x_{2}))&&p(f(x_{1},x_{2}))&\rightarrow&f(p(x_{1}),p^{\prime}(x_{2}))\\\
p^{\prime}(f(x_{1},x_{2}))&\rightarrow&f(p^{\prime}(x_{1}),p^{\prime}(x_{2}))&&p^{\prime}(f(x_{1},x_{2}))&\rightarrow&f(p^{\prime}(x_{1}),p(x_{2}))\\\
p(a)&\rightarrow&a&&p^{\prime}(b)&\rightarrow&b.\end{array}$

Informally, the state $p$ checks whether or not the leftmost leaf of its input
tree is $a$. The state $p^{\prime}$ does the same for $b$. Consider the tree
$s=f(a,f(p,b))$. For $s$ the tree $\langle f,p,p\rangle(a,\langle
f,p,p^{\prime}\rangle(p,b))$ is a valid relabeling. The tree $\langle
f,p,p^{\prime}\rangle(a,\langle f,p^{\prime},p^{\prime}\rangle(p,b))$ on the
other hand is not.

###  0.D.1 If $M$ is functional then $\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is
functional

In this section we formally prove the only-if statement of Corollary 1, i.e.,
we show that if $M$ is functional then $\hat{T}_{1}\,\hat{\circ}\,_{2}$ is
functional. More precisely we formally show that
$\mathcal{R}(\hat{T}_{1})\circ\mathcal{R}(T_{2})\subseteq\mathcal{R}(M)$.
Obviously this implies our result.

In the following we formally prove Lemma 5. More precisely we prove the
following lemma which is a more detailed version of Lemma 5.

###### Lemma 15

Let $(q_{1},S)$ be a state of $\hat{T}_{1}$ and $q_{2}$ be a state of $T_{2}$.
Let $s\in T_{\Sigma}$. Consider the state $(q_{1},S,q_{2})$ of $M$. If

$[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s)\Rightarrow
t\quad\text{and}\quad[\\![q_{2}]\\!]^{T_{2}}(t)\Rightarrow r$

then $[\\![(q_{1},S,q_{2})]\\!]^{M}(s)\Rightarrow r$.

###### Proof

We prove our claim by induction on the structure of $s$. Let
$s=a(s_{1},\dots,s_{k})$ where $a\in\Sigma_{k}$, $k\geq 0$, and for $i\in[k]$,
$s_{1},\dots,s_{k}\in T_{\Sigma}$. First, we prove the following claim.

###### Claim 16

If $[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s)\Rightarrow t$ and
$[\\![q_{2}]\\!]^{T_{2}}(t)\Rightarrow r$ and
$[\\![(q_{1},S,q_{2})]\\!]^{M}(s)\Rightarrow r$, then trees $\xi$ and $\psi$
exist such that

$\xi\in\text{rhs}_{\hat{T}_{1}}((q_{1},S),a)\quad\text{and}\quad[\\![q_{2}]\\!]^{T_{2}}(\xi)\Rightarrow\psi.$

Furthermore, $\xi$ and $\psi$ have the following properties.

  1. (1)

Let $u$ be a node of $\xi$. If a node of $\psi$ is labeled by
$q_{2}^{\prime}(u)$ then a state $(q_{1}^{\prime},S^{\prime})$ of
$\hat{T}_{1}$ exists such that $u$ is labeled by
$(q_{1}^{\prime},S^{\prime})(x_{\iota})$ in $\xi$, where $\iota\in[k]$, and
$q_{2}^{\prime}\in S^{\prime}$.

  2. (2)

It holds that

$t\in\xi[q(x_{i})\leftarrow[\\![q]\\!]^{T_{1}^{\prime}}(s_{i})\mid q\in
Q_{1}^{\prime},i\in[k]]$

and

$r\in\psi[q(u)\leftarrow[\\![q]\\!]^{T_{2}}(t/u)\mid q\in Q_{2},u\in V(\xi)].$

###### Proof of Claim

By definition, $[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s)\Rightarrow t$ implies
$[\\![q_{1}]\\!]^{{T}_{1}}(s)\Rightarrow t$ and thus

$t\in\xi^{\prime}[q(x_{i})\leftarrow[\\![q]\\!]^{T_{1}}(s_{i})\mid q\in
Q_{1},i\in[k]]$ (1)

for some $\xi^{\prime}\in\text{rhs}(q_{1},a)$. Furthermore, by Lemma 12,
$[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s)\Rightarrow t$ implies that
$t\in\bigcap_{q^{\prime}\in S}\text{dom}(q^{\prime})$. In the following, let
$S=\\{q_{2}^{1},\dots,q_{2}^{n}\\}$. As $t\in\bigcap_{q^{\prime}\in
S}\text{dom}(q^{\prime})$ and due to Equation 1, for all $j\in[n]$, trees
$\psi_{j}$ and $r_{j}$ exists such that

  1. (a)

$[\\![q_{2}^{j}]\\!]^{T_{2}}(\xi^{\prime})\Rightarrow\psi_{j}$ and

  2. (b)

$[\\![q_{2}^{j}]\\!]^{T_{2}}(t)\Rightarrow r_{j}$ such that

$r_{j}\in\psi_{j}[q_{2}^{\prime}(u)\leftarrow[\\![q_{2}^{\prime}]\\!]^{T_{2}}(t/u)\mid
q_{2}^{\prime}\in Q_{2},u\in V(\xi^{\prime})].$

By our premise, the state $(q_{1},S,q_{2})$ of $M$ is defined which implies
that $q_{2}\in S$. W.l.o.g. let $q_{2}^{1}=q_{2}$. Furthermore, as
$[\\![q_{2}]\\!]^{T_{2}}(t)\Rightarrow r$, we can also assume that $r_{1}=r$.

Recall that by definition, if a node of $\psi_{j}$ is labeled by
$q_{2}^{\prime}(u)$, where $q_{2}^{\prime}\in Q_{2}$ and $u$ is a node, then
the node $u$ is labeled by some symbol in $Q_{1}(X)$ in $\xi^{\prime}$. Let
$u_{1},\dots,u_{m}$ be the nodes of $\xi^{\prime}$ that are labeled by a
symbol in $Q_{1}(X)$.

In the following we first prove Statement (1). Due to Lemma 10, (a) implies

$[\\![S]\\!]^{A}(\xi^{\prime})\Rightarrow\xi^{\prime}[u_{i}\leftarrow
S_{i}(u_{i})\mid i\in[m]],$

where $A$ is the domain automaton of $T_{2}$ and
$S_{i}=\bigcup_{j\in[n]}\psi_{j}\langle u_{i}\rangle$, which in turn implies
that $\hat{T}_{1}$ contains the rule
$(q_{1},S)(a(x_{1},\dots,x_{k}))\rightarrow\xi$ where

$\xi=\xi^{\prime}[u_{i}\leftarrow(q^{\prime},S_{i})(x_{\iota})\mid\xi[u_{i}]=q^{\prime}(x_{\iota}),\iota\in[k]]$

as $\hat{T}_{1}$ is obtained from the p-construction of $T_{1}$ and $A$. In
the following, consider the node $u_{i}$. Assume that in $\psi_{j}$ a node
labeled by $q_{2}^{\prime}(u_{i})$ occurs. Recall that this means that the
node $u_{i}$ is labeled by a symbol of the form $q^{\prime}(x_{\iota})$ in
$\xi^{\prime}$. By construction, $u_{i}$ is labeled by $q^{\prime}(x_{\iota})$
in $\xi^{\prime}$ if and only if $u_{i}$ is labeled by $q^{\prime}(x_{\iota})$
in $\xi^{\prime}$. As $S_{i}=\bigcup_{j\in[n]}\psi_{j}\langle u_{i}\rangle$,
obviously $q_{2}^{\prime}\in S_{i}$.

As $q_{2}^{1}=q_{2}$, Statement (1) follows with $\psi=\psi_{1}$. Note that
clearly, for all $j\in[n]$, it holds that

$[\\![q_{2}^{j}]\\!]^{T_{2}}(\xi^{\prime})\Rightarrow\psi_{j}\quad\text{if and
only if}\quad[\\![q_{2}^{j}]\\!]^{T_{2}}(\xi)\Rightarrow\psi_{j}.$ (2)

We now prove Statement (2). In particular, we prove the first part of
Statement (2), i.e., that

$t\in\xi[q(x_{i})\leftarrow[\\![q]\\!]^{T_{1}^{\prime}}(s_{i})\mid q\in
Q_{1}^{\prime},i\in[k]].$

Let the node $u_{i}$ be labeled by $(q^{\prime}_{1},S_{i})(x_{\iota})$ in
$\xi$. Consider an arbitrary state $q_{2}^{\prime}\in S_{i}$ where $i\in[m]$.
In particular, this means that $q_{2}^{\prime}\in\psi_{j}\langle u_{i}\rangle$
for some $j\in[n]$. In other words, a node $g$ exists such that $g$ is labeled
by $q_{2}^{\prime}(u_{i})$ in $\psi_{j}$. Clearly, Statement (b) implies that
$q_{2}^{\prime}$ can produce the tree $r_{j}/g$ on input $t/u_{i}$. This
statement can be generalized. More precisely, it holds that any state
$q_{2}^{\prime}\in S_{i}$ can produce some output tree on input $t/u_{i}$.
Therefore, $t/u_{i}\in\bigcap_{q_{2}^{\prime}\in
S_{i}}\text{dom}(q_{2}^{\prime})$. Equation 1 implies that
$[\\![q^{\prime}_{1}]\\!]^{T_{1}}(s_{\iota})\Rightarrow t/u_{i}$ if
$\xi^{\prime}[u_{i}]=q^{\prime}_{1}(x_{\iota})$. Together with Lemma 13 and as
$t/u_{i}\in\bigcap_{q_{2}^{\prime}\in S_{i}}\text{dom}(q_{2}^{\prime})$, it
follows that

$[\\![(q^{\prime}_{1},S_{i})]\\!]^{\hat{T}_{1}}(s_{\iota})\Rightarrow
t/u_{i}.$

By construction the node $u_{i}$ is labeled by
$(q^{\prime}_{1},S_{i})(x_{\iota})$ in $\xi$ if and only if $u_{i}$ is labeled
by $q^{\prime}(x_{\iota})$ in $\xi^{\prime}$. With the rule
$(q_{1},S)(a(x_{1},\dots,x_{k}))\rightarrow\xi$ and Equation 1 it follows that
the $(q_{1},S)$ can generate the tree $t$ on input $s$. More precisely, it
follows that

$t\in\xi[q(x_{i})\leftarrow[\\![q]\\!]^{\hat{T}_{1}}(s_{i})\mid q\in
Q_{1}^{\prime},i\in[k]].$

The second part of Statement (2) follows due to Statement (b) and Equation 2.
∎

Let $\xi$ and $\psi$ be as in Claim 16. Due to Statement (1) of Claim 16, it
follows that $M$ contains the rule

$(q_{1},S,q_{2})(a(x_{1}\\!:\\!l_{1},\dots,x_{k}\\!:\\!l_{k}))\rightarrow\gamma$

where $\gamma$ is obtained from $\psi$ by substituting occurrences of
$q_{2}^{\prime}(u)$ in $\psi$, where $q_{2}^{\prime}\in Q_{2}$ and $u$ is a
leaf of $\xi$ labeled by a symbol of the form
$(q^{\prime}_{1},S^{\prime})(x_{i})$, by
$(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(x_{i})$. Furthermore, for
$i\in[k]$, $\xi\langle x_{i}\rangle=l_{i}$.

We now show that $[\\![(q_{1},S,q_{2})]\\!]^{M}(s)\Rightarrow r$. Recall that
$s=a(s_{1},\dots,s_{k})$ where $a\in\Sigma_{k}$, $k\geq 0$, and for $i\in[k]$,
$s_{1},\dots,s_{k}\in T_{\Sigma}$. Note that as $\xi\langle
x_{i}\rangle=l_{i}$ and due to Statement (2) of Claim 16 and Lemma 1,
$s_{i}\in\text{dom}(l_{i})$ for $i\in[k]$.

Consider a node $g$. By definition of $\gamma$, $g$ is labeled by
$(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(x_{i})$ in $\gamma$ if and only if
$g$ is labeled by $q^{\prime}_{2}(u)$ in $\psi$ and the node $u$ is labeled by
$(q_{1}^{\prime},S^{\prime})(x_{i})$ in $\xi$. Statement (2) of Claim 16
implies that
$[\\![(q_{1}^{\prime},S^{\prime})]\\!]^{\hat{T}_{1}}(s_{i})\Rightarrow t/u$
and $[\\![q^{\prime}_{2}]\\!]^{T_{2}}(t/u)\Rightarrow r/g$. Therefore, by
induction hypothesis,
$[\\![(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})]\\!]^{M}(s_{i})\Rightarrow
r/g$. Clearly, our claim follows. ∎

Clearly, Lemma 15 implies Lemma 4. Lemma 15 also yields the following two
auxiliary results.

###### Lemma 17

Let $(q_{1},S)$ be a state of $\hat{T}_{1}$ and $q_{2}$ be a state of $T_{2}$
such that $q_{2}\in S$. Then, for the state $(q_{1},S,q_{2})$ of $M$,
$\text{dom}((q_{1},S,q_{2}))=\text{dom}((q_{1},S))$ holds.

###### Proof

Let $s=a(s_{1},\dots,s_{k})$, $a\in\Sigma_{k}$, $k\geq 0$ and
$s_{1},\dots,s_{k}\in T_{\Sigma}$. Let $s\in\text{dom}((q_{1},S,q_{2}))$,
i.e., $[\\![(q_{1},S,q_{2})]\\!](s)\Rightarrow r$ for some tree $r$. Consider
the first rule of $M$ applied in this translation. Let

$\eta=(q_{1},S,q_{2})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma$

be this rule. By construction $\eta$ is obtained from a rule
$(q_{1},S)(a(x_{1},\dots,x_{k}))\rightarrow\xi$ of $\hat{T}_{1}$ such that for
$i\in[k]$, $\xi\langle x_{i}\rangle\subseteq l_{i}$. The application of $\eta$
implies $s_{i}\in l_{i}$ for $i\in[k]$. This implies
$s\in\text{dom}((q_{1},S))$.

Conversely, let $s\in\text{dom}((q_{1},S))$, i.e.,
$[\\![(q_{1},S)]\\!](s)\rightarrow t$ for some tree $t$. Note that the state
$(q_{1},S,q_{2})$ of $M$ implies $q_{2}\in S$. Due to Lemma 12, it follows
that $[\\![q_{2}]\\!]^{T_{2}}(t)\neq\emptyset$. Therefore, we deduce that due
to Lemma 15, $s\in\text{dom}((q_{1},S,q_{2}))$. ∎

###### Lemma 18

Let $s\in T_{\Sigma}[L]$. Let $M(s)\Rightarrow r_{M}$ and let
$(q_{1},S,q_{2})(v)$ occurs in $r_{M}$, where $(q_{1},S,q_{2})$ is a state of
$M$ and $v$ is a node of $s$ labeled by a symbol $l\in L$. Then
$\text{dom}(l)\subseteq\text{dom}((q_{1},S,q_{2}))$.

###### Proof

Let the parent node of $v$ be labeled by $a\in\Sigma_{k}$ where $k>0$.
W.l.o.g. let $v$ be the first child of its parent node. Then, clearly the
occurrence of $(q_{1},S,q_{2})(v)$ in $r_{M}$ originates from the application
of a rule
$(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma$
of $M$ such that $(q_{1},S,q_{2})(x_{1})$ occurs in $\gamma$. Recall that by
definition, $l_{1},\dots l_{k}$ are sets of states of $\hat{T}_{1}$. By the
definition of relabelings of trees in $T_{\Sigma}[L]$, the parent node of $v$
is relabeled by a symbol of the form $\langle a,l,l^{\prime}_{2},\dots
l_{k}^{\prime}\rangle$ which implies $l=l_{1}$.

Consider the rule
$(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma$.
Recall that by construction of $M$, this rule is obtained from a rule
$(q_{1}^{\prime},S^{\prime})(a(x_{1},\dots,x_{k}))\rightarrow\xi$ of
$\hat{T}_{1}$ such that for $i\in[k]$, $\xi\langle x_{i}\rangle\subseteq
l_{i}$. Note that the occurrence of $(q_{1},S,q_{2})(x_{1})$ in $\gamma$
implies that $(q_{1},S)(x_{1})$ occurs in $\xi$. Therefore, the state
$(q_{1},S)$ of $\hat{T}_{1}$ is included in $l$. As $s\in\text{dom}(l)$ if and
only if $s\in\bigcap_{\hat{q}\in l}\text{dom}(\hat{q})$, our claim follows due
to Lemma 17. ∎

###  0.D.2 If $\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional then $M$ is
functional.

In this section we formally prove the only-if statement of Corollary 1, i.e.,
we show that if $\hat{T}_{1}\,\hat{\circ}\,T_{2}$ is functional then $M$ is
functional.

First we introduce the following definition. Recall that we have introduced
_synchronized_ translations of $M$ in Section 3.1. In the following, we extend
this definition. Let $s\in T_{\Sigma}[L]$. We call the trees $s$, $t$, $r$ and
$r_{M}$ _synchronized_ if

  1. 1.

$\hat{T}_{1}(s)\Rightarrow t$ and $T_{2}(t)\Rightarrow r$ and $M(s)\Rightarrow
r_{M}$ and

  2. 2.

the tree $r_{M}$ is obtained from $r$ by substituting all occurrences of
$q_{2}^{\prime}(u)$ in $r$ by $(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(v)$,
where $(q^{\prime}_{1},S^{\prime})$ and $q_{2}^{\prime}$ are states of
$\hat{T}_{1}$ and $T_{2}$, respectively, and $u$ is a leaf of $t$ labeled by
$(q^{\prime}_{1},S^{\prime})(v)$.

Informally, $s$, $t$, $r$ and $r_{M}$ are _synchronized_ if on input $s$, $M$
produces the tree $r_{M}$ by accurately simulating
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$. More precisely: Recall that when a state
$(q_{1},S,q_{2})$ of $M$ processes a subtree $s^{\prime}$ of $s$ then
$(q_{1},S,q_{2})$ guesses what the state $(q_{1},S)$ of $\hat{T}_{1}$ might
have produced before producing output according to this guess. Informally, if
all such guesses of $M$ are correct, i.e., the states of $\hat{T}_{1}$ have
indeed produced the trees $M$ has guessed, then $s$, $t$, $r$ and $r_{M}$ are
_synchronized_.

Before we prove a more detailed version of Lemma 6, recall that by definition,
a state $l$ in $L$ is a set of states of $\hat{T}_{1}$. Consider a tree $s\in
T_{\Sigma}[L]$. Informally, if a symbol $l\in L$ occurs at some leaf of $s$
then $l$ can be considered a placeholder for some tree $s^{\prime}$ such that
$s^{\prime}\in\bigcap_{(q_{1},S)\in l}\text{dom}(q_{1},S)$. We now show that
the following holds.

###### Lemma 19

Let $s\in T_{\Sigma}[L]$. Let $M(s)\Rightarrow r_{M}$ and let
$(q_{1},S,q_{2})(v)$ occur in $r_{M}$. Then trees $t$, $r$ and
$r_{M}^{\prime}$ exist such that $s$, $t$, $r$ and $r_{m}^{\prime}$ are
synchronized and $(q_{1},S,q_{2})(v)$ occurs in $r^{\prime}_{M}$. Furthermore,
let $v^{\prime}$ be a leaf of $s$ that is labeled by $l\in L$. Then, it holds
that if $(q^{\prime}_{1},S^{\prime})(v^{\prime})$ occurs in $t$ then
$(q^{\prime}_{1},S^{\prime})\in l$.

###### Proof

We prove our claim by structural induction. First, let $\bar{v}$ be a node of
$s$ such that the subtree of $s$ rooted at $\bar{v}$ is of the form
$a(l_{1},\dots,l_{k})$ where $a\in\Sigma_{k}$, $k\geq 0$, and
$l_{1},\dots,l_{k}\in L$. Note that by definition $\bar{v}$ can be a leaf.
Then, a state $l\in L$ exists such that

$l(a(x_{1},\dots,x_{k}))\rightarrow a(l_{1}(x_{1}),\dots,l_{k}(x_{k}))$

is a rule of the la-automaton of $M$. Furthermore, as $M(s)\Rightarrow r_{M}$,
on input $\bar{s}=s[\bar{v}\leftarrow l]$, the $M$ produces the tree
$\bar{r}_{M}$ such that

$r_{M}\in\bar{r}_{M}[(q)(\bar{v})\leftarrow[\\![q]\\!]^{M}_{\bar{v}}(a(l_{1},\dots,l_{k}))\mid
q\text{ is a state of }M].$

We remark that all trees in $[\\![q]\\!]^{M}_{\bar{v}}(a(l_{1},\dots,l_{k}))$
are of the form $\gamma\langle x_{i}\leftarrow\bar{v}.i\mid i\in[k]\rangle$
where $\gamma\in\text{rhs}(q,a,l_{1},\dots,l_{k})$. Recall that by our
premise, $(q_{1},S,q_{2})(v)$ occurs in $r_{M}$. Then one of the following
cases arises:

  1. (a)

$(q_{1},S,q_{2})(v)$ does not already occur in $\bar{r}_{M}$.

  2. (b)

$(q_{1},S,q_{2})(v)$ already occurs in $\bar{r}_{M}$.

First, we consider case (b). By induction hypothesis, as
$M(\bar{s})\Rightarrow\bar{r}_{M}$ and a node labeled by $(q_{1},S,q_{2})(v)$
occurs in $\bar{r}_{M}$, trees $\bar{t}$, $\bar{r}$ and $\bar{r}_{M}^{\prime}$
exist such that $\bar{s}$, $\bar{t}$, $\bar{r}$ and $\bar{r}_{M}^{\prime}$ are
synchronized and $(q_{1},S,q_{2})(v)$ occurs in $\bar{r}^{\prime}_{M}$.
Furthermore, by induction hypothesis, it holds that if
$(q^{\prime}_{1},S^{\prime})(\bar{v})$ occurs in $\bar{t}$ then
$(q^{\prime}_{1},S^{\prime})\in l$.

First, we construct the tree $t$. Recall that the la-automaton of $M$ is the
domain automaton of $\hat{T}_{1}$. Therefore the existence of rule

$l(a(x_{1},\dots,x_{k}))\rightarrow a(l_{1}(x_{1}),\dots,l_{k}(x_{k}))$

of the la-automaton implies that for all states
$(q^{\prime}_{1},S^{\prime})\in l$, a right-hand side
$\xi^{\prime}\in\text{rhs}_{\hat{T}_{1}}((q_{1}^{\prime},S^{\prime}),a)$
exists such that $\xi^{\prime}\langle x_{i}\rangle\subseteq l_{i}$ for
$i\in[k]$ $(*)$.

In the following, we define
$t_{(q_{1}^{\prime},S^{\prime})}=\xi^{\prime}\langle
x_{i}\leftarrow\bar{v}.i\mid i\in[k]\rangle$ if
$(q^{\prime}_{1},S^{\prime})\in l$. Then clearly $\hat{T}_{1}(s)\Rightarrow t$
where

$t=\bar{t}[(q^{\prime}_{1},S^{\prime})(\bar{v})\leftarrow
t_{(q_{1}^{\prime},S^{\prime})}\mid(q^{\prime}_{1},S^{\prime})\in
Q_{1}^{\prime}].$

We now show that for arbitrary nodes $v^{\prime}$ of $s$ it holds that if
$v^{\prime}$ is labeled by $l$ in $s$ and
$(q^{\prime}_{1},S^{\prime})(v^{\prime})$ occurs in $t$ then
$(q^{\prime}_{1},S^{\prime})\in l$. Due to (*), this holds for all nodes
$v^{\prime}$ that are descendants of $\bar{v}$. Now assume that $v^{\prime}$
is not be a descendant of $\bar{v}$. Let $v^{\prime}$ be labeled by the symbol
$\bar{l}\in L$ in $s$. Then obviously, the node $v^{\prime}$ is also labeled
by $\bar{l}$ in $\bar{s}$. Thus, by definition of $\bar{t}$, if
$(q^{\prime}_{1},S^{\prime})(v^{\prime})$ occurs in $\bar{t}$ then
$(q^{\prime}_{1},S^{\prime})\in\bar{l}$. By construction of $t$,
$(q^{\prime}_{1},S^{\prime})(v^{\prime})$ occurs in $t$ if and only if
$(q^{\prime}_{1},S^{\prime})(v^{\prime})$ occurs in $\bar{t}$. This yields our
claim.

We now construct $r$ and $r_{M}^{\prime}$. First recall that, by induction
hypothesis, the trees $\bar{s}$, $\bar{t}$, $\bar{r}$ and
$\bar{r}_{M}^{\prime}$ are synchronized. Therefore, for an arbitrary node $g$
the following holds: $g$ is labeled by
$(q^{\prime}_{1},S^{\prime},q_{2}^{\prime})(v)$ in $\bar{r}_{M}$ if and only
if $g$ is labeled by $q_{2}^{\prime}(u)$ in $\bar{r}$ and $u$ is a node of
$\bar{t}$ labeled by $(q^{\prime}_{1},S^{\prime})(v)$ $(\dagger)$.

Now let the node $g$ be labeled by $q_{2}^{\prime}(u)$ in $\bar{r}$ and let
the node $u$ be labeled by $(q^{\prime}_{1},S^{\prime})(\bar{v})$ in
$\bar{t}$. Consider the right-hand side $\xi^{\prime}$ assigned to the state
$(q^{\prime}_{1},S^{\prime})$ in $(*)$. Due to how rules of $\hat{T}_{1}$ are
defined, it holds that

$[\\![S^{\prime}]\\!]^{A}(\xi^{\prime})\Rightarrow\xi^{\prime}[u\leftarrow\bar{S}(u)\mid
u\in V(\xi^{\prime}),\xi^{\prime}[u]=(\bar{q},\bar{S})(x_{i})].$

Note that $(\dagger)$ implies $q_{2}^{\prime}\in S$. This follows as the state
$(q^{\prime}_{1},S^{\prime},q_{2}^{\prime})$ is defined. Therefore by Lemma
11, a tree $\psi^{\prime}$ exists such that

  1. 1.

$[\\![q_{2}^{\prime}]\\!]^{T_{2}}(\xi^{\prime})\Rightarrow\psi^{\prime}$ and

  2. 2.

if the node $u^{\prime}$ is labeled by $(\tilde{q},\tilde{S})(x_{i})$ in
$\xi^{\prime}$ then ${\psi^{\prime}}\langle
u^{\prime}\rangle\subseteq\tilde{S}$.

The later implies that if $\tilde{q}_{2}(u^{\prime})$ occurs in
$\psi^{\prime}$ then $\tilde{q}_{2}\in\tilde{S}$. Due to $(*)$, for $i\in[k]$,
it holds that $\xi^{\prime}\langle x_{i}\rangle\subseteq l_{i}$. Therefore, by
construction of $M$ the rule

$(q^{\prime}_{1},S^{\prime},q_{2}^{\prime})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma^{\prime}$

is defined where $\gamma^{\prime}$ is obtained from $\psi^{\prime}$ by
substituting occurrences of $\tilde{q}_{2}(u^{\prime})$ in $\psi$ by
$(\tilde{q}_{1},\tilde{S},\tilde{q}_{2})(x_{i})$, where
$(\tilde{q}_{1},\tilde{S})$ and $\tilde{q}_{2}$ are states of $\hat{T}_{1}$
and $T_{2}$, respectively, and $u^{\prime}$ is a leaf of $\xi^{\prime}$
labeled by a symbol of the form $(\tilde{q}_{1},\tilde{S})(x_{i})$.

For the node $g$ we define $r_{T_{2},g}=\psi^{\prime}\langle
u^{\prime}\leftarrow u.u^{\prime}\mid u^{\prime}\in V\rangle$. Additionally,
we define $r_{M,g}=\gamma^{\prime}\langle x_{i}\leftarrow\bar{v}.i\mid
i\in[k]\rangle$.

Recall that $(\dagger)$ holds. Then, $T_{2}(t)\Rightarrow r$ where

$r=\bar{r}[g\leftarrow r_{T_{2},g}\mid\bar{r}[g]=q_{2}^{\prime}(u)\text{ and
}\bar{t}[u]=(q_{1}^{\prime},S^{\prime})(\bar{v})]$

and $M(s)\Rightarrow r_{M}^{\prime}$ where

$r_{M}^{\prime}=\bar{r}_{M}^{\prime}[g\leftarrow
r_{M,g}\mid\bar{r}_{M}[g]=(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(\bar{v})].$

Note that the node $\bar{v}$ of $s$ is relabeled by $\langle
a,l_{1},\dots,l_{k}\rangle$ via the relabeling induced by the rule
$l(a(x_{1},\dots,x_{k}))\rightarrow a(l_{1}(x_{1}),\dots,l_{k}(x_{k}))$ of the
la-automaton of $M$. Thus, $r_{M}^{\prime}$ is well defined. Clearly,
$\hat{T}_{1}(s)\Rightarrow t$ and $T_{2}(t)\Rightarrow r$ and $M(s)\Rightarrow
r_{M}^{\prime}$. Due to $(\dagger)$ and the construction of $r$ and
$r_{M}^{\prime}$, it follows that the second part of the synchronized-property
holds as well.

We now consider case (a). As $(q_{1},S,q_{2})(v)$ occurs in $r_{M}$ but not in
$\bar{r}_{M}$, it follows that $v=\bar{v}.i$ for some $i\in[k]$. W.l.o.g. let
$v=\bar{v}.1$, i.e., $v$ is the first child of the node $\bar{v}$.
Furthermore, it follows that a rule

$(\tilde{q}_{1},\tilde{S},\tilde{q}_{2})(a(x_{1}\\!:\\!l_{1},\dots,x_{k}\\!:\\!l_{k}))\rightarrow\tilde{\gamma}$

exists such that $(\tilde{q}_{1},\tilde{S},\tilde{q}_{2})(\bar{v})$ occurs in
$\bar{r}_{M}$ and $(q_{1},S,q_{2})(x_{1})$ occurs in $\tilde{\gamma}$. Let the
rule of $M$ above be obtained from the rule
$(\tilde{q}_{1},\tilde{S})(a(x_{1},\dots,x_{k}))\rightarrow\tilde{\xi}$ of
$\hat{T}_{1}$ and subsequently translating $\tilde{\xi}$ by the state
$\tilde{q}_{2}$ of $T_{2}$. In particular, this means that a tree
$\tilde{\psi}$ exists such that

  1. (a)

$[\\![\tilde{q}_{2}]\\!]^{T_{2}}(\tilde{\xi})\Rightarrow\tilde{\psi}$ and

  2. (b)

$\tilde{\gamma}$ is obtained from $\tilde{\psi}$ by substituting occurrences
of $q_{2}^{\prime}(u)$ in $\tilde{\psi}$ by
$(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(x_{i})$, where
$(q_{1}^{\prime},S^{\prime})$ and $q_{2}^{\prime}$ are states of $\hat{T}_{1}$
and $T_{2}$, respectively, and $u$ is a leaf of $\xi^{\prime}$ labeled by
$(q^{\prime}_{1},S^{\prime})(x_{i})$,

By induction hypothesis, as $M(\bar{s})\Rightarrow\bar{r}_{M}$ and a node
labeled by $(\tilde{q}_{1},\tilde{S},\tilde{q}_{2})(\bar{v})$ occurs in
$\bar{r}_{M}$, trees $\bar{t}$, $\bar{r}$ and $\bar{r}_{M}^{\prime}$ exist
such that $\bar{s}$, $\bar{t}$, $\bar{r}$ and $\bar{r}_{M}^{\prime}$ are
synchronized and $(\tilde{q}_{1},\tilde{S},\tilde{q}_{2})(\bar{v})$ occurs in
$\bar{r}^{\prime}_{M}$.

Let the node $\bar{g}$ be labeled by
$(\tilde{q}_{1},\tilde{S},\tilde{q}_{2})(\bar{v})$ in $\bar{r}^{\prime}_{M}$.
Due to the synchronized property, the node $\bar{g}$ is labeled by
$q_{2}(\bar{u})$ in $\bar{r}$, where $\bar{u}$ is a node that is labeled by
$(q_{1},S)(\bar{v})$ in $\bar{t}$.

To construct the trees $t$, $r$ and $r_{M}^{\prime}$, we then proceed as in
case (b) but set

  * •

$t_{(\tilde{q}_{1},\tilde{S})}=\tilde{\xi}\langle x_{i}\leftarrow\bar{v}.i\mid
i\in[k]\rangle$,

  * •

$r_{T_{2},\hat{g}}=\tilde{\psi}\langle
u^{\prime}\leftarrow\bar{u}.u^{\prime}\mid u^{\prime}\in V\rangle$ and

  * •

$r_{M,\hat{g}}=\tilde{\gamma}\langle x_{i}\leftarrow\bar{v}.i\mid
i\in[k]\rangle$.

This yields our claim. ∎

Lemma 19 and and Proposition 1 allow us to formally prove the following
version of Lemma 7.

###### Lemma 20

Let $s\in T_{\Sigma}[L]$ such that only a single node $v$ of $s$ is labeled by
a symbol in $L$. Let $v$ be labeled by $l\in L$. Let $M(s)\Rightarrow r_{M}$
such that $(q_{1},S,q_{2})(v)$ occurs in $r_{M}$.

Consider the tree $\tilde{s}=s[v\leftarrow s^{\prime}]$ where
$s^{\prime}\in\text{dom}(l)$. If $T_{1}\,\hat{\circ}\,T_{2}(\tilde{s})$ is a
singleton then $[\\![(q_{1},S,q_{2})]\\!](s^{\prime})$ is a singleton.

###### Proof

Note that by Lemma 18, $s^{\prime}\in\text{dom}((q_{1},S,q_{2}))$. Hence,
$[\\![(q_{1},S,q_{2})]\\!](s^{\prime})\neq\emptyset$. Assume that
$[\\![(q_{1},S,q_{2})]\\!](s^{\prime})$ is not a singleton, i.e., assume that
distinct trees $r_{1}$, $r_{2}$ exist such that
$r_{1},r_{2}\in[\\![(q_{1},S,q_{2})]\\!](s^{\prime})$.

We claim that for $r_{1}$, a tree $t_{1}$ exists such that

  1. 1.

on input $s^{\prime}$, the state $(q_{1},S)$ of $\hat{T}_{1}$ produces $t_{1}$
and

  2. 2.

on input $t_{1}$, the state $q_{2}$ of $T_{2}$ produces $r_{1}$.

We will later prove this claim in detail. It can be shown that a tree $t_{2}$
with the same properties exists for $r_{2}$.

Using this claim and Proposition 1, we now prove that contrary to the
assumption $r_{1}=r_{2}$.

Due to Lemma 19, as $M(s)\Rightarrow r_{M}$ and $(q_{1},S,q_{2})(v)$ occurs in
$r_{M}$, it follows that trees $t$, $r$ and $r_{M}^{\prime}$ exist such that
$s$, $t$, $r$ and $r_{M}^{\prime}$ are synchronized and $(q_{1},S,q_{2})(v)$
occurs in $r_{M}^{\prime}$. Moreover, if $(q^{\prime},S^{\prime})(v)$ occurs
in $t$, where $(q^{\prime},S^{\prime})$ is some state of $\hat{T}_{1}$, then
$(q^{\prime},S^{\prime})\in l$. Recall that by our premise, $v$ is labeled by
$l$ in $s$. Therefore,
$\text{dom}(l)\subseteq\text{dom}((q^{\prime},S^{\prime}))$ due to Lemma 1.
Consequently, $s^{\prime}\in\text{dom}((q^{\prime},S^{\prime}))$. Therefore,
for all states $(q^{\prime},S^{\prime})$ of $\hat{T}_{1}$ such that
$(q^{\prime},S^{\prime})(v)$ occurs in $t$, a tree $t^{\prime}$ exists such
that $[\\![(q^{\prime},S^{\prime})]\\!]^{\hat{T}_{1}}(s^{\prime})\Rightarrow
t^{\prime}$. In the following, let $t\langle
v\rangle=\\{(q^{1},S^{1}),\dots,(q^{n},S^{n})\\}$ and for $j\in[n]$, let
$[\\![(q^{j},S^{j})]\\!]^{\hat{T}_{1}}(s^{\prime})\Rightarrow t_{j}^{\prime}$.
Then clearly on input $\tilde{s}$, the transducer $\hat{T}_{1}$ can produce
the tree $\tilde{t}$ where

$\tilde{t}=t[(q^{j},S^{j})(v)\leftarrow t_{j}^{\prime}\mid j\in[n]].$

Now consider the tree $r$. Let $q^{\prime}_{2}$ be a state of $T_{2}$ and $u$
be a node. By definition of $t$ and $r$, if $q^{\prime}_{2}(u)$ occurs in $r$,
then the node $u$ is labeled by a symbol of the form
$(q^{\prime},S^{\prime})(v)$ in $t$. Furthermore, the synchronized property
implies that $q_{2}^{\prime}\in S^{\prime}$. This follows as a state
$(q^{\prime},S^{\prime},q_{2}^{\prime})$ of $M$ has the property that
$q_{2}^{\prime}\in S^{\prime}$. The subtree of $\tilde{t}$ rooted at $u$ is a
tree $t^{\prime}$ such that
$[\\![(q^{\prime},S^{\prime})]\\!]^{\hat{T}_{1}}(s^{\prime})\Rightarrow
t^{\prime}$. By Lemma 12, it follows that $t^{\prime}\in\text{dom}(q_{2})$.
Therefore, it follows easily that $T_{2}(\tilde{t})\Rightarrow\tilde{r}$ where

$\tilde{r}=r[q_{2}^{\prime}(u)\leftarrow r_{u}\mid q_{2}^{\prime}\in
Q_{2},\tilde{t}[u]=t_{j}^{\prime}\text{ and
}[\\![q_{2}^{\prime}]\\!]^{T_{2}}(t_{j}^{\prime})\Rightarrow r_{u}].$

By our premise a node $g$ exists such that $g$ is labeled by
$(q_{1},S,q_{2})(v)$ in $r_{M}^{\prime}$. As the trees $s$, $t$, $r$ and
$r_{M}^{\prime}$ are synchronized, $g$ is labeled by $q_{2}(u)$ in $r$ where
$u$ is a node of $t$ such that $t[u]=(q_{1},S)(v)$. Due to our claim, a tree
$t_{1}$ exists such that
$[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s^{\prime})\Rightarrow t_{1}$ and and
$[\\![q_{2}]\\!]^{T_{2}}(t_{1})\Rightarrow r_{1}$. W.l.o.g. we assume that
$(q^{1},S^{1})=(q_{1},S)$ and $t_{1}^{\prime}=t_{1}$. Then, it follows easily
that on input $\tilde{s}$, the composition $\hat{T}_{1}\,\hat{\circ}\,T_{2}$
can produce a tree $\tilde{r}_{1}$ such that $\tilde{r}_{1}/g=r_{1}$.
Analogously, it follows easily that on input $\tilde{s}$, the composition
$\hat{T}_{1}\,\hat{\circ}\,T_{2}$ can produce a tree $\tilde{r}_{2}$ such that
$\tilde{r}_{2}/g=r_{2}$. Due to Proposition 1, $\tilde{r}_{1}=\tilde{r}_{2}$
and therefore

$r_{1}=\tilde{r}_{1}/g=\tilde{r}_{2}/g=r_{2}.$

Now all that is left is to prove our previous claim that for $r_{1}$ and
$r_{2}$, trees $t_{1}$ and $t_{2}$ exist such that

  * •

$[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s^{\prime})\Rightarrow t_{1}$ and and
$[\\![q_{2}]\\!]^{T_{2}}(t_{1})\Rightarrow r_{1}$

  * •

$[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s^{\prime})\Rightarrow t_{2}$ and and
$[\\![q_{2}]\\!]^{T_{2}}(t_{2})\Rightarrow r_{2}$.

We prove our claim for $r_{1}$. The proof for $r_{2}$ is analogous. Let
$s^{\prime}=a(s_{1},\dots,s_{k})$ where $a\in\Sigma_{k}$, $k\geq 0$, and
$s_{1},\dots,s_{k}\in T_{\Sigma}$. As $r_{1}$ is producible by
${(q_{1},S,q_{2})}$ on input $s^{\prime}$, it follows that

$r_{1}\in\gamma[q_{M}(x_{i})\leftarrow[\\![q_{M}]\\!](s_{i})\mid i\in[k]\text{
and }q_{M}\text{ is a state of }M]$ (2)

where
$(q_{1},S,q_{2})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma$ is
a rule of $M$, $l_{1},\dots,l_{k}$ are states of the la-automaton of $M$ and
for $i\in[k]$, $s_{i}\in\text{dom}(l_{i})$.

Before we prove our claim, we prove the following result by induction on the
statement of Lemma 20.

###### Claim 21

Let $q_{M}$ be a state of $M$ and let $q_{M}(x_{i})$ occur $\gamma$ where
$i\in[k]$. Then the set $[\\![q_{M}]\\!](s_{i})$ is a singleton.

###### Proof of Claim

Before, we prove our claim consider the following. Let $q_{M}^{\prime}$ be a
state of $M$. Then, by Lemma 18, $s^{\prime}\in\text{dom}(q_{M}^{\prime})$, if
$q_{M}^{\prime}(v)$ occurs in $r_{M}$ $(\dagger)$.

Now, we prove our claim. W.l.o.g., we consider the case $i=1$. Consider the
tree $\bar{s}=a(l_{1},s_{2},\dots,s_{k})$. Due to $(\dagger)$, it follows that
on input $\bar{s}$, any state $q_{M}^{\prime}$ such that $q_{M}^{\prime}(v)$
occurs in $r_{M}$ can produce some partial tree, i.e., a tree with leafs with
label of the form $\breve{q}_{M}(v.1)$ where $\breve{q}_{M}$ is a state of
$M$. In particular, by our premise, $(q_{1},S,q_{2})(v)$ occurs in $r_{M}$. As
the tree $r_{1}$ is producible by $(q_{1},S,q_{2})$ on input $s^{\prime}$ by
applying the rule
$(q_{1},S,q_{2})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma$, it
follows easily that on input $\bar{s}$, the state $(q_{1},S,q_{2})$ generates
a tree $\hat{r}$ such that $q_{M}(v.1)$ occurs in $\hat{r}$ if $q_{M}(x_{1})$
occurs $\gamma$.

Thus, it follows that $M$ on input $s[v\leftarrow\bar{s}]$ produces a tree in
which $q_{M}(v.1)$ occurs. Clearly, the node $v.1$ is labeled by $l_{1}$ in
$\bar{s}$. Note that $s_{1}\in\text{dom}(l_{1})$. By induction hypotheses,
$[\\![q_{M}]\\!](s_{i})$ is a singleton. ∎

We now prove our main claim.

###### Claim 22

A tree $t_{1}$ exists such that
$[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s^{\prime})\Rightarrow t_{1}$ and and
$[\\![q_{2}]\\!]^{T_{2}}(t_{1})\Rightarrow r_{1}$.

###### Proof of Claim

Let $i\in[k]$ and $q_{M}$ be a state of $M$. Let $q_{M}(x_{i})$ occur in
$\gamma$. By Claim 21, the set $[\\![q_{M}]\\!](s_{i})$ is a singleton. Let
$[\\![q_{M}]\\!](s_{i})=\\{r^{\prime}\\}$. Let
$q_{M}=(q^{\prime}_{1},S^{\prime},q^{\prime}_{2})$ where
$(q_{1}^{\prime},S^{\prime})$ and $q_{2}^{\prime}$ are states of $\hat{T}_{1}$
and $T_{2}$, respectively. Due to Lemma 17, $s_{i}\in\text{dom}(q_{M})$
implies $s_{i}\in\text{dom}((q^{\prime}_{1},S^{\prime}))$, i.e.,
$[\\![(q_{1}^{\prime},S^{\prime})]\\!]^{\hat{T}_{1}}(s_{i})$ is not empty. In
the following, we show that if $[\\![q_{M}]\\!](s_{i})=\\{r^{\prime}\\}$ then
for all trees $t^{\prime}$ contained in
$[\\![(q_{1}^{\prime},S^{\prime})]\\!]^{\hat{T}_{1}}(s_{i})$, it holds that
$[\\![q_{2}^{\prime}]\\!]^{T_{2}}(t^{\prime})=\\{r^{\prime}\\}$ $(*)$.

In the following, consider such a tree $t^{\prime}$. By Lemma 12,

$t^{\prime}\in\bigcap_{\bar{q}_{2}\in S^{\prime}}\text{dom}(\bar{q}_{2})$

and thus $t^{\prime}\in\text{dom}(q^{\prime}_{2})$. Recall that by definition
the state $q_{M}=(q^{\prime}_{1},S^{\prime},q^{\prime}_{2})$ implies
$q_{2}^{\prime}\in S^{\prime}$. Therefore, the set
$[\\![q_{2}^{\prime}]\\!]^{T_{2}}(t^{\prime})$ is not empty. As
$[\\![q_{M}]\\!](s_{i})=\\{r^{\prime}\\}$, we deduce that
$[\\![q_{2}^{\prime}]\\!]^{T_{2}}(t^{\prime})=\\{r^{\prime}\\}$ due to Lemma
15. Therefore, $(*)$ follows.

By definition, the rule
$(q_{1},S,q_{2})(a(x_{1}\\!:l_{1},\dots,x_{k}\\!:l_{k}))\rightarrow\gamma$ of
$M$ is defined only if a rule $(q_{1},S)(a(x_{1},\dots,x_{k}))\rightarrow\xi$
of $\hat{T}_{1}$ and a tree $\psi$ exist such that

  1. 1.

$[\\![q_{2}]\\!]^{T_{2}}(\xi)\Rightarrow\psi$

  2. 2.

the tree $\gamma$ is obtained from $\psi$ by substituting all occurrences of
$q_{2}^{\prime}(u)$ in $\psi$ by
$(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(x_{i})$, where
$(q^{\prime}_{1},S^{\prime})$ and $q_{2}^{\prime}$ are states of $\hat{T}_{1}$
and $T_{2}$, respectively, and $u$ is a leaf of $\xi$ labeled by
$(q^{\prime}_{1},S^{\prime})(x_{i})$

  3. 3.

for $i\in[k]$, it holds that $\xi\langle x_{i}\rangle\subseteq l_{i}$.

By definition of $r_{1}$ (see Equation 2), for $i\in[k]$, it holds that
$s_{i}\in l_{i}$. Therefore, it follows due to Statement 3 that if
$(q_{1}^{\prime},S^{\prime})(x_{i})$ occurs in $\xi$ then
$s_{i}\in\text{dom}((q_{1}^{\prime},S^{\prime}))$. Thus,
$[\\![(q_{1},S)]\\!]^{\hat{T}_{1}}(s^{\prime}))\Rightarrow t_{1}$ where

$t_{1}\in\xi[(q_{1}^{\prime},S^{\prime})(x_{i})\leftarrow[\\![(q_{1}^{\prime},S^{\prime})]\\!]^{\hat{T}_{1}}(s_{i})\mid(q_{1}^{\prime},S^{\prime})\in
Q_{1}^{\prime},i\in[k]]$

and $[\\![q_{2}]\\!]^{T_{2}}(t_{1})\Rightarrow r_{1}^{\prime}$ where

$r_{1}^{\prime}\in\psi[q_{2}^{\prime}(u)\leftarrow[\\![q_{2}^{\prime}]\\!]^{T_{2}}(t_{1}/u)\mid
q_{2}^{\prime}\in Q_{2},u\in V(\xi)].$

Note that the tree $t_{1}/u$ is produced by the state
$(q_{1}^{\prime},S^{\prime})$ on input $s_{i}$ if
$\xi[u]=(q_{1}^{\prime},S^{\prime})(x_{i})$. We remark that the node $g$ is
labeled by $q_{2}(u)$ in $\psi$ where $u$ is a node of $\xi$ such that $u$ is
labeled by a symbol of the form $(q_{1}^{\prime},S^{\prime})(x_{i})$ if and
only if $g$ is labeled by $(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})(x_{i})$
in $\gamma$ due to Statement 2. Due to $(*)$, it follows that

$[\\![(q_{1}^{\prime},S^{\prime},q_{2}^{\prime})]\\!]^{M}(s_{i})=\\{r^{\prime}\\}=[\\![q_{2}^{\prime}]\\!]^{T_{2}}(t_{1}/u).$

Therefore, $(*)$ yields $r_{1}^{\prime}/g=r_{1}/g$. Due to the definition of
$\gamma$ and $\psi$, i.e. Statement 2, our claim follows. ∎

∎