i\rrparenthesis}_{\mathfrak{L}}={\llparenthesis\widehat{w}\rrparenthesis}_{\mathfrak{SR}}$
for any $w\in\Gamma^{*}$ is merely a matter of performing
$\beta\eta$-conversions starting from the above equation on $F(\widehat{w})$;
we leave this to the reader. Since every
$f\in\mathsf{Hom}_{\mathcal{SR}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},\Bot\right)$
is of the form $f=\widehat{w}$ for some $w\in\Gamma^{*}$, this suffices to
show that $(F,i,o)$ fits the definition of a morphism of streaming settings.

However, note that this does not alone tells us that $\mathfrak{SR}$-SSTs are
subsumed by $\lambda\ell^{\oplus\with}$, as Lemma 24 only allows us to use
single-state $\mathcal{L}$-SSTs. To circumvent this, we will later prove that
a streaming setting with coproducts allows to simulate state with single-state
SSTs, thus completing a proof of the easier direction of Theorem 1.

In order to build morphisms from $\mathfrak{L}$ to other streaming settings,
we shall make use of the following:

######  Lemma 27.

Let $\mathfrak{C}$ be a streaming setting
$(\mathcal{C},\mathbf{I},\Bot,{\llparenthesis-\rrparenthesis})$ whose
underlying category $\mathcal{C}$ is symmetric monoidal closed with monoidal
unit $\mathbf{I}$. Suppose that $\mathcal{C}$ additionally has chosen finite
products and coproducts. Let $(f_{b})_{b\in\Gamma}$ be a family of morphisms
$\mathsf{Hom}_{\mathcal{C}}\left(\Bot,\Bot\right)^{\Gamma}$ and
$e\in\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},\Bot\right)$
a distinguished morphism such that ${\llparenthesis e\rrparenthesis}$ is the
empty word and, for every
$g\in\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},\Bot\right)$,
we have ${\llparenthesis f_{b}\circ g\rrparenthesis}=b{\llparenthesis
g\rrparenthesis}$ (that is, $f_{b}$ acts by concatenating the single-letter
word $b$ on the left).

Then there is a canonical morphism $\mathfrak{L}\to\mathfrak{C}$ of streaming
settings. Moreover the underlying functor is strong monoidal for $\oplus$,
$\with$, $\otimes$ and preserves $\multimap$.

Without spelling out the details, this Lemma essentially states that
$\mathcal{L}$ is _initial_ among symmetric monoidal closed categories with
products and coproducts. We do not offer a proof of this statement, which we
consider folklore. The interested reader may find a similar development in
[Bie94, Chapter 4] for the case of $\mathcal{L}(\varnothing)$ (i.e., where the
$\lambda\ell^{\oplus\with}$-terms have no free variables). Let us note that,
because of the specific way we defined $\mathcal{L}$, Remark 23, showing the
conservativity of the congruence $=_{\beta\eta}$ of
$\lambda\ell^{\oplus\with}$ over the purely linear fragment should be the
first step in this proof. This is because the notion of symmetric monoidal
closed category does not require the existence of an exponential modality
$\oc$, and thus, all the equations in the initial symmetic monoidal closed
category with products and coproducts should only satisfy those equations
mentioning those constructs.

###  3.4. The free coproduct completion (or finite states)

####  3.4.1. Definition and basic properties

We give here an elementary definition of “the” free finite coproduct
completion of categories $\mathcal{C}$ and some of its basic properties. The
construction consists essentially in considering finite families of objects of
$\mathcal{C}$ as “formal coproducts” (equivalently, one could use finite lists
as in [Gal20, Definition 3]).

Let $\mathcal{C}$ be a category. The _free finite coproduct completion_
$\mathcal{C}_{\oplus}$ is defined as follows:

  * •

An object of $\mathcal{C}_{\oplus}$ is a pair $(U,(C_{u})_{u\in U})$
consisting of a finite set $U$ and a family of objects of $\mathcal{C}$ over
$U$. We write those as formal sums $\bigoplus_{u\in U}C_{u}$ in the sequel.

  * •

A morphism from $\bigoplus_{u\in U}C_{u}\to\bigoplus_{v\in V}C_{v}$ is a
$U$-indexed family of pairs $(v_{u},g_{u})_{u\in U}$ with $v_{u}\in V$ and
$g_{u}:C_{u}\to C_{v_{u}}$ in $\mathcal{C}$. In short,

$\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\bigoplus_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigoplus_{v\in V}C_{v}\right)\;=\;\prod_{u\in
U}\sum_{v\in V}\mathsf{Hom}_{\mathcal{C}}\left(C_{u},C_{v}\right)$

  * •

The identity at object $\bigoplus_{u\in U}C_{u}$ is the family
$(u,\mathrm{id}_{C_{u}})_{u\in U}$. Given two composable maps

$(w_{v},h_{v})_{v\in V}:\bigoplus_{v\in V}C_{v}\to\bigoplus_{w\in
W}C_{w}\qquad\qquad\text{and}\qquad\qquad(v_{u},g_{u})_{u\in
U}:\bigoplus_{u\in U}C_{u}\to\bigoplus_{v\in V}C_{v}$

the composite is defined to be the family

$(w_{v_{u}},h_{v_{u}}\circ g_{u}):\bigoplus_{u\in U}C_{u}\to\bigoplus_{w\in
W}C_{w}$

There is a full and faithful functor
$\iota_{\oplus}:\mathcal{C}\to\mathcal{C}_{\oplus}$ taking an object
$C\in\mathsf{Obj}(\mathcal{C})$ to the one-element family
$\bigoplus_{1}C\in\mathsf{Obj}(\mathcal{C}_{\oplus})$. Objects lying in the
image of this functor will be called _basic_ objects of
$\mathcal{C}_{\oplus}$. The formal sum notation reflects that families
$\bigoplus_{u\in U}C_{u}$ should really be understood as coproducts of those
basic objects $C_{u}$. More generally, it is straightforward to check that,
for any finite set $I$ and family $\bigoplus_{u\in U_{i}}C_{u}$ over $i\in I$,
canonical coproducts in $\mathcal{C}_{\oplus}$ can be computed as follows

$\bigoplus_{i\in I}\bigoplus_{u\in
U_{i}}C_{i,u}\quad=\quad\bigoplus_{(i,u)\in\sum_{i\in I}U_{i}}C_{i,u}$

As advertised, this is a free finite coproduct completion in the following
sense: for any functor $F:\mathcal{C}\to\mathcal{D}$ to a category
$\mathcal{D}$ with finite coproducts, there is an extension
$\widetilde{F}:\mathcal{C}_{\oplus}\to\mathcal{D}$ preserving finite
coproducts making the following diagram commute:

---
$\textstyle{\mathcal{C}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{\oplus}}$$\scriptstyle{F}$$\textstyle{\mathcal{D}}$$\textstyle{\mathcal{C}_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{F}}$

and it is unique up to unique natural isomorphism under those conditions.

Finally, suppose that we are a monoidal structure on $\mathcal{C}$. Then, it
is possible to extend it to a monoidal structure over $\mathcal{C}_{\oplus}$
in a rather canonical way: we require that $\otimes$ distributes over
$\oplus$, i.e., that $A\otimes(B\oplus C)\cong(A\otimes B)\oplus(A\otimes C)$.
Formally speaking, we set202020For readers more familiar with the free
cocompletion ${\sf Set}^{\mathcal{C}^{\mathrm{op}}}$ of $\mathcal{C}$, note
that the coproduct-preserving functor $E$ determined by
$\textstyle{\mathcal{C}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{\oplus}}$$\scriptstyle{{\bf
y}}$$\textstyle{\mathcal{C}_{\oplus}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{E}$$\textstyle{{\sf
Set}^{\mathcal{C}^{\mathrm{op}}}}$ is full and faithful, as well as strong
monoidal when ${\sf Set}^{\mathcal{C}^{\mathrm{op}}}$ is equipped with the
_Day convolution_ as monoidal product. The latter is computed as the following
coend using a monoidal product $\otimes$ in $\mathcal{C}$ $(P\otimes
Q)(U)=\int^{V,W}\mathsf{Hom}_{\mathcal{C}}\left(U,V\otimes W\right)\times
P(V)\times Q(W)$

$\left(\bigoplus_{u\in U}C_{u}\right)\otimes\left(\bigoplus_{v\in
V}C_{v}\right)\quad=\quad\bigoplus_{(u,v)\in U\times V}C_{u}\otimes C_{v}$

If $\mathbf{I}$ is the unit of the tensor product in $\mathcal{C}$, then the
basic object $\bigoplus_{1}\mathbf{I}$ is taken to be the unit of the tensor
product in $\mathcal{C}_{\oplus}$. An affine symmetric monoidal structure on
$\mathcal{C}$ can be lifted in a satisfactory manner to this new tensor
product (in particular $\iota_{\oplus}(\top)$ is still a terminal object).

The following property, which is arguably obvious from the definition of
$\mathcal{C}_{\oplus}$, will turn out to be quite important later.

######  Proposition 28.

For any $A,B\in\mathsf{Obj}(\mathcal{C}_{\oplus})$, there is a natural
isomorphism

$\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\iota_{\oplus}(-),A\oplus
B\right)\quad\cong\quad\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\iota_{\oplus}(-),A\right)+\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\iota_{\oplus}(-),B\right)$

######  Remark 29.

Compare with the following natural isomorphism, which holds for any category
$\mathcal{D}$ and $A,B\in\mathsf{Obj}(\mathcal{D})$:

$\mathsf{Hom}_{\mathcal{D}}\left(A\oplus
B,-\right)\quad\cong\quad\mathsf{Hom}_{\mathcal{D}}\left(A,-\right)\times\mathsf{Hom}_{\mathcal{D}}\left(B,-\right)$

In fact, this characterizes the coproduct of $A$ and $B$. Just like
Proposition 8, this is an instance of a general equivalence between universal
properties and natural bijections involving homsets.

####  3.4.2. Conservativity over affine monoidal settings

First, note that the coproduct completion can be lifted at the level of
streaming settings.

Given a streaming setting
$\mathfrak{C}=(\mathcal{C},\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},\Bot,{\llparenthesis-\rrparenthesis}_{\mathcal{C}})$,
define $\mathfrak{C}_{\oplus}$ as the tuple

$(\mathcal{C}_{\oplus},\iota_{\oplus}(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}),\iota_{\oplus}(\Bot),{\llparenthesis-\rrparenthesis}_{\mathcal{C}_{\oplus}})$

where ${\llparenthesis-\rrparenthesis}_{\mathcal{C}_{\oplus}}$ is obtained by
precomposing the canonical isomorphism (recalling that $\iota_{\oplus}$ is
full and faithful)

$\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\iota_{\oplus}(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}),\iota_{\oplus}(\Bot)\right)\cong\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},\Bot\right)$

Before moving on, let us make the following definition: an object $A$ in a
monoidal category $(\mathcal{C},\otimes,\mathbf{I})$ is said to have _unitary
support_ if there exists a map $\mathbf{I}\to A$. This is quite useful in
affine categories for transductions, as it ensures the following.

######  Lemma 30.

Let $\mathcal{C}$ be a symmetric affine monoidal category. Then, for any pair
of finite families $(C_{u})_{u\in U}$ and $(C_{v})_{v\in V}$ of objects of
$\mathcal{C}$ such that all $C_{u}$ and $C_{v}$ have unitary support, we have
a $U\times V$-indexed family of embeddings

$\mathtt{padwithjunk}_{u,v}:\mathsf{Hom}_{\mathcal{C}}\left(C_{u},C_{v}\right)\;\to\;\mathsf{Hom}_{\mathcal{C}}\left(\bigotimes_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigotimes_{v\in V}C_{v}\right)$

The basic idea behind Lemma 30 can be pictured using string diagrams as in
Figure 6: a morphism $C_{u}\to C_{v}$ can be pictured as a single string,
which is to be embedded in a diagram with $U$-many inputs and $V$-many
outputs. The fact that $\mathcal{C}$ is affine allows us to cut all input
strings for $u^{\prime}\neq u$ using a weakening node, and unitary support
allow us to create some “junk” strings with no input to connect to those
$v^{\prime}\neq v$. This might fail for arbitrary symmetric affine monoidal
categories: take for instance the category of finite sets and surjections
between them, with the coproduct as a monoidal product.

Figure 6.
$\mathtt{padwithjunk}_{D,B}:\mathsf{Hom}_{\mathcal{C}}\left(D,C\right)\to\mathsf{Hom}_{\mathcal{C}}\left(A\otimes
B\otimes C\otimes D,A\otimes B\otimes C\otimes D\right)$

We are now ready to state our first theorem asserting that, in those favorable
circumstances, coproduct completions do not give rise to more expressive SSTs.

######  Theorem 31.

Let $\mathfrak{C}$ be an affine symmetric monoidal streaming setting where all
objects $C$ such that
$\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},C\right)\neq\varnothing\neq\mathsf{Hom}_{\mathcal{C}}\left(C,\Bot\right)$
have unitary support.

$\mathfrak{C}$-SSTs are equivalent to $\mathfrak{C}_{\oplus}$-SSTs.

######  Proof 3.6.

Since $\iota_{\oplus}$ extends to a morphism of streaming settings,
$\mathfrak{C}_{\oplus}$-SSTs subsume $\mathfrak{C}$-SSTs.

Conversely, let $\mathcal{T}=\left(Q,q_{0},\bigoplus_{u\in
U}C_{u},\delta,i,o\right)$ be a $\mathfrak{C}_{\oplus}$-SST with input
$\Sigma^{*}$ and $C_{u}$ basic objects. Then, we construct a
$\mathfrak{C}$-SST

$\mathcal{T}^{\prime}=\left(Q\times U,\;(q_{0},u_{0}),\;\bigotimes_{u\in
U}C_{u},\;\delta^{\prime},\;i_{u_{0}},\;o^{\prime}\right)$

such that
${\llbracket\mathcal{T}\rrbracket}={\llbracket\mathcal{T}^{\prime}\rrbracket}$.
We define successively $(u_{0},i_{u_{0}})$, $\delta^{\prime}$ and
$o^{\prime}$.

  * •

We have
$i\in\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\iota_{\oplus}(\top),\bigoplus_{i\in
I}C_{i}\right)$ which can be rewritten as a factorization

$\textstyle{\displaystyle\iota_{\oplus}(\top)=\bigoplus_{1}\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\quad({\sf
in}_{u_{0}},*\mapsto\mathrm{id})}$$\textstyle{\displaystyle\bigoplus_{U}\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\mathrm{id},u\mapsto
i_{u})}$$\textstyle{\displaystyle\bigoplus_{u\in U}C_{u}}$

for some $u_{0}\in U$ (the $i_{u}$ for $u\neq u_{0}$ are taken arbitrarily
thanks to the assumption that the $C_{u}$ have unitary support). This $u_{0}$
is the second component of the initial state of $\mathcal{T}^{\prime}$.

  * •

We set $\delta^{\prime}(a,(q,u))=(q^{\prime},\alpha_{u}(f^{\prime}))$ if
$\delta(a,q)=(q^{\prime},f^{\prime})$, where

$(\alpha_{u})_{u\in U}\;:\;\prod_{u\in
U}\left[\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\bigoplus_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigoplus_{u\in
U}C_{u}\right)\to\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\bigotimes_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigotimes_{u\in U}C_{u}\right)\right]$

is defined by taking the pointwise composite of

$\begin{array}[]{lrccc}&{\widetilde{\alpha}_{u}}:&\displaystyle\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\bigoplus_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigoplus_{u^{\prime}\in
U}C_{u^{\prime}}\right)&\rightarrow&\displaystyle\sum_{u^{\prime}\in
U}\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(C_{u},C_{u^{\prime}}\right)\\\
&\beta_{u}:&\displaystyle\sum_{u^{\prime}\in
U}\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(C_{u},C_{u^{\prime}}\right)&\rightarrow&\displaystyle
U\times\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\bigotimes_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigotimes_{u\in U}C_{u}\right)\\\
&\pi:&\displaystyle
U\times\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\bigotimes_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigotimes_{u\in
U}C_{u}\right)&\rightarrow&\displaystyle\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(\bigotimes_{u\in
U}C_{u}\text{{\Huge{,}}}\;\bigotimes_{u\in U}C_{u}\right)\end{array}$

where $\widetilde{\alpha}_{u}$ is obtained by evaluating its input
$f\in\prod_{u\in U}\sum_{u^{\prime}\in
U}\mathsf{Hom}_{\mathcal{C}_{\oplus}}\left(C_{u},C_{u^{\prime}}\right)$ at
$u$, $\beta_{u}={\sum_{u^{\prime}}\mathtt{padwithjunk}_{u,u^{\prime}}}$ (with
$\mathtt{padwithjunk}$ given as per Lemma 30) and $\pi$ taken to be the second
projection.

  * •

Finally, we set
$o^{\prime}(q,u)\in\mathsf{Hom}_{\mathcal{C}}\left(\bigotimes_{v\in
U}C_{v},\Bot\right)$ to
$\widetilde{o}_{u}\in\mathsf{Hom}_{\mathcal{C}}\left(C_{u},\Bot\right)$
precomposed with the projection
$\pi_{u}\in\mathsf{Hom}_{\mathcal{C}}\left(\bigotimes_{v\in
U}C_{v},C_{u}\right)$.

To conclude, one can check by induction that
${\llbracket\mathcal{T}\rrbracket}(w)={\llbracket\mathcal{T}^{\prime}\rrbracket}(w)$
for every $w\in\Sigma^{*}$.

######  Corollary 32.

$\mathfrak{SR}_{\oplus}$-SSTs are equivalent to $\mathfrak{SR}$-SSTs.

######  Proof 3.7.

All objects of $\mathcal{SR}$ have unitary support via an induction: tensor
with the map $\varepsilon:\mathbf{I}\to\Gamma^{*}$ corresponding to the empty
word at the recursive step.

####  3.4.3. State-dependent memory SSTs

The free coproduct completion encourages us to define the notion of _state-
dependent memory SST_ , generalizing usual copyless SSTs as follows: instead
of taking a single object $C\in\mathsf{Obj}(\mathcal{C})$ as an abstract
infinitary memory, we allow to take a family $(C_{q})_{q\in
Q}\in\mathsf{Obj}(\mathcal{C})^{Q}$ indexed by the states of the SST. A
_state-dependent memory_ $\mathfrak{C}$-_SST_ (henceforth abbreviated
sdm-$\mathfrak{C}$-SST or sdmSST when $\mathfrak{C}$ is clear form context)
with input $\Sigma^{*}$ is a tuple $(Q,q_{0},\delta,(C_{q})_{q\in Q},i,o)$
where

  * •

$Q$ is a finite set of states

  * •

$q_{0}\in Q$ is some initial state

  * •

$\displaystyle\delta:\Sigma\to\prod_{q\in Q}\sum_{r\in
Q}\mathsf{Hom}_{\mathcal{C}}\left(C_{q},C_{r}\right)$ is a transition function

  * •

$i\in\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},C_{q_{0}}\right)$
is the initialization morphism

  * •

$o\in\prod_{q\in Q}\mathsf{Hom}_{\mathcal{C}}\left(C_{q},\Bot\right)$ is the
output family of morphism

In the sequel, we shall often use sdmSSTs because we find them convenient to
give more elegant constructions that produce little “junk”, as is encoded in
Lemma 30. They essentially give the full power of coproducts in any given
situation as shown below.

######  Lemma 33.

Let $\mathfrak{C}$ be a streaming setting. State-dependent memory
$\mathfrak{C}$-SSTs are exactly as expressive as $\mathfrak{C}_{\oplus}$-SSTs.

######  Proof 3.8 (Proof sketch).

Given a $\mathfrak{C}_{\oplus}$-SST $\left(Q,q_{0},\bigoplus_{u\in
U}C_{u},\delta,i,o\right)$ where $i(*)={\sf in}_{u_{0}}(i^{\prime})$ one may
check that the following sdm-$\mathfrak{C}$-SST computes the same function:

$\left(Q\times U,(q_{0},u_{0}),(C_{u})_{(q,u)\in Q\times
U},\delta^{\prime},i^{\prime},(o(q)_{u})_{(q,u)\in Q\times U}\right)$

where $\delta^{\prime}(a)_{q,u}=((r,u^{\prime}),f)$ if and only if
$\delta(a,q)=(r,v)$ and $v_{u}=(u^{\prime},f)$.

Conversely, letting $(Q,q_{0},(C_{q})_{q\in Q},\delta,i,o)$ be a
sdm-$\mathfrak{C}$-SST, an equivalent $\mathfrak{C}_{\oplus}$-SST is given by
$(Q,q_{0},\bigoplus_{q\in Q}C_{q},\delta^{\prime},{\sf
in}_{q_{0}}(i),o^{\prime})$, where it is sufficient to define $o^{\prime}(q)$
as $(o_{q})_{q}$ and to ensure that if
$\delta^{\prime}(a,q)=(r,(r_{q^{\prime}},f_{q^{\prime}})_{q^{\prime}\in Q})$,
then $\delta(a)_{q}=(r,f_{q})$ and $r_{q}=r$. This can be done.

Finally, let us remark that the notions of single-state, “normal” and state-
dependent memory $\mathfrak{C}$-SSTs coincide if $\mathfrak{C}$ has all
coproducts.

######  Lemma 34.

If $\mathfrak{C}$ is a streaming setting with coproducts, single-state
$\mathfrak{C}$-SSTs are as expressive as general $\mathfrak{C}$-SSTs and
sdm-$\mathfrak{C}$-SSTs.

######  Proof 3.9.

Take a sdmSST $(Q,q_{0},(C_{q})_{q\in Q},\delta,i,o)$ to the single-state SST

$\left(\\{\bullet\\},\,\bullet,\,\bigoplus_{q\in
Q}C_{q},\,\delta^{\prime},\,{\sf in}_{q_{0}}\circ i,\,[o(q)]_{q\in Q}\right)$

where $\delta^{\prime}$ is defined from $\delta$ through the maps

$\textstyle{\displaystyle\left[\prod_{q\in Q}\sum_{r\in
Q}\mathsf{Hom}_{\mathcal{C}}\left(C_{q},C_{r}\right)\right]^{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\left[\prod_{q\in
Q}\mathsf{Hom}_{\mathcal{C}}\left(C_{q},\bigoplus_{r\in
Q}C_{r}\right)\right]^{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sim}$$\textstyle{\displaystyle\left[\mathsf{Hom}_{\mathcal{C}}\left(\bigoplus_{q\in
Q}C_{q},\bigoplus_{r\in Q}C_{r}\right)\right]^{\Sigma}}$

######  Remark 35.

The comparison between single-state, standard and state-dependent memory
$\mathfrak{C}$-SSTs can be summed up in terms of completion with the following
“equalities”:

$\mathfrak{C}$-SSTs = single-state $\mathfrak{C}_{\oplus\mathrm{const}}$-SSTs
sdm-$\mathfrak{C}$-SSTs = single-state $\mathfrak{C}_{\oplus}$-SSTs

where $\mathfrak{C}_{\oplus\mathrm{const}}$ designates the following
restriction of $\mathfrak{C}_{\oplus}$: the category $\mathcal{C}_{\oplus}$ is
restricted to the full subcategory $\mathcal{C}_{\oplus\mathrm{const}}$ whose
objects are constant formal sums $\bigoplus_{i\in I}C$ for some
$C\in\mathsf{Obj}(\mathcal{C})$.

####  3.4.4. Some function spaces in $\mathcal{SR}_{\oplus}$

Now we study $\mathcal{SR}_{\oplus}$ in some more detail. This category is
unfortunately not able to interpret even the $\otimes/\multimap$ fragment of
$\lambda\ell^{\oplus\with}$, because, like $\mathcal{SR}$, it lacks internal
homsets $A\multimap B$ for every pair
$(A,B)\in\mathsf{Obj}(\mathcal{SR}_{\oplus})^{2}$. However, they exist when
$A$ lies in the image of $\iota_{\oplus}$. It will turn out to be very useful
later on.

Now we reframe a useful technical argument, typically made when dealing with
determinization and composition of standard copyless SSTs to obtain the
internal homsets we desire. The core of this argument (sketched in [BC18,
p.206-207]) is that register transitions may be effectively coded using a
combination of state and a larger set of registers. Here, the intuition is
that the free coproduct completion allows the category $\mathcal{SR}_{\oplus}$
to integrate all the features of the additional finite set of states provided
by the SSTs.

######  Lemma 36.

Let $R,S\in\mathsf{Obj}(\mathcal{SR})$. There is an internal homset
$\iota_{\oplus}(R)\multimap\iota_{\oplus}(S)$ in $\mathcal{SR}_{\oplus}$.

In Example 3.4.4, we work through the proof below in a concrete case.

######  Proof 3.10.

First, recall that $\iota_{\oplus}$ is full and faithful, and that it is thus
pertinent to focus our preliminary analysis on morphisms in $\mathcal{SR}$.
Recall that a register transition $f:R\to S$, which is a set-theoretical map
$S\to(\Gamma+R)^{*}$ where for every $r\leq R$, $\sum_{s\in
S}|f(s)|_{\mathsf{in}_{2}(r)}\leq 1$ (i.e., it is copyless). Consider the map
$(\Gamma+R)^{*}\to R^{*}$ erasing the letters of $\Gamma$. Then, the image of
the induced map $p:\mathsf{Hom}_{\mathcal{SR}}\left(R,S\right)\to[S\to R^{*}]$
is clearly finite because of copylessness. In fact, letting ${\sf LO}(X)$ be
the set of all total orders over some set $X$, we have an isomorphism between
the image of $\mathsf{Hom}_{\mathcal{SR}}\left(R,S\right)$ under $p$ and the
following dependent sum

$\mathcal{O}(R,S)\qquad=\qquad\sum_{\hat{f}:R\rightharpoonup S}\prod_{s\in
S}{\sf LO}(\hat{f}^{-1}(s))$

The intuition is that $\hat{f}$ tracks where register variables in $R$ get
affected and the additional data encode in which order they appear in an
affectation. Once this crucial finitary information $(\hat{f},(<_{s})_{s\in
S})$ is encoded in the internal homset using coproducts, it only remains to
recover the information we erased with $p$, i.e. what words in $\Gamma^{*}$
located between occurrences of register variables. This information cannot be
bounded by the size of $R$ and $S$, but the number of intermediate words can;
we may index them by $S+{\sf{dom}}(\hat{f})$.

Putting everything together, it means that we take

$\iota_{\oplus}(R)\multimap\iota_{\oplus}(S)\qquad=\qquad\bigoplus_{(\hat{f},<)\in\mathcal{O}(R,S)}\iota_{\oplus}(S+{\sf{dom}}(\hat{f}))$

Now, we need to define the evaluation map
$\mathrm{ev}_{R,S}:[\iota_{\oplus}(R)\multimap\iota_{\oplus}(S)]\otimes\iota_{\oplus}(R)\to\iota_{\oplus}(S)$.
Recall that the tensor distributes over $\oplus$, so we really need to exhibit
$\mathrm{ev}_{R,S}$ in

$\mathsf{Hom}_{\mathcal{SR}_{\oplus}}\left(\bigoplus_{(\hat{f},<)}\iota_{\oplus}(S+{\sf{dom}}(\hat{f})+R)\text{{\Huge{,}}}\;\iota_{\oplus}(S)\right)\leavevmode\nobreak\
\leavevmode\nobreak\ \cong\leavevmode\nobreak\ \leavevmode\nobreak\
\prod_{(\hat{f},<)}\mathsf{Hom}_{\mathcal{SR}}\left(S+{\sf{dom}}(\hat{f})+R\text{{\Huge{,}}}\;S\right)$

where the indices $(\hat{f},<)$ ranges over $\mathcal{O}(R,S)$ on both sides.
Call $\mathrm{ev}_{R,S,\hat{f},<}$ the corresponding family of
$\mathcal{SR}$-morphisms, whose members are set-theoretic maps
$S\to(S+{\sf{dom}}(\hat{f})+R)^{*}$. Calling $\\{r_{1},\ldots,r_{k}\\}$ the
subset of ${\sf{dom}}(\hat{f})$ ordered by $r_{1}<\ldots<r_{k}$, we set

$\mathrm{ev}_{R,S,\hat{f},<}(s)\leavevmode\nobreak\ \leavevmode\nobreak\
=\leavevmode\nobreak\ \leavevmode\nobreak\ {\sf in}_{0}(s){\sf
in}_{2}(r_{1}){\sf in}_{1}(r_{1})\ldots{\sf in}_{2}(r_{k}){\sf in}_{1}(r_{k})$

This concludes the definition of $\mathrm{ev}$. We now leave checking that
this satisfies the required universal property to the reader.

Let us illustrate this construction in a simple case. Consider the following
register transition for the concrete base alphabet $\\{a,b\\}$ and register
names $x,y,z,u,r,s$:

$\begin{array}[]{lcl}r&\leftarrow&zaxabyaa\\\ s&\leftarrow&bab\\\ \end{array}$

Up to the evident isomorphism $\\{x,y,z,u\\}\cong\\{x\\}\otimes\\{y,z,u\\}$,
this determines a morphism
$f\in\mathsf{Hom}_{\mathcal{SR}}\left(\\{x\\}\otimes\\{y,z,u\\},\\{r,s\\}\right)$.
Let us describe the unique map $\Lambda(f)$ in

$\mathsf{Hom}_{\mathcal{SR}_{\oplus}}\left(\iota_{\oplus}(\\{x\\}),\;\iota_{\oplus}(\\{y,z,u\\})\multimap\iota_{\oplus}(\\{r,s\\})\right)\cong\sum_{\hat{f},<}\mathsf{Hom}_{\mathcal{SR}}\left(\\{x\\},\\{r,s\\}+{\sf{dom}}(\hat{f})\right)$

such that $\mathrm{ev}\circ(\Lambda(f)\otimes\mathrm{id})=f$. On its first
component, we set $\hat{f}(y)=\hat{f}(z)=r$ and leave it undefined on $u$; as
for the order, we set $z<_{r}y$. The last component corresponds to the
register transition $h$ depicted below on the left, where, for legibility, we
write $\bf r,s,z$ and $\bf y$ for
$\mathsf{in}_{1}(r),\mathsf{in}_{1}(s),\mathsf{in}_{2}(z)$ and
$\mathsf{in}_{2}(y)$. Using the same notations, we also display on the right
the relevant component of
$\mathrm{ev}_{\\{y,z,u\\},\\{r,s\\},\hat{f},<}\in\mathsf{Hom}_{\mathcal{SR}}\left((\\{r,s\\}+\\{z,y\\})+\\{z,y\\},\\{r,s\\}\right)$,
so that the reader may convince themself that the composite
$\mathrm{ev}_{\\{y,z,u\\},\\{r,s\\},\hat{f},<}\circ(h\otimes\mathrm{id}_{\\{y,z,u\\}})$
is indeed $f$.

$\begin{array}[]{lcl}{\bf r}&\leftarrow&\varepsilon\\\ {\bf
z}&\leftarrow&axab\\\ {\bf y}&\leftarrow&aa\\\ {\bf s}&\leftarrow&bab\\\
\end{array}\qquad\qquad\begin{array}[]{lcl}r&\leftarrow&\mathsf{in}_{1}({\bf
r})\;{\bf y}\;\mathsf{in}_{1}({\bf y})\;{\bf z}\;\mathsf{in}_{1}({\bf z})\\\
s&\leftarrow&\mathsf{in}_{1}({\bf s})\\\ \end{array}$

Lemma 36 can be extended to define internal homsets
$\iota_{\oplus}(R)\multimap C$ for arbitrary
$C\in\mathsf{Obj}(\mathcal{SR}_{\oplus})$ through the natural isomorphism of
Proposition 28. However, extending this to all homsets (i.e. allowing any
object of $\mathcal{SR}_{\oplus}$ in the left-hand side) seems impossible: the
lack of _products_ prevents us from doing so.

###  3.5. The product completion (or non-determinism)

The above point (among others) leads us to study the free finite product
completion of streaming settings. As for coproducts, we first discuss the
categorical construction before turning to the expressiveness. Here, the
situation is more intricate as it turns out that
sdm-$\mathfrak{C}_{\with}$-SSTs of interest will roughly have the power of
_non-deterministic_ sdm-$\mathfrak{C}$-SSTs. We make that connection precise.

Thankfully, a determinization theorem for usual copyless SSTs, i.e.
$\mathfrak{SR}$-SSTs, exists in the literature [AD11] (the proof in the given
reference is indirect and goes through monadic second-order logic). It could
be applied without difficulty to show that non-determinism does not increase
the power of _sdm_ -$\mathfrak{SR}$-SSTs.

To keep the exposition self-contained _and_ illustrate our framework, we give
in Section 4.2 a direct determinization argument generalized to our setting by
using, crucially, the concept of internal homsets (and Lemma 36 for the
desired application).

####  3.5.1. Definition and basic properties

The product completion can, of course, be defined as the dual of the coproduct
completion. Let $\mathcal{C}$ be a category. Its _free finite product
completion_ is
$\mathcal{C}_{\with}=((\mathcal{C}^{\mathrm{op}})_{\oplus})^{\mathrm{op}}$.

While conceptually immaculate, this definition merits a bit of unfolding. The
objects of $\mathcal{C}_{\with}$ are still finite families $(C_{x})_{x\in X}$
– in this context, we write them as formal products $\bigwith_{x\in X}C_{x}$.
As for homsets, we have the dualized situation

$\mathsf{Hom}_{\mathcal{C}_{\with}}\left(\bigwith_{x\in
X}C_{x}\text{{\Huge{,}}}\;\bigwith_{y\in
Y}C_{y}\right)\quad\cong\quad\prod_{y\in Y}\sum_{x\in
X}\mathsf{Hom}_{\mathcal{C}_{\with}}\left(C_{x},C_{y}\right)$

We also a full and faithful functor
$\iota_{\with}:\mathcal{C}\to\mathcal{C}_{\with}$ with a similar universal
property as for the coproduct completion.

As with the coproduct completion, one may want to produce a tensor product in
$\mathcal{C}_{\oplus}$ if the underlying category $\mathcal{C}$ has one. The
very same recipe can be applied: we define the tensor so that the
distributivity $A\otimes(B\with C)\cong(A\otimes B)\with(A\otimes C)$ holds.

$\left(\bigwith_{x\in X}C_{x}\right)\otimes\left(\bigwith_{y\in
Y}C_{y}\right)\quad=\quad\bigwith_{(x,y)\in X\times Y}C_{x}\otimes C_{y}$

######  Remark 37.

One might be disturbed by this distributivity of $\otimes$ over $\with$, which
goes against the non-linear intuition of thinking of $\with$ and $\otimes$ as
“morally the same”. This feeling may also be exacerbated by the familiar iso

$\mathsf{Hom}_{\mathcal{SR}_{\oplus}}\left(\top,R\otimes
S\right)\cong\mathsf{Hom}_{\mathcal{SR}_{\oplus}}\left(\top,R\right)\times\mathsf{Hom}_{\mathcal{SR}_{\oplus}}\left(\top,S\right)$

This indeed becomes false when going from $\mathcal{SR}$ to
$\mathcal{SR}_{\with}$. The useful mnemonic here (which is untrue for pure
LL!) is that the _multiplicative_ connective distributes over both _additive_
connectives in the same way.

######  Remark 38.

While $\mathcal{C}_{\with}$ inherits a monoidal product from $\mathcal{C}$
much like with the coproduct completion, it does _not_ preserve the
_affineness_ of monoidal products. The product completion indeed adds a new
terminal object, namely the empty family, which can _never_ be isomorphic to
the singleton family $\iota_{\with}(\top)$. More generally, $\iota_{\with}$
preserves colimits rather than limits.

It is also straightforward to extend the product completion at the level of
streaming settings $\mathfrak{C}\mapsto\mathfrak{C}_{\with}$.

####  3.5.2. Relationship with non-determinism

At this juncture, our goal is to prove the equivalence between
sdm-$\mathfrak{SR}_{\with}$-SSTs and sdm-$\mathfrak{SR}$-SSTs. One direction
is trivial; for the other, we actually prove that
sdm-$\mathfrak{SR}_{\with}$-SSTs are subsumed by
sdm-$\mathfrak{SR}_{\oplus}$-SSTs.

This result involves some non-trivial combinatorics. We prove it via
_uniformization_ of non-deterministic sdm-$\mathfrak{SR}$-SSTs, a mild
generalization of determinization212121We work with uniformization here we
find it slightly more convenient to handle. This choice of uniformization over
determinization is rather inessential..

Our non-deterministic devices make _finitely branching_ choices, following the
case of the usual non-deterministic SSTs [AD11, Section 2.2]. To express this,
we use the notation $\mathcal{P}_{<\infty}(X)$ for the set of _finite_ subsets
of a set $X$. (Note that if $Q$ is some finite set of states, we have the
simplification $\mathcal{P}(X)=\mathcal{P}_{<\infty}(X)$.)

Let $\mathfrak{C}$ be streaming setting with output $X$. A _non-deterministic_
sdm-$\mathfrak{C}$-SST with input $\Sigma^{*}$ and output $X$ is a tuple
$\left(Q,I,(C_{q})_{q\in Q},\Delta,i,o\right)$ where

  * •

$Q$ is a finite set of states and $I\subseteq Q$

  * •

$(C_{q})_{q\in Q}$ is a family of objects of $\mathcal{C}$

  * •

$\Delta$ is a finite transition relation:
$\displaystyle\Delta\in\mathcal{P}_{<\infty}\left(\Sigma\times\sum_{(q,r)\in
Q^{2}}\mathsf{Hom}_{\mathcal{C}}\left(C_{q},C_{r}\right)\right)$

  * •

$i\in\displaystyle\prod_{q_{0}\in
I}\mathsf{Hom}_{\mathcal{C}}\left(\top,C_{q_{0}}\right)$ is a family of input
morphisms

  * •

$o\in\displaystyle\prod_{q\in
Q}(\mathsf{Hom}_{\mathcal{C}}\left(C_{q},\Bot\right)+1)$ is a family of
partial output morphisms

A _partial_ sdm-$\mathfrak{C}$-SST $(Q,q_{0},(C_{q})_{q\in Q},\delta,i,o)$ has
the same definition as a (deterministic) sdm-$\mathfrak{C}$-SST (Definition
3.4.3), except for the output $o$, which is allowed to be partial, just as in
the last item above.

By transposing the usual notion of run of a non-deterministic finite
automaton, one sees that a non-deterministic sdm-$\mathfrak{C}$-SST
$\mathcal{T}$ gives rise to a function
${\llbracket\mathcal{T}\rrbracket}:\Sigma^{*}\to\mathcal{P}_{<\infty}(X)$ (for
an input alphabet $\Sigma$ and output set $X$). Similarly, a partial
sdm-$\mathfrak{C}$-SST $\mathcal{T}^{\prime}$ is interpreted as a partial
function ${\llbracket\mathcal{T}\rrbracket}:\Sigma^{*}\rightharpoonup X$.

######  Remark 39.

In line with Remark 35, we may describe non-deterministic
sdm-$\mathfrak{C}$-SSTs as single-state (deterministic) SSTs over an enriched
streaming setting.

Let
$\mathfrak{C}=(\mathcal{C},\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}_{\mathfrak{C}},\Bot_{\mathfrak{C}},{\llparenthesis-\rrparenthesis}_{\mathfrak{C}})$,
with output $X$. We first define the category $\mathsf{NFA}(\mathcal{C})$:

  * •

its objects consist of a finite set $Q$ with a family $(C_{q})_{q\in
Q}\in\mathsf{Obj}(\mathcal{C})^{Q}$;

  * •

its morphisms are
$\displaystyle\mathsf{Hom}_{\mathsf{NFA}(\mathcal{C})}\left((C_{q})_{q\in
Q},(C^{\prime}_{r})_{r\in R}\right)=\mathcal{P}_{<\infty}\left(\sum_{(q,r)\in
Q\times R}\mathsf{Hom}_{\mathcal{C}}\left(C_{q},C_{r}\right)\right)$

  * •

the composition of morphisms extends that of binary relations:

$\varphi\circ\psi=\\{(q,\,s,\,f\circ g)\mid(q,\;r,\;f:C_{q}\to
C^{\prime}_{r})\in\varphi,\;(r,\;s,\;g:C^{\prime}_{r}\to
C^{\prime\prime}_{s})\in\psi\\}$

To lift this to a construction $\mathsf{NFA}(\mathfrak{C})$ on streaming
settings, we take:

  * •

$\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}_{\mathsf{NFA}(\mathfrak{C})}$
and $\Bot_{\mathsf{NFA}(\mathfrak{C})}$ are the $\\{\bullet\\}$-indexed
families containing respectively
$\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}_{\mathfrak{C}}$ and
$\Bot_{\mathfrak{C}}$, so that
$\mathsf{Hom}_{\mathsf{NFA}(\mathcal{C})}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}_{\mathsf{NFA}(\mathfrak{C})},\Bot_{\mathsf{NFA}(\mathfrak{C})}\right)=\mathcal{P}_{<\infty}\left(\\{(\bullet,\bullet)\\}\times\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}_{\mathfrak{C}},\Bot\mathfrak{C}\right)\right)$

  * •

${\llparenthesis\varphi\rrparenthesis}_{\mathsf{NFA}(\mathfrak{C})}=\\{{\llparenthesis
f\rrparenthesis}_{\mathfrak{C}}\mid(\bullet,\bullet,f)\in\varphi\\}\subseteq
X$, so that the output set of a $\mathsf{NFA}(\mathfrak{C})$-SST is
$\mathcal{P}_{<\infty}(X)$.

There is a slight mismatch between the above definition of non-deterministic
sdm-$\mathfrak{C}$-SSTs and single-state $\mathsf{NFA}(\mathfrak{C})$-SSTs: in
the latter, two distinct input (resp. output) morphisms may correspond to the
same initial (resp. final) state. However, the former can encode such
situations by enlarging the set of states (to keep it finite, the use of
$\mathcal{P}_{<\infty}(-)$ in the definitions is crucial).

One can also give an analogous account of partial sdm-$\mathfrak{C}$-SSTs; we
leave the interested reader to work out the details.

Coming back to our main point, we now state the slight variation of the
determinization theorem for copyless SSTs [AD11] that fits our purposes. Given
an arbitrary function $F:X\to\mathcal{P}(Y)$, we say that $f:X\rightharpoonup
Y$ _uniformizes_ $F$ if and only if ${\sf{dom}}(f)=X\setminus
F^{-1}(\varnothing)$ and $\forall x\in{\sf{dom}}(f).\;f(x)\in F(x)$.

######  Theorem 40.

For every non-derministic $\mathfrak{SR}$-SSTs $\mathcal{T}$ with input
$\Sigma^{*}$, there exists a partial deterministic $\mathfrak{SR}$-SST
$\mathcal{T}^{\prime}$ such that ${\llbracket\mathcal{T}^{\prime}\rrbracket}$
uniformizes ${\llbracket\mathcal{T}\rrbracket}$.

We now show that studying the uniformization property between classes of
sdmSSTs parameterized by streaming setting $\mathfrak{C}$ and $\mathfrak{D}$
is morally the same as comparing the expressiveness of
sdm-$\mathfrak{C}_{\with}$-SSTs and sdm-$\mathfrak{D}$-SSTs.

######  Lemma 41.

Non-deterministic sdm-$\mathfrak{C}$-SSTs are uniformizable by partial
sdm-$\mathfrak{D}$-SSTs if and only if sdm-$\mathfrak{D}$-SSTs subsume
sdm-$\mathfrak{C}_{\with}$-SSTs.

######  Proof 3.11.

First, let us assume that sdm-$\mathfrak{C}$-SSTs uniformize
sdm-$\mathfrak{D}$-SSTs and let

$\mathcal{T}\;=\;\left(Q,q_{0},(A_{q})_{q\in
Q},\delta,i,o\right)\qquad\text{with}\qquad A_{q}\;=\;\bigwith_{x\in
X_{q}}C_{q,x}$

be a $\mathfrak{C}_{\with}$-SST with input $\Sigma$. We first define a non-
deterministic sdm-$\mathfrak{C}$-SST $\mathcal{T}^{\prime}$ by setting

$\begin{array}[]{c}\mathcal{T}^{\prime}=\left(I+Q^{\prime},I,(C_{p(m)})_{m\in
I+Q^{\prime}},\Delta,i^{\prime},o^{\prime}\right)\\\ \\\ \end{array}$
$\begin{array}[]{c}\begin{array}[]{lcl}Q^{\prime}&=&\sum_{q\in Q}X_{q}\\\
I&=&\sum_{x\in X_{q_{0}}}\\{f\mid
i_{*}=(x,f)\\}\end{array}\qquad\qquad\begin{array}[]{lrcl}p:&I+Q^{\prime}&\to&Q^{\prime}\\\
&\mathsf{in}_{1}(x,f)&\mapsto&(q_{0},x)\\\
&\mathsf{in}_{2}(q,x)&\mapsto&(q,x)\\\ \end{array}\end{array}$
$\begin{array}[]{c}i^{\prime}_{\mathsf{in}_{1}(x,f)}=f\qquad\qquad
o^{\prime}_{m}=\mathsf{in}_{1}\left(\pi_{2}\left((o_{\pi_{1}(p(m))})_{\pi_{2}(p(m))}\right)\right)\end{array}$
$\begin{array}[]{c}\begin{array}[]{lcl}\Delta&=&\left\\{(a,((m,\mathsf{in}_{2}(r,y)),f)_{m})\left|\begin{array}[]{llcl}\lx@intercol\forall(x,q)\in
Q^{\prime}.\forall m\in p^{-1}(x,q).\hfil\lx@intercol\\\
&\pi_{1}(\delta(a)_{q})&=&r\\\
\wedge&\pi_{2}(\delta(a)_{q})_{y}&=&(x,f)\end{array}\right.\right\\}\\\ \\\
\end{array}\end{array}$

Taking $\mathcal{T}^{\prime\prime}$ to be a sdm-$\mathfrak{D}$-SST
uniformizing $\mathcal{T}^{\prime}$, we have
$\\{-\\}\circ{\llbracket\mathcal{T}^{\prime\prime}\rrbracket}={\llbracket\mathcal{T}^{\prime}\rrbracket}=\\{-\\}\circ{\llbracket\mathcal{T}\rrbracket}$,
so we are done.

For the converse, assume that sdm-$\mathfrak{D}$-SSTs subsume
sdm-$\mathfrak{C}_{\with}$-SSTs and suppose we have some non-deterministic
sdm-$\mathfrak{C}$-SST $\mathcal{T}=(Q,I,(A_{q})_{q\in Q},\Delta,i,o)$ to
uniformize. Fix a total order $\preceq$ over the morphisms of $\mathcal{C}$
occurring in $\Delta$ (recall that there are finitely many of them). Consider
a partial deterministic sdm-$\mathfrak{C}_{\with}$-SST $\mathcal{T}^{\prime}$
obtained from $\mathcal{T}$ by a powerset construction

$\mathcal{T}^{\prime}\;\quad=\;\left(\mathcal{P}(Q),\;I,\;\left(\bigwith_{r\in
R}A_{r}\right)_{R\subseteq Q},\;\delta,\;i,\;o^{\prime}\right)$
$\text{where}\leavevmode\nobreak\ \delta(a)_{R}\leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
(S,(r_{s},f_{s})_{s\in S})\quad\text{if and only if}\quad\forall s\in
S\leavevmode\nobreak\
\left[\begin{array}[]{ll}(a,((r_{s},s),f_{s}))\in\Delta\\\ \forall
g.(a,((r_{s},s),g))\in\Delta\Rightarrow f_{s}\preceq g\end{array}\right.$

and $o^{\prime}_{R}=o\upharpoonright r$ for some arbitrary $r$ such that the
right hand-side is defined; if there is no such $r$, $o^{\prime}_{R}$ is
undefined and we call $R$ a _dead_ set of states. By padding $o^{\prime}$ with
some arbitrary values on such dead states, we may extend
$\mathcal{T}^{\prime}$ to a non-partial deterministic $\mathfrak{C}$-SST
$\mathcal{T}^{\prime\prime}$ so that
${\llbracket\mathcal{T}^{\prime}\rrbracket}\subseteq{\llbracket\mathcal{T}^{\prime\prime}\rrbracket}$.
We may then consider a sdm-$\mathfrak{D}$-SST
$\mathcal{T}^{\prime\prime\prime}=(Q^{\prime},q_{0},(D_{q})_{q\in
Q^{\prime}},\delta,i^{\prime\prime},o^{\prime\prime})$ such that
${\llbracket\mathcal{T}^{\prime}\rrbracket}(w)={\llbracket\mathcal{T}^{\prime\prime}\rrbracket}(w)={\llbracket\mathcal{T}^{\prime\prime\prime}\rrbracket}$
for $w\in{\sf{dom}}({\llbracket\mathcal{T}^{\prime}\rrbracket})$. This
$\mathcal{T}^{\prime\prime\prime}$ is almost our uniformizer; we only need to
restrict the domain of its output function. This can be achieved by adding a
$\mathcal{P}(Q)$ component to the state space corresponding to the set of
states reached by $\mathcal{T}$ and forcing the output function to be
undefined if this component contains a dead set of states.

Putting Lemma 41 together with Theorem 40 yields the desired result.

######  Theorem 42.

sdm-$\mathfrak{SR}_{\with}$-SSTs are subsumed by sdm-$\mathfrak{SR}$-SSTs.

We also provide a direct self-contained proof of the following statement
generalizing Theorem 42.

######  Theorem 43.

Let $\mathfrak{C}$ and $\mathfrak{D}$ be streaming settings such that there is
a morphism of streaming settings $\mathfrak{C}\to\mathfrak{D}$, whose
underlying functor is $F:\mathcal{C}\to\mathcal{D}$. Assume further that
$\mathcal{D}$ carries a symmetric monoidal affine structure and has internal
homsets $F(C)\multimap F(C^{\prime})$ for every pair of objects
$C,C^{\prime}\in\mathsf{Obj}(\mathcal{C})$.

Then, sdm-$\mathfrak{C}_{\with}$-SSTs are subsumed by sdm-$\mathfrak{D}$-SSTs.

Let us check that our technical development until now allows deriving Theorem
42 from the above result. We instantiate $\mathfrak{C}=\mathfrak{SR}$ and
$\mathfrak{D}=\mathfrak{SR}_{\oplus}$, with the functor
$\iota_{\oplus}:\mathcal{SR}\to\mathcal{SR}_{\oplus}$. We have already seen
that $\mathcal{SR}_{\oplus}$ is a symmetric monoidal affine category. The
assumption on internal homsets is exactly Lemma 36. The theorem then tells us
that sdm-$\mathfrak{SR}_{\with}$-SSTs are subsumed by
sdm-$\mathfrak{SR}_{\oplus}$-SSTs, and the latter are no more expressive than
sdm-$\mathfrak{SR}$-SSTs by Corollary 32.

Note that, conversely, Theorem 42 also implies Theorem 40 through Lemma 41.
Therefore, while Theorem 40 is a variant of the previously known
determinization of copyless SSTs, we generalized it in a more abstract
setting. Our main contribution is identifying the notion of internal homsets
as one of the key components which make the direct determinization proof (that
does not appear in [AD11], but might be part of the folklore, see e.g. [BC18,
Problem 139 (p. 226)]) work. The proof itself is thus rather unsuprising, but
rather involved, so we postpone it to Subsection 4.2.

###  3.6. The $\oplus\with$-completion (a Dialectica-like construction)

We now consider the composition of the coproduct completion with the product
completion $(\mathcal{C}_{\with})_{\oplus}$. Unraveling the formal definition
and distributing sums and products at the right spots, we define an isomorphic
category $\mathcal{C}_{\oplus\with}$ which is a bit less cumbersome to
manipulate in practice.

######  Theorem 44.

Given an arbitrary category $\mathcal{C}$, there is an _isomorphism of
categories_ (not just an equivalence) between $(\mathcal{C}_{\with})_{\oplus}$
and the category $\mathcal{C}_{\oplus\with}$ defined below.

  * •

The objects of $\mathcal{C}_{\oplus\with}$ are triples
$(U,(X_{u})_{u},(C_{u,x})_{(u,x)})$ where $U$ is a finite set, $(X_{u})_{u\in
U}$ is a family of finite sets and $C_{u,x}$ is a family of objects of
$\mathcal{C}$ indexed by $(u,x)\in\sum_{u\in U}X_{u}$. We drop the first index
$u$ when it is determined by $x\in X_{u}$ from context and write those objects
$\bigoplus_{u\in U}\bigwith_{x\in X_{u}}C_{x}$ for short.

  * •

Its homsets are defined as

$\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigoplus_{u\in
U}\bigwith_{x\in X_{u}}C_{x}\text{{\Huge{,}}}\;\bigoplus_{v\in
V}\bigwith_{y\in Y_{v}}C_{y}\right)\quad=\quad\prod_{u\in U}\sum_{v\in
V}\prod_{y\in Y_{v}}\sum_{x\in
X_{u}}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)$

  * •

Its identities are maps

$\begin{array}[]{c@{}c@{}c@{}c@{}c@{}c@{}c@{}cl}\displaystyle\prod_{u\in
U}&&\displaystyle\sum_{u^{\prime}\in U}&&\displaystyle\prod_{x^{\prime}\in
X_{u}}&&\displaystyle\sum_{x\in
X_{u^{\prime}}}&&\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{,x^{\prime}}\right)\\\
\\\
u&\mapsto&\big{[}u&,&\big{(}x&\mapsto&(x&,&\mathrm{id}_{C_{x}})\big{)}\big{]}\end{array}$

  * •

Composition is defined as in Figure 7. The interesting steps of this
computation are those involving $v$ and $y$; since they are similar, let us
focus on $v$. A map of the form

$\begin{array}[]{c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c}\displaystyle\prod_{v\in
V}A_{v}&\quad\times&\quad\displaystyle\sum_{v\in
V}&\;B_{v}&\quad\longrightarrow&\quad\displaystyle\sum_{v\in
V}&\;A_{v}&\;\times&\;B_{v}\\\ \\\ (a_{v})_{v\in
V}&\quad,&(v^{\prime},&b)&\quad\mapsto&(v^{\prime},&(a_{v^{\prime}}&\;,&b))\end{array}$

is applied. This makes the two $\mathcal{C}_{\oplus\with}$-morphisms interact
(an interaction represented in Remark 46 below as a move in a game): the
$v^{\prime}$ provided by the right one selects $a_{v^{\prime}}$ among all the
possibilities $(a_{v})_{v}$ proposed by the left one.

######  Proof 3.12.

By mechanical unfolding of the definitions.

$\textstyle{\displaystyle\mathsf{Hom}\left(\bigoplus\limits_{v}\bigwith\limits_{y}C_{y}\text{{\Huge{,}}}\;\bigoplus\limits_{w}\bigwith\limits_{z}C_{z}\right)\times\mathsf{Hom}\left(\bigoplus\limits_{u}\bigwith\limits_{x}C_{x}\text{{\Huge{,}}}\;\bigoplus\limits_{v}\bigwith\limits_{y}C_{y}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\prod_{v}\sum_{w}\prod_{z}\sum_{y}\mathsf{Hom}_{\mathcal{C}}\left(C_{y},C_{z}\right)\quad\times\quad\prod_{u}\sum_{v}\prod_{y}\sum_{x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\prod_{u}\left(\prod_{v}\sum_{w}\prod_{z}\sum_{y}\mathsf{Hom}_{\mathcal{C}}\left(C_{y},C_{z}\right)\;\times\;\sum_{v}\prod_{y}\sum_{x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\prod_{u}\sum_{v}\left(\sum_{w}\prod_{z}\sum_{y}\mathsf{Hom}_{\mathcal{C}}\left(C_{y},C_{z}\right)\quad\times\quad\prod_{y}\sum_{x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sim}$$\textstyle{\displaystyle\prod_{u}\sum_{v,w}\left(\prod_{z}\sum_{y}\mathsf{Hom}_{\mathcal{C}}\left(C_{y},C_{z}\right)\quad\times\quad\prod_{y}\sum_{x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\prod_{u}\sum_{v,w}\prod_{z}\left(\sum_{y}\mathsf{Hom}_{\mathcal{C}}\left(C_{y},C_{z}\right)\quad\times\quad\prod_{y}\sum_{x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\prod_{u}\sum_{v,w}\prod_{z}\sum_{y}\left(\mathsf{Hom}_{\mathcal{C}}\left(C_{y},C_{z}\right)\quad\times\quad\sum_{x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sim}$$\textstyle{\displaystyle\prod_{u}\sum_{v,w}\prod_{z}\sum_{y,x}\left(\mathsf{Hom}_{\mathcal{C}}\left(C_{y},C_{z}\right)\times\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$composition
in
$\mathcal{C}$$\textstyle{\displaystyle\prod_{u}\sum_{v,w}\prod_{z}\sum_{y,x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{z}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$project
away
$v,y$$\textstyle{\displaystyle\prod_{u}\sum_{w}\prod_{z}\sum_{x}\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{z}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigoplus_{u}\bigwith_{x}C_{x}\text{{\Huge{,}}}\;\bigoplus_{w}\bigwith_{z}C_{z}\right)}$

Figure 7. Composition in $\mathcal{C}_{\oplus\with}$ ($-\in-$ are omitted from
indices)

######  Remark 45.

The reader may notice that composition in $\mathcal{C}_{\oplus\with}$ is very
similar to the interpretation of cuts in Gödel’s Dialectica interpretation
[Göd58] and/or composition in categories of _polynomial functors_ [GK13,
MvG18]. This intuition can be made formal. In particular, see [Hof11] for a
decomposition of a general version of the categorical Dialectica construction
into free completions with _simple_ sums and products. In our context, the
completion with simple coproducts would be the $(-)_{\oplus\mathrm{const}}$ of
Remark 35; conversely, a “dependent Dialectica” could be defined in the
fibrational setting of [Hof11] analogously to our
$(-)_{\oplus\with}$-completion by removing the simplicity restriction.

######  Remark 46.

For the uninitiated, it can be helpful to compute this completion on the
trivial category $\mathbbl{1}$ with one object and only its identity morphism.
In this case, objects consists of a pair of a finite set $U$ together with a
family $(X_{u})_{u\in U}$ of finite sets that can be regarded as a two-move
sequential game (with no outcome) between player $\oplus$ and $\with$: first
$\oplus$ plays some $u\in U$ and then $\with$ plays some $x\in X_{u}$. One can
then consider _simulation games_ between $(U,(X_{u})_{u})$ (the “left hand-
side”) and $(V,(Y_{v})_{v})$ (the “right hand-side”) proceeding as follows:

• first, $\with$ plays some $u\in U$ on the left • then, $\oplus$ plays some $v\in V$ on the right • $\with$ answers with some $y\in Y_{v}$ on the right • finally $\oplus$ answers with $x\in X_{u}$ on the left. |  $\begin{array}[]{l| l @{~}c@{~} ll l @{~}c@{~} @{~}c}&U\hfil\leavevmode\nobreak\ &,\hfil\leavevmode\nobreak\ &(X_{u})_{u}&\to&V,\hfil\leavevmode\nobreak\ &(Y_{v})_{v}\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \\\ \hline\cr\with&u\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ &&&\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \\\ \oplus&\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ &&&v\hfil\leavevmode\nobreak\ \\\ \with&\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ &&&\hfil\leavevmode\nobreak\ &y\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \\\ \oplus&\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ &x\\\ \end{array}$
---|---

Morphisms in $\mathbbl{1}_{\oplus\with}$ are $\oplus$-strategies in such
games. Identities correspond to copycat strategies and composition is (a
simple version) of an usual scheme in game semantics. As for
$\mathcal{C}_{\oplus\with}$, one may consider that once this simulation game
is played, $\oplus$ needs to provide a datum in some
$\mathsf{Hom}_{\mathcal{C}}\left(C_{x},C_{y}\right)$ which depends on the
outcome of the game.

We write $\iota_{\oplus\with}:\mathcal{C}\to\mathcal{C}_{\oplus\with}$ for the
(full and faithful) embedding sending an object $C$ to the one-element family
$\bigoplus_{1}C$. As the coproduct completion preserves limits, it means that
$\mathcal{C}_{\oplus\with}$ always boasts both binary cartesian products and
coproducts. Concretely, products are computed using the distributivity of
products over coproducts

$\bigwith_{i\in I}\bigoplus_{j\in
J_{i}}A_{j}\quad\cong\quad\bigoplus_{f\in\prod_{i\in I}J_{i}}\bigwith_{i\in
I}A_{f(i)}$

If $\mathcal{C}$ has a symmetric monoidal structure $(\otimes,\mathbf{I})$,
the lifting is computed in $\mathcal{C}_{\oplus\with}$ as

$\bigotimes_{i\in I}\leavevmode\nobreak\ \leavevmode\nobreak\ \bigoplus_{u\in
U_{i}}\leavevmode\nobreak\ \leavevmode\nobreak\ \bigwith_{x\in
X_{u}}\leavevmode\nobreak\ \leavevmode\nobreak\
C_{x}\qquad=\qquad\bigoplus_{f\in\prod\limits_{i\in
I}U_{i}}\leavevmode\nobreak\ \leavevmode\nobreak\
\bigwith_{g\in\prod\limits_{i\in I}X_{i,f(i)}}\leavevmode\nobreak\
\leavevmode\nobreak\ \bigotimes_{i\in I}\leavevmode\nobreak\
\leavevmode\nobreak\ C_{g(i)}$

####  3.6.1. The monoidal closure theorem

Recall from the introduction that a result of central importance in this paper
is the fact that the category $(\mathcal{SR}_{\with})_{\oplus}$ is symmetric
monoidal closed (Theorem 3). This will be a consequence of the general
property below.

######  Theorem 47.

Let $(\mathcal{C},\otimes,\mathbf{I})$ be a symmetric monoidal category.
Assume that its coproduct completion $\mathcal{C}_{\oplus}$ admits internal
homsets $\iota_{\oplus}(A)\multimap\iota_{\oplus}(B)$ for every
$A,B\in\mathsf{Obj}(\mathcal{C})$. Then its Dialectica-like completion
$\mathcal{C}_{\oplus\with}$ is monoidal closed.

Indeed, since Lemma 36 gives us precisely the assumption on internal homsets
in the above statement for $\mathcal{C}=\mathcal{SR}$, we immediately get:

######  Corollary 48 (equivalent to Theorem 3).

$\mathcal{SR}_{\oplus\with}$ is monoidal closed.

$\begin{array}[]{l}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(A\otimes
B,C\right)\\\ \begin{array}[]{lcl@{\kern
0em}c}&=&{\displaystyle\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\left[\bigoplus_{w\in
W}\bigwith_{z\in
Z_{w}}\iota_{\oplus\with}(A_{z})\right]\otimes\left[\bigoplus_{u\in
U}\bigwith_{x\in
X_{u}}\iota_{\oplus\with}(B_{x})\right]\text{{\Huge{,}}}\;\bigoplus_{v\in
V}\bigwith_{y\in Y_{v}}\iota_{\oplus\with}(C_{y})\right)}\hfil\kern 0.0pt\\\
&=&{\displaystyle\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigoplus_{(w,u)\in
W\times U}\bigwith_{(z,x)\in Z_{w}\times
X_{u}}\iota_{\oplus\with}(A_{z}\otimes
B_{x})\text{{\Huge{,}}}\;\bigoplus_{v\in V}\bigwith_{y\in
Y_{v}}\iota_{\oplus\with}(C_{y})\right)}\hfil\kern 0.0pt\\\
&\cong&{\displaystyle\prod_{w\in W}\prod_{u\in U}\sum_{v\in V}\prod_{y\in
Y_{v}}\sum_{z\in Z_{w}}\sum_{x\in
X_{u}}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\iota_{\oplus\with}(A_{z})\otimes\iota_{\oplus\with}(B_{x})\text{{\Huge{,}}}\;\iota_{\oplus\with}(C_{y})\right)}\hfil\kern
0.0pt\\\ &\cong&{\displaystyle\prod_{w\in W}\prod_{u\in U}\sum_{v\in
V}\prod_{y\in Y_{v}}\sum_{z\in Z_{w}}\sum_{x\in
X_{u}}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\iota_{\oplus\with}(A_{z})\text{{\Huge{,}}}\;\iota_{\with}^{\oplus}(\iota_{\oplus\with}(B_{x})\multimap\iota_{\oplus\with}(C_{y}))\right)}\hfil\kern
0.0pt\\\ &\cong&{\displaystyle\prod_{w\in W}\prod_{u\in U}\sum_{v\in
V}\prod_{y\in Y_{v}}\sum_{z\in
Z_{w}}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\iota_{\oplus\with}(A_{z})\text{{\Huge{,}}}\;\bigoplus_{x\in
X_{u}}\iota_{\with}^{\oplus}(\iota_{\oplus\with}(B_{x})\multimap\iota_{\oplus\with}(C_{y}))\right)}\hfil\kern
0.0pt&\text{\raisebox{20.00003pt}{$(\dagger)$}}\\\
&\cong&{\displaystyle\prod_{w\in W}\prod_{u\in U}\sum_{v\in V}\prod_{y\in
Y_{v}}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigwith_{z\in
Z_{w}}\iota_{\oplus\with}(A_{z})\text{{\Huge{,}}}\;\bigoplus_{x\in
X_{u}}\iota_{\with}^{\oplus}(\iota_{\oplus\with}(B_{x})\multimap\iota_{\oplus\with}(C_{y}))\right)}\hfil\kern
0.0pt&\text{\raisebox{20.00003pt}{$(\heartsuit)$}}\\\
&\cong&{\displaystyle\prod_{w\in W}\prod_{u\in U}\sum_{v\in
V}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigwith_{z\in
Z_{w}}\iota_{\oplus\with}(A_{z})\text{{\Huge{,}}}\;\bigwith_{y\in
Y_{v}}\bigoplus_{x\in
X_{u}}\iota_{\with}^{\oplus}(\iota_{\oplus\with}(B_{x})\multimap\iota_{\oplus\with}(C_{y}))\right)}\hfil\kern
0.0pt\\\ &\cong&{\displaystyle\prod_{w\in W}\prod_{u\in
U}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigwith_{z\in
Z_{w}}\iota_{\oplus\with}(A_{z})\text{{\Huge{,}}}\;\bigoplus_{v\in
V}\bigwith_{y\in Y_{v}}\bigoplus_{x\in
X_{u}}\iota_{\with}^{\oplus}(\iota_{\oplus\with}(B_{x})\multimap\iota_{\oplus\with}(C_{y}))\right)}\hfil\kern
0.0pt&\text{\raisebox{20.00003pt}{$(\dagger)$}}\\\
&\cong&{\displaystyle\prod_{w\in
W}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigwith_{z\in
Z_{w}}\iota_{\oplus\with}(A_{z})\text{{\Huge{,}}}\;B\multimap
C\right)}\hfil\kern 0.0pt\\\
&\cong&\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(A,B\multimap
C\right)\hfil\kern 0.0pt\\\ \end{array}\\\ \\\ \hline\cr\end{array}$ Figure 8.
Monoidal closure of $\mathcal{C}_{\oplus\with}$ (Theorem 47).

Let us now sketch how the proof of Theorem 47 goes. To this end, assume that
we have $A=\bigoplus_{u\in U}\bigwith_{x\in X_{u}}\iota_{\oplus\with}(A_{x})$
and $B=\bigoplus_{v\in V}\bigwith_{y\in Y_{v}}\iota_{\oplus\with}(B_{y})$ be
objects of $\mathcal{C}_{\oplus\with}$ and assume that we have internal
homsets $\iota_{\oplus\with}(A_{x})\multimap\iota_{\oplus\with}(B_{y})$ for
every $(u,x)\in\sum_{u\in U}X_{u}$ and $(v,y)\in\sum_{v\in V}Y_{v}$. Let

$\iota_{\with}^{\oplus}:\mathcal{C}_{\oplus}\to\mathcal{C}_{\oplus\with}\quad\text{such
that}\quad\iota_{\oplus\with}=\iota_{\with}^{\oplus}\circ\iota_{\oplus}$

be the full and faithful embedding be obtained by applying the universal
property of $\mathcal{C}_{\oplus}$ to the coproduct-preserving functor
$\iota_{\oplus\with}$. The linear arrow $A\multimap B$ can then be defined as
follows

$A\multimap B\quad=\quad\bigwith_{u\in U}\bigoplus_{v\in V}\bigwith_{y\in
Y_{v}}\bigoplus_{x\in
X_{u}}\iota_{\with}^{\oplus}(\iota_{\oplus}(A_{x})\multimap\iota_{\oplus}(B_{y}))$

It is clear that this is meant to mimick the definition of
$\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(-,-\right)$ by substituting
external hom, products and coproducts with internal ones, as is customary with
Dialectica. To show that $B\multimap-$ is right adjoint to $-\otimes B$, one
may directly establish that we have an isomorphism of homsets

$\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(A\otimes
B,C\right)\cong\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(A,B\multimap
C\right)$

_natural in $A$_ using the recipe of Figure 8. Unmarked steps follow from
definitions or standard abstract nonsense (characterization of internal
(co)products in terms of external ones). The two $(\dagger)$ steps involve
instances of the isomorphism

$\sum_{i\in I}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigwith_{x\in
X}\iota_{\oplus\with}(Z_{x})\text{{\Huge{,}}}\;D_{i}\right)\leavevmode\nobreak\
\leavevmode\nobreak\ \cong\leavevmode\nobreak\ \leavevmode\nobreak\
\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigwith_{x\in
X}\iota_{\oplus\with}(Z_{x})\text{{\Huge{,}}}\;\bigoplus_{i\in I}D_{i}\right)$

which holds for any family $(Z_{x})_{x\in X}$ of objects of $\mathcal{C}$ and
family $(D_{i})_{i\in I}$ of objects of $\mathcal{C}_{\oplus\with}$. This is a
formal computation corresponding to the tail end of Proposition 28, which
applies because of the equivalence
$\mathcal{C}_{\oplus\with}\cong\left(\mathcal{C}_{\with}\right)_{\oplus}$.

The most subtle step, labelled with $(\heartsuit)$, necessitates a more
detailed computation that relies crucially on the fact that
$\iota_{\with}^{\oplus}(\iota_{\oplus}(A_{x})\multimap\iota_{\oplus}(B_{y}))$
is $\with$-free. This can be regarded as a generic isomorphism for arbitrary
families of objects $(E_{u})_{u\in U}$ and $(Z_{x})_{x\in X}$ of $\mathcal{C}$

$\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(\bigwith_{x\in
X}\iota_{\oplus\with}(Z_{x}),\bigoplus_{u\in
U}\iota_{\oplus\with}(E_{u})\right)\quad\cong\quad\sum_{x\in
X}\mathsf{Hom}_{\mathcal{C}_{\oplus\with}}\left(Z_{x},\bigoplus_{u\in
U}\iota_{\oplus\with}(E_{u})\right)$

which is easy to compute explicitly.

In addition to checking that there is a chain of isomorphisms as per Figure 8,
it should also be checked that they are natural in $A$. This requires
identifying precisely what presheaves over $\mathcal{C}_{\oplus\with}$ are
involved at every step and arguing that the maps are indeed natural. This is
not necessarily so straightforward, so we offer a more detailed proof of
Theorem 47 in Appendix D.

###  3.7. Proof of the main result on strings

We can now give the proof of Theorem 1, which can be summarized as the
equality

$\text{$\lambda\ell^{\oplus\with}$-definable}\leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
\text{$\mathfrak{SR}$-SSTs}$

thanks to Fact 17. We start with the consequences of our syntactic analysis

$\text{$\lambda\ell^{\oplus\with}$-definable}\;\underset{\overset{\uparrow}{\text{Lemma\leavevmode\nobreak\
\ref{lem:lamlsst}}}}{=}\;\text{single-state
$\mathfrak{L}$-SSTs}\;\underset{\overset{\uparrow}{\text{Lemma\leavevmode\nobreak\
\ref{lem:coprod-whatever}}}}{=}\;\text{$\mathfrak{L}$-SSTs}$

reducing our goal to

$\text{$\mathfrak{L}$-SSTs}\leavevmode\nobreak\ \leavevmode\nobreak\
=\leavevmode\nobreak\ \leavevmode\nobreak\ \text{$\mathfrak{SR}$-SSTs}$

For the above equality, the right-to-left inclusion is simpler than its
converse: the existence of a morphism of streaming settings from
$\mathfrak{SR}$ to $\mathfrak{L}$ (Lemma 26) entails that $\mathfrak{L}$-SSTs
subsume $\mathfrak{SR}$-SSTs (by Lemma 14). (Were we only interested only
proving that regular functions are $\lambda\ell^{\oplus\with}$-definable, our
setting would be a complete overkill.)

On the other hand, the other direction mobilizes almost the whole development.
First, our semantic evaluation argument combines Lemma 27 with Corollary 48 to
get

$\text{$\mathfrak{L}$-SSTs}\leavevmode\nobreak\ \leavevmode\nobreak\
\subseteq\leavevmode\nobreak\ \leavevmode\nobreak\
\text{$\mathfrak{SR}_{\oplus\with}$-SSTs}$

We then finish proving Theorem 1 with automata-theoretic considerations:

$\text{$\mathfrak{SR}_{\oplus\with}$-SSTs}\;\underset{\overset{\uparrow}{\text{Lemma\leavevmode\nobreak\
\ref{lem:sdmSST-
oplus}}}}{=}\;\text{sdm-$\mathfrak{SR}_{\with}$-SSTs}\;\underset{\overset{\uparrow}{\text{Theorem\leavevmode\nobreak\
\ref{thm:with-reg-conservativity}}}}{=}\;\text{sdm-$\mathfrak{SR}$-SSTs}$

$\text{sdm-$\mathfrak{SR}$-SSTs}\;\underset{\overset{\uparrow}{\text{Corollary\leavevmode\nobreak\
\ref{cor:oplus-sst-reg-
conservative}}}}{=}\;\text{$\mathfrak{SR}_{\oplus}$-SSTs}\;\underset{\overset{\uparrow}{\text{Lemma\leavevmode\nobreak\
\ref{lem:coprod-whatever}}}}{=}\;\text{$\mathfrak{SR}$-SSTs}$

##  4\. Some transducer-theoretic applications of $\mathfrak{C}$-SSTs and
internal homsets

This section is devoted to showing that the notion of monoidal closure can be
used to give a satisfying self-contained description of two important
transformations of usual streaming string transducers, both of which are not
entirely straightforward: the composition of two copyless SSTs and the
uniformization of non-deterministic copyless SSTs.

We take advantage of our abstract setting to give proofs for categorical
generalizations of those two statements, similarly in spirit to the
generalized minimization argument found in [CP20]. The specialized theorem
then follows easily from previous theorems in our developments having to do
with monoidal closure, especially Theorem 47 and Lemma 36.

The ideas behind our arguments are not new; our main goal is to vindicate the
view that the notion of internal homset is the key to showing those results,
even if it does not appear explicitly in previous arguments.

###  4.1. On closure under precomposition by regular functions

First, let us recall right off the bat that the closure under composition of
functions definable by copyless streaming string transducers follows from our
main result on strings (Theorem 1) together with basic considerations on typed
$\lambda$-calculi (see e.g. [NP20, Lemma 2.8] that applies mutatis mutandis to
the $\lambda\ell^{\oplus\with}$-calculus) that entail the closure under
composition of $\lambda\ell^{\oplus\with}$-definable functions. However, note
that Theorem 1 relies on the syntactic analysis of Lemma 25, which is arguably
a non-trivial result about the $\lambda\ell^{\oplus\with}$-calculus (as
demonstrated by the size of Appendices B and C, which are both necessary to
prove it).

The argument we give in this section circumvents that difficulty and does not
appeal to Theorem 1 nor to Lemma 25. That said, it still shares some (non-
syntactic) ingredients with our proof of Theorem 1, namely:

  * •

the monoidal closure and quasi-affineness (see below) of
$\mathcal{SR}_{\oplus\with}$;

  * •

the fact that $\mathfrak{SR}_{\oplus\with}$-SSTs are no more expressive than
$\mathfrak{SR}$-SSTs.

These results still require substantial developments – indeed, this
composition property is quite non-trivial as mentioned in the introduction –
but bypass the need of mentioning the $\lambda\ell^{\oplus\with}$-calculus.

Beyond this simplification, the main advantage of our approach here is that we
get a more general theorem, that applies to many streaming settings; in
particular, the final output does not have to be a string. Without further
ado, let us state it.

######  Theorem 49.

Let $\mathfrak{C}$ be a string streaming setting with output set $X$. Suppose
that the underlying category $\mathcal{C}$ is _symmetric monoidal closed_ and
_quasi-affine_. Furthermore, let us assume that
$\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}_{\mathfrak{C}}$ is
equal to the monoidal unit $\mathbf{I}$.

Then for any $f:\Gamma^{*}\to X$ computed by some $\mathfrak{C}$-SST, and any
regular $g:\Sigma^{*}\to\Gamma^{*}$, the function $f\circ g:\Sigma^{*}\to X$
is computed by some (stateful) $\mathfrak{C}$-SST. In other words, the class
of functions defined by $\mathfrak{C}$-SSTs is _closed under precomposition by
regular functions_.

Before proving the above theorem, let us check that it entails known
preservation and composition properties.

######  Corollary 50.

Let $L\subseteq\Gamma^{*}$ be a regular language and
$g:\Sigma^{*}\to\Gamma^{*}$ be a regular function. Then the language
$g^{-1}(L)\subseteq\Sigma^{*}$ is regular.

######  Proof 4.1.

That $L$ is regular is equivalent to its indicator function
$\chi_{L}:\Gamma^{*}\to\\{0,1\\}$ being computed by some single-state
$\mathfrak{Finset}_{2}$-SST, see Example 13. The underlying category of finite
sets is _cartesian closed_ , and the monoidal structure given by a cartesian
product is automatically symmetric and affine. According to Theorem 49,
$\chi_{L}\circ g$ can therefore be computed by some
$\mathfrak{Finset}_{2}$-SST. Observing that the category of finite sets has
coproducts, and applying Lemma 34, we even have a _single-state_
$\mathfrak{Finset}_{2}$-SST for $\chi_{L}\circ g$. Finally, the latter is none
other than the indicator function of $g^{-1}(L)$.

######  Corollary 51.

Let $f:\Gamma^{*}\to\Delta^{*}$ and $g:\Sigma^{*}\to\Gamma^{*}$ be regular
functions. Then $f\circ g$ is also a regular function.

######  Proof 4.2.

This is just the application of Theorem 49 to
$\mathfrak{SR}_{\oplus\with}$-SSTs – indeed, we saw at the very end of Section
3 that the functions computed by $\mathfrak{SR}_{\oplus\with}$-SSTs are
exactly the regular functions. By Theorem 3 / Corollary 48, the underlying
category $\mathcal{SR}_{\oplus\with}$ is symmetric monoidal closed. Finally,
$\mathcal{SR}_{\oplus\with}$ is quasi-affine since it has all cartesian
products by construction.

We now come to the proof of this generalized preservation theorem.

######  Proof 4.3 (Proof of Theorem 49).

We give below a proof assuming that $f$ is defined by some _single-state_
$\mathfrak{C}$-SST (but beware: the $\mathfrak{C}$-SST computing $f\circ g$
will still be stateful!). The general case can be applied by considering the
streaming setting $\mathfrak{C}_{\oplus\mathrm{const}}$-SST, as was briefly
mentioned in Remark 35, and using the fact that single-state
$\mathfrak{C}_{\oplus\mathrm{const}}$-SSTs, stateful
$\mathfrak{C}_{\oplus\mathrm{const}}$-SSTs and stateful $\mathfrak{C}$-SSTs
are equally expressive. We leave it to the reader to check that the symmetric
monoidal structure and the cartesian products in $\mathcal{C}$ can be lifted
to $\mathcal{C}_{\oplus\mathrm{const}}$, making this generalization possible.

Therefore, we may assume without loss of generality that $f$ is computed by a
single-state $\mathfrak{C}$-SST
$T_{f}=(\\{\bullet\\},A_{f},\delta_{f},i_{f},o_{f})$ where $A_{f}$ is an
object of $\mathcal{C}$ and

$\delta_{f}:\Gamma\to\mathsf{Hom}_{\mathcal{C}}\left(A_{f},A_{f}\right)\qquad
i_{f}\in\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},A_{f}\right)\qquad
o_{f}\in\mathsf{Hom}_{\mathcal{C}}\left(A_{f},\Bot\right)$

Let $T_{g}=(Q,q_{0},R_{g},\delta_{g},i_{g},o_{g})$ be an usual copyless SST
(i.e., a $\mathcal{SR}$-SST) computing the regular function $g$, where $Q$ and
$R_{g}$ are finite sets and

$q_{0}\in Q\qquad\delta_{g}:\Sigma\times Q\to
Q\times[R_{g}\to_{\mathcal{SR}}R_{g}]$
$i_{g}\in[\varnothing\to_{\mathcal{SR}}R_{g}]\qquad
o_{g}:Q\to[R_{g}\to_{\mathcal{SR}}\\{\bullet\\}]$

We will write $A=A_{f}$ and $R=R_{g}$ for short.

We want to build from this data a $\mathfrak{C}$-SST $T$ defining $f\circ g$.
Since $\mathcal{C}$ is quasi-affine and symmetric monoidal closed, we can
apply Corollary 22 to the object $A\multimap A$ and to a family of morphisms
$(\widetilde{\delta_{f}}(c))_{c\in\Gamma}\in\mathsf{Hom}_{\mathcal{C}}\left(A\multimap
A,\;A\multimap A\right)^{\Gamma}$ that will be defined later. This gives us a
functor $F_{\delta_{f}}:\mathcal{SR}\to\mathcal{C}$, enjoying various
properties that will be progressively recalled, which is at the heart of our
construction.

The set of states of our new $\mathfrak{C}$-SST $T$ is $Q$, with initial state
$q_{0}$, and its memory object is $F_{\delta_{f}}(R)$. The initialization
morphism is defined as
$i=F_{\delta_{f}}(i_{g})\in\mathsf{Hom}_{\mathcal{C}}\left(\mathbf{I},F_{\delta_{f}}(R)\right)$
– we use the assumption
$\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}=\mathbf{I}$, and the
fact that $F_{\delta_{f}}(\varnothing)=\mathbf{I}$ (by Corollary 22). The
transition function is

$\begin{array}[]{c@{}c@{}c@{}c@{}c@{}c@{}c@{}c}\delta:&\quad\Sigma&\;\times&\;Q&\quad\longrightarrow&Q&\times&\quad\mathsf{Hom}_{\mathcal{C}}\left(F_{\delta_{f}}(R),F_{\delta_{f}}(R)\right)\\\
\\\ &\quad
c&\;,&q&\quad\mapsto&\quad\pi_{1}(\delta_{g}(c,q))&,&F_{\delta_{f}}(\pi_{2}(\delta_{g}(c,q)))\end{array}$

Finally, using $j_{f}:F_{\delta_{f}}(\\{\bullet\\})\to A$ to be defined later,
we take as our new output function

$o:q\in Q\mapsto o_{f}\circ j_{f}\circ
F_{\delta_{f}}(o_{g}(q))\in\mathsf{Hom}_{\mathcal{C}}\left(F_{\delta_{f}}(R),\Bot\right)$

Let us now sketch the verification that this defines the intended function
$f\circ g:\Sigma^{*}\to X$. In the process, we will fill the missing
definitions to make everything work out.

Let $w=w_{1}\ldots w_{n}\in\Sigma^{*}$ be an input string. The sequence
$q_{0},\ldots,q_{n}\in Q$ of states visited by both $T_{g}$ and $T$ when fed
this input is obtained by $q_{i+1}=\pi_{1}(\delta_{g}(w_{i},q_{i}))$ from the
initial $q_{0}$. By definition of the output of $T_{g}$, we have:

$\widehat{g(w)}\quad=\quad
o_{g}(q_{n})\circ\pi_{2}(\delta_{g}(w_{n},q_{n-1}))\circ\dots\circ\pi_{2}(\delta_{g}(w_{1},q_{0}))\circ
i_{g}$

where $\widehat{g(w)}\in[\varnothing\to_{\mathcal{SR}(\Gamma)}\\{\bullet\\}]$
corresponds to $g(w)\in\Gamma^{*}$ (cf. Theorem 20) and the ‘$\circ$’ denotes
a composition of register transitions (i.e. of $\mathcal{SR}$-morphisms).
Similarly, the output $T(w)$ of the $\mathfrak{C}$-SST $T$ that we built on
the input $w$ is defined as

$T(w)\quad=\quad{\llparenthesis o(q_{n})\circ
F_{\delta_{f}}(\pi_{2}(\delta_{g}(w_{n},q_{n-1})))\circ\dots\circ
F_{\delta_{f}}(\pi_{2}(\delta_{g}(w_{1},q_{0})))\circ i\rrparenthesis}$

which, by unfolding the definitions of $o$ and $i$, applying the functoriality
of $F_{\delta_{f}}$ and comparing with the previous equality, one can simplify
into

$T(w)\quad=\quad{\llparenthesis o_{f}\circ j_{f}\circ
F_{\delta_{f}}\\!\left(\widehat{g(w)}\right)\rrparenthesis}$

It is now time to define
$j_{f}\in\mathsf{Hom}_{\mathcal{C}}\left(F_{\delta_{f}}(\\{\bullet\\}),A\right)$.
To do so, let us first introduce

$\mathsf{appto}(\varphi)\;:\;B\multimap C\xrightarrow{\;\sim\;}(B\multimap
C)\otimes\mathbf{I}\xrightarrow{\;\mathrm{id}\otimes\varphi\;}(B\multimap
C)\otimes B\xrightarrow{\;\mathrm{ev}\;}C$

where the last arrow is the evaluation map $\mathrm{ev}_{B,C}$, for any
$B,C\in\mathsf{Obj}(\mathcal{C})$ and $\varphi:\mathbf{I}\to B$. An useful
property, whose verification we leave to the reader, is

$\mathsf{appto}(\varphi)\circ\Lambda^{\prime}(\psi)\quad=\quad\psi\circ\varphi\qquad\text{for
any}\ \psi:B\to C$

where
$\Lambda^{\prime}:\mathsf{Hom}_{\mathcal{C}}\left(B,C\right)\xrightarrow{\sim}\mathsf{Hom}_{\mathcal{C}}\left(\mathbf{I},\,B\multimap
C\right)$ is defined in Proposition 10. We then take

$j_{f}\;:\;F_{\delta_{f}}(\\{\bullet\\})\xrightarrow{\;\pi_{1}\;}(A\multimap
A)\multimap(A\multimap
A)\xrightarrow{\;\mathsf{appto}(\Lambda^{\prime}(\mathrm{id}_{A}))}A\multimap
A\xrightarrow{\;\mathsf{appto}(i_{f})\;}A$

where $\pi_{1}$ is the left projection from
$F_{\delta_{f}}(\\{\bullet\\})=((A\multimap A)\multimap(A\multimap
A))\with\mathbf{I}$ (this equality is guaranteed by Corollary 22) and $i_{f}$
is the initialization morphism of $T_{f}$. Using the equation

$F_{\delta_{f}}\\!\left(\widehat{g(w)}\right)\quad=\quad\left\langle\Lambda^{\prime}\left(\widetilde{\delta_{f}}(g(w)_{1})\circ\dots\circ\widetilde{\delta_{f}}(g(w)_{m})\right),\;\mathrm{id}_{\mathbf{I}}\right\rangle\quad\text{where}\
m={|g(w)|}$

coming from Corollary 22, we then have

$j_{f}\circ
F_{\delta_{f}}\\!\left(\widehat{g(w)}\right)\quad=\quad\mathsf{appto}(i_{f})\circ\widetilde{\delta_{f}}(g(w)_{1})\circ\dots\circ\widetilde{\delta_{f}}(g(w)_{m})\circ\Lambda^{\prime}(\mathrm{id}_{A})$

Next, we define
$\widetilde{\delta_{f}}(c)=\Lambda(\mathrm{ev}_{A,A}\circ(\mathrm{id}_{A\multimap
A}\otimes\delta_{f}(c)))\in\mathsf{Hom}_{\mathcal{C}}\left(A\multimap
A,\;A\multimap A\right)$ for $c\in\Gamma$. In other words,
$\widetilde{\delta_{f}}(c)$ is the curryfication of

$(A\multimap A)\otimes
A\xrightarrow{\;\mathrm{id}\otimes\delta_{f}(c)\;}(A\multimap A)\otimes
A\xrightarrow{\;\mathrm{ev}\;}A$

One can then check that
$\widetilde{\delta_{f}}(c)\circ\Lambda^{\prime}(\psi)=\Lambda^{\prime}(\psi\circ(\delta_{f}(c)))$
for any $\psi:A\to A$. Putting everything together, we finally have

$\displaystyle T(w)$ $\displaystyle={\llparenthesis
o_{f}\circ\mathsf{appto}(i_{f})\circ\widetilde{\delta_{f}}(g(w)_{1})\circ\dots\circ\widetilde{\delta_{f}}(g(w)_{m})\circ\Lambda^{\prime}(\mathrm{id}_{A})\rrparenthesis}$
$\displaystyle={\llparenthesis
o_{f}\circ\mathsf{appto}(i_{f})\circ\Lambda^{\prime}(\delta_{f}(g(w)_{m})\circ\dots\circ\delta_{f}(g(w)_{1}))\rrparenthesis}$
$\displaystyle={\llparenthesis
o_{f}\circ\delta_{f}(g(w)_{m})\circ\dots\circ\delta_{f}(g(w)_{1})\circ
i_{f}\rrparenthesis}$

and this final expression is precisely the definition of the output of $T_{f}$
on $g(w)$. Since $T_{f}$ computes $f$, we end up with $T(w)=f(g(w))$, as we
wanted.

To conclude this section, let us note that an analogous result for
precomposition by regular tree functions can be shown by leveraging the
results of Section 5; we leave it as an exercise. An important subtlety: since
the presence of the additive conjunction is important to compute regular tree
functions (as we stressed in the introduction), one must consider tree
streaming settings whose underlying categories _have finite cartesian
products_ (which entails quasi-affineness).

###  4.2. Uniformization through monoidal closure

We recall below the categorical uniformization theorem that we used in Section
3.5 and provide its proof. See 43

Recall that according to Lemma 41, the conclusion amounts to saying that non-
deterministic sdm-$\mathfrak{C}$-SSTs are uniformizable by partial
sdm-$\mathfrak{D}$-SSTs.

######  Proof 4.4.

We do not prove the statement in excruciating details, but provide key formal
definitions so that a reader familiar with a modicum of automata theory and
category theory should be able to reconstitute a fully formal argument with
ease. Let us stress once again that all of the combinatorics may be regarded
as adaptation of known arguments.

The argument is based on a notion of _transformation forest_ , a name that we
borrow from [BC18, Chapter 13] for an extremely similar concept222222There are
two formal differences between our notions, which are not very big but worth
mentioning for readers of [BC18]. First, edges of a transformation forest are
intended to be associated with (elements of) a monoid, while ours should be
associated with (“elements of”) internal homsets $F(C_{u})\multimap F(C_{v})$.
Were we trying to prove $\mathfrak{D}$-uniformization for $\mathfrak{C}$-SSTs,
we would have necessarily $C_{u}=C_{v}$ and the aforementioned object would
have a monoid structure internal to $\mathcal{D}$, so this distinction is more
an artefact of our settings rather than an essential one. Second, what [BC18]
calls transformation forests refers to a class of forest with “no junk”, such
as dangling leaves not referring to an intended output or spurious internal
nodes, while we allow those in an initial definition; we add the adjective
“normalized” for those containing “no junk” as we shall see later, so this is
merely a terminological detail.. This gadget is also reminiscent of trees used
in determinization procedures like the Muller-Schupp construction for automata
over $\omega$-words [MS95] (another exposition can be found in [BC18, Chapter
1]), and of the sharing techniques used in the original paper on SSTs [AČ10,
§5.2]. In determinization procedures, this constitutes an elaboration of
powerset constructions recalling not only reachable states, but also crucial
information on _how_ those states are reached. Here, the vertices $v$ of such
forests will be labelled by objects $C_{v}$ of $\mathcal{C}$ and each edge
$(u,v)$ will be correspond to a “register containing a value of type
$F(C_{u})\multimap F(C_{v})$”.

We decompose this proof sketch in three parts: first, we introduce
transformation forests, their semantic interpretation as families of maps in
$\mathcal{D}$; we explain how they may be composed and that maps in
$\mathcal{C}_{\with}$ may be regarded as depth-1 transformation forests. Then,
we explain how to reduce the size of transformation forests in a sound way
(this is the crucial part ensuring that the resulting sdm-$\mathfrak{D}$-SSTs
will have finitely many states). Finally, we explain how to put all of this
together to uniformize sdm-$\mathfrak{C}$-SSTs.

####  4.2.1. Transformation forests and their semantics

A transformation forest is defined as a tuple
$\mathcal{F}=(V,E,O,(C_{v})_{v\in V})$ where

  * •

$V$ is a non-empty finite set of vertices

  * •

$E\subseteq V^{2}$ is a set of directed edges, pointing from parents to
children

  * •

$O$ is a non-empty subset of $V$ which we cal the set of _output nodes_

  * •

every $C_{v}$ is an object of $\mathcal{C}$

When a transformation forest $\mathcal{F}$ is fixed, we call $I_{\mathcal{F}}$
its set of roots (which we may sometimes _input nodes_ ; we drop the subscript
when there is no ambiguity). Given a transformation forest
$\mathcal{F}=(V,E,(v_{o})_{o\in O},(C_{v})_{v\in V})$, we assign the following
object of $\mathcal{D}$:

$\mathrm{Ty}(\mathcal{F})\quad=\quad\bigotimes_{(u,v)\in E}F(C_{u})\multimap
F(C_{v})$

An example of a transformation forest $\mathcal{F}$ and a computation of its
type $\mathrm{Ty}(\mathcal{F})$ is pictured in Figure 9.

Figure 9. A transformation forest $\mathcal{F}:T\with
S\to\displaystyle\bigwith_{i=0}^{4}C_{i}$
($S,T,U,V,C_{0},\ldots,C_{4}\in\mathsf{Obj}(\mathcal{C})$).

To guide the intuition, one may note that there is an embedding232323This
becomes an isomorphism when $\mathsf{Hom}_{\mathcal{D}}\left(\top,A\otimes
B\right)\cong\mathsf{Hom}_{\mathcal{D}}\left(\top,A\right)\times\mathsf{Hom}_{\mathcal{D}}\left(\top,B\right)$;
this is the case for our intended application
$\mathcal{D}=\mathcal{SR}_{\oplus}$. of a set of suitable labellings of the
forest $\mathcal{F}$ into
$\mathsf{Hom}_{\mathcal{D}}\left(\top,\mathrm{Ty}(\mathcal{F})\right)$.

$\textstyle{\prod_{(u,v)\in
E}\mathsf{Hom}_{\mathcal{D}}\left(F(C_{u}),F(C_{v})\right)\quad\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\quad\mathsf{Hom}_{\mathcal{D}}\left(\top,\mathrm{Ty}(\mathcal{F})\right)}$

We will now call abusively the input of $\mathcal{F}$ the object
$A=\bigwith_{i\in I}C_{i}$ and the output $B=\bigwith_{o\in O}C_{o}$; we write
$\mathcal{F}:A\to B$ in the sequel. The justification for this notation is
that there is a family of maps

${\llbracket\mathcal{F}\rrbracket}\;\in\;\prod_{o\in O}\sum_{i\in
I}\mathsf{Hom}_{\mathcal{D}}\left(\mathrm{Ty}(\mathcal{F}),F(C_{i})\multimap
F(C_{o})\right)$

obtained by internalizing the composition of morphisms along branches of
$\mathcal{F}$, which we call the _semantics of $\mathcal{F}$_.

We also note that this allow to interpret arbitrary $\mathcal{C}_{\with}$
morphisms: such a morphism $f:A\to B$ can be mapped to a pair
$(\mathrm{Grph}(f),\widehat{f})$ consisting of

  * •

a depth-1 transformation forest $\mathrm{Grph}(f):\bigwith_{i\in
I}C_{i}\to\bigwith_{o\in O}C_{o}$ (an example is depicted in Figure 10)

  * •

a morphism
$\widehat{f}\in\mathsf{Hom}_{\mathcal{D}}\left(\top,\mathrm{Ty}(\mathcal{F})\right)$

so that, if $f=(i_{o},\alpha_{o})_{o\in O}$, we have
${\llbracket\mathrm{Grph}(f)\rrbracket}_{o}\circ\widehat{f}=(i_{o},\Lambda(\alpha_{o}\circ\rho^{-1}))$.

Figure 10. A depth-$1$ transformation forest.

Given two forests $\mathcal{F}:A\to B$ and $\mathcal{F}^{\prime}:B\to C$,
there is a composition $\mathcal{F}^{\prime}\circ\mathcal{F}$ obtained by
gluing the input nodes of $\mathcal{F}^{\prime}$ along the output nodes of
$\mathcal{F}$. A crucial point is that the semantics of the composite
${\llbracket-\rrbracket}$ may be computed as follows

${\llbracket\mathcal{F}^{\prime}\circ\mathcal{F}\rrbracket}(o)\;=\;\left({\llbracket\mathcal{F}\rrbracket}_{1}({\llbracket\mathcal{F}^{\prime}\rrbracket}_{1}(o^{\prime})),{\llbracket\mathcal{F}^{\prime}\rrbracket}_{2}(o^{\prime})\circ{\llbracket\mathcal{F}\rrbracket}_{2}({\llbracket\mathcal{F}^{\prime}\rrbracket}_{1})\right)$

####  4.2.2. Reducing transformation forests

We now introduce two elementary transformations
$\mathcal{F}\mapsto\mathcal{F}^{\prime}$ over transformation forests, together
with associated morphisms
$\mathrm{Ty}(\mathcal{F})\to\mathrm{Ty}(\mathcal{F}^{\prime})$:

  * •

Pruning: if $v\in V_{\mathcal{F}}$ is a leaf which is not an output node in
the forest $\mathcal{F}:A\to B$, call $\mathrm{prune}(\mathcal{F},v):A\to B$
the forest obtained by removing $v$ and adjacent edges from $\mathcal{F}$.

This induces a canonical map

${prune}(v):\mathrm{Ty}(\mathcal{F})\to\mathrm{Ty}(\mathrm{prune}(\mathcal{F},v))$

by using the weakening maps on the components corresponding to the deleted
edges.

  * •

Contraction: If there is a vertex $v$ with a unique child $c$ and a (unique)
parent $p$ in the forest $\mathcal{F}:A\to B$, call
$\mathrm{contract}(\mathcal{F},v):A\to B$ the forest obtained by replacing the
edges $(p,v)$ and $(v,c)$ with a single edge $(p,c)$ and removing $v$.

There is a canonical map

${contract}(v):\mathrm{Ty}(\mathcal{F})\to\mathrm{Ty}(\mathrm{contract}(\mathcal{F},v))$

induced by the internal composition map

$\mathsf{Hom}_{\mathcal{D}}\left([F(C_{p})\multimap
F(C_{v})]\otimes[F(C_{v})\multimap F(C_{c})],F(C_{p})\multimap
F(C_{c})\right)$

The auxiliary maps ${prune}$ and ${contract}$ operations are compatible with
the semantic map ${\llbracket\cdot\rrbracket}$ in the sense that for every
$o\in O$ and suitable vertices $u,v$ of $\mathcal{F}$ , we have

$i=\pi_{1}({\llbracket\mathcal{F}\rrbracket}(o))=\pi_{1}({\llbracket\mathrm{prune}(\mathcal{F},u)\rrbracket}(o))=\pi_{1}({\llbracket\mathrm{contract}(\mathcal{F},v)\rrbracket}(o))$

and the following diagrams commute in $\mathcal{D}$

---
$\textstyle{\mathrm{Ty}(\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\llbracket\mathcal{F}\rrbracket}(o)}$$\scriptstyle{{prune}(v)}$$\textstyle{F(C_{i})\multimap
F(C_{o})}$$\textstyle{\mathrm{Ty}(\mathrm{prune}(\mathcal{F},v))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\qquad{\llbracket\mathrm{prune}(\mathcal{F},v)\rrbracket}(o)}$
---
$\textstyle{\mathrm{Ty}(\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\llbracket\mathcal{F}\rrbracket}(o)}$$\scriptstyle{{contract}(v)}$$\textstyle{F(C_{i})\multimap
F(C_{o})}$$\textstyle{\mathrm{Ty}(\mathrm{contract}(\mathcal{F},v))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\qquad{\llbracket\mathrm{contract}(\mathcal{F},v)\rrbracket}(o)}$

Consider the rewrite system $\leadsto$ over forests $\mathcal{F}:A\to B$
induced by those two operations, and call $\leadsto^{=}$ its reflexive closure
and $\leadsto^{*}$ the transitive closure of $\leadsto^{=}$. It can be shown
that the reflexive closure $\leadsto^{=}$ satisfies the _diamond lemma_ ,
i.e., that for every $\mathcal{F},\mathcal{F}^{\prime}$ and
$\mathcal{F}^{\prime\prime}$ such that
$\mathcal{F}\leadsto^{=}\mathcal{F}^{\prime}$ and
$\mathcal{F}\leadsto^{=}\mathcal{F}^{\prime\prime}$, there exists
$\mathcal{F}^{\prime\prime\prime}$ such that
$\mathcal{F}^{\prime}\leadsto^{=}\mathcal{F}^{\prime\prime\prime}$ and
$\mathcal{F}^{\prime\prime}\leadsto^{=}\mathcal{F}^{\prime\prime\prime}$. This
ensures that $\leadsto$ is confluent. Furthermore, given a rewrite
$\mathcal{F}\leadsto^{*}\mathcal{F}^{\prime}$, there is a map
$\mathrm{Ty}(\mathcal{F})\to\mathrm{Ty}(\mathcal{F}^{\prime})$ obtained by
composing maps ${prune}(v)$ and ${contract}(v)$ (and identities for trivial
rewrites $\mathcal{F}\leadsto^{*}\mathcal{F}$). It can be shown that this map
does _not_ depend on the rewrite path. This is done first by arguing that if
we have a rewrite square for $\leadsto^{=}$, the associated diagram in
$\mathcal{D}$ is commutative, and then proceed by induction over the rewrite
paths using the diamond lemma.

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
7.8039pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathcal{F}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
66.24939pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
0.0pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
66.24939pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\mathcal{F}^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
73.28328pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathcal{F}^{\prime\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
64.7094pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
64.7094pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\mathcal{F}^{\prime\prime\prime}}$}}}}}}}\ignorespaces}}}}\ignorespaces\qquad\qquad\begin{array}[]{c}\\\
\\\ \\\ \longmapsto\end{array}\qquad\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
17.80391pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
76.24939pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-29.49998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
76.24939pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathcal{F}^{\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
93.28331pt\raise-29.49998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathcal{F}^{\prime\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
74.70941pt\raise-40.88885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
74.70941pt\raise-40.88885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathcal{F}^{\prime\prime\prime})}$}}}}}}}\ignorespaces}}}}\ignorespaces$

Defining the size of a forest as its number of vertices, it is clear that
$\mathrm{prune}(\mathcal{F},u)$ and $\mathrm{contract}(\mathcal{F},v)$ have
size strictly less than $\mathcal{F}$, so the rewrite system is also
terminating. With confluence, it means that for every forest $\mathcal{F}:A\to
B$, there is a unique forest $\mathrm{reduce}(\mathcal{F}):A\to B$ such that
$\mathcal{F}\leadsto^{*}\mathrm{reduce}(\mathcal{F})$ and there is no
$\mathcal{F}^{\prime}$ such that
$\mathrm{reduce}(\mathcal{F})\leadsto\mathcal{F}^{\prime}$. We call
$\mathrm{reduce}(\mathcal{F})$ the _normal form_ of $\mathcal{F}$; a forest
$\mathcal{F}$ is called _normal_ if
$\mathrm{reduce}(\mathcal{F})=\mathcal{F}$. By the discussion above, there are
canonical maps
$reduce_{\mathcal{F}}:\mathrm{Ty}(\mathcal{F})\to\mathrm{Ty}(\mathrm{reduce}(\mathcal{F}))$
coming from rewrites.

Figure 11. An example of composing normal transformation forests, where first
the usual composition and then two big steps of reduction, corresponding
respectively to pruning and contracting, are carried out in succession.

The last important thing to note is that, if the input $A=\bigwith_{i\in
I}C_{i}$ and output $B=\bigwith_{o\in O}C_{o}$ are fixed, up to isomorphism,
there are finitely many normal forests $\mathcal{F}:A\to B$ as their size is
bounded by $2({|I|}+{|O|})$. We write $\mathrm{NF}\left({A},{B}\right)$ for a
finite set of representative for all normal forests $A\to B$, and given
$\mathcal{F}\in\mathrm{NF}\left({B},{C}\right)$ and
$\mathcal{F}^{\prime}\in\mathrm{NF}\left({A},{B}\right)$, we write
$\mathcal{F}\circ_{\mathcal{N}}\mathcal{F}^{\prime}$ for the unique forest in
$\mathrm{NF}\left({A},{C}\right)$ which is isomorphic to
$\mathrm{reduce}(\mathcal{F}\circ\mathcal{F}^{\prime})$; an example of the
full computation of a $\mathcal{F}\circ_{\mathcal{N}}\mathcal{F}^{\prime}$ is
given in Figure 11. Similarly, we assume that
$\mathrm{Grph}(f)\in\mathrm{NF}\left({A},{B}\right)$ for every morphism
$f\in\mathsf{Hom}_{\mathcal{C}_{\with}}\left(A,B\right)$.

####  4.2.3. Putting everything together

Let $\mathcal{T}=\left(Q,q_{0},\left(A_{q}\right)_{q\in Q},\delta,i,o\right)$
be a sdm-$\mathfrak{C}_{\with}$-SST with input $\Sigma^{*}$. We define the
sdm-$\mathfrak{D}$-SST

$\mathcal{T}^{\prime}\leavevmode\nobreak\ \leavevmode\nobreak\
=\leavevmode\nobreak\ \leavevmode\nobreak\ \left(\sum_{q\in
Q}\mathrm{NF}\left({A_{q_{0}}},{A_{q}}\right),(q_{0},\mathrm{Grph}(\mathrm{id})),(\mathrm{Ty}(\mathcal{F}))_{q,\mathcal{F}},\delta^{\prime},i^{\prime}o^{\prime}\right)$

where

$\begin{array}[]{c}\displaystyle\delta^{\prime}\leavevmode\nobreak\
\leavevmode\nobreak\ :\leavevmode\nobreak\ \leavevmode\nobreak\
\Sigma\to\prod_{q,\mathcal{F}}\sum_{r,\mathcal{F}^{\prime}}\mathsf{Hom}_{\mathcal{D}}\left(\mathrm{Ty}(\mathcal{F}),\mathrm{Ty}(\mathcal{F}^{\prime})\right)\\\
\\\ \displaystyle
i^{\prime}\in\mathsf{Hom}_{\mathcal{D}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}},\mathrm{Grph}(\mathrm{id})\right)\qquad\qquad
o^{\prime}\in\prod_{q,\mathcal{F}}\mathsf{Hom}_{\mathcal{D}}\left(\mathrm{Ty}(\mathcal{F}),\Bot\right)\end{array}$

are given as follows, assuming that $A_{q}=\displaystyle\bigwith_{x\in
X_{q}}C_{q,x}$

$\begin{array}[]{|c@{\qquad}|@{\qquad}c|}\hline\cr\delta^{\mathcal{D}}(a)_{q,\mathcal{F}}&o^{\prime}_{q,\mathcal{F}}\\\
\hline\cr&\\\ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
66.84872pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-16.26392pt\raise-35.0pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-55.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.28406pt\hbox{$\scriptstyle{\sim}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-64.5pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\top\otimes\mathrm{Ty}(\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-95.33943pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-3.31946pt\hbox{$\scriptstyle{\widehat{\delta^{\mathcal{C}_{\with}}(a)_{q}}\otimes\mathrm{id}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-103.8211pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathrm{Grph}(\delta^{\mathcal{C}_{\with}}(a)_{q}))\otimes\mathrm{Ty}(\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-136.35776pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.28406pt\hbox{$\scriptstyle{\sim}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-145.17886pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathrm{Grph}(\delta^{\mathcal{C}_{\with}}(a)_{q})\circ\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-177.71552pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{reduce}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-186.53662pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathrm{reduce}(\mathrm{Grph}(\delta^{\mathcal{C}_{\with}}(a)_{q})\circ\mathcal{F}))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\hbox{\kern
1.0pt\raise 0.0pt\hbox{\lx<EMAIL_ADDRESS>0.0pt\hbox{\lx@xy@droprule}}}}\ignorespaces{}{\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{\lx<EMAIL_ADDRESS>0.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{\lx<EMAIL_ADDRESS>0.0pt\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\delta^{\mathrm{NF}}(a)_{q,\mathcal{F}})}$}}}}}}}\ignorespaces}}}}\ignorespaces&\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
70.90828pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Ty}(\mathcal{F})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-20.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-29.5pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{F(C_{q_{0},x_{0}})}\multimap{F(C_{q,x})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-60.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.28406pt\hbox{$\scriptstyle{\sim}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-69.5pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{({F(C_{q_{0},x_{0}})}\multimap{F(C_{q,x})})\otimes\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-109.5pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{({F(C_{q_{0},x_{0}})}\multimap{F(C_{q,x})})\otimes
F(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-140.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.6789pt\hbox{$\scriptstyle{\mathrm{id}\otimes
F(i_{x_{0}})}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern
0.0pt\raise-149.5pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{({F(C_{q_{0},x_{0}})}\multimap{F(C_{q,x})})\otimes
F(C_{q_{0},x_{0}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-180.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\mathrm{ev}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-189.5pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{F(C_{q,x})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
0.0pt\raise-220.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{F(o^{\mathcal{C}})}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-229.5pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{F(\Bot)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-268.58334pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\Bot}$}}}}}}}\ignorespaces}}}}\ignorespaces\\\
\hline\cr\end{array}$ Figure 12. Definition of
$\delta^{\mathcal{D}}(a)_{q,\mathcal{F}}$ and $o^{\prime}_{q,\mathcal{F}}$.

  * •

Notice that $\mathrm{Ty}(\mathrm{Grph}(\mathrm{id}))=\bigotimes_{x\in
X_{q_{0}}}F(C_{q_{0},x})\multimap F(C_{q_{0},x})$; we simply take the constant
map corresponding to the $X_{q_{0}}$-fold tensor of
$\Lambda(\mathrm{id}_{C_{q_{0},x}})$ for $i^{\prime}$.

  * •

Fix $a\in\Sigma$ and recall that $\delta(a)$ is a family of pairs

$(\delta^{Q}(a)_{q},\delta^{\mathcal{C}_{\with}}(a)_{q})_{q\in
Q}\leavevmode\nobreak\ \leavevmode\nobreak\ \in\leavevmode\nobreak\
\leavevmode\nobreak\ \prod_{q\in Q}\sum_{r\in
Q}\mathsf{Hom}_{\mathcal{C}_{\with}}\left(A_{q},A_{r}\right)$

$\delta^{\prime}$ is then defined by the equation

$\delta^{\prime}(a)_{q,\mathcal{F}}\leavevmode\nobreak\ \leavevmode\nobreak\
=\leavevmode\nobreak\ \leavevmode\nobreak\
\left(\left(\delta^{Q}(a)_{q},\delta^{\mathrm{NF}}(a)_{q,\mathcal{F}}\right),\delta^{\mathcal{D}}(a)_{q,\mathcal{F}}\right)$

where we set
$\delta^{\mathrm{NF}}(a)_{q,\mathcal{F}}=\mathrm{Grph}(\delta^{\mathcal{C}_{\with}}(a)_{q})\circ_{\mathcal{N}}\mathcal{F}$
and $\delta^{\mathcal{D}}(a)_{q,\mathcal{F}}$ is obtained as in Figure 12

  * •

Finally, for $q,\mathcal{F}$ ranging over states of $\mathcal{T}^{\prime}$, we
define $o^{\prime}_{q,\mathcal{F}}$. Recall that $\mathcal{F}$ determines a
canonical family

${\llbracket\mathcal{F}\rrbracket}\in\prod_{x\in X_{q}}\sum_{x_{0}\in
X_{q_{0}}}\mathsf{Hom}_{\mathcal{D}}\left(\mathrm{Ty}(\mathcal{F}),F(C_{q_{0},x_{0}})\multimap
F(C_{q,x})\right)$

First, as $\Bot^{\mathfrak{C}_{\with}}=\iota_{\with}(\Bot^{\mathfrak{C}})$,
note that there is a unique $x\in X_{q}$ such that
$o_{q}=(x,o^{\mathcal{C}})_{*}$ for some
$o^{\mathcal{C}}\in\mathsf{Hom}_{\mathcal{C}}\left(C_{q,x},\Bot^{\mathfrak{C}}\right)$.
Writing the pair ${\llbracket\mathcal{F}\rrbracket}_{x}$ as $(x_{0},f)$,
$o^{\prime}_{q,\mathcal{F}}$ is depicted in Figure 12.

We omit the proof that
${\llbracket\mathcal{T}\rrbracket}={\llbracket\mathcal{T}^{\prime}\rrbracket}$
by induction over the length of an input word. While spelling it out may be a
bit notation-heavy, there is no particular difficulty considering the remarks
above linking ${\llbracket-\rrbracket}$, the composition of transformation
forests and their normal forms.

##  5\. Regular tree functions in the $\lambda\ell^{\oplus\with}$-calculus

The goal of this section is now to prove our main theorem for tree functions
(that we recall below), extending the case of strings (Theorem 1).

See 2

To prove this theorem, we follow a similar approach as in Section 3.

######  Remark 52.

While the result on strings follows as a corollary of Theorem 2, this relies
on the equivalence between regular string functions and regular tree functions
when strings are regarded as particular trees. Given that we start from
transducer-based characterization of these notions, this means that we would
use e.g. [AD17, Theorem 3.16-3.17], which are themselves non-trivial
results242424A self-contained proof is also possible by building on our
development by exploiting Theorem 42, arguably the most intricate argument
presented here..

We thus first define a generalized notion of bottom-up ranked tree transducers
(BRTT) parameterized by a notion of _tree streaming setting_.

Let $X$ be a set. A _tree streaming setting_ with output $X$ is a tuple
$\mathfrak{C}=(\mathcal{C},\otimes,\mathbf{I},\Bot,{\llparenthesis-\rrparenthesis})$
where

  * •

$(\mathcal{C},\otimes,\mathbf{I})$ is a _symmetric monoidal_ category

  * •

$\Bot$ is an object of $\mathcal{C}$

  * •

${\llparenthesis-\rrparenthesis}$ is a set-theoretic map
$\mathsf{Hom}_{\mathcal{C}}\left(\mathbf{I},\Bot\right)\to X$

This notion essentially differs by asking that the underlying category be
equipped with a symmetric monoidal product, which is used in defining the
semantics of $\mathfrak{C}$-BRTTs. The tensor product is used to fit the
branching structure of trees and $\mathbf{I}$ is used for terminal nodes (so
there is no need of a distinguished initial object  $\Bot$ as in string
streaming settings).

Let
$\mathfrak{C}=(\mathcal{C},\otimes,\mathbf{I},\Bot,{\llparenthesis-\rrparenthesis})$
be a tree streaming setting with output $X$. A $\mathfrak{C}$-BRTT with input
(ranked) alphabet $\bf\Sigma$ and output $X$ is a tuple $(Q,R,\delta,o)$ where

  * •

$Q$ is a finite set of states

  * •

$R$ is an object of $\mathcal{C}$

  * •

$\delta$ is a function
$\displaystyle\prod_{a\in\Sigma}\left(Q^{\mathrm{ar}(a)}\to
Q\times\mathsf{Hom}_{\mathcal{C}}\left(\bigotimes_{\mathrm{ar}(a)}R\text{{\Huge{,}}}\;R\right)\right)$

  * •

$o\in\mathsf{Hom}_{\mathcal{C}}\left(R,\Bot\right)$ is an output morphism

Its semantics is a set-theoretic map $\mathbf{Tree}({\bf\Sigma})\to X$ defined
as follows: writing $\delta_{Q}(a,(t_{i})_{i\in\mathrm{ar}(a)})$ for
$\pi_{1}(\delta(a,(t_{i})_{i\in\mathrm{ar}(a)}))$ and
$\delta_{\mathcal{C}}(a,(t_{i})_{i\in\mathrm{ar}(a)})$ for
$\pi_{2}(\delta(a,(t_{i})_{i\in\mathrm{ar}(a)}))$, define auxiliary functions
$\delta^{*}_{Q}:\mathbf{Tree}({\bf\Sigma})\to Q$ and
$\delta^{*}_{\mathcal{C}}:\mathbf{Tree}({\bf\Sigma})\to\mathsf{Hom}_{\mathcal{C}}\left(\mathbf{I},R\right)$
by iterating $\delta$:

$\begin{array}[]{lcl}\delta_{Q}^{*}\left(a\left((t_{i})_{i\in\mathrm{ar}(a)}\right)\right)&\leavevmode\nobreak\
\leavevmode\nobreak\
=\nobreak\leavevmode\nobreak\leavevmode&\delta_{Q}\left(a,(\delta^{*}_{Q}(t_{i}))_{i\in\mathrm{ar}(a)}\right)\\\
\delta_{\mathcal{C}}^{*}\left(a\left((t_{i})_{i\in\mathrm{ar}(a)}\right)\right)&\leavevmode\nobreak\
\leavevmode\nobreak\
=\nobreak\leavevmode\nobreak\leavevmode&\displaystyle\delta_{\mathcal{C}}\left(a,(\delta^{*}_{Q}(t_{i}))_{i\in\mathrm{ar}(a)}\right)\circ\left(\bigotimes_{i\in\mathrm{ar}(a)}\delta^{*}_{\mathcal{C}}(t_{i})\right)\circ\varphi_{\mathrm{ar}(a)}\end{array}$

where $\varphi_{\mathrm{ar}(a)}$ is the unique isomorphism
$\mathbf{I}\xrightarrow{\,\sim\,}\bigotimes_{i\in\mathrm{ar}(a)}\mathbf{I}$
generated by the associator and unitors of $(\mathcal{C},\otimes,\mathbf{I})$.
The output function
${\llbracket\mathcal{T}\rrbracket}:\mathbf{Tree}({\bf\Sigma})\to X$ is defined
as ${\llbracket\mathcal{T}\rrbracket}={\llparenthesis
o\circ\delta^{*}_{\mathcal{C}}\rrparenthesis}$.

######  Remark 53.

Strictly speaking, we do not need the monoidal product to be symmetric for the
notion to make sense, but it would require using a fixed order over the input
ranked alphabet $\bf\Sigma$. Although one could choose an arbitrary total
order over $\bf\Sigma$, different orders might define different classes of
functions $\mathbf{Tree}({\bf\Sigma})$ when the monoidal product is not
symmetric. This is why we work in symmetric monoidal categories.

As with string streaming settings, it is convenient to define a notion of
morphism of tree streaming settings to compare the expressiveness of classes
of BRTTs.

Let
$\mathfrak{C}=(\mathcal{C},\mathbf{I}_{\mathcal{C}},\otimes_{\mathcal{C}},\Bot_{\mathcal{C}},{\llparenthesis-\rrparenthesis}_{\mathfrak{C}})$
and
$\mathfrak{D}=(\mathcal{D},\mathbf{I}_{\mathcal{D}},\otimes_{\mathcal{C}},\Bot_{\mathcal{D}},{\llparenthesis-\rrparenthesis}_{\mathfrak{D}})$
be tree streaming settings with output $X$. A morphism of tree streaming
settings is given by a lax monoidal functor
$F:(\mathcal{C},\otimes_{\mathcal{C}},\mathbf{I}_{\mathcal{C}})\to(\mathcal{D},\otimes_{\mathcal{D}},\mathbf{I}_{\mathcal{D}})$
and a $\mathcal{D}$-arrow $o:F(\Bot_{\mathcal{C}})\to\Bot_{\mathcal{D}}$ such
that, for every
$f\in\mathsf{Hom}_{\mathcal{C}}\left(\text{{\raisebox{0.0pt}{\scalebox{1.0}[-1.0]{$\Bot$}}}}_{\mathcal{C}},\Bot_{\mathcal{C}}\right)$,
we have

${\llparenthesis o\circ F(f)\circ
i\rrparenthesis}_{\mathcal{D}}={\llparenthesis f\rrparenthesis}_{\mathcal{C}}$

where $i:\mathbf{I}_{\mathcal{D}}\to F(\mathbf{I}_{\mathcal{C}})$ is obtained
as part of the lax monoidal functor structure over $F$.

Observe that we do not require those functors to commute with the symmetry
morphisms for the monoidal products, as promised in Section 2.4. This is
consistent with the fact that the symmetries are not really involved in
computing the image of a tree by a $\mathfrak{C}$-BRTT, according to Remark
53: it is only their mere existence that matters.

######  Lemma 54.

If there is a morphism of tree streaming settings
$\mathfrak{C}\to\mathfrak{D}$, then $\mathfrak{D}$-BRTTs subsume
$\mathfrak{C}$-BRTTs.

######  Proof 5.1.

Let us give the proof for single-state BRTTs; the proof for general BRTTs
would be notationally heavier but not much more insightful. Suppose that we
have some single-state $\mathfrak{C}$-BRTT $\mathcal{T}=(R,\delta,o)$ – where
we leave the only state implicit and regard the transition function $\delta$
and output function $o$ as elements of
$\prod_{a\in\Sigma}\mathsf{Hom}_{\mathcal{C}}\left(\bigotimes_{\mathrm{ar}(a)}R\text{{\Huge{,}}}\;R\right)$
and $\mathsf{Hom}_{\mathcal{C}}\left(R,\Bot\right)$ respectively – and that
the morphism under consideration is composed of a lax monoidal functor
$F:\mathcal{C}\to\mathcal{D}$ and a $\mathcal{D}$-arrow
$o^{\prime}:F(\Bot_{\mathcal{C}})\to\Bot_{\mathcal{D}}$.

Since $F$ is lax monoidal, we have a family of natural transformations

$m_{I,A}\leavevmode\nobreak\ :\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
\bigotimes_{I}F(A)\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
F\left(\bigotimes_{I}A\right)$

where $I$ ranges over all finite sets252525Recall from Section 2.1 that an
operation $\bigotimes_{i\in I}(-)$ – here, a functor – is associated to every
finite indexing set $I$ by choosing an arbitrary total order over $I$. and $A$
over objects of $\mathcal{C}$; this family is compatible with the associators
and unitors in $\mathcal{C}$ and $\mathcal{D}$. Furthermore,
$m_{\varnothing,A}:\mathbf{I}\to F(\mathbf{I})$ is the same for all
$A\in\mathsf{Obj}(C)$, so we shall abbreviate it as $m_{\varnothing}$.

We claim that
${\llbracket\mathcal{T}\rrbracket}={\llbracket\mathcal{T}^{\prime}\rrbracket}$,
where $\mathcal{T}^{\prime}$ is the single-state $\mathfrak{D}$-BRTT
$(F(R),\delta^{\prime},o^{\prime}\circ F(o))$ with the same typing conventions
and $\delta^{\prime}_{a}=F(\delta_{a})\circ m_{\mathrm{ar}(a),R}$. Let us
prove this. To do so we first consider the iterations of the transition
functions

$\delta^{*}:\mathbf{Tree}({\bf\Sigma})\to\mathsf{Hom}_{\mathcal{C}}\left(\mathbf{I},R\right)\qquad\text{and}\qquad\delta^{\prime*}:\mathbf{Tree}({\bf\Sigma})\to\mathsf{Hom}_{\mathcal{D}}\left(\mathbf{I},F(R)\right)$

and show that $\delta^{\prime*}(t)=F(\delta(t))\circ m_{\varnothing}$ by
induction over $t\in\mathbf{Tree}({\bf\Sigma})$. So suppose that
$t=a((u_{x})_{x\in\mathrm{ar}(a)})$ and that the inductive hypothesis holds
(this also takes care of the base case: when $\mathrm{ar}(a)=\varnothing$, the
inductive hypothesis is vacuous). In such a case, let us show that each face
in the following diagram commutes (where all tensor products have arity
$\mathrm{ar}(a)$):

|
---|---
$\textstyle{\mathbf{I}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathtt{(b)}}$$\scriptstyle{m_{\varnothing}}$$\scriptstyle{\sim}$$\scriptstyle{\delta^{\prime*}(t)}$$\scriptstyle{\mathtt{(a)}}$$\textstyle{\bigotimes\mathbf{I}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\bigotimes
m_{\varnothing}}$$\scriptstyle{\bigotimes\limits_{x}\delta^{\prime*}(u_{x})}$$\textstyle{\bigotimes
F(\mathbf{I})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathtt{(c)}}$$\scriptstyle{\bigotimes\limits_{x}F(\delta^{*}(u_{x}))}$$\scriptstyle{m_{\mathrm{ar}(a),\mathbf{I}}}$$\textstyle{\bigotimes
F(R)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta^{\prime}_{a}}$$\scriptstyle{m_{\mathrm{ar}(a),R}}$$\scriptstyle{\mathtt{(e)}}$$\textstyle{F(R)}$$\textstyle{F\left(\bigotimes\mathbf{I}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathtt{(d)}}$$\scriptstyle{F\left(\bigotimes\limits_{x}\delta^{*}(u_{x})\right)}$$\textstyle{F\left(\bigotimes
R\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F(\delta_{a})}$$\textstyle{F(\mathbf{I})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathtt{(f)}}$$\scriptstyle{F(\sim)}$$\scriptstyle{F(\delta^{*}(t))}$

Faces (a) and (f) commute by definition of iterated transition functions and
face (e) corresponds to the definition of $\delta^{\prime}$. Face (d) commutes
because of the naturality of $m_{-,-}$ and face (b) because of its
compatibility with associators. Finally, face (c) corresponds to the inductive
hypothesis. Therefore, the topmost and bottommost paths coincide, so we have
$\delta^{\prime*}(t)=F(\delta(t))\circ m_{\varnothing}$, which concludes our
inductive argument. We can then conclude since we have, for every tree $t$,

$\begin{array}[]{lcll}{\llbracket\mathcal{T}^{\prime}\rrbracket}(t)&=&{\llparenthesis
o^{\prime}\circ
F(o)\circ(\delta^{\prime*}(t))\rrparenthesis}_{\mathfrak{D}}&\text{by
definition}\\\ &=&{\llparenthesis o^{\prime}\circ F(o)\circ
F(\delta^{*}(t))\circ
m_{\varnothing}\rrparenthesis}_{\mathfrak{D}}&\text{inductive argument}\\\
&=&{\llparenthesis o^{\prime}\circ F(o\circ\delta^{*}(t))\circ
m_{\varnothing}\rrparenthesis}_{\mathfrak{D}}&\text{by functoriality}\\\
&=&{\llparenthesis
o\circ(\delta^{*}(t))\rrparenthesis}_{\mathfrak{C}}&\text{since
$(F,o^{\prime})$ is part of a morphism $\mathfrak{C}\to\mathfrak{D}$}\\\
&=&{\llbracket\mathcal{T}\rrbracket}(t)&\text{by definition}\\\ \end{array}$

From now on, we may omit the “tree” in when discussing streaming settings.

As for SSTs, linearity is an important concept for traditional BRTTs over
ranked alphabets. Rather than starting from the category corresponding exactly
to usual BRTTs, we will first study a more convenient, albeit less expressive,
streaming setting based on the idea of trees with multiple holes. For this, it
will be convenient to introduce the notion of _multicategory_ , which is
essentially a notion of category where morphisms are allowed to have multiple
input objects. We will thus first devote Section 5.1 to some preliminaries
describing how to (freely) generate affine monoidal categories from
multicategories.

After spelling out the universal properties that will allow us to easily
define functors and a quick review of the generalization of the results of
Section 3.4 pertaining to coproduct completions in Section 5.2, we present a
basic multicategory of registers $\mathcal{TR}^{\mathrm{m}}$ containing “trees
with holes” in Section 5.3, and the corresponding streaming setting
$\mathfrak{TR}$ on top of a category $\mathcal{TR}$. The usual restriction to
registers containing “trees with at most one hole” is also discussed and shown
to be no less expressive thanks to our basic results on the coproduct
completion. Then, we explain how the usual notion of BRTT presented in [AD17]
can be shown to have the same expressiveness as $\mathfrak{TR}_{\with}$-BRTTs
in Section 5.4.

Finally, in Section 5.5, we show that $\mathcal{TR}_{\oplus}$ has internal
homsets $\iota_{\oplus}(R)\multimap\iota_{\oplus}(S)$ and conclude that
$\mathcal{TR}_{\oplus\with}$ is monoidal-closed. We conclude the proof of
Theorem 2 in Section 5.7.

For the rest of this part, we fix a ranked alphabet $\bf\Gamma$ so that we may
focus on outputs contained in $\mathbf{Tree}({\bf\Gamma})$, much like we
focussed on outputs in some fixed $\Gamma^{*}$ before.

###  5.1. Multicategorical preliminaries

This section is devoted to spelling out the formal definition of the notion of
multicategory that we use in the sequel, and their relation to symmetric
affine monoidal category. While technically necessary for the sequel, it is
rather dry and should maybe only be skimmed over at first reading.

A (weak symmetric) multicategory $\mathcal{M}$ consists of

  * •

a class of objects $\mathsf{Obj}(\mathcal{M})$

  * •

a class of _multimorphisms_ going from pairs $(I,(A_{i})_{i\in I})$ of a
finite index set $I$ and a family $(A_{i})_{i\in I}$ of objects to objects
$B$. We omit the first component of the source and write
$\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in I},B\right)$ for the set of
these multimorphisms.

  * •

for every object $A$, a distinguished identity multimorphism
$\mathrm{id}_{A}\in\mathsf{Hom}_{\mathcal{M}}\left((A)_{*\in 1},A\right)$.

  * •

for every set-theoretic map $f:I\to J$, families $(A_{i})_{i\in I}$,
$(B_{j})_{j\in J}$ and object $C$, a composition operation

$\begin{array}[]{ccccl}\mathsf{Hom}_{\mathcal{M}}\left((B_{j})_{j\in
J},C\right)&\times&\left[\prod_{j\in
J}\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in
f^{-1}(j)},B_{j}\right)\right]&\longrightarrow&\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in
I},C\right)\\\ \alpha&,&(\beta_{j})_{j\in
J}&\longmapsto&\alpha*_{f}\beta\end{array}$

  * •

for every bijection $\sigma:I^{\prime}\to I$ between finite sets, a family of
actions

$\sigma^{*}:\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in
I},B\right)\to\mathsf{Hom}_{\mathcal{M}}\left((A_{\sigma(i^{\prime})})_{i^{\prime}\in
I^{\prime}},B\right)$

correspond to reindexing along symmetries.

Furthermore, the above data is required to obey the following laws.

  * •

The identity morphism be a neutral for composition: for any
$\alpha\in\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in I},B\right)$,

$\mathrm{id}_{B}*_{!}(\alpha)_{*\in
1}\quad=\quad\alpha\quad=\quad\alpha*_{\mathrm{id}_{I}}(\mathrm{id}_{A_{i}})_{i\in
I}$

  * •

Composition is associative: for any finite sets $I,J$ and $K$, functions
$f:K\to J$ and $g:J\to I$, families of objects $(A_{k})_{k\in K}$,
$(B_{j})_{j\in J}$, $(C_{i})_{i\in I}$, $D$ and families of morphisms

$\begin{array}[]{l}\alpha\in\prod_{j\in
J}\mathsf{Hom}_{\mathcal{M}}\left((A_{k})_{k\in f^{-1}(j)},B_{j}\right)\\\
\beta\in\prod_{i\in I}\mathsf{Hom}_{\mathcal{M}}\left((B_{j})_{j\in
g^{-1}(i)},C_{i}\right)\\\
\gamma\in\mathsf{Hom}_{\mathcal{M}}\left((C_{i})_{i\in I},D\right)\end{array}$

the following equation holds

$\gamma*_{g}\left(\beta*_{f}\alpha\right)=\left(\gamma*_{g\upharpoonright
f^{-1}(j)}\beta\right)_{j}*_{f}\alpha$

  * •

Permutations act functorially: for any $(A_{i})_{i\in I}$, $B$ and bijections
$\sigma:I^{\prime}\to I$ and $\sigma^{\prime}:I^{\prime\prime}\to I^{\prime}$,
the following commute

$\textstyle{\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in
I},B\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Hom}_{\mathcal{M}}\left((A_{\sigma(i^{\prime})})_{i^{\prime}\in
I^{\prime}},B\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Hom}_{\mathcal{M}}\left((A_{\sigma(\sigma^{\prime}(i^{\prime\prime}))})_{i^{\prime\prime}\in
I^{\prime\prime}},B\right)}$

and $\mathrm{id}_{I}^{*}:\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in
I},B\right)\to\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in I},B\right)$ is
the identity.

  * •

Composition is compatible with permutations: for every commuting square

$\textstyle{J^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{I^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma}$$\textstyle{J\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{I}$

in ${\sf FinSet}$ such that the vertical arrows be bijections, note in
particular that for every $i\in I$, there is a bijection
$\sigma_{i}:g^{-1}(I^{\prime})\to f^{-1}(I)$; we thus require that

$\alpha*_{f}\left(\beta_{j\in f^{-1}(i)}\right)_{i\in
I}\quad=\quad\sigma^{*}(\alpha)*_{g}\left(\sigma_{i}^{*}\left(\beta_{j\in
f^{-1}(i)}\right)\right)_{i\in I}$

for every suitable $\alpha$ and $\beta_{j}$s.

Every symmetric monoidal category $\mathcal{C}$ can be mapped to a
multicategory $\mathcal{C}_{\mathrm{mcat}}$ by taking

$\mathsf{Hom}_{\mathcal{C}_{\mathrm{mcat}}}\left((A_{i})_{i\in
I},B\right)\quad=\quad\mathsf{Hom}_{\mathcal{C}}\left(\bigotimes_{i\in
I}A_{i}\text{{\Huge{,}}}\;B\right)$

We may make this map functorial, provided we equip the class of
multicategories and the class of symmetric monoidal categories with
categorical structures.

Given two weak multicategories $\mathcal{M}$ and $\mathcal{N}$, a functor
$F:\mathcal{M}\to\mathcal{N}$ consists of maps of objects
$F:\mathsf{Obj}(\mathcal{M})\to\mathsf{Obj}(\mathcal{N})$ and of
multimorphisms

$F\leavevmode\nobreak\ :\leavevmode\nobreak\
\mathsf{Hom}_{\mathcal{M}}\left((A_{i})_{i\in I},B\right)\leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\
\mathsf{Hom}_{\mathcal{N}}\left((F(A_{i}))_{i\in I},F(B)\right)$

such that $F(\mathrm{id}_{A})=\mathrm{id}_{F(A)}$,
$F\left(\alpha*_{f}\left(\beta_{j}\right)_{j\in
f^{-1}(i)}\right)=F(\alpha)*_{f}(F(\beta_{j}))_{j\in f^{-1}(i)}$ and
$F(\sigma*(\alpha))=\sigma^{*}(F(\alpha))$ for all suitable objects, index
sets, set-theoretic functions and morphisms.

Definition 5.1 gives a class of arrows for a large category $\sf MCat$ of
multicategories. Calling $\sf Aff$ the category whose objects are symmetric
affine monoidal categories and morphisms are strong monoidal functors, the map
$\mathcal{C}\to\mathcal{C}_{\mathrm{mcat}}$ extends to a functor $\sf
Aff\to\sf MCat$. We are now interested in the inverse process of generating
freely a symmetric affine monoidal category out of a weak multicategory.

Let $\mathcal{M}$ be a weak multicategory. The _free affine symmetric monoidal
category_ generated by $\mathcal{M}$ is the category
$\mathcal{M}_{\mathrm{aff}}$ such that

  * •

objects are pairs $(I,(A_{i})_{i\in I})$ of a finite set $I$ and a family of
objects of $\mathcal{M}$; write $\bigotimes_{i\in I}A_{i}$ for such objects.

  * •

morphisms $\bigotimes_{i\in I}A_{i}\to\bigotimes_{j\in J}B_{j}$ are pairs
$(f,(\alpha_{j})_{j\in J})$ where $f$ is a partial function $I\rightharpoonup
J$ and $\alpha_{j}$ is a $\mathcal{M}$ multimorphism $(A_{i})_{i\in
f^{-1}(J)}\to B_{j}$.

  * •

identities $\bigotimes_{i\in I}A_{i}\to\bigotimes_{i\in I}A_{i}$ are the pairs
$(\mathrm{id}_{I},(\mathrm{id}_{A_{i}})_{i\in I})$.

  * •

the composition of

$(f,(\alpha_{j})_{j\in J}):\bigotimes_{i\in I}A_{i}\to\bigotimes_{j\in
J}B_{j}\leavevmode\nobreak\ \leavevmode\nobreak\
\text{and}\leavevmode\nobreak\ \leavevmode\nobreak\ (g,(\beta_{k})_{k\in
K}):\bigotimes_{j\in J}B_{j}\to\bigotimes_{k\in K}C_{k}$

is $\left(g\circ f,\left(\beta_{k}*\left(\alpha_{j}\right)_{j\in
g^{-1}(k)}\right)_{k\in K}\right)$.

For any bijection $\sigma:I^{\prime}\to I$, we have canonical isomorphisms
$\bigotimes_{i\in I}A_{i}\to\bigotimes_{i\in I}A_{\sigma(i)}$. We take the
binary tensor product to be

$\left(\bigotimes_{i\in I}A_{i}\right)\otimes\left(\bigotimes_{j\in
J}B_{j}\right)\leavevmode\nobreak\ \leavevmode\nobreak\ =\leavevmode\nobreak\
\leavevmode\nobreak\ \bigotimes_{x\in
I+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 the unit to be the terminal object, which is the nullary family
$\bigotimes_{\varnothing}$. The associator and symmetries are induced by the
isomorphisms $(I+J)+K\cong I+(J+K)$ and $I+J\cong J+I$ respectively, and the
units by $I+\varnothing\cong I\cong\varnothing+I$. The axioms of weak
symmetric multicategories then imply that this indeed endows
$\mathcal{M}_{\mathrm{aff}}$ with a symmetric affine monoidal structure. We
skip checking the details.

###  5.2. The coproduct completion

Similarly as for strings, the coproduct completion of a category induces a map
$\mathfrak{C}\mapsto\mathfrak{C}_{\oplus}$ over tree streaming settings.
Furthermore, expressiveness of $\mathfrak{C}$ and $\mathfrak{C}_{\oplus}$
remain the same under similar hypotheses as Theorem 31.

######  Theorem 55.

Let $\mathfrak{C}$ be a tree streaming setting whose monoidal product is
affine and such that all objects of the underlying category have unitary
support. Then, $\mathfrak{C}$-BRTTs and $\mathfrak{C}_{\oplus}$-BRTTs are
equi-expressive.

The proof is an unsurprising adaptation of the one of Theorem 31. We leave it
to the interested reader. Similarly, we define the notion of a state-dependent
memory $\mathfrak{C}$-streaming tree transducer (sdm-$\mathfrak{C}$-BRTT),
which can be shown to be as expressive as sdm-$\mathfrak{C}_{\oplus}$-BRTT. We
only state the definition and the generalization of Lemma 33, whose proof we
defer to the interested reader.

A $\mathfrak{C}$-_state-dependent memory BRTT_ with input
$\mathbf{Tree}({\bf\Sigma})$ is a tuple $(Q,\delta,(C_{q})_{q\in Q},o)$ where

  * •

$Q$ is a finite set of states

  * •

$(C_{q})_{q\in Q}$ is a $Q$-indexed family of objects of $\mathcal{C}$

  * •

$\displaystyle\delta\in\left[\prod_{a\in\Sigma}\prod_{q\in
Q^{\mathrm{ar}(a)}}\sum_{r\in
Q}\mathsf{Hom}_{\mathcal{C}}\left(\bigotimes_{x\in\mathrm{ar}(a)}C_{q(x)},C_{r}\right)\right]$
is a transition function

  * •

$\displaystyle o\in\prod_{q\in
Q}\mathsf{Hom}_{\mathcal{C}}\left(C_{q},\Bot\right)$ is the output family of
morphisms

######  Lemma 56.

Let $\mathfrak{C}$ be a streaming setting. State-dependent memory
$\mathfrak{C}$-BRTTs are as expressive as $\mathfrak{C}_{\oplus}$-BRTTs.

###  5.3. The combinatorial multicategory $\mathcal{TR}^{\mathrm{m}}$

We are now ready to give a smooth definition of a category of register