First-order tree-to-tree functions
Mikołaj Bojańczyk and Amina Doumane

We study tree-to-tree transformations that can be defined in   first-order logic or  monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from  prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition.

§ INTRODUCTION

The purpose of this paper is to decompose tree transformations into simple building blocks. An important inspiration  is the Krohn-Rhodes theorem <cit.>, which says that every string-to-string function recognised by a Mealy machine can be decomposed into certain prime functions.

*Regular functions. The transformations studied in this paper are the  regular functions.

In <cit.>, Engelfriet and Hoogeboom proved that deterministic two-way transducers recognise the same string-to-string functions as transductions. Because of this and other properties – such as closure under composition <cit.> and decidable equivalence <cit.> –  this class of functions is now called the regular string-to-string functions. Other  equivalent descriptions of the regular functions include: string transducers of Alur and Černý [2], and several models based on combinators [4, 16, 11].

There are also regular functions for trees, which can be defined using any of the following equivalent models: tree-to-tree transductions <cit.>, single use attributed tree grammars [7], macro tree transducers of linear size increase <cit.>, and streaming tree transducers <cit.>.

The goal of this paper is to prove a decomposition result for regular tree-to-tree functions. As in the Krohn-Rhodes theorem, we want to show that every such function can be obtained by combining certain prime functions.

*First-order transductions.  Although transductions are the more popular model, we work mainly with the less expressive model of first-order transductions. Why?

As we explain in Section <ref>, every tree-to-tree transduction can be decomposed as: (a) first, a relabelling defined in , which does not change the tree structure; followed by (b) a first-order tree-to-tree transduction. In this sense, as far as transformations of the tree structure are concerned,  first-order and transductions have the same expressive power. Another argument for the importance of first-order tree-to-tree transductions is a connection with the $\lambda$-calculus. As we explain in Section <ref>, first-order tree-to-tree transductions are expressive enough to capture evaluation of $\lambda$-terms (assuming linearity, i.e. every variable is used once), and such evaluation turns out to be one of the core computational steps implicit in a tree-to-tree transduction.

Another advantage of first-order logic on trees, compared to , is  a better decomposition theory, in the sense of decomposing formulas into  simpler ones [23, 8, 20].

For our paper, the most useful decomposition is a remarkable theorem of Schlingloff, which says that first-order logic on trees is equivalent to a certain two-way variant  of ctl <cit.>. In contrast, there are no such results for .

Summing up, we believe that first-order  tree transformations are  expressive, have a strong theory, and deserve to leave the shadow of their better known cousin.

*Structured datatypes. We present our main decomposition result in a formalism based on  functional programming (in a combinatory variant, i.e. without variables), with structured datatypes such as pairs or co-pairs.  The motivation behind this approach  – which is inspired by [11] – is to avoid encoding datatypes in our constructions using syntactic annotation such as endmarkers and separators. Thanks to the  structured datatypes,  we can use established operations such as map, and we can assign informative types to our functions, such as $\Sigma_1 \times \Sigma_2 \to \Sigma_i$ for projection, as opposed to saying that all functions input and output trees.

The choice of datatypes for trees is harder than for the string case that was studied in [11].  The difficulty is in splitting the input into smaller pieces. A piece of a string is also a string, but this is no longer true for trees, where the pieces have dangling edges (or variables). As a result, more complicated  datatypes are needed; and our design choices lead us to functions that operate on ranked sets, where each element has an associated arity.

This is a long paper. Given the limited space, we have decided to prioritise  explaining  design choices and intuitions, with  examples and many pictures. As a result, almost all of the proofs are in the appendix.

§ TREES AND TREE-TO-TREE FUNCTIONS

In this section, we describe the trees and tree-to-tree functions that are discussed in this paper.

A ranked set is a set where each element has an associated arity in $\set{0,1,2,\ldots}$. If $a$ of a ranked set has arity $n$, then elements of $\set{1,\ldots,n}$ are called ports of $a$. We adopt the convention that ranked sets are red, e.g. $\rSigma$ or $\rGamma$, and other objects (elements of ranked sets, or unranked sets) are black.  We use ranked sets as building blocks for trees. The following picture describes the notion of trees that we use and some terminology:

We use standard tree terminology, such as ancestor, descendant, child, parent. We write $\trees \rSigma$ for the (unranked) set of trees over a ranked set $\rSigma$. This paper is about tree-to-tree functions, which are functions of the type
\begin{align*}
f : \trees \rSigma \to \trees \rGamma.
\end{align*}

§.§ First-order logic and transductions

To define tree-to-tree functions and tree languages, we use  logic, mainly first-order logic and monadic second-order logic . The  idea is to view a tree as a model, and to use logic to describe properties and transformations of such models.

A vocabulary is defined to be a set of relation names, each one with associated arity.  We do not use function symbols in this paper. A  vocabulary can be formalised as a ranked set, which is why we use red letters like $\ranked \sigma $ or $\ranked \tau$ for  vocabularies.

For a tree $t$  over a ranked alphabet $\rSigma$, its associated model

is defined as follows. The  universe is the nodes of the tree, and it is equipped with the following relations:

x<y &  &   \text{$x$ is an ancestor of $y$} & \text{arity 2}\\
\mathrm{child}_i(x) &  & \text{$x$ is an $i$-th child ($i\in \set{1,2,\ldots}$)} & \text{arity 1} \\
a(x) &  &   \text{$x$ has label $a$ ($a \in \rSigma$)} & \text{arity 1}
\end{array}$$

The $i$-th child predicates are only needed for $i$ up to the maximal arity of letters in the ranked alphabet, and hence the vocabulary in the above definition is finite. We refer to this vocabulary as the vocabulary of trees over $\rSigma$.
A sentence of first-order logic (or  )  over this vocabulary   describes a tree language, namely the set of trees whose associated models satisfy the sentence.  For example, the sentence

\begin{align*}
\forall x \ a(x) \Rightarrow \exists y \ x < y \land b(x)
\end{align*}

is true in (the models associated to)  trees $t$ where every node with label $a$ has a descendant with label $b$. For more background about defining properties of trees using logic, see the survey of Thomas [32].

The regular tree languages are exactly those that can be defined in , which was proved by Doner <cit.>, and also Thatcher and Wright <cit.>. The tree languages definable in first-order logic are a proper subset  of those definable in , and it is an open problem whether or not one can decide if a regular tree language can be defined in first-order logic <cit.>. This is in contrast to the case of words, where the decidable characterisation of  first-order logic by Schützenberger-McNaughton-Papert <cit.> is  a cornerstone of algebraic language theory.

*Tree-to-tree functions.
Apart from defining tree languages, logic can also be used  to define transformations on  models. In the context of this paper, we are interested mainly in first-order transductions, defined below.  Roughly speaking, a first-order transduction uses first-order logic to define a new tree structure on the input tree.

A tree-to-tree function is called a  first-order transduction if it can be obtained  by composing any number of operations[There is a normal form of first-order transductions, where at two phases are used: first  item 1, then item 2. We do not need the normal form, so we do not prove it, but it can be shown similarly to <cit.>. ] of the following two kinds:

* Copying. Let  $k \in \set{1,2,\ldots}$. Define  $k$-copying to be the operation which inputs a tree and outputs a tree where every node is preceded by a chain of $k-1$ unary nodes with a fresh label $\blueball$, as in the following picture:
After $k$-copying, the number of nodes grows $k$ times.

* Non-copying first-order transductions. This is a tree-to-tree function which uses first-order logic to define a new tree structure over the nodes of the input tree. The syntax of such a transduction is given by:

* Input and output alphabets $\rSigma$ and $\rGamma$, which are finite ranked sets. We use the name input vocabulary for the vocabulary of trees over the input alphabet $\rSigma$, likewise we define the output vocabulary.

*  A first-order formula over the input vocabulary, with one free variable, called the universe formula.

*  For each relation of the output vocabulary, of arity $n$, a corresponding first-order formula  over the input vocabulary with $n$ free variables.

The transduction inputs a tree over the input alphabet, and outputs a tree over the output alphabet where:

* the nodes  are those nodes of the input tree that satisfy the universe formula in item <ref>;

* the labels, descendant, and child relations are defined by the formulas in item <ref>.

In order for the transduction to be well defined, the formulas in item <ref> must be such that they produce a tree model for every input tree.

If we allowed  monadic second-order logic in items <ref> and <ref> (the free variables of the formulas would  still be first-order variables ranging over tree nodes), then we would get the tree-to-tree transductions of Bloem and Ensgelfriet <cit.>. We  discuss these in  Section <ref>.

We conclude this section with two examples of first-order tree-to-tree transductions.

Let the input and output alphabets be:

and consider the  function which removes the unary nodes:

This is a non-copying first-order  transduction. The universe formula selects nodes which have non-unary labels. The descendant relation is inherited from the input tree. To define the child relation on the output tree, we  use the descendant relation in the input tree. A node $x$  satisfies the unary  $i$-th child predicate   in the output tree if it satisfies the following first-order formula in the input tree:

\begin{align*}
\exists y \ \child i (y) \land \underbrace{y \le x \land   \forall z\ (y \le z < x \Rightarrow \blueball(z))}_{\substack{\text{$y$ is the farthest ancestor that can be} \\ \text{reached from $x$ using only unary nodes}}}.
\end{align*}

This example shows the usefulness of first-order logic with descendant, as opposed to child only as used in [6].

Define  pre-order on nodes in a tree as follows:  $x$ is before  $y$ if either $x \le y$, or there exist nodes $x'$ and $y'$ such that $x' \le x$, $y' \le y$, and $x'$ is a sibling of $y'$ with a  smaller child number.  Consider  the tree-to-tree function which transforms a tree into a list of its nodes in pre-order traversal, as explained in the following picture:
This function is a first-order tree-to-tree transduction,
because the pre-order is first-order  definable. Unlike Example <ref>, we need copying, because a node of arity $n$ in the input tree corresponds to $n+2$ nodes in the output tree.

§ DERIVABLE FUNCTIONS

In this section, we state the main result of this paper, which says that the  first-order tree-to-tree transductions are exactly those that  can be  obtained by starting with certain prime functions (such as pre-order traversal from Example <ref>) and applying certain  combinators (such as function composition).

The guiding principle behind our approach is to describe tree-to-tree functions without using  any iteration mechanisms, such as states or fold functions. This principle validates the choice of first-order logic. If we were to use , at the very least we would need to have some mechanism for groups, which are a basic building block for Krohn-Rhodes decompositions, or for evaluating Boolean formulas.

§.§ Datatypes

The prime functions and combinators  use  datatypes  such as pairs of trees, or pairs of trees of pairs, etc. Although these datatypes  could be encoded in trees, we avoid this encoding and use explicit datatype constructors.

An important property of our datatypes is that they represent ranked sets, i.e. each element of a datatype has an arity. The datatypes are obtained from the atomic datatypes by applying four datatype constructors, as described below.

*Atomic datatypes. Every finite ranked set is an atomic datatype. Apart from finite ranked sets, we allow one more atomic datatype: the   terminal ranked set  $\termset$ which contains exactly one element of every arity.

The set is called terminal because it admits a unique arity preserving function from every  ranked set.
We use $\termset$ for partial functions: a partial function with output  type  $\rSigma$ can be seen as a total function of output type $\ranked{\rSigma + \termset}$, which uses  $\termset$  for  undefined values.

*Terms. The central datatype constructor is the  term constructor, which is a generalisation of trees to higher arities. A term is a tree with dangling edges, called ports. The dangling edges ares used to decompose trees (and other terms) into smaller pieces, as  illustrated by the figure below.

Formally speaking, terms are defined by induction as follows. As term over a  ranked set $\rSigma$ is either the identity term denoted by  $\portletter$, which consists of a port and nothing else,
or otherwise it is an expression of the  form $a \tensorpair{t_1,\ldots,t_n}$ where $a \in \rSigma$ has arity $n$, and $t_1,\ldots,t_n$ are already defined terms. The arity of a term is the number of ports. Terms of arity zero are the same as trees. We write $\tmonad \rSigma$ for the ranked set of terms over a ranked set $\rSigma$.   Because the term constructor – like other datatype constructors – outputs a ranked set, it makes sense to talk about terms of terms, etc.

Terms are a monad, in the category of ranked sets and arity preserving functions[An almost identical monad is used in  <cit.>, which differs from ours in  that it allows multiple uses of a single port.]. The unit of the monad,  an operation of type $\ranked{\rSigma \to \tmonad \rSigma}$, is illustrated in the following picture:
The product of the monad,  an operation of type $\ranked{\tmonad \tmonad \rSigma \to \tmonad \rSigma}$ that we call flattening, is illustrated in the following picture:
This monad structure will be part of our prime functions.

*Products and coproducts.
There are two binary datatype constructors

\begin{align*}
\underbrace{\ranked{\Sigma_1 \product \Sigma_2}}_{\text{product}} \qquad \underbrace{\ranked{\Sigma_1 + \Sigma_2}}_{\text{coproduct}}.
\end{align*}

An element of the product is a pair $\tensorpair{a_1,a_2}$ where $a_i \in \ranked{\Sigma_i}$. The arity of the pair is the sum of arities of its two coordinates $a_1$ and $a_2$.

An element of the coproduct is a pair $(i,a)$ where $i \in \set{1,2}$ and $a \in \ranked{\Sigma_i}$. The arity is inherited from $a$.

The set of terms can be defined in terms of  products and coproducts, as the least solution of the equation:

\begin{align*}
\tmonad \rSigma = \redset{\portletter}  \ranked{+\coprod_{\black {a \in} \rSigma}}
\powersmall{(\tmonad \rSigma)} {\text{arity of $a$}}
\end{align*}
where $\ranked \coprod$ denotes possibly infinite coproduct  and $\powersmall X n$ denotes the $n$-fold product of a ranked set $\ranked X$ with itself.

The final – and maybe least natural – datatype constructor called folding. Folding has two main purposes: (1) reordering ports in a term; and (2) reducing arities by grouping ports into groups.

Folding is not one constructor, but a family of unary constructors $\reduce k \rSigma$, one  for every $k \in \set{1,2,3,\ldots}$.  An $n$-ary element of $\reduce k \rSigma$, which is called a $k$-fold, consists of an element      $a \in \rSigma$  together with an injective    grouping  function

\begin{align*}
f :  \underbrace{\set{1,\ldots,\text{arity of $a$}}}_{\substack{\text{an element of this set is}\\\text{called a  port of $a$}}} \to \underbrace{\set{1,\ldots,n} \times \set{1,\ldots,k} }_{\text{these pairs are called \emph{sub-ports}}}
\end{align*}

We denote such an element as $a/f$ and draw it like this: 53

Already for $k=1$, the constructor $\reduce 1$ is non-trivial. For example,  $\reduce 1 \tmonad \rSigma$ is a generalisation of terms where ports are not necessarily ordered left-to-right (because the grouping function need not be monotone), and some ports need not appear (because the grouping function need not be total); in other words this is the same as terms in the usual sense of universal algebra, with the restriction that each variable is used at most once (sometimes called linearity).

When viewed as a family of datatype constructors,  folds have a monad-like structure: they are a graded  monad in the sense of <cit.>. The unit is the operation
of type $\ranked{\Sigma \to \reduce 1 \Sigma}$, while  the product (or flattening) in the graded monad is the family of operations of type

\begin{align*}
\ranked{\reduce {k_2} \reduce {k_1} \Sigma \to \reduce {k_1 \cdot k_2} \Sigma},
\end{align*}

indexed by $k_1,k_2 \in \set{1,2,\ldots}$, that is illustrated below:
More formally, the flattening of a double fold $(a/{f_1})/{f_2}$ has the grouping function defined by

\begin{align*}
% \label{eq:fold-grouping}
i \mapsto (i_2, \pi(p_1,p_2)) \qquad \text{where} \begin{cases}
(i_1,p_1) &= f_1(i)\\
(i_2,p_2) &= f_2(i_1)
\end{cases}
\end{align*}

and $\pi$ is the natural bijection between $\set{1,\ldots,k_1} \times \set{1\ldots,k_2}$ and  $\set{1,\ldots,k_1k_2}$.

This completes the list of  datatype constructors.

The datatypes are the least class of ranked sets which contains all finite ranked sets, the terminal set, and which is closed under applying the constructors

\begin{align*}
\ranked{\tmonad \rSigma \qquad \rSigma_1 \product \rSigma_2 \qquad \rSigma_1 + \rSigma_2 \qquad \reduce k \rSigma}.
\end{align*}

* Function composition.

\ranked{f \circ g : \Sigma \to \Delta} \qquad \text{for }\ranked{f : \Sigma \to \Gamma} \text{ and } \ranked{g : \Gamma \to \Delta}

* Lifting of functions along datatype constructors

\combfunc{f_1 + f_2}{\Sigma_1 + \Sigma_2}{\Gamma_1 + \Gamma_2} {\set{f_i : \rSigma_i \to \rGamma_i }_{i =1,2}}\\
\combfunc{\tensorpair{f_1,f_2}}{\Sigma_1 \product \Sigma_2}{\Gamma_1 \product \Gamma_2} {\set{f_i : \rSigma_i \to \rGamma_i }_{i =1,2}}\\
\combfunc{\reduce k f}{\reduce k \Sigma}{\reduce k \Gamma} {f : \rSigma \to \rGamma }\\
\label{eq:liftterm}
\combfunc{\tmonad f}{\tmonad \Sigma}{\tmonad \Gamma} {f : \rSigma \to \rGamma}
\end{array}$$

§.§ Derivable functions

We now present the central definition of this paper.

An  arity preserving function between two datatypes is called derivable  if it can be generated, by using the combinators in Figure <ref>, from  the following prime functions:

* for every $\rSigma$, the unique arity preserving function $\ranked{\Sigma \to \termset}$;

* all arity preserving functions with finite domain;

* the prime functions in Figures <ref>,<ref> and <ref>;

The combinators in Figure <ref> are  function composition, and the obvious liftings of functions along the datatype constructors.
The prime functions in Figure <ref> describe the monad structure of terms and folds, and were explained in Section <ref>. The prime functions in Figure <ref> are  simple syntactic transformations, which are intended to have no computational content.  Figure <ref> contains   less obvious operations, whose definitions are  deferred to Section <ref>.

We are now ready to state the main theorem of this paper.
We say that a tree-to-tree function

\begin{align*}
f : \trees \rSigma \to \trees \rGamma
\end{align*}

is derivable if it agrees on arguments that are trees with some derivable partial function

\begin{align*}
\ranked {f : \tmonad \Sigma \to \tmonad \Gamma + \termset}.
\end{align*}

The main result of this paper is the following theorem.
A tree-to-tree function is a first-order transduction if and only if it is derivable.

The right-to-left implication in the above theorem is proved by a relatively straightforward induction on the derivation. The general idea is that we associate to each datatype a relational structure; for example the relational structure associated to a pair $\tensorpair {a_1,a_2}$ is the disjoint union of the relational structures associated to $a_1$ and $a_2$.  In the appendix, we show that all prime functions are first-order transductions (adapted suitably to structures other than trees); and that this property is preserved under applying the combinators. There is one nontrivial step in the proof, which concerns monotone unfolding, and will be discussed below.

The  left-to-right implication in the theorem, which says that every first-order transduction is derivable, is the main contribution of this paper, and is discussed in Sections <ref>–<ref>.

§.§ The prime functions from Figure <ref>

In this section, we  describe the prime functions from Figure <ref>.
Each of these functions will play a key role in one of the main results of the paper.

§.§.§ Factorisations

We begin with the two factorisation functions

\begin{align*}
\ancfact,\decfact  : \ranked{\tmonad(\Sigma_1+\Sigma_2) \to \tmonad(\tmonad \Sigma_1 + \tmonad \Sigma_2)},
\end{align*}

which are used to cut  terms into smaller parts.
Define a factorisation of a term   to be any term of terms that flattens to it.  An alternative view is that a factorisation is an equivalence relation on nodes in a term, where every equivalence class is connected via the parent-child relation.

Consider a  term $t \in \ranked{\tmonad(\rSigma_1 + \rSigma_2)}$.
We say that two nodes have the same type if both have labels in the same  $\ranked{\Sigma_i}$; otherwise we say that nodes have opposing type. Define  two equivalence relations on  nodes in a term as follows: (a) nodes are called  $\uparrow$-equivalent  if they have the same type and the same proper ancestors of opposing type; (b) nodes are  called  $\downarrow$-equivalent  if they  are $\uparrow$-equivalent and have the same proper descendants of opposing type.
Here is a picture of the equivalence classes, with $\ranked{\Sigma_1}$ being red and $\ranked{\Sigma_2}$ being blue:

For both  equivalence relations, the equivalence classes are connected  under the parent-child relation, and therefore the equivalences can be seen as factorisations. These are the factorisations  produced by the functions $\ancfact$ and $\decfact$.

§.§.§ Pre-order traversal.
The pre-order traversal function

\begin{align*}
\ranked{\preorder : \tmonad \Sigma \to \reduce 1 \tmonad (\rSigma + \redset{\grayball,\grayballbin})}
\end{align*}

is the natural extension – from trees to terms – of the pre-order function in Example <ref>. The fold in the output type is used to reorder the ports in a way which matches the input term, as illustrated in the following picture:

§ REGISTER TREE TRANSDUCERS

We now begin the proof of the harder implication in Theorem <ref>, which says that every first-order tree-to-tree transduction is derivable. Our proof passes  through an automaton model, which  is roughly based on existing transducer models for transductions from [7, 3].
The automaton  uses registers to store parts of the output tree. The semantics of the automaton involves two phases: (a) mapping the input tree to an expression that uses register updates; (b) evaluating the expression. These phases are described in more detail below.

*Register valuations and updates. We begin by explaining how the registers work.  The registers store terms that are used to construct the output tree. Each register has an arity: registers of arity zero  store trees, registers of arity one store unary terms, etc.

Fix two finite ranked sets: the register names $\regnames$ and the output alphabet $\rGamma$.
A register valuation is defined to be any arity preserving function from the register names $\regnames$ to terms $\tmonad \rGamma$.

To transform register valuations, we use register updates.  A register update is an operation which inputs several  register valuations and outputs a single register valuation. For  $n \in \set{0,1,\ldots}$, an $n$-ary register update  is defined to be any arity-preserving function

\begin{align*}
% \ranked {u : \regnames \rto \tmonad ( \rGamma + \underbrace{{\regnames + \cdots + \regnames}}_{\text{$n$ times}})}
\ranked {u : \regnames \rto \tmonad ( \rGamma + n\regnames)},
\end{align*}

where $\ranked{nR}$ stands for the disjoint union of $n$ copies of $\regnames$. The $i$-th copy of $\regnames$ represents the register contents in the $i$-th argument.

Here is a picture of a register update which has arity 3 and uses two registers $r$ and $s$:
An $n$-ary register update $\ranked u$ induces a operation, which inputs  $n$ register valuations and  outputs the  register valuation obtained by  taking $\ranked u$ and replacing the $i$-th copy of a register name with the  contents of that register in the $i$-th input register valuation.
Register updates have arities, and therefore the ranked set of register updates is written in red, and can be used for labels in a tree. For such a  tree

\begin{align*}
t \in  \trees(\ranked{\text{register updates}}),
\end{align*}

define its evaluation to be the register valuation defined by induction in the natural way. Note that register updates of arity zero are the same as register valuations, which gives the induction base.

*First-order relabellings. Our automaton model has no states. Instead, it uses a first-order relabelling, as defined below, to  directly assign to each node of the input tree a register update that will be applied in that node. A similar model is used by    Bloem and Engelfriet <cit.>, except that in their case, the first phase uses  relabellings, and the second phase is   an attribute grammar.

A first-order relabelling is given by two finite ranked sets $\rSigma$ and $\rGamma$, called the input and output alphabets, and a family

\begin{align*}
\set{\varphi_a(x)}_{a \in \rGamma}
\end{align*}

of first-order formulas over the vocabulary of trees over  $\rSigma$. These formulas need to satisfy the following restriction:

(*) for every tree over the input alphabet and node in that tree, there is a unique output letter $a \in \rGamma$ such that $\varphi_a(x)$ selects the node; furthermore, the arity of $a$ is the same as the arity of (the label of) the  node.

The semantics of a  first-order tree relabelling is a function

\begin{align*}
\trees \rSigma \to \trees \rGamma,
\end{align*}

which changes the label of every node in the input tree to the unique letter described in  (*).

A first-order tree relabelling is a very special case of a first-order tree-to-tree transduction, where only the labelling of the input tree is changed, while the universe as well as the child and descendant relations are not affected.

*Register transducers. Having defined registers, register updates, and first-order tree relabellings, we are now ready to define our automaton model.

The syntax of a first-order register transducer consists of:

* An input alphabet $\rSigma$, which is a finite ranked set;

* An output alphabet $\rGamma$, which is a finite ranked set;

* A set $\regnames$ of registers, which is a finite ranked set;

* A total order on the registers.

* A designated output register in $\regnames$, of arity zero.

* A transition function, which is a  first-order  relabelling

\begin{align*}
\trees{\rSigma} \to \trees{\rDelta},
\end{align*}
for some finite set $\rDelta$ of  register updates over registers $\regnames$ and output alphabet $\rGamma$. We require  all register updates in  $\rDelta$ to be single-use and monotone, as defined below:

* Single-use[The  single-use restriction  is a standard feature of transducer models with linear size increase [7, 1, 3].   It prohibits iterated duplication of registers, which would lead to exponential size outputs.
].  An $n$-ary register update $\ranked{u}$ is  called  single-use if   every $r \in \ranked{n \regnames}$
appears in at most one term from $\set{\ranked u(s)}_{s \in \regnames}$, and it appears at most once in that term.

* Monotone[This is notion of monotonicity corresponds to the one used in Section <ref>, see the comments on page page:monotone-discussed. A similar notion  appears in <cit.>.]. This condition uses the total order on registers.  An $n$-ary  register update $\ranked u$ is called monotone  if for every $i \in \set{1,\ldots,n}$, the binary relation $\to_i$ on register names $r,s \in \regnames$  defined by

\begin{align*}
r \to_i s \quad \text{if} \quad  \text{the $i$-th copy of $r$ appears in $\ranked u(s)$},
\end{align*}

which is a partial function from $r$ to $s$ when $\ranked u$ is single-use, is monotone:

\begin{align*}
r_1 \leq r_2 \land r_1 \to_i s_1  \land  r_2 \to_i s_2  \quad \Rightarrow \quad  s_1 \leq s_2
\end{align*}

The semantics of the transducer is  a tree-to-tree function, defined as follows. The input is a tree over the input alphabet. To this tree,  apply the transition function, yielding a tree of register updates. Next, evaluate the tree of register updates, yielding a register valuation. The output tree is defined to be the contents of the designated output register.

The main difference of our model with respect to prior work is that we want to capture  tree transformations defined in first-order logic, as opposed to used in [7, 1, 3]. This is why we use first-order relabellings instead of  relabellings.  For the same reason, we require the register updates to be monotone, see the discussion in Section <ref>.

The main result of this section is that first-order register transducers are expressively complete for first-order tree-to-tree transductions.

Every first-order tree-to-tree transduction is recognised by a first-order  register transducer.

The proof, which is in Appendix <ref>, uses the composition method for logic,  like similar proofs for <cit.> and <cit.>.
The converse  inclusion in the  theorem is also true. This is can be shown directly without much difficulty, following the same lines as in <cit.>. The converse inclusion also follows from   other results in this paper: (a) we show in the following sections that every function computed by the transducer is derivable; and (b)  derivable functions are first-order tree-to-tree transductions by the easy implication in Theorem <ref>.

*Proof strategy for Sections <ref>–<ref>. By Theorem <ref>, to prove derivability of  every first-order tree-to-tree transduction, and thus finish the proof of our main theorem, it suffices to prove derivability for first-order register transducers. In a first-order register transducer,  the computation  has two steps: a first-order relabelling, followed by evaluation of the register updates. The first step is handled in Section <ref>, and the second step is handled in Section <ref>.

§ DERIVABLE FUNCTIONS ARE FIRST-ORDER TRANSDUCTIONS

In this section, we give an overview on the proof of the right-to-left implication in Theorem <ref>, namely that if $\rSigma,\rGamma$ are finite ranked sets, then for every derivable function $\ranked {f : \tmonad \rSigma \to \tmonad \rGamma}$, its restriction to trees $f : \trees \rSigma \to \trees \rGamma$
is a first-order tree-to-tree transduction. The proof is a simple induction on the derivation of  $\ranked f$. In the induction, we must deal with functions that manipulate types that are more complex than trees, e.g. tensor pairs of terms of coproducts.  To operate on such types with first-order transductions, we need to show how such types can be modeled as relational structures. For this purpose, we associate to each type $\rSigma$

* a relational vocabulary denoted  voc$ \rSigma$;

* a map $\underline{\bullet}: a \in \rSigma  \mapsto \underline a \in \text{models over voc$ \rSigma$}$;

which interprets every inhabitant of $\rSigma$ as a relational structure over the vocabulary of $\rSigma$,

both defined in a natural way by induction on types. Their precise definition are given in  Definition <ref>.

The following proposition immediately yields the right-to-left implication in Theorem <ref>. Its proof, which is a straightforward case analysis of all prime functions and combinators, is in the appendix.

If $f : \rSigma \to \rGamma$ is derivable, then there is a first-order transduction $g$
which makes the following diagram commute

\begin{align*}
\xymatrix@C=3cm{
\rSigma \ar[d]_{a \mapsto \underline a}\ar[r]^f &  \rGamma \ar[d]^{a \mapsto \underline a} \\
\text{models over  Voc$\rSigma$} \ar[r]_g &  \text{models over Voc$ \rGamma$}.
\end{align*}

§ FIRST-ORDER  RELABELLINGS

In this section we prove derivability of the first computation step used in first-order register transducers.

Every first-order relabelling is derivable.

To prove the proposition, we use a decomposition of first-order relabellings into simpler functions, in the style of the Krohn-Rhodes theorem.

We use the name unary query for a first-order formula with one free variable over the vocabulary of trees. This assumes some implicit alphabet $\rSigma$.
For a  unary query,  define its  characteristic function,  of type

\begin{align*}
\trees \rSigma \to \trees (\ranked{\rSigma + \rSigma}),
\end{align*}

to be the function which replaces the label of each node by its first or second copy, depending on whether the node is selected by the query. This is a special case of a first-order relabelling. The key to Proposition <ref> is the following  lemma, which decomposes first-order relabellings  into characteristic functions of certain basic unary queries.

Every first-order relabelling can be obtained by composing the following functions:

*  Letter-to-letter homomorphisms. For  every finite $\rGamma,\rSigma$ and $\ranked {f : \rSigma \to \rGamma}$, its tree lifting $\trees \ranked f : \trees \rSigma \to \trees \rGamma$.

*  For every finite  $\rSigma$ and its subsets $\rDelta, \rGamma \subseteq \rSigma$, the characteristic functions of the following unary queries over alphabet $\rSigma$:

*  Child: $x$ is an $i$-th child, for $i \in \set{1,2,\ldots}$

\begin{align*}
\child i (x);
\end{align*}

*  Until:  $x$ has a descendant $y$ with label in $\rDelta$, such that all nodes strictly between $x$ and $y$ have label in $\rGamma$

\begin{align*}
\exists y\ y > x \land \rDelta(y) \land  \forall z \ (x < z < y \Rightarrow \rGamma(z));
\end{align*}

* Since: $x$ has an ancestor $y$ with label in $\rDelta$, such that all nodes strictly between $x$ and $y$ have label in $\rGamma$

\begin{align*}
\exists y\ y < x \land \rDelta(y) \land  \forall z \ (y < z < x \Rightarrow \rGamma(z)).
\end{align*}

The  lemma uses a theorem of   Schlingloff <cit.>, which says  that all first-order definable tree properties can be defined using a temporal logic with operators similar to the ones used in items <ref> of the lemma. Note that the temporal logic is a two-way logic, because  until depends on the descendants of the node $x$, while since depends on the ancestors. In fact, there is no temporal logic which characterises first-order logic, uses only descendants, and has finitely many operators <cit.>.
The exact reduction to Schlingloff's theorem is  in Appendix <ref>.

It remains to show that all of the functions from Lemma <ref> are derivable.
The letter-to-letter homomorphisms from item <ref> are   a special case of homomorphisms discussed in Example <ref>, and hence derivable. In Appendix <ref>, we show that the functions from item <ref> are also derivable. In the proof, a key role is played by the factorisation functions discussed in Section <ref>.

§ MATRIX POWER

In this section, we define the matrix power, which can be seen as a way of representing several trees in one.

For $k \in \set{1,2,\ldots}$ define the $k$-th matrix power[
The name  matrix power is based the matrix power in  universal algebra (for the latter, see [29] or <cit.>). Roughly speaking, the restrictions that we place on the original definition correspond to the single-use and monotone conditions from Definition <ref>.
] of a ranked set $\rSigma$
to be

\begin{align*}
\mati k \rSigma \quad \eqdef \quad \ranked{\reduce k \rSigma^k}.
\end{align*}

Here is a picture of a binary element in the matrix power, where $k=3$:

A matrix power of arity $n$ is used as an abstraction of an $n$-ary register update $\ranked{R\to \tmonad(\Gamma+R+\dots+R)}$. The number $k$ represents the number of registers (that is the size of $\ranked {R}$), and each letter from $\rSigma$ represents a register update (that is, an element of $\ranked{\tmonad(\Gamma+R+\dots+R)}$). When two letters share the same port in the matrix power, this means that the corresponding register updates call the same component of $\ranked{R+\dots+R}$ in their definition, the position in the fold indicates which precise register is called. For instance, the register update above is an abstraction of the following binary register update of registers $r, s$ and $t$:

When we run a STT on an input tree, we decorate it with register updates following the transition function. In order to evaluate this tree, the first thing to do is to determine, for each register update of the root, its "dependency tree" that is to say the register updates they call, inductively. When register updates are abstracted by matrix powers, this operation of determining the dependency tree is what we call unfolding. We illustrate it by the following example

Formally, unfolding is a function of type

\begin{align*}
\ranked{\unfold : \tmonad \mati k \rSigma \to \mati k {(\tmonad \Sigma)} }
\end{align*}

which is defined as follows by induction on the size of the input term. If the input is an empty term, then the output is this term:

Otherwise, if the input is a nonempty term $a(t_1,\ldots,t_n)$ then the output is obtained by first applying unfolding to to the smaller terms $t_1,\ldots,t_n$, and then applying the following derivable function, which we call shallow unfold.

\begin{align*}
\ranked{
\xymatrix{
\shallowterm{\mati k \rSigma} {\mati k \rGamma}  \ar[r] & \mati k {(\shallowterm \Sigma \Gamma)}.
\end{align*}

Here is a picture of unfolding for shallow terms:

More formally, unfolding for shallow terms is defined to be   the composition of the following functions

\begin{align*}
\xymatrix<EMAIL_ADDRESS>\shallowterm{\mati k \rSigma} {\mati k \rGamma} \\{=\shallowterm{\reduce k {\Sigma^k}}{\reduce k {\Gamma^k}}}
\end{array}}  \ar[d]_{{\mathrm{Commutativity}}}\ar[r]^{\mathrm{Shallow\  unfold}} &  {\begin{array}{c}
\ranked{\mati k {(\shallowterm \Sigma \Gamma)}} \\=  \ranked{ \reduce k(\shallowterm{\Sigma}{ {\Gamma}})^k}
\end{array}} \\
\reduce k(\shallowterm{\reduce k {\Sigma^k}}{ {\Gamma^k}})  \ar[r]_{{\mathrm{Matching}}} &  \ranked{ \reduce k(\shallowterm{\Sigma^k}{ {\Gamma}}) } \ar[u]_{\mathrm{Commutativity}}
\end{align*}

Since our prime functions and combinators do not have any general mechanisms for induction, it is not clear how to derive the unfolding operation. In fact, it is not derivable in general, but it will become derivable after imposing a monotonicity requirement. The need for this condition is shown in Example <ref>.  Let us define it in the following.

For a port $i$ in an element of the matrix power $a/f \in \mati k \rSigma$ define its twist to be the partial function from $\set{1,\ldots,k}$ to itself
which is the composition of

\begin{align*}
\xymatrix{
[1,k] \ar[r]^-{j \mapsto {(j,i)}} & [1,k] \times [1,n] \ar[r]^-{f^{-1}} & [1,\arity a] \ar[r] & [1,k]
\end{align*}

where the last function maps each port of the tuple $a$ to the coordinate of the tuple that created that port. Here is a picture:

We say that an element of the $k$-matrix power is monotone if all of its ports have monotone twist. For instance, the right example above is not monotone.
We are now ready to state the principal result of this section.

For every finite ranked set $\rSigma$ and every $k \in \set{1,2,\ldots}$ there is a derivable function

\begin{align*}
\ranked{ f : \tmonad \mati k \Sigma \to \mati k {(\tmonad \Sigma)}}
\end{align*}

which coincides with term unfolding for monotone inputs.

The proof of the  above lemma is one of the main technical contributions of this paper, and it is given in the appendix. One of the ingredients of the proof is a first-order (in fact, derivable) version of the Factorisation Forest Theorem for trees, which is based in Colcombet's splits from [14].

§ EVALUATION OF REGISTER UPDATES

In this section, we deal with the second computation phase in a first-order register transducer, namely evaluating register updates. As  discussed in the end of Section <ref>, this completes the proof of our main theorem.

Our proof uses the language of $\lambda$-calculus.  In Section <ref>,  we discuss derivability of normalisation of $\lambda$-terms. In Section <ref>, we reduce evaluation of register updates to  unfolding the matrix power  and normalisation of $\lambda$-terms.

§.§ Evaluation of register updates

Equipped with Theorem <ref>, we  prove derivability of  evaluation of  register updates.
Fix a first-order register transducer.

From now on, when speaking about register updates or register valuations, we mean those of the fixed transducer.
Our goal is to prove the following lemma, which completes the proof of our main theorem.

the   tree-to-tree function, which inputs a tree of  register updates, evaluates it, and outputs the  contents of the designated output register. This function is derivable.

*Output letters in $\lambda$-terms. We will   use $\lambda$-terms to represent register updates, which involve letters of the output alphabet $\rGamma$. Therefore, for the  rest of Section <ref>, we use an extended notion of $\lambda$-terms, which allows  building $\lambda$-terms of the form

\begin{align}\label{eq:non-pure}
a(M_1,\ldots,M_n) \qquad \text{for every $a \in \rGamma$ of arity $n$.}
\end{align}

The typing rules are extended as follows: if the arguments $M_1,\ldots,M_n$ all have type $\otype$ (no other type is allowed for arguments of $a$),  then (<ref>) has type $\otype$. These $\lambda$-terms can  be represented as trees, as in the following picture:

Theorem <ref> works without change for the extended notion of  $\lambda$-terms used in this section. Note that there is no $\beta$-reduction rule for $\lambda$-terms of the form (<ref>).

*$\lambda$-representations of register updates.

To prove Lemma <ref>, we represent  register updates using a matrix power of $\lambda$-terms. The idea is that the matrix power handles the parallel evaluation of registers.

Let $X$ be a set of variables $\set{x_1\dots,x_m}$, all of them having type $\otype$,  where $m$ is the maximal arity among registers. Define  $\ranked{\Gamma_\lambda}$ to be the output alphabet $\rGamma$ plus the ranked alphabet defined in (<ref>) for tree representations of  $\lambda$-terms.

Recall that a register update – of arity say $n$ – consists of a family of terms  over alphabet $\ranked{\Gamma + n\regnames}$, one for each register $r \in \regnames$. We begin by explaining the $\lambda$-representation for terms in the family, which is a function
of type

\begin{align}\label{eq:placeholders}
\xymatrix@C=2cm{
\ranked{\tmonad(\rGamma+n R)} \ar[r]^-{\text{$\lambda$-representation}} &
\ranked{\tmonad {\Gamma_\lambda}}
\end{align}

This function  is not arity preserving, which is why it is not written in red. Define a  placeholder to be an element of $\ranked{n \regnames}$; we write placeholders as $r_i$ with $r \in \regnames$ and  $i \in \set{1,\ldots,n}$.
The function (<ref>)  is  explained in the following picture:
Note how the
arities need not be preserved: the arity of the output is the number of placeholders in the input, which need not be the same as the number of ports in the input. The correspondence of ports in the output term with placeholders in the input term is defined with respect to some arbitrary order on the set $\ranked{n \regnames}$ of placeholders, say lexicographic with respect to the order on registers and  $\set{1,\ldots,n}$.

Having defined the $\lambda$-representation of terms with placeholders, we lift it a $\lambda$-representation of  register updates

\begin{align}\label{eq:lambda-representation-regup}
\ranked{
\xymatrix@C=2cm{
\text{register updates}    \ar[r]^-{\text{$\lambda$-representation}} &
\mati k {(\tmonad\Gamma_\lambda)}
\end{align}

where $k$ is the number of registers. This function is arity preserving.

For a register update $(t_1,\ldots,t_k)$, where $t_i$ is the term with placeholders used in the $i$-th register,  its $\lambda$-representation is defined to be

\begin{align*}
(\text{$\lambda$-representation of $t_1$},\ldots,\text{$\lambda$-representation of $t_k$})/f ,
\end{align*}

where the grouping function $f$ connects a placeholder $r_i$ to the $r$-th sub-port of port $i$.
Here is a picture

The following  three properties of the $\lambda$-representation for register updates will be used later in the proof:

(P1)  If we restrict the domain to a finite set of register updates, e.g. those used in the transducer, then it is a prime function, by virtue of having finite domain.

(P2) A register update is monotone  (as in Definition <ref>)  if and only if its $\lambda$-representation is monotone (as defined in    Section <ref> for the matrix power).

(P3) Every bound variable in the $\lambda$-representation is used exactly once, and the types that appear are of the form

\begin{align*}
\overbrace{\otype \to \otype \to \cdots \to \otype \to \otype}^{\text{at most (maximal arity in $\rGamma$) times}} \to \otype,
\end{align*}

hence Theorem <ref> can be applied.

*Putting it all together. To finish the proof of Lemma <ref>, we   observe  that the semantics of a register automaton are translated – under the $\lambda$-representation – to unfolding the matrix power and normalising a $\lambda$-term.  This observation is formalised by saying that the diagram in Figure <ref> commutes, and it  follows directly from the definitions. Instead of giving a proof, we illustrate it on an example in Figure <ref>.

\begin{align*}
\xymatrix@C=3cm{
\trees \ranked{\text{(register updates)}}
\ar[dd]_{\substack{\text{evaluate}\\\text{register}\\\text{updates}}}^{\text{(a)}}
\ar[r]^-{\trees(\text{\ranked{$\lambda$-representation}})}_{\text{(c)}}
\trees \ranked{(\mati k{(\tmonad \Gamma_\lambda)})}
\ar[d]^{\substack{\text{unfold}\\\text{matrix}\\\text{power}}}_{\text{(d)}} \\
\txt{{\tiny arity 0 elements of }\\
\mati k {\ranked{(\tmonad \Gamma_\lambda)}}
\ar[d]^{\substack{\text{normalise}\\\text{$\lambda$-terms}}}_{\text{(e)}}\\
\text{register valuations}
\ar[r]_-{\ranked{\text{$\lambda$-representation}}}^{\text{(b)}}
\txt{{\tiny arity 0 elements of }\\
\mati k {\ranked{(\tmonad \Gamma_\lambda)}}
\end{align*}

Example for Figure <ref>.

We claim that all of the arrows (c), (d) and (e) on the  right-down path  in  Figure <ref>  are derivable:

(c) Since we work with a fixed register transducer, there is a finite subset $\rDelta$ of register updates  used, and therefore  operation (a) in the figure is derivable by property (P1).

(d) Arrow (d) represents the unfolding of the matrix power. By property (P2), the outputs of arrow (c) are monotone, and so we can use the monotone unfolding operation, which is a  prime function and therefore derivable.

(e) Finally, arrow (e) represents normalisation of $\lambda$-terms. This arrow is derivable by Theorem <ref>. The assumptions of this theorem are met by property (P3).

Since the arrows (c), (d), (e) are derivable, and the diagram commutes, it follows that  the composition of the arrows (a) and (b) is derivable. In other words, there is a derivable function which maps a tree of register updates to the $\lambda$-representation of the resulting register valuation (when viewing a register valuation as a special case of a register update of arity zero). Finally, to get the contents of the output register, we get rid of the fold in the matrix power by using the last function from Figure <ref>, and  project onto the coordinate for the output register.

This completes the proof of Lemma <ref>, and therefore also of the main theorem.

In this section, we present an overview of the top-down implication in the  proof of Theorem <ref>, which says that every first-order tree-to-tree transduction is (the restriction to trees of) a derivable function. The proof has five steps, which are spread across Sections <ref>–<ref>, and summarised below.

*Section <ref>: first-order tree relabellings. We begin the proof of the left-to-right  implication  with a special case of first-order tree-to-tree transductions, which we call first-order  tree relabellings. In such a  function, every node of the input tree  is given a new label, depending on first-order definable properties of the node. An example is:  “if a leaf $x$ in the input tree has at least one ancestor with label $a$, then replace the label of $x$ with the letter $c$”. First-order tree relabellings  do not cover all first-order transductions, because they do not change the shape of the input tree, but they are an important subcase.
The main result of Section <ref> is:
Proposition <ref>
Every first-order tree relabelling is derivable.
The main tool used in the proof of Proposition <ref> is a theorem of Schlingloff <cit.>, which can be seen as tree version of Kamp's theorem about ltl being  expressively complete for first-order logic.

*Section <ref>: register transducers. To prove that  first-order tree-to-tree transductions are derivable, it will be more convenient to use an automaton model. In Section <ref>, we present  this  automaton model, which we call register transducers[These are the only kind of register transducer used in this paper. A more complete name would be first-order tree-to-tree register transducers.]. This  is a bottom-up tree automaton, which uses registers to store parts of the output tree. The model is based on streaming tree transducers from [3], but it is  appropriately restricted so that it matches first-order logic, as opposed to monadic second-order logic which was used in [3]. The main result of Section <ref> is:
Theorem <ref>
Every first-order  tree-to-tree transduction can be computed by a  register transducer.
The proof of the above theorem, like for similar results in [3] or <cit.>, is based on the composition method in logic.
The converse implication is also true, and follows from Proposition <ref> and the bottom-up implication in Theorem <ref>.

*Section <ref>: register transducers with one register. By Theorem <ref>, in order to prove the left-to-right implication in Theorem <ref>, it is enough to show that register transducers can only compute  derivable  functions. As a first step, we consider register transducers with only one register. When there is only one register, the computed function turns out to be a composition of a first-order tree relabelling, as treated  Proposition <ref>, followed by the evaluation (i.e. computation of the $\beta$-normal form) of    a simply typed $\lambda$-term which is affine (i.e. uses each variable at most once). The main result of Section <ref> is that evaluation of  affine $\lambda$-terms is  derivable, as stated in the following theorem:
Theorem <ref>
The following function is derivable

\begin{align*}
\text{affine $\lambda$-term} \qquad \mapsto \qquad \text{its $\beta$-normal form,}
\end{align*}

if we restrict inputs so that they use  a fixed number of variables, and all subterms have types from a fixed finite set of simple types.

*Section <ref>: deriving a register transducer.  In Section <ref>, we complete the proof of Theorem <ref>:
Proposition <ref>
Every function computed by a register transducer is derivable.
The above result, together with Theorem <ref>, completes the proof of the left-to-right implication in Theorem <ref>. The proof of Proposition <ref> is the observation that register automata with many registers can be reduced to register automata with one register, using the unfolding operation. For register transducers with one register only, the only computation that is done is iterated substitution, which is derivable thanks to Theorem <ref>.

§ FUNCTIONS COMPUTED BY REGISTER TRANSDUCERS ARE DERIVABLE

We now  have all of the ingredients needed to derive functions computed by register transducers, as stated in the following proposition.

For every first-order  tree transducer, the computed function is derivable.

The above proposition  completes the proof of the left-to-right implication in Theorem <ref>: we have seen, by Proposition <ref>, that first-order tree-to-tree transductions can be computed by first-order tree transducers, and Proposition <ref> shows that the later are derivable, which concludes the proof.

The rest of this section is devoted to proving Proposition <ref>. There will be four main ingredients, namely derivability for: first-order tree relabelings (Proposition <ref>), normalisation of affine $\lambda$-terms (Theorem <ref>), and unfolding of the matrix power (Proposition <ref>).

To put these ingredients together,  we use  terminology inspired by universal algebra, as given in the following definition.

An algebra $\alg$ consists of two sets

\begin{align*}
\overbrace{\algdom \alg}^{\text{unranked}} \qquad \overbrace{\algops \alg}^{\text{ranked}},
\end{align*}

equipped with a  shallow product[
A more standard approach would be to use a family of operations indexed by the signature

\begin{align*}
\set{f^\alg : (\algdom \alg)^{\arity f} \to \algdom \alg}_{f \in \algops \alg}.
\end{align*}

Our approach is equivalent, i.e. defining a shallow product is the same as defining a family of operations.
], which is function of type

\begin{align*}
\shallowterm {(\algops \alg)}{\underbrace{(\algdom \alg)}_{\substack{\text{viewed as a ranked}\\ \text{set, with all elements}\\ \text{having arity zero}}}} \rto \redpar {\algdom \alg}.
\end{align*}

For an algebra $\alg$, define its product to be the function of type

\begin{align*}
\treepar {\algops \alg} \to \algdom \alg
\end{align*}

defined in the natural way.

One example of an algebra is when the signature is some ranked set $\rSigma$, the domain is  $\trees \rSigma$, and the interpretation is defined in the natural way. In this case, the product operation is the identity. A variant of this algebra is when the signature is replaced by $\tmonad \rSigma$; in this case the product operation becomes flattening.

Let us begin the proof of Proposition <ref>.
Fix a register transducer with $k$ registers. For the rest of this section, when talking about register valuations and register updates, we mean the registers of the fixed register transducer.
Another example of an algebra was implicit in the definition of register transducers: the domain is the register valuations and the signature is the  register updates. To prove  Proposition <ref>, we will show that the algebra of register updates embeds – via the matrix power – in an algebra, call it $\alg$, whose product operation is derivable as a special case of normalisation of affine $\lambda$-terms.
The idea behind the algebra  $\alg$ is to use  $\lambda$-terms to represent register contents, according to the following picture:

Let  $\nmax$  be the maximal arity of registers in the fixed register transducer, and let  $\rGamma$ be its  output alphabet. For a term $t \in \tmonad \rGamma$ of arity at most $\nmax$, its representation as a  $\lambda$-term, which we denote by $t^\lambda$,  uses variables from the following finite set (we use the notation $\otype^i \to \otype$ defined in Example <ref>):

\begin{align*}
X  \quad \eqdef \quad \set{\typevar {x_a} {\otype^i \to \otype} : a \in \rGamma \text{ of arity $i$}} \cup \set{\typevar {x_i} \otype : i \in \set{1,2,\ldots,\nmax }}.
\end{align*}

Furthermore, $t^\lambda$ is affine and it can be typed using simple types  from  the following set finite set :

\begin{align*}
\Tt \quad \eqdef \quad \set{\otype^i \to \otype : i \in \set{0,\ldots,\nmax}}
\end{align*}

This means that if $t$ has arity at most $\nmax$ – which is true for any term that can appear in a register of our fixed register transducer – then its $\lambda$-term representation $t^\lambda$ satisfies constraints as in Theorem <ref>.  On its own, $t^\lambda$ is already in normal form, so there is no need to normalise it, but we intend to compose  such $\lambda$-terms, leading to terms that are not in normal form (but which still use variables from $X$ and types from $\Tt$).
This motivates the  following definition of an algebra, call it $\alg$. Its domain and signature are given by

\begin{align*}
\overbrace{\set \bot + \trees \lamrank X}^{\algdom \alg}  \qquad \overbrace{ \tmonad \lamrank X}^{\algops \alg}
\end{align*}

\begin{align*}
\text{where }\lamrank X = {\overbrace{\set{x : x \in X}}^{\text{arity 0}} \cup \overbrace{\set{\lambda x : x \in X}}^{\text{arity 1}} \cup  \overbrace{\set @}^{\text{arity 2}}}
\end{align*}

In other words, the domain is $\lambda$-terms plus an error element, and the signature is $\lambda$-terms  with ports. The   product operation is

\begin{align*}
t^\alg(t_1,\ldots,t_n) = \begin{cases}
\text{normal form of $t(t_1,\ldots,t_n)$} & \text{if $t(t_1,\ldots,t_n)$ is affine and can be typed using $\Tt$}\\
\bot & \text{otherwise}
\end{cases}
\end{align*}

In particular, if one of the inputs $t_1,\ldots,t_n$ is $\bot$, then the output is also $\bot$.  The algebra $\alg$ is designed so that we can apply Theorem <ref> about normalising $\lambda$-terms to see that the  product operation in the  algebra $\alg$ is derivable. Next, by observing that the matrix power is a form of syntactic sugar for manipulating registers in a register automaton, we see that there is an arity preserving

\begin{align*}
\ranked h : \regups \to \mati k {(\algops \alg)}
\end{align*}

which has only monotone elements in its image, and which makes the following diagram commute

\begin{align*}
\xymatrix@C=2cm{
\treepar {\regups} \ar[r]^-{\trees \ranked h}\ar[d]_{\text{product}} &
\treepar {\mati k {(\algops \alg)}}\ar[r]^{\text{Corollary~\ref{cor:matrix-power}}}  &
\treepar {\algops \alg} \ar[d]^{\text{product}} \\
\regvalss \ar[rr]_{(t_1,\ldots,t_k) \mapsto t^\lambda_1}&  & \algdom {\alg^{[k]}}
\end{align*}

Putting this all together, we see that there is a derivable function which inputs a tree of register updates, and outputs the value of the first register, represented as a $\lambda$-term. The last remaining observation is that function $t^\lambda \mapsto t$, i.e. the inverse of the $\lambda$-term representation, is derivable. This inverse can be achieved, for example, by composing a first-order tree relabelling with a tree homomorphism. This completes the proof of Proposition <ref>, and therefore also of Theorem <ref>.

§ MONADIC SECOND-ORDER TRANSDUCTIONS

We finish the paper by discussing a variant of our main theorem for   tree-to-tree transductions.
We simply add, as prime functions, all relabellings, which are defined the  same way as the first-order relabellings from Definition <ref>, except that the unary queries can use logic instead of first-order logic.

A tree-to-tree function is an transduction if and only if it can be derived  using  Definition <ref>  extended by  adding  all relabellings as prime functions.

In <cit.>, Colcombet shows that every formula on trees can be replaced by a first-order formula that runs on an relabelling of the input tree. Applying that result to transductions, we see that every tree-to-tree transduction can be decomposed as: (a) an relabelling; followed by (b) a first-order tree-to-tree transduction.  The theorem follows.

The solution above is not particularly subtle, and contrasts our results for  first-order logic and chain logic, where  we took care to have a small number of primitives. This  was possible thanks in part to the decomposition of first-order queries into simpler ones that was is in Section <ref>, and the Krohn-Rhodes theorem that is used in the proof of Theorem <ref> about chain logic.  In principle,  a decomposition of relabellings could be possible, but proving it  would likely require developing a new decomposition  theory for regular tree languages, in the style of the Krohn-Rhodes theorem, which we feel is beyond the scope of this paper. One would expect a Krohn-Rhodes theorem  for trees to yield an effective characterisation of first-order logic – as it does for words – but finding such a characterisation remains a major open problem <cit.>.

The final  prime function is called monotone unfolding. The general idea is that unfolding unpacks a representation of several trees inside a single tree.  Before describing this function in more detail,  we introduce some notation,  inspired by the matrix power in  universal algebra <cit.>.
For $k \in \set{1,2,\ldots}$ define the $k$-th matrix power of a ranked set $\rSigma$, denoted by $\mati k \rSigma$, to be the ranked set $\reduce k \powersmall \rSigma k$.

Here is a picture of elements in the third matrix power:

Unfolding the matrix power

An element of the $k$-th matrix power  can be seen as having a group of $k$ incoming edges, and each of its ports  can be seen as a group of $k$ outgoing edges. The general unfolding operation, which has type

\begin{align*}
\ranked{\tmonad \mati k{\Sigma} \to \mati k{( \tmonad \Sigma)}},
\end{align*}

matches the $k$ incoming edges in a node with the $k$ outgoing edges in the parent port; it also removes the unreachable nodes. This operation is illustrated in Figure <ref>, and  a formal definition  is  in the appendix.

*Chain logic.
The general unfolding operation is too powerful  to be included in the derivable functions, as we explain below. It does, however, admit a characterisation in terms of a fragment of called chain logic,  see <cit.> or <cit.>, whose expressive power is strictly between first-order logic and . Chain logic is defined to be the fragment of  where set quantification is restricted to sets  where all nodes are comparable by  the descendant relation.

The following conditions are equivalent for tree-to-tree functions:

* is derivable, as in Definition <ref>, except that general unfold is used instead of monotone unfold;

* is a transduction,  as in  Definition <ref>,  except that chain logic is used instead of first-order logic.

To see why chain logic is needed to describe general unfolding, consider the following unfolding, where two coordinates are swapped in each node of the input tree:
For inputs with an odd number of swaps, the output of unfolding has a white leaf in the first coordinate, and for inputs with an even number of swaps, the output has a white leaf in the first coordinate.  Checking if a path has even length can be done in chain logic, but not in  first-order logic.

*Monotone unfolding
To avoid the problems with cyclic swaps, the unfolding function in Figure <ref> imposes a monotonicity requirement on the matrix power, described below.

Let  $a \in \mati k \rSigma$ be an element of the matrix power,  let $p,q \in \set{1,\ldots,k}$, and let  $i$ be a port of $a$. Define the twist function of port $i$, denoted by $\to_i$, as follows:
$q \to_i p$
if coordinate $q$ in the $i$-th outgoing edge  is connected to  coordinate $p$ in root, as described in the following picture:
The twist function is partial. Call  an element of the matrix power  monotone if for every port, its twist functions is monotone (when restricted to inputs where it is defined). In the picture above, $\to_1$ is monotone, while $\to_2$ is not. Also, the problems with an even number of swaps discussed earlier arise from  a non-monotone twist function:
The monotone unfolding operation in Figure <ref> defined to be the restriction of general unfolding,  which  is undefined if the input contains at least one label which is non-monotone, and otherwise returns the output of the general unfolding.

*Is unfolding derivable? The  prime functions in our main theorem  are meant to be simple syntactic rewritings. It is debatable whether the  unfolding operation – even in its monotone variant – is of this kind. For example, our proof  that monotone unfolding is a first-order transduction requires an invocation of the Schützenberger-McNaughton-Papert theorem about first-order logic on words being the same as counter-free automata.

Is it possible to break down monotone unfolding into simpler primitives?
In the appendix, we devote considerable resources to answering this question. We propose one new  datatype

and seventeen additional prime functions, which can be called syntactic rewriting without straining the reader's patience. Then, we show that monotone unfolding can be derived using   the new datatype and functions. The proof of this result is one of the main technical contributions of this paper.

[1]
Rajeev Alur.
Streaming String Transducers.
In Workshop on Logic, Language, Information and
Computation, WoLLIC 2011, Philadelphia, USA, volume 6642 of
Lecture Notes in Computer Science, page 1. Springer, 2011.

[2]
Rajeev Alur and Pavol Černý.
Expressiveness of streaming string transducers.
In Foundations of Software Technology and Theoretical
Computer Science, FSTTCS 2010, Chennai, India, volume 8 of
LIPIcs, pages 1–12. Schloss Dagstuhl - Leibniz-Zentrum fuer
Informatik, 2010.

[3]
Rajeev Alur and Loris D'Antoni.
Streaming tree transducers.
Journal of the ACM (JACM), 64(5):31, 2017.

[4]
Rajeev Alur, Adam Freilich, and Mukund Raghothaman.
Regular combinators for string transformations.
In Computer Science Logic and Logic in Computer Science,
CSL-LICS 2014, Vienna, Austria,, pages 1–10. ACM, 2014.

[5]
Augustin Baziramwabo, Pierre McKenzie, and Denis Thérien.
Modular temporal logic.
In Logic in Computer Science LICS, Trento, Italy, pages
344–351. IEEE, 1999.

[6]
Michael Benedikt and Luc Segoufin.
Regular tree languages definable in FO and in
ACM Trans. Comput. Log., 11(1):4:1–4:32, 2009.

[7]
Roderick Bloem and Joost Engelfriet.
A Comparison of Tree Transductions Defined by Monadic
Second Order Logic and by Attribute Grammars.
Journal of Computer and System Sciences, 61(1):1–50, August

[8]
Mikołaj Bojańczyk.
Decidable Properties of Tree Languages.
PhD Thesis, University of Warsaw, 2004.

[9]
Mikołaj Bojańczyk.
Some open problems in automata and logic.
ACM SIGLOG News, 2(4):3–15, 2014.

[10]
Mikołaj Bojańczyk.
Recognisable languages over monads.
CoRR, abs/1502.04898, 2015.

[11]
Mikołaj Bojańczyk, Laure Daviaud, and Shankara Narayanan Krishna.
Regular and First-Order List Functions.
In Logic in Computer Science, LICS 2018, Oxford,
UK,, pages 125–134. ACM, 2018.

[12]
Mikołaj Bojańczyk, Howard Straubing, and Igor Walukiewicz.
Wreath Products of Forest Algebras, with Applications to
Tree Logics.
Logical Methods in Computer Science, 8(3), 2012.

[13]
Michal Chytil and Vojtech Jákl.
Serial Composition of 2-Way Finite-State Transducers and
Simple Programs on Strings.
In International Colloquium on Automata, Languages and
Programming, ICALP, Turku, Finland, volume 52 of Lecture
Notes in Computer Science, pages 135–147. Springer, 1977.

[14]
Thomas Colcombet.
A Combinatorial Theorem for Trees.
In International Colloquium on Automata, Languages and
Programming, ICALP, Wrocław, Poland, Lecture Notes in
Computer Science, pages 901–912. Springer, 2007.

[15]
Bruno Courcelle.
The monadic second-order logic of graphs v: on closing the gap
between definability and recognizability.
Theoretical Computer Science, 80(2):153 – 202, 1991.

[16]
Vrunda Dave, Paul Gastin, and Shankara Narayanan Krishna.
Regular transducer expressions for regular transformations.
In Logic in Computer Science, LICS 2018, Oxford,
UK,, pages 315–324, 2018.

[17]
John Doner.
Tree acceptors and some of their applications.
J. Comput. System Sci., 4:406–451, 1970.

[18]
J. Engelfriet and S. Maneth.
Macro Tree Translations of Linear Size Increase are MSO
SIAM Journal on Computing, 32(4):950–1006, January 2003.

[19]
Joost Engelfriet and Hendrik Jan Hoogeboom.
MSO Definable String Transductions and Two-way
Finite-state Transducers.
ACM Trans. Comput. Logic, 2(2):216–254, April 2001.

[20]
Z. Ésik and P. Weil.
On logically defined recognizable tree languages.
In FSTTCS, volume 2914 of LNCS, pages 195–207, 2003.

[21]
Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès.
Towards a formal theory of graded monads.
In Foundations of Software Science and Computation
Structures, FoSSaCS, Eindhoven, the Netherlands, Lecture
Notes in Computer Science, pages 513–530. Springer, 2016.

[22]
Eitan M. Gurari.
The Equivalence Problem for Deterministic Two-Way
Sequential Transducers is Decidable.
SIAM J. Comput., 11(3):448–452, 1982.

[23]
Thilo Hafer and Wolfgang Thomas.
Computation tree logic CTL* and path quantifiers in the monadic
theory of the binary tree.
In International Colloquium on Automata, Languages and
Programming, ICALP, Turku, Finland, pages 269–279. Springer,

[24]
Kenneth Krohn and John Rhodes.
Algebraic theory of machines. i. prime decomposition theorem for
finite semigroups and machines.
Transactions of the American Mathematical Society,
116:450–450, 1965.

[25]
Robert McNaughton and Seymour Papert.
Counter-free automata.
The M.I.T. Press, Cambridge, Mass.-London, 1971.

[26]
Bernd-Holger Schlingloff.
Expressive completeness of temporal logic of trees.
Journal of Applied Non-Classical Logics, 2(2):157–180, 1992.

[27]
Morten Heine Sorensen and Pawel Urzyczyn.
Lectures on the Curry-Howard Isomorphism.
Elsevier, July 2006.

[28]
Howard Straubing.
Finite Automata, Formal Logic, and Circuit Complexity.
Birkhauser. 1994.

[29]
Walter Taylor.
The fine spectrum of a variety.
Algebra Universalis, 5(1):263–303, 1975.

[30]
J. W. Thatcher and J. B. Wright.
Generalized finite automata theory with an application to a decision
problem of second-order logic.
Mathematical systems theory, 2(1):57–81, March 1968.

[31]
Wolfgang Thomas.
Infinite trees and automaton- definable relations over
Theoretical Computer Science, 103(1):143 – 159, 1992.

[32]
Wolfgang Thomas.
Languages, automata, and logic.
In Handbook of formal languages, pages 389–455. Springer,

§ UNFOLDING THE MATRIX POWER

In this part of the appendix, we define formally the unfolding function

\begin{align*}
\ranked{\tmonad \mati k{\Sigma} \to \mati k{( \tmonad \Sigma)}}
\end{align*}

that was described in Section <ref>. We  present the definition in a slightly verbose manner,  by  decomposing unfolding into simpler operations. The  presentation highlights the inductive character of unfolding, and the reasons why we are uneasy about it being a prime operation.

§.§ Shallow terms

We begin by defining unfolding  for terms of depth two, called shallow terms. Later, we extend the definition to all other terms by induction.
We describe shallow terms as a separate datatype, since this datatype will also be used later, in Section <ref>, to derive the (monotone) unfolding operation.
For now, shallow terms are just an intermediate type used to define formally the unfolding function.

Let $\rSigma$ and $\rGamma$ be two ranked sets. The  shallow terms datatype, which is  denoted $\shallowterm \rSigma \rGamma$, consists of  expressions of the form $a\tensorpair{b_1,\dots,b_n}$ where $a$ is an $n$-ary element of $\rSigma$ and $b_1,\dots, b_n$ are elements of $\rGamma$. The arity of such an expression is the sum of arities of $b_1,\ldots,b_n$. We draw shallow terms as terms of depth two, where the root is from $\rSigma$ and  the children are from $\rGamma$:
An equivalent definition of shallow terms, in terms of products and co-products, is

\begin{align}\label{eq:shallowterm-definition}
\shallowterm \rSigma \rGamma \quad \eqdef   \quad \ranked{\coprod_{\black{a \in} \rSigma} } \overbrace{\ranked{\Gamma \product \cdots \product \Gamma},}^{\text{arity of $a$ times}}
\end{align}

§.§ Terms as an inductive datatype

Using shallow terms, we can define the set of terms as the least solution of the equation

\begin{align*}
\ranked{\tmonad \rSigma = \set{\portletter} + \shallowterm \Sigma {(\tmonad \rSigma)}}.
\end{align*}

With this inductive definition, in order to define an operation of type $\ranked{ \tmonad \rSigma \to \Gamma}$
on terms, it is enough to explain the induction base for the  identity term and the induction step for shallow unfolding, as captured by two operations of types

\begin{align*}
\underbrace{\ranked{\set \portletter \to \Gamma}}_{\text{induction base}}
\qquad
\underbrace{\ranked{\shallowterm \Sigma \Gamma \to \Gamma}.}_{\text{induction step}}
\end{align*}

We use such an induction below to define general unfolding.  The crucial step is defining the induction step, which the unfolding for shallow terms defined in Section <ref> below.

As mentioned at the beginning of Section <ref>, the guiding principle behind our approach is to avoid iteration mechanisms. The inductive definition of general unfolding could be seen as such an iteration mechanism; this is the reason for Section <ref>, where (monotone) unfolding is derived using simpler operations.  In contrast, we believe that iteration is indeed avoided by  the operations used in the induction step that are presented in Section <ref> below.

We do not formalise what we mean by  “avoiding iteration”. One possible direction would be to say that an operation “avoids iteration” if it can be computed by a family of bounded depth circuits, as in the circuit class AC$^0$. A further requirement could be that the family of circuits not only exists, but it is also easy to see.

§.§ Unfolding for shallow terms

The induction step in general unfolding is the operation

\begin{align*}
\ranked{
\xymatrix{
\shallowterm{\mati k \rSigma} {\mati k \rGamma}  \ar[r] & \mati k {(\shallowterm \Sigma \Gamma)},
\end{align*}

which we call shallow unfolding, and
which is explained in the following picture:
To define this operation formally, we further decompose it using  three functions manipulating shallow terms. These functions, which are used here as  intermediate functions in the definition of shallow unfolding, will become prime functions when we decompose the unfolding function in Appendix <ref>.

§.§.§ Distribute shallow terms over fold

Let $\rGamma$ and $\rSigma$ be two datatypes.  Consider the function $\ranked{f_1}$

\begin{align*}
\ranked{\shallowterm  \Gamma {\reduce k \Sigma}} \ranked{\xrightarrow{\quad f_1 \quad}} \ranked{\reduce k(\shallowterm  \Gamma  \Sigma)}
\end{align*}

which distributes shallow terms over folding. This function is illustrated by the following picture
and  defined by

a(b_1/g_1,\dots,b_n/g_n)&\mapsto& a(b_1,\dots,b_n)/g
\end{array}$$

where $g$ is the function defined as follows. For every  $i \in\set{1,\dots,n}$,  if  $j\in\set{1,\dots,\arity{b_i}}$ then

\begin{align*}
\xymatrix@C=5cm{
\begin{array}{c}
\overbrace{j+\underset{l<i}{\Sigma} \arity{b_l}}^{\text{Position of the $j$-th port of $b_i$ is shifted}}
\end{array}
\ar@{|->}[d]^{g}\\
\begin{array}{c}
\biggl(\ \ \ \underbrace{\pi_2(g_i(j))+\underset{l<i}{\Sigma} \arity{b_l/g_l}}_{\text{Position of the group is shifted}}\ \ , \underbrace{\pi_1(g_i(j))}_{\begin{array}{c}
{ \scriptsize\text{Position inside}}\\[-5pt]{\scriptsize \text{the group is unchaged}}
\end{array}}\biggr)
\end{array}}
\end{align*}

§.§.§ Matching function

We now define a function

\begin{align*}
\ranked{\shallowterm  {(\reduce k \Gamma)} {(\Sigma^k)} \xrightarrow{\quad f_2\quad} \reduce 1 (\shallowterm  \Gamma  \Sigma)}
\end{align*}

which matches the $k$-th fold with the $k$-th power[In order to reduce the number of parentheses, in  the rest of the paper we assume a notational convention where the unary datatype constructors – like folding, terms or powering – have priority over the binary shallow term constructor. Under this convention, the operation $\ranked{f_2}$ is written as

\begin{align*}
\ranked{\shallowterm  {\reduce k \Gamma} {\Sigma^k} \xrightarrow{\quad f_2\quad} \reduce 1 (\shallowterm  \Gamma  \Sigma)}
\end{align*}
The function $\ranked{f_2}$ is illustrated by the following  picture

and  defined by

\begin{eqnarray*}
\xymatrix{
(a/g)((b_{1,1},\dots,b_{1,k}),\dots, (b_{n,1},\dots,b_{n,k}))
% \in  \ranked{\shallowterm  {\reduce k \Gamma} {\Sigma^k}  }
\ar@{|->}[d]^{\ranked{f_2}} \\
\end{eqnarray*}

where $m$ is the arity of $a$ and the grouping function  $g'$ is  the natural embedding of ports

\begin{align*}
\xymatrix{
\text{ports of $a(b_{g(1)},\dots,b_{g(m)}))$}
\ar[d]
\\
\displaystyle{\biggl(\coprod_{\substack{i \in \set{1,\ldots,n}\\ j \in \set{1,\ldots,k}}} \text{ports of $b_{i,j}$}, 1 \biggr)}
\end{align*}

§.§.§ Distribute shallow terms over product

Finally, consider the function

\begin{align*}
\ranked{\shallowterm  {\Gamma^k} {\Sigma} \xrightarrow{\quad f_3\quad} (\shallowterm  \Gamma  \Sigma)^k}
\end{align*}

which distributes shallow terms over the $k$-th power.  This function is illustrated by the following  picture
and defined by

\begin{eqnarray*}
\xymatrix{
\ar@{|->}[d]^{\ranked{f_2}} \\
(a_1(b_1,\dots,b_{\text{ar}_1}), a_2(b_{\text{ar}_1+1},\dots,b_{\text{ar}_2}),\dots ,a_k(b_{\text{ar}_{k-1}+1},\dots,b_{\text{ar}_k}))
\end{eqnarray*}

where $\text{ar}_i$ is the arity of $a_i$ for $i\in\set{1,\dots,k}$.

§.§.§ Unfolding shallow terms.
The following diagram defines  unfolding of shallow terms in terms of the   operations $\ranked{f_1}, \ranked{f_2}, \ranked{f_3}$   defined above:

\begin{align*}
<EMAIL_ADDRESS>\ranked{\shallowterm{\mati k \rSigma} {\mati k \rGamma} = {\shallowterm{\reduce k {\Sigma^k}}{\reduce k {\Gamma^k}}}
\ar[d]_{\ranked{\substack{f_1}}}
\ar[r]^-{\ranked{\text{Shallow unfold}}}}
\ranked{ \reduce k(\shallowterm{\Sigma}{ {\Gamma}})^k = \mati k {(\shallowterm \Sigma \Gamma)}}
\\
\ranked{  \reduce k(\shallowterm{\reduce k {\Sigma^k}}{ {\Gamma^k}})}
\ar[r]_-{\ranked{\flatt\circ \reduce k f_2}}
\ranked{   \reduce k(\shallowterm{\Sigma^k}{ {\Gamma}}) } \ar[u]^{\ranked{\reduce k  f_3}}
\end{align*}

§.§ Definition of unfolding

Having defined shallow unfolding, we apply the induction principle described in Section <ref> to  define unfolding for general terms

\begin{align*}
\ranked{\unfold : \tmonad \mati k \rSigma \to \mati k {(\tmonad \Sigma)} }.
\end{align*}

If the input to general unfolding is the identity term $\portletter$, then  the output is:
Otherwise, if the input is a nonempty term $a(t_1,\ldots,t_n)$ then the output is obtained by first applying term unfolding to to the smaller terms $t_1,\ldots,t_n$, and then applying the shallow unfold.

§ EXAMPLES

To illustrate derivable functions, we present a series of examples, some of them will be useful later. In the rest of this section, for every $k\in\set{1,2,\dots}$ the set $\ranked{k}$ designates the ranked set containing a single element of arity $k$ that we denote by simply by $k$.

[Parent and children]  Let $\rGamma$ be a finite type. We define $\ranked{\rGamma_0}$  to be the ranked set obtained from $\rGamma$ by setting the arity of every element to $0$.
Consider the function:

$$\ranked{ \mathsf{Parent}: \tmonad \rGamma \to \tmonad (\rGamma\product (\rGamma_0+0))}$$

which adds to every node of a term in $\tmonad \rSigma$ the label  of its parent if it has one, and $0$ if it is the root.

Let us explain how $\ranked{\mathsf{Parent}}$ can be derived. To illustrate this construction, we use the following alphabet $\rGamma$

and the following term as a running example.

We denote by $\ranked{\Gamma_1}$ the ranked set obtained from $\rGamma$ by setting the arity of every element to $1$. If $a$ is a element of $\rGamma$, we denote by $a_1$ the corresponding element of $\ranked{\Gamma_1}$. In our example, the alphabet $\ranked{\Gamma_1}$ is

* First, we apply the homomorphism

\begin{align*}
\ranked{\mathsf{Hom}_g:\tmonad\Gamma\to \tmonad(\Gamma+\Gamma_1+1)}
\end{align*}

where $\ranked{g}$ is defined on the elements of $\rGamma$ as follows

\begin{align*}
\ranked{g: \Gamma} & \ranked{\to  \tmonad(\Gamma+\Gamma_1+1 )}\\
a & \mapsto a\tensorpair{1\tensorpair{a_1\tensorpair{\portletter}},\dots, 1\tensorpair{a_1\tensorpair{\portletter}}}
\end{align*}

In our example, the action of $\ranked{g}$ on the elements of $\rGamma$ looks like this

Hence, after the application of the homomorphism $\ranked{\mathsf{Hom}_g}$, our initial term becomes

* We apply the factorization

\begin{align*}
\ranked{\ancfact: \tmonad(\Gamma+\Gamma_1+1) \to \tmonad(\tmonad(\Gamma+\Gamma_1)+\tmonad 1)}
\end{align*}

to separate the symbol $1$ form the other symbols. After this operation, each node lies in the same factor as (the element of $\ranked{\Gamma_1}$ representing) its parent. In our example, the obtained term is the following

* Consider the function

\begin{align*}
\ranked{h: \tmonad 1 \to \tmonad((\Gamma+\Gamma_1)\product(\Gamma_0+0))}
\end{align*}

which is the empty term constant function. It is derivable by lifting the empty term constant function over $1$ to terms.
And let $k$ be the function

\begin{align*}
\ranked{k: \tmonad(\Gamma+\Gamma_1) \to \tmonad((\Gamma+\Gamma_1)\product(\Gamma_0+0))}
\end{align*}

which is the identity function, except for the following terms in which it is defined as follows

a\tensorpair{\portletter,\dots, \portletter}& \mapsto & \tensorpair{a,0}\tensorpair{\portletter,\dots,\portletter}\\
b_1\tensorpair{a\tensorpair{\portletter,\dots,\portletter}}&\mapsto& \tensorpair{a,b_0}\tensorpair{\portletter,\dots,\portletter}\\
b_1\tensorpair{\portletter} &\mapsto& \portletter
\end{array}$$

We apply the function $\ranked{h}$ to the factors $\ranked{\tmonad 1}$ and the function $\ranked{k}$ to the factors $\ranked{\tmonad(\rGamma+\rGamma_1)}$. Doing so, we obtain a term in $\ranked{\tmonad\tmonad((\Gamma+\Gamma_1)\product(\Gamma_0+0))}$, which we flatten, then we erase the symbols $\ranked{\Gamma_1}$ using the function $\mathsf{Filter}$ of Example <ref> to obtain the desired term.

If $\rGamma$ is a finite ranked set, we define $\ranked{\Gamma^*}$ as

$$\coprod_{i \leq \text{ maximal arity in } \rGamma} \underbrace{\ranked{\rGamma\product \cdots \product \rGamma}}_{i\text{ times}}$$

Now consider the function
$$\ranked{\mathsf{Children}:\tmonad\rGamma\to \tmonad (\rGamma\product (\rGamma_0+0)^*)}$$
which tags every node of a term in $\tmonad \rGamma$ by the list  of its children symbols. When a child is a port, it is marked by $0$ in the list.
The function $\ranked{\mathsf{Children}}$ can be derived using a similar construction as above.

[Root and leaves] Let $\rSigma$ be a finite type and $\ranked{f:\rSigma \to \rGamma}$, $\ranked{g: \rSigma \to \rGamma}$ be derivable functions. The function
$$\ranked{\mathsf{Root}_{f,g} : \tmonad\rSigma \to \tmonad\rGamma}$$

which applies $\ranked{f}$ to the root and $\ranked{g}$ to the rest of the tree is a derivable function.
To show this, we first start by applying the function $\ranked{\mathsf{Parent}}$. Doing so, the root can be distinguished from the other nodes since it will be tagged by $0$.

The function $\ranked{h}$ defined below is derivable since its domain is finite.

\begin{align*}
\ranked{h:\rSigma\product(\rSigma_0+0)}&\ranked{\to \rGamma}\\
\tensorpair{a,0} &\mapsto f(a) \\
\tensorpair{a,b} &\mapsto g(a) \text{ if } b\neq 0.
\end{align*}

We lift $\ranked{h}$ to terms to conclude.

Similarly, the function
$$\ranked{\mathsf{Leaves}_{f,g} : \tmonad\rSigma \to \tmonad\rGamma}$$

which applies $\ranked{f}$ to the leaves and $\ranked{g}$ to the rest of the tree is derivable. This is done using the same ideas as before, but invoking the function $\ranked{\mathsf{Children}}$ instead of the function $\ranked{\mathsf{Parent}}$: leaves can be distinguished from the other nodes since they are tagged either by a list of $0$ or the empty list.

[Descendants and ancestors] If $\rSigma$ is a finite type and $\ranked{\rGamma\subseteq \rSigma}$, then the functions

* $\ranked{\mathsf{Descendant}_\rGamma: \tmonad \rSigma \to \tmonad (\rSigma+\rSigma)}$ which replaces the label of each node by its first or second copy, depending on whether it has a descendant in $\rGamma$,

* $\ranked{\mathsf{Ancestor}_\rGamma: \tmonad \rSigma \to \tmonad (\rSigma+\rSigma)}$ which replaces the label of each node by its first or second copy, depending on whether it has a descendant in $\rGamma$,

are derivable.

To derive $\ranked{\mathsf{Descendant}_\rGamma}$, we start by applying the factorization
$$\ranked{\decfact: \tmonad\rSigma\to \tmonad(\tmonad\rGamma+\tmonad(\rSigma\setminus\rGamma))}$$
which regroups the elements of $\rSigma$ and the elements of $\ranked{\rSigma\setminus\rGamma}$ into factors depending on whether they have the same ancestors of the same type.

Obviously, all the nodes of the $\rGamma$ factors have a descendant in $\rGamma$.
In the $\ranked{\rSigma\setminus\rGamma}$ factors which are not leaves in the factorized term, all the nodes have a $\rGamma$ descendant in the original term. To show this, take $f$ to be one of these factors, and suppose by contradiction that one of its nodes does not have a descendant in $\rGamma$. By definition of $\ancfact$, all the elements of $f$ do not have a descendant in $\rGamma$ as well. Since $f$ is not a leaf, it has a child $g$. The factor $g$ cannot be a $\rGamma$
factor as the nodes of $f$ would have a descendant in $\rGamma$. The factor $g$ is then necessarily  a $\ranked{\rSigma\setminus \rGamma}$ factor. If a node of $g$ has a descendant in $\rGamma$, this would give a $\rGamma$ descendant to one of the node of $f$. Thus all the nodes of $g$ are in $\ranked{\rSigma\setminus \rGamma}$ and do not have a descendant in $\rGamma$, meaning that $f$ and $g$ are actually the same factor, which gives a contradiction. Finally, the $\ranked{\rSigma\setminus\rGamma}$ factors which are leaves do not have a descendant in $\rGamma$. With these observations, we can now implement $\mathsf{Descendant}_\rGamma$.

Let us consider the functions

\ranked{\mathsf{Yes}_\rGamma :} & \rGamma &\ranked{\to} &\ranked{ \rSigma+\rSigma}\\%\noindent\begin{example}[Filter]\label{ex:filter} Consider the types $\rGamma, \rSigma$  where $\rGamma$ is a finite type of unary symbols. Consider the function:
%$$ \ranked{f:\tmonad (\rSigma+\rGamma)\to\tmonad \rSigma}$$
%which erases the elements of $\rGamma$ from the input term. This function is well defined since erasing unary symbols does not break the tree structure of the input.
%Let us explain why this is a derivable function.
%Consider the basic functions $\ranked{\unit_\rSigma:\rSigma\to\tmonad\rSigma}$ and the constant function $\ranked{\mathsf{empty}:\rGamma\to\tmonad\rSigma}$ which associates to every element of $\rGamma$ the empty term. We compose the following two functions
%    \ranked{\rSigma+\rGamma}\quad \ar[r]^-{\ranked{\unit_\Sigma+\mathsf{empty}}} & \quad \ranked{\tmonad\rSigma+\tmonad\rSigma}\ar[r]^-{\ranked{\mathrm{forget}}} &\tmonad\rSigma
%Then we lift the obtained function to terms, and compose the result with the $\flatt$ function to obtain our function $\ranked{f}$.
\ranked{\mathsf{Yes}_{\ranked{\rSigma\setminus\rGamma}:}}& \ranked{\rSigma\setminus\rGamma}&\ranked{\to} &\ranked{ \rSigma+\rSigma}\\
\ranked{\mathsf{No}_{\ranked{\rSigma\setminus\rGamma}: }}&\ranked{\rSigma\setminus\rGamma} &\ranked{\to}& \ranked{ \rSigma+\rSigma}
\end{array}$$

which replaces the label of each node by its first copy for $\ranked{\mathsf{Yes}_\Gamma}$ and $\ranked{\mathsf{Yes}_{\rSigma\setminus\rGamma}}$, and by its second copy for $\ranked{\mathsf{No}_{\rSigma\setminus\rGamma}}$. The three functions are derivable as their domains are finite.
Consider the functions

\begin{align*}
\ranked{f:=} &\ranked{ \tmonad\mathsf{Yes}_\rGamma +\tmonad\mathsf{No}_{\rSigma\setminus \rGamma}}\ranked{: \tmonad\rGamma+\tmonad(\rSigma\setminus\rGamma) \to \tmonad (\rSigma+\rSigma)}
\\
\ranked{g:=} & \ranked{ \tmonad\mathsf{Yes}_\rGamma
+\tmonad\mathsf{Yes}_{\rSigma\setminus \rGamma}}\ranked{: \tmonad\rGamma+\tmonad(\rSigma\setminus\rGamma) \to \tmonad (\rSigma+\rSigma)}
\end{align*}

The descendant function is obtained by applying $\ranked{\mathsf{leaves}_{f,g}}$ followed by a flattening.

To derive the function $\ranked{\mathsf{Ancestor}_\Gamma}$, we apply first a the factorization

\begin{align*}
\ranked{\ancfact: \tmonad\rSigma\to \tmonad(\tmonad\rGamma+\tmonad(\rSigma\setminus\rGamma))}
\end{align*}
which regroups the elements of $\rSigma$ and the elements of $\ranked{\rSigma\setminus\rGamma}$ into factors depending on whether they have the same descendants of the same type.
Using similar arguments as before, we can conclude that:

* The nodes inside $\rGamma$ factors have $\rGamma$ ancestors.

* If a $\ranked{\rSigma\setminus\rGamma}$ factor is the root of the factorized term, then its nodes do not have a $\rGamma$ ancestor.

* If a $\ranked{\rSigma\setminus\rGamma}$ factor is not the root of the factorized term, then its nodes do have a $\rGamma[Descendants and ancestors]\label{ex:descendant}$ ancestor.

The ancestor function is obtained by applying $\ranked{\mathsf{root}_{f,g}}$ followed by a flattening.

[Error raising.]
We can think of the type $\ranked{\bot}$ as an error type. Indeed, the following raising error functions are derivable.

Let $\rSigma$ and $\rGamma$ be two datatypes. The functions

\ranked{\tmonad(\Sigma+\bot)} &\ranked{\to }&\ranked{\tmonad \Sigma +\bot}\\
\ranked{(\Sigma+\bot) \product (\Gamma+\bot)} &\ranked{\to} &\ranked{\Sigma\product \Gamma+\bot }\\
\ranked{\shallowterm {(\Sigma+\bot)}{(\Gamma+\bot)}} &\ranked{\to} &\ranked{\shallowterm\Sigma\Gamma +\bot}\\
\ranked{\reduce k (\Sigma+\bot)} &\ranked{\to} &\ranked{\reduce k \Sigma +\bot}
\end{array}$$

which are defined as follows

\begin{align*}
t \text{ of arity } n \ \ \mapsto \  \begin{cases}
t &
\text{if $t$ does not contain any element of $\ranked{\bot}$,}\\
n & \text{otherwise.}
\end{cases}
\end{align*}
are derivable.

These functions can be easily derived using Proposition <ref> and distributivity prime functions. The details of the proof are left as an exercise to the reader.

[Partial functions.]
Thinking of $\ranked{\bot}$ as an error datatype, a function of type $\ranked{\Sigma \to \Gamma +\bot}$
can be seen as a partial function from $\rSigma$ to $\rGamma$. We write

\begin{align*}
\ranked{\Sigma\rightharpoonup \Gamma}
\end{align*}

as a notation for the function type $\ranked{\Sigma \to \Gamma +\bot}$.
Using the error raising mechanisms discussed earlier, we can manipulate transparently partial function. Indeed, all datatype constructors can be lifted to partial functions, by composing the liftings (1)–(4) with the error raising functions from Lemma <ref>. For example, if $\ranked{f:\Sigma\rightharpoonup \Gamma}$ is a partial function, then $\ranked{\tmonad f:\tmonad\Sigma\rightharpoonup \tmonad\Gamma}$ is defined as the composition

\begin{align*}
\ranked{\tmonad\Sigma\xrightarrow{\tmonad f} \tmonad(\Gamma+\bot) \xrightarrow{\text{Error raising}} \tmonad \Gamma +\bot}.
\end{align*}

§ DERIVABLE FUNCTIONS CAN BE DESCRIBED IN FIRST-ORDER LOGIC

The goal of this section is to show the right-to-left implication of Theorem <ref>, which says that derivable functions can be implemented by first-order transductions.

As discussed in the body of the paper, we proceed by induction on the derivation. During this induction, we will need to show that every prime function is a first-order transduction. Prime functions are not tree-to-tree functions, instead they transform dataypes into datatypes. This is the reason why we need

* to generalize tree-to-tree transductions into  transductions that can transform models over arbitrary vocabularies (and not only the vocabulary of trees).

* show how datatypes (terms, pairs, copairs and folds) can be encoded as models over a well chosen vocabulary. More precisely, we will associate to every datatype $\rSigma$ a relational vocabulary that we call vocabulary of $\rSigma$. Structures over this vocabulary will be called models over $\rSigma$. Then we will define a function

\begin{align*}
\xymatrix@C=2cm{
\rSigma \ar[r]^-{x \mapsto \underline x} &
\text{models over $\rSigma$}
\end{align*}

which assigns to each element $x \in \rSigma$ a corresponding model  over $\rSigma$, which is denoted by $\underline x$.

Right-to-left implication of Theorem <ref> can be then generalized to the following statement, more suited to a proof by induction:

Let $\rGamma$ and $\rSigma$ be two datatype.  For every derivable function $\ranked{f}$, there is a first-order transduction $g$ such that the following diagram commutes

\begin{align*}
<EMAIL_ADDRESS>\rSigma
\ar[d]_{x \mapsto \underline x}
\ar[r]^-{\ranked{f}}
\rGamma \ar[d]^{x \mapsto \underline x}
\\
\text{models over $\rSigma$}
\ar[r]_-{g}
\text{models over $\rGamma$}
\end{align*}

The rest of this section is organized as follows. We define first-order transductions transforming arbitrary models in Section <ref>. In Section <ref> we define the vocabularies for the  datatypes and the model representation $x \mapsto \underline x$. Finally, we prove Proposition <ref> which gives as a corollary the right-to-left implication of Theorem <ref>.

§.§ First-order transductions

The following definition introduces first-order transductions, which generalizes tree-to-tree transductions given in Definition <ref> to arbitrary models.

A first-order transduction is defined to be any  composition of the following two kinds of transformations on structures:

* Copying. Fix some  relational vocabulary $\ranked \sigma$ and let $k \in \set{1,2,\ldots}$. Define $k$-copying to be the operation of type

\begin{align*}
\xymatrix{
\text{models over $\ranked \sigma$} \ar[d]\\
\txt{models over $\ranked \sigma$  extended\\
with a $k$-ary relation $\mathrm{copy}$}
\end{align*}

which inputs a model $\mathbb A$, and outputs $k$ disjoint copies of $\mathbb A$, where the  $\mathrm{copy}$ relation is interpreted as the set of tuples $(a_1,\ldots,a_k)$ such that, for  some $a \in \mathbb A$, the first copy of $a$ is  $a_1$, the second copy of $a$ is $a_2$, etc. The $\mathrm{copy}$ relation  is not commutative, because we distinguish the copies.

* Non-copying first-order transduction. The syntax of a non-copying first-order transduction  is given by:

* Input relational vocabulary $\ranked\sigma$ and output relational vocalbulary $\ranked{\gamma}$.

* A first-order universe formula $\varphi(x)$ over $\ranked{\sigma}$.

* For every relation $R$ in vacubulary $\ranked{\gamma}$, a first-order  formula $\varphi_R(x_1,\ldots,x_{\arity R})$ over $\ranked{\sigma}$.

The semantics of a non-copying first-order transduction is  a function

\begin{align*}
\xymatrix{
\text{models over $\ranked \sigma$} \ar[d]\\
\text{models over $\ranked \gamma$}
\end{align*}

defined as follows. If the input model is $\mathbb A$, then the output model is defined as follows: the universe is elements of $\mathbb A$ which satisfy the universe formula, and each relation $R$ is interpreted as those tuples that satisfy $\varphi_R$.

The notion of copying used in the above definition is slightly different from the notion of copying used for tree-to-tree transductions in Definition <ref>, which was specifically tailored to stay within the realm of trees. Nevertheless, the two definitions are easily seen to define the same class of tree-to-tree functions.

§.§ Datatypes  as models.

Let us show how to encode datatypes as relational vocabularies and data as models over these vocabularies.
To each type  $\rSigma$ we associate a vocabulary, called the vocabulary of $\rSigma$, and a map

\begin{align*}
a \in \rSigma \qquad \mapsto \qquad \underbrace{\underline a \in \text{models over the  vocabulary of  $\rSigma$}}_{\text{associated model of $a$}}.
\end{align*}

Furthermore, for each $a \in \rSigma$ we  distinguish a  sequence (whose length is the arity of $a$) of elements in $\underline a$, which are called the ports of $\underline a$.   The definitions are by induction on the structure of $\rSigma$, as given below.

* Finite ranked sets. Elements of a ranked set
\begin{align*}
\rSigma =  \set{a_1,\ldots,a_k}
\end{align*}
are modelled  using a vocabulary which has unary relations $a_1,\ldots,a_k$ and $P_1,\ldots,P_m$ where $m$ is the maximal arity of elements in $\rSigma$.
For $a \in \rSigma$ of arity $n$, the  universe of $\underline a$ is $\set{0,1,\ldots,n}$, with the ports being $1,\ldots,n$.
The  relation $P_i$  is interpreted as $\set i$ when $i \in \set{1,\ldots,n}$ and as the empty set otherwise. The relation $a_i$ is interpreted as $\set 0$ when $a = a_i$ and as the empty set otherwise.

* Coproduct.  Elements of the coproduct $\ranked{\Sigma_1 + \Sigma_2}$ are modelled using the disjoint union of the vocabularies of $\ranked{\Sigma_1}$ and $\ranked{\Sigma_2}$.
If an element of the coproduct comes from $\ranked{\Sigma_1}$, then its associated model is defined as for the type $\ranked{\Sigma_1}$, with  the remaining relations from the vocabulary of   $\ranked{\Sigma_2}$ interpreted   as empty sets. The definition is analogous for  elements from $\ranked{\Sigma_2}$.

* Product.   Pairs in   $\ranked{\Sigma_1 \product \Sigma_2}$ are modelled
using the disjoint union of the vocabularies of $\ranked{\Sigma_1}$ and $\ranked{\Sigma_2}$.
For  $\tensorpair{a_1,a_2}$, the associated model is    the disjoint union of models $\underline{a_1} + \underline {a_2}$, with the relations of $\underline {a_1}$ using the  vocabulary of ${\ranked{\Sigma_1}}$, and the relations of $\underline {a_2}$ using the vocabulary  ${\ranked{\Sigma_1}}$.
If $n_1$ is the arity of $a_1$, then the first $n_1$ ports are inherited from  $\underline {a_1}$ and the remaining ports are inherited from  $\underline {a_2}$.

* Folding.   For $k \in \set{1,2,\ldots}$, elements of   $\reduce k \rSigma$ are modelled using the  vocabulary of $\rSigma$ plus two extra binary relations $\portord$ and $R$. If $a \in \rSigma$ has arity $nk$, then the model associated to $a/f$ – which has arity $n$ –   is obtained from  $\underline{a}$ by adding a copy of the model below, where $\sqsubset$ is the natural ordering on integers

\begin{align*}
(\set{1,\ldots,n}, \portord),
\end{align*}

whose elements are used as the ports, and interpreting the binary relation $R$ as

\begin{align*}
\set{(\text{$i$-th port of $\underline a$},f(i)) : i \in \set{1,\ldots,nk}}
\end{align*}

* Terms.   Terms in $\tmonad \rSigma$ are modelled using vocabulary of $\rSigma$ extended with two fresh binary relations $\anceord$ and $\portord$.
Let $t \in \tmonad \rSigma$. Consider the disjoint union of models

\begin{align}\label{eq:non-port}
\coprod_{x \in \text{non-port nodes in $t$}} \underline{a(x)},
\end{align}

where  $\underline a(x)$ is the model over vocabulary of $\rSigma$ that  is defined by induction assumption.   In the above  disjoint union, the same vocabulary, namely the vocabulary of $\rSigma$,  is used  for all parts of the disjoint union. Next, consider  the model

\begin{align}\label{eq:ports}
(\set{1,\ldots,n}, \portord)
\end{align}

where $\portord$ is the natural ordering on $\set{1,\ldots,n}$.
The model of $t$ is defined by taking the disjoint union of the models in (<ref>) and (<ref>), and defining the descendent relation $\anceord$ as the set of pairs $(u,v)$ such that:

* either $u$ is the $i$-th port of $\underline{a(x)}$ for some node $x$ of $a$, $v$ is a port of $\underline{a(y)}$ for some node $y$ which is a descendent of the $i$-th child of $x$.

* or $u$ is the $i$-th port of $\underline{a(x)}$ for some node $x$ of $a$, $v=j\in\{1,\dots,n\}$ and the $j$-th port of $a$ is a descendent of the $i$-th child of $x$.

The above  definition creates a certain ambiguity for trees, because if $t$ is a tree over a finite ranked set $\rSigma$, then $\underline t$ can be understood in two ways: as per  Definition <ref> for trees, or as per Definition <ref> when $t$ is viewed as a special case of a term $t \in \tmonad \rSigma$. Since we only use first-order transductions to transform relational structures,  this ambiguity is not a problem, because one can easily define first-order transductions which map one definition of $\underline t$ to the other.

§.§ Proof of Proposition <ref>

The proof proceeds by induction, following the definition of derivable functions.
In the induction step, we have to deal with function composition and the lifting of function along the datatype constructors. First-order transductions are closed under composition by definition, while the liftings are immediate.

In the induction base, we need to show that all of the prime functions are first-order transductions.
All the cases are easy, and consist mainly on unfolding the definitions; this is the point of calling these functions prime. There is one exception, which requires some more explanation, namely monotone unfolding. We explain below just one of the easy functions, the unit function $\ranked{\Sigma \to \tmonad \Sigma}$, and the monotone unfolding. The other prime functions are left as an exercise.

§.§.§ A first-order transduction for the term unit

In the following, it will be convenient to use, as part of the vocabulary of $\rSigma$, a unary relation  $\mathsf{Port}_\rSigma$ which selects the ports of the structures over the vocabulary of $\rSigma$; and a binary relation $\sqsubset_\rSigma$ which orders these ports. By induction on $\rSigma$, we can show that both relations are definable by first-order formulas over  the vocabulary of $\rSigma$.

Given an element $x$ of $\rSigma$, let us show how  $\unit(x)$ can be implemented using a first-order transduction.  The copying constant is 2,
the first copy will contain the whole structure $\underline{x}$ and the second copy will select only the ports of $\underline{x}$ which will serve as the ports of the structure $\underline{\unit(x)}$, as illustrated by the following picture

The universe formulas are then:

\begin{align*}
\varphi_1(x)=\mathsf{True} \qquad \varphi_2(x)=\mathsf{Port}_\rSigma(x)
\end{align*}

In the first copy, the vocabulary of $\rSigma$ will be interpreted as in the original structure, and as the empty set in the second copy. That is, for every unary relation $R$ and for every binary relation $S$ in the vocabulary of  $\rSigma$, we set:

\begin{align*}
\varphi_R^{1}(x)=R(x) \quad&\quad \varphi_S^{1,1}(x,y)=S(x,y)\\
\varphi_R^{2}(x)=\mathsf{False} \quad&\quad \varphi_S^{2,2}(x,y)=\mathsf{False}
\end{align*}

Let us interpret the relations $<$ and $\sqsubset$ of the vocabulary of $\tmonad\rSigma$. The  ports of $\underline{\unit(x)}$ inherit the order of the ports of $\underline{x}$, this is why we set:

\begin{align*}
\varphi_\sqsubset^{2,2}(x,y)=x\sqsubset_\rSigma y
\end{align*}

The descendant relation $<$ connects the $i^{th}$ port of $\underline{x}$ to the $i^{th}$ port of $\underline{\unit(x)}$. Since these nodes come from the same node in the original structure, we set:

\begin{align*}
\varphi_<^{1,2}(x,y)=x=y
\end{align*}

§.§.§ A first-order transduction for monotone unfolding

Having illustrated the syntax of first-order transductions on the example of the unit function, we describe a first-order transduction for the monotone unfolding operation

\begin{align*}
\ranked{\tmonad \mati k{\Sigma} \to \mati k{( \tmonad \Sigma)} + \termset}.
\end{align*}

This is the only prime function whose corresponding first-order transduction is not obvious.
Unlike in Section <ref>,  we focus more  on the underlying conceptual difficulties than on the syntax of first-order transductions.

Recall  that when  defining the  monotone  unfolding operation,  for each element $a \in \ranked{\tmonad \mati k{\Sigma}}$ of the matrix power, we used a family of (partial) twist functions

\begin{align*}
\to_i : \set{1,\ldots,k} \to \set{1,\ldots,k},
\end{align*}

one for each port $i$ of $a$. For the reader's convenience, we repeat a picture from Section <ref>, which explains the twist functions:

In this example, the twist function $\to_1$ is monotone, but  $\to_2$ is not. The monotone unfolding operation works in the same way as general  unfolding, except that it uses the undefined value $\termset$ if the input term has at least one letter which uses at least one non-monotone twist.

The following lemma, whose simple proof is left to the reader, shows that the twist functions can be defined using first-order logic.

Let $\rSigma$ be a datatype and let $k \in \set{1,2,\ldots}$. For every partial function

\begin{align*}
\tau : \set{1,\ldots,k} \to \set{1,\ldots,k}
\end{align*}

there is a first-order formula $\varphi_\tau(x)$ such that for every $a \in \mati k \rSigma$,

\begin{align*}
\underline a \models \varphi_\tau(x)
\end{align*}

if and only if $x$ represents a port  with twist function $\tau$.

By using the formulas from the above lemma, one can construct  a first-order formula which checks if a term in $\tmonad \mati k \rSigma$ uses only monotone twists, i.e. whether or not the output of monotone unfolding should be $\termset$.

We now proceed to the more interesting part of monotone unfolding, i.e. actually doing the unfolding for  monotone inputs. Consider an input $t \in \tmonad \mati k \rSigma$ to monotone unfolding.
Define a sub-node of $t$ to be a pair (node of $t$, number in $\set{1,\ldots,k$}), as explained in the following picture:
\mypic{124}

In the output of the monotone unfolding, which is of the form
\begin{align*}
(t_1,\ldots,t_k)/f \in \mati k {\tmonad \rSigma},
\end{align*}
the nodes of the  output terms $t_1,\ldots,t_k$ will correspond to the sub-nodes in the input $t$. The sub-nodes can be produced by  copying the input term $k$-times.

The most interesting part of the structure in the output is the descendant relation in the terms $t_1,\ldots,t_k$. This relation  can be viewed as a descendant relation on the sub-nodes. We only describe how the descendant relation on the sub-nodes can be defined in first-order logic, and the rest of the transduction is left to the reader.

When defining the descendant relation on sub-nodes, the crucial part is composing the twist functions.  Suppose that we want to check the descendant relationship between two sub-nodes
\begin{align}\label{eq:descendant-relationship}
(x,i) \stackrel?{\le} (y,j),
\end{align}
where $x,y$ are nodes on the input term and $i,j \in \set{1,\ldots,k}$. We will show that the descendant relationship~\eqref{eq:descendant-relationship} holds if and only if $x$ is an ancestor of $y$ in the input term,  and the twist functions on the path connecting $x$ and $y$ maps $j$ to $i$, as explained below.

Consider a path in the input term, which connects  node $x$ with $y$, as  illustrated in the following picture
\mypic{123}
Each edge in the input term corresponds to a chosen port in some node, which in turn corresponds to some twist function, and therefore it makes sense to talk about the twist function associated to an edge in the input term. Define
\begin{align*}
\tau_y^x : \set{1,\ldots,k} \to \set{1,\ldots,k}
\end{align*}
to be the partial function, which is obtained by composing all of the twist functions corresponding to edges on the path connecting $y$ to $x$,  starting with $y$ and ending with $x$. In the example from the above picture, we compose two twist functions, which correspond to edges marked in yellow.

Equipped with the above definitions, we can now characterise the descendant ordering on sub-nodes by
\begin{align*}
(x,i) \le (y,j) \qquad \text{iff} \qquad x \le y \land \tau_y^x(j)=i.
\end{align*}
Therefore, to complete the proof, it remains to show the following lemma. This is where we use the monotonicity assumption.

\begin{lemma}\label{lem:counter-free}
For every $i,j \in \set{1,\ldots,k}$
there is a first-order formula $\psi_j^i(x,y)$ such that for every $t  \in \tmonad \mati k \rSigma$
\begin{align*}
\underline t \models \psi_j^i(x,y) \qquad \text{iff} \qquad \tau_y^x(j)=i.
\end{align*}
\end{lemma}
\begin{proof}
Let $F$ be the set of monotone partial functions  from $\set{1,\ldots,k}$ to itself. Define $L \subseteq F^*$ to be the set of those words $f_1 \cdots f_n$ such that the composition of functions $f_n\circ \cdots \circ f_1$ maps $i$ to $j$. We will show that -- thanks to the monotonicity assumption -- the language $L$ is definable in first-order logic. To get the conclusion of the lemma, we check if the sequence of twist functions on the path  from $x$ to $y$ satisfies the first-order formula defining the language $L$.

The language $L$ is recognised by a finite automaton, which has states $\set{1,\ldots,k,\bot}$, and which simply applies the function in its input letter to the present state. We show below that this automaton is counter-free, in the sense of McNaughton and Papert~\cite[p.~6]{McNaughtonPapert71}, and therefore it can be defined in first-order logic.

Recall that a counter in an automaton is a sequence of at least two pairwise distinct states $q_1,\ldots,q_n$ such that
\begin{align*}
q_1  \stackrel w \to q_2 \stackrel w \to \cdots \stackrel w \to q_n \stackrel w \to q_1
\end{align*}
holds for some common input string $w$. In the automaton for the language $L$ that we have discussed above, there is no counter. Indeed, if we would have $q_1 \le q_2$, then by monotonicity of the function   $w \in F$ we would have
\begin{align*}
q_1 \le q_2 \le \cdots \le q_n \le q_1
\end{align*}
and therefore all of $q_1,\ldots,q_n$ would be equal, contradicting the assumption that they are pairwise distinct. The same argument would work when $q_1 \ge q_2$. By~\cite[Theorem 10.5]{McNaughtonPapert71}, if an automaton has no counter, then its language is definable in first-order logic.

\end{proof}
\section{Appendix on first-order relabelling}~\label{sec:AppendixForat}

The goal of this section is to show Proposition~\ref{prop:forat}, which says that first-order relabeling are derivable. As discussed in the body of the paper, the proof of this proposition is based on an equivalence result between first-order queries on trees  and a temporal logic, as stated in Lemma~\ref{lem:schlingloff}. While this result is deaply inspired from a similar result of Schlingloff [26], our frameworks are not exactly the same (he uses for ainstance unranked trees).
In the rest of this section, we provide more details about the reduction from Schilgloff's result to our lemma (Section~\ref{sec:reduction-schilingloff}). Then we show in Section~\ref{sec:relabeling}  how to use it in order to prove Proposition~\ref{prop:forat}.

\subsection{Reduction to Schilgloff's theorem}\label{sec:reduction-schilingloff}

Let us proceed to the proof of Lemma~\ref{lem:schlingloff}.
Clearly the functions in the lemma are first-order tree relabeling, and first-order tree relabeling are easily seen to be closed under composition, which gives the right-to-left inclusion in the lemma. The hard part is the left-to-right inclusion, which says that every first-order tree relabeling can be decomposed into functions as in items~\ref{it:relabelling},\ref{it:child}--\ref{it:since}.
The first  step in the proof of  the right-to-left inclusion is the observation that  every first-order tree relabeling can be decomposed as
\begin{align*}
g \circ f_1 \circ \cdots \circ f_n
\end{align*}
where $g$ is a relabeling as in item~\ref{it:relabelling} of the lemma and each $f_i$ is a  characteristic function of some unary query (not necessarily of the simple form indicated in items~\ref{it:child} -- \ref{it:since} in the lemma). This is a simple observation: the functions $f_1,\ldots,f_n$ annotate the tree with the truth values of the unary queries used in the definition of the  first-order relabeling, and $g$ uses these truth values to select the appropriate output label. The hard part of the lemma is showing that each $f_i$  can be further decomposed into functions as indicated in the lemma. This is where we us the result of Schlingloff~\cite[Theorem 2.6]{schlingloff1992expressive}, which says that all first-order definable tree properties can be defined using a temporal logic that has operators similar to the ones used in items~\ref{it:child} -- \ref{it:since} of the lemma.

The following table summarizes our framework (first column) and Schlingloff's one (second column). The first row describes the models under consideration, the second row the corresponding version of first-order logic, and the third row the corresponding temporal logic.
\begin{center}
\begin{tabular}{|C{1.8cm}|C{2.9cm}|C{2.8cm}|}
\cline{1-3}
\textbf{Models} & \textbf{Trees over a finite ranked alphabet $\rGamma$}: finitely branching, ranked trees, labeled from $\rGamma$. & \textbf{Models over a set of propositions $P$}: finitely branching, unranked trees, labeled from $2^P$.\\
\hline
\multirow{3}{1.8cm}{\begin{center}\textbf{First-order logic}\end{center}}&\multicolumn{2}{C{5.6cm}|}{Usual first-order connectives ($\exists, \vee, \neg$) with the descendant predicate $x\leq y$ and the following predicates:}\\
\cline{2-3}
& $a(x)$:  $x$ is labeled $a$  $(a \in \rGamma)$.  & $p(x)$: label of $x$ contains $p$
($p\in P$). \\
&\hspace{-.14cm}$\child i(x)$: $x$ is an $i$-th child. &\\
&       \textbf{We call it $\rGamma$-\fo.}    &  \textbf{We call it $P$-\fo. }            \\
\hline
\multirow{4}{1.8cm}{\begin{center}
\textbf{Temporal logic}
\end{center}}& \multicolumn{2}{C{5.6cm}|}{Usual CTL connectives ($S$ (Since), $U$ (Until), $\vee$, $\neg$) together with:}\\
\cline{2-3}

& $a \in \rGamma$, & $p \in P$, \\
& $\odot_i \phi$: the $i$-th child satisfies $\phi$. & $X_i \phi$: at least $i$ children satisfy $\phi$.\\
&       \textbf{ We call it 2-CTL. }   &   \textbf{We call it 4-CTL.            } \\
\hline
\end{tabular}
\end{center}
What is named $\rGamma$-\fo in the table is what we simply called first-order logic along the paper. The operators of 2-CTL are those of Lemma~\ref{lem:schlingloff}.  Using the notation of the table,
Schlingloff's theorem says that $P$-\fo formulas are equivalent to 4-CTL formulas, and  Lemma~\ref{lem:schlingloff} states that $\rGamma$-\fo formulas are equivalent to 2-CTL ones. To deduce the later from the former, we will show how to translate every ranked tree $t$ over $\rGamma$ into a model $[t]$ over a well chosen set of propositions $P$, then we will apply the following scheme
\varphi \in \rGamma\text{-\fo}
\ar@{<->}[r]^{\forall t, \ t\models \varphi \ \leftrightarrow \ [t] \models \psi}_{\text{Lemma}~\ref{lem:from-Gamma-to-P-FO}}
\psi \in P \text{-\fo}
\ar@{<->}[d]^{\substack{\text{Schlingloff's}\\\text{theorem}}} \\
\theta \in \text{2-CTL}
\ar@{<->}[r]^{\forall t, \ t\models \theta \ \leftrightarrow \ [t] \models \delta}_{\text{Lemma}~\ref{lem:from-4-CTL-to-2CTL}}
\delta \in \text{4-CTL}
The translation $[\_]$ and Lemmas~\ref{lem:from-Gamma-to-P-FO} and \ref{lem:from-4-CTL-to-2CTL} are explained below.

\paragraph{From ranked trees to Schlingloff's models.} Let us fix a ranked alphabet $\rGamma$. Let $P$ be the following set of propositions
\begin{align*}
P\eqdef \rGamma\cup\set{i\text{-th-child}\ |\ i\in[1, \text{max arity of }\rGamma]}
\end{align*}
Let $t$ be a ranked tree over $\rGamma$. The translation $[t]$ of $t$ is the model defined as follows. It has the same set of nodes and the same descendant relation as $t$. The label of a node contains $a$ if its label in $t$ is $a$. It contains the proposition $i\text{-th-child}$ if it is an $i$-th child in $t$.

\paragraph{First-order logic for ranked and unranked trees.} Let $\rGamma$ and $P$ be as above. Let us show that $\rGamma$-\fo and $P$-\fo are equivalent.
\begin{lemma}\label{lem:from-Gamma-to-P-FO}
For every $\rGamma$-\fo formula $\phi$, there is a $P$-\fo formula $\psi$ such that
$$ \forall t\in \trees\rGamma, \qquad t\models \phi \leftrightarrow [t]\models \psi$$
and conversely.
\end{lemma}
\begin{proof}
To show this lemma its is enough to show how to translate the specific predicates of each formalism into the other. The predicate $a(x)$ of $\rGamma$-\fo can be translated by the same predicate in $P$-\fo and conversely. The predicate $\child i(x)$ can be translated by $i\text{-th-child}(x)$ and conversely.  It is clear that these translations preserve the semantics.
\end{proof}

\paragraph{Temporal logic for ranked and unranked trees.}
Let $\rGamma$ and $P$ be as above. We show that 2-CTL and 4-CTL are equivalent.
\begin{lemma}\label{lem:from-4-CTL-to-2CTL}
For every $\rGamma$-\fo formula $\phi$, there is a $P$-\fo formula $\psi$ such that
$$ \forall t\in \trees\rGamma, \qquad t\models \phi \leftrightarrow [t]\models \psi$$
and conversely. \end{lemma}
\begin{proof}
Here again, it is enough to translate the specific connectives of each formalism into the other. The connective $X_i$ can be encoded in 2-CTL as follows, where $b$ is the maximal arity of $\rGamma$
\begin{align*}
\underset{\begin{array}{c}
{\scriptstyle I\subseteq [1,b]}\\ {\scriptstyle\#I=i}
\end{array}}{\bigvee} \underset{j\in I}{\bigwedge} \odot_j \phi
\end{align*}
Conversely, the connective $\odot_i$ can be encoded in 4-CTL as follows:
\begin{align*}
X_1(i\text{-th-child}\wedge \phi)
\end{align*}
\end{proof}
%Let $\rGamma$ be a ranked alphabet. The formulas of 2-$\mathsf{CTL}$ are generated by the following syntax:
%\varphi, \psi:= \ a\in \rGamma \ | \ \odot_i \phi \ | \ \varphi\untilmod \psi \ | \ \varphi\sincemod\psi
%The semantics of these formulas are defined for the ranked trees of $\trees \rGamma$ as follows.
%\item A tree of $\trees \rGamma$ satisfies the formula $a\in\rGamma$ at the node $x$ if the label of $x$ is $a$.
%\item $t, x\models \odot_i \varphi$ if the $i$-th child of $x$ satisfies $\varphi$.
%\item  The formula $\varphi\untilmod \psi$  is valid  in the node $x$ if $x$ has a descendant $y$ with label in $\rDelta$, such that all nodes between $x$ and $y$ have label in $\rGamma$.
%\item $x$ has a descendant $y$ with label in $\rDelta$, such tha all nodes between $x$ and $y$ have label in $\rGamma$.
%\begin{lemma}%[Decomposition lemma]
%For every first-ordre formula $\phi$, there is a $2$-$\mathsf{CTL}$ formula $T$ such that
%$$ \forall t\in \trees \rGamma \qquad t,x\models \varphi \Leftrightarrow t,x\models T.$$
%Shclingloff considers node labeled, branching bounded and   unordered (there is no order between the children of a node) trees. If $\Gamma$ is an (unranked) alphabet, we denote by $\trees_b\Gamma$ the set of unordered trees, labelled from $\Gamma$ and whose branching is at most $b$.
%The formulas of $4$-$\mathsf{CTL}$ are generated by the following syntax:
%\varphi, \psi:= \ a\in \Gamma \ | \ \nextmod_i \phi \ | \ \varphi\untilmod \psi \ | \ \varphi\sincemod\psi
%The semantics of $4$-$\mathsf{CTL}$ formulas is as before. The connective $\nextmod_i$ have the following semantics:
%%\begin{theorem}\cite{}%[Decomposition lemma]
%%For every first-ordre formula $\phi$, there is a $4$-$\mathsf{CTL}$ formula $T$ such that
%%$$ \forall t\in \trees_b \Gamma \qquad t,x\models \varphi \Leftrightarrow t,x\models T.$$
%% Let us explain how Lemma~\ref{} can be derived from Theorem~\ref{}. First Comment plonger les arbres de $\trees \rGamma$ dans le framework de Schlingloff. Soit $b$ l'arite maximale des elements de $\rGamma$. On denote par $\overline{\rGamma}$ le (unranked) set underlying $\rGamma$.
%%Il y a un plongement naturel
%%$$ \overline{\bullet}: \trees\rGamma \to \trees_b\Gamma$$
%\paragraph*{Encoding our trees by Schlingloff's trees}
%\paragraph*{Translating first-order formulas}
%\begin{lemma} Let $\rGamma$ be a ranked set and $\phi$ be a first-order formula.
%\forall t\in \trees \rGamma, \qquad t\models \phi \leftrightarrow t \models [\phi]
%\paragraph*{From 4-CLT to 2-CTL}
% \begin{lemma} Let $\rGamma$ be a ranked set and $\phi$ be a first-order formula.
%\forall t\in \trees \rGamma, \qquad t\models \overline{\phi} \leftrightarrow [t] \models \phi
\subsection{First-order relabelling are derivable}\label{sec:relabeling}
To show Proposition~\ref{prop:forat}, saying that first-order relabelling are derivable, we will show that each function appearing in Lemma~\ref{lem:schlingloff} and corresponding to each operator of 2-CTL is derivable. This is the role of Lemmas\ref{lem:nextmod}--\ref{lem:sincemod} presented below.
\begin{lemma}\label{lem:nextmod}
For every finite $\rSigma$, $\rGamma\subseteq \rSigma$ and $i \in \set{1,2,\ldots}$, the characteristic function $\ranked{f:\tmonad \rSigma\to\tmonad(\rSigma+\rSigma)}$ of the  unary query
\begin{align*}
\text{``The }i\text{-th child of }x\text{ is in }\rGamma\text{''}
\end{align*}
is derivable.
\end{lemma}
\begin{proof}
To show that $\ranked{f}$ is derivable, we start applying the children function \begin{align*}
\ranked{\mathsf{Children}:\tmonad\rSigma\to \tmonad (\rSigma\product (\rSigma_0+0)^*)}
\end{align*} from Example~\ref{ex:sibling} which tags every nodes by the list of its children. Consider the function $g$
\ranked{g:}  \ranked{\rSigma\product (\rSigma_0+0)^*} &\ranked{\to}& \ranked{\Sigma +\Sigma}&\\
\tensorpair{a,l}                           &
\mapsto& \tensorpair{a,1}              &\text{if } l[i]\in\ranked{\rGamma_0}, \\
&   \mapsto& \tensorpair{a,2} &\text{otherwise.}
\end{array}$$
which maps an element of $\rSigma$ tagged by a list to the first copy of $\rSigma$ if the $i$-th element of the list is in $\rGamma$ and to the second copy otherwise. The function $g$ is derivable since its domain is finite.
We finally get $\ranked{f}$ by lifting $\ranked{g}$ to terms.
\end{proof}

\medskip
\begin{lemma}\label{lem:untilmod}
For every finite $\rGamma, \rDelta \subseteq \rSigma$,  the characteristic function $\ranked{f:\tmonad\rSigma\to\tmonad(\rSigma+\rSigma)}$ of the unary query
\begin{align*}
\underbrace{\exists y\ y \geq x \land \rDelta(y) \land  \forall z \ (x < z < y \Rightarrow \rGamma(z)).}_{\substack{\text{$x$ has a descendant $y$ with label in $\rDelta$, such that}\\ \text{all nodes between $x$ and $y$ have label in $\rGamma$}}}
\end{align*}
is derivable.
\end{lemma}
\begin{proof}
We start by applying the factorization
\begin{align*}
\ranked{\ancfact : \tmonad \Sigma \to \tmonad(\tmonad(\Sigma\setminus(\Gamma\cup\Delta)) +\tmonad(\Gamma\cup\Delta))}
\end{align*}
which decomposes our terms into factors, depending on whether their node labels are in $\ranked{\Gamma\cup\Delta}$ or not.
Note that the value of a node w.r.t. the until query depends only on the node labels of its factor. %(it is constant equal to $0$ in the case of $\Sigma\setminus(\Gamma\cup\Delta)$ blocks).

The nodes of the $\ranked{\tmonad(\rSigma\setminus(\rGamma\cup\rDelta))}$ factors do not satisfy the query, thus we will apply to them the function $\ranked{\tmonad g}$ obtained by lifting the function
\ranked{g:}& \ranked{\rSigma\setminus(\rGamma\cup\rDelta)}& \ranked{\to} &\ranked{\rSigma+\rSigma}\\
&a&\mapsto& \tensorpair{a,2}.
\end{array}$$

Nodes of the $\ranked{\tmonad(\Gamma\cup\Delta)}$  factors satisfy the query if and only if they have a descendant in  $\rDelta$.
Consider the function $\ranked{h}$ obtained by composing the descendant function $\ranked{\mathsf{Descendant}_\Delta}$ from Example~\ref{ex:descendant} with an injection $\ranked{\tmonad(\iota+\iota)}$
\begin{align*}
\underbrace{\ranked{\tmonad(\Gamma\cup\Delta) \xrightarrow{\ranked{\mathsf{Descendant}_\Delta}} \tmonad(\Gamma\cup\Delta+\Gamma\cup\Delta) \xrightarrow{\ranked{\tmonad(\iota+\iota)}}\tmonad(\Sigma+\Sigma)}}_{\ranked{h}}
\end{align*}
Finally, to get the characteristic function $\ranked{f}$, we apply $\ranked{\tmonad{g}}$ to the $\ranked{\tmonad(\Sigma\setminus(\Gamma\cup\Delta))}$ factors and $\ranked{h}$ to the other factors using the co-pairing combinator, then we flat the obtained term.
\end{proof}

\begin{lemma}\label{lem:sincemod}
For every finite $\rGamma, \rDelta \subseteq \rSigma$,    the characteristic function of the unary query
\begin{align*}
\underbrace{\exists y\ y \leq x \land \rDelta(y) \land  \forall z \ (y < z < x \Rightarrow \rGamma(z)).}_{\substack{\text{$x$ has a descendant $y$ with label in $\rDelta$, such that}\\ \text{all nodes strictly between $x$ and $y$ have label in $\rGamma$}}}
\end{align*}
is derivable.
\end{lemma}
\begin{proof}
The same proof as above, one only needs to replace the use of the function $\ranked{\mathsf{Descendant}_\Delta}$ by that of $\ranked{\mathsf{Ancestor}_\Delta}$, introduced in Example~\ref{ex:descendant}.
\end{proof}

\section{Proof of Theorem~\ref{thm:stt}}
\label{sec:stt-appendix}
In this part of the appendix, we prove Theorem~\ref{thm:stt}, which says that every first-order tree-to-tree transduction is recognised by a register transducer.

According to Definition~\ref{def:fo-transduction}, a first-order transductions is a composition of any number of functions each of which is either  copying (item 1) or a non-copying first-order transduction (item 2). In other words:
\text{first-order transductions} \\ \eqdef (\text{copying} \cup \text{(non-copying first-order transductions)})^*
\end{array}$$
where the star denotes closure under composition. Although register transducers are closed under composition, this is not very   easy to show directly, and therefore we begin by simplifying the function composition in the definition of first-order transductions.  It is not hard to see that copying commutes with non-copying first-order transductions in the following sense:
\begin{align*}
\text{copying} \circ  \text{(non-copying first-order transductions)}  \\ \subseteq   \text{(non-copying first-order transductions)} \circ \text{copying}.
\end{align*}
Furthermore, since the class of copying functions is closed under composition, and the same is true for non-copying first-order transductions, we get the following normal form of first-order transductions:
\text{first-order transductions} \\=  \text{(non-copying first-order transductions)} \circ \text{copying}.
\end{array}$$
Therefore, in order to prove Theorem~\ref{thm:stt}, it suffices to show that a register transducer can compute any function which first copies the nodes of the input tree a fixed number of times, and then applies a non-copying first-order transduction.
% To make notation lighter, we ignore the copying, and only show that register transducers can simulate non copying first-order transductions. The proof with copying follows the same lines.

For the rest of this section, fix  a tree-to-tree function
\begin{align*}
f : \trees \rSigma \to \trees \rGamma
\end{align*}
which is a composition of first copying (some fixed number of times), followed by a non-copying first-order transduction. We will show that $f$ is computed by some register transducer.

\newcommand{\origin}[1]{\mathrm{origin}_{#1}}
\newcommand{\orcol}[2]{\mathrm{orcol}_{#1}^{#2}}
In the proof, we use the origin information associated to $f$, i.e.~how nodes of the output tree can be traced back to nodes in the input tree. For an input tree $t \in \trees \rSigma$, define its origin map
to be the function of type
\begin{align*}
\text{nodes in $f(t)$} \to \text{nodes in $t$}
\end{align*}