transition for trees, generalizing Proposition 16. As announced, we find it
more convenient to first give a multicategory $\mathcal{TR}^{\mathrm{m}}$ and
then move to monoidal categories by taking
$\mathcal{TR}=(\mathcal{TR}^{\mathrm{m}})_{\mathrm{aff}}$. We then discuss the
restriction consisting of limiting the number of holes in the tree expressions
stored in register to at most one and show that it is not limiting.

  * Notations

Recall that we regard ranked alphabets $\bf R$ as pairs $(R,\mathrm{ar})$
where $R$ is a finite set of letters and $(\mathrm{ar}(a))_{a\in R}$ is a
family $R\to{\sf FinSet}$ of arities. Given two ranked alphabets $\bf R$ and
$\bf S$, we suggestively write $\bf R\otimes\bf S$ for the ranked alphabet
$(R+S,[\mathrm{ar},\mathrm{ar}])$. Given a finite set $U$, call
$\mathcal{O}(U)$ the ranked alphabet $(U,(\varnothing)_{u\in U})$ consisting
of ${|U|}$-many terminal letters and $\mathcal{I}(U)$ for the ranked alphabet
consisting of a single letter of arity $U$. Given a ranked alphabet
${\bf\Sigma}=(\Sigma,\mathrm{ar})$ and a subset $X\subseteq\Sigma$, we write
${\bf\Sigma}\upharpoonright X$ for the restriction
$(X,\mathrm{ar}\upharpoonright X)$.

####  5.3.1. Definition of $\mathcal{TR}$

Before giving the definition of $\mathcal{TR}^{\mathrm{m}}$, we first need to
make formal a notion of trees with linearly many occurrences of certain
constructors. Let $\bf R$ be a ranked alphabet. We define the set
$\mathbf{LTree}_{\bf\Gamma}({\bf R})$ of $\bf R$-linear trees as the set of
$({\bf\Gamma}\otimes{\bf R})$-trees $\mathbf{Tree}({\bf\Gamma}\otimes{\bf R})$
such that all constructors of $\bf R$ appear exactly once.

Define $\mathcal{TR}^{\mathrm{m}}({\bf\Gamma})$ (abbreviated
$\mathcal{TR}^{\mathrm{m}}$ in the sequel) as the multicategory

  * •

whose class of objects $\mathsf{Obj}(\mathcal{TR}^{\mathrm{m}})$ is ${\sf
FinSet}$.

  * •

whose class of multimorphisms from $(A_{i})_{i\in I}$ to $B$ is the set of
linear trees over the joint alphabet $(I,A)\otimes\mathcal{O}(B)$ (recall that
$(I,A)$ can formally be regarded as a ranked alphabet: its set of letters is
$I$ and the arity of $i\in I$ is $A(i)=A_{i}$).

$\mathsf{Hom}_{\mathcal{TR}^{\mathrm{m}}}\left((A_{i})_{i\in
I},B\right)\quad=\quad\mathbf{LTree}_{\bf\Gamma}((I,A)\otimes\mathcal{O}(B))$

  * •

whose composition operations are given by substitution: given a map $f:I\to J$
and multimorphisms

$t\in\mathbf{LTree}_{\bf\Gamma}((J,B)\otimes\mathcal{O}(C))\qquad\text{and}\qquad
u\in\prod_{j\in
J}\mathbf{LTree}_{\bf\Gamma}((f^{-1}(j),(A_{i})_{i})\otimes\mathcal{O}(B_{j}))$

the composite $t*_{f}u$ is defined by recursion over $t$:

    * –

if $t=a((t^{\prime}_{k})_{k})$ for some $a=\mathsf{in}_{1}(b)$ with
$b\in\Gamma$ or $a=\mathsf{in}_{2}(\mathsf{in}_{2}(c))$ for $c\in C$, then

$t*_{f}u=a((t^{\prime}_{k}*_{f}u)_{k})$

    * –

otherwise $t=\mathsf{in}_{2}(\mathsf{in}_{1}(j))((t^{\prime}_{b})_{b\in
B_{j}})$ with $j\in J$ and $t^{\prime}_{b}$ in some
$\mathbf{LTree}_{\bf\Gamma}((J_{b},B_{b})\otimes\mathcal{O}(C_{j}))$ for
$\bigcup_{b\in B_{j}}J_{b}=J\setminus\\{j\\}$, $B_{b}=B\upharpoonright J_{b}$
and $\bigcup_{b\in B_{j}}C_{b}=C$. In such a case, we set

$t*_{f}u=u_{j}[(t^{\prime}_{b}*_{\mathrm{id}_{J_{b}}}(u_{j^{\prime}})_{j^{\prime}\in
J_{b}})/b]_{b\in B_{j}}$

where $[-/-]_{-\in-}$ denotes the more usual substitution of leaves by
subtrees (recall that every $b\in B$, and a fortiori $B_{j}$ has arity
$\varnothing$).

While the definition of composition of multimorphisms in
$\mathcal{TR}^{\mathrm{m}}$ looks daunting, we claim it is rather natural.
Figure 13 depicts the composition $\alpha*_{f}(\beta_{x})_{x\in\\{t,u\\}}$
with

$\alpha=t(a(u(c()),*()),c())\qquad\beta_{t}=a(x(p(),b(q())),y())\quad\text{and}\quad\beta_{u}=z(c(),r(),c())$

Figure 13. Composition of some multimorphisms of $\mathcal{TR}^{\mathrm{m}}$.

We now set $\mathcal{TR}=(\mathcal{TR}^{\mathrm{m}})_{\mathrm{aff}}$; while
objects of $(\mathcal{TR}^{\mathrm{m}})_{\mathrm{aff}}$ are supposed to be
families of finite sets $(A_{i})_{i\in I}$, in the sequel, we sometimes
identify them with the ranked alphabets $(I,A)$ in $\mathcal{TR}$ for
notational convenience. As such, the notation ${\bf R}\otimes{\bf S}$
corresponds to the expected tensorial product in $\mathcal{TR}$.

We are now ready to define our first tree streaming setting.

$\mathfrak{TR}$ is the tree streaming setting
$(\mathcal{TR},\otimes,\top,\mathcal{I}(\varnothing),{\llparenthesis-\rrparenthesis})$,
where ${\llparenthesis-\rrparenthesis}$ is the canonical isomorphism
$\mathsf{Hom}_{\mathcal{TR}}\left(\top,\mathcal{I}(\varnothing)\right)\cong\mathsf{Hom}_{\mathcal{TR}^{\mathrm{m}}}\left(()_{\varnothing},\varnothing\right)\cong\mathbf{LTree}_{\bf\Gamma}(\varnothing)\cong\mathbf{Tree}({\bf\Gamma})$
(where $()_{\varnothing}$ is the empty family).

Call $\mathcal{TR}^{\mathrm{m},\leq 1}$ the full submulticategory of
$\mathcal{TR}^{\mathrm{m}}$ whose objects are empty or singleton sets, and
$\mathcal{TR}^{\leq 1}\cong\mathcal{TR}^{\mathrm{m},\leq 1}_{\mathrm{aff}}$ to
be the corresponding full subcategory of $\mathcal{TR}$. The monoidal
structure of $\mathcal{TR}$ restricts to $\mathcal{TR}^{\leq 1}$ without any
difficulty, and that $\mathcal{I}(\varnothing)$ is an object of
$\mathcal{TR}^{\leq 1}$. This means that $\mathfrak{TR}$ has a restriction to
a streaming setting $\mathfrak{TR}^{\leq 1}$.

While $\mathfrak{TR}^{\leq 1}$ turns out to be more elementary and a good
building block toward the definition of usual BRTTs, it is easier to show the
monoidal closure of $\mathfrak{TR}_{\oplus\with}$ than $\mathfrak{TR}^{\leq
1}$. Thankfully, it turns out that the expressiveness of BRTTs over
$\mathfrak{TR}$ and $\mathfrak{TR}^{\leq 1}$ is the same.

For one direction, there is a morphism $\mathfrak{TR}^{\leq
1}\to\mathfrak{TR}$ corresponding to the embedding $\mathcal{TR}^{\leq
1}\to\mathcal{TR}$. For the other direction, we exploit Theorem 55. The proof
involves some combinatorics, but nothing surprising as it amounts to the
classical decomposition of multi-hole trees into families of single-hole trees
as found in e.g. [AD17, §3.5].

######  Lemma 57.

There is a morphism of streaming settings $\mathfrak{TR}\to\mathfrak{TR}^{\leq
1}_{\oplus}$.

######  Proof 5.2 (Proof sketch).

We focus on giving enough ingredients to define the underlying (strong)
monoidal functor $F:\mathcal{TR}\to\mathcal{TR}^{\leq 1}_{\oplus}$, which is
going to preserve $\Bot$ (i.e., we will have
$F(\mathcal{I}(\varnothing))\cong\iota_{\oplus}(\mathcal{I}(\varnothing))$).

Rather than giving a direct explicit construction of $F$ (which is rather
tedious over morphisms), we obtain it as a composition of two strong monoidal
functors: the strong monoidal embedding
$\iota_{\oplus}:\mathcal{TR}\to\mathcal{TR}_{\oplus}$ and a functor
$R:\mathcal{TR}_{\oplus}\to\mathcal{TR}^{\leq 1}_{\oplus}$ right adjoint to
the inclusion $I:\mathcal{TR}^{\leq 1}_{\oplus}\to\mathcal{TR}_{\oplus}$.

$\textstyle{\mathcal{TR}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{\oplus}}$$\textstyle{\mathcal{TR}_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R}$$\scriptstyle{\top}$$\textstyle{\mathcal{TR}^{\leq
1}_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{I}$

$I$ is strong symmetric monoidal. Therefore, by [Mel09, Proposition 14,
Section 5.17], once we construct $R$ right adjoint to $I$, it comes equipped
with a canonical lax monoidal structure. Furthermore, since we want $I\dashv
R$, we can use the implicit characterization of adjoints given in [ML98, item
(iv), Theorem 2, Section IV.1]: to define $R$, it suffices to give the value
of $R\left(A\right)$ for every object
$A\in\mathsf{Obj}(\mathcal{TR}_{\oplus})$ and counit maps
$\epsilon_{A}:I(R(A))\to A$ such that, for every object
$B\in\mathsf{Obj}(\mathcal{TR}^{\leq 1}_{\oplus})$ and map
$h\in\mathsf{Hom}_{\mathcal{TR}_{\oplus}}\left(I(B),A\right)$, there is a
unique $\widetilde{h}\in\mathsf{Hom}_{\mathcal{TR}^{\leq
1}_{\oplus}}\left(R(A),B\right)$ such that the following diagram commutes

$\textstyle{I(B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\scriptstyle{I(\widetilde{h})}$$\textstyle{I(R(A))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\epsilon_{A}}$$\textstyle{A}$

So we only need to define $R(A)$ and $\epsilon_{A}$ to obtain our functor $R$;
once those are defined, we leave checking that the universal property holds to
the reader. We first focus on the case where
$A=\iota_{\oplus}(\mathcal{I}(U))$ for some finite set $U$. Recall that a
single-letter alphabet $\mathcal{I}(U)$, when seen as an object of
$\mathcal{TR}$, should be should be intuitively regarded as a register
containing a tree with $U$-many holes. If ${|U|}\leq 1$, we may simply take
$R(\iota_{\oplus}(\mathcal{I}(U)))=\iota_{\oplus}(\mathcal{I}(U))$. Otherwise,
${|U|}\geq 2$ and $\mathcal{I}(U)$ is not an object $\mathcal{TR}^{\leq 1}$;
in that case, we use the following recursive definition

$R(\iota_{\oplus}(\mathcal{I}(U)))\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \mathcal{I}(1)\leavevmode\nobreak\ \leavevmode\nobreak\
\otimes\leavevmode\nobreak\ \leavevmode\nobreak\
\bigoplus\limits_{b\in\Gamma}\bigoplus\limits_{\begin{subarray}{c}f:U\to\mathrm{ar}(b)\\\
\text{nonconstant}\end{subarray}}\bigotimes\limits_{x\in\mathrm{ar}(b)}R(\iota_{\oplus}(\mathcal{I}(f^{-1}(x))))$

Note that this definition is well-founded because the function $f$ in the
second sum is taken to be non constant, so that ${|f^{-1}(x)|}<{|U|}$ for
every $x$. While this suffices as a definition of
$R(\iota_{\oplus}(\mathcal{I}(U)))$, this might be a bit opaque without having
the definition of $\epsilon_{R(\iota_{\oplus}(\mathcal{I}(U)))}$. Before
giving that, let us attempt to give an intuitive rationale behind this
definition: there is an isomorphism262626Which we may later on define formally
as a composite  $\mathsf{Hom}_{\mathcal{TR}^{\leq
1}_{\oplus}}\left(\top,R(\iota_{\oplus}(\mathcal{I}(U)))\right)\xrightarrow{\;I\;}\mathsf{Hom}_{\mathcal{TR}_{\oplus}}\left(\top,R(\iota_{\oplus}(\mathcal{I}(U)))\right)\to\mathsf{Hom}_{\mathcal{TR}_{\oplus}}\left(\top,\mathcal{I}(U)\right)\xrightarrow{\;\sim\;}\mathbf{LTree}_{\bf\Gamma}(U)$
where the mediating arrow is the post-composition by
$\epsilon_{\iota_{\oplus}(\mathcal{I}(U))}$.

$\mathsf{Hom}_{\mathcal{TR}^{\leq
1}_{\oplus}}\left(\top,R(\iota_{\oplus}(\mathcal{I}(U)))\right)\cong\mathbf{LTree}_{\bf\Gamma}(U)$

which can be nicely pictured, provided we actually compute recursively
$R(\iota_{\oplus}(\mathcal{I}(U)))$ and spell out a normal form

$R(\iota_{\oplus}(\mathcal{I}(U)))\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \cong\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \bigoplus_{t\in{\bf PT}(U)}\bigotimes_{n\in N(t)}A_{n}$

with all $A_{n}=\mathcal{I}(\varnothing)$ or $A_{n}\cong\mathcal{I}(1)$. It is
always possible to build a suitable set ${\bf PT}(U)$ simply because all
objects of $\mathcal{TR}^{\leq 1}_{\oplus}$ have this shape, but an intuitive
definition of what one might call a set of _partitioning trees over $U$_ is
also possible for $\bf PT$, and $N(t)$ would then correspond to the nodes of
the trees. We skip defining this notion formally, but note that the announced
bijection would then match trees with $U$-many holes with pairs
$(t,(u_{i})_{i\in N(t)})$ of a partitioning tree $t$ and a family of trees
with at most one-hole $(u_{i})_{i\in N(t)}$. This bijective correspondence is
pictured in Figure 14.

Figure 14. Decomposition of a multi-hole tree
$\mathbf{LTree}_{\\{a:2,b:1,c:0,d:3\\}}(\\{x,y,z,t\\})$ as a tuple consisting
of a partitioning tree and trees with at most one hole.

Now, we define
$\epsilon_{R(\iota_{\oplus}(\mathcal{I}(U)))}\in\mathsf{Hom}_{\mathcal{TR}^{\leq
1}_{\oplus}}\left(I(R(\iota_{\oplus}(\mathcal{I}(U)))),\iota_{\oplus}(\mathcal{I}(U))\right)$,
by induction over the size of $U$. If ${|U|}\leq 1$, we take
$\epsilon_{R(\iota_{\oplus}(\mathcal{I}(U)))}:\iota_{\oplus}(\mathcal{I}(U))\to\iota_{\oplus}(\mathcal{I}(U))$
to be the identity. Otherwise, we need to define a map

$g_{U}\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\
I\left(\bigoplus_{b\in\Gamma}\bigoplus_{\begin{subarray}{c}f:U\to\mathrm{ar}(b)\\\
\text{nonconstant}\end{subarray}}\bigotimes_{x\in\mathrm{ar}(b)}R(\iota_{\oplus}(\mathcal{I}(f^{-1}(x))))\right)\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\iota_{\oplus}(\mathcal{I}(U))$

or, equivalently, a family of $\mathcal{TR}_{\oplus}$-maps indexed by
$b\in\Gamma$ and $f:U\to\mathrm{ar}(b)$ non-constant

$g_{b,f}\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\
\bigotimes_{x\in\mathrm{ar}(b)}I(R(\iota_{\oplus}(\mathcal{I}(f^{-1}(x)))))\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\iota_{\oplus}(\mathcal{I}(U))$

By the induction hypothesis, we have a family of $\mathcal{TR}_{\oplus}$-maps
$(g_{x})_{x\in\mathrm{ar}(b)}$

$g_{x}\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\
I(R(\iota_{\oplus}(\mathcal{I}(f^{-1}(x)))))\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\iota_{\oplus}(\mathcal{I}(f^{-1}(x)))$

We define $g_{b,f}$ as the composite

$\bigotimes_{x\in\mathrm{ar}(b)}I(R(\iota_{\oplus}(\mathcal{I}(f^{-1}(x)))))\leavevmode\nobreak\
\xrightarrow{\leavevmode\nobreak\ \leavevmode\nobreak\
\bigotimes_{x}g_{x}\leavevmode\nobreak\ \leavevmode\nobreak\
}\leavevmode\nobreak\
\displaystyle\bigotimes_{x\in\mathrm{ar}(b)}\iota_{\oplus}(\mathcal{I}(f^{-1}(x)))\leavevmode\nobreak\
\xrightarrow{\leavevmode\nobreak\ \leavevmode\nobreak\
\overline{b}\leavevmode\nobreak\ \leavevmode\nobreak\ }\leavevmode\nobreak\
\iota_{\oplus}(\mathcal{I}(U))$

where $\overline{b}$ is obtained from the map of $\mathcal{TR}^{\mathrm{m}}$
which intuitively takes a family $(t_{x})_{x\in\mathrm{ar}(b)}$ of trees into
a single tree $b((t_{x})_{x\in\mathrm{ar}(b)})$ (officially, the tree
$b((*)_{x\in\mathrm{ar}(b)})\in\mathbf{LTree}_{\bf\Gamma}(\mathcal{O}(U))$.

Now, $R$ is defined on objects of the shape $\iota_{\oplus}(\mathcal{I}(U))$,
as well as $\epsilon$, so we need to extend this to the whole category
$\mathcal{TR}_{\oplus}$. Recall that every object $A$ of
$\mathcal{TR}_{\oplus}$ can be written as $A=\bigoplus_{v\in
V}\bigotimes_{j\in J_{u}}\iota_{\oplus}(\mathcal{I}(U_{j}))$. In the end, the
functor $R$ is expected to be strong monoidal, and we may force it to preserve
coproducts, so we set

$R(A)\leavevmode\nobreak\ \leavevmode\nobreak\ =\leavevmode\nobreak\
\leavevmode\nobreak\ \bigoplus_{v\in V}\bigotimes_{j\in
J_{u}}R(\iota_{\oplus}(\mathcal{I}(U_{j})))\qquad\qquad\qquad\epsilon_{A}\leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
\bigoplus_{v\in V}\bigotimes_{j\in
J_{u}}\epsilon_{\iota_{\oplus}(\mathcal{I}(U_{j}))}$

####  5.3.2. Relationship to $\lambda\ell^{\oplus\with}$

Recall that if ${\bf\Gamma}=\\{a_{1}:A_{1},\ldots,a_{k}:A_{k}\\}$ is an output
alphabet, we call $\widetilde{\bf\Gamma}$ the context
$a_{1}:\mathbbl{o}\multimap\ldots\multimap\mathbbl{o},\ldots,a_{k}:\mathbbl{o}\multimap\ldots\multimap\mathbbl{o}$
where the type of $a_{i}$ has ${|A_{i}|}$ arguments. Definition 3.3 provides
us with a suitable affine monoidal closed category
$\mathcal{L}(\widetilde{\bf\Gamma})$, which we still call $\mathcal{L}$ when
$\widetilde{\bf\Gamma}$ is clear from context. Since we have a monoidal
product, we may easily adapt Definition 3.3 to get a tree streaming setting
$\mathfrak{L}$. Then we may relate $\lambda\ell^{\oplus\with}$-definability to
(single-state) $\mathfrak{L}$-BRTT.

######  Lemma 58.

Computability by single-state $\mathfrak{L}$-BRTTs and
$\lambda\ell^{\oplus\with}$-definability are equivalent for functions
$\mathbf{Tree}({\bf\Sigma})\to\mathbf{Tree}({\bf\Gamma})$.

######  Proof 5.3 (Proof idea).

This is proven in a similar way as Lemma 24, based on the syntactic Lemma 25.
The proof is even more straightforward as there is no mismatch between the
processing of trees by BRTTs and $\lambda\ell^{\oplus\with}$-terms working
with Church encodings, contrary to SSTs for strings (which operate top-down
rather than bottom-up when regarding strings as trees).

We can now notice that $\mathfrak{L}$-BRTTs are more expressive than
$\mathcal{TR}^{\leq 1}$-BRTTs thanks to the notion of streaming setting
morphisms, much like with strings (this generalizes Lemma 26).

######  Lemma 59.

There is a morphism of streaming settings $\mathfrak{TR}\to\mathfrak{L}$.

######  Proof 5.4 (Proof sketch).

Let us focus on the underlying functor $F:\mathcal{TR}\to\mathcal{L}$. For
objects (which are finite sets), we put

$F\left(\bigotimes_{i\in I}U_{i}\right)=\bigotimes_{i\in
I}\left(\left(\mathbbl{o}^{\otimes
U_{i}}\multimap\mathbbl{o}\right)\with\mathbf{I}\right)$

A multimorphism
$f\in\mathsf{Hom}_{\mathcal{TR}^{\mathrm{m}}}\left((U_{i})_{i\in I},V\right)$
is an element of $\mathbf{LTree}_{\bf\Gamma}\left(\left(\bigotimes_{i\in
I}\mathcal{I}(U_{i})\right)\otimes\mathcal{O}(V)\right)$ which has a Church
encoding $\underline{f}$ which has a type isomorphic to $\bigotimes_{i\in
I}\left(\mathbbl{o}^{\otimes{U_{i}}}\multimap\mathbbl{o}\right)\multimap\mathbbl{o}$,
and thus embeds into $F\left(\bigotimes_{i\in I}U_{i}\right)$ through well-
typed term $\iota$. We take $F(f_{\mathrm{aff}})=\lambda
x.\iota\;\underline{f}$, and extend this definition to arbitrary morphisms
$(f,(\alpha_{j})_{j}):\bigotimes_{i\in I}U_{i}\to\bigotimes_{j\in J}V_{j}$ in
$\mathcal{TR}$ by first using the second projection $\pi_{2}$ to restrict to
the case where ${\sf{dom}}(f)=I$, and then by piecing together the
$F((\alpha_{j})_{\mathrm{aff}})$.

######  Corollary 60.

There is a morphism of streaming settings
$\mathfrak{TR}_{\oplus\with}\to\mathfrak{L}$.

######  Proof 5.5 (Proof idea).

Starting from Lemma 59, we have a functor $\mathcal{TR}\to\mathcal{L}$. Since
$\mathcal{L}$ has all products and coproducts, the universal properties of the
$(-)_{\with}$ and $(-)_{\oplus}$ completion yield a functor
$F:\mathcal{TR}_{\oplus\with}\to\mathcal{L}$. The monoidal structure of the
initial functor $\mathcal{TR}\to\mathcal{L}$ can be lifted accordingly. For
any finite family of objects $(((A_{k})_{k\in K_{j}})_{j\in J_{i}})_{i\in I}$
sitting in a symmetric monoidal closed category with products and coproducts,
there are canonical morphisms

$\left(\bigoplus_{u\in U}\bigwith_{x\in
X_{u}}A_{x}\right)\otimes\left(\bigoplus_{v\in V}\bigwith_{v\in
Y_{v}}B_{y}\right)\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \bigoplus_{(u,v)\in
U\times V}\bigwith_{(x,y)\in X_{u}\times Y_{v}}A_{x}\otimes B_{y}$

which are not isomorphisms in general, but constitute the non-trivial part of
the lax monoidal structure of $F$; $m^{0}:\mathbf{I}\to F(\mathbf{I})$ is
actually the identity.

###  5.4. $\mathfrak{TR}_{\with}$-BRTTs coincide with regular functions, via
coherence spaces

We define a streaming setting $\mathfrak{TR}^{\incoh}$ and its restriction
$\mathfrak{TR}^{\incoh,\leq 1}$ (with respective underlying categories
$\mathcal{TR}^{\incoh}$, $\mathcal{TR}^{\incoh,\leq 1}$) so that
$\mathfrak{TR}^{\incoh,\leq 1}$-BRTTs coincide with Alur and D’Antoni’s notion
of single-use-restricted BRTT [AD17], which they showed to characterize
regular tree functions. We then show that there are morphisms of streaming
settings
$\mathfrak{TR}_{\with}\to\mathfrak{TR}^{\incoh}\to\mathfrak{TR}_{\with}$ and
thus establish that $\mathfrak{TR}_{\with}$-BRTTs capture exactly regular tree
functions.

Much like $\mathcal{TR}$, the category $\mathcal{TR}^{\incoh}$ is obtained by
applying a generic construction to $\mathcal{TR}^{\mathrm{m}}$, taking weak
symmetric multicategories to symmetric affine monoidal categories. In
particular, objects of $\mathcal{TR}^{\incoh}$ will consist of formal tensor
products of objects of $\mathcal{TR}^{\mathrm{m}}$. The main difference is
that morphisms of $\mathcal{TR}^{\incoh}$ will induce a dependency _relation_
$D\subseteq I\times J$ over indexing sets, rather than a partial function
$J\rightharpoonup I$. This corresponds to a relaxation of the copylessness
condition. However, objects of $\mathcal{TR}^{\incoh}$ will also be equipped
with a _conflict relation_ $\incoh$ over their indexed sets, and $D$ will be
required to satisfy a linearity constraint. Calling $\coh$ the dual _coherence
relation_ such that $x\coh y$ is equivalent to $x=y\vee\neg(x\incoh y)$, if we
have $(i,j)\in D$ and $(i^{\prime},j^{\prime})\in D$, the linearity constraint
enforces

$j\coh_{J}j^{\prime}\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
i\coh_{I}i^{\prime}\qquad\text{and}\qquad
i\incoh_{I}i^{\prime}\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ j\incoh_{J}j^{\prime}$

This corresponds to the _single use restriction_ imposed on BRTTs [AD17,
§2.1], whose introduction was motivated in Section 2.2.3. The BRTT that we
gave for the “conditional swap” function in Example 5 is single-use-restricted
according to the above by taking its two registers (i.e. objects of
$\mathcal{TR}^{\mathrm{m}}$) to be in conflict. But as our choice of notation
and vocabulary suggests, this is also related to the category of (finite)
_coherence spaces_ , the first denotational model of linear logic [Gir87]
(predated by a similar semantics for system F [Gir86]). As far as we know,
this observation is new (the conflict relation is denoted by $\mathbf{\eta}$
in [AD17], while $\incoh$ comes from the linear logic literature). The
coherence semantics of the linear $\lambda$-calculus has been used in
particular by Gallot, Lemay and Salvati [GLS20] to analyze a top-down tree
transducer model containing linear $\lambda$-terms. Unlike them, we do not use
coherence spaces _as a semantics_ here; what happens here is much closer the
use of a coherence/conflict relation to handle additive connectives – we will
indeed show a connection with the $\with$-completion – in proof nets, see
[Gir96, Appendix A.1] and [HH16].

[see e.g. [Gir95, §2.2.3]] A coherence space $I$ is a pair $(\|I\|,\coh_{I})$
of a set $\|I\|$, called the _web_ , and a binary reflexive symmetric relation
$\coh_{I}$ over $\|I\|$ called the _coherence relation_. As usual, given a
coherence relation $\coh$, we write $\incoh$ for the dual defined by $i\incoh
i^{\prime}\Leftrightarrow(i=i^{\prime}\vee\neg(i\coh i^{\prime}))$. Finite
coherence spaces are those coherence spaces whose webs are finite. A _linear
map_ of coherence spaces $f:I\to J$ is a relation $f\subseteq\|I\|\times\|J\|$
such that, whenever $(i,j)\in f$ and $(i^{\prime},j^{\prime})\in f$, we have

$i\coh_{I}i^{\prime}\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
j\coh_{J}j^{\prime}\qquad\text{and}\qquad
j\incoh_{J}j^{\prime}\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ i\incoh_{I}i^{\prime}$

Note that these are the _converse implications_ of those stated above for
BRTTs.

The diagonal $\\{(i,i)\mid i\in\|I\|\\}$ is a linear map $I\to I$ and the
relational composition of two linear maps $I\to J\to K$ is again a linear map,
so that we have a category ${\sf FinCoh}$ whose objects are coherence spaces
and morphisms are linear maps.

${\sf FinCoh}$, equipped with the tensorial product

$(\|I\|,\coh_{I})\otimes(\|J\|,\coh_{J})=(\|I\|\times\|J\|,\coh_{I}\times\coh_{J})$

and dualizing object $(1,1\times 1)$, is a well-studied $*$-autonomous
category with cartesian products and coproducts. The latter may be defined
pointwise as

$(\|I\|,\coh_{I})\oplus(\|J\|,\coh_{J})=(\|I\|+\|J\|,\;\coh_{I\oplus J})$

where $\coh_{I\oplus J}$ is the _smallest_ relation such that

$\mathsf{in}_{1}(i)\coh_{I\oplus J}\mathsf{in}_{1}(i^{\prime})\ \;\text{when}\
\;i\coh_{I}i^{\prime}\qquad\text{and}\qquad\mathsf{in}_{2}(j)\coh_{I\oplus
J}\mathsf{in}_{2}(j^{\prime})\ \;\text{when}\ \;j\coh_{J}j^{\prime}$

Dualizing an object corresponds to moving from $\coh$ to $\incoh$, i.e.
$(\|I\|,\coh_{I})^{\bot}=(\|I\|,\incoh_{I})$, and the product is $I\with
J=(I^{\bot}\oplus J^{\bot})^{\bot}$.

With this in mind, we can describe how to turn a multicategory into an affine
monoidal category where monoidal products may be indexed by coherence spaces.
The construction has a vague family resemblance with the _coherence completion
of categories_ introduced by Hu and Joyal [HJ99], but appears to have quite
different properties.

Let $\mathcal{M}$ be a weak symmetric multicategory. We define
$\mathcal{M}_{\mathrm{coh}}$ to be the category

  * •

whose objects are pairs $(X,(R_{x})_{x\in\|X\|})$ where $X$ is a finite
coherence space and $(R_{x})_{x\in\|X\|}$ a family of objects of
$\mathcal{M}$. We suggestively write them $\bigodot_{x\in X}R_{x}$.

  * •

whose morphisms

$(f,(\alpha_{y})_{y\in\|Y\|})\in\mathsf{Hom}_{\mathcal{M}_{\mathrm{coh}}}\left(\bigodot_{x\in
X}R_{x},\bigodot_{y\in Y}S_{y}\right)$

are pairs consisting of a linear map $f\in\mathsf{Hom}_{{\sf
FinCoh}}\left(Y,X\right)$ and a family of multimorphisms
$\alpha_{y}\in\mathsf{Hom}_{\mathcal{M}}\left((R_{x})_{x\in
f(y)},S_{y}\right)$.

  * •

whose identities are pairs
$(\mathrm{id}_{X},(\mathrm{id}_{R_{x}})_{x\in\|X\|})$.

  * •

where the composition of

$(f,(\alpha_{y})_{y\in\|Y\|})\in\mathsf{Hom}\left(\bigodot_{x\in
X}R_{x},\bigodot_{y\in Y}S_{y}\right)\leavevmode\nobreak\ \leavevmode\nobreak\
\text{and}\leavevmode\nobreak\ \leavevmode\nobreak\
(g,(\beta_{z})_{z\in\|Z\|})\in\mathsf{Hom}\left(\bigodot_{y\in
Y}S_{y},\bigodot_{z\in Z}T_{z}\right)$

is $(f\circ g,(\beta_{z}*(\alpha_{y})_{y\in g(z)})_{z\in Z})$.

We set $\mathcal{TR}^{\incoh}=(\mathcal{TR}^{\mathrm{m}})_{\mathrm{coh}}$ and
$\mathcal{TR}^{\incoh,\leq 1}$ to be its full subcategory consisting of
objects $\bigodot_{x\in X}A_{x}$ where each $A_{x}$ is either empty or a
singleton (so that $\mathcal{TR}^{\incoh,\leq 1}$ is isomorphic to
$(\mathcal{TR}^{\mathrm{m},\leq 1})_{\mathrm{coh}}$).

######  Proposition 61.

BRTTs over the restricted tree streaming setting $\mathfrak{TR}^{\incoh,\leq
1}$ compute exactly the regular tree functions.

######  Proof 5.6.

By virtue of being equivalent to Alur and D’Antoni’s notion of single-use-
restricted BRTT [AD17]. We point the reader to Appendix A for a self-contained
definition of those not involving categories, and leave it as an exercise to
formally match those two descriptions. Although [AD17] and our Appendix A only
consider BRTTs over _binary_ trees, the proof of equivalence between the
latter and regular tree functions goes through _macro tree transducers_ (with
regular look-ahead and single use restriction) which are known to compute
regular functions for trees over arbitrary ranked alphabets [EM99], so
everything can be made to work out with arbitrary arities in the end.

This being done, the remainder of this section does not depend on
$\mathcal{TR}^{\mathrm{m}}$; the arguments apply to any weak symmetric
multicategory $\mathcal{M}$ and designated object
$\Bot\in\mathsf{Obj}(\mathcal{M})$.

Accordingly, fix such an $\mathcal{M}$ and a $\Bot$ for the remainder of this
section. Fix also a set $O$ and a map
${\llparenthesis-\rrparenthesis}:\mathsf{Hom}_{\mathcal{M}}\left((\cdot)_{\varnothing},\Bot\right)\to
O$.

######  Proposition 62.

$\mathcal{M}_{\mathrm{coh}}$ has a terminal object, given by the unique family
over the empty coherence space, and can be equipped with a symmetric monoidal
affine structure $(\otimes,\top)$ where

$\left(\bigodot_{i\in I}A_{i}\right)\otimes\left(\bigodot_{j\in
J}B_{j}\right)\leavevmode\nobreak\ \leavevmode\nobreak\ =\leavevmode\nobreak\
\leavevmode\nobreak\ \bigodot_{x\in I\with
J}\left\\{\begin{array}[]{ll}A_{i}&\text{if $x=\mathsf{in}_{1}(i)$}\\\
B_{j}&\text{if $x=\mathsf{in}_{2}(j)$}\\\ \end{array}\right.$

and $I\with J$ designates the cartesian product in ${\sf FinCoh}$.

######  Proof 5.7.

Left to the reader. Strictly speaking, later developments will depend on the
precise structure itself and not merely on its existence, but there is a
single sensible choice of bifunctorial action and structural morphisms making
the above a monoidal product.

######  Remark 63.

To start making sense of the use of the cartesian product of ${\sf FinCoh}$,
there is a useful analogy with $\mathcal{M}_{\mathrm{aff}}$ here. There is a
projection functor $\mathcal{M}_{\mathrm{aff}}\to{\sf PartFinSet}$ where ${\sf
PartFinSet}$ is the category of finite sets and partial functions. The
tensorial product of $\mathcal{M}_{\mathrm{aff}}$ required a coproduct at the
level of indices. Here, we have a projection functor
$\mathcal{M}_{\mathrm{coh}}\to{\sf FinCoh}^{\mathrm{op}}$, and we again use a
coproduct at the level of indices (which becomes a product due to the
contravariance).

We call $\mathfrak{M}_{\mathrm{aff}}$ the tree streaming setting based on
$\mathcal{M}_{\mathrm{aff}}$, $\Bot$ and ${\llparenthesis-\rrparenthesis})$,
and $\mathfrak{M}_{\mathrm{coh}}$ the corresponding tree streaming setting
based on $\mathcal{M}_{\mathrm{coh}}$.

######  Proposition 64.

There is a full and faithful strong monoidal functor
$\mathcal{M}_{\mathrm{aff}}\to\mathcal{M}_{\mathrm{coh}}$ extending to a
morphism of streaming setting
$\mathfrak{M}_{\mathrm{aff}}\to\mathfrak{M}_{\mathrm{coh}}$.

######  Proof 5.8.

Call $F$ this functor, and, for any set $I$, write $\Delta$ for the functor
${\sf PartFinSet}\to{\sf FinCoh}$ taking a set $I$ to the discrete coherence
space $\Delta(I)=(I,\\{(i,i)\mid i\in I\\})$. Note that we have
$\Delta(I)^{\bot}=(I,I\times I)$, which may be regarded as the codiscrete
coherence space generated by $I$. On objects of $\mathcal{M}_{\mathrm{aff}}$,
we define $F$ as

$F\left(\bigotimes_{i\in I}A_{i}\right)=\bigodot_{i\in\Delta(I)^{\bot}}A_{i}$

For morphisms $(f,(\alpha_{j})_{j\in
J})\in\mathsf{Hom}_{\mathcal{M}_{\mathrm{aff}}}\left(\bigotimes_{i\in
I}A_{i},\bigotimes_{j\in J}B_{j}\right)$, we set

$F(f,(\alpha_{j})_{j\in J})=(\\{(j,i)\mid j=f(i)\\},(\alpha_{j})_{j\in J})$

It is rather straightforward to check that $F$ is indeed full, faithful and
strong monoidal, and the extension to a morphism
$\mathfrak{M}_{\mathrm{aff}}\to\mathfrak{M}_{\mathrm{coh}}$ is immediate.

######  Proposition 65.

$\mathcal{M}_{\mathrm{coh}}$ also has cartesian products, which may be defined
as

$\left(\bigodot_{i\in I}A_{i}\right)\with\left(\bigodot_{j\in
J}B_{j}\right)\leavevmode\nobreak\ \leavevmode\nobreak\ =\leavevmode\nobreak\
\leavevmode\nobreak\ \bigodot_{x\in I\oplus
J}\left\\{\begin{array}[]{ll}A_{i}&\text{if $x=\mathsf{in}_{1}(i)$}\\\
B_{j}&\text{if $x=\mathsf{in}_{2}(j)$}\\\ \end{array}\right.$

(The proof is left to the reader.) Therefore, we can extend Proposition 64:

######  Corollary 66.

There is a functor
$E:(\mathcal{M}_{\mathrm{aff}})_{\with}\to\mathcal{M}_{\mathrm{coh}}$ that is
full, faithful and lax (but _not_ strong) monoidal, extending to a morphism of
streaming settings
$(\mathfrak{M}_{\mathrm{aff}})_{\with}\to\mathfrak{M}_{\mathrm{coh}}$.

In the following proof and the rest of this section, we write explicitly
$\mathbf{I}_{\mathrm{coh}}$ for the monoidal unit of $\otimes$ in
$\mathcal{M}_{\mathrm{coh}}$ and ${\mathbf{I}_{\mathrm{aff}}}_{\with}$ for the
unit in $(\mathcal{M}_{\mathrm{aff}})_{\with}$.

######  Proof 5.9 (Proof idea).

The universal property of the free product completion defines $E$ as the
unique product-preserving functor extending the functor of Proposition 64. It
remains to equip it with a lax monoidal functor structure. The map
$m^{0}:\mathbf{I}_{\mathrm{coh}}\to E({\mathbf{I}_{\mathrm{aff}}}_{\with})$ is
an obvious isomorphism, while the natural transformation
$m^{2}_{A,B}:E(A)\otimes E(B)\to E(A\otimes B)$ can be obtained via the
canonical map

$\left(\bigwith_{i\in I}A_{i}\right)\otimes\left(\bigwith_{j\in
J}B_{j}\right)\to\bigwith_{(i,j)\in I\times J}A_{i}\otimes B_{j}$

in $\mathcal{M}_{\mathrm{coh}}$ (it exists in all monoidal categories with
products).

We can now go the other way around.

######  Lemma 67.

There is a strong monoidal functor
$\mathcal{M}_{\mathrm{coh}}\to(\mathcal{M}_{\mathrm{aff}})_{\with}$, which
extends to a morphism of streaming settings
$\mathfrak{M}_{\mathrm{coh}}\to(\mathfrak{M}_{\mathrm{aff}})_{\with}$.

######  Proof 5.10.

For a coherence space $(\|X\|,\coh_{X})$, write
$\mathrm{Cl}(X)\subseteq\mathcal{P}(X)$ the set of _cliques_ of $X$

$\mathrm{Cl}(X)\leavevmode\nobreak\ \leavevmode\nobreak\ =\leavevmode\nobreak\
\leavevmode\nobreak\ \\{S\in\mathcal{P}(X)\mid\forall x\;y\in
S.\;x\coh_{X}y\\}$

We now define the functor
$F:\mathcal{M}_{\mathrm{coh}}\to(\mathcal{M}_{\mathrm{aff}})_{\with}$ on
objects as

$F\left(\bigodot_{x\in X}A_{x}\right)\leavevmode\nobreak\ \leavevmode\nobreak\
=\leavevmode\nobreak\ \leavevmode\nobreak\
\bigwith_{S\in\mathrm{Cl}(X)}\bigotimes_{x\in S}A_{x}$

As for morphisms, first recall that a morphism
$(R,\alpha)\in\mathsf{Hom}_{\mathcal{M}_{\mathrm{coh}}}\left(\bigodot_{x\in
X}A_{x},\bigodot_{y\in Y}B_{y}\right)$ consists of a linear map
$R\in\mathsf{Hom}_{{\sf FinCoh}}\left(Y,X\right)$ and a family

$(\alpha_{y})_{y\in\|Y\|}\in\prod_{y\in\|Y\|}\mathsf{Hom}_{\mathcal{M}}\left((A_{x})_{(y,x)\in
R},B_{y}\right)$

We set out to define

$F(R,\alpha)\in\mathsf{Hom}_{(\mathcal{M}_{\mathrm{aff}})_{\with}}\left(F\left(\bigotimes_{x\in
S}A_{x}\right),F\left(\bigotimes_{y\in S^{\prime}}B_{y}\right)\right)$

recalling that

$\begin{array}[]{l}\displaystyle\mathsf{Hom}_{(\mathcal{M}_{\mathrm{aff}})_{\with}}\left(F\left(\bigotimes_{x\in
S}A_{x}\right),F\left(\bigotimes_{y\in S^{\prime}}B_{y}\right)\right)\\\ \\\
\hskip 100.00015pt=\leavevmode\nobreak\ \leavevmode\nobreak\
\displaystyle\prod_{S^{\prime}\in\mathrm{Cl}(Y)}\sum_{S\in\mathrm{Cl}(X)}\sum_{f:S\rightharpoonup
S^{\prime}}\prod_{y\in
S^{\prime}}\mathsf{Hom}_{\mathcal{M}}\left((A_{x})_{x\in
f^{-1}(x)},B_{y}\right)\end{array}$

So fixing $S^{\prime}\in\mathrm{Cl}(Y)$ and recall that $R$ being linear means
that we have

$(y,x)\in R\wedge(y^{\prime},x)\in
R\qquad\Rightarrow\qquad\left\\{\begin{array}[]{lcll}y\coh_{Y}y^{\prime}&\Rightarrow&x\coh_{X}x^{\prime}&(1)\\\
x=x^{\prime}&\Rightarrow&y\incoh_{Y}y^{\prime}&(2)\\\ \end{array}\right.$

In particular, $(1)$ implies that $\\{x\in\|X\|\mid(y,x)\in R\\}$ is a clique;
we take that to be $S$. $(2)$, and the fact that $y\coh_{Y}y^{\prime}\wedge
y\incoh_{Y}y^{\prime}\Rightarrow y=y^{\prime}$, imply that $R$ determines a
(total) function $S\rightharpoonup S^{\prime}$, which we take to be $f$.
Finally, once $y\in S^{\prime}$ is fixed, we pick the component $\alpha_{y}$
to complete the definition, which makes sense as $f^{-1}(y)=\\{x\in
S\mid(y,x)\in R\\}=\\{x\in\|X\|\mid(y,x)\in R)\\}$. This completes the
definition of $F(R,\alpha)$; we leave checking functoriality to the reader.

Now, we turn to defining a morphism of streaming setting
$\mathfrak{M}_{\mathrm{coh}}\to(\mathfrak{M}_{\mathrm{aff}})_{\with}$ from
$F$. To this end, we must first equip $F$ with a lax monoidal structure, that
is to define $(\mathcal{M}_{\mathrm{aff}})_{\with}$-maps

$m^{0}:{\mathbf{I}_{\mathrm{aff}}}_{\with}\to
F(\mathbf{I}_{\mathrm{coh}})\quad\;m^{2}:F\left(\bigodot_{x\in
X}A_{x}\right)\otimes F\left(\bigodot_{y\in Y}B_{y}\right)\to
F\left(\left[\bigodot_{x\in X}A_{x}\right]\otimes\left[\bigodot_{y\in
Y}B_{y}\right]\right)$

satisfying the relevant coherence diagrams. We do not check them here, but
indicate how to build those two maps. $m^{0}$ arises as an obvious isomorphism
$F(\mathbf{I}_{\mathrm{coh}})\cong\mathbf{I}_{\mathrm{aff}}$. $m^{2}$ is also
an isomorphism, which may be computed as per Figure 15.

$\displaystyle F\left(\bigodot_{x\in X}A_{x}\right)\otimes
F\left(\bigodot_{y\in Y}B_{y}\right)\qquad$
$\displaystyle\cong\qquad\left(\bigwith_{S\in\mathrm{Cl}(X)}\bigotimes_{x\in
S}A_{x}\right)\otimes\left(\bigwith_{S^{\prime}\in\mathrm{Cl}(Y)}\bigotimes_{y\in
S^{\prime}}B_{y}\right)$
$\displaystyle\cong\qquad\bigwith\limits_{\begin{subarray}{c}S\in\mathrm{Cl}(X)\\\
S^{\prime}\in\mathrm{Cl}(Y)\end{subarray}}\left(\bigotimes_{x\in
X}A_{x}\right)\otimes\left(\bigotimes_{y\in Y}B_{y}\right)$
$\displaystyle\cong\qquad\bigwith_{S\in\mathrm{Cl}(X\with Y)}\bigotimes_{z\in
S}C_{z}$ $\displaystyle\cong\qquad F\left(\bigodot_{z\in X\with
Y}C_{z}\right)$ $\displaystyle\cong\qquad F\left(\left(\bigodot_{x\in
X}A_{x}\right)\otimes\left(\bigodot_{y\in Y}B_{y}\right)\right)$ Figure 15.
The main structural natural isomorphism making the functor
$\mathcal{M}_{\mathrm{coh}}\to(\mathcal{M}_{\mathrm{aff}})_{\with}$ strong
monoidal, writing $A_{x}$ for $C_{\mathsf{in}_{1}(x)}$ and $B_{y}$ for
$C_{\mathsf{in}_{2}(y)}$.

Finally, there is a canonical isomorphism $F(\Bot)\cong\Bot$ which allows to
complete the definition of the morphism
$\mathfrak{M}_{\mathrm{coh}}\to(\mathfrak{M}_{\mathrm{aff}})_{\with}$.

We thus conclude this section by first specializing the above to the case
$\mathcal{M}=\mathcal{TR}^{\leq 1}$, and then making a final tangential
observation.

######  Lemma 68.

There are morphisms of streaming settings $\mathfrak{TR}^{\leq
1}_{\with}\to\mathfrak{TR}^{\incoh,\leq 1}\to\mathfrak{TR}^{\leq 1}_{\with}$.
In particular, $\mathfrak{TR}^{\leq 1}_{\with}$-BRTTs compute exactly the
regular functions.

######  Remark 69.

One idea that one could take from Hu and Joyal’s coherence completion [HJ99] –
but that we do not explore further here – is to look at objects whose indexing
coherence spaces are (up to isomorphism) generated from singletons by the
$\with/\oplus$ operations of ${\sf FinCoh}$. (Those are called “contractible”
in [HJ99, Section 4], and considering coherence spaces as undirected graphs,
this corresponds to the classical notion of _cograph_ in combinatorics.)

In the case of the coherence completion of some category $\mathcal{C}$, the
full subcategory spanned by such objects turns out to be the free completion
of $\mathcal{C}$ under finite products and coproducts (which differs from our
$(-)_{\oplus\with}$ in not making ‘$\with$’ distribute over ‘$\oplus$’); this
is formalized as a universal property in [HJ99, Theorem 4.3]. In the same
vein, we conjecture that the full subcategory of $\mathcal{M}_{\mathrm{coh}}$
consisting of cograph-indexed objects – that is, of objects that are generated
from those of $\mathcal{M}$ by means of the operations $\otimes/\with$ in
$\mathcal{M}_{\mathrm{coh}}$ – is in some way the _free affine symmetric
monoidal category with products generated by the multicategory $\mathcal{M}$_.

###  5.5. $\mathcal{TR}_{\oplus\with}$ is monoidal closed

Now, we consider the category $\mathcal{TR}_{\oplus\with}$ in the context of
trees. Much like with strings, this category is symmetric monoidal monoidal
closed with finite products and coproducts, which makes it an ideal target to
compile $\lambda\ell^{\oplus\with}$-terms. This structure over
$\mathcal{TR}_{\oplus\with}$ is obtained in the same way as for strings: the
monoidal product over $\mathcal{TR}$ is defined as distributing over formal
sums and products and the usual products and coproducts are created by the
$(-)_{\oplus\with}$ completion. Similarly, monoidal closure can be obtained in
a generic way once we show that the objects coming from $\mathcal{TR}$ have
internal homsets $\mathcal{TR}_{\oplus}$ (echoing Lemma 36). This section is
mostly dedicated to proving this fact, whose proof relies on decomposing
linear trees in a similar way as in Lemma 57.

######  Lemma 70.

For any two objects $\bf R$ and $\bf S$ of $\mathcal{TR}$, there is an
internal hom $\iota_{\oplus}(\bf R)\multimap\iota_{\oplus}(\bf S)$ in
$\mathcal{TR}_{\oplus}$.

######  Proof 5.11.

First, we treat the special case where ${\bf S}=\mathcal{I}(U)$ for some
finite set $U$. To make sense of the definition of $\iota_{\oplus}({\bf
R})\multimap\iota_{\oplus}(\mathcal{I}(U))$ it is helpful to notice that it
will ultimately induce an isomorphism

$\mathsf{Hom}_{\mathcal{TR}_{\oplus}}\left(\top,\iota_{\oplus}({\bf
R})\multimap\iota_{\oplus}(\mathcal{I}(U))\right)\cong\mathsf{Hom}_{\mathcal{TR}}\left({\bf
R},\mathcal{I}(U)\right)\cong\mathbf{LTree}_{\bf\Gamma}({\bf
R}\otimes\mathcal{O}(U))$

so, recalling that objects of $\mathcal{TR}_{\oplus}$ are of the shape
$\bigoplus_{i\in I}\bigotimes_{j\in J_{i}}\mathcal{I}(V_{j})$ for $V_{j}$
being finite sets, the operational intuition is that one may code trees with
“holes with arity” into some bounded finitary data (which we may informally
call a partitioning tree) plus finitely many trees containing holes “without
arity”; this bijection is pictured in Figure 16.

Figure 16. Decomposition of a map of
$\mathsf{Hom}_{\mathcal{TR}(\\{a:2,b:1,c:0\\})}\left(\\{x:3,y:3\\},\mathcal{I}(7)\right)$
(which is defined as
$\mathbf{LTree}_{\\{a:2,b:1,c:0\\}}(\\{x:3,y:3\\}\otimes\mathcal{O}(7))$) as a
tuple consisting of a partitioning tree and trees without the letters $x$ and
$y$.

As with Lemma 57, we will not use this as our official definition for the
internal homset, but rather use the following recursive definition:

  * •

If ${\bf R}=\top$, set $\iota_{\oplus}({\bf
R})\multimap\iota_{\oplus}(\mathcal{I}(U))\leavevmode\nobreak\
=\leavevmode\nobreak\ \iota_{\oplus}(\mathcal{I}(U))$.

  * •

Otherwise, define $\iota_{\oplus}({\bf
R})\multimap\iota_{\oplus}(\mathcal{I}(U))$ as

$\bigoplus_{U=V\uplus
W}\iota_{\oplus}(\mathcal{I}(V+1))\otimes\left(\bigoplus_{b\in{\bf\Gamma}}\left({\bf
R}\multimap_{b}\mathcal{I}(W)\right)\oplus\bigoplus_{r\in R}\left({\bf
R}\multimap_{r}\mathcal{I}(W)\right)\right)\\\ \\\ $

where ${\bf R}\multimap_{r}\mathcal{I}(W)$ and ${\bf
R}\multimap_{b}\mathcal{I}(W)$ are auxiliary definitions which correspond to
the following situations (recalling that morphisms can be regarded as trees):

    * –

$\iota_{\oplus}(\mathcal{I}(V+1))\otimes\left({\bf
R}\multimap_{r}\mathcal{I}(W)\right)$ correspond to morphisms such that there
is a _unique_ minimal path leading from the root to a node labelled by a
letter in $R$, and that letter is $r$. The second component ${\bf
R}\multimap_{r}\mathcal{I}(W)$ is meant to include the immediate subtrees of
that node while the first $\iota_{\oplus}(\mathcal{I}(V+1))$ contains the tree
where a nullary node labeled is inserted instead of that node. The combination
of both these data and $r$ allows to recover the original morphism.

    * –

$\bigoplus_{b\in{\bf\Gamma}}\iota_{\oplus}(\mathcal{I}(V+1))\otimes{\bf
R}\multimap_{b}\mathcal{I}(W)$ correspond to all the other morphisms. In such
a case there is a topmost node labelled by some letter $b$ of $\bf\Gamma$ with
which has at least two distinct immediate subtrees which have at least one
node of $R$ each. Similarly to the first subcase, ${\bf
R}\multimap_{b}\mathcal{I}(W)$ is intended to include the immediate subtrees
of that node labeled by $b$ while $\iota_{\oplus}(\mathcal{I}(V+1))$ contains
the tree where a nullary node labeled is inserted instead of that node. The
combination of these data and $b$ allows to recover the original morphism.

Their formal definition is as follows:

$\begin{array}[]{*4{>{\displaystyle}l}}&{\bf
R}\multimap_{b}\mathcal{I}(W)&=&\bigoplus\limits_{\begin{subarray}{c}f:W\to\mathrm{ar}(b)\\\
g:R\to\mathrm{ar}(b)\\\ g\text{
nonconstant}\end{subarray}}\bigotimes\limits_{x\in\mathrm{ar}(\Gamma)}\iota_{\oplus}({\bf
R}\upharpoonright g^{-1}(x))\multimap\iota_{\oplus}(f^{-1}(x))\\\ \\\ &{\bf
R}\multimap_{r}\mathcal{I}(W)&=&\bigoplus\limits_{\begin{subarray}{c}f:W\to\mathrm{ar}(r)\\\
g:R\setminus\\{r\\}\to\mathrm{ar}(r)\end{subarray}}\bigotimes\limits_{x\in\mathrm{ar}(r)}\iota_{\oplus}({\bf
R}\upharpoonright g^{-1}(x))\multimap\iota_{\oplus}(f^{-1}(x))\end{array}$

Note that the definitions of $\iota_{\oplus}({\bf
R})\multimap\iota_{\oplus}(\mathcal{I}(U))$, ${\bf
R}\multimap_{b}\mathcal{I}(W)$ and ${\bf R}\multimap_{r}\mathcal{I}(W)$
mutually depend on one another. Still this is is well-defined as the
definitions of ${\bf R}\multimap_{b}\mathcal{I}(W)$ and ${\bf
R}\multimap_{r}\mathcal{I}(W)$ only require $\iota_{\oplus}({\bf
S})\multimap\iota_{\oplus}(\mathcal{I}(V))$ for ${\bf S}$ strictly smaller
than ${\bf R}$.

We now describe the associated evaluation map

$\mathrm{ev}_{{\bf R},\mathcal{I}(U)}\leavevmode\nobreak\ \leavevmode\nobreak\
:\leavevmode\nobreak\ \leavevmode\nobreak\ (\iota_{\oplus}({\bf
R})\multimap\iota_{\oplus}(\mathcal{I}(U)))\otimes{\bf R}\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathcal{I}(U)$

also by recursion over $\bf R$.

  * •

If ${\bf R}=\top$, it is the identity.

  * •

Otherwise, we need to provide maps

$\left(\mathcal{I}(V+1)\otimes\left(\bigoplus_{b\in{\bf\Gamma}}\left({\bf
R}\multimap_{b}\mathcal{I}(W)\right)\oplus\bigoplus_{r\in R}\left({\bf
R}\multimap_{r}\mathcal{I}(W)\right)\right)\right)\otimes{\bf
R}\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \mathcal{I}(U)$

for every decomposition $U=V\uplus W$, the intuition being that
$\mathcal{I}(V+1)$ is a context containing the top of the tree corresponding
to the function we want to apply. Therefore, once we provide a map

$\left(\bigoplus_{b\in{\bf\Gamma}}\left({\bf
R}\multimap_{b}\mathcal{I}(W)\right)\oplus\bigoplus_{r\in R}\left({\bf
R}\multimap_{r}\mathcal{I}(W)\right)\right)\otimes{\bf R}\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathcal{I}(W)$

we may post-compose it with
$\mathcal{I}(V+1)\otimes\mathcal{I}(W)\to\mathcal{I}(V+W)\cong\mathcal{I}(V\uplus
W)=\mathcal{I}(U)$ to define $\mathrm{ev}_{{\bf R}\multimap\mathcal{I}(U)}$.
Recalling that $\otimes$ distributes over $\oplus$, it suffices to provide
specialized maps

$\mathrm{ev}^{b}_{{\bf R},\mathcal{I}(W)}:{\bf
R}\multimap_{b}\mathcal{I}(W)\otimes{\bf
R}\to\mathcal{I}(W)\quad\text{and}\quad\mathrm{ev}^{r}_{{\bf
R},\mathcal{I}(W)}:{\bf R}\multimap_{r}\mathcal{I}(W)\otimes{\bf
R}\to\mathcal{I}(W)$

for $b\in\Gamma$ and $r\in R$, which we describe now.

    * –

For $\mathrm{ev}^{b}_{{\bf R},\mathcal{I}(W)}$, it suffices to define a family
of $\mathcal{TR}$-maps indexed by $f:W\to\mathrm{ar}(b)$ and
$g:R\to\mathrm{ar}(b)$ with $g$ non-constant

$\displaystyle\left(\bigotimes_{x\in\mathrm{ar}(\Gamma)}({\bf
R}\upharpoonright g^{-1}(x))\multimap\mathcal{I}(f^{-1}(x))\right)\otimes{\bf
R}\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \mathcal{I}(W)$

Recall that $b$ can be seen as tree constructor and induces a canonical map

$\overline{b}\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\
\bigotimes_{x\in\mathrm{ar}(b)}\mathcal{I}(f^{-1}(x))\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathcal{I}(W)$

Using the induction hypothesis, we have evaluation maps

$\left(({\bf R}\upharpoonright
g^{-1}(x))\multimap\mathcal{I}(f^{-1}(x))\right)\otimes({\bf R}\upharpoonright
g^{-1}(x))\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \mathcal{I}(W)$

We can then compose $\overline{b}$ with the product of those maps over
$x\in\mathrm{ar}(b)$ and then the isomorphism ${\bf
R}\cong\bigotimes_{x\in\mathrm{ar}(b)}{\bf R}\upharpoonright f^{-1}(x)$ to
conclude the definition of $\mathrm{ev}^{b}_{{\bf R},\mathcal{I}(W)}$.

    * –

For $\mathrm{ev}^{r}_{{\bf R},\mathcal{I}(W)}$, it suffices to define a family
of $\mathcal{TR}$-maps indexed by $f:W\to\mathrm{ar}(r)$ and
$g:R\setminus\\{r\\}\to\mathrm{ar}(r)$

$\left(\bigotimes_{x\in\mathrm{ar}(\Gamma)}({\bf R}\upharpoonright
g^{-1}(x))\multimap\mathcal{I}(f^{-1}(x))\right)\otimes{\bf
R}\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \mathcal{I}(W)$

By exploiting the isomorphism ${\bf
R}\cong\mathcal{I}(\mathrm{ar}(r))\otimes\bigotimes_{x\in\mathrm{ar}(r)}({\bf
R}\upharpoonright g^{-1}(x))$ and using the inductive hypothesis as in the
previous case, we obtain a map

$\left(\bigotimes_{x\in\mathrm{ar}(\Gamma)}({\bf R}\upharpoonright
g^{-1}(x))\multimap\mathcal{I}(f^{-1}(x))\right)\otimes{\bf
R}\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\displaystyle\mathcal{I}(\mathrm{ar}(r))\otimes\bigotimes_{x\in\mathrm{ar}(r)}\mathcal{I}(f^{-1}(x))$

and we may conclude by post-composing by the map

$\mathcal{I}(\mathrm{ar}(r))\otimes\bigotimes_{x\in\mathrm{ar}(r)}\mathcal{I}(f^{-1}(x))\to\mathcal{I}(W)$

which is induced by the depth-$2$ tree whose root corresponds to the first
component, whose children correspond to the successive elements of
$\bigotimes_{x\in\mathrm{ar}(r)}\mathcal{I}(f^{-1}(x))$ and other leaves are
in $W$.

While the definition is a bit wordy, there is then little difficulty in
checking that this yields the expected universal property.

---
$\textstyle{\iota_{\oplus}({\bf
R}\multimap\mathcal{I}(U))\otimes\iota_{\oplus}(\mathcal{I}(U))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\iota_{\oplus}(\mathcal{I}(U))}$$\textstyle{A\otimes\iota_{\oplus}({\bf
R})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Lambda(h)\otimes\mathrm{id}}$$\scriptstyle{h}$

One needs then to extend the definition for the general case where $\bf S$ is
not necessarily $\mathcal{I}(U)$; this is done using a similar approach as for
strings, by using a coproduct over partial maps $R\rightharpoonup S$ tracking
which letter of the input participates in which letter of the output, and
employing the particular case where there is one letter in the
output272727This could be factored out as a more general result concerning the
existence of internal homsets in categories of the shape
$\mathcal{M}_{\mathrm{aff}}$ for multicategories $\mathcal{M}$.

$\iota_{\oplus}({\bf R})\multimap\iota_{\oplus}({\bf S})\leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
\bigoplus_{f:R\rightharpoonup S}\bigotimes_{s\in S}\iota_{\oplus}({\bf
R}\upharpoonright
f^{-1}(s))\multimap\iota_{\oplus}(\mathcal{I}(\mathrm{ar}(s)))$

The evaluation function can then be extended and the universal property
accordingly lifted to the more general case.

The above lemma tells us that $\mathcal{TR}_{\oplus\with}$ satisfies the
premises of Theorem 47, hence:

######  Theorem 71.

The category $\mathcal{TR}_{\oplus\with}$ has cartesian products, coproducts
and a symmetric monoidal _closed_ structure.

######  Remark 72.

Given the close relationship between the constructions
$((-)_{\mathrm{aff}})_{\with}$ and $(-)_{\mathrm{coh}}$, it seems plausible
that $(\mathcal{TR}_{\mathrm{coh}})_{\oplus}$ could be monoidal closed (we
know that it has products, coproducts and a symmetric monoidal structure). We
leave this question to further work.

In other words, $\mathcal{TR}_{\oplus\with}$ provides a categorical semantics
for the purely linear fragment of the $\lambda\ell^{\oplus\with}$-calculus.
Concretely, by a suitable adaptation of Lemma 27 to tree streaming settings,
we finally have:

######  Corollary 73.

There is a morphism of streaming settings
$\mathfrak{L}\to\mathfrak{TR}_{\oplus\with}$.

###  5.6. Preservation properties of finite completions

We have now proven all of the combinatorial results leading to the main
theorem for trees. At this stage, we only need to make explicit a few
preservation properties of the completions $(-)_{\oplus}$ and $(-)_{\with}$.
We only state the minimal requirements that we need to proceed282828 The
following, which would entail these requirements, should hold (but we have not
checked it): the completions $(-)_{\oplus}$ and $(-)_{\with}$ should behave as
pseudo-monads over the 2-category of tree streaming settings, admitting a
pseudo-distributive law $((-)_{\oplus})_{\with}\to((-)_{\with})_{\oplus}$
giving rise to the pseudo-monad $(-)_{\oplus\with}$..

######  Lemma 74.

Let $\square\in\\{\oplus,\with,\oplus\with\\}$ and $\mathfrak{C},\mathfrak{D}$
be streaming settings. Then if there is a morphism
$\mathfrak{C}\to\mathfrak{D}$, there is also a morphism
$\mathfrak{C}_{\square}\to\mathfrak{C}_{\square}$.

######  Proof 5.12 (Proof idea).

Let us only discuss the case $\square=\oplus$ and assume that we have a
streaming setting morphism whose underlying lax monoidal functor is
$F:\mathcal{C}\to\mathcal{D}$. Then we consider
$F_{\oplus}:\mathcal{C}_{\oplus}\to\mathcal{D}_{\oplus}$ defined using the
universal property of $\mathcal{C}_{\oplus}$ from the functor
$\iota_{\oplus}\circ F:\mathcal{C}\to\mathcal{D}_{\oplus}$ such that

$F_{\oplus}\left(\bigoplus_{u\in
U}\iota_{\oplus}(C_{u})\right)\leavevmode\nobreak\ \leavevmode\nobreak\
=\leavevmode\nobreak\ \leavevmode\nobreak\ \bigoplus_{u\in
U}\iota_{\oplus}(F(C_{u}))$

so that $F_{\oplus}$ inherits a lax monoidal structure from $F$ by lifting the
relevant maps functorially. For instance, we have
$\iota_{\oplus}(\mathbf{I})\to\iota_{\oplus}(F(\mathbf{I}))=F_{\oplus}(\mathbf{I})$
for the unit. We leave checking the coherence diagram, the case of the binary
tensor to the reader, as well as checking that the rest of the structure of
morphisms of streaming settings lift accordingly.

######  Lemma 75.

Let $\mathfrak{C}$ be a streaming setting. Then there are morphisms of
streaming settings
$\mathfrak{C}_{\oplus\with}\to(\mathfrak{C}_{\oplus})_{\oplus\with}$ and
$(\mathfrak{C}_{\oplus})_{\oplus\with}\to\mathfrak{C}_{\oplus\with}$.

######  Proof 5.13 (Proof idea).

The first morphism can be obtained using Lemma 74 with the morphism of
streaming setting $\mathfrak{C}\to\mathfrak{C}_{\oplus}$ corresponding to
$\iota_{\oplus}$. The second morphism can be written as a composite

$\textstyle{(\mathfrak{C}_{\oplus})_{\oplus\with}\cong((\mathfrak{C}_{\oplus})_{\with})_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\mathfrak{Dist}_{\mathfrak{C}})_{\oplus}}$$\textstyle{((\mathfrak{C}_{\with})_{\oplus})_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathfrak{Mu}_{\mathfrak{C}_{\with}}}$$\textstyle{(\mathfrak{C}_{\with})_{\oplus}\cong\mathfrak{C}_{\oplus\with}}$

where $(\mathfrak{Dist}_{\mathfrak{C}})_{\oplus}$ is obtained from a morphism
$\mathfrak{Dist}_{\mathfrak{C}}:(\mathfrak{C}_{\oplus})_{\with}\to(\mathfrak{C}_{\with})_{\oplus}$
by Lemma 74. $\mathfrak{Dist}_{\mathfrak{C}}$ itself is built from a functor
$D_{\mathcal{C}}:(\mathcal{C}_{\oplus})_{\with}\to(\mathcal{C}_{\with})_{\oplus}$
defined on object following the mantra “products distribute over coproducts”.

$D_{\mathcal{C}}\left(\bigwith_{x\in X}\iota_{\with}\left(\bigoplus_{u\in
U_{x}}\iota_{\oplus}(C_{x,u})\right)\right)\leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
\bigoplus_{F\in\prod_{x}U_{x}}\iota_{\oplus}\left(\bigwith_{x\in
X}\iota_{\with}(C_{x,u})\right)$

On the other hand, the functor $M:\mathcal{C}$ which is part of
$\mathfrak{Mu}_{\mathfrak{C}}$ is obtained by using the universal property of
$(-)_{\oplus}$ so that

$M\left(\bigoplus_{u\in U}\iota_{\oplus}\left(\bigoplus_{v\in
V}\iota_{\oplus}(C_{u,v})\right)\right)\leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
\bigoplus_{(u,v)}\iota_{\oplus}(C_{u,v})$

###  5.7. Proof of the main result on trees

We can now give the proof of Theorem 2, which can be summarized as the string
of equalities

$\begin{array}[]{lcl@{\quad}l}\lambda\ell^{\oplus\with}&=&\text{single-state
$\mathfrak{L}$-BRTTs}&\text{\small by Lemma\leavevmode\nobreak\
\ref{lem:lamlbrtt}}\\\ &=&\text{single-state $\mathfrak{TR}^{\incoh,\leq
1}_{\oplus}$-BRTTs}&(\dagger)\\\ &=&\text{$\mathfrak{TR}^{\incoh,\leq
1}$-BRTTs}&\text{\small by Theorem\leavevmode\nobreak\ \ref{thm:oplus-brtt-
conservative}}\\\ &=&\text{regular tree functions}&\text{\small by
Proposition\leavevmode\nobreak\ \ref{prop:brtt-regular}}\end{array}$

Note that applying Theorem 55 in the last step requires that objects of
$\mathcal{TR}^{\incoh,\leq 1}$ have unitary support, which is easily checked
for output alphabets ${\bf\Gamma}$ containing at least one letter of arity
$\varnothing$. It remains to justify step $(\dagger)$, i.e., that single-state
$\mathfrak{L}$-BRTTs and $\mathfrak{TR}^{\incoh,\leq 1}_{\oplus}$-BRTTs are
equi-expressive. By Lemma 54, it suffices to have morphisms of streaming
settings both ways $\mathfrak{L}\leftrightarrow\mathfrak{TR}^{\incoh,\leq
1}_{\oplus}$ to conclude. They may be obtained as the following composites
(where we leave implicit the uses of Lemma 74 and some easily inferrable
steps).

$\textstyle{\mathfrak{L}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Cor.
73$\textstyle{\mathfrak{TR}_{\oplus\with}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lem.
75Cor.
60$\textstyle{(\mathfrak{TR}_{\oplus})_{\oplus\with}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lem
57$\textstyle{(\mathfrak{TR}^{\leq
1}_{\oplus})_{\oplus\with}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lem.
75$\textstyle{\mathfrak{TR}^{\leq
1}_{\oplus\with}\cong\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces(\mathfrak{TR}^{\leq
1}_{\with})_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lem.
68$\textstyle{\mathfrak{TR}^{\incoh,\leq
1}_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

##  6\. Conclusion & further work

We have proven that the tree (and string) functions definable at type
$\mathrm{Tree}_{\bf\Sigma}[A]\multimap\mathrm{Tree}_{\bf\Gamma}$ in the
$\lambda\ell^{\oplus\with}$-calculus correspond exactly to regular functions.
To prove the non-trivial left-to-right inclusion, we used a syntactic lemma
for $\lambda\ell^{\oplus\with}$-terms allowing to compile those terms into a
kind of transducer model using purely linear $\lambda\ell^{\oplus\with}$-terms
as its memory ($\mathfrak{L}$-BRTTs). We then showed in a principled way that
those transducers are equivalent to the more standard single-use-restricted
Bottom-up Ranked Tree Transducers (expressed as $\mathfrak{TR}^{\incoh,\leq
1}$-BRTTs in our framework) which capture regular tree functions. Along the
way, we revisited a few results on string transducers under the light of our
categorical framework, exhibiting some points of convergence with our
semantics for $\lambda\ell^{\oplus\with}$-terms.

There are a number of ways one could plan on expanding this work. We list some
of the most relevant problems, regarding the definable functions between
strings and trees in various $\lambda$-calculi, that we expect could be
tackled using similar methods or minor variations of our setting.

#### Removing the additive connectives

$\lambda\ell^{\oplus\with}$ features the additive connectives $\oplus$ and
$\with$ (as well as the relevant units $0$ and $\top$). A natural question is
whether all regular functions are still encodable if we remove access to those
connectives and use the $\lambda\kern-0.50003pt\mbox{ \hskip 5.00002pt{1 0 0.4
1} \hbox to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}} }$-calculus, an
_affine_ version of $\lambda\ell^{\oplus\with}$ without those connectives; for
strings, this is first half of [NP20, Claim 6.2].

In a sense, we went further than that in showing that
$\lambda\ell^{\oplus\with}$-definable functions are regular, since it can be
checked that all $\lambda\kern-0.50003pt\mbox{ \hskip 5.00002pt{1 0 0.4 1}
\hbox to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}} }$-definable string-
to-string functions are also $\lambda\ell^{\oplus\with}$-definable. However,
we did not give evidence for the converse direction, as our encoding of states
of BRTTs use the additive connectives. We believe this can be remedied by
leveraging our previous work on encoding sequential transducers [NP20,
Sections 4-5] (that relies on the highly non-trivial Krohn-Rhodes theorem).

As for functions taking trees as input, we suspect that the
$\lambda\kern-0.50003pt\mbox{ \hskip 5.00002pt{1 0 0.4 1} \hbox
to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}} }$-calculus is _strictly
less expressive_ than copyless BRTTs ($\mathfrak{TR}$-BRTTs) – in fact, that
$\lambda\kern-0.50003pt\mbox{ \hskip 5.00002pt{1 0 0.4 1} \hbox
to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}} }$-terms are even unable to
recognize all regular tree _languages_. We expect that this can be shown by
interpreting purely affine $\lambda\kern-0.50003pt\mbox{ \hskip 5.00002pt{1 0
0.4 1} \hbox to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}} }$-terms into
(a variant of) the geometry of interaction semantics mentioned in Example 18.
Our intent is to deduce from this that $\lambda\kern-0.50003pt\mbox{ \hskip
5.00002pt{1 0 0.4 1} \hbox to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}}
}$-definable languages can be recognized by _tree-walking automata_ – which
are indeed a natural extension to trees of the two-way automata from Example
18 – and some regular tree languages are known to be unrecognizable by such
devices [BC08].

Anecdotally, we show in Appendix F that removing the additive disjunction
‘$\oplus$’ from the $\lambda\ell^{\oplus\with}$-calculus while keeping the
additive conjunction ‘$\with$’ does not affect the definability of tree
functions. While this is a routine application of a continuation-passing-style
transformation, the nice thing is that it can be entirely carried out at the
level of streaming settings.

#### Dropping commutativity

The second half of [NP20, Claim 6.2] raised the issue of definable string-to-
string transductions in the $\lambda\wp$-calculus, the restriction of the
$\lambda\kern-0.50003pt\mbox{ \hskip 5.00002pt{1 0 0.4 1} \hbox
to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}} }$-calculus to a _non-
commutative_ multiplicative structure. By analogy with the main result of
[NP20], which was that $\lambda\wp$-definable languages are star-free (i.e.
first-order definable) while $\lambda\kern-0.50003pt\mbox{ \hskip 5.00002pt{1
0 0.4 1} \hbox to0.0pt{\hss\leavevmode\hbox{\set@color\text{a}}} }$ defines
regular languages, the natural guess is that they correspond to _first-order
regular functions_. We expect non-commutative typing to translate into a
_planarity_ condition in the above-mentioned category of diagrams (close to a
free (non-symmetric) compact-closed category [KL80]).

The situation with trees looks more delicate, although trying to compare the
expressiveness of the $\lambda\wp$-calculus with the functional combinators
described in [BD20] might be a good starting point.

#### Duplicating the input

Going to higher complexities, but without escalating to the towers of
exponentials definable in the simply-typed $\lambda$-calculus, one natural
question is: how expressive are $\lambda\ell^{\oplus\with}$-terms of type
$\mathrm{Tree}_{\bf\Sigma}[\kappa]\to\mathrm{Tree}_{\bf\Gamma}$, for purely
linear $\kappa$? We expect that this problem could be tackled by reusing our
semantic interpretation of purely linear $\lambda\ell^{\oplus\with}$-terms
together with a suitable refinement of Lemma 25. Concerning the case of
strings, our current conjecture is that the expressible functions have
polynomial growth and form a strict subclass of _polyregular functions_
[Boj18, BKL19].

#### Semantic interpretation of exponentials

One frustrating aspect of our approach is that we need to rely on the
normalization of $\lambda\ell^{\oplus\with}$-terms and a special-purpose
syntactic lemma to dissect the term under consideration and extract the
relevant purely linear subterms before being able to go to semantic
interpretations and more high-level arguments. The reason behind this is that
our semantics does not interpret the non-linear arrow ‘$\to$’ or,
equivalently, a version of the exponential modality ‘$\oc$’ of linear logic.
It might be more pleasant to have more general semantic settings with those
features that still allow us to show our characterizations. Furthermore, such
a setting would be _necessary_ if we hope to tackle the question of the
expressiveness of functions
$\mathrm{Tree}_{\bf\Sigma}[A]\to\mathrm{Tree}_{\bf\Sigma}$ for general $A$
using semantic tools (this last variant of the problem is equivalent to the
setting of the simply-typed $\lambda$-calculus without linearity constraints).

## References

  * [AČ10] Rajeev Alur and Pavol Černý.  Expressiveness of streaming string transducers.  In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 1–12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010.  doi:10.4230/LIPIcs.FSTTCS.2010.1.
  * [AD11] Rajeev Alur and Jyotirmoy V. Deshmukh.  Nondeterministic streaming string transducers.  In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 1–20. Springer, 2011.  doi:10.1007/978-3-642-22012-8_1.
  * [AD17] Rajeev Alur and Loris D’Antoni.  Streaming Tree Transducers.  Journal of the ACM, 64(5):1–55, August 2017.  doi:10.1145/3092842.
  * [ADHS01] Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott.  Normalization by evaluation for typed lambda calculus with coproducts.  In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pages 303–310. IEEE Computer Society, 2001.  doi:10.1109/LICS.2001.932506.
  * [AFR14] Rajeev Alur, Adam Freilich, and Mukund Raghothaman.  Regular combinators for string transformations.  In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - CSL-LICS ’14, pages 1–10, Vienna, Austria, 2014. ACM Press.  doi:10.1145/2603088.2603151.
  * [AFT12] Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi.  Regular Transformations of Infinite Strings.  In 2012 27th Annual IEEE Symposium on Logic in Computer Science, pages 65–74, Dubrovnik, Croatia, June 2012. IEEE.  doi:10.1109/LICS.2012.18.
  * [Bar96] 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/.
  * [BB85] Corrado Böhm and Alessandro Berarducci.  Automatic synthesis of typed $\lambda$-programs on term algebras.  Theoretical Computer Science, 39:135–154, January 1985.  doi:10.1016/0304-3975(85)90135-5.
  * [BC08] 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.
  * [BC18] Mikołaj Bojańczyk and Wojciech Czerwiński.  An automata toolbox.  Lecture notes for a course at the University of Warsaw, 2018.  URL: https://www.mimuw.edu.pl/~bojan/paper/automata-toolbox-book.
  * [BD20] Mikołaj Bojańczyk and Amina Doumane.  First-order tree-to-tree functions.  In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany (online conference), July 8-11, 2020, pages 252–265. ACM, 2020.  doi:10.1145/3373718.3394785.
  * [BDBRDR18] Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca.  Characterizing polynomial and exponential complexity classes in elementary lambda-calculus.  Information and Computation, 261:55–77, August 2018.  doi:10.1016/j.ic.2018.05.005.
  * [BDK18] Mikołaj Bojańczyk, Laure Daviaud, and Shankara Narayanan Krishna.  Regular and First-Order List Functions.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS ’18, pages 125–134, Oxford, United Kingdom, 2018. ACM Press.  doi:10.1145/3209108.3209163.
  * [BDSW17] Michael Benedikt, Timothy Duff, Aditya Sharad, and James Worrell.  Polynomial automata: Zeroness and applications.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, Reykjavik, Iceland, June 2017. IEEE.  doi:10.1109/LICS.2017.8005101.
  * [BE00] 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.
  * [Bie94] Gavin M. Bierman.  On Intuitionistic Linear Logic.  Technical report UCAM-CL-TR-346, University of Cambridge, Computer Laboratory, August 1994.  URL: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.114.588&rep=rep1&type=pdf.
  * [BKL19] Mikołaj Bojańczyk, Sandra Kiefer, and Nathan Lhote.  String-to-String Interpretations With Polynomial-Size Output.  In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 106:1–106:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.  doi:10.4230/LIPIcs.ICALP.2019.106.
  * [BM10] Patrick Baillot and Damiano Mazza.  Linear Logic by Levels and Bounded Time Complexity.  Theoretical Computer Science, 411(2):470–503, January 2010.  doi:10.1016/j.tcs.2009.09.015.
  * [Boj] Mikołaj Bojańczyk.  Algebra for trees.  To appear in the Handbook of Automata Theory.  URL: https://www.mimuw.edu.pl/~bojan/papers/treealgs.pdf.
  * [Boj18] Mikołaj Bojańczyk.  Polyregular functions, 2018.  arXiv:1810.08760.
  * [CM19] 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.
  * [CP17a] Thomas Colcombet and Daniela Petrişan.  Automata and minimization.  ACM SIGLOG News, 4(2):4–27, May 2017.  doi:10.1145/3090064.3090066.
  * [CP17b] Thomas Colcombet and Daniela Petrişan.  Automata in the Category of Glued Vector Spaces.  In Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), volume 83 of Leibniz International Proceedings in Informatics (LIPIcs), pages 52:1–52:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017.  doi:10.4230/LIPIcs.MFCS.2017.52.
  * [CP20] Thomas Colcombet and Daniela Petrişan.  Automata Minimization: a Functorial Approach.  Logical Methods in Computer Science, 16(1), March 2020.  doi:10.23638/LMCS-16(1:32)2020.
  * [DGK18] Vrunda Dave, Paul Gastin, and Shankara Narayanan Krishna.  Regular Transducer Expressions for Regular Transformations.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS ’18, pages 315–324, Oxford, United Kingdom, 2018. ACM Press.  doi:10.1145/3209108.3209182.
  * [DJR18] Luc Dartois, Ismaël Jecker, and Pierre-Alain Reynier.  Aperiodic String Transducers.  International Journal of Foundations of Computer Science, 29(05):801–824, August 2018.  doi:10.1142/S0129054118420054.
  * [dP89] Valeria C. V. de Paiva.  The Dialectica categories.  In John W. Gray and Andre Scedrov, editors, Contemporary Mathematics, volume 92, pages 47–62. American Mathematical Society, Providence, Rhode Island, 1989.  doi:10.1090/conm/092/1003194.
  * [DP16] Henry DeYoung and Frank Pfenning.  Substructural proofs as automata.  In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 3–22, 2016.  doi:10.1007/978-3-319-47958-3_1.
  * [EH01] Joost Engelfriet and Hendrik Jan Hoogeboom.  MSO definable string transductions and two-way finite-state transducers.  ACM Transactions on Computational Logic, 2(2):216–254, April 2001\.  doi:10.1145/371316.371512.
  * [EM99] 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.
  * [ERS80] Joost Engelfriet, Grzegorz Rozenberg, and Giora Slutzki.  Tree transducers, L systems, and two-way machines.  Journal of Computer and System Sciences, 20(2):150–202, 1980.  doi:10.1016/0022-0000(80)90058-6.
  * [FLO83] Steven Fortune, Daniel Leivant, and Michael O’Donnell.  The Expressiveness of Simple and Second-Order Type Structures.  Journal of the ACM, 30(1):151–185, January 1983.  doi:10.1145/322358.322370.
  * [FR16] Emmanuel Filiot and Pierre-Alain Reynier.  Transducers, Logic and Algebra for Functions of Finite Words.  ACM SIGLOG News, 3(3):4–19, August 2016.  doi:10.1145/2984450.2984453.
  * [FR21] Emmanuel Filiot and Pierre-Alain Reynier.  Copyful streaming string transducers.  Fundamenta Informaticae, 178(1-2):59–76, January 2021.  doi:10.3233/FI-2021-1998.
  * [Gal20] Zeinab Galal.  A profunctorial scott semantics.  In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 16:1–16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.  doi:10.4230/LIPIcs.FSCD.2020.16.
  * [Gir86] Jean-Yves Girard.  The system F of variable types, fifteen years later.  Theoretical Computer Science, 45:159–192, January 1986.  doi:10.1016/0304-3975(86)90044-7.
  * [Gir87] Jean-Yves Girard.  Linear logic.  Theoretical Computer Science, 50(1):1–101, January 1987.  doi:10.1016/0304-3975(87)90045-4.
  * [Gir89] Jean-Yves Girard.  Towards a geometry of interaction.  In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 69–108. American Mathematical Society, Providence, RI, 1989.  Proceedings of a Summer Research Conference held June 14–20, 1987.  doi:10.1090/conm/092/1003197.
  * [Gir95] Jean-Yves Girard.  Linear logic: its syntax and semantics.  In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Notes, pages 1–42. Cambridge University Press, 1995.  doi:10.1017/CBO9780511629150.002.
  * [Gir96] Jean-Yves Girard.  Proof-nets: The parallel syntax for proof-theory.  In Logic and Algebra, pages 97–124. Marcel Dekker, 1996.
  * [Gir98] Jean-Yves Girard.  Light Linear Logic.  Information and Computation, 143(2):175–204, June 1998.  doi:10.1006/inco.1998.2700.
  * [GK13] Nicola Gambino and Joachim Kock.  Polynomial functors and polynomial monads.  In Mathematical Proceedings of the Cambridge Philosophical Society, volume 154, pages 153–192. Cambridge University Press, 2013.  doi:10.1017/S0305004112000394.
  * [GLS20] 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.
  * [Göd58] Kurt Gödel.  Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes.  Dialectica, 12(3-4):280–287, 1958.  doi:10.1111/j.1746-8361.1958.tb01464.x.
  * [Gre16] Charles Grellois.  Semantics of linear logic and higher-order model-checking.  PhD thesis, Université Paris 7, April 2016.  URL: https://tel.archives-ouvertes.fr/tel-01311150/.
  * [GRV09] Marco Gaboardi, Luca Roversi, and Luca Vercelli.  A By-Level Analysis of Multiplicative Exponential Linear Logic.  In Mathematical Foundations of Computer Science 2009, Lecture Notes in Computer Science, pages 344–355. Springer, Berlin, Heidelberg, August 2009.  doi:10.1007/978-3-642-03816-7_30.
  * [GSS92] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott.  Bounded linear logic: a modular approach to polynomial-time computability.  Theoretical Computer Science, 97(1):1–66, April 1992.  doi:10.1016/0304-3975(92)90386-T.
  * [Hed18] Jules Hedges.  Morphisms of open games.  In Sam Staton, editor, Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, volume 341 of Electronic Notes in Theoretical Computer Science, pages 151–177, 2018.  doi:10.1016/j.entcs.2018.11.008.
  * [HH16] Dominic Hughes and Willem Heijltjes.  Conflict nets: Efficient locally canonical MALL proof nets.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016, pages 437–446, New York, U. S. A., July 2016. ACM.  doi:10.1145/2933575.2934559.
  * [Hin03] Peter Hines.  A categorical framework for finite state machines.  Mathematical Structures in Computer Science, 13(3):451–480, 2003\.  doi:10.1017/S0960129503003931.
  * [HJ99] Hongde Hu and André Joyal.  Coherence completions of categories.  Theoretical Computer Science, 227(1):153–184, September 1999.  doi:10.1016/S0304-3975(99)00051-1.
  * [HK96] Gerd G. Hillebrand and Paris C. Kanellakis.  On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi.  In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pages 253–263. IEEE Computer Society, 1996\.  doi:10.1109/LICS.1996.561337.
  * [HKM96] Gerd G. Hillebrand, Paris C. Kanellakis, and Harry G. Mairson.  Database Query Languages Embedded in the Typed Lambda Calculus.  Information and Computation, 127(2):117–144, June 1996.  doi:10.1006/inco.1996.0055.
  * [Hof11] Pieter Hofstra.  The dialectica monad and its cousins.  In Bradd Hart, Thomas Kucera, Anand Pillay, Philip Scott, and Robert Seely, editors, Models, Logics, and Higher-Dimensional Categories: A Tribute to the Work of Mihály Makkai, volume 53 of CRM Proceedings and Lecture Notes. American Mathematical Society, Providence, Rhode Island, September 2011.  doi:10.1090/crmp/053.
  * [KL80] Gregory M. Kelly and Miguel L. Laplaza.  Coherence for compact closed categories.  Journal of pure and applied algebra, 19:193–213, 1980.  doi:10.1016/0022-4049(80)90101-2.
  * [Lam58] Joachim Lambek.  The mathematics of sentence structure.  The American Mathematical Monthly, 65(3):154–170, 1958.  URL: http://www.jstor.org/stable/2310058.
  * [Lin07] Sam Lindley.  Extensional rewriting with sums.  In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of Lecture Notes in Computer Science, pages 255–271. Springer, 2007.  doi:10.1007/978-3-540-73228-0_19.
  * [Mel09] Paul-André Melliès.  Categorical semantics of linear logic.  In Interactive models of computation and program behaviour, volume 27 of Panoramas et Synthèses, pages 1–196. Société Mathématique de France, 2009.  URL: https://www.irif.fr/~mellies/papers/panorama.pdf.
  * [Mel17] Paul-André Melliès.  Higher-order parity automata.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, Reykjavik, Iceland, June 2017. IEEE.  doi:10.1109/LICS.2017.8005077.
  * [ML98] Saunders Mac Lane.  Categories for the Working Mathematician (2nd edition.  Graduate Texts in Mathematics. Springer, 1998.
  * [MP19] 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.
  * [MS95] David E. Muller and Paul E. Schupp.  Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra.  Theoretical Computer Science, 141(1–2):69 – 107, 1995.  doi:10.1016/0304-3975(94)00214-4.
  * [MT03] Harry G. Mairson and Kazushige Terui.  On the computational complexity of cut-elimination in linear logic.  In Carlo Blundo and Cosimo Laneve, editors, Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings, volume 2841 of Lecture Notes in Computer Science, pages 23–36. Springer, 2003.  doi:10.1007/978-3-540-45208-9_4.
  * [MvG18] Sean K. Moss and Tamara von Glehn.  Dialectica models of type theory.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 739–748. ACM Press, 2018.  doi:10.1145/3209108.3209207.
  * [Ngu19] Lê Thành Dũng Nguyễn.  On the Elementary Affine Lambda-Calculus with and Without Fixed Points.  Electronic Proceedings in Theoretical Computer Science, 298:15–29, August 2019.  In Proceedings DICE-FOPARA 2019.  doi:10.4204/EPTCS.298.2.
  * [nLa20] nLab authors.  Semicartesian monoidal category.  http://ncatlab.org/nlab/show/semicartesian%20monoidal%20category, March 2020\.  Revision 24.
  * [NP19] Lê Thành Dũng Nguyễn and Pierre Pradic.  From normal functors to logarithmic space queries.  In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 123:1–123:15. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.  doi:10.4230/LIPIcs.ICALP.2019.123.
  * [NP20] Lê Thành Dũng Nguyễn and Pierre 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.
  * [PR18] Pierre Pradic and Colin Riba.  LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 849–858, New York, NY, USA, 2018. ACM.  doi:10.1145/3209108.3209195.
  * [PR19] Pierre Pradic and Colin Riba.  A dialectica-like interpretation of a linear MSO on infinite words.  In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, volume 11425 of Lecture Notes in Computer Science, pages 470–487. Springer, 2019.  doi:10.1007/978-3-030-17127-8_27.
  * [Rey93] John C. Reynolds.  The discoveries of continuations.  LISP and Symbolic Computation, 6(3):233–247, Nov 1993.  doi:10.1007/BF01019459.
  * [Rib20] Colin Riba.  Monoidal-closed categories of tree automata.  Mathematical Structures in Computer Science, 30(1):62–117, January 2020.  doi:10.1017/S0960129519000173.
  * [RR97] Simona Ronchi Della Rocca and Luca Roversi.  Lambda calculus and intuitionistic linear logic.  Studia Logica, 59(3):417–448, 1997.  doi:10.1023/A:1005092630115.
  * [Sch16] Gabriel Scherer.  Which types have a unique inhabitant? : Focusing on pure program equivalence. PhD thesis, Paris Diderot University, France, 2016.  URL: https://tel.archives-ouvertes.fr/tel-01309712.
  * [Ter12] Kazushige Terui.  Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus.  In 23rd International Conference on Rewriting Techniques and Applications (RTA’12), pages 323–338, 2012.  doi:10.4230/LIPIcs.RTA.2012.323.
  * [Til87] Bret Tilson.  Categories as algebra: An essential ingredient in the theory of monoids.  Journal of Pure and Applied Algebra, 48(1):83–198, September 1987\.  doi:10.1016/0022-4049(87)90108-3.
  * [vHKR+19] Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva.  Tree automata as algebras: Minimisation and determinisation.  In Markus Roggenbach and Ana Sokolova, editors, 8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019, June 3-6, 2019, London, United Kingdom, volume 139 of LIPIcs, pages 6:1–6:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  doi:10.4230/LIPIcs.CALCO.2019.6.
  * [Wad07] Philip Wadler.  The Girard–Reynolds isomorphism (second edition).  Theoretical Computer Science, 375(1-3):201–226, May 2007.  doi:10.1016/j.tcs.2006.12.042.
  * [Zai87] Marek Zaionc.  Word operation definable in the typed $\lambda$-calculus.  Theoretical Computer Science, 52(1):1–14, January 1987.  doi:10.1016/0304-3975(87)90077-6.

##  Appendix A Alur and D’Antoni’s Bottom-Up Ranked Tree Transducers

We give here a self-contained definition of the notion of BRTT corresponding
to regular tree functions, as they were designed in [AD17]. Since the paper
[AD17] is mainly concerned with transducers over unranked trees, the
information concerning the definition of BRTTs is spread over its sections
2.1, 3.7 and 3.8. We restrict here to binary trees (as in [AD17, Sections 3.7
and 3.8]) and avoid using multicategories.

[[AD17, p. 31:36]] The set $\mathrm{BinTree}(\Sigma)$ of _binary trees_ over
the alphabet $\Sigma$, and the set $\partial\mathrm{BinTree}(\Sigma)$ of _one-
hole binary trees_ are generated by the respective grammars

$T,U::=\lceil\cdot\rceil\mid a\lceil T,U\rceil\quad(a\in\Sigma)\qquad\qquad
T^{\prime},U^{\prime}::=\square\mid a\lceil T^{\prime},U\rceil\mid a\lceil
T,U^{\prime}\rceil\quad(a\in\Sigma)$

That is, $\mathrm{BinTree}(\Sigma)$ consists of binary trees whose leaves are
all equal to $\langle\rangle$ and whose nodes are labeled with letters in
$\Sigma$. As for $\partial\mathrm{BinTree}(\Sigma)$, it contains trees with
exactly one leaf labeled $\square$ instead of $\lceil\cdot\rceil$. This “hole”
$\square$ is intended to be substituted by a tree: for
$T^{\prime}\in\partial\mathrm{BinTree}(\Sigma)$ and
$U\in\mathrm{BinTree}(\Sigma)$, $T^{\prime}[U]$ denotes $T^{\prime}$ where
$\square$ has been replaced by $U$. [[AD17, p. 31:40]] The _binary tree
expressions_ ($E,F$ below, forming the set
$\mathrm{ExprBT}(\Sigma,V,V^{\prime})$) and _one-hole binary tree expressions_
($E^{\prime},F^{\prime}$ below, forming the set
$\mathrm{Expr}\partial\mathrm{BT}(\Sigma,V,V^{\prime})$) over the variable
sets $V$ and $V^{\prime}$ are generated by the grammar (with $x\in V$,
$x^{\prime}\in V^{\prime}$ and $a\in\Sigma$)

$E,F::=\lceil\cdot\rceil\mid x\mid a\lceil E,F\rceil\mid E^{\prime}[F]\qquad
E^{\prime},F^{\prime}:=\square\mid x^{\prime}\mid a\lceil
E^{\prime},F\rceil\mid a\lceil E,F^{\prime}\rceil\mid E^{\prime}[F^{\prime}]$

Given $\rho:V\to\mathrm{BinTree}(\Sigma)$ and
$\rho^{\prime}:V^{\prime}\to\partial\mathrm{BinTree}(\Sigma)$, one defines
$E(\rho,\rho^{\prime})\in\mathrm{BinTree}(\Sigma)$ for
$E\in\mathrm{ExprBT}(\Sigma)$ and
$E^{\prime}(\rho,\rho^{\prime})\in\partial\mathrm{BinTree}(\Sigma)$ for
$E\in\mathrm{Expr}\partial\mathrm{BT}(\Sigma)$ in the obvious way.

[[AD17, §3.7]] Let us fix an input alphabet $\Gamma$ and output alphabet
$\Sigma$. The set of _register assignments_ over two disjoint sets
$R,R^{\prime}$, whose elements are called _registers_ , is

$\mathcal{A}(\Sigma,R,R^{\prime})=\mathrm{ExprBT}(\Sigma,R_{\triangleleft\triangleright},R^{\prime}_{\triangleleft\triangleright})^{R}\times\mathrm{Expr}\partial\mathrm{BT}(\Sigma,R_{\triangleleft\triangleright},R^{\prime}_{\triangleleft\triangleright})^{R^{\prime}}\quad\text{where}\
R_{\triangleleft\triangleright}=R\times\\{\triangleleft,\triangleright\\}$

A _register tree transducer_ consists of a _finite_ set $Q$ of _states_ with
an _initial state_ $q_{I}\in Q$, two disjoint _finite_ sets $R,R^{\prime}$ of
_registers_ , a _transition function_ $\delta:Q\times Q\times\Gamma\to
Q\times\mathcal{A}(\Sigma,R,R^{\prime})$ and an _output function_
$F:Q\to\mathrm{ExprBT}(\Sigma,R,R^{\prime})$. To each tree
$T\in\mathrm{BinTree}(\Gamma)$, it associates inductively a _configuration_
$\mathrm{Conf}(T)\in
Q\times\mathrm{BinTree}(\Sigma)^{R}\times\partial\mathrm{BinTree}(\Sigma)^{R^{\prime}}$:

  * •

The base case is
$\mathrm{Conf}(\lceil\cdot\rceil)=(q_{I},(r\mapsto\lceil\cdot\rceil),(r^{\prime}\mapsto\square))$.

  * •

When
$\mathrm{Conf}(T)=(q_{\triangleleft},\rho_{\triangleleft},\rho^{\prime}_{\triangleleft})$,
$\mathrm{Conf}(U)=(q_{\triangleright},\rho_{\triangleright},\rho^{\prime}_{\triangleright})$
and
$\delta(c,q_{\triangleleft},q_{\triangleright})=(q,(\varepsilon,\varepsilon^{\prime}))$,
we set $\mathrm{Conf}(c\lceil
T,U\rceil)=(q,(r\mapsto\varepsilon(r)(\rho,\rho^{\prime})),(r^{\prime}\mapsto\varepsilon^{\prime}(r^{\prime})(\rho,\rho^{\prime})))$
where $\rho(r,d)=\rho_{d}(r)$ for $(r,d)\in
R\times\\{\triangleleft,\triangleright\\}$ and similarly for $\rho^{\prime}$.

The function defined by the transducer is $T\in\mathrm{BinTree}(\Gamma)\mapsto
F(q_{\mathrm{fin}}(T))(\rho_{\mathrm{fin}}(T),\rho^{\prime}_{\mathrm{fin}}(T))$
where
$(q_{\mathrm{fin}}(T),\rho_{\mathrm{fin}}(T),\rho^{\prime}_{\mathrm{fin}}(T))=\mathrm{Conf}(T)$
(recall that $F$ is the output function).

Figure 17. First few steps of the run of the bottom-up ranked tree transducer
of Figure 17 over a tree whose alphabet of node labels is
$\Sigma=\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bullet},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bullet}\\}\cong\\{a,b\\}$.
The configuration at each subtree is represented by two boxes; the top (resp.
bottom) box displays the contents of $r_{1}$ (resp. $r_{2}$). (The single
state is omitted from the visual representation of the configuration.)

[illustrated by Figure 17] Let us consider a transducer over the alphabets
$\Gamma=\Sigma=\\{a,b\\}$, with a single state ($|Q|=1$) and two registers,
both tree-valued (so $R=\\{r_{1},r_{2}\\}$ and $R^{\prime}=\varnothing$). This
simplifies the transition function $\delta$ into a function
$\Gamma\to\mathrm{ExprBT}(\Sigma,R_{\triangleleft\triangleright},\varnothing)^{R}$
– equivalently, we will consider $\delta:\Gamma\times
R\to\mathrm{ExprBT}(\Sigma,R_{\triangleleft\triangleright},\varnothing)$.

We take
$\delta(c,r_{1})=c\lceil(r_{1})_{\triangleleft},(r_{1})_{\triangleright}\rceil$
and
$\delta(c,r_{2})=c\lceil(r_{2})_{\triangleright},(r_{2})_{\triangleleft}\rceil$
for $c\in\\{a,b\\}$, where $r_{\triangleleft}$ is a notation for
$(r,\triangleleft)\in
R_{\triangleleft\triangleright}=R\times\\{\triangleleft,\triangleright\\}$. If
we write $\hat{r}_{i}(T)$ ($i\in\\{1,2\\}$) for the contents of the register
$r_{i}$ at the end of a run of the transducer on $T\in\mathtt{BT}(\Gamma)$,
then this $\delta$ translates into:

$\hat{r}_{1}(c\lceil
T,U\rceil)=c\lceil\hat{r}_{1}(T),\hat{r}_{1}(U)\rceil\qquad\hat{r}_{2}(c\lceil
T,U\rceil)=c\lceil\hat{r}_{2}(U),\hat{r}_{2}(T)\rceil\qquad(c\in\\{a,b\\})$

And the initial condition is
$\hat{r}_{1}(\lceil\cdot\rceil)=\hat{r}_{2}(\lceil\cdot\rceil)=\lceil\cdot\rceil$.
Therefore $\hat{r}_{1}(T)=T$ and $\hat{r}_{2}(T)$ is $T$ “mirrored” by
exchanging left and right; let us write $\hat{r}_{2}(T)=\mathtt{reverse}(T)$.

The output function $F$ is also simplified into an expression in
$\mathrm{ExprBT}(\Sigma,R,\varnothing)$. By taking $F=a\lceil
r_{1},r_{2}\rceil$, we define a transducer computing the regular function
$T\mapsto a\lceil T,\mathtt{reverse}(T)\rceil$.

To characterize regular functions, a condition must be imposed292929Without
this restriction, one could have outputs of exponential size, whereas regular
functions have linearly bounded output. Filiot and Reynier [FR21] have shown
that the analogous unrestricted model for strings corresponds to HDT0L
systems; we are not aware of any similar result on trees. on the register
assignments: the _single use restriction_. It is not intrinsic and depends on
an additional piece of data, namely a _conflict relation_ between the
registers. [[AD17, §2.1]] A _conflict relation_ is a binary reflexive and
symmetric relation.

An expression
$E\in\mathrm{ExprBT}(\Sigma,V,V^{\prime})\cup\mathrm{Expr}\partial\mathrm{BT}(\Sigma,V,V^{\prime})$
is said to be _consistent with_ a conflict relation $\incoh$ over $V\cup
V^{\prime}$ when each variable in $V\cup V^{\prime}$ appears at most once in
$E$, and for all $x,y\in V\cup V^{\prime}$, if $x\neq y$ and $x\incoh y$, then
$E$ does not contain both $x$ and $y$.

A register assignment
$(\varepsilon,\varepsilon^{\prime})\in\mathcal{A}(\Sigma,R,R^{\prime})$ is
_single use restricted_ with respect to a conflict relation $\incoh$ over
$R\cup R^{\prime}$ when:

  * •

all $\varepsilon(r)$ for $r\in R$ and all $\varepsilon^{\prime}(r^{\prime})$
for $r^{\prime}\in R^{\prime}$ are consistent with $\incoh$;

  * •

if $x_{1},x_{2},y_{1},y_{2}\in R\cup R^{\prime}$, $x_{1}\incoh x_{2}$ and, for
some $d\in\\{\triangleleft,\triangleright\\}$, $(x_{1},d)$ appears in303030By
$\varepsilon\cup\varepsilon^{\prime}$ we mean the map on the _disjoint_ union
$R\cup R^{\prime}$ induced in the obvious way by $\varepsilon$ and
$\varepsilon^{\prime}$. $(\varepsilon\cup\varepsilon^{\prime})(y_{1})$ and
$(x_{2},d)$ appears in $(\varepsilon\cup\varepsilon^{\prime})(y_{2})$, then
$y_{1}\incoh y_{2}$ (note that this includes the case $x_{1}=x_{2}$).

A _bottom-up ranked tree transducer (BRTT)_ is a register tree transducer
$(Q,q_{I},R,R^{\prime},\delta,F)$ endowed with a conflict relation $\incoh$ on
$R\cup R^{\prime}$, such that $F(q)$ is consistent with $\incoh$ and all
register assignments in the image of $\delta$ are single use restricted w.r.t.
$\incoh$.

A _regular tree function_ is a function computed by a BRTT.

When the conflict relation is trivial (i.e. coincides with equality), we say
that the BRTT is _copyless_. We also say that a register tree transducer is
copyless if it becomes a BRTT when endowed with a trivial conflict relation.

##  Appendix B Normalization of the $\lambda\ell^{\oplus\with}$-calculus

This section is devoted to proving that the
$\lambda\ell^{\oplus\with}$-calculus is strongly normalizing. What it means is
that any $\lambda\ell^{\oplus\with}$-term $t$ admitting a typing derivation
$\Psi;\;\Delta\vdash t:A$ can be shown to be $\beta\eta$-equivalent to a
_normal_ term $u$. The notion of normal ($\mathrm{NF}$) and _neutral_
($\mathrm{NE}$) are defined via the typing system presented in Figure 20. The
intuition is that a normal term cannot be $\beta$-reduced further, and that
neutral terms substituted in normal terms produce terms that stay normal.

The purpose of this section is to show that _any_ typed term $t$ can be turned
into a normal term $t^{\prime}$ of the same type via a sequence of
$\beta$-reductions. Because $\lambda\ell^{\oplus\with}$ features _positive_
type constructors $\otimes$ and $\oplus$, the reality is not quite so
straightforward: it is not sufficient to $\beta$-reduce a term to reach a
normal form. In certain circumstances, one must additionally use
$\eta$-conversion to make certain $\beta$-redexes appear and proceed with the
computation of normal terms. This difficulty is rather well-known in the
context of $\lambda$-calculus extended with coproducts [Lin07, ADHS01, Sch16].
However we are not aware of a text treating exactly
$\lambda\ell^{\oplus\with}$ (e.g., incorporating additives, a native $\otimes$
and units), so we include a proof using reducibility candidates along the
lines of [RR97, Appendix A.1].

To describe said reducibility candidates, we first need to give an oriented
version of $\beta\eta$-equality. The $\beta$-reduction relation $\to_{\beta}$
is obtained by closing the relations given in Figure 18 by congruence. We
write $\to_{\beta}^{*}$ for the reflexive transitive closure relation. Much
like with $=_{\beta}$, we assume that terms related by $\to_{\beta}$ have the
same type in the same context.

$\begin{array}[]{l !\; c !{\;\;} c}\text{$\beta$-redexes}&(\lambda
x.t)\;u\leavevmode\nobreak\ \to_{\beta}\leavevmode\nobreak\
t[u/x]&(\lambda^{\oc}x.t)\;u\leavevmode\nobreak\
\to_{\beta}\leavevmode\nobreak\ t[u/x]\\\ &\pi_{1}(\left\langle
t,u\right\rangle)\leavevmode\nobreak\ \to_{\beta}\leavevmode\nobreak\
t&\pi_{2}(\left\langle t,u\right\rangle)\leavevmode\nobreak\
\to_{\beta}\leavevmode\nobreak\ u\\\
&{\mathsf{case}}(\mathsf{in}_{1}(t),x.u,x.v)\leavevmode\nobreak\
\to_{\beta}\leavevmode\nobreak\
u[t/x]&{\mathsf{case}}(\mathsf{in}_{2}(t),x.u,x.v)\leavevmode\nobreak\
\to_{\beta}\leavevmode\nobreak\ v[t/x]\\\ &{\mathsf{let}}\;{x\otimes
y}={t\otimes u}\;{\mathsf{in}}\;{v}\leavevmode\nobreak\ \leavevmode\nobreak\
\to_{\beta}\leavevmode\nobreak\ \leavevmode\nobreak\
v[t/x][u/y]&{\mathsf{let}}\;{()}={()}\;{\mathsf{in}}\;{t}\leavevmode\nobreak\
\to_{\beta}\leavevmode\nobreak\ t\\\ \\\ \end{array}$ Figure 18.
$\beta$-redexes.

As it is not the case that every typable term $\beta$-reduces to a normal
form, we need to describe another set of reduction rules which involve
$=_{\eta}$. Those _extrusion rules_ are listed in Figure 19; we also write
$\to_{\varepsilon}$ for the congruence closure of the relation described
there. While the number of cases is daunting, it should be remarked that these
rules are obtained mechanically by considering the nesting of an eliminator
for a positive type (i.e., the
${\mathsf{let}}\;{\cdot}={\cdot}\;{\mathsf{in}}\;{\cdot}$ constructions
($\otimes,\mathbf{I}$), ${\mathsf{case}}$ ($\oplus$) and ${\mathsf{abort}}$
($0$)) within another eliminator (the aforementioned constructions plus
function application ($\to,\multimap$) and projections $\pi_{1},\pi_{2}$
($\with$)). For a more careful discussion of (a subset) of these rules, we
point the reader to [Sch16, Section 3.3]. We write $\to_{\varepsilon}^{*}$ for
the reflexive transitive closure of $\to_{\varepsilon}$,
$\to_{\beta\varepsilon}$ for the union of $\to_{\varepsilon}$ and
$\to_{\beta}$ and $\to_{\varepsilon}$, and $\to_{\beta\varepsilon}^{*}$ for
its reflexive transitive closure. With these notations, we can state the finer
version of the normalization theorem for $\lambda\ell^{\oplus\with}$.

######  Theorem 76.

For every term term $t$ such that $\Psi;\;\Delta\vdash t:\tau$, there exists
$t^{\prime}$ such that $t\to_{\beta\varepsilon}^{*}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime}:\tau$.

Before embarking on the definitions of the reducibility candidates and the
proof of Theorem 76 itself, we first make a couple of observations relating
$\to_{\beta\varepsilon}^{*}$ and $=_{\beta\eta}$.

######  Lemma 77.

Suppose that we terms $t$ and $t^{\prime}$ with matching types and that
$t\to_{\beta\varepsilon}t^{\prime}$. Then, we have $t=_{\beta\eta}t^{\prime}$.
Furthermore if $t$ is normal, so is $t^{\prime}$. Similarly, if $t$ is
neutral, so is $t^{\prime}$.

######  Lemma 78.

If $t$ is normal, then there is no $t^{\prime}$ such that
$t\to_{\beta}t^{\prime}$.

$\begin{array}[]{c}\footnotesize\text{Nested $\otimes/\mathbf{I}$
eliminator}\\\ \\\
\begin{array}[]{rcl}\footnotesize({\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{u})\;v&\to_{\varepsilon}&{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{(u\;v)}\\\
\pi_{i}({\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{u})&\to_{\varepsilon}&{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{\pi_{i}(u)}\\\
{\mathsf{let}}\;{q}={{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{u}}\;{\mathsf{in}}\;{v}&\to_{\varepsilon}&{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{{\mathsf{let}}\;{q}={u}\;{\mathsf{in}}\;{v}}\\\
{\mathsf{abort}}({\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{u})&\to_{\varepsilon}&{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{{\mathsf{abort}}(u)}\\\
{\mathsf{case}}({\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{u},x.v,y.w)&\to_{\varepsilon}&{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{{\mathsf{case}}(u,x.v,y.w)}\\\
\end{array}\\\ \\\ \footnotesize\text{Nested $0$ eliminator}\\\ \\\
\begin{array}[]{rcl}\footnotesize{\mathsf{abort}}(t)\;u&\to_{\varepsilon}&{\mathsf{abort}}(t)\\\
\pi_{i}({\mathsf{abort}}(t))&\to_{\varepsilon}&{\mathsf{abort}}(t)\\\
{\mathsf{let}}\;{p}={{\mathsf{abort}}(t)}\;{\mathsf{in}}\;{u}&\to_{\varepsilon}&{\mathsf{abort}}(t)\\\
{\mathsf{abort}}({\mathsf{abort}}(t))&\to_{\varepsilon}&{\mathsf{abort}}(t)\\\
{\mathsf{case}}({\mathsf{abort}}(t),x.u,y.v)&\to_{\varepsilon}&{\mathsf{abort}}(t)\\\
\end{array}\\\ \\\ \footnotesize\text{Nested $\oplus$ eliminator}\\\ \\\
\begin{array}[]{r@{~}c@{~}l}\footnotesize{\mathsf{case}}(t,x.u,y.v)\;w\leavevmode\nobreak\
&\to_{\varepsilon}\hfil\leavevmode\nobreak\
&{\mathsf{case}}(t,x.u\;w,y.v\;w)\\\
\pi_{i}({\mathsf{case}}(t,x.u,y.v))\leavevmode\nobreak\
&\to_{\varepsilon}\hfil\leavevmode\nobreak\
&{\mathsf{case}}(t,x.\pi_{i}(u),y.\pi_{i}(v))\\\
{\mathsf{let}}\;{p}={{\mathsf{case}}(t,x.u,y.v)}\;{\mathsf{in}}\;{w}\leavevmode\nobreak\
&\to_{\varepsilon}\hfil\leavevmode\nobreak\
&{\mathsf{case}}(t,x.{\mathsf{let}}\;{p}={u}\;{\mathsf{in}}\;{w},y.{\mathsf{let}}\;{p}={v}\;{\mathsf{in}}\;{w})\\\
{\mathsf{abort}}({\mathsf{case}}(t,x.u,y.v))\leavevmode\nobreak\
&\to_{\varepsilon}\hfil\leavevmode\nobreak\
&{\mathsf{case}}(t,x.{\mathsf{abort}}(u),y.{\mathsf{abort}}(v))\\\
{\mathsf{case}}({\mathsf{case}}(t,x.u,y.v),x^{\prime}.u^{\prime},y^{\prime}.v^{\prime})\leavevmode\nobreak\
&\to_{\varepsilon}\hfil\leavevmode\nobreak\
&{\mathsf{case}}(t,x.{\mathsf{case}}(u,x^{\prime}.u^{\prime},y^{\prime}.v^{\prime}),y.{\mathsf{case}}(v,x^{\prime}.u^{\prime},y^{\prime}.v^{\prime}))\\\
\end{array}\\\ \\\ \end{array}$ Figure 19. The extrusion relation
$\to_{\varepsilon}$ ($i=1,2$ and $p,q$ are patterns $()$ or $z\otimes
z^{\prime}$). $\begin{array}[]{c !\;
c}{\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau}{\Psi;\;\Delta\vdash_{\mathrm{NF}}t:\tau}}\\\
\\\
\dfrac{}{\Psi;\;x:\tau\vdash_{\mathrm{NE}}x:\tau}&\dfrac{}{\Psi,x:\tau;\;\cdot\vdash_{\mathrm{NE}}x:\tau}\\\
\\\
\begin{array}[]{c}\dfrac{\Psi;\;\Delta,\;x:\tau\vdash_{\mathrm{NF}}t:\sigma}{\Psi;\;\Delta\vdash_{\mathrm{NF}}\lambda
x.t:\tau\multimap\sigma}\\\ \\\
\dfrac{\Psi,\;x:\tau;\;\Delta\vdash_{\mathrm{NF}}t:\sigma}{\Psi;\;\Delta\vdash_{\mathrm{NF}}\lambda^{\oc}x.t:\tau\to\sigma}\end{array}&\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau\multimap\sigma\qquad\Psi;\;\Delta^{\prime}\vdash_{\mathrm{NF}}u:\tau}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{\mathrm{NE}}t\;u:\sigma}\\\
\\\
\dfrac{\tiny\Psi;\;\Delta\vdash_{\mathrm{NF}}t:\tau\qquad\Psi;\;\Delta^{\prime}\vdash_{\mathrm{NF}}u:\sigma}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{\mathrm{NF}}t\otimes
u:\tau\otimes\sigma}&\dfrac{\tiny\Psi;\;\Delta^{\prime}\vdash_{\mathrm{NE}}t:\tau\otimes\sigma\qquad\Psi;\;\Delta,\;x:\tau,\;y:\sigma\vdash_{X}u:\kappa}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{X}{\mathsf{let}}\;{x\otimes
y}={t}\;{\mathsf{in}}\;{u}:\kappa}\\\ \\\
\dfrac{}{\Psi;\;\cdot\vdash_{\mathrm{NF}}():\mathbf{I}}&\dfrac{\Psi;\;\Delta^{\prime}\vdash_{\mathrm{NE}}t:\mathbf{I}\qquad\Psi;\;\Delta\vdash_{X}u:\kappa}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{X}{\mathsf{let}}\;{()}={t}\;{\mathsf{in}}\;{u}:\kappa}\\\
\\\ \\\
\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NF}}t:\tau\qquad\Psi;\;\Delta\vdash_{\mathrm{NF}}u:\sigma}{\Psi;\;\Delta\vdash_{\mathrm{NF}}\left\langle
t,u\right\rangle:\tau\with\sigma}&\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau\with\sigma}{\Psi;\;\Delta\vdash_{\mathrm{NE}}\pi_{1}(t):\tau}\qquad\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau\with\sigma}{\Psi;\;\Delta\vdash_{\mathrm{NE}}\pi_{2}(t):\sigma}\\\
\\\ \\\
\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NF}}t:\tau}{\Psi;\;\Delta\vdash_{\mathrm{NF}}\mathsf{in}_{1}(t):\tau\oplus\sigma}&\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NF}}t:\sigma}{\Psi;\;\Delta\vdash_{\mathrm{NF}}\mathsf{in}_{2}(t):\tau\oplus\sigma}\\\
\\\ \\\
\lx@intercol\hfil\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\sigma\oplus\tau\qquad\Psi;\;\Delta^{\prime},\;x:\sigma\vdash_{X}u:\kappa\qquad\Psi;\;\Delta^{\prime},\;y:\tau\vdash_{X}v:\kappa}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{X}{\mathsf{case}}(t,x.u,y.v):\kappa}\hfil\lx@intercol\\\
\\\
\dfrac{}{\Psi;\;\Delta\vdash_{\mathrm{NF}}\left\langle\right\rangle:\top}&\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NE}}t:0}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{\mathrm{NE}}{\mathsf{abort}}(t):\tau}\\\
\\\ \\\ \end{array}$ Figure 20. Normal forms for
$\lambda\ell^{\oplus\with}$-terms ($\vdash_{\mathrm{NF}}$ for normal forms and
$\vdash_{\mathrm{NE}}$ for neutral forms and
$X\in\\{\mathrm{NE},\mathrm{NF}\\}$).

Both of these Lemmas are proved by straightforward induction on the relations
$\to_{\beta}$ and $\to_{\beta\varepsilon}$.

Another crucial ingredient is the confluence of the reduction relation
$\to_{\beta\varepsilon}$ (or Church-Rosser property). Alas, this does not hold
for syntactic equality (up to $\alpha$-equivalence. However, it holds up to
_commuting conversions_ , an equivalence relation $\approx_{c}$ inductively
defined by the clauses in Figure 21 and closure under congruence. We merely
state the confluence property that we will use.

######  Theorem 79.

If we have $t\to^{*}_{\beta\varepsilon}u$ and $t\to^{*}_{\beta\varepsilon}v$,
then there exists $u^{\prime}$ and $v^{\prime}$ such that
$u\to^{*}_{\beta\varepsilon}u^{\prime}$,
$v\to^{*}_{\beta\varepsilon}v^{\prime}$ and $u^{\prime}\approx_{c}v^{\prime}$.

A first observation is these are compatible with $=_{\beta\eta}$ and that
neutral and normal term are preserved by commutative conversions.

######  Lemma 80.

If $t\approx_{c}t^{\prime}$, then $t=_{\beta\eta}t^{\prime}$.

######  Lemma 81.

If $t$ is neutral (resp. normal) and $t\approx_{c}t^{\prime}$, then
$t^{\prime}$ is also neutral (resp. normal).

$\begin{array}[]{c}\begin{array}[]{rcl}\footnotesize{\mathsf{let}}\;{q}={u}\;{\mathsf{in}}\;{{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{v}}&\approx_{c}&{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{{\mathsf{let}}\;{q}={u}\;{\mathsf{in}}\;{v}}\\\
{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{{\mathsf{abort}}(u)}&\approx_{c}&{\mathsf{abort}}({\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{u})\\\
{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{{\mathsf{case}}(u,x.v,y.w)}&\approx_{c}&{\mathsf{case}}(u,x.{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{v},y.{\mathsf{let}}\;{p}={t}\;{\mathsf{in}}\;{w})\\\
{\mathsf{case}}(u,x.{\mathsf{abort}}(t),y.{\mathsf{abort}}(v))&\approx_{c}&{\mathsf{abort}}({\mathsf{case}}(u,x.t,y.v))\\\
\end{array}\\\ \\\
\begin{array}[]{c}{\mathsf{case}}(t,x.{\mathsf{case}}(u,x^{\prime}.v,y^{\prime}.w),y.{\mathsf{case}}(u,x^{\prime}.v^{\prime},y^{\prime}.w^{\prime}))\\\
\approx_{c}\\\
{\mathsf{case}}(u,x^{\prime}.{\mathsf{case}}(t,x.v,y.v^{\prime}),y^{\prime}.{\mathsf{case}}(t,x.w,y.w^{\prime}))\\\
\end{array}\\\ \end{array}$ Figure 21. Commutative conversions $\approx_{c}$
($p,q$ are patterns $()$ or $z\otimes z^{\prime}$ and both sides are assumed
to be well-scoped).

We can now turn to the definition of the reducibility candidates, where we
write $t\to^{*}_{\beta\varepsilon}\approx_{c}t^{\prime}$ when there is some
$t^{\prime\prime}$ such that $t\to^{*}_{\beta\varepsilon}t^{\prime\prime}$ and
$t^{\prime\prime}\approx_{c}t^{\prime}$ hold.

Define a judgment $\Psi;\;\Delta\models t:\tau$ by induction over the type
$\tau$ as follows:

  * •

for $\tau=\mathbbl{o},\mathbf{I},0$ or $\top$, we have $\Psi;\;\Delta\models
t:\tau$ if and only if there is $t^{\prime}$ such that
$t\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NE}}t^{\prime}:\tau$

  * •

$\Psi;\;\Delta\models t:\tau\multimap\sigma$ holds if and only if

    * –

there is $t^{\prime}$ such that $t\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime}:\tau\multimap\sigma$

    * –

for every $u,\Delta^{\prime}$ such that $\Psi;\;\Delta^{\prime}\models
u:\tau$, we have $\Psi;\;\Delta,\;\Delta^{\prime}\models t\;u:\sigma$

  * •

$\Psi;\;\Delta\models t:\tau\to\sigma$ holds if and only if

    * –

there is $t^{\prime}$ such that $t\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime}:\tau\to\sigma$

    * –

for every $u$ such that $\Psi;\;\cdot\models u:\tau$, we have
$\Psi;\;\Delta\models t\;u:\sigma$

  * •

$\Psi;\;\Delta\models t:\tau\otimes\sigma$ holds if and only if

    * –

there is $t^{\prime}$ such that $t\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime}:\tau\otimes\sigma$

    * –

if there are $t_{1},t_{2}$ such that and
$t\to^{*}_{\beta\varepsilon}t_{1}\otimes t_{2}$, then there are $\Delta_{1}$
and $\Delta_{2}$ such that $\Delta=\Delta_{1},\Delta_{2}$ and

$\Psi;\;\Delta_{1}\models
t_{1}:\tau\qquad\text{and}\qquad\Psi;\;\Delta_{2}\models t_{2}:\sigma$

  * •

$\Psi;\;\Delta\models t:\tau\with\sigma$ holds if and only if

    * –

there is $t^{\prime}$ such that $t\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime}:\tau\with\sigma$

    * –

$\Psi;\;\Delta\models\pi_{1}(t):\tau$

    * –

$\Psi;\;\Delta\models\pi_{2}(t):\sigma$

  * •

$\Psi;\;\Delta\models t:\tau\oplus\sigma$ holds if and only if

    * –

there is $t^{\prime}$ such that $t\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime}:\tau\oplus\sigma$

    * –

if there is $u$ such that
$t\to^{*}_{\beta\varepsilon}\approx_{c}\mathsf{in}_{1}(u)$, then
$\Psi;\;\Delta\models u:\tau$

    * –

if there is $v$ such that
$t\to^{*}_{\beta\varepsilon}\approx_{c}\mathsf{in}_{2}(v)$, then
$\Psi;\;\Delta\models v:\sigma$

The set of terms $t$ such that $\Psi;\;\Delta\models t:\tau$ constitutes our
set of reducibility candidates at type $\tau$ in the context $\Psi;\;\Delta$.
They are defined in such a way that if $\Psi;\;\Delta\models t:\tau$, then
there is $t^{\prime}$ such that $t\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime}:\tau$. We shall be able to
conclude this section if we show an _adequacy lemma_ stating that every
typable term lies in a reducibility candidate. Before doing that, we first
need a couple of stability properties: closure under anti-reduction, and the
fact that every neutral term lies in a reducibility candidate.

######  Lemma 82.

If $t$ is a neutral term, then $t$ cannot be $\beta\eta$-equivalent to one of
the following

$\lambda x.u\qquad\lambda^{\oc}x.u\qquad(u,v)\qquad u\otimes
v\qquad\langle\rangle\qquad()\qquad\mathsf{in}_{1}(u)\qquad\mathsf{in}_{2}(u)$

######  Proof B.1.

Trivial case-analysis.

######  Theorem 83.

Suppose that $\Psi;\;\Delta\models t^{\prime}:\tau$. Then the following hold:

  * •

There exists $t^{\prime\prime}$ such that
$t^{\prime}\to^{*}_{\beta\varepsilon}t^{\prime\prime}$ and
$\Psi;\;\Delta\vdash_{\mathrm{NF}}t^{\prime\prime}:\tau$.

  * •

If we have $t\to^{*}_{\beta\varepsilon}t^{\prime}$, then we also have
$\Psi;\;\Delta\models t:\tau$.

  * •

If $\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau$, then $\Psi;\;\Delta\models
t:\tau$.

  * •

If $t^{\prime}\approx_{c}t^{\prime\prime}$, then $\Psi;\;\Delta\models
t^{\prime\prime}:\tau$.

  * •

If $t^{\prime}\to^{*}_{\beta\varepsilon}t^{\prime\prime}$, then we also have
$\Psi;\;\Delta\models t^{\prime\prime}:\tau$.

######  Proof B.2.

The first point can be proven via an easy case analysis on $\tau$ that we
skip. The second point we may prove by induction over $\tau$; let us sketch a
few representative cases:

  * •

If $\tau$ is $\mathbbl{o}$, $0$, $\mathbf{I}$ or $\top$, this is immediate.

  * •

Suppose that $\tau\leavevmode\nobreak\ =\leavevmode\nobreak\
\sigma\multimap\kappa$ and that $t\to^{*}_{\beta\varepsilon}t^{\prime}$. By
definition of $\models$ at $\tau\multimap\kappa$, there is some normal
$t^{\prime\prime}$ such that
$t^{\prime}\to^{*}_{\beta\varepsilon}t^{\prime\prime}$, so we also have
$t\to^{*}_{\beta\varepsilon}t^{\prime\prime}$ by transitivity. Now suppose
that we are given some $u$ and $\Delta^{\prime}$ such that
$\Psi;\;\Delta^{\prime}\models u:\tau$. By definition, we have
$\Psi;\;\Delta,\;\Delta^{\prime}\models t^{\prime}\;u:\kappa$. Using the
induction hypothesis at $\kappa$ and the fact that
$t\;u\to^{*}_{\beta\varepsilon}t^{\prime}\;u$, we thus have that
$\Psi;\;\Delta,\;\Delta^{\prime}\models t\;u:\kappa$. We can thus conclude
that $\Psi;\;\Delta\models t:\kappa$.

  * •

Suppose that $\tau\leavevmode\nobreak\ =\leavevmode\nobreak\
\sigma\oplus\kappa$ and that $t\to^{*}_{\beta\varepsilon}t^{\prime}$. By
definition of $\models$, there is some normal $t^{\prime\prime}$ such that
$t^{\prime}\to^{*}_{\beta\varepsilon}t^{\prime\prime}$, so we also have
$t\to^{*}_{\beta\varepsilon}t^{\prime\prime}$ by transitivity. Now if we have
$u$ (resp. $v$) such that
$t\to_{\beta\varepsilon}^{*}\approx_{c}\mathsf{in}_{1}(u)$ (resp.
$\mathsf{in}_{2}(v)$), then, thanks to confluence (Theorem 79) we also have
$t^{\prime}\to^{*}_{\beta\varepsilon}\approx_{c}\mathsf{in}_{1}(u)$ (resp.
$\mathsf{in}_{2}(v)$), so we have $\Psi;\;\Delta\models u:\sigma$ (resp.
$\Psi;\;\Delta\models u:\kappa$) by definition. Therefore, we may conclude
that $\Psi;\;\Delta\models t:\sigma\oplus\kappa$.

The third point is also proved via a straightforward induction over $\tau$ by
leveraging Lemma 82. The last two points follow from induction over $\tau$
combined with Theorem 79 and Lemma 81.

######  Corollary 84.

If $x$ is a variable of type $\tau$ in either $\Psi$ or $\Delta$, we have
$\Psi;\;\Delta\models x:\tau$.

######  Proof B.3.

Immediate as variables are neutral.

######  Lemma 85.

Suppose that we have $\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau\otimes\sigma$
and $\Psi;\;\Delta^{\prime},x:\tau,y:\sigma\models u:\kappa$. Then we have
$\Psi;\;\Delta,\;\Delta^{\prime}\models{\mathsf{let}}\;{x\otimes
y}={t}\;{\mathsf{in}}\;{u}:\kappa$.

Similarly, if $\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau\oplus\sigma$,
$\Psi;\;\Delta^{\prime},x:\tau\models u:\kappa$ and
$\Psi;\;\Delta^{\prime},y:\sigma\models u^{\prime}:\kappa$, we have
$\Psi;\;\Delta,\Delta^{\prime}\models{\mathsf{case}}(t,x.u,y.u^{\prime}):\kappa$.

Finally, if $\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\mathbf{I}$ and
$\Psi;\;\Delta^{\prime}\models u:\kappa$, we also have
$\Psi;\;\Delta,\;\Delta^{\prime}\models{\mathsf{let}}\;{()}={t}\;{\mathsf{in}}\;{u}:\kappa$.

######  Proof B.4.

By induction over $\kappa$.

######  Theorem 86 (Adequacy).

Suppose that we have a non-linear context $\Psi\leavevmode\nobreak\
=\leavevmode\nobreak\ x_{1}:\sigma_{1},\;\ldots,\;x_{k}:\sigma_{k}$, a linear
context $\Delta\leavevmode\nobreak\ =\leavevmode\nobreak\
a_{1}:\tau_{1},\ldots,\;a_{n}:\tau_{n}$ and a term $v$ such that
$\Psi;\;\Delta\vdash v:\kappa$ for some type $\kappa$. Further, assume that
$\Psi^{\prime},\Delta^{\prime}_{1},\ldots,\Delta^{\prime}_{n}$ and terms
$t_{1},\ldots t_{k},u_{1},\ldots,u_{n}$ such that
$\Psi^{\prime};\;\cdot\models t_{i}:\sigma_{i}$ for $1\leq i\leq k$ and
$\Psi^{\prime};\;\Delta^{\prime}_{j}\models u_{j}:\tau_{j}$ for $1\leq j\leq
n$. Then we have

$\Psi^{\prime};\;\Delta^{\prime}_{1},\ldots,\;\Delta^{\prime}_{n}\models
v[t_{1}/x_{1},\ldots,t_{k}/x_{k},u_{1}/a_{1},\ldots,u_{n}/a_{n}]:\kappa$

######  Proof B.5.

The proof goes by induction over the typing derivation $\Psi;\;\Delta\vdash
v:\kappa$; we sketch a few representative subcases below. To keep notations
short, we write $\gamma$ (respectively $\delta$) instead of the sequence of
assignments $t_{1}/x_{1},\ldots,t_{k}/x_{k}$ (respectively
$u_{1}/a_{1},\ldots,u_{n}/a_{n}$) and
$\Delta^{\prime}=\Delta^{\prime}_{1},\ldots,\;\Delta^{\prime}_{n}$.

  * •

If the last rule used in an axiom, the conclusion is immediate.

  * •

If the last rule used is a linear function application

$\dfrac{\Psi;\;\Delta_{1}\vdash
v:\kappa\multimap\kappa^{\prime}\qquad\Psi;\;\Delta_{2}\vdash
v^{\prime}:\kappa}{\Psi;\;\Delta_{1},\;\Delta_{2}\vdash
v\;v^{\prime}:\kappa^{\prime}}$

with $\delta_{1},\delta_{2}$ and
$\Delta^{\prime\prime}_{1},\;\Delta^{\prime\prime}_{2}$ the obvious
decomposition of $\delta$ and $\Delta^{\prime}$, the induction hypothesis
yields

$\Psi^{\prime};\;\Delta^{\prime\prime}_{1}\models
v[\gamma,\delta_{1}]:\kappa\multimap\kappa^{\prime}\qquad\text{and}\qquad\Psi^{\prime};\;\Delta^{\prime\prime}_{2}\models
v^{\prime}[\gamma,\delta_{2}]:\kappa$

By definition of $\models$ for type $\kappa\multimap\kappa^{\prime}$, we thus
have $\Psi^{\prime};\;\Delta^{\prime}\models
v[\gamma,\delta_{1}]\;v^{\prime}[\gamma,\delta_{2}]:\kappa^{\prime}$, so we
may conclude.

  * •

The case of non-linear function application is entirely analogous.

  * •

If the last rule is the typing of a linear $\lambda$-abstraction

$\dfrac{\Psi;\;\Delta,\;c:\kappa\vdash
v:\kappa^{\prime}}{\Psi;\;\Delta\vdash\lambda
c.v:\kappa\multimap\kappa^{\prime}}$

by the inductive hypothesis, we have
$\Psi^{\prime};\;\Delta^{\prime},\Delta^{\prime\prime}\vdash
v[\gamma,\delta,v^{\prime}/c]:\kappa^{\prime}$ for any $v^{\prime}$ and
$\Delta^{\prime\prime}$ such that
$\Psi^{\prime};\;\Delta^{\prime\prime}\models v^{\prime}:\kappa$. We can prove
the conjunct defining $\Psi^{\prime};\;\Delta^{\prime}\models(\lambda
c.v)[\gamma,\delta]:\kappa\multimap\kappa^{\prime}$ as follows:

    * –

First, by taking $\Delta^{\prime\prime}=c:\kappa$ (Corollary 84), we obtain
that there exists some $v^{\prime\prime}$ such that
$v[\gamma,\delta]\to^{*}_{\beta\varepsilon}v^{\prime\prime}$ and
$\Psi;\;\Delta,\;c:\kappa\vdash_{\mathrm{NF}}v^{\prime\prime}:\kappa^{\prime}$.
Therefore we have $\lambda c.v[\gamma,\delta]\to^{*}_{\beta\varepsilon}\lambda
c.v^{\prime}$ and $\Psi;\;\Delta\vdash_{\mathrm{NF}}\lambda
c.v^{\prime}:\kappa\multimap\kappa^{\prime}$.

    * –

Then, assume we have some $v^{\prime}$ and
$\Psi;\;\Delta^{\prime\prime}\models v^{\prime}:\kappa$, so that we have
$\Psi^{\prime};\;\Delta^{\prime},\Delta^{\prime\prime}\vdash
v[\gamma,\delta,v^{\prime}/c]:\kappa^{\prime}$ by the inductive hypothesis.
Because

$(\lambda c.v)[\gamma,\delta]\;v^{\prime}=(\lambda
c.v[\gamma,\delta])\;v^{\prime}\to_{\beta}v[\gamma,\delta,v^{\prime}/c]$

we may apply Theorem 83 to conclude that
$\Psi^{\prime};\;\Delta^{\prime},\;\Delta^{\prime\prime}\models(\lambda
c.v)[\gamma,\delta]\;v^{\prime}:\kappa^{\prime}$

  * •

The case of the non-linear $\lambda$-abstraction for $\to$ is similar.

  * •

If the last rule applied is an introduction of $\otimes$,

$\dfrac{\Psi;\;\Delta_{1}\vdash t:\tau\qquad\Psi;\;\Delta_{2}\vdash
u:\sigma}{\Psi;\;\Delta_{1},\;\Delta_{2}\vdash t\otimes u:\tau\otimes\sigma}$

call $\delta_{1},\delta_{2}$ the splitting of $\delta$ according to the
decomposition $\Delta=\Delta_{1},\;\Delta_{2}$. The induction hypothesis
yields

$\Psi^{\prime};\;\Delta^{\prime}_{1}\models
t[\gamma,\delta_{1}]:\tau\qquad\text{and}\qquad\Psi^{\prime};\;\Delta^{\prime}_{2}\models
u[\gamma,\delta_{2}]:\sigma$

By definition it means that we have normal terms $t^{\prime}$ and $u^{\prime}$
such that $t[\gamma,\delta_{1}]\to^{*}_{\beta\varepsilon}t^{\prime}$ and
$u[\gamma,\delta_{2}]\to^{*}_{\beta\varepsilon}u^{\prime}$, so $(t\otimes
u)[\gamma,\delta]\to^{*}_{\beta\varepsilon}t\otimes u^{\prime}$. Now suppose
that we have $(t\otimes
u)[\gamma,\delta]\to_{\beta\varepsilon}^{*}\approx_{c}t^{\prime\prime}\otimes
u^{\prime\prime}$. It is not difficult to check (by induction over the length
of the reductions $\to_{\beta\varepsilon}^{*}$ and derivation of
$\approx_{c}$) that we have
$t[\gamma,\delta_{1}]\to_{\beta\varepsilon}^{*}\approx_{c}t^{\prime\prime}$
and
$u[\gamma,\delta_{2}]\to_{\beta\varepsilon}^{*}\approx_{c}u^{\prime\prime}$.
So by Theorem 83, we have that $\Psi;\;\Delta_{1}\models
t^{\prime\prime}:\tau$ and $\Psi;\;\Delta_{2}\models
u^{\prime\prime}:\sigma$,so we may conclude.

  * •

If the last rule applied is an elimination of $\otimes$

$\dfrac{\Psi;\;\Delta_{1}\vdash
u:\tau\otimes\sigma\qquad\Psi;\;\Delta_{2},x:\tau,y:\sigma\vdash
t:\kappa}{\Psi;\;\Delta_{1},\;\Delta_{2}\vdash{\mathsf{let}}\;{x\otimes
y}={u}\;{\mathsf{in}}\;{t}:\kappa}$

with $\delta_{1},\delta_{2}$ the obvious decomposition of $\delta$ along
$\Delta_{1},\;\Delta_{2}$, the induction hypothesis applied to the first
premise yields $\Psi^{\prime};\;\Delta^{\prime}_{1}\models
u[\gamma,\delta_{1}]:\tau\otimes\sigma$. In particular, this means we have
$u[\gamma,\delta_{1}]\to_{\beta\varepsilon}^{*}u^{\prime}$ such that
$\Psi^{\prime};\;\Delta^{\prime}_{1}\vdash_{\mathrm{NF}}u^{\prime}:\tau\otimes\sigma$.
By Theorem 83, it suffices to show that ${\mathsf{let}}\;{x\otimes
y}={u^{\prime}}\;{\mathsf{in}}\;{t[\gamma,\delta_{2}]}\to_{\beta\varepsilon}^{*}v$
such that $\Psi^{\prime};\;\Delta^{\prime}_{1},\;\Delta^{\prime}_{2}\models
v:\kappa$ to conclude. We do so by going by induction over the judgment
$\Psi^{\prime};\;\Delta^{\prime}_{1}\vdash_{\mathrm{NF}}u^{\prime}:\tau\otimes\sigma$.

    * –

If we have
$\Psi^{\prime};\;\Delta^{\prime}_{1}\vdash_{\mathrm{NE}}u^{\prime}:\tau\otimes\sigma$,
then we may use the outer inductive hypothesis
$\Psi^{\prime};\;\Delta^{\prime}_{2},\;x:\tau,\;y:\sigma\models
t[\gamma,\delta_{2}]:\kappa$ and apply Lemma 85.

    * –

If we have $u^{\prime}={\mathsf{let}}\;{x^{\prime}\otimes
y^{\prime}}={u^{\prime\prime}}\;{\mathsf{in}}\;{u^{\prime\prime\prime}}$,
applying the induction hypothesis, we have some $v$ such that

${\mathsf{let}}\;{x\otimes
y}={u^{\prime\prime\prime}}\;{\mathsf{in}}\;{t[\gamma,\delta_{2}]}\to_{\beta\varepsilon}^{*}v\qquad\text{and}\qquad\Psi^{\prime};\;\Delta^{\prime},x^{\prime}:\tau^{\prime},y^{\prime}:\sigma^{\prime}\models
v:\kappa$

We may thus conclude using the sequence of reductions

$\begin{array}[]{rll}{\mathsf{let}}\;{x\otimes
y}={{\mathsf{let}}\;{x^{\prime}\otimes
y^{\prime}}={u^{\prime\prime}}\;{\mathsf{in}}\;{u^{\prime\prime\prime}}}\;{\mathsf{in}}\;{t[\gamma,\delta_{2}]}&\to_{\varepsilon}&{\mathsf{let}}\;{x^{\prime}\otimes
y^{\prime}}={u^{\prime\prime}}\;{\mathsf{in}}\;{{\mathsf{let}}\;{x\otimes
y}={u^{\prime\prime\prime}}\;{\mathsf{in}}\;{t[\gamma,\delta_{2}]}}\\\
&\to_{\beta\varepsilon}^{*}&{\mathsf{let}}\;{x^{\prime}\otimes
y^{\prime}}={u^{\prime\prime}}\;{\mathsf{in}}\;{v}\end{array}$

and Lemma 85

    * –

We proceed similarly if
$u^{\prime}={\mathsf{case}}(u^{\prime\prime},x^{\prime}.u^{\prime\prime\prime},y^{\prime}.u^{\prime\prime\prime\prime})$,
${\mathsf{let}}\;{()}={u^{\prime\prime}}\;{\mathsf{in}}\;{u^{\prime\prime\prime}}$
or $\pi_{i}(u^{\prime\prime})$.

    * –

Finally, if $u^{\prime}=u^{\prime\prime}\otimes u^{\prime\prime\prime}$, we
apply the outer induction hypothesis with the substitution
$\gamma,\delta_{2},u^{\prime\prime}/x,u^{\prime\prime\prime}/y$ to conclude.

######  Proof B.6 (Proof of Theorem 76).

Instantiate Theorem 86 in the case of a trivial substitution ($t_{i}=x_{i}$
and $u_{j}=a_{j}$) using Corollary 84 and conclude with Theorem 83.

##  Appendix C Proof Lemma 25 (on $\lambda\ell^{\oplus\with}$-terms defining
tree functions)

Write $\sqsubseteq_{+}$ for the least preorder relation over
$\lambda\ell^{\oplus\with}$ types satisfying the following for every types
$\tau$ and $\sigma$

$\tau,\sigma\sqsubseteq_{+}\tau\otimes\sigma\quad\tau,\sigma\sqsubseteq_{+}\tau\oplus\sigma\quad\tau,\sigma\sqsubseteq_{+}\tau\with\sigma\quad\sigma\sqsubseteq_{+}\tau\multimap\sigma\quad\sigma\sqsubseteq_{+}\tau\to\sigma$

We say that $\tau$ is a _strictly positive subtype_ of $\sigma$ whenever
$\tau\sqsubseteq_{+}\sigma$.

A context $\Psi;\;\Delta$ is called _consistent_ if there is no term $t$ such
that $\Psi;\;\Delta\vdash t:0$.

######  Lemma 87.

A context $\Psi;\;\Delta$ is inconsistent if and only if there is a neutral
term $t$ such that $\Psi;\;\Delta\vdash_{\mathrm{NE}}t:0$.

Furthermore, if $\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau$, the last typing
rule applied has one premise
$\Psi^{\prime};\;\Delta^{\prime}\vdash_{\mathrm{NE}}u:\tau^{\prime}$ and
$\Psi;\;\Delta$ is consistent, then so is $\Psi^{\prime};\;\Delta^{\prime}$.

######  Proof C.1.

The first point is an easy corollary of Theorem 76. The second point follows
from a case analysis, using the following facts:

  * •

If $\Psi,\;\Psi^{\prime};\;\Delta,\;\Delta^{\prime}$ is consistent, then so is
$\Psi;\;\Delta$.

  * •

If $\Psi;\;\Delta,\;\Delta^{\prime}$ is consistent and
$\Psi;\;\Delta^{\prime}\vdash t:\tau$, then $\Psi;\;\Delta,\;x:\tau$ is
consistent.

######  Lemma 88.

If $\Psi;\;\Delta$ is consistent and
$\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau$, then there is a variable in
$\Psi;\;\Delta$ of type $\sigma$ with $\tau\sqsubseteq_{+}\sigma$.

######  Proof C.2.

By induction on the judgement $\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau$.

  * •

If the last rule applied was a variable lookup.  Ψ; x : τ⊢_NEx : τ  Ψ, x : τ;
⋅⊢_NEx : τ then the conclusion immediately follows.

  * •

The more interesting cases are those of the elimination rules for $\multimap$,
$\otimes$ and $\with$.  Ψ; Δ⊢_NEt : τ⊸σ Ψ; Δ’ ⊢_NFu : τΨ; Δ, Δ’ ⊢_NEt u : σ Ψ;
Δ’ ⊢_NEt : τ⊗σ Ψ; Δ, x : τ, y : σ⊢_NEu : κΨ; Δ, Δ’ ⊢_NElet x ⊗y = t in u : κ
Ψ; Δ⊢_NEt : τσΨ; Δ⊢_NEπ_1(t) : τ Ψ; Δ⊢_NEt : τσΨ; Δ⊢_NEπ_2(t) : σ Ψ; Δ⊢_NEt :
σ⊕τ Ψ; Δ’, x : σ⊢_NEu : κ Ψ; Δ’, y : τ⊢_NEv : κΨ; Δ, Δ’ ⊢_NEcase(t,x.u,y.v) :
κ Ψ; Δ’ ⊢NEt : I Ψ; Δ⊢Xu : κΨ; Δ, Δ’ ⊢Xlet () = t in u : κ Ψ; Δ⊢NEt : 0Ψ
Δ⊢NEabort(t) : τ  The treatment of $\with$ and $\mathbf{I}$ is rather
straightforward and $0$ is ruled out because $\Psi;\;\Delta$ is assumed to be
consistent, so we only explain the inductive step for $\multimap$, $\otimes$
and $\oplus$.

    * –

If the last rule applied is the elimination of a linear arrow

$\dfrac{\Psi;\;\Delta\vdash_{\mathrm{NE}}t:\tau\multimap\sigma\qquad\Psi;\;\Delta^{\prime}\vdash_{\mathrm{NF}}u:\tau}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{\mathrm{NE}}t\;u:\sigma}$

then the induction hypothesis applied to the first premise means that there is
a variable $x$ in $\Psi;\;\Delta$ of type $\kappa$ such that
$\tau\multimap\sigma\sqsubseteq_{+}\kappa$, and we may conclude since
$\sigma\sqsubseteq_{+}\tau\multimap\sigma$.

    * –

If the last rule applied is the elimination of a tensor product

$\dfrac{\Psi;\;\Delta^{\prime}\vdash_{\mathrm{NE}}t:\tau\otimes\sigma\qquad\Psi;\;\Delta,\;x:\tau,\;y:\sigma\vdash_{\mathrm{NE}}u:\kappa}{\Psi;\;\Delta,\;\Delta^{\prime}\vdash_{\mathrm{NE}}{\mathsf{let}}\;{x\otimes
y}={t}\;{\mathsf{in}}\;{u}:\kappa}$

then the induction hypothesis applied to the first premise yields a variable
$z$ in $\Psi;\;\Delta,\;x:\tau,\;y:\sigma$ of type $\zeta$ with
$\kappa\sqsubseteq_{+}\zeta$. If $z\notin\\{x,y\\}$, then $z$ occurs in
$\Psi;\;\Delta$ and we may conclude. Otherwise, suppose that $z=x$; applying
the induction hypothesis to the second premise, we know that
$\tau\otimes\sigma\sqsubseteq_{+}\tau\sqsubseteq_{+}\zeta^{\prime}$ for a
$\zeta^{\prime}$ being the type of some variable in $\Delta^{\prime}$ or a
$\zeta^{\prime}=\oc\zeta^{\prime\prime}$ with $\zeta^{\prime\prime}$ being the
type of some variable in $\Psi$. Therefore, we may conclude since
${\kappa}\sqsubseteq_{+}{\tau}\sqsubseteq_{+}{\tau\otimes\sigma}\sqsubseteq_{+}{\zeta^{\prime}}$.
The case of $z=y$ is treated similarly.

  * •

If the last rule applied is the elimination of a coproduct