LIP, École Normale Supérieure de Lyon, France and
https://nguyentito.eu/nltd@nguyentito.euhttps://orcid.org/0000-0002-6900-5577Supported
by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the
program Investissements d’Avenir (ANR-11-IDEX-0007) operated by the French
National Research Agency (ANR).IRIF, CNRS, Université Paris Cité, France and
<EMAIL_ADDRESS>by the
ANR project PPS: ANR-19-CE48-0014 and by the European Union’s Horizon 2020
research and innovation programme under the Marie Sklodowska-Curie grant
agreement No 101034255. [500]Theory of computation Linear logic [500]Theory of
computation Transducers

###### Acknowledgements.

0

# (Almost) Affine Higher-Order Tree Transducers

Lê Thành Dũng (Tito) Nguyễn  Gabriele Vanoni

###### Abstract

We investigate the tree-to-tree functions computed by affine
$\lambda$-transducers: tree automata whose memory consists of an affine
$\lambda$-term instead of a finite state. They can be seen as variations on
Gallot, Lemay and Salvati’s Linear High-Order Deterministic Tree Transducers.
When the memory is almost purely affine (à la Kanazawa), we show that these
machines can be translated to tree-walking transducers (and with a purely
affine memory, we get a reversible tree-walking transducer). This leads to a
proof of an inexpressivity conjecture of Nguyễn and Pradic on implicit
automata in an affine $\lambda$-calculus. The key technical tool in our proofs
is the Interaction Abstract Machine (IAM), an operational avatar of the
geometry of interaction semantics of linear logic. We work with ad-hoc
specializations to (almost) affine $\lambda$-terms of a tree-generating
version of the IAM.

###### keywords:

lambda-calculus, geometry of interaction, tree-walking automata

###### category:

##  1 Introduction

This paper investigates the expressive power of two kinds of _tree
transducers_ : automata computing tree-to-tree functions. This is a topic with
a long history, and many equivalences between machine models are already
known. For instance, the class of monadic second-order transductions111 We
consider only tree-to-tree transductions here, but there is a rich theory of
MSOTs between graphs, or between arbitrary relational structures, cf. [12].
See also [7] for a history of MSO transductions. In the well-studied special
case of string functions, MSOTs are called regular functions, cf. [30].
(MSOTs), whose name refers to a definition by logic, is also captured by
various tree transducer models (e.g. [17]) or by a system of primitive
functions and combinators [10]. This class is closed under composition, and
includes functions such as:

mirror and add a $d$ above each $b$: $\displaystyle\quad a(b(c),c)\mapsto
a(c,d(b(c)))$ relabel each $c$ by parity of its depth: $\displaystyle\quad
a(b(c),c)\mapsto a(b(0),1)$ count number of non-$a$ nodes in unary:
$\displaystyle\quad a(b(c),c)\mapsto S(S(S(0)))$

Some machines for MSOTs, such as the restricted macro tree transducers222Which
are very similar to some other transducer models for MSOTs: the bottom-up
ranked tree transducers of [4, Sections 3.7–3.8] and to the register tree
transducers of [10, Section 4]. of [18], involve _tree contexts_ as data
structures used in their computation. A tree context is a tree with holes at
some leaves – for example $b(a(c,a(\langle\cdot\rangle{},c)))$ – and these
holes are meant to be substituted by other trees. Thus, it represents a simple
function taking trees to trees: these transducers use functions as data. From
this point of view, in the spirit of functional programming, it also makes
sense to consider transducers manipulating _higher-order data_ , that is,
functions that may take functions as arguments (a function of order $k+1$
takes arguments of order at most $k$). This idea goes back to the 1980s [20]
(cf. LABEL:rem:hltt-mtt), and a recent variant by Gallot, Lemay and Salvati
[21, 22] computes exactly the tree-to-tree MSOTs.

### Linear/affine $\lambda$-calculus for MSOTs.

Gallot et al. [21, 22] use the _$\lambda$ -calculus_ to represent higher-order
data, and in order to control the expressive power, they impose a _linearity_
restriction on $\lambda$-terms. In programming language theory, a _linear_
function uses its argument _exactly once_ , while an _affine_ function must
use its argument _at most once_ – affineness thus mirrors the single-use
restrictions that appear in various tree transducer models [6, 18, 4, 10].

An independent but similar characterization of MSOTs appeared around the same
time in Nguyễn and Pradic’s work on implicit automata [33, 31]. In an
analogous fashion to how the untyped $\lambda$-calculus can be used as a
Turing-complete programming language, they consider typed $\lambda$-terms seen
as standalone programs. For a well-chosen type system – which enforces a
linearity restriction – and input/output convention, it turns out that the
functions computed by these $\lambda$-terms are exactly the MSO tree
transductions [31, Theorem 1.2.3].

In fact, the proof of [31, Theorem 1.2.3] introduces, as an intermediate step,
a machine model – the single-state $\mathfrak{L}$-BRTTs of [31, Section 6.4] –
that uses $\lambda$-terms as memory to capture the class of MSOTs. Clearly,
this device is very close to the tree transducer model of Gallot et al. Yet
there are also important differences between the two: they can be understood
as two distinct ways of extending what we call purely linear
$\lambda$-transducers, as we will explain. Actually, to avoid some
uninteresting pathologies (cf. [31, Theorem 7.0.2]), we shall prefer to work
with affine $\lambda$-transducers instead.

######  Example 1.1.

Purely affine $\lambda$-transducers will be properly defined later, but for
now, for the sake of concreteness, let us exhibit one such transducer. It
takes input trees with binary $a$-labeled nodes, unary $b$-labeled nodes and
$c$-labeled leaves, and is specified by the $\lambda$-terms:

$t_{a}=\lambda\ell.\;\lambda r.\;\lambda x.\;\ell\;(r\;x)\qquad t_{b}=\lambda
f.\;\lambda x.\;S\;(f\;x)\qquad t_{c}=S\qquad u=\lambda f.\;f\;0$

where $S$ and $0$ are constants from the output alphabet. The input
$a(b(c),c)$ is then mapped to $u\;(t_{a}\;(t_{b}\;t_{c})\;t_{c})$ which
evaluates to the normal form $S\;(S\;(S\;0))$. So this $\lambda$-transducer
computes the aforementioned number of non-$a$ nodes written in unary function.
(It actually is purely linear: each bound variable has exactly one
occurrence.)

The issue with this transducer model is its lack of expressiveness, as shown
by the following consequence of our results, which settles an equivalent333A
routine syntactic analysis akin to [33, Lemma 3.6] shows that it is indeed
equivalent. Note that the results of [33] are indeed about affine, not linear,
$\lambda$-calculi. conjecture on implicit automata that had been put forth by
Nguyễn and Pradic in [33, Section 5.3]. (We will come back in Remark 7.1 to
how they overcome this to characterize tree-to-tree MSO transductions.)

######  Corollary 1.2 (of Theorem 1.4 below).

There exists a regular tree444This phenomenon depends on using trees as
inputs. Over strings, purely affine $\lambda$-terms can be used to recognize
any regular language [33, Theorem 5.1]. language whose indicator function
cannot be computed by any purely affine $\lambda$-transducer.

Gallot et al. avoid this limitation by extending the transducer model with
common automata-theoretic features. They then show [22, Chapter 7] that the
usual linear $\lambda$-terms leads to the previously mentioned
characterization of MSOTs, while relaxing the linearity condition to use
almost linear $\lambda$-terms (in the sense of Kanazawa [25], who also studied
the almost affine case in [24]) yields the larger class of MSOTs with
sharing555An MSOT-S can be decomposed as an MSO tree-to-graph transduction
(Footnote 1), that produces a rooted directed acyclic graph (DAG), followed by
the unfolding of this graph into a tree. The rooted DAG is a compressed
representation of the output tree with some sharing of subtrees. (MSOT-S).

### Flavors of affine types.

We shall work with an affine type system that allows some data to be marked as
duplicable via the exponential modality ‘$!$’. The grammar of types is thus
$A,B\mathrel{\mathrel{\mathop{\mathchar 58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=}o\mathrel{|}A\multimap B\mathrel{|}\oc A$ – the connective
$\multimap$ is the affine function arrow.

The point is to allow us to restrict duplication by means of syntactic
constraints on ‘!’.

######  Definition 1.3.

A _purely affine_ type does not contain any ‘!’, i.e. is built from $o$ and
$\multimap$.

A type is said to be _almost purely affine_ when the only occurrences of ‘!’
are applied to $o$. In particular, every purely affine type is almost purely
affine.

For example, $(o\multimap\oc o)\multimap\oc o$ is almost purely affine but not
$\oc(o\multimap o)$.

The latter definition is motivated by the aforementioned almost affine
$\lambda$-terms [24], which allow the variables of base type $o$ to be used
multiple times, e.g. $\lambda y.\;\lambda f.\;\lambda g.\;(\lambda
x.\;f\;x\;x)\;(g\;y\;y)$ is almost affine (and even almost linear) for
$x\mathrel{\mathop{\mathchar 58\relax}}o$ and $y\mathrel{\mathop{\mathchar
58\relax}}o$. Inconveniently, almost linear/affine $\lambda$-terms are not
closed under $\beta$-reduction, as remarked in [24, §4]. For instance, the
previous term reduces to $\lambda y.\;\lambda f.\;\lambda
g.\;f\;(g\;y\;y)\;(g\;y\;y)$ which uses $g\mathrel{\mathop{\mathchar
58\relax}}o\multimap o\multimap o$ twice. The ‘$\oc$’ modality provides a
convenient way to realize a similar idea while avoiding this drawback.

Each $\lambda$-transducer has in its definition a _memory type_ , which is for
instance $o\multimap o$ for Example 1.1. We extend Definition 1.3 to
$\lambda$-transducers: a $\lambda$-transducer is purely (resp. almost purely)
affine when its memory type is purely (resp. almost purely) affine.

### Contributions.

First, we study (almost) purely affine $\lambda$-transducers, relating them to
yet another machine model: _tree-walking tree transducers_ , see e.g. [17].
Those are devices with a finite-state control and a reading head moving around
the nodes of the input tree; in one step, the head can move to the parent or
one of the children of the current node.

######  Theorem 1.4.

Writing $\subseteq$ for a comparison in expressive power, we have:

purely affine $\lambda$-transducer $\displaystyle\subseteq\text{reversible
tree-walking transducer}$ almost purely affine $\lambda$-transducer
$\displaystyle\subseteq\text{tree-walking transducer}$

Corollary 1.2 then follows immediately from a result of Bojańczyk and
Colcombet [9]: there exists a regular tree language not recognized by any
tree-walking automaton.

We also obtain characterizations of MSOTs and of MSOT-Ss, by preprocessing the
input with an _MSO relabeling_ – a special kind of MSOT that can only change
the node labels in a tree, but keeps its structure as it is. Morally, this
preprocessing amounts to the same thing as the automata-theoretic features –
finite states and regular look-ahead – used in [21, 22].

######  Theorem 1.5.

Using $\equiv$ to denote an equivalence in expressive power, we have:

$\displaystyle\text{purely affine $\lambda$-transducer}\circ\text{MSO
relabeling}$ $\displaystyle\equiv\text{MSOT}$ $\displaystyle\text{almost
purely affine $\lambda$-transducer}\circ\text{MSO relabeling}$
$\displaystyle\equiv\text{MSOT-S}$

This should be informally understood as a mere rephrasing of the results of
Gallot et al., except with affine rather than linear $\lambda$-terms. On a
technical level, we derive our right-to-left inclusions from their results;
there turns out to be a minor mismatch, and working with affineness rather
than linearity proves convenient to overcome it. As for the left-to-right
inclusions, we get them as corollaries of Theorem 1.4.

### Key tool: the Interaction Abstract Machine (IAM).

To translate $\lambda$-transducers into tree-walking or invisible pebble tree
transducers, we use a mechanism that evaluates a $\lambda$-term using a
pointer to its syntax tree that is moved by local steps – just like a tree-
walking reading head. This mechanism, called the Interaction Abstract Machine,
was derived from a family of semantics of linear $\lambda$-calculi known as
geometry of interaction – cf. [36, Chapter 3] for more on its history. Our
approach thus differs from both the proofs of Gallot et al. in [22], which go
through a syntactic procedure for lowering the order of $\lambda$-terms, and
those of Nguyễn and Pradic in [31], which rely on another kind of denotational
semantics.

The IAM satisfies a well-known _reversibility_ property, see e.g. [36,
Proposition 3.3.4] – it even appears in the title of the seminal paper [13].
In the purely affine case, this gives us reversible tree-walking transducers
in Theorem 1.4 – these have not appeared explicitly in the literature, but we
define them similarly to the existing reversible graph-walking automata [34]
and reversible two-way string transducers [14]. In the almost purely affine,
we use an ad-hoc optimization of the IAM that breaks reversibility.

### Preliminaries on trees.

A _ranked alphabet_ $\Sigma$ is a finite set with a rank (or arity)
$\mathrm{rk}(c)\in\mathbb{N}=\\{0,1,\dots\\}$ associated to each letter
$c\in\Sigma$. It can be seen as a first-order signature of function symbols,
and by a _tree_ over $\Sigma$ we mean a closed first-order term over this
signature. For instance, the set $\mathrm{Tree}(\\{a\mathrel{\mathop{\mathchar
58\relax}}2,\;b\mathrel{\mathop{\mathchar
58\relax}}1,\;c\mathrel{\mathop{\mathchar 58\relax}}0\\})$ consists of trees
with binary $a$-labeled nodes, unary $b$-labeled nodes and $c$-labeled leaves,
e.g. $a(b(c),c)$ or $b(a(a(c,c),c))$.

It will also be convenient to work with the sets
$\mathrm{Tree}(\Sigma,X)=\mathrm{Tree}(\Sigma\cup\\{x\mathrel{\mathop{\mathchar
58\relax}}0\mid x\in X\\})$ of trees over the ranked alphabet $\Sigma$ with
the additional possibility of having $X$-labeled leaves.

### Appendix.

This is a preliminary arXiv preprint. The submission will be updated with the
technical appendix soon.

##  2 Affine $\lambda$-terms and tree-to-tree $\lambda$-transducers

The grammar of our $\lambda$-terms, where $a$ ranges over constants and $x$
over variables, is

$t,u\mathrel{\mathrel{\mathop{\mathchar 58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=}a\mathrel{|}x\mathrel{|}\lambda
x.\;t\mathrel{|}t\;u\mathrel{|}\oc{t}\mathrel{|}\mathtt{let}\ \oc x=u\
\mathtt{in}\ t$

These $\lambda$-terms are considered up to renaming of bound variables
($\lambda x.\;t$ binds $x$ in $t$, while $\mathtt{let}\ \oc x=u\ \mathtt{in}\
t$ binds $x$ in $t$ but not in $u$). We will also use _contexts_ with one hole
$\langle\cdot\rangle$, for example $C=\lambda x.\;t\;\langle\cdot\rangle$, in
which $\lambda$-terms can be plugged (we have $C\langle u\;v\rangle=\lambda
x.\;t\;(u\;v)$).

The linear logic tradition calls a term of the form $\oc{t}$ a _box_ , and the
number of nested boxes surrounding a subterm of some term is called its
_depth_ within this term. Similarly, the _depth of a (one-hole) context_ $C$
is defined to be the number of boxes surrounding the hole
$\langle\cdot\rangle$.

### Typing rules.

Our type system is a variant of Dual Intuitionistic Linear Logic [5], with
weakening to make it affine. As already said, our grammar of types is
$A,B\mathrel{\mathrel{\mathop{\mathchar 58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=}o\mathrel{|}A\multimap B\mathrel{|}\oc A$. As usual, $\multimap$
is right-associative: the parentheses in $A\multimap(B\multimap C)$ can be
dropped.

The typing contexts are of the form (unrestricted variables) | (affine variables). In the rules below, a comma between two sets of typed affine variables denotes a disjoint union; this corresponds to prohibiting the use of the same affine free variable in two distinct subterms.

$\frac{}{\Theta\mid\Phi,x\mathrel{\mathop{\mathchar 58\relax}}A\vdash
x\mathrel{\mathop{\mathchar
58\relax}}A}\qquad\frac{\Theta\mid\Phi,x\mathrel{\mathop{\mathchar
58\relax}}A\vdash t\mathrel{\mathop{\mathchar
58\relax}}B}{\Theta\mid\Phi\vdash\lambda x.\;t\mathrel{\mathop{\mathchar
58\relax}}A\multimap B}\qquad\frac{\Theta\mid\Phi\vdash
t\mathrel{\mathop{\mathchar 58\relax}}A\multimap
B\quad\Theta\mid\Phi^{\prime}\vdash u\mathrel{\mathop{\mathchar
58\relax}}A}{\Theta\mid\Phi,\Phi^{\prime}\vdash t\;u\mathrel{\mathop{\mathchar
58\relax}}B}$ $\frac{}{\Theta,x\mathrel{\mathop{\mathchar
58\relax}}A\mid\Phi\vdash x\mathrel{\mathop{\mathchar
58\relax}}A}\qquad\frac{\Theta\mid\varnothing\vdash
t\mathrel{\mathop{\mathchar 58\relax}}A}{\Theta\mid\varnothing\vdash\oc
t\mathrel{\mathop{\mathchar 58\relax}}\oc A}\qquad\frac{\Theta\mid\Phi\vdash
u\mathrel{\mathop{\mathchar 58\relax}}\oc
A\quad\Theta,x\mathrel{\mathop{\mathchar 58\relax}}A\mid\Phi^{\prime}\vdash
t\mathrel{\mathop{\mathchar
58\relax}}B}{\Theta\mid\Phi,\Phi^{\prime}\vdash\mathtt{let}\ \oc x=u\
\mathtt{in}\ t\mathrel{\mathop{\mathchar 58\relax}}B}$

We also work with constants whose types are fixed in advance. Fixing
$a\mathrel{\mathop{\mathchar 58\relax}}A$ means that we have the typing rule
$\overline{\Theta\mid\Phi\vdash a\mathrel{\mathop{\mathchar 58\relax}}A}$. We
shall also abbreviate $\varnothing\mid\varnothing\vdash
t\mathrel{\mathop{\mathchar 58\relax}}A$ as $t\mathrel{\mathop{\mathchar
58\relax}}A$.

######  Claim 1 (Affineness).

If $\lambda x.\;t$ is well-typed, the variable $x$ occurs at most once in $t$,
at depth 0. (But let-bound variables are not subject to any such restriction).

### Normalization.

Our $\beta$-reduction rules are as follows, where the context $L$ consists of
a succession of let-binders (i.e. $L\mathrel{\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=}\langle\cdot\rangle\mid\mathtt{let}\ \oc x^{\prime}=t^{\prime}\
\mathtt{in}\ L$):

$L\langle\lambda x.\;t\rangle\;u\longrightarrow_{\beta}L\langle
t\\{x\mathrel{\mathop{\mathchar
58\relax}}=u\\}\rangle\qquad\qquad\mathtt{let}\ \oc x=L\langle\oc u\rangle\
\mathtt{in}\ t\longrightarrow_{\beta}L\langle t\\{x\mathrel{\mathop{\mathchar
58\relax}}=u\\}\rangle$

For instance, the following is a valid $\beta$-reduction:

$(\mathtt{let}\ \oc x=u\ \mathtt{in}\ \mathtt{let}\ \oc y=v\ \mathtt{in}\
\lambda z.\;z\;x\;y)\;t\quad\longrightarrow_{\beta}^{*}\quad\mathtt{let}\ \oc
x=u\ \mathtt{in}\ \mathtt{let}\ \oc y=v\ \mathtt{in}\ t\;x\;y$

This reduction at a distance – an idea of Accattoli & Kesner [1] – is a way to
get the desirable Proposition 2.3 below without having to introduce cumbersome
commuting conversions. For an extended discussion in the context of a system
very close to ours, see [28, §1.2.1].

######  Proposition 2.1 (Normalization and subject reduction).

Any well-typed term has a $\beta$-normal form. Furthermore, if
$\Theta\mid\Phi\vdash t\mathrel{\mathop{\mathchar 58\relax}}A$ then
$\Theta\mid\Phi\vdash t^{\prime}\mathrel{\mathop{\mathchar 58\relax}}A$ for
any $\beta$-normal form $t^{\prime}$ of $t$.

######  Definition 2.2.

We say that a term is purely affine when _all of its subterms_ have purely
affine types (cf. Definition 1.3) which implies that it contains no !-box or
let-binding. We also call almost purely affine the terms in which, for every
subterm $t$,

  * •

the type of $t$ is almost purely affine ,

  * •

if $t=\oc u$ then $u$ is purely affine.

######  Proposition 2.3.

Assume that we work with purely affine constants, as will always be the case
in this paper. Let $\Theta\mid\Phi\vdash t\mathrel{\mathop{\mathchar
58\relax}}A$ and _suppose $t$ is in normal form_. If $A$ and the types in
$\Theta$ and $\Phi$ are purely affine (resp. almost purely affine), then so is
$t$.

For example, $\mathtt{let}\ \oc z=\oc(\lambda x.\;x)\ \mathtt{in}\
z\mathrel{\mathop{\mathchar 58\relax}}o\multimap o$ is not purely affine but
its normal form $\lambda x.\;x$ is.

### Encoding of trees in our affine $\lambda$-calculus.

Fix a ranked alphabet $\Sigma$. We consider $\lambda$-terms built over the
constants $c\mathrel{\mathop{\mathchar 58\relax}}o^{\mathrm{rk}(c)}\multimap
o$ for $c\in\Sigma$. There is a canonical encoding $\widetilde{(\,\cdot\,)}$
of trees as closed terms of type $o$; for instance, $\tau=a(b(c),c)$ is
encoded as $\widetilde{\tau}=a\;(b\;c)\;c$.

######  Proposition 2.4.

Every closed term _of type $o$_ using these constants admits a _unique_ normal
form. Furthermore, $\widetilde{(\,\cdot\,)}$ is a _bijection_ between
$\mathrm{Tree}(\Sigma)$ and these normal forms.

Given a type $A$ and a family of $\lambda$-terms
$\vec{t}=(t_{c})_{c\in\Sigma}$ such that $t_{c}\mathrel{\mathop{\mathchar
58\relax}}A^{\mathrm{rk}(c)}\multimap A$ for each letter $c\in\Sigma$, we
write $\widehat{\tau}(\vec{t})$ for the result of replacing each constant $c$
in $\widetilde{\tau}$ by $t_{c}$. It is always well typed, with type $A$. For
the example $\tau=a(b(c),c)$, we have
$\widehat{\tau}((t_{x})_{x\in\\{a,b,c\\}})=t_{a}\;(t_{b}\;t_{c})\;t_{c}$.

### Higher-order transducers (or $\lambda$-transducers).

Let us fix an input ranked alphabet $\Gamma$.

######  Definition 2.5.

An _(affine) $\lambda$-transducer_
$\mathrm{Tree}(\Gamma)\rightarrow\mathrm{Tree}(\Sigma)$ is specified by a
_memory type_ $A$ and a family of terms (that can use the aforementioned
constants from $\Sigma$):

$\underbrace{t_{a}\mathrel{\mathop{\mathchar
58\relax}}A^{\mathrm{rk}(a)}\multimap A}_{\mathclap{\text{\enquote{transition
terms}}}}\ \text{for each letter}\
a\in\Gamma\qquad\text{and}\qquad\underbrace{u\mathrel{\mathop{\mathchar
58\relax}}A\multimap o}_{\mathclap{\text{\enquote{output term}}}}$

The $\lambda$-transducer defines the function

$\tau\in\mathrm{Tree}(\Gamma)\quad\mapsto\quad\underbrace{\sigma\in\mathrm{Tree}(\Sigma)\
\text{such that}\ \widetilde{\sigma}\ \text{is the normal form of}\
\overbrace{u\;\widehat{\tau}((t_{a})_{a\in\Gamma})}^{\mathclap{\text{well-
typed with type $o$}}}}_{\mathclap{\text{well-defined and unique thanks to
\lx@cref{creftypecap~refnum}{prop:encoding}}}}$

This amounts to specifying a structurally recursive function over
$\mathrm{Tree}(\Gamma)$ with return type $A$, followed by some post-processing
that produces an output tree. Alternatively, a $\lambda$-transducer can be
seen as a kind of tree automaton whose memory consists of affine
$\lambda$-terms of some type $A$ (with constants from $\Sigma$) and whose
bottom-up transitions are also defined by $\lambda$-terms.

In addition to the purely affine Example 1.1, we exhibit also an almost purely
affine $\lambda$-transducer.

######  Example 2.6.

The following almost affine $\lambda$-transducer maps
$S^{n}(0)=S(\dots(S(0)))$ to the list $[1,2,\dots,n]$, encoded as the tree
$\mathtt{cons}(S(0),\dots(\mathtt{cons}(S^{n}(0),\mathtt{nil})\dots)$.

$\displaystyle t_{0}$ $\displaystyle=\lambda
x.\;\mathtt{nil}\mathrel{\mathop{\mathchar 58\relax}}\oc o\multimap o\
\text{(memory type)}\qquad\qquad\qquad u=\lambda g.\;g\;\oc(S\;0)$
$\displaystyle t_{S}$ $\displaystyle=\lambda g.\;\lambda x.\;\mathtt{let}\ \oc
y=x\ \mathtt{in}\ \mathtt{cons}\;y\;(g\;\oc(S\;y))$

##  3 Tree-walking transducers (last definitions needed for Theorem 1.4)

### Generalities.

In this paper, we shall encounter several machine models that generate some
output tree in a top-down fashion, starting from the root. (This is not the
case of $\lambda$-transducers.) They follow a common pattern, which we
abstract as a lightweight formalism here: essentially, a deterministic regular
tree grammar with infinitely many non-terminals.

######  Remark 3.1.

Engelfriet’s tree grammars with storage (see for instance [16]) are more
complex formalisms that also attempt to unify several definitions of tree
transducer models.

######  Definition 3.2.

A _tree-generating machine_ over the ranked alphabet $\Sigma$ consists of:

  * •

a (possibly infinite) set $\mathcal{K}$ of _configurations_ ;

  * •

an _initial configuration_ $\kappa_{0}\in\mathcal{K}$ – in concrete instances,
$\kappa_{0}$ will be defined as a simple function of some input tree (for tree
transducers) or some given $\lambda$-term (for the IAM);

  * •

a _computation-step (partial) function_
$\mathcal{K}\rightharpoonup\mathrm{Tree}(\Sigma,\mathcal{K})$.

######  Example 3.3.

To motivate the formal semantics for these machines that we will soon define,
we give a tree-generating machine that is meant to produce the list
$[1,2,\dots,n]$ (for an arbitrarily chosen $n\in\mathbb{N}$), encoded as in
Example 2.6.

  * •

The set of configurations is
$\mathcal{K}=\\{\mathsf{spine,num}\\}\times\mathbb{N}$ where $\mathsf{spine}$
and $\mathsf{num}$ are formal symbols.

  * •

The initial configuration is $(\mathsf{spine},n)$ – let us write this pair as
$\langle\mathsf{spine},n\rangle$.

  * •

The computation-step function is $\left\\{\begin{aligned}
\langle\mathsf{spine},0\rangle&\mapsto\mathtt{nil}\\\
\langle\mathsf{spine},m+1\rangle&\mapsto\mathtt{cons}(\langle\mathsf{num},n-m\rangle,\langle\mathsf{spine},m\rangle)\\\
\langle\mathsf{num},0\rangle&\mapsto 0\\\
\langle\mathsf{num},m+1\rangle&\mapsto
S(\langle\mathsf{num},m\rangle)\end{aligned}\right.$

For $n=3$, one possible run is

$\langle\mathsf{spine},3\rangle\rightsquigarrow\mathtt{cons}(\langle\mathsf{num},1\rangle,\langle\mathsf{spine},2\rangle)\rightsquigarrow\mathtt{cons}(S(\langle\mathsf{num},0\rangle),\langle\mathsf{spine},2\rangle)\rightsquigarrow\dots$

All runs starting from $\langle\mathsf{spine},3\rangle$ eventually reach the
tree that encodes $[1,2,3]$.

Let us now discuss the general case. Intuitively, the execution of the machine
involves spawning several independent concurrent processes, outputting
disjoint subtrees. We formalize this parallel computation as a rewriting
system $\rightsquigarrow$ on $\mathrm{Tree}(\Sigma,\mathcal{K})$: we have
$\tau_{1}\rightsquigarrow\tau_{2}$ whenever $\tau_{2}$ is obtained from
$\tau_{1}$ by substituting one of its configuration leaves by its image by the
computation-step function. This rewriting system is orthogonal, and therefore
confluent, which means that the initial configuration has at most one normal
form. If this normal form exists and belongs to $\mathrm{Tree}(\Sigma)$, it is
the output of the machine; we then say that the machine converges. Otherwise,
the output is undefined; the machine diverges.

### Tree-walking transducers.

Before giving the definition, let us see a concrete example.

######  Example 3.4.

According to this theorem, since the $\lambda$-transducer of Example 1.1 is
purely affine, the function count non-$a$ nodes that it defines can also be
computed by some (reversible) tree-walking transducer. We show the run of such
a transducer on the input $a_{1}(b_{2}(c_{3}),c_{4})$ – the indices are not
part of the node labels, they serve to distinguish positions:

$\displaystyle(q,\circlearrowleft,a_{1})$
$\displaystyle\rightsquigarrow(q,\downarrow_{\bullet},b_{2})\rightsquigarrow
S((q,\downarrow_{\bullet},c_{3}))\rightsquigarrow
S(S((q,\uparrow_{1}^{\bullet},b_{2})))\rightsquigarrow
S(S((q,\uparrow_{1}^{\bullet},a_{1})))$ $\displaystyle\rightsquigarrow
S(S((q,\downarrow_{\bullet},c_{4})))\rightsquigarrow
S(S(S((q,\uparrow_{2}^{\bullet},a_{1})))))\rightsquigarrow S(S(S(0)))$

where $q$ is the single state of the transducer. The second component records
the provenance, i.e. the previous position of the tree-walking transducer
relatively to the current node (stored in the third component):
$\downarrow_{\bullet}$ refers to its parent, $\circlearrowleft$ to itself, and
$\uparrow_{i}^{\bullet}$ to its $i$-th child.

######  Definition 3.5.

A _tree-walking transducer (TWT)_
$\mathrm{Tree}(\Gamma)\rightharpoonup\mathrm{Tree}(\Sigma)$ consists of:

  * •

a finite set of _states_ $Q$ with an _initial state_ $q_{0}\in Q$

  * •

a family of (partial) _transition functions_ for $a\in\Gamma$

$\delta_{a}\colon
Q\times\\{\downarrow_{\bullet},\circlearrowleft,\uparrow_{1}^{\bullet},\dots,\uparrow_{k}^{\bullet}\\}\rightharpoonup\mathrm{Tree}(\Sigma,\;Q\times\\{\uparrow_{\bullet},\circlearrowleft,\downarrow^{\bullet}_{1},\dots,\downarrow^{\bullet}_{k}\\})\quad\text{where}\
k=\mathrm{rk}(a)$

  * •

a family of (partial) _transition functions at the root_ for $a\in\Gamma$

$\delta_{a}\colon
Q\times\\{\circlearrowleft,\uparrow_{1}^{\bullet},\dots,\uparrow_{k}^{\bullet}\\}\rightharpoonup\mathrm{Tree}(\Sigma,\;Q\times\\{\circlearrowleft,\downarrow^{\bullet}_{1},\dots,\downarrow^{\bullet}_{k}\\})\quad\text{where}\
k=\mathrm{rk}(a)$

The TWT associates to each input tree $\tau$ a tree-generating machine whose
output is the image of $\tau$. Its set of configurations is
$Q\times\\{\downarrow_{\bullet},\circlearrowleft,\uparrow_{1}^{\bullet},\dots\\}\times\\{\text{nodes
of}\ \tau\\}$ and its initial configuration of is
$(q_{0},\;\circlearrowleft,\;\text{root of $\tau$})$.

To define the image of $(q,p,v)$ by the computation-step function (it is
undefined if one of the following steps is undefined), we start with either
$\delta^{\mathrm{root}}_{a}(q,d)$ if $v$ is the root or $\delta_{a}(q,p)$
otherwise – where $a$ is the label of the node $v$ – then replace each
$(q^{\prime},p)\in Q\times\\{\uparrow_{\bullet},\dots\\}$ by

$\begin{cases}(q^{\prime},\;\downarrow_{\bullet},\;\text{$i$-th child of
$v$})&\text{if}\
d=\;\downarrow_{i}^{\bullet}\qquad\qquad\qquad\qquad\qquad\qquad\quad(q^{\prime},\circlearrowleft,v)\quad\text{if}\
d=\;\circlearrowleft\\\ (q^{\prime},\;\uparrow_{j}^{\bullet},\;\text{parent of
$v$})&\text{if}\ d=\;\uparrow_{\bullet}\ \text{and $v$ is the $j$-th child of
its parent}\end{cases}$

######  Example 3.6.

Using the idea of Example 3.3, we define a tree-walking transducer that
computes the function $n\mapsto[1,\dots,n]$ modulo encodings of Example 2.6.
Its set of states is $Q=\\{\mathsf{spine,num}\\}$, its initial state is
$\mathsf{spine}$ and its transitions are

$\displaystyle\delta^{\mathrm{root}}_{S}(\mathsf{spine},\circlearrowleft)$
$\displaystyle=\delta_{S}(\mathsf{spine},\downarrow_{\bullet})=\mathtt{cons}((\mathsf{num},\circlearrowleft),(\mathsf{spine},\downarrow^{\bullet}_{1}))$
$\displaystyle\delta_{S}(\mathsf{num},\circlearrowleft)$
$\displaystyle=\delta_{S}(\mathsf{num},\uparrow_{1}^{\bullet})=S((\mathsf{num},\uparrow_{\bullet}))$
$\displaystyle\delta^{\mathrm{root}}_{S}(\mathsf{num},\circlearrowleft)$
$\displaystyle=\delta^{\mathrm{root}}_{S}(\mathsf{num},\uparrow_{1}^{\bullet})=S(0)\qquad\qquad\delta^{\mathrm{root}}_{0}(\mathsf{spine},\circlearrowleft)=\delta_{0}(\mathsf{spine},\downarrow_{\bullet})=\mathtt{nil}$

######  Remark 3.7.

In the above example, the provenance information in
$\\{\downarrow_{\bullet},\dots\\}$ plays no role. On the contrary, it is
crucial in the former Example 3.4, where we have
$\delta_{a}^{\mathrm{root}}(q,\uparrow_{2}^{\bullet})=0$ and

$\delta_{a}^{\mathrm{root}}(q,\circlearrowleft)=\delta_{a}(q,\downarrow_{\bullet})=(q,\downarrow^{\bullet}_{1})\qquad\underbrace{\delta_{a}^{\mathrm{root}}(q,\uparrow_{1}^{\bullet})=\delta_{a}(q,\uparrow_{1}^{\bullet})=(q,\downarrow^{\bullet}_{2})}_{\mathclap{\text{\enquote{after
returning from the 1st child, the traversal starts visiting the 2nd
child}}}}\qquad\delta_{a}(q,\uparrow_{2}^{\bullet})=(q,\uparrow_{\bullet})$

In the definitions of tree-walking automata or transducers in the literature,
e.g. [9, 15, 17], transitions often do not have access to this provenance, but
instead they can depend on the child number $i$ the current node (such that
the node is an $i$-th child of its parent). One can easily simulate one
variant with the other; but if neither of these features were available, the
machine model would be strictly weaker [23, Theorem 5.5].

Our main motivation for using provenances instead of child numbers is that,
according to [34, Sections 5 and 6], being direction-determinate – i.e.
knowing which previous node the current configuration came from – is important
in the reversible case. This can indeed be observed in the proof of 2.
(Directed states are used in [14] for a similar reason.)

Let us say that a map $\delta\colon X\rightarrow\mathrm{Tree}(\Sigma,Y)$ is
_$Y$ -leaf-injective_ whenever in the family of trees $(\delta(x)\mid x\in
X)$, each $y\in Y$ occurs at most once: $y$ appears in at most one tree of the
family, and if it does appear, this tree has a single leaf with label $y$.

######  Definition 3.8.

A tree-walking transducer
$\mathrm{Tree}(\Gamma)\rightharpoonup\mathrm{Tree}(\Sigma)$ is _reversible_
when all maps $\delta_{a}$ and $\delta^{\mathrm{root}}_{a}$ for $a\in\Gamma$
are
$(Q\times\\{\uparrow_{\bullet},\circlearrowleft,\downarrow_{1}^{\bullet},\dots,\downarrow_{\mathrm{rk}(a)}^{\bullet}\\})$-leaf-
injective.

Example 3.4 is reversible, but not Example 3.6.

######  Claim 2 (The meaning of reversibility).

Fix a reversible tree-walking transducer and an input tree. Any configuration
$C$ has at most one predecessor configuration, i.e. one configuration
$C^{\prime}$ whose image by the computation-step function contains $C$ as a
leaf.

##  4 From the Interaction Abstract Machine to (reversible) TWTs

This section finally discusses the proof of Theorem 1.4. (For lack of space,
we focus on stating some key definitions and illustrating the ideas on
examples; rigorous details are left to the technical appendix.) By definition,
computing the image of an input tree by a $\lambda$-transducer involves
normalizing a $\lambda$-term. Unfortunately, iterating $\beta$-reductions
until a normal form is reached requires too much working memory to be
implemented by a finite-state device, such as a tree-walking transducer. That
is why we rely on other ways to normalize terms of base type $o$, namely
variants of the Interaction Abstract Machine (IAM).

### The purely affine IAM.

Let us start with a machine that can normalize a purely affine term
$v\mathrel{\mathop{\mathchar 58\relax}}o$. Intuitively, it moves a token
around the _edges_ of the syntax tree of $v$; we represent the situation where
the token is on the edge connecting the subterm $t$ to its context $C$ (such
that $C\langle t\rangle=v$) and is moving down (resp. up) as
$C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle$
(resp.
$C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle$).
The token carries a small amount of additional information: a tape which is a
stack using the symbols $\bullet$ and $\circ$.

We reuse the formalism of tree-generating machines from the previous section,
and we denote by $X^{*}$ (with the Kleene star) the set of lists with elements
in $X$.

######  Definition 4.1.

Let $v\mathrel{\mathop{\mathchar 58\relax}}o$ be purely affine. The tree-
generating machine $\mathrm{PAIAM}(v)$ has:

  * •

configurations of the form $(d,t,C,T)$ where
$d\in\\{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\}$,
$C\langle t\rangle=v$ and $T\in\\{\bullet,\circ\\}^{*}$ – which we abbreviate
as
$(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)$
when
$d={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
or
$(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)$
when
$d={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$;

  * •

the initial configuration
$({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}},\varepsilon)=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}},t,\langle\cdot\rangle,\varepsilon)$;

  * •

the following computation-step function:

$\begin{array}[]{rclcrcl}(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t\,u}}\rangle,T)&\mapsto&(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\,u\rangle,\bullet{\cdot}T)&&(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\,u\rangle,\bullet{\cdot}T)&\mapsto&(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t\,u}}\rangle,T)\\\
(C\langle
t\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{u}}\rangle,T)&\mapsto&(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\,u\rangle,\circ{\cdot}T)&&(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\,u\rangle,\circ{\cdot}T)&\mapsto&(C\langle
t\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{u}}\rangle,T)\\\
(C\langle\lambda
x.\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)&\mapsto&(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\lambda
x.\,t}}\rangle,\bullet{\cdot}T)&&(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\lambda
x.\,t}}\rangle,\bullet{\cdot}T)&\mapsto&(C\langle\lambda
x.\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)\\\
(C\langle\lambda
x.\,D\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{x}}\rangle\rangle,T)&\mapsto&(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\lambda
x.\,D\langle
x\rangle}}\rangle,\circ{\cdot}T)&&(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\lambda
x.\,D\langle x\rangle}}\rangle,\circ{\cdot}T)&\mapsto&(C\langle\lambda
x.\,D\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{x}}\rangle\rangle,T)\\\
(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{c}}\rangle,\bullet^{\mathrm{rk}(c)}{\cdot}T)&\mapsto&\lx@intercol
c\bigl{(}(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{c}}\rangle,\circ{\cdot}T),(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{c}}\rangle,\bullet{\cdot}\circ{\cdot}T),\dots,(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{c}}\rangle,\bullet^{\mathrm{rk}(c)-1}{\cdot}\circ{\cdot}T)\bigr{)}\hfil\lx@intercol\end{array}$

The last rule handles constants $c\mathrel{\mathop{\mathchar
58\relax}}o^{\mathrm{rk}(c)}\multimap o$ coming from a fixed ranked alphabet
$\Sigma$. When $\mathrm{rk}(c)=0$, the right-hand side is simply the tree with
a single node labeled by $c$; otherwise, it is a tree of height 1, whose
leaves are all configurations.

######  Example 4.2.

Let $u$ and $(t_{x})_{x\in\\{a,b,c\\}}$ be the terms defining the purely
affine $\lambda$-transducer from Example 1.1. On the term
$v=u\;(t_{a}\;(t_{b}\;t_{c})\;t_{c})$, we have the following IAM execution
(where $C\rightsquigarrow^{n}C^{\prime}$ means that $C$ rewrites into
$C^{\prime}$ in $n$ steps):

$\displaystyle({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{v}},\varepsilon)$
$\displaystyle\rightsquigarrow^{\phantom{*}}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{u}}\;(t_{a}\;(t_{b}\;t_{c})\;t_{c}),\bullet)\rightsquigarrow((\lambda
f.\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{f\;0}})\;(t_{a}\;(t_{b}\;t_{c})\;t_{c}),\varepsilon)\rightsquigarrow((\lambda
f.\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{f}}\;0)\;(\dots),\bullet)$
$\displaystyle\rightsquigarrow^{\phantom{*}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{(\lambda
f.\;f\;0)}}\;(t_{a}\;(t_{b}\;t_{c})\;t_{c}),\circ\bullet)\rightsquigarrow(u\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{(t_{a}\;(t_{b}\;t_{c})\;t_{c})}},\bullet)\rightsquigarrow^{2}(u\;({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t_{a}}}\;(t_{b}\;t_{c})\;t_{c}),\bullet\bullet\bullet)$
$\displaystyle\rightsquigarrow^{4}(u\;((\lambda\ell.\;\lambda r.\;\lambda
x.\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\ell}}\;(r\;x))\;(t_{b}\;t_{c})\;t_{c}),\bullet)\rightsquigarrow(u\;({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t_{a}}}\;(t_{b}\;t_{c})\;t_{c}),\circ\bullet)\rightsquigarrow^{2}(\dots\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t_{b}}\dots,\bullet\bullet)$
$\displaystyle\rightsquigarrow^{3}(u\;(t_{a}\;((\lambda f.\;\lambda
x.\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{S}}\;(f\;x))\;t_{c})\;t_{c}),\bullet)\rightsquigarrow\underbracket{S}_{\mathclap{\qquad\qquad\qquad\qquad\text{output
node (will be the root of the output tree)}}}((u\;(t_{a}\;((\lambda
f.\;\lambda
x.\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{S}}\;(f\;x))\;t_{c})\;t_{c}),\circ))$
$\displaystyle\rightsquigarrow^{*}\ldots[\text{many steps}]\ldots$
$\displaystyle\rightsquigarrow^{*}S(S((u\;(\dots\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t_{c}}),\bullet)))\rightsquigarrow
S^{3}((u\;(t_{a}\;(t_{b}\;t_{c})\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{S}}),\circ))\rightsquigarrow
S^{3}((u\;({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t_{a}\;(t_{b}\;t_{c})}}\;S),\circ\circ))$
$\displaystyle\rightsquigarrow^{2}S^{3}((u\;((\lambda\ell.\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\lambda
r.\;\lambda
x.\;\ell\;(r\;x)}})\;(t_{b}\;t_{c})\;t_{c}),\circ\circ))\rightsquigarrow
S^{3}((\dots({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{r}}\;x)\dots,\circ))$
$\displaystyle\rightsquigarrow^{\phantom{*}}S^{3}((\dots(r\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{x}})\dots,\varepsilon))\rightsquigarrow
S^{3}((u\;((\lambda\ell.\;\lambda
r.\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\lambda
x.\;\ell\;(r\;x)}})\;(t_{b}\;t_{c})\;t_{c}),\circ))$
$\displaystyle\rightsquigarrow^{2}S^{3}((u\;({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t_{a}}}\;(t_{b}\;t_{c})\;t_{c}),\bullet\bullet\circ))\rightsquigarrow^{2}S^{3}((u\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{(t_{a}\;(t_{b}\;t_{c})\;t_{c})}},\circ))\rightsquigarrow
S^{3}(({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{u}}\dots,\circ\circ))$
$\displaystyle\rightsquigarrow^{\phantom{*}}S^{3}(((\lambda
f.\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{f}}\;0)\dots,\circ))\rightsquigarrow
S^{3}(((\lambda
f.\;f\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{0}})\dots,\varepsilon))\rightsquigarrow
S(S(S(0)))$

Aside from our bespoke extension dedicated to constants from $\Sigma$, all the
other rules in Definition 4.1 come from the Linear IAM described by Accattoli
et al. [2, Section 3] (see also [36, §3.1]) – we refer to those papers for
high-level explanations of these rules. Despite its name, the Linear IAM also
works for affine terms (cf. [28, §3.3.4]).

######  Theorem 4.3 (Soundness of the purely affine IAM).

For any purely affine term $v\mathrel{\mathop{\mathchar 58\relax}}o$, the
output of $\mathrm{PAIAM}(v)$ is the unique $\tau\in\mathrm{Tree}(\Sigma)$
such that $\widetilde{\tau}$ is the normal form of $v$.

### Simulating $\lambda$-transducers by tree-walking transducers.

Fix a purely affine $\lambda$-transducer given by
$t_{a}\mathrel{\mathop{\mathchar 58\relax}}A^{\mathrm{rk}(a)}\multimap A$ for
$a\in\Gamma$ and $u\mathrel{\mathop{\mathchar 58\relax}}A\multimap o$. Thanks
to Proposition 2.1, we may assume that $u$ and every $t_{a}$ are in normal
form. Proposition 2.3 then tells us that since $A$ is purely affine, so are
these terms – and therefore, so is
$u\,\widehat{\tau}((t_{a})_{a\in\Gamma})\mathrel{\mathop{\mathchar
58\relax}}o$ for any input $\tau\in\mathrm{Tree}(\Gamma)$. Thus, we can use
the purely affine IAM to compute the tree encoded by its normal form – which,
by definition, gives us the image of $\tau$ by our $\lambda$-transducer.

To prove the first part of Theorem 1.4, we just need to simulate (in an
appropriate sense, made precise in the appendix)
$\mathrm{PAIAM}(u\,\widehat{\tau}((t_{a})_{a\in\Gamma}))$ by a TWT running on
$\tau$. Example 4.4 below illustrates how this works: a configuration of
$\mathrm{PAIAM}(u\,\widehat{\tau}((t_{a})_{a\in\Gamma}))$ is represented by a
configuration on input $\tau$ of a TWT in which each state consists of

  * •

a formal symbol in $\\{\mathsf{U,T},\nabla,\Delta\\}$;

  * •

if the symbol is $\mathsf{U}$ (resp. $\mathsf{T}$), a position in $u$ (resp.
$t_{a}\;\lozenge_{1}\;\dots\;\lozenge_{\mathrm{rk}(a)}$ for some
$a\in\Gamma$);

  * •

a tape in $\\{\bullet,\circ\\}^{*}$ that appears in the run of
$\mathrm{PAIAM}(u\,\widehat{\sigma}((t_{a})_{a\in\Gamma}))$ for some
$\sigma\in\mathrm{Tree}(\Gamma)$.

The information in the first two components is clearly bounded, but this is
not so obvious for the third one. We shall address this issue using Corollary
4.6 below, after the example.

######  Example 4.4.

We translate Example 1.1 to a TWT that has the following run on the input
$a_{1}(b_{2}(c_{3}),c_{4})$ – note how the steps correspond to those of the
IAM run in Example 4.2. This run visits the same input nodes as Example 3.4,
in the same order. The only difference is that it stays for longer on each
node ($\circlearrowleft$ appears very frequently).

$\displaystyle(\mathsf{I},\circlearrowleft,a_{1})$
$\displaystyle\rightsquigarrow^{\phantom{*}}(\mathsf{U}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\lambda
f.\;f\;0}},\bullet),\circlearrowleft,a_{1})\rightsquigarrow^{3}(\mathsf{U}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\lambda
f.\;f\;0}},\circ\bullet),\circlearrowleft,a_{1})\rightsquigarrow(\nabla(\bullet),\circlearrowleft,a_{1})$
$\displaystyle\rightsquigarrow^{\phantom{*}}(\mathsf{T}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t_{a}\;\lozenge_{1}}}\;\lozenge_{2},\bullet\bullet),\circlearrowleft,a_{1})\rightsquigarrow^{5}(\mathsf{T}((\lambda\ell.\;\lambda
r.\;\lambda
x.\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\ell}}\;(r\;x))\;\lozenge_{1}\;\lozenge_{2},\bullet),\circlearrowleft,a_{1})$
$\displaystyle\rightsquigarrow^{\phantom{*}}(\mathsf{T}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t_{a}}}\;\lozenge_{1}\;\lozenge_{2},\circ\bullet),\circlearrowleft,a_{1})\rightsquigarrow(\nabla(\bullet),\downarrow_{\bullet},b_{2})\rightsquigarrow(\mathsf{T}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t_{b}}}\;\lozenge_{1},\bullet\bullet),\circlearrowleft,b_{2})$
$\displaystyle\rightsquigarrow^{3}(\mathsf{T}((\lambda f.\;\lambda
x.\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{S}}\;(f\;x))\;\lozenge_{1},\bullet),\circlearrowleft,b_{2})\rightsquigarrow
S((\mathsf{T}((\lambda f.\;\lambda
x.\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{S}}\;(f\;x))\;\lozenge_{1},\circ),\circlearrowleft,b_{2}))$
$\displaystyle\rightsquigarrow^{*}\ldots[\text{many steps}]\ldots$
$\displaystyle\rightsquigarrow^{*}S(S((\nabla(\bullet),\downarrow_{\bullet},c_{4})))\rightsquigarrow
S^{3}((\Delta(\circ),\uparrow^{\bullet}_{2},a_{1}))\rightsquigarrow(\mathsf{T}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t_{a}\;\lozenge_{1}}}\;\lozenge_{2},\circ\circ),\circlearrowleft,a_{1})$
$\displaystyle\rightsquigarrow^{7}S^{3}(\mathsf{T}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t_{a}}}\;\lozenge_{1}\;\lozenge_{2}),\bullet\bullet\circ),\circlearrowleft,a_{1})\rightsquigarrow^{2}S^{3}((\Delta(\circ),\circlearrowleft,a_{1}))\rightsquigarrow
S^{3}(\mathsf{U}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{u}},\circ\circ),\circlearrowleft,a_{1})$
$\displaystyle\rightsquigarrow^{2}S^{3}((\mathsf{U}(\lambda
f.\;f\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{0}},\varepsilon),\circlearrowleft,a_{1}))\rightsquigarrow
S(S(S(0)))$

### Finite states via a typing invariant.

To bound the size of tapes $T\in\\{\bullet,\circ\\}^{*}$, we leverage the type
system. The idea is that a tape that appears in an IAM run points to an
occurrence of the base type $o$ in the type of the current subterm. Formally,
we define inductively:

$A\lightning\varepsilon=A\qquad(A\multimap
B)\lightning\circ{\cdot}T=A\qquad(A\multimap B)\lightning\bullet{\cdot}T=B$

(thus, $o\lightning T$ is undefined for $T\neq\varepsilon$). We then have the
following invariant on configurations:

######  Proposition 4.5 (compare with [28, Lemma 32 in §3.3.5]).

Suppose that either
$(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)$
or
$(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)$
appears in a run of $\mathrm{PAIAM}(v)$ for some $v\mathrel{\mathop{\mathchar
58\relax}}o$. If the (not necessarily closed) term $t$ is given the type $A$
as part of a typing derivation for $v\mathrel{\mathop{\mathchar 58\relax}}o$,
then $A\lightning T=o$.

Since $|T|\leq\mathrm{height}(A)$ is a necessary condition for $A\lightning T$
to be defined, we immediately get:

######  Corollary 4.6.

The sizes of the tapes that appear in a run of $\mathrm{PAIAM}(v)$ are bounded
by the maximum, over all subterms $t$ of $v$, of the height of the syntax tree
of the type of $v$.

Therefore, the tapes that can appear in a run of
$\mathrm{PAIAM}(u\,\widehat{\tau}((t_{a})_{a\in\Gamma}))$ have their size
bounded depending only on the subterms of $u$ and of each $t_{a}$,
independently of $\tau\in\mathrm{Tree}(\Gamma)$. This ensures that the TWT we
build from a purely affine $\lambda$-transducer has a finite set of states –
which concludes our exposition of the key ingredients for the first half of
Theorem 1.4.

### The almost purely affine case.

To prove the second half of Theorem 1.4, we add non-standard rules for let-
bindings and !-boxes to the Interaction Abstract Machine.

######  Definition 4.7.

Let $v\mathrel{\mathop{\mathchar 58\relax}}o$ be an almost purely affine term.
$\mathrm{APAIAM}(v)$ is the extension of $\mathrm{PAIAM}(v)$ (cf. Definition
4.1) with the following new cases in the computation-step function:

$\displaystyle(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\mathtt{let}\
\oc x=u\ \mathtt{in}\ t}}\rangle,T)$
$\displaystyle\mapsto(C\langle\mathtt{let}\ \oc x=u\ \mathtt{in}\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)\qquad\quad(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{\oc
t}}\rangle,T)\mapsto(C\langle\oc{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)$
$\displaystyle(C\langle\mathtt{let}\ \oc x=u\ \mathtt{in}\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)$
$\displaystyle\mapsto(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\mathtt{let}\
\oc x=u\ \mathtt{in}\ t}}\rangle,T)$ $\displaystyle(C\langle\mathtt{let}\ \oc
x=u\ \mathtt{in}\
D\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{x}}\rangle\rangle,T)$
$\displaystyle\mapsto(C\langle\mathtt{let}\ \oc
x={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{u}}\
\mathtt{in}\ D\langle x\rangle\rangle,T)$

######  Claim 3.

Proposition 4.5 extends to $\mathrm{APAIAM}(v)$ with $\oc A\lightning
T=A\lightning T$.

The last two rules in Definition 4.7 break a key duality principle at work in
the purely affine IAM (and suggested by the layout of Definition 4.1): if any
rule – except the one for constants from $\Sigma$ – sends a configuration
$\kappa_{1}$ to another configuration $\kappa_{2}$, then there is a dual rule
sending $\kappa_{2}^{\perp}$ to $\kappa_{1}^{\perp}$, where
$(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)^{\perp}=(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)$
and conversely
$(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)^{\perp}=(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)$.

In fact, our new rule for let-bound variables
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{x}}$
_cannot_ have a dual, because it is not injective. Indeed, consider a term of
the form $C\langle\mathtt{let}\ \oc x=u\ \mathtt{in}\ t\rangle$ where $t$
contains multiple occurrences of $x$, i.e. $t=D_{1}\langle
x\rangle=D_{2}\langle x\rangle$ for some contexts $D_{1}\neq D_{2}$ – this may
happen, since let-bound variables are not affine. Then for any
$T\in\\{\bullet,\circ\\}^{*}$, the computation-step function sends both
$(C\langle\mathtt{let}\ \oc x=u\ \mathtt{in}\
D_{1}\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{x}}\rangle\rangle,T)$
and $(C\langle\mathtt{let}\ \oc x=u\ \mathtt{in}\
D_{2}\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{x}}\rangle\rangle,T)$
to the same configuration $(C\langle\mathtt{let}\ \oc
x={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{u}}\
\mathtt{in}\ t\rangle,T)$ due to the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{x}}$
rule. This is why _reversible_ TWTs can simulate the purely affine IAM, but
not the _almost_ purely affine IAM.

To be sure that the missing dual rule is unnecessary, we show that
configurations of the form $(C\langle\mathtt{let}\ \oc
x={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{u}}\
\mathtt{in}\ t\rangle,T)$ cannot occur in an actual run. Assume the opposite
for the sake of contradiction. The typing rule for let-bindings forces the
type of $u$ to have the form $\oc A$, and by almost pure affineness, it must
be $\oc o$. By 3, $\oc o\lightning T=o$; therefore, $T=\varepsilon$, which
contradicts another invariant:

######  Proposition 4.8.

If
$(C\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)$
(resp.
$(C\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{t}}\rangle,T)$)
appears in a run of $\mathrm{APAIAM}(v)$ for some almost purely affine
$v\mathrel{\mathop{\mathchar 58\relax}}o$, then $T$ contains an odd (resp.
even) number of $\circ$s.

The same reasoning also shows that
$(C\langle\oc{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{t}}\rangle,T)$
cannot occur in a run. Having ruled out these problematic configurations, we
can establish soundness for the almost purely affine IAM, extending Theorem
4.3. The simulation by tree-walking transducers then follows the same pattern
than in the purely affine case (except we do not get reversibility).

##  5 Upper bounds on $\lambda$-transducers with preprocessing

We shall now apply Theorem 1.4 to quickly prove the left-to-right inclusions
in Theorems 1.5. We will not need to recall the definitions of MSO
transductions and MSO relabelings here, but we will use the closure of both
MSOTs and MSOT-Ss under precomposition by MSO relabelings – cf. [6, Section
3]666A warning concerning the tree transducer literature: composition is
written in the nonstandard order $f\circ g(x)=g(f(x))$ in [6, 17] (but we
prefer to follow the usual convention).  where MSOT-Ss are called MSO term
graph transductions. Thus, it suffices to prove our inclusions without an MSO
relabeling on the left-hand side.

Purely affine $\lambda$-transducer $\subseteq$ MSOT.

Let $f$ be defined by some purely affine $\lambda$-transducer. Then, by
Theorem 1.4, it is computed by some tree-walking transducer. Furthermore, it
has linear growth, i.e. $|f(\tau)|=O(|\tau|)$ – an immediate consequence of
the fact that $\beta$-reduction decreases the size of purely affine terms. To
conclude, it is known that any function computed by a TWT of linear growth is
an MSOT (see e.g. [17, §6.2]).

Almost purely affine $\lambda$-transducer $\subseteq$ MSOT-S.

We appeal to Theorem 1.4 to reduce our goal to the inclusion
$\text{TWT}\subseteq\text{MSOT-S}$ which implicitly appears in the literature.
Indeed, as explained by Engelfriet and Maneth [19, Section 3.2], tree-
walking777Called 0-pebble tree transducers in [19], as a special case of the
$k$-pebble tree transducers introduced in [29] (the latter have seen a
resurgence in recent years in the study of polyregular functions [8]). The
terminology tree-walking was only later used to speak of 0-pebble transducers,
starting with [15], but it was already in use for the tree-to-string version
of these devices since the late 1960s [3] (let us also mention the RT(Tree-
walk) transducers of [16] from the 1980s, discussed in [19, Section 3.3]).
transducers are syntactically the same888We sweep under the carpet subtleties
related to noncircularity here, as noncircularity is completely unnecessary to
prove that $\text{ATT}\subseteq\text{MSOT-S}$. as attributed tree transducers
(ATTs); and Bloem and Engelfriet have shown [6, Theorem 17] that
$\text{ATT}\circ\text{MSO relabeling}\equiv\text{MSOT-S}$. (Let us remark that
Gallot et al. use ATTs to prove both directions of their results in [22,
Chapter 7].)

##  6 Expressiveness of $\lambda$-transducers with preprocessing

The only thing that remains to be proved is the right-to-left inclusion in
Theorem 1.5. We derive it from the results of Gallot, Lemay and Salvati [21,
22].

### MSOT $\subseteq$ purely affine $\lambda$-transducer $\circ$ MSO
relabeling.

First, we introduce a slight generalization of Gallot et al.’s machine model
for MSOTs [21, §2.3]. While their model involves bottom-up regular lookahead,
this feature is just a special case of the MSO tests mentioned at the end of
the previous section, so it can be simulated by preprocessing by an MSO
relabeling (cf. appendix); this is why we do not include it in our version.

######  Definition 6.1.

A _GLS-transducer_ $\mathrm{Tree}(\Gamma)\rightarrow\mathrm{Tree}(\Sigma)$
consists of:

  * •

a finite set $Q$ of states, with a family $(A_{q})_{q\in Q}$ of purely affine
types;

  * •

an initial state $q_{0}\in Q$ and an output term $u\mathrel{\mathop{\mathchar
58\relax}}A_{q_{0}}\multimap o$ – which, like all the terms $t$ below, may use
constants $c\mathrel{\mathop{\mathchar 58\relax}}o^{\mathrm{rk}(c)}\multimap
o$ for $c\in\Sigma$;

  * •

for each $q\in Q$ and $a\in\Gamma$, a rule $q\langle
a(x_{1},\dots,x_{\mathrm{rk}(a)})\rangle\rightarrow t\;q_{1}\langle
x_{1}\rangle\;\dots\;q_{\mathrm{rk}(a)}\langle x_{\mathrm{rk}(a)}\rangle$
where the $q_{i}$ and $t\mathrel{\mathop{\mathchar
58\relax}}A_{q_{1}}\multimap\dots\multimap A_{q_{\mathrm{rk}(a)}}\multimap
A_{q}$ are chosen depending on $(q,a)$.

The semantics is that a GLS-transducer performs a top-down traversal
$q_{0}\langle\tau\rangle\rightarrow^{*}\tau^{\Downarrow}$ of its input tree
$\tau$ which builds a $\lambda$-term
$\tau^{\Downarrow}\mathrel{\mathop{\mathchar 58\relax}}A_{q_{0}}$. The normal
form of $u\;\tau^{\Downarrow}$ then encodes the output tree. Our model is a
bit more syntactically permissive than that of Gallot et al. (theirs would
correspond to using linear rather than affine terms, and forcing $u$ to be
$\lambda x.\;x$ – so $A_{q_{0}}=o$); therefore, it can compute at least
everything that their model can:

######  Theorem 6.2 (from [21, Theorem 3]).

MSOT $\subseteq$ GLS-transducer $\circ$ MSO relabeling.

We derive our desired result on $\lambda$-transducers in two steps. They are
detailed in the appendix (together with a more explicit specification of the
semantics of a GLS-transducer).

  * •

Every GLS-transducer can be made type-constant: $\exists
A\mathrel{\mathop{\mathchar 58\relax}}\forall q,\,A_{q}=A$. This uses an
encoding trick that preserves pure affineness, but not linearity.

  * •

A type-constant GLS-transducer can be turned into an MSO relabeling (that adds
to each node its top-down propagated state) followed by a purely affine
$\lambda$-transducer (which is just a GLS-transducer with $|Q|=1$).

From Theorem 6.2, we thus get MSOT $\subseteq$ purely affine
$\lambda\text{-transducer}\circ(\text{MSO relabeling})^{2}$, and since MSO
relabelings are closed under composition [6, §3], we are done.

### MSOT-S $\subseteq$ almost purely affine $\lambda$-transducer $\circ$ MSO
relabeling.

Following the same recipe as above, we reduce this to Gallot et al.’s
characterization of MSOT-S [21, Theorem 3]. Since they use Kanazawa’s almost
linear $\lambda$-terms [25] (which we discussed in the introduction), we need
to translate such terms into our almost purely affine terms. Let us introduce
the abbreviation $\lambda!x.\,t=(\lambda y.\,\mathtt{let}\ \oc x=y\
\mathtt{in}\ t)$ where $y$ is a fresh variable. We define inductively: $\wn
c=\lambda!x_{1}.\,\dots\,\lambda!x_{\mathrm{rk}(c)}.\,\oc(c\,x_{1}\,\dots\,x_{\mathrm{rk}(c)})$
for constants $c$ in a ranked alphabet $\Sigma$, and

$\wn x=\begin{cases}\oc x&\text{if}\ x\mathrel{\mathop{\mathchar
58\relax}}o\\\ x&\text{otherwise}\end{cases}\qquad\wn(\lambda
x.\,t)=\begin{cases}\lambda\oc x.\,\wn t&\text{if}\
x\mathrel{\mathop{\mathchar 58\relax}}o\\\ \lambda x.\,\wn
x&\text{otherwise}\end{cases}\qquad\wn(t\,u)=(\wn t)\,(\wn u)$

######  Claim 4.

Let $t\mathrel{\mathop{\mathchar 58\relax}}A$ be almost affine as defined in
[24]. Then $\wn t$ is almost purely affine, with type
$A\\{o\mathrel{\mathop{\mathchar 58\relax}}=\oc o\\}$. When
$t\mathrel{\mathop{\mathchar 58\relax}}o$, if
$t\longrightarrow_{\beta}^{*}\widetilde{\tau}$ (for some
$\tau\in\mathrm{Tree}(\Sigma)$) then $\wn
t\longrightarrow_{\beta}^{*}\oc\widetilde{\tau}$.

The inductive rule for application implies that
$\wn(u\;\widehat{\tau}((t_{a})_{a\in\Gamma}))=(\wn u)\;\widehat{\tau}((\wn
t_{a})_{a\in\Gamma})$, so the above claim allows us to translate
$\lambda$-transducers using almost affine terms à la Kanazawa.

##  7 Conclusion

### More related work.

Katsumata [26] has connected a categorical version of the Geometry of
Interaction (the Int-construction) to attribute grammars [27], and the latter
are closely related to the attributed tree transducers discussed in Section 5;
further GoI-automata connections of this kind are discussed in [32, §1.1]. Our
methodology of connecting $\lambda$-calculus and automata via abstract
machines may be compared to Salvati and Walukiewicz’s [35] use of Krivine
machines in the theory of higher-order recursion schemes. Clairambault and
Murawski [11] also compile affine recursion schemes to automata using a game
semantics that can be seen as a denotational counterpart of the operational
Interaction Abstract Machine.

######  Remark 7.1.

The aforementioned work [11] is a rare example of application of some GoI
variant to a setting that features the _additive connectives_ of linear logic.
It yields a translation from $\lambda$-terms to infinite-state systems, making
it unsuited to our purposes. In most versions of the GoI, the support for
additives is not as satisfactory as their handling of additive-free linear
logic – a well-known issue in the linear logic community.

This obstruction also motivated our choice, discussed in the introduction, to
follow the approach of Gallot et al. [21, 22] rather than Nguyễn and Pradic’s
implicit automata [33, 31]. Indeed, the latter’s solution to overcome the
limitations evidenced by Corollary 1.2 is to work with a linear
$\lambda$-calculus with additive connectives, enabling more flexible linear
usage patterns. This is analogous (see [31, Remark 6.0.1] for an actual
technical connection) to moving from strongly single use to single use macro
tree transducers [18, Section 5].

### Perspectives.

The obvious direction for further work is to study other relaxations of the
affine constraint. For example, one could introduce a !-depth $n$
$\lambda$-calculus, where the nesting depth of $!$-boxes is at most $n$. Would
our techniques be still usable? What kind of transducers would be
characterized? In particular, we formulate the following

######  Conjecture 7.2.

Almost !-depth 1 $\lambda$-transducer $\circ$ MSO relabeling $\equiv$ MSOT-S².

The _reversible_ tree-walking transducers that we have introduced also deserve
to be studied further: we believe that they should be closed under composition
(cf. [14] over strings) and verify the single-use restriction of [12, §8.2] –
implying that reversible TWT $\subseteq$ MSOT.

## References

  * [1] Beniamino Accattoli and Delia Kesner.  The structural $\lambda$-calculus.  In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 381–395. Springer, 2010.  doi:10.1007/978-3-642-15205-4_30.
  * [2] Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni.  The machinery of interaction.  In PPDP ’20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020, pages 4:1–4:15. ACM, 2020.  doi:10.1145/3414080.3414108.
  * [3] Alfred V. Aho and Jeffrey D. Ullman.  Translations on a context-free grammar.  Information and Control, 19(5):439–475, 1971.  Journal version of a STOC 1969 paper.  doi:10.1016/S0019-9958(71)90706-6.
  * [4] Rajeev Alur and Loris D’Antoni.  Streaming Tree Transducers.  Journal of the ACM, 64(5):1–55, August 2017.  doi:10.1145/3092842.
  * [5] Andrew Barber.  Dual Intuitionistic Linear Logic.  Technical report ECS-LFCS-96-347, LFCS, University of Edinburgh, 1996\.  URL: http://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/.
  * [6] 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 2000\.  doi:10.1006/jcss.1999.1684.
  * [7] Mikołaj Bojańczyk.  Who to cite: MSO transductions, December 2019.  URL: https://web.archive.org/web/20230810161232/https://www.mimuw.edu.pl/~bojan/posts/who-to-cite-mso-transductions.
  * [8] Mikołaj Bojańczyk.  Transducers of polynomial growth.  In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 1:1–1:27. ACM, 2022.  doi:10.1145/3531130.3533326.
  * [9] Mikołaj Bojańczyk and Thomas Colcombet.  Tree-walking automata do not recognize all regular languages.  SIAM Journal on Computing, 38(2):658–701, 2008.  doi:10.1137/050645427.
  * [10] Mikołaj Bojańczyk and Amina Doumane.  First-order tree-to-tree functions, 2020.  Corrected version with erratum of a LICS 2020 paper.  arXiv:2002.09307v2.
  * [11] Pierre Clairambault and Andrzej S. Murawski.  On the Expressivity of Linear Recursion Schemes.  In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of Leibniz International Proceedings in Informatics (LIPIcs), pages 50:1–50:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.  doi:10.4230/LIPIcs.MFCS.2019.50.
  * [12] Bruno Courcelle and Joost Engelfriet.  Graph structure and monadic second-order logic. A language-theoretic approach. Encyclopedia of Mathematics and its applications, Vol. 138. Cambridge University Press, June 2012.  Collection Encyclopedia of Mathematics and Applications, Vol. 138.  URL: https://hal.archives-ouvertes.fr/hal-00646514.
  * [13] Vincent Danos and Laurent Regnier.  Reversible, irreversible and optimal $\lambda$-machines.  Theoretical Computer Science, 227(1):79–97, September 1999.  doi:10.1016/S0304-3975(99)00049-3.
  * [14] Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote.  On reversible transducers.  In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 113:1–113:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.  doi:10.4230/LIPIcs.ICALP.2017.113.
  * [15] Joost Engelfriet.  The time complexity of typechecking tree-walking tree transducers.  Acta Informatica, 46(2):139–154, 2009.  doi:10.1007/s00236-008-0087-y.
  * [16] Joost Engelfriet.  Context-free grammars with storage, 2014.  Revised version of a 1986 technical report.  arXiv:1408.0683.
  * [17] Joost Engelfriet, Kazuhiro Inaba, and Sebastian Maneth.  Linear-bounded composition of tree-walking tree transducers: linear size increase and complexity.  Acta Informatica, 58(1-2):95–152, 2021.  doi:10.1007/s00236-019-00360-8.
  * [18] Joost Engelfriet and Sebastian Maneth.  Macro Tree Transducers, Attribute Grammars, and MSO Definable Tree Translations.  Information and Computation, 154(1):34–91, October 1999.  doi:10.1006/inco.1999.2807.
  * [19] Joost Engelfriet and Sebastian Maneth.  A comparison of pebble tree transducers with macro tree transducers.  Acta Informatica, 39(9):613–698, 2003.  doi:10.1007/s00236-003-0120-0.
  * [20] Joost Engelfriet and Heiko Vogler.  High level tree transducers and iterated pushdown tree transducers.  Acta Informatica, 26(1/2):131–192, 1988.  doi:10.1007/BF02915449.
  * [21] Paul Gallot, Aurélien Lemay, and Sylvain Salvati.  Linear high-order deterministic tree transducers with regular look-ahead.  In Javier Esparza and Daniel Král’, editors, 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic, volume 170 of LIPIcs, pages 38:1–38:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.  doi:10.4230/LIPIcs.MFCS.2020.38.
  * [22] Paul D. Gallot.  Safety of transformations of data trees: tree transducer theory applied to a verification problem on shell scripts.  PhD thesis, Université de Lille, December 2021.  URL: https://theses.hal.science/tel-03773108.
  * [23] Tsutomu Kamimura and Giora Slutzki.  Parallel and two-way automata on directed ordered acyclic graphs.  Information and Control, 49(1):10–51, 1981.  doi:10.1016/S0019-9958(81)90438-1.
  * [24] Makoto Kanazawa.  Almost affine lambda terms.  Technical report NII-2012-003E, National Institute of Informatics, Tokyo, 2012.  URL: https://www.nii.ac.jp/TechReports/public_html/12-003E.pdf.
  * [25] Makoto Kanazawa.  Parsing and generation as datalog query evaluation.  IfCoLog Journal of Logics and their Applications (FLAP), 4(4), 2017\.  Long version of an ACL 2007 paper.  URL: http://www.collegepublications.co.uk/downloads/ifcolog00013.pdf.
  * [26] Shin-ya Katsumata.  Attribute grammars and categorical semantics.  In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 271–282. Springer, 2008.  doi:10.1007/978-3-540-70583-3_23.
  * [27] Donald E. Knuth.  The genesis of attribute grammars.  In Pierre Deransart and Martin Jourdan, editors, Attribute Grammars and their Applications, International Conference WAGA, Paris, France, September 19-21, 1990, Proceedings, volume 461 of Lecture Notes in Computer Science, pages 1–12. Springer, 1990.  doi:10.1007/3-540-53101-7_1.
  * [28] Damiano Mazza.  Polyadic Approximations in Logic and Computation.  Habilitation à diriger des recherches, Université Paris XIII (Sorbonne Paris Nord), November 2017.  URL: https://theses.hal.science/tel-04238579.
  * [29] Tova Milo, Dan Suciu, and Victor Vianu.  Typechecking for XML transformers.  Journal of Computer and System Sciences, 66(1):66–97, 2003.  Journal version of a PODS 2000 paper.  doi:10.1016/S0022-0000(02)00030-2.
  * [30] Anca Muscholl and Gabriele Puppis.  The Many Facets of String Transducers.  In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019), volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1–2:21. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.  doi:10.4230/LIPIcs.STACS.2019.2.
  * [31] Lê Thành Dũng Nguyễn.  Implicit automata in linear logic and categorical transducer theory.  PhD thesis, Université Paris XIII (Sorbonne Paris Nord), December 2021\.  URL: https://theses.hal.science/tel-04132636.
  * [32] Lê Thành Dũng Nguyễn, Camille Noûs, and Cécilia Pradic.  Two-way automata and transducers with planar behaviours are aperiodic, 2023.  arXiv:2307.11057.
  * [33] Lê Thành Dũng Nguyễn and Cécilia Pradic.  Implicit automata in typed $\lambda$-calculi I: aperiodicity in a non-commutative logic.  In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 135:1–135:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.  doi:10.4230/LIPIcs.ICALP.2020.135.
  * [34] Alexander Okhotin.  Graph-walking automata: From whence they come, and whither they are bound.  In Michal Hospodár and Galina Jirásková, editors, Implementation and Application of Automata - 24th International Conference, CIAA 2019, Košice, Slovakia, July 22-25, 2019, Proceedings, volume 11601 of Lecture Notes in Computer Science, pages 10–29. Springer, 2019.  doi:10.1007/978-3-030-23679-3_2.
  * [35] Sylvain Salvati and Igor Walukiewicz.  Simply typed fixpoint calculus and collapsible pushdown automata.  Mathematical Structures in Computer Science, 26(7):1304–1350, October 2016.  doi:10.1017/S0960129514000590.
  * [36] Gabriele Vanoni.  On Reasonable Space and Time Cost Models for the $\lambda$-Calculus.  PhD thesis, Alma Mater Studiorum – Università di Bologna, June 2022\.  doi:10.48676/unibo/amsdottorato/10276.