# Composing Copyless Streaming String Transducers

Rajeev Alur  University of Pennsylvania  Taylor Dohmen  University of Colorado
Boulder  Ashutosh Trivedi  University of Colorado Boulder

###### Abstract

Streaming string transducers (SSTs) implement string-to-string transformations
by reading their input in a single left-to-right pass while maintaining
fragments of potential outputs in a finite set of string variables. These
variables get updated on transitions of the transducer where they can be
reassigned to concatenations of variables and symbols. An SST is called
_copyless_ if every update is such that no variable gets copied to more than
once. Copyless SSTs capture Courcelle’s monadic second-order definable graph
transformations (MSOT) when restricted to string-to-string rewritings. The
extension of copyless SSTs with nondeterminism is also known to be equivalent
to the nondeterministic variant of MSOTs.

MSOTs, both deterministic and nondeterministic, are closed under composition.
Given the equivalence of MSOT and copyless SSTs, it is easy to see that
copyless SSTs are also closed under composition. The original proofs of this
fact, however, were based on a direct construction to produce a composite
copyless SST from two given copyless SSTs. A counterexample discovered by
Joost Englefriet showed that this construction may produce copyful
transducers. We revisit the original composition constructions for both
deterministic and nondeterministic SSTs and show that, although they can
introduce copyful updates, the resulting copyful behavior they exhibit is
superficial and is characterized by a property we call “diamond-free”: two
copies of the variables are never merged. To recover a modified version of the
original construction, we provide a method for producing an equivalent
copyless NSST from any diamond-free copyful NSST.

##  1 Introduction

Deterministic streaming string transducers (DSSTs) of Alur and Cerný [1, 2]
are single-pass machines that serve as a computational model characterizing
certain functions over finite strings. Nondeterministic SSTs (NSSTs) of Alur
and Deshmukh [3] generalize this formalism and are interpreted as defining
relations rather than functions. Upon reading a symbol, an SST changes state
and updates a finite set of string variables, which are initially set to the
empty string $\varepsilon$, using concatenation expressions, such as
$x=ax_{1}bx_{2}c$, comprised of variables and symbols from a designated output
alphabet. The final output of the transducer is determined by a similar
combination of variables and symbols, depending on the final state reached
after reading the entire input string. As demonstrated by Alur and Cerný [1],
Alur and Deshmukh [3], the families of transductions definable by copyless
SSTs coincide with those definable by the monadic second-order logic (MSO)
string transducers of Courcelle and Engelfriet [6]. Due to this
correspondence, transductions definable by copyless DSSTs and NSSTs are called
_regular functions_ and _regular relations_.

$q_{0}$start$a\mid x=xax$$xa$ Figure 1: A copyful SST.

A key condition on SSTs that enables their equivalence with MSO transducers is
the copylessness of the variable updates. This condition requires each
variable to be used at most once across all variable updates occurring on a
single transition. For instance, the copyless restriction prohibits the
assignment of the form
$(x,y)=(a{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}y}b{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}y}c,x)$,
where two copies of $y$ are flowing into $x$, or the assignment
$(x,y)=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}y},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}y})$,
where variable $y$ is copied into variables $x$ and $y$ both. This ensures
that the length of any output string grows linearly in the length of the
corresponding input string. For instance, a copyful SST, such as the one
depicted in fig. 1, can implement the mapping $a^{k}\mapsto a^{2^{k}}$, which
is not definable via an MSO transducer.

The regular functions and regular relations have a number of desirable
properties concerning closure and decidability. In particular, as proven in
the realm of MSO transducers [6], the regular functions and regular relations
are closed under function composition and relation composition, respectively.
Effective procedures are given in [1, 3] to construct a copyless SST that
realizes the composition of two copyless SSTs given as input. Joost Englefriet
observed [4] that these constructions may result in transducers with copyful
assignments. Consider, for instance, the three SSTs shown in fig. 2 where
$T_{3}$ is the composition of $T_{1}$ and $T_{2}$, constructed according to
the methods provided by Alur and Cerný [1], Alur and Deshmukh [3]. The
transducer $T_{1}$ implements the mapping $a^{n}\mapsto\left(ab\right)^{n}$,
while $T_{2}$ captures the mapping $a^{n_{1}}b^{m_{1}}\cdots
a^{n_{k}}b^{m_{k}}\mapsto a^{n_{1}}b\cdots a^{n_{k}}b$ for inputs ending in
the symbol $b$. Notice that both input transducers are copyless and
deterministic, yet there is a transition in $T_{3}$ with a copyful assignment.
On the other hand, one may notice that none of these copies are ever combined
via concatenation. In the assignment $\gamma^{2}$, for instance, there are two
variables, $z_{1}$ and $z_{3}$, both updated using a copy of $z_{3}$, but then
$z_{1}$ and $z_{3}$ are never combined in any later assignment.

$q_{0}$start$a\mid\alpha\begin{cases}x=abx\end{cases}$$x$

$p_{0}$start$p_{1}$$a\mid\beta^{1}\begin{cases}y=ya\end{cases}$$b\mid\beta^{2}\begin{cases}y=yb\end{cases}$$a\mid\beta^{3}\begin{cases}y=ya\end{cases}$$b\mid\beta^{4}\begin{cases}y=y\end{cases}$$y$

$r_{0}$start$r_{1}$$a\mid\gamma^{1}\begin{cases}z_{1}=\varepsilon&z_{2}=ab\\\
z_{3}=\varepsilon&z_{4}=ab\end{cases}$$a\mid\gamma^{2}\begin{cases}z_{1}=z_{3}&z_{2}=abz_{4}\\\
z_{3}=z_{3}&z_{4}=abz_{4}\end{cases}$$z_{1}z_{2}$

Figure 2: SSTs $T_{1}$ (top left), $T_{2}$ (top right), and their composition
$T_{3}$ (bottom).

$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$

Figure 3: Consecutive applications of $\gamma^{2}$.

The diagram in fig. 3 illustrates how variables flow into other variables
during two consecutive applications of assignment $\gamma^{2}$ in $T_{3}$.
Despite these assignments being copyful, the diagram makes clear that there is
no possibility of two copies of $z_{3}$ or $z_{4}$ converging and contributing
to a common variable on a level further down. We call copyful SSTs exhibiting
this type of behavior _diamond-free_. Intuitively, an SST is diamond-free if
there is at most one path between any two vertices in the assignment graph
induced by any computation. We establish that the families of transductions
definable by copyless SSTs and diamond-free SSTs coincide. Thus, the diamond-
free restriction, while weaker than the copyless restriction, preserves its
semantic intent, which is that outputs are linear in length relative to their
corresponding inputs.

#### Contributions and Outline.

In section 2, we provide preliminary definitions and notations. In section 3,
we present the composition construction for both DSSTs and NSSTs, prove their
correctness, and establish bounds on the size of the resulting transducers in
section 3.1. A key difference between our composition construction and that of
[1, 3] is that we carefully index variables of the composite in order to
partition them based on their role in the process. In section 3.2, we use this
indexing scheme to show that the composite transducer is always diamond-free.
Finally, in section 4, we formulate a construction that obtains, from any
diamond-free NSST, an equivalent copyless NSST. As a result, the removal of
non-copyless assignments can be added as post-processing step to the original
composition construction to yield a complete method for combining two copyless
SSTs into a third copyless SST realizing their composition. A diagrammatic
summary of our results in is given in fig. 4. By recovering a composition
construction that acts directly on copyless SSTs, we solidify the foundations
of works depending on this operation like those of Thakkar et al. [13], Dave
et al. [7]. While our construction yields a large SST, with a state space of
triply exponential size in the sizes of the input transducers, it circumvents
the process of converting the inputs into MSOTs, composing them, and compiling
the result back into a machine, which leads to SSTs of non-elementary size
relative to the inputs [11].

copyless $\textup{DSST}{}\circ\textup{DSST}{}$diamond-free DSSTfunctional
copyless NSSTcopyless DSSTdefinition 1definition 3Thm 3.5 of [3]copyless DSST
composition

copyless $\textup{NSST}{}\circ\textup{NSST}{}$diamond-free NSSTcopyless
NSSTdefinition 2definition 3copyless NSST composition

Figure 4: Schematic of the constructions comprising the procedures for
composing copyless SSTs.

#### Related Work.

The diamond-free property has been considered by Lopez, Monmege, and Talbot
[10] to study determinization of finitely-ambiguous cost-register automata.
While our notion of diamond-freeness coincides with theirs, our results are
independent and apply in distinct contexts.

Another restriction on copying behavior in SSTs, called _bounded-copy_ , is
introduced by Alur, Filiot, and Trivedi [5]. In that work, an SST is bounded-
copy if in the assignment graph for any computation, there are finitely many
paths between any two vertices. For any non-negative integer $k$, a bounded
copy SST is called $k$-copy if there at most $k$ paths between any two
vertices in the assignment graph induced by any computation. From this
definition, it is clear that diamond-free SSTs correspond to 1-copy SST. Note,
however, that [5] considers deterministic SSTs while the present work
considers nondeterministic SSTs. Furthermore the methods we use to convert
diamond-free NSSTs into copyless NSSTs are distinct from those employed in [5]
to convert bounded-copy DSSTs into copyless DSSTs.

##  2 Preliminaries

Let $\Sigma^{*}$ be the set of all strings over the alphabet $\Sigma$ and let
$\varepsilon$ be the empty string $\varepsilon$. For $s\in\Sigma$ and
$w\in\Sigma^{*}$ we write $s\in w$ if the symbol $s$ occurs in the string $w$.
We use the notation $\preceq$ for the prefix relation: $w\preceq w^{\prime}$
if some prefix of $w^{\prime}$ matches $w$ exactly. The symbol $\sqsubseteq$
will denote the suffix relation: $w\sqsubseteq w^{\prime}$ if some suffix of
$w^{\prime}$ matches $w$ exactly. We write $|w|$ for the length of the string
$w$ and $|w|_{s}$ for the number of occurrences of the symbol $s$ within $w$.
We use product notation to denote iterated concatenation, i.e.
$\prod^{n}_{k=1}w_{k}=w_{1}w_{2}\cdots w_{n}$.

For a relation $R\subseteq X\times Y$, we write
$\operatorname{\textup{dom}}{R}$ for its domain and
$\operatorname{\textup{im}}{R}$ for its image. The composition $f_{1}\circ
f_{2}:X\to Z$ of two functions $f_{1}:Y\to Z$ and $f_{2}:X\to Y$ is defined in
the standard fashion as $f_{1}\circ f_{2}=x\mapsto f_{1}(f_{2}(x))$. For a set
$X$, let $\textup{Id}_{X}$ be the identity function on $X$ which maps every
element $x$ to itself, and let $\textup{Er}_{X}$ be the erasing function on
$X$ which maps every element of $X$ to the empty string $\varepsilon$.

###  2.1 Streaming String Transducers

A streaming string transducer is a finite state machine equipped with a set of
write-only string variables that are updated at each step of a computation and
used to form an output. More formally, a streaming string transducer $T$ is a
tuple $(\Sigma,\Omega,Q,q_{0},X,A,\Delta,F)$ where $\Sigma$ and $\Omega$ are
finite input and output alphabets, $Q$ is a finite set of states, $q_{0}\in Q$
is the initial state, $X$ is a finite set of string variables, $A$ is a finite
set of type $X\to(\Omega\cup X)^{*}$ variable assignment functions,
$\Delta\subseteq Q\times\Sigma\times A\times Q$ is a transition relation,
$F:Q\to(\Omega\cup X)^{*}$ is a partial output function.

An assignment $\alpha$ of type $X\to(\Omega\cup X)^{*}$ can naturally be
extended to a morphism $(\Omega\cup X)^{*}\to(\Omega\cup X)^{*}$ such that
$\alpha(s)=s$, for $s\in\Omega$ and
$\alpha\left(\prod^{n}_{k=1}w_{k}\right)=\prod^{n}_{k=1}\alpha(w_{k})$, for
words in $(\Omega\cup X)^{*}$. When viewed in this manner as morphisms,
assignments can be composed in sequence, and we write
$\operatorname*{\bigcirc}^{n}_{k=1}\alpha_{k}=\alpha_{1}\circ\alpha_{2}\circ\ldots\circ\alpha_{n}$.

#### Semantics.

A run $\rho$ of an SST on an input word $w=w_{1}\cdots w_{n}\in\Sigma^{*}$ is
a finite sequence of transitions
$q_{0}\xrightarrow{w_{1},\alpha_{1}}\ldots\xrightarrow{w_{n},\alpha_{n}}q_{n}$
such that $(q_{k-1},w_{k},\alpha_{k},q_{k})\in\Delta$ for all $1\leq k\leq n$.
Define the valuation $\mathcal{V}_{\rho}$, of $\rho$, as
$\operatorname*{\bigcirc}^{n}_{k=1}\alpha_{k}$. An SST $T$ specifies a
relation $[\\![{T}]\\!]\subseteq\Sigma^{*}\times\Omega^{*}$ where

$[\\![{T}]\\!]=\left\\{\left(w,\textup{Er}_{X}\circ\mathcal{V}_{\rho}\circ
F(q_{n})\right):\textup{exists run }\rho\textup{ in }T\textup{ on }w\textup{
ending in }q_{n}\textup{ and
}q_{n}\in\operatorname{\textup{dom}}{F}\right\\}.$

An SST is deterministic (DSST), if for every pair $(q,s)\in Q\times\Sigma$
there is exactly one transition $(q,s,\alpha,q^{\prime})\in\Delta$, and is
nondeterministic (NSST) otherwise. A _functional_ NSST is one for which every
element of $\operatorname{\textup{dom}}{[\\![{T}]\\!]}$ maps to at most one
element of $\operatorname{\textup{im}}{[\\![{T}]\\!]}$.

#### Copying Variables.

A string $w\in(\Sigma_{1}\cup\Sigma_{2})^{*}$ is copyless in $\Sigma_{1}$ if
each element of $\Sigma_{1}$ occurs at most once in $w$; in other terms, when
$\max_{s\in\Sigma_{1}}\left|w\right|_{s}\leq 1$. We write
$\langle\Sigma_{1}\rangle$ for the set of copyless strings over
$\Sigma_{1}^{*}$. We write $\langle\Sigma_{1},\Sigma_{2}\rangle$ for set of
strings over $(\Sigma_{1}\cup\Sigma_{2})^{*}$ that are copyless in
$\Sigma_{1}$. An assignment $\alpha\in A$ is _copyless_ if the string
$\alpha(x_{1})\cdots\alpha(x_{\left|X\right|})$ is copyless in $X$. It is
straightforward to observe that any composition of copyless assignments is
also copyless. We say an SST is copyless if, for all transitions
$(q,s,\alpha,q^{\prime})\in\Delta$, the assignment $\alpha$ is copyless. An
SST is called _copyful_ , as studied by [8, 9], when it does not adhere to the
copyless restriction, i.e. it has at least one copyful assignment.

The following proposition characterizes the cardinality of the set of all
copyless strings over a finite alphabet in terms of the size of that alphabet,
and will be used to establish bounds on the size of composite SSTs in section
3.1.

######  Proposition 1.

If $\left|X\right|=n$ such that $2\leq n$, then $\left|\langle
X\rangle\right|=\left\lfloor en!\right\rfloor$.

###### Proof.

Strings in $\langle X\rangle$ can be any length less than or equal to $n$, so
counting the number of elements amounts to counting the number of ways to
choose without repetition and order $k$ elements from $X$ for
$0{\leq}k{\leq}n$. Thus,

$\left|\langle
X\rangle\right|=\sum^{n}_{k=0}\frac{n!}{(n-k)!}=n!\sum^{n}_{k=0}\frac{1}{(n-k)!}=n!\sum^{n}_{k=0}\frac{1}{k!}.$

By Taylor’s theorem, $e=\sum^{n}_{k=0}\frac{1}{k!}+\frac{e^{a}}{(n+1)!}$, for
some $a\in(0,1)$, and so we obtain the equation

$\left|\langle
X\rangle\right|=n!\left(e-\frac{e^{a}}{(n+1)!}\right)=en!-\frac{e^{a}}{n+1}.$

Since the map $a\mapsto e^{a}$ is increasing on $[0,1]$, the right-most term
of the above difference may be bounded as

$\frac{1}{n+1}\leq\frac{e^{a}}{n+1}\leq\frac{e}{n+1}.$

Furthermore, the assumption that $n\geq 2$ implies that $\frac{e^{a}}{n+1}<1$.
Finally, $\langle X\rangle$ is a finite set and thus has cardinality in the
positive integers, so we conclude that $\left|\langle
X\rangle\right|=\left\lfloor en!\right\rfloor$. ∎

#### Flow Graphs and Diamonds.

The copying behavior of an SST is characterized by _flow graphs_ associated to
its assignments. The flow graph, or simply the graph, of an assignment
$\alpha$ is a bipartite graph $G(\alpha)=(V(\alpha),E(\alpha))$ such that
$V(\alpha)=X^{S}\cup X^{T}$, where $X^{S}=\left\\{x^{S}:x\in X\right\\}$ and
$X^{T}=\left\\{x^{T}:x\in X\right\\}$ are distinguished copies of $X$, and
$E(\alpha)=\left\\{(x^{S},y^{T}):x\in\alpha(y)\right\\}$. The subsets $X^{S}$
and $X^{T}$ of $V(\alpha)$ are, respectively, the source and target layers of
the graph. Define $G(\alpha\alpha)=(V(\alpha\alpha),E(\alpha\alpha))$ to be
the tripartite graph obtained by gluing together two copies of $G(\alpha)$
such that the target layer of the first copy is the source layer of the
second. More precisely, $V(\alpha\alpha)=X^{S}\cup X\cup X^{T}$ and
$E(\alpha\alpha)=\left\\{(x^{S},y):x\in\alpha(y)\right\\}\cup\left\\{(x,y^{T}):x\in\alpha(y)\right\\}$.

A _diamond_ in $G(\alpha\alpha)$ is a subgraph consisting of four vertices
$x^{S},x,y,x^{T}$ and four edges $(x^{S},x)$, $(x^{S},y)$, $(x,x^{T})$,
$(y,x^{T})$. As a degenerate case, parallel edges, that is when $x=y$, are
considered diamonds as well. An assignment is _diamond-free_ if there are no
diamonds present in the graph $G(\alpha\alpha)$. Note that copyless
assignments are diamond-free, but diamond-free assignments are not necessarily
copyless. The graph $G(\rho)=G(\alpha_{1}\cdots\alpha_{n})$ of a run
$\rho=q_{0}\xrightarrow{w_{1},\alpha_{1}}\cdots\xrightarrow{w_{n},\alpha_{n}}q_{n}$
is obtained by gluing together the graphs $G(\alpha_{1}),\ldots,G(\alpha_{n})$
in the same manner used to construct $G(\alpha\alpha)$. Since runs can be
arbitrary length, we use superscripts matching the subscripts on the states in
the run to distinguish the layers of $G(\rho)$. Thus, we have that
$V(\rho)=\bigcup^{n}_{k=0}X^{k}$ and
$E(\rho)=\bigcup^{n}_{k=1}\left\\{(x^{k-1},y^{k}):x\in\alpha_{k}(y)\right\\}$.
A run is diamond-free iff there is at most one path between any two vertices,
i.e. if it does not have a diamond-shaped subgraph. An SST $T$ is diamond-free
iff every run in $T$ is diamond-free. Note that an SST may not be diamond-free
even if all its assignments are diamond-free.

##  3 Composition Construction

This section presents a modified and elaborated presentation of the
composition construction of [1, 3]. The departure from [1, 3] is in a detailed
indexing of the string variables of the composite that allows a clean
partition based on their role in the process, and allows us to establish
diamond-freeness in an almost type-directed manner. For this section, fix
copyless SSTs $T_{12}=(\Sigma_{1},\Sigma_{2},Q,q_{0},X,A,\Delta_{12},F_{12})$
and $T_{23}=(\Sigma_{2},\Sigma_{3},P,p_{0},Y,B,\Delta_{23},F_{23})$ as inputs
and $T_{13}=(\Sigma_{1},\Sigma_{3},R,r_{0},Z,C,\Delta_{13},F_{13})$ as their
composite.

The procedure relies on storing two types of _summaries_ as finite maps in the
states of the composite.

  1. 1.

The first map is the _state summary_ map $f:(P\times X)\to P$ that records the
state in $T_{23}$ that is reached when reading the contents of a variable $x$,
for every possible combination of starting states in $p\in P$ of $T_{23}$ and
variables $x\in X$ of $T_{12}$.

  2. 2.

The second map is the _shape summary_ map $g:(P\times X\times Y)\to\langle
Y\cup Z\rangle$ that stores the shape of each variable $y\in Y$ after reading
a variable $x\in X$ from a starting point $p\in P$, for every possible
combination of inputs.

Since their domains and ranges are finite, these maps are finitely
representable and furthermore there are finitely many maps of each given type.
We write $\mathbb{F}$ for the space of all functions with type $(P\times X)\to
P$ and $\mathbb{G}$ for the space of all functions of type $(P\times X\times
Y)\to\langle Y\cup Z\rangle$.

The main idea of the construction is to simulate the state transitions of
$T_{12}$ while keeping a record of what $T_{23}$ does when reading any
possible register in $X$ from any possible state in $P$. Since $T_{12}$ builds
its output in a piecewise manner, and not linearly as ordinary one-way finite
state transducers do, these records are essential. By storing the actions of
$T_{23}$ for any possible eventuality, it is possible to then string together
those actions which correspond to the run of $T_{23}$ on the output of
$T_{12}$. The $f$ map allows us to store a destination state based on the
contents of the $X$ variables, while the $g$ map tracks the shapes of
variables in $T_{23}$ resulting from applying sequences of assignments induced
by the contents of variables in $T_{12}$. The $Z$ variables are used by the
shape summary maps to store non-variable substrings of shapes and thereby
ensure the finitude of shape summaries.

Below are defined a number of functions that will facilitate the construction
of $T_{13}$. We use $\vec{x}$ to represent strings from $\langle
X,\Sigma_{2}\rangle$, $\vec{y}$ to denote strings from $\langle Y\cup
Z,\Sigma_{3}\rangle$ or $\langle Y,\Sigma_{3}\rangle$, and $\vec{z}$ to denote
strings from $\langle Z,\Sigma_{3}\rangle$. We write $g^{p}_{x}$ for the map
$y\mapsto g(p,x,y)$, where $g\in\mathbb{G}$.

$y_{k}$$\qquad\vec{z}_{k-1}\qquad$$\quad\cdots\quad$$\qquad\vec{z}_{k}\qquad$$\quad\cdots\quad$$y_{1}$$\qquad\vec{z}_{0}\qquad$$y_{n}$$\qquad\vec{z}_{n}\qquad$$y_{k}$$z^{p,x}_{y_{k},0}$$\quad\cdots\quad$$z^{p,x}_{y_{k+1},0}$$\quad\cdots\quad$$y_{1}$$z^{p,x}_{y_{1},0}$$y_{n}$$z^{p,x}_{y,1}$$h(y)=$$g^{p}_{x}(y)=$$\gamma^{p}_{x}$

Figure 5: The relationship between an assignment summary
$h=\mathcal{G}(p,\alpha(x),f,g)$, and the corresponding shape
$g^{p}_{x}=\mathcal{S}^{p}_{x}(h)$ and assignment
$\gamma^{p}_{x}=\mathcal{A}^{p}_{x}(h)$.

#### State Transition Summarizer.

The operator $\mathcal{F}:(P\times\langle
X,\Sigma_{2}\rangle\times\mathbb{F})\to P$ is defined as

$\mathcal{F}(p,\vec{x},f)=\begin{cases}p&\textup{if }\vec{x}=\varepsilon\\\
\mathcal{F}(p^{\prime},\vec{x}^{\prime},f)&\textup{if
}\vec{x}=s\vec{x}^{\prime}\textup{ and
}(p,s,\alpha,p^{\prime})\in\Delta_{23}\\\
\mathcal{F}(f(p,x),\vec{x}^{\prime},f)&\textup{if
}\vec{x}=x\vec{x}^{\prime}.\end{cases}$ (1)

#### Assignment Summarizer.

The processes that create shape summaries and assignments share a dependency
on operator $\mathcal{G}:(P\times\langle
X,\Sigma_{2}\rangle\times\mathbb{F}\times\mathbb{G})\to(Y\to\langle Y\cup
Z,\Sigma_{3}\rangle)$ defined as

$\mathcal{G}(p,\vec{x},f,g)=\begin{cases}\textup{Id}_{Y}&\text{if
}\vec{x}=\varepsilon\\\
\beta\circ\mathcal{G}(p^{\prime},\vec{x}^{\prime},f,g)&\textup{if
}\vec{x}=s\vec{x}^{\prime}\textup{ and
}(p,s,\beta,p^{\prime})\in\Delta_{23}\\\
g^{p}_{x}\circ\mathcal{G}(f(p,x),\vec{x}^{\prime},f,g)&\textup{if
}\vec{x}=x\vec{x}^{\prime}.\end{cases}$ (2)

#### Shape Generator.

The operator $\mathcal{S}:(P\times X\times(Y\to\langle Y\cup
Z,\Sigma_{3}\rangle))\to(Y\to\langle Y\cup Z\rangle)$ computes shape summaries
and is given as

$\mathcal{S}(p,x,h)=y\mapsto\left(\prod^{n}_{k=1}z^{p,x}_{y_{k},0}y_{k}\right)z^{p,x}_{y,1}\qquad\textup{
if }h(y)=\vec{z}_{0}\prod^{n}_{k=1}y_{k}\vec{z}_{k}.$ (3)

#### Assignment Generator.

The operator $\mathcal{A}:(P\times X\times(Y\to\langle Y\cup
Z,\Sigma_{3}\rangle))\to(Z\to\langle Z,\Sigma_{3}\rangle)$ computes
assignments and is given as

$\mathcal{A}(p,x,h)=\begin{cases}z^{p,x}_{y,0}\mapsto\varepsilon&\textup{if
}y\notin h(y^{\prime}),\textup{ for all }y^{\prime}\in Y\\\
z^{p,x}_{y,0}\mapsto\vec{z}&\textup{if }\vec{z}y\preceq h(y^{\prime})\textup{
or }y^{\prime\prime}\vec{z}y\in h(y^{\prime})\textup{ for some
}y^{\prime},y^{\prime\prime}\in Y\\\ z^{p,x}_{y,1}\mapsto\vec{z}&\textup{if
}h(y)=\vec{z}\textup{ or }y^{\prime}\vec{z}\sqsubseteq h(y),\textup{ for some
}y^{\prime}\in Y.\end{cases}$ (4)

We write $\mathcal{S}^{p}_{x}$ and $\mathcal{A}^{p}_{x}$, respectively, for
the mappings $h\mapsto\mathcal{S}(p,x,h)$ and $h\mapsto\mathcal{A}(p,x,h)$.
Alternatively stated, $\mathcal{S}^{p}_{x}$ and $\mathcal{A}^{p}_{x}$ are
defined such that the next equation holds for all $y\in Y$.

$\mathcal{G}(p,\alpha(x),f,g)(y)=\gamma^{p}_{x}\circ g^{p}_{x}(y).$ (5)

Thus, the following diagram, in which $\pi_{k}$ and $\iota_{k}$ are the
$k^{\textup{th}}$ canonical projection and injection, commutes. This
relationship is further illustrated in fig. 5.

${\mathcal{G}(p,\alpha(x),f,g)}$${\gamma^{p}_{x}}$${(\gamma^{p}_{x},g^{p}_{x})}$${g^{p}_{x}}$$\scriptstyle{\mathcal{S}^{p}_{x}}$$\scriptstyle{(\mathcal{A}^{p}_{x},\mathcal{S}^{p}_{x})}$$\scriptstyle{\mathcal{A}^{p}_{x}}$$\scriptstyle{\iota_{1}}$$\scriptstyle{\pi_{2}}$$\scriptstyle{\pi_{1}}$$\scriptstyle{\circ}$$\scriptstyle{\iota_{2}}$

The following definition formalizes the construction of $T_{3}$ from DSSTs
$T_{1}$ and $T_{2}$ using the operators we have just defined.

######  Definition 1 (DSST Composition).

For a pair of copyless DSSTs
$T_{12}=(\Sigma_{1},\Sigma_{2},Q,q_{0},X,A,\Delta_{12},F_{12})$ and
$T_{23}=(\Sigma_{2},\Sigma_{3},P,p_{0},Y,B,\Delta_{23},F_{23})$, their
composition is a DSST
$T_{13}=(\Sigma_{1},\Sigma_{3},R,r_{0},Z,C,\Delta_{13},F_{13})$ where

  * •

$R=Q\times\mathbb{F}\times\mathbb{G}$ such that $r_{0}=(q_{0},f_{0},g_{0})$
with $f_{0}(p,x)=p$ and $g_{0}(p,x,y)=y$,

  * •

$Z=\left\\{z^{p,x}_{y,0},z^{p,x}_{y,1}:(p,x,y)\in P\times X\times Y\right\\}$,

  * •

$C=\left\\{\gamma:(r,s,\gamma,r^{\prime})\in\Delta_{13}\right\\}$,

  * •

$((q,f,g),s,\gamma,(q^{\prime},f^{\prime},g^{\prime}))\in\Delta_{13}$ iff,
there exists $(q,s,\alpha,q^{\prime})\in\Delta_{12}$ such that

    * –

$f^{\prime}(p,x)=\mathcal{F}(p,\alpha(x),f)$,

    * –

$g^{\prime}(p,x,y)=\mathcal{S}^{p}_{x}(\mathcal{G}(p,\alpha(x),f,g))(y)$,

    * –

$\gamma(z)=\mathcal{A}^{p}_{x}(\mathcal{G}(p,\alpha(x),f,g))(z)$ for
$z\in\left\\{z^{p,x}_{y,0},z^{p,x}_{y,1}:y\in Y\right\\}$,

  * •

$F_{13}(q,f,g)=\textup{Er}_{Y}\circ\mathcal{G}(p_{0},F_{12}(q),f,g)\circ
F_{23}(\mathcal{F}(p_{0},F_{12}(q),f))$.

| $f_{0}$ | $g_{0}$
---|---|---
$q_{0}$ | $(p_{0},x){\mapsto}p_{0}$ | $(p_{0},x,y){\mapsto}y$
| $(p_{1},x){\mapsto}p_{1}$ | $(p_{1},x,y){\mapsto}y$
start | $f_{1}$ | $g_{1}$
---|---|---
$q_{0}$ | $(p_{0},x){\mapsto}p_{1}$ | $(p_{0},x,y){\mapsto}z_{1}yz_{2}$
| $(p_{1},x){\mapsto}p_{1}$ | $(p_{1},x,y){\mapsto}z_{3}yz_{4}$
$a\mid\gamma^{1}\begin{cases}z_{1}=\varepsilon&z_{2}=ab\\\
z_{3}=\varepsilon&z_{4}=ab\end{cases}$$a\mid\gamma^{2}\begin{cases}z_{1}=z_{3}&z_{2}=abz_{4}\\\
z_{3}=z_{3}&z_{4}=abz_{4}\end{cases}$$z_{1}z_{2}$ Figure 6: A detailed view of
internal maps contained in the states of $T_{3}$ from Figure 2, when
constructed according to Definition 1. Note that we omit unreachable states.

Definition 1 requires minimal adaptation for NSSTs. In particular, it becomes
necessary to synchronize the computation of state summaries with the
computation of shape summaries and assignments. To see why, consider the NSST
in fig. 7. If we use $\mathcal{F}$ and $\mathcal{G}$ independently, we end up
with pairs like $(p_{4},\beta_{2}\circ\beta_{6})$ which summarize runs that
are not possible in the machine. This synchronization is achieved by combining
$\mathcal{F}$ and $\mathcal{G}$ into another operator
$\mathcal{H}:(P\times\langle
X,\Sigma_{2}\rangle\times\mathbb{F}\times\mathbb{G})\to 2^{P\times(Y\to\langle
Y\cup Z,\Sigma_{3}\rangle)}$ which is given as follows.

$\mathcal{H}(p,\vec{x},f,g)=\begin{cases}\left\\{\left(p,\textup{Id}_{Y}\right)\right\\}&\textup{if
}\vec{x}=\varepsilon\\\
\bigcup_{(p,s,\alpha,p^{\prime})\in\Delta_{23}}\left\\{(p^{\prime\prime},\alpha\circ
h):(p^{\prime\prime},h)\in\mathcal{H}(p^{\prime},\vec{x}^{\prime},f,g)\right\\}&\textup{if
}\vec{x}=s\vec{x}^{\prime}\\\ \left\\{(p^{\prime},g^{p}_{x}\circ
h):(p^{\prime},h)\in\mathcal{H}(f(p,x),\vec{x}^{\prime},f,g)\right\\}&\textup{if
}\vec{x}=x\vec{x}^{\prime}\end{cases}$

The following definition formalizes the construction of $T_{3}$ from NSSTs
$T_{1}$ and $T_{2}$.

######  Definition 2 (NSST Composition).

For a pair of copyless NSSTs
$T_{12}=(\Sigma_{1},\Sigma_{2},Q,q_{0},X,A,\Delta_{12},F_{12})$ and
$T_{23}=(\Sigma_{2},\Sigma_{3},P,p_{0},Y,B,\Delta_{23},F_{23})$, their
composite is a NSST
$T_{13}=(\Sigma_{1},\Sigma_{3},R,r_{0},Z,C,\Delta_{13},F_{13})$ where

  * •

$R=Q\times\mathbb{F}\times\mathbb{G}$ such that $r_{0}=(q_{0},f_{0},g_{0})$
with $f_{0}(p,x)=p$ and $g_{0}(p,x,y)=y$,

  * •

$Z=\left\\{z^{p,x}_{y,0},z^{p,x}_{y,1}:(p,x,y)\in P\times X\times Y\right\\}$,

  * •

$C=\left\\{\gamma:(r,s,\gamma,r^{\prime})\in\Delta_{13}\right\\}$,

  * •

$((q,f,g),s,\gamma,(q^{\prime},f^{\prime},g^{\prime}))\in\Delta_{13}$ iff
there exist $(q,s,\alpha,q^{\prime})\in\Delta_{12}$ such that

    * –

$(p^{\prime},h)\in\mathcal{H}(p,\alpha(x),f,g)$,

    * –

$f^{\prime}(p,x)=p^{\prime}$,

    * –

$g^{\prime}(p,x,y)=\mathcal{S}^{p}_{x}(h)(y)$,

    * –

$\gamma(z)=\mathcal{A}^{p}_{x}(h)(z)$, for
$z\in\left\\{z^{p,x}_{y,0},z^{p,x}_{y,1}:y\in Y\right\\}$,

  * •

$F_{13}(q,f,g)=\textup{Er}_{Y}\circ h\circ F_{23}(p)$ with
$(p,h)\in\mathcal{H}(p_{0},F_{12}(q),f,g)$ chosen nondeterministically.

$p_{1}$start$p_{2}$$p_{4}$$p_{5}$$p_{3}$$p_{6}$$p_{7}$$a\mid\beta_{1}$$a\mid\beta_{2}$$a\mid\beta_{3}$$a\mid\beta_{4}$$a\mid\beta_{5}$$a\mid\beta_{6}$
Figure 7: An NSST illustrating the need for $\mathcal{H}$.

Note that, besides accommodating nondeterminism in the inputs, the use of
$\mathcal{H}$ in definition 2 does not change the essential nature of the
composition construction. In particular, the methods by which summaries and
corresponding assignments are computed are identical in both definitions 1 and
2. The way in which these elements are combined to form transitions in
$\Delta_{13}$ differs, but this does not influence the manner in which
variables are copied by assignments in $C$. Fortunately, our results are
largely independent of this distinction. In order to minimize the book-keeping
and notation involved in our arguments, the analyses in sections 3.1 and 3.2
are given in terms of DSSTs and definition 1. Theorems 1 and 2, however, apply
both for DSSTs and for NSSTs.

###  3.1 Correctness and Size Bounds

Suppose $(s,t)\in[\\![{T_{12}}]\\!]$ and $(t,u)\in[\\![{T_{23}}]\\!]$ such
that there are corresponding runs
$\rho=q_{0}\xrightarrow{s_{1},\alpha_{1}}\ldots\xrightarrow{s_{n},\alpha_{n}}q_{n}$
and
$\sigma=p_{0}\xrightarrow{t_{1},\beta_{1}}\ldots\xrightarrow{t_{m},\beta_{m}}p_{m}$.
By definition 1, for every transition
$(q_{k-1},s_{k},\alpha_{k},q_{k})\in\Delta_{12}$ occurring in $\rho$, there
exists a transition
$((q_{k-1},f_{k-1},g_{k-1}),s_{k},\gamma_{k},(q_{k},f_{k},g_{k}))\in\Delta_{13}$.
Let $\tau$ be the corresponding run
$(q_{0},f_{0},g_{0})\xrightarrow{s_{1},\gamma_{1}}\ldots\xrightarrow{s_{n},\gamma_{n}}(q_{n},f_{n},g_{n})$
in $T_{13}$. Also, let $\alpha=\operatorname*{\bigcirc}^{n}_{k=1}\alpha_{k}$
and $\gamma=\operatorname*{\bigcirc}^{n}_{k=1}\gamma_{k}$.

######  Lemma 1.

For any $x\in X$ and $p\in P$, if $\sigma(p,x)$ is the run in $T_{12}$ on
input $\mathcal{V}_{\rho}(x)$, starting from state $p$ and ending in state
$p^{\prime}$, then the following equation holds for all $n\in\mathbb{N}$.

$f_{n}(p,x)=p^{\prime}$ (6)

###### Proof.

We proceed by induction on $n$, the length of $\rho$ and $\tau$.

Base case.

_eq. 6 holds when $n=0$._

If $n=0$, then $\rho=q_{0}$ and $\tau=(q_{0},f_{0},g_{0})$. Therefore,
$\mathcal{V}_{\rho}(x)=\varepsilon$, for all $x\in X$, and so for all $p\in P$
and $x\in X$, we have $\sigma(p,x)=p=p^{\prime}$. By definition 1, it holds
that $f_{0}(p,x)=p$.

Inductive case.

_If eq. 6 holds for $n-1$, then it also holds for $n$._

By definition 1, $f_{n}(p,x)=\mathcal{F}(p,\alpha_{n}(x),f_{n-1})$, for all
$(p,x)\in P\times X$. Observe that $\mathcal{F}(p,\alpha_{n}(x),f_{n-1})$
partially simulates the transitions of $T_{23}$, by reading $\alpha_{n}(x)$ in
sequence and keeping track of the current state. This simulation operates
according to $\Delta_{23}$ when the next symbol of $\alpha_{n}(x)$ comes from
$\Sigma_{2}$ and according to $f_{n-1}$ when the next symbol comes from $X$.
In other other words, for every state $p$, $\alpha_{n}(x)$ induces a sequence
of states $\langle p_{k}\rangle^{\left|\alpha_{n}(x)\right|}_{k=0}$, via
$\mathcal{F}$, such that $p_{0}=p$ and either (i)
$(p_{k},s,\beta,p_{k+1})\in\Delta_{23}$ for some $\beta\in B$, if the
$k^{\textup{th}}$ symbol of $\alpha_{n}(x)$ is $s\in\Sigma_{2}$, or (ii)
$f_{n-1}(p_{k},x^{\prime})=p_{k+1}$, if the $k^{\textup{th}}$ symbol of
$\alpha_{n}(x)$ is $x^{\prime}\in X$. The former case is correct by
definition, while the latter follows from the inductive hypothesis. Thus
$f_{n}(p,x)=\mathcal{F}(p,\alpha_{n}(x),f_{n-1})=p_{\left|\alpha_{n}(x)\right|}=p^{\prime}$,
and correctness of $f_{n-1}$ implies correctness of $f_{n}$. ∎

######  Lemma 2.

Consider $\gamma:Z\to\langle Z,\Sigma_{3}\rangle$ and $h:Y\to\langle Y\cup
Z,\Sigma_{3}\rangle$, and suppose $\phi(a)=a$ for any function $\phi$ and
$a\notin\operatorname{\textup{dom}}{\phi}$. For all $z\in Z$, the equation
$\gamma(z)=h\circ\gamma(z)=\gamma\circ h(z)$ holds.

###### Proof.

Follows from the fact that $\operatorname{\textup{dom}}{h}=Y$ is disjoint from
$\operatorname{\textup{im}}{\gamma}=\langle Z,\Sigma_{3}\rangle$. ∎

######  Lemma 3.

For any $x\in X$, $p\in P$, and $y\in Y$, if $\sigma(p,x)$ is the run in
$T_{12}$ on input $\mathcal{V}_{\rho}(x)$, starting from state $p$, then the
following equation holds for all $n\in\mathbb{N}$.

$\mathcal{V}_{\sigma(p,x)}(y)=\textup{Er}_{Z}\circ\mathcal{V}_{\tau}\circ
g_{n}(p,x,y)$ (7)

###### Proof.

We proceed by induction on $n$.

Base case.

_eq. 7 holds when $n=0$._

Because $\sigma(p,x)=p$, we have that $\mathcal{V}_{\sigma(p,x)}(y)=y$, for
all $y\in Y$. By definition 1 $g_{0}(p,x,y)=y$, and so
$\mathcal{V}_{\tau}\circ g_{0}(p,x,y)=y$, since $\mathcal{V}_{\tau}$ is of
type $\langle Z,\Sigma_{3}\rangle\to\langle Z,\Sigma_{3}\rangle$. Likewise
$\textup{Er}_{Z}$ does not erase variables from $Y$, so
$\textup{Er}_{Z}\circ\mathcal{V}_{\tau}\circ
g_{0}(p,x,y)=y=\mathcal{V}_{\sigma(p,x)}(y)$.

Inductive case.

_If eq. 7 holds for $n-1$, then it also holds for $n$._

Suppose that
$\rho^{\prime}=q_{0}\xrightarrow{s_{1},\alpha_{1}}\ldots\xrightarrow{s_{n-1},\alpha_{n-1}}q_{n-1}$,
where $\rho=\rho^{\prime}\xrightarrow{s_{n},\alpha_{n}}q_{n}$, and that
$\tau^{\prime}=(q_{0},f_{0},g_{0})\xrightarrow{s_{1},\gamma_{1}}\ldots\xrightarrow{s_{n-1},\gamma_{n-1}}(q_{n-1},f_{n-1},g_{n-1})$
where $\tau=\tau^{\prime}\xrightarrow{s_{n},\gamma_{n}}(q_{n},f_{n},g_{n})$.
Further suppose that $\sigma^{\prime}(p,x)$ is the run in $T_{23}$ on
$\mathcal{V}_{\rho^{\prime}}(x)$, starting from state $p$. Let
$\alpha_{n}(x)=w_{0}x_{1}\cdots x_{l}w_{l}$, and let $w^{j}_{i}$ denote the
$j^{\textup{th}}$ symbol in $w_{i}$. A run $\sigma(p,x)$ in $T_{23}$ can be
written as

$\sigma(p,x)=p\xrightarrow{w^{1}_{0},\beta^{1}_{0}}\ldots
p_{\left|w_{1}x_{1}\cdots
w_{i}\right|}\xrightarrow{x_{i},\mathcal{V}_{\sigma^{\prime}(p_{|w_{0}x_{1}\cdots
w_{i-1}|},x_{i})}}p_{\left|w_{0}x_{1}\cdots
x_{i}\right|}\ldots\xrightarrow{w^{\left|w_{l}\right|}_{l},\beta^{\left|w_{l}\right|}_{l}}p_{\left|\alpha_{n}(x)\right|}.$

Consequently, we obtain the following derivation, which completes the proof.

$\displaystyle\mathcal{V}_{\sigma(p,x)}(y)$
$\displaystyle=\left(\operatorname*{\bigcirc}^{\left|w_{0}\right|}_{k=1}\beta^{k}_{0}\circ\operatorname*{\bigcirc}^{l}_{i=1}\mathcal{V}_{\sigma^{\prime}(p_{w_{0}x_{1}\cdots
w_{i-1}},x_{i})}\circ\operatorname*{\bigcirc}^{\left|w_{i}\right|}_{j=1}\beta^{i}_{j}\right)(y)$
(8)
$\displaystyle=\left(\operatorname*{\bigcirc}^{\left|w_{0}\right|}_{k=1}\beta^{k}_{0}\circ\operatorname*{\bigcirc}^{l}_{i=1}\textup{Er}_{Z}\circ\mathcal{V}_{\tau^{\prime}}\circ
g_{n-1}(p_{w_{0}x_{1}\cdots
w_{i-1}},x_{i},\cdot)\circ\operatorname*{\bigcirc}^{\left|w_{i}\right|}_{j=1}\beta^{i}_{j}\right)(y)$
(9)
$\displaystyle=\left(\textup{Er}_{Z}\circ\mathcal{V}_{\tau^{\prime}}\circ\operatorname*{\bigcirc}^{\left|w_{0}\right|}_{k=1}\beta^{k}_{0}\circ\operatorname*{\bigcirc}^{l}_{i=1}g_{n-1}(p_{w_{0}x_{1}\cdots
w_{i-1}},x_{i},\cdot)\circ\operatorname*{\bigcirc}^{\left|w_{i}\right|}_{j=1}\beta^{i}_{j}\right)(y)$
(10)
$\displaystyle=\textup{Er}_{Z}\circ\mathcal{V}_{\tau^{\prime}}\circ\mathcal{G}(p,\alpha_{n}(x),f_{n-1},g_{n-1})(y)$
(11)
$\displaystyle=\textup{Er}_{Z}\circ\mathcal{V}_{\tau^{\prime}}\circ\gamma_{n}\circ
g_{n}(p,x,y)$ (12) $\displaystyle=\textup{Er}_{Z}\circ\mathcal{V}_{\tau}\circ
g_{n}(p,x,y)$ (13)

From eq. 8, we obtain eq. 9 from the inductive hypothesis. We get eq. 10 by
applying lemma 2. From here, eq. 11 is obtained from the definition of
$\mathcal{G}$ in eq. 2. Next, eq. 12 follows from eq. 5 and the definitions of
$\mathcal{S}$ and $\mathcal{A}$. Finally, eq. 13 is implied by the definition
of valuation.

∎

######  Theorem 1.

If $T_{13}$ is a composition of $T_{23}$ and $T_{12}$ according to the
construction detailed in this section, then the following hold.

  1. 1.

$[\\![{T_{13}}]\\!]=[\\![{T_{23}}]\\!]\circ[\\![{T_{12}}]\\!]$

  2. 2.

If $T_{12}$ has $k$ states and $l$ variables and $T_{23}$ has $n$ states and
$m$ variables, then $T_{13}$ has a state space of size
$O(kn^{ln}((2lnm+m)!)^{lnm})$ and $2lnm$ variables.

###### Proof.

The proof is in two parts.

  1. 1.

Observe the following derivation:

$\displaystyle[\\![{T_{13}}]\\!](s)$
$\displaystyle=\textup{Er}_{Z}\circ\mathcal{V}_{\tau}\circ
F_{13}((q_{n},f_{n},g_{n}))$ (14)
$\displaystyle=\textup{Er}_{Z}\circ\mathcal{V}_{\tau}\circ\textup{Er}_{Y}\circ\mathcal{G}(p_{0},F_{12}(q_{n}),f_{n},g_{n})\circ
F_{23}(\mathcal{F}(p_{0},F_{12}(q_{n}),f_{n}))$ (15)
$\displaystyle=\textup{Er}_{Y}\circ\textup{Er}_{Z}\circ\mathcal{V}_{\tau}\circ\mathcal{G}(p_{0},F_{12}(q_{n}),f_{n},g_{n})\circ
F_{23}(p_{m}).$ (16)

From eq. 14, we obtain eq. 15 by applying definition 1. Equation 16 follows
from eq. 15 via application of lemma 1. Considering the output of $T_{12}$ as
the value of a variable $x_{\textup{out}}$, as in [12], we can rewrite eq. 16
as

$\displaystyle[\\![{T_{13}}]\\!](s)=\textup{Er}_{Y}\circ\textup{Er}_{Z}\circ\mathcal{V}_{\tau}\circ\gamma_{n+1}\circ
g_{n+1}(p_{0},x_{\textup{out}},\cdot)\circ F_{23}(p_{m}),$ (17)
$\displaystyle\textup{where}\qquad\gamma_{n+1}=\mathcal{A}(p_{0},x_{\textup{out}},\mathcal{G}(p_{0},F_{12}(q_{n}),f_{n},g_{n}))$
$\displaystyle\textup{and}\qquad
g_{n+1}(p_{0},x_{\textup{out}},\cdot)=\mathcal{S}(p_{0},x_{\textup{out}},\mathcal{G}(p_{0},F_{12}(q_{n}),f_{n},g_{n})).$

Since by definition
$[\\![{T_{12}}]\\!](s)=\textup{Er}_{X}\circ\mathcal{V}_{\rho}(x_{\textup{out}})$,
applying lemma 3 to eq. 17 yields

$[\\![{T_{13}}]\\!](s)=\textup{Er}_{Y}\circ\mathcal{V}_{\sigma}\circ
F_{23}(p_{m})=[\\![{T_{23}}]\\!](t).$

  2. 2.

By definition 1, the state space of $R$ of $T_{13}$ is comprised by the
product $Q\times\mathbb{F}\times\mathbb{G}$ where $\mathbb{F}=(P\times X)\to
P$ and $\mathbb{G}=(P\times X\times Y)\to\langle Y\cup Z\rangle$. Therefore,
we have

$\displaystyle\left|\mathbb{F}\right|=\left|P\right|^{\left|P\times
X\right|}=n^{ln}\textup{ and}$
$\displaystyle\left|\mathbb{G}\right|=\left|\langle Y\cup
Z\rangle\right|^{\left|P\times X\times Y\right|}=\left|\langle Y\cup
Z\rangle\right|^{lnm}.$

It is clear from definition 1 that $\left|Z\right|=2lnm$, and applying
proposition 1 yields the equality

$\left|\langle Y\cup Z\rangle\right|=\left\lfloor e(m+2lnm)!\right\rfloor.$

As a result, we get that $\left|R\right|=kn^{ln}\left\lfloor
e(m+2lnm)!\right\rfloor^{lnm}$ and thus $\left|R\right|\in
O\left(kn^{ln}((2lnm+m)!)^{lnm}\right)$.

∎

###  3.2 Establishing the Diamond-Free Property

We define two binary relations, $\overset{\scriptscriptstyle{X}}{\sim}$ and
$\equiv$, over the $Z$ variables:

  1. 1.

$z^{p,x}_{y,b}\overset{\scriptscriptstyle{X}}{\sim}z^{x^{\prime},p^{\prime}}_{y^{\prime},b^{\prime}}$
iff $x=x^{\prime}$,

  2. 2.

$z^{p,x}_{y,b}\equiv z^{x^{\prime},p^{\prime}}_{y^{\prime},b^{\prime}}$ iff
$x=x^{\prime}$ and $p=p^{\prime}$.

It is easy to see that $\overset{\scriptscriptstyle{X}}{\sim}$ and $\equiv$
are equivalence relations. The relation
$\overset{\scriptscriptstyle{X}}{\sim}$ partitions $Z$ into $|X|$ classes,
each of size $2|Y{\times}P|$. Similarly, the relation $\equiv$ partitions $Z$
into $|X\times P|$ classes each of size $2|Y|$. Abusing notation, we sometimes
write $[z]_{\overset{\scriptscriptstyle{X}}{\sim}}=x$ to denote that $z$
belongs to the class indexed by $x$. Similarly, we write $[z]_{\equiv}=(p,x)$
to denote that the equivalence class of $z$ is indexed by this pair. We next
utilize these relations and the structure they impose on $Z$ to show that the
composite transducer is bounded-copy. In the following, $\alpha$ is always an
assignment in $T_{13}$, and $z,z^{\prime},z_{1},$ etc. will refer to generic
variables from $Z$.

######  Lemma 4.

For any state $(q,f,g)\in R$, variable $z\in Z$, and $(p,x,y)\in P\times
X\times Y$, it holds that $\left|g(p,x,y)\right|_{z}\leq 1$ and if $z\in
g(p,x,y)$, then $[z]_{\equiv}=(p,x)$.

###### Proof.

By definition of the initial shape summary $g_{0}$ it is clear that
$\left|g_{0}(p,x,y)\right|_{z}=0$, regardless of $p,x,y,z$. Any other shape
summary occurring in $T_{13}$ is constructed by the map $\mathcal{S}$ which is
defined, in eq. 3, such that no variable from $Z$ occurs twice in the image of
a single element of the domain. Additionally, it is easy to see from the same
definition in eq. 3 that any $z\in\mathcal{S}(p,x,h)(y)$ must be indexed by
the pair $(p,x)$, invariant of $h$ and $y$, thus implying that
$[z]_{\equiv}=(p,x)$. ∎

######  Lemma 5.

Let $\alpha:X\to\langle X,\Sigma_{2}\rangle$ be arbitrary and suppose that
$z_{1}\in\mathcal{G}(p_{1},\alpha(x_{1}),f,g)(y_{1})$ and
$z_{2}\in\mathcal{G}(p_{2},\alpha(x_{2}),f,g)(y_{2})$. If $x_{1}\neq x_{2}$,
then $z_{1}\not\overset{\scriptscriptstyle{X}}{\sim}z_{2}$.

###### Proof.

If $z_{1}\overset{\scriptscriptstyle{X}}{\sim}z_{2}$, then there must be a
unique variable $x$ such that $\mathcal{G}(p_{1},\alpha(x_{1}),f,g)$ uses a
shape summary $g^{p_{1}^{\prime}}_{x}$ and
$\mathcal{G}(p_{2},\alpha(x_{2}),f,g)$ uses a shape summary
$g^{p_{2}^{\prime}}_{x}$ for some states $p^{\prime}_{1},p^{\prime}_{2}$. This
implies that $x\in\alpha(x_{1})$ and $x\in\alpha(x_{2})$ which contradicts our
assumption that $\alpha$ is copyless. Consequently, we conclude that the pair
of inclusions $z_{1}\in\mathcal{G}(p_{1},\alpha(x_{1}),f,g)(y_{1})$ and
$z_{2}\in\mathcal{G}(p_{2},\alpha(x_{2}),f,g)(y_{2})$ imply that
$z_{1}\not\overset{\scriptscriptstyle{X}}{\sim}z_{2}$. ∎

######  Lemma 6.

For any state $(q,f,g)\in R$, copyless assignment $\alpha:X\to\langle
X,\Sigma_{2}\rangle$, variable $z\in Z$, and $(p,x,y)\in P\times X\times Y$ it
holds that $\left|\mathcal{G}(p,\alpha(x),f,g)(y)\right|_{z}\leq 1$.

###### Proof.

We proceed by induction on $\alpha(x)$.

Base case.

$\left|\mathcal{G}(p,\varepsilon,f,g)\right|_{z}\leq 1$.

By definition of $\mathcal{G}$, in eq. 2, it follows that
$\mathcal{G}(p,\varepsilon,f,g)(y)=y$ when $\alpha(x)=\varepsilon$. Since no
variables from $Z$ ever occur in such a string,
$\left|\mathcal{G}(p,\varepsilon,f,g)(y)\right|_{z}=0\leq 1$.

Inductive case.

_If $\left|\mathcal{G}(p,\vec{x},f,g)(y)\right|_{z}\leq 1$ and either
$\alpha(x)=\vec{x}s$ or $\alpha(x)=\vec{x}x^{\prime}$, then
$\left|\mathcal{G}(p,\alpha(x),f,g)(y)\right|_{z}\leq 1$._

In the case that $\alpha(x)=\vec{x}s$, by applying the definition of
$\mathcal{G}$ we obtain the equation
$\mathcal{G}(p,\alpha(x),f,g)=\mathcal{G}(p,\vec{x},f,g)\circ\beta$, where
$(\mathcal{F}(p,\vec{x},f),s,\beta,p^{\prime})\in\Delta_{23}$. Since the type
of $\beta$ is $Y\to\langle Y,\Sigma_{3}\rangle$, composing this assignment
with $\mathcal{G}(p,\vec{x},f,g)$ does not introduce or remove any $Z$
variables from the resulting strings, we get

$\left|\mathcal{G}(p,\vec{x}s,f,g)(y)\right|_{z}=\left|\mathcal{G}(p,\vec{x},f,g)\circ\beta(y)\right|_{z}=\left|\mathcal{G}(p,\vec{x},f,g)(y)\right|_{z}.$
(18)

Assuming the inductive hypothesis, we have
$\left|\mathcal{G}(p,\vec{x},f,g)(y)\right|_{z}\leq 1$, which, in combination
with eq. 18, implies the desired inequality:
$\left|\mathcal{G}(p,\vec{x}s,f,g)(y)\right|_{z}\leq 1$.

Otherwise, $\alpha(x)=\vec{x}x^{\prime}$ and applying the definition of
$\mathcal{G}$ yields the functional equation:

$\mathcal{G}(p,\beta(x),f,g)=\mathcal{G}(p,\vec{x},f,g)\circ
g(\mathcal{F}(p,\vec{x},f),x^{\prime},\cdot).$

By assumption, we know that
$\left|\mathcal{G}(p,\vec{x},f,g)(y)\right|_{z}\leq 1$, and, applying lemma 4,
we obtain the inequality
$\left|g(\mathcal{F}(p,\vec{x},f),x^{\prime},y)\right|_{z}\leq 1$. However,
$z\in\mathcal{G}(p,\vec{x},f,g)(y)$ and $z\in
g(\mathcal{F}(p,\vec{x},f),x^{\prime})(y)$ cannot hold simultaneously, since
this would imply that $\left|\alpha(x)\right|_{x^{\prime}}=2$ thereby
contradicting the assumption that $\alpha$ is copyless. This mutual
exclusivity may be restated quantitatively as
$\left|\mathcal{G}(p,\vec{x},f,g)(y)\right|_{z}+\left|g(\mathcal{F}(p,\vec{x},f),x^{\prime},y)\right|_{z}\leq
1$, implying $\left|\mathcal{G}(p,\vec{x}x^{\prime},f,g)(y)\right|_{z}\leq 1$.

∎

######  Lemma 7.

For any state $(q,f,g)\in R$, copyless assignment $\alpha:X\to\langle
X,\Sigma_{2}\rangle$, variable $z\in Z$, and $(p,x)\in P\times X$, it holds
that $\sum_{Y}\left|\mathcal{G}(p,\alpha(x),f,g)(y)\right|_{z}\leq 1$.

###### Proof.

Suppose that $(q,s,\alpha,q^{\prime})\in\Delta_{12}$ is the corresponding
transition in $T_{12}$. If both the inclusions
$z\in\mathcal{G}(p,\alpha(x),f,g)(y_{1})$ and
$z\in\mathcal{G}(p,\alpha(x),f,g)(y_{2})$ hold, then there must exist
$\vec{x},\vec{x}^{\prime}\in(X\cup\Sigma_{2})^{*}$ and $x^{\prime}\in X$ such
that $\vec{x}x^{\prime}\vec{x}^{\prime}=\alpha(x)$ and $z\in
g(\mathcal{F}(p,\vec{x},f),x^{\prime},y_{3})$, for some variable $y_{3}$,
occurring both $\mathcal{G}(p,\vec{x},f,g)(y_{1})$ and
$\mathcal{G}(p,\vec{x},f,g)(y_{2})$. However, we know that compositions of
copyless assignments, such as $\mathcal{G}(p,\vec{x},f,g)$, remain copyless.
Thus, if $y_{3}\in\mathcal{G}(p,\vec{x},f,g)(y_{1})$ and
$y_{3}\in\mathcal{G}(p,\vec{x},f,g)(y_{2})$ both hold, there must exist a
copyful assignment in $T_{23}$. This contradicts our initial assumption that
$T_{23}$ is copyless, so we infer that a single variable $z$ cannot occur in
more than one element of the set $\left\\{\mathcal{G}(p,\alpha(x),f,g)(y):y\in
Y\right\\}$. This fact, in combination with lemma 6, which asserts that $z$
can occur at most once in any element of this set, allows us to conclude that
$\sum_{y\in Y}\left|\mathcal{G}(p,\alpha(x),f,g)(y)\right|_{z}\leq 1$. ∎

######  Lemma 8.

Consider $z\in Z$ and $\alpha:X\to\langle X,\Sigma_{2}\rangle$. If
$z\in\mathcal{G}(p_{1},\alpha(x_{1}),f,g)(y_{1})$ and
$z\in\mathcal{G}(p_{2},\alpha(x_{2}),f,g)(y_{2})$, then $x_{1}=x_{2}$ and
either (i) $p_{1}=p_{2}$ and $y_{1}=y_{2}$ or (ii) $p_{1}\neq p_{2}$.

###### Proof.

Since $z\overset{\scriptscriptstyle{X}}{\sim}z$, lemma 5 implies that
$x_{1}=x_{2}$. This leaves two cases.

  1. 1.

First, suppose that $p_{1}=p_{2}$. If $y_{1}\neq y_{2}$, then we have that
$z\in\mathcal{G}(p,\alpha(x),f,g)(y_{1})$ and
$z\in\mathcal{G}(p,\alpha(x),f,g)(y_{2})$. It implies that
$\left|\mathcal{G}(p,\alpha(x),f,g)(y_{1})\right|_{z}+\left|\mathcal{G}(p,\alpha(x),f,g)(y_{2})\right|_{z}=2$
and therefore contradicts lemma 7, so $p_{1}=p_{2}$ implies $y_{1}=y_{2}$.

  2. 2.

Otherwise $p_{1}\neq p_{2}$. If $y_{1}=y_{2}$, then
$z\in\mathcal{G}(p_{1},\alpha(x),f,g)(y)$ and
$z\in\mathcal{G}(p_{2},\alpha(x),f,g)(y)$. If $y_{1}\neq y_{2}$, then
$z\in\mathcal{G}(p_{1},\alpha(x),f,g)(y_{2})$ and
$z\in\mathcal{G}(p_{2},\alpha(x),f,g)(y_{1})$.

Neither possibility raises a contradiction, so either may hold when $p_{1}\neq
p_{2}$. ∎

######  Lemma 9.

For any $\gamma:Z\to\langle Z,\Sigma_{3}\rangle$ and $z,z_{1},z_{2}\in Z$, if
$z\in\gamma(z_{1})$ and $z\in\gamma(z_{2})$, then
$z_{1}\overset{\scriptscriptstyle{X}}{\sim}z_{2}$ and either (i) $z_{1}=z_{2}$
or (ii) $z_{1}\not\equiv z_{2}$.

###### Proof.

If $z\in\gamma(z_{1})$ and $z\in\gamma(z_{2})$, then there exist pairs
$(p_{1},x_{1})$ and $(p_{2},x_{2})$ such that we have the inclusions
$z\in\mathcal{A}^{p_{1}}_{x_{1}}(\mathcal{G}(p_{1},\alpha(x_{1}),f,g))(z_{1})$
and
$z\in\mathcal{A}^{p_{2}}_{x_{2}}(\mathcal{G}(p_{2},\alpha(x_{2}),f,g))(z_{2})$.
From eq. 4, it follows that if these inclusions hold, then so do the
inclusions $z\in\mathcal{G}(p_{1},\alpha(x_{1}),f,g)(y_{1})$ and
$z\in\mathcal{G}(p_{2},\alpha(x_{2}),f,g)(y_{2})$, for some $y_{1},y_{2}\in
Y$. Now, lemma 8 entails that either $x_{1}=x_{2}$, $p_{1}=p_{2}$,
$y_{1}=y_{2}$, or $x_{1}=x_{2}$ and $p_{1}\neq p_{2}$. In either case,
$z_{1}\overset{\scriptscriptstyle{X}}{\sim}z_{2}$. In the former case, we have
equality of the states and $Y$ variables, which, in combination with lemma 7,
implies $z_{1}=z_{2}$. In the latter case, $z_{1}$ and $z_{2}$ are not indexed
by the same state, so $z_{1}\not\equiv z_{2}$. ∎

######  Lemma 10.

For $\gamma:Z\to\langle Z,\Sigma_{3}\rangle$, if $z_{1}\in\gamma(z)$ and
$z_{2}\in\gamma(z)$, then $z_{1}\equiv z_{2}$ or
$z_{1}\not\overset{\scriptscriptstyle{X}}{\sim}z_{2}$.

###### Proof.

If $z_{1},z_{2}\in\gamma(z)$, then
$z_{1},z_{2}\in\mathcal{G}(p,\alpha(x),f,g)(y)$ for some $y$. Both variables
must be introduced by a shape summary constructed by
$\mathcal{G}(p,\alpha(x),f,g)$. This yields two cases: (1) both variables
belong to a summary mapping $g^{p^{\prime}}_{x^{\prime}}$ with common
parameters from $P$ and $X$, or (2) each variable belongs to summary mappings
$g^{p_{1}}_{x_{1}}$ and $g^{p_{2}}_{x_{2}}$ with distinct parameters. When
$z_{1},z_{2}$ both occur in some element of $\bigcup_{y\in
Y}g(p^{\prime},x^{\prime},y)$, then $z_{1}\equiv z_{2}$ by lemma 4. Otherwise,
when $z_{1}$ occurs in an element of $\bigcup_{y\in Y}g(p_{1},x_{1},y)$ and
$z_{2}$ occurs in some element of $\bigcup_{y\in Y}g(p_{2},x_{2},y)$, it must
hold that $x_{1}\neq x_{2}$ because $\alpha$ is copyless. Since the $Z$
variables in question cannot be indexed by the same $X$ variable, we conclude
that $z_{1}\not\overset{\scriptscriptstyle{X}}{\sim}z_{2}$. ∎

Lemmas 10 and 9 imply that any pair of copies of a single variable never occur
in a common variable later in the computation. Therefore, it is impossible for
a diamond to occur in any graph of a run in $T_{13}$, completing our key
observation.

######  Theorem 2.

$T_{13}$ is diamond-free.

##  4 Removing Copies from Diamond-Free NSSTs

In this section, we show that diamond-free NSSTs are equivalently expressive
to copyless NSSTs and provide a procedure that produces an equivalent copyless
NSST when given a diamond-free NSST. As a corollary, we establish a semantic-
preserving transformation between the class of diamond-free DSSTs and copyless
functional NSSTs. The SST $T_{3}$ from fig. 2, also displayed in fig. 8 along
with the graphs of its assignments, will be used as a running example to
illustrate the argument.

$r_{0}$start$r_{1}$$a\mid\gamma^{1}$$a\mid\gamma^{2}$$z_{1}z_{2}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$G(\gamma^{1})$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$G(\gamma^{2})$
Figure 8: The SST $T_{3}$ from fig. 2 (left) and graphs of each assignment
(right).

#### Assignment Decomposition.

The first portion of the conversion procedure involves decomposing each
copyful assignment $\alpha$ in the given diamond-free NSST into a collection
of copyless assignments that “cover” $\alpha$ in the sense that the union of
these copyless mappings coincides exactly with the mapping $\alpha$. This
decomposition subroutine—Decompose—is given in algorithm 1. Figure 9 provides
an illustration of the algorithm Decompose applied to the copyful assignment
$\gamma^{2}$ of $T_{3}$. Henceforth, let $\mathcal{D}$ be used to denote the
mapping $\alpha\mapsto\textup{{Decompose}}(\alpha,\emptyset)$.

1

2

3function  _Decompose(_$\alpha,D$_)_

4 if $\alpha$ is copyless then

5 return $D\cup\left\\{\alpha\right\\}$

6 Choose $x\in X$ with distinct $y,z\in X$ such that $x\in\alpha(y)$ and
$x\in\alpha(z)$

7 foreach $y\in X$ such that $x\in\alpha(y)$ do

8 foreach $z\in X\setminus\left\\{y\right\\}$ such that $x\in\alpha(z)$ do

9 $\beta\leftarrow\alpha$

10 $\beta(z)\leftarrow\varepsilon$

11 if $\beta$ is copyless then

12 $D\leftarrow D\cup\left\\{\beta\right\\}$

13 else

14 $D\leftarrow D$ $\cup$ Decompose(_$\beta,D$_)

15 return $D$

16

Algorithm 1 Decompose copyful assignment into collection of copyless
assignments.

$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$G(\gamma^{2})$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$G(\gamma^{2}_{1})$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$G(\gamma^{2}_{2})$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$G(\gamma^{2}_{3})$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$z_{1}$$z_{2}$$z_{3}$$z_{4}$$G(\gamma^{2}_{4})$

Figure 9: An illustration of Decompose applied to the copyful assignment
$\gamma^{2}$ of $T_{3}$.

######  Lemma 11.

If $\alpha$ is diamond-free and $\alpha^{\prime}\in\mathcal{D}(\alpha)$, then
$\alpha^{\prime}$ is copyless and
$\alpha=\bigcup_{\alpha^{\prime}\in\mathcal{D}(\alpha)}\alpha^{\prime}$.

###### Proof.

Each $\alpha_{k}$ being copyless follows from the fact that
$\textup{{Decompose}}(\alpha,D)$ is called with $D$ initially set to
$\emptyset$ and the conditionals at lines 1 and 1 of algorithm 1 ensure only
copyless assignments are added to $D$. If the conditional at line 1 is entered
then $\left\\{\alpha\right\\}$ is returned and $\alpha=\alpha$, thus
satisfying the second assertion of the lemma. Otherwise a variable $x$ is
selected such that $x$ is copied by $\alpha$. The subsequent loop iterates
through the possible target variables of for $x$, fixes one such $y$ at each
iteration, creates a new assignment $\beta$ as a identical copy of $\alpha$,
and then deletes $\beta(z)$ for all other variables $z$ such that
$x\in\alpha(z)$. Thus, every mapping in the assignment $\alpha$ is present in
$\beta$ for at least one iteration of the loop. Furthermore, this process
either adds each $\beta$ into $D$ or recurses with $\beta$ as a parameter. The
former guarantees that at least one assignment in $D$ includes any given
mapping from $\alpha$. In the latter case, a mapping will not be removed later
on, since the variable $x$ will no longer be copied in any of the assignments
$\beta$ passed recursively to Decompose. Therefore, every mapping present in
$\alpha$ occurs in some assignment in the decomposition $D$, so
$\alpha=\bigcup^{n}_{k=1}\alpha_{k}$. ∎

######  Definition 3 (Diamond-Free $\to$ Copyless).

If $T=(\Sigma,\Omega,Q,q_{0},X,A,\Delta,F)$ is a diamond-free NSST, then
$T^{\prime}=(\Sigma,\Omega,Q^{\prime},q^{\prime}_{0},X,A^{\prime},\Delta^{\prime},F^{\prime})$
is an equivalent copyless NSST where

  * •

$Q^{\prime}=Q\times 2^{X}$ and $q^{\prime}_{0}=(q_{0},\emptyset)$,

  * •

$A^{\prime}=\bigcup_{\alpha\in A}\mathcal{D}(\alpha)$,

  * •

$((p,Y),s,\beta,(q,Z))\in\Delta^{\prime}$ iff

    * –

there does not exist any pair $x,y\in X$ such that $y\in Y$ and $y\in\beta(x)$
and

    * –

there exists $(p,s,\alpha,q)\in\Delta$ such that (i)
$\beta\in\mathcal{D}(\alpha)$ and (ii) $y\in Z$ iff there exists $x\in X$ such
that $x\in\alpha(y)$ and $x\notin\beta(y)$,

  * •

$F^{\prime}((q,Y))=\begin{cases}\bot&\textup{if there exists }x\in Y\textup{
such that }x\in F(q)\\\ F(q)&\textup{otherwise.}\end{cases}$

$r_{0},\emptyset$start$r_{1},\emptyset$$r_{1},\left\\{z_{3},z_{4}\right\\}$$r_{1},\left\\{z_{2},z_{3}\right\\}$$r_{1},\left\\{z_{1},z_{4}\right\\}$$r_{1},\left\\{z_{1},z_{2}\right\\}$$a\mid\gamma^{1}$$a\mid\gamma^{2}_{1}$$a\mid\gamma^{2}_{2}$$a\mid\gamma^{2}_{3}$$a\mid\gamma^{2}_{4}$$a\mid\gamma^{2}_{4}$$a\mid\gamma^{2}_{1}$$a\mid\gamma^{2}_{2}$$a\mid\gamma^{2}_{3}$$z_{1}z_{2}$$z_{1}z_{2}$
Figure 10: A copyless functional NSST equivalent to $T_{3}$ from fig. 2 and
constructed according to definition 3. Note that we omit a number of
irrelevant states from the diagram.

In the sequel, suppose that $T=(\Sigma,\Omega,Q,q_{0},X,A,\Delta,F)$ is a
diamond-free NSST. Additionally suppose that
$T^{\prime}=(\Sigma,\Omega,Q^{\prime},q^{\prime}_{0},X,A^{\prime},\Delta^{\prime},F^{\prime})$
is the copyless NSST constructed according to definition 3. Let $\rho$ be an
arbitrary run
$q_{0}\xrightarrow{w_{1},\alpha_{1}}\ldots\xrightarrow{w_{n},\alpha_{n}}q_{n}$
in $T$, and let $\mathcal{R}(\rho)$ bet the set of all runs of the form
$(q_{0},\emptyset)\xrightarrow{w_{1},\beta_{1}}\ldots\xrightarrow{w_{n},\beta_{n}}(q_{n},Y_{n})$
in $T^{\prime}$ where
$((q_{k-1},Y_{k-1}),w_{k},\beta_{k},(q_{k},Y_{k}))\in\Delta^{\prime}$, for all
$1\leq k\leq n$.

######  Lemma 12.

$\mathcal{V}_{\rho}=\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\mathcal{V}_{\rho^{\prime}}$

###### Proof.

We proceed by induction on the run $\rho$.

Base case.

_$\rho$ is the empty run._

In this case, $\mathcal{R}(\rho)$ is a singleton set containing the empty run
and thus
$\mathcal{V}_{\rho}=\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\mathcal{V}_{\rho^{\prime}}$.

Inductive case.

_$\sigma=\rho\xrightarrow{s,\alpha}r$ is a run in $T$ on $ws$ and
$\mathcal{V}_{\rho}=\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\mathcal{V}_{\rho^{\prime}}$._

The valuation for $\sigma$ in $T$ may be written as
$\mathcal{V}_{\sigma}=\mathcal{V}_{\rho}\circ\alpha$, and
$\mathcal{R}(\sigma)$ may be written as

$\mathcal{R}(\sigma)=\bigcup_{\beta\in\mathcal{D}(\alpha)}\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\left\\{\rho^{\prime}\xrightarrow{s,\beta}(r,Z):((q_{n},Y_{n}),s,\alpha,(r,Z))\in\Delta^{\prime}\right\\}.$

As a result, we have that
$\bigcup_{\sigma^{\prime}\in\mathcal{R}(\sigma)}\mathcal{V}_{\sigma^{\prime}}=\bigcup_{\beta\in\mathcal{D}(\alpha)}\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\mathcal{V}_{\rho^{\prime}}\circ\beta$.
Applying the inductive hypothesis and lemma 11 to this equation, we obtain the
desired equivalence:

$\bigcup_{\sigma^{\prime}\in\mathcal{R}(\sigma)}\mathcal{V}_{\sigma^{\prime}}=\bigcup_{\beta\in\mathcal{D}(\alpha)}\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\mathcal{V}_{\rho^{\prime}}\circ\beta=\bigcup_{\beta\in\mathcal{D}(\alpha)}\mathcal{V}_{\rho}\circ\beta=\mathcal{V}_{\rho}\circ\bigcup_{\beta\in\mathcal{D}(\alpha)}\beta=\mathcal{V}_{\rho}\circ\alpha=\mathcal{V}_{\sigma}.$

∎

######  Lemma 13.

If $(w,w^{\prime})\in[\\![{T}]\\!]$, then
$(w,w^{\prime})\in[\\![{T^{\prime}}]\\!]$.

###### Proof.

Assuming $(w,w^{\prime})\in[\\![{T}]\\!]$, then there must be a run
$\rho=q_{0}\xrightarrow{w_{1},\alpha_{1}}\ldots\xrightarrow{w_{n},\alpha_{n}}q_{n}$
in $T$ on $w$ such that $\textup{Er}_{X}\circ\mathcal{V}_{\rho}\circ
F(q_{n})=w^{\prime}$. By lemma 12, it holds that
$\textup{Er}_{X}\circ\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\mathcal{V}_{\rho^{\prime}}\circ
F(q_{n})=w^{\prime}$, and, by definition 3, it holds that
$\textup{Er}_{X}\circ\bigcup_{\rho^{\prime}\in\mathcal{R}(\rho)}\mathcal{V}_{\rho^{\prime}}\circ
F^{\prime}((q_{n},Y_{n}))=w^{\prime}$ for any $Y_{n}\subseteq X$ such that
there is no variable $x$ occurring both in $Y_{n}$ and in $F(q_{n})$. Each run
in $\mathcal{R}(\rho)$ corresponds to a nondeterministic choice resolving
which copies induced by assignments in $\rho$ will be used later in the
computation. Since each assignment in $\rho$ is diamond-free, no two copies
can be combined in a later assignment, and thus there at least one run in
$\mathcal{R}(\rho)$ corresponding to the appropriate choice of copies for
simulating $\rho$. Therefore, $(w,w^{\prime})\in[\\![{T}]\\!]$ implies
$(w,w^{\prime})\in[\\![{T^{\prime}}]\\!]$. ∎

######  Lemma 14.

If $(w,w^{\prime})\in[\\![{T^{\prime}}]\\!]$, then
$(w,w^{\prime})\in[\\![{T}]\\!]$.

###### Proof.

Assuming $(w,w^{\prime})\in[\\![{T^{\prime}}]\\!]$, there exists a run
$\rho^{\prime}=(q_{0},\emptyset)\xrightarrow{w_{1},\beta_{1}}\ldots\xrightarrow{w_{n},\beta_{n}}(q_{n},Y_{n})$
in $T^{\prime}$ on $w$ such that
$\textup{Er}_{X}\circ\mathcal{V}_{\rho^{\prime}}\circ
F^{\prime}((q_{n},Y_{n}))=w^{\prime}$. By definition 3, there exists
$(q_{k-1},w_{k},\alpha_{k},q_{k})\in\Delta$, for each transition
$((q_{k-1},Y_{k-1}),w_{k},\beta_{k},(q_{k},Y_{k}))\in\Delta^{\prime}$
occurring in $\rho^{\prime}$, such that (i)
$\beta_{k}\in\mathcal{D}(\alpha_{k})$ and (ii) $y\in Y_{k}$ iff there exists
$x\in X$ such that $x\in\alpha_{k}(y)$ and $x\notin\beta_{k}(y)$. Therefore,
we may construct the run
$\rho=q_{0}\xrightarrow{w_{1},\alpha_{1}}\ldots\xrightarrow{w_{n},\alpha_{n}}q_{n}$
for which $\rho^{\prime}\in\mathcal{R}(\rho)$ by stringing together these
transitions from $\Delta$. This shows that every accepting run $\rho^{\prime}$
in $T^{\prime}$ on $w$ has a corresponding accepting run $\rho$ in $T$ on $w$
such that $\mathcal{V}_{\rho}\circ F(q_{n})=\mathcal{V}_{\rho^{\prime}}\circ
F^{\prime}((q_{n},Y_{n}))$. Hence, $(w,w^{\prime})\in[\\![{T^{\prime}}]\\!]$
implies $(w,w^{\prime})\in[\\![{T}]\\!]$. ∎

######  Theorem 3.

Every diamond-free NSST with $n$ states and $m$ variables is equivalent to a
copyless NSST with $n2^{m}$ states and $m$ variables.

###### Proof.

Equivalence of $[\\![{T}]\\!]$ and $[\\![{T^{\prime}}]\\!]$ follows
immediately from the conjunction of lemmas 13 and 14. The number of states and
variables in $T^{\prime}$ is clear from definition 3. ∎

Combining theorem 3 with theorem 3.5 of Alur and Deshmukh [3], which states
that every functional NSST is equivalent to a DSST, we obtain the following
corollary.

######  Corollary 1.

Every diamond-free DSST is equivalent to a copyless DSST.

##  5 Conclusion

This paper revisits the constructions for the sequential composition of
copyless streaming string transducers developed by Alur and Cerný [1], Alur
and Deshmukh [3]. While those constructions result in a copyful transducer in
general, we showed that these composite transducers exhibit only the tamest of
copyful behavior. As a characterization, we defined diamond-free SSTs and
proved that the composite transducer is always an element of this subclass of
copyful SSTs. Moreover, we showed that diamond-free SSTs are no more powerful
than copyless SSTs. To achieve this, we formulated a method for transforming
any diamond-free SST into an equivalent copyless SST. The composition
construction followed by the conversion from diamond-free to copyless SSTs
comprise a complete and direct procedure for composing copyless SSTs.

## References

  * Alur and Cerný [2010] Rajeev Alur and Pavol Cerný.  Expressiveness of streaming string transducers.  In _International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)_ , LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010.  URL https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1.
  * Alur and Cerný [2011] Rajeev Alur and Pavol Cerný.  Streaming transducers for algorithmic verification of single-pass list-processing programs.  In _Symposium on Principles of Programming Languages (POPL)_. ACM, 2011.  URL https://doi.org/10.1145/1926385.1926454.
  * Alur and Deshmukh [2011a] Rajeev Alur and Jyotirmoy V. Deshmukh.  Nondeterministic streaming string transducers.  In _International Colloquium on Automata, Languages and Programming (ICALP (2))_ , LNCS. Springer, 2011a.  URL https://doi.org/10.1007/978-3-642-22012-8_1.
  * Alur and Deshmukh [2011b] Rajeev Alur and Jyotirmoy V. Deshmukh.  Nondeterministic streaming string transducers.  Departmental papers (CIS), Department of Computer & Information Science, University of Pennsylvania, 2011b.  URL https://repository.upenn.edu/cgi/viewcontent.cgi?article=1607&context=cis_papers.
  * Alur et al. [2012] Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi.  Regular transformations of infinite strings.  In _LICS_. IEEE Computer Society, 2012.  URL https://doi.org/10.1109/LICS.2012.18.
  * Courcelle and Engelfriet [2012] Bruno Courcelle and Joost Engelfriet.  _Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach_.  Cambridge University Press, New York, USA, 2012.
  * Dave et al. [2021] Vrunda Dave, Taylor Dohmen, Shankara Narayanan Krishna, and Ashutosh Trivedi.  Regular model checking with regular relations.  In _Fundamentals of Computation Theory - 23rd International Symposium, FCT_ , volume 12867 of _Lecture Notes in Computer Science_ , pages 190–203. Springer, 2021.  URL https://doi.org/10.1007/978-3-030-86593-1_13.
  * Filiot and Reynier [2017] Emmanuel Filiot and Pierre-Alain Reynier.  Copyful streaming string transducers.  In _Reachability Problems RP_ , volume 10506 of _Lecture Notes in Computer Science_ , pages 75–86. Springer, 2017.  URL https://doi.org/10.1007/978-3-319-67089-8_6.
  * Filiot and Reynier [2021] Emmanuel Filiot and Pierre-Alain Reynier.  Copyful streaming string transducers.  _Fundam. Informaticae_ , 178(1-2):59–76, 2021\.  URL https://doi.org/10.3233/FI-2021-1998.
  * Lopez et al. [2019] Théodore Lopez, Benjamin Monmege, and Jean-Marc Talbot.  Determinisation of finitely-ambiguous copyless cost register automata.  In _44th International Symposium on Mathematical Foundations of Computer Science, MFCS_ , volume 138 of _LIPIcs_ , pages 75:1–75:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  URL https://doi.org/10.4230/LIPIcs.MFCS.2019.75.
  * Meyer [1975] Albert R Meyer.  Weak monadic second order theory of succesor is not elementary-recursive.  In _Logic colloquium_ , pages 132–154. Springer, 1975.
  * Muscholl and Puppis [2019] Anca Muscholl and Gabriele Puppis.  Equivalence of finite-valued streaming string transducers is decidable.  In _46th International Colloquium on Automata, Languages, and Programming, ICALP_ , volume 132 of _LIPIcs_ , pages 122:1–122:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  URL https://doi.org/10.4230/LIPIcs.ICALP.2019.122.
  * Thakkar et al. [2013] Jay Thakkar, Aditya Kanade, and Rajeev Alur.  Transducer-based algorithmic verification of retransmission protocols over noisy channels.  In _Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS/FORTE_ , volume 7892 of _Lecture Notes in Computer Science_ , pages 209–224. Springer, 2013.  URL https://doi.org/10.1007/978-3-642-38592-6_15.