Graphical Language with Delayed Trace:
Picturing Quantum Computing with Finite Memory
Titouan Carette
Université de Lorraine,
CNRS, Inria, LORIA
F 54000 Nancy, France
Email<EMAIL_ADDRESS>Marc de Visme
Université de Lorraine,
CNRS, Inria, LORIA
F 54000 Nancy, France
Email<EMAIL_ADDRESS>Simon Perdrix
Université de Lorraine,
CNRS, Inria, LORIA
F 54000 Nancy, France
Email<EMAIL_ADDRESS>
Graphical languages, like quantum circuits or ZX-calculus, have been successfully designed to represent (memoryless) quantum computations acting on a finite number of qubits. Meanwhile, delayed traces have been used as a graphical way to represent finite-memory computations on streams, in a classical setting (cartesian data types). We merge those two approaches and describe a general construction that extends any graphical language, equipped with a notion of discarding, to a graphical language of finite memory computations. In order to handle cases like the ZX-calculus, which is complete for post-selected quantum mechanics, we extend the delayed trace formalism beyond the causal case, refining the notion of causality for stream transformers. We design a stream semantics based on stateful morphism sequences and, under some assumptions, show universality and completeness results. Finally, we investigate the links of our framework with previous works on cartesian data types, signal flow graphs, and quantum channels with memories.

§ INTRODUCTION

Motivations. Several graphical languages have been successfully developed for representing finite-dimensional quantum processes. The quantum circuits and the ZX-calculus are the main  examples of such graphical languages. The ZX-calculus is equipped with a complete equational theory [1, 2], that allows, among other applications,
to perform circuit optimization [3, 4], and to design fault tolerant computations [5, 6].
These graphical languages have been designed for finite-dimensional quantum mechanics: each wire represents a finite system – generally a qubit – as a consequence, a finite diagram can only represent a finite-dimensional quantum evolution. Notice that using the scalable construction [7], one can represent finite registers, with the possibility to split and merge  registers. This construction makes the representation more compact but it remains a representation of finite-dimensional quantum computations.
There is a fundamental reason for this restriction: finite-dimensional Hilbert spaces, contrary to infinite-dimensional ones, form a compact closed category, and the compact closure is the cornerstone of graphical languages like the ZX-calculus.

To go beyond finite registers, we explore in this paper the design of graphical languages for quantum stream transformations, i.e., computations taking (infinite) sequences of quantum inputs to (infinite) sequences of quantum outputs. Intuitively a transformation acting on a stream of qubits, inputs a qubit and outputs a qubit at each clock tick. In order to allow interactions between systems input at distinct clock ticks, a memory mechanism is required to store some data across the ticks. Such a quantum transformation is called a  quantum channel with memory in [8].

We choose to graphically represent  the memory mechanism using delayed traces, i.e., feedback loops that  store qubits from clock tick to the next. The example in Fig. <ref> consists in applying a CNot gate on consecutive qubits of a stream.

$\tikzfig{CNot-casc}\qquad \qquad\tikzfig{cnc-intro}$
Left: A cascade of CNots on a stream of qubits. At the first tick, a CNot is applied: the control qubit is in the $\ket 0$ state, the target qubit is the first qubit of the input stream. The control qubit is then output and the target qubit stored in the memory. At the second tick the stored qubit becomes the control qubit and the second qubit of the input stream becomes the target qubit and so on. Right: An informal unfolded version of the cascade of CNots.

Delayed traces have been studied [9] as a construction which can be applied to any cartesian category. We explore the extension of this construction to the quantum case, since a quantum graphical language, from a category point of view, form a category which is symmetric monoidal but not cartesian.

Depicting finite memory quantum computations on streams does not provide a universal model of quantum computation. It is however an interesting  fragment to explore, strictly more expressive than memory-free languages designed for finite registers, and an intermediate scale model potentially easier to implement using quantum technologies available in the short term, than a universal quantum computer.

We introduce a general construction that extends any (not necessarily quantum) graphical language $\G$ equipped with a discarding map, to a graphical language $\Stream$ with finite memory acting on streams. The construction consists in adding a delayed trace to model the memory, as well as stream constructors and destructors.

A key property of the construction is that the delay only commutes with causal transformations. Indeed, applying a non-causal transformation before storing a system can produce some side effect on the output at tick $k$ which would occur only at tick $k+1$ if the transformation is applied later on. Moreover, the infinite nature of the computation requires the introduction of a coinduction principle, to show for instance that storing forever a system in a memory and never using it, is equivalent to discard this system right away.

We introduce the finite approximations of a $\Stream$-diagram $D$ as a sequence of $\G$-diagrams: the $k^\text{th}$ diagram of the sequence represents the behavior of $D$ from the initial  to the $k^\text{th}$
tick. The semantics of a $\Stream$-diagram is then defined as the sequence of interpretations of its finite approximations.

When an evolution is causal,
its $k^\text{th}$ approximation can be obtained from the $(k+1)^\text{th}$ approximation by discarding the last outputs. This property witnesses the fact that the state of the first $k$  outputs should only depends on the first $k$  inputs. This is however not the case with non-causal evolutions, and in particular post-selected quantum evolutions (i.e., quantum evolutions where one can freely choose the classical outcomes of the measurements). Post-selected evolutions can be represented in several graphical languages including the ZX-calculus. As a consequence, we introduce a new monotonicity condition for finite approximations.

The monotonicity conditions allow us to identify the finite approximations that can be represented in $\Stream$. In particular, these evolutions should satisfy some additional regularity condition, which corresponds to the fact that they can be implemented with a finite memory.
Finally, we also show the completeness of the language, up to some additional assumptions which are satisfied in the quantum case.

Related works.
In [9], a delayed trace construction is introduced for the classical case (cartesian data type), we extend the construction to the non-cartesian case. Moreover we axiomatize, using a graphical language, the delayed trace construction.
A categorical formulation of delayed traces as infinite combs has also been proposed by [10] but again, only in the cartesian or semi-cartesian case.

In categorical quantum mechanics, $!$-boxes [11] and the scalable construction [7] can be used to represent an infinite family of diagrams at once, and thus a computation acting on a finite but unbounded number of qubits. There is however no notion of stream or memory.
Since infinite-dimensional Hilbert spaces are not compact closed there are few attempts of graphical languages in infinite dimensions [12, 13] –
notice the work of [14] based on non-standard analysis. Nevertheless, our construction  preserves  compact structures. There is no contradiction here, our scalars are not complex numbers but sequences of complex numbers. Thus, the relevant way to interpret our construction in the categorical quantum mechanic setting would be to consider $\mathbb{C}^\mathbb{N}$-modules instead of infinite-dimensionalal vector spaces over $\mathbb{C}$.

In quantum computing, quantum channels with memory and quantum cellular automata [15, 16] are examples of computational models with an infinite number of qubits. Notice that typical results in this field are structure theorems which  state for instance that if an evolution is translation invariant and causal then it can be decomposed into a series of local operations. In section <ref>, we discuss the connection between the structure theorem of [8] and the diagrams of $\Stream$.

Delayed traces as been used in [17] to axiomatize rational streams. They rely heavily on the properties of linear streams providing a semantics in terms of formal Laurent series. This is the only example we know of previous works on delayed trace in the compact closed, hence non-semi-cartesian, setting. We discuss the links with our formalism in <ref>.

Structure of the paper.
We present in Section II some preliminaries on quantum computation, describing how quantum states are represented and the preexisting graphical language of quantum circuits. We then explore the different notions that naturally arise when we add memory to quantum circuits.

In Section III, we rely on the intuitions coming from the quantum case and work at a much greater level of generality: for every graphical language $\G$, we define the graphical language $\Stream$ which manipulates both single inputs and streams of inputs, and allows for the storage of information through time.

While diagrams of $\Stream$ are finite, we study in Section IV their infinite unfoldings into stateful morphism sequences [9], and show an equivalence between those sequences that are ultimately constants, and the diagrams of $\Stream$. Those unfoldings are a major intermediate step for the definition of the semantics of diagrams of $\Stream$.

In Section V, we explain how to build a semantics for $\Stream$ from a semantics for $\G$, and show that under some reasonable assumptions, this semantics is complete, meaning that the rewriting rules of our language generate all the sound rewriting rules, and universal, meaning that the generators of our language generate all the (regular) stream processes.

At last, in Section VI, we explore the applications of the construction, in particular for the ZX-calculus. We also present a fragment of our graphical language, $\Stream_0$, which matches more closely with the preexisting works. In this fragment, one is forced to behave uniformly through time, and operations such that “changing the third element of a stream” are not possible.

All the proofs can be found in Appendix <ref>.

§ FINITE MEMORY QUANTUM COMPUTING

In this section, we review various notions of quantum computing and motivate by examples the kind of computations the language presented in the next section is designed to represent.

§.§ Completely Positive Maps

We use the density matrix formalism of finite-dimensionalal quantum mechanics over qubits, see [18] for a more complete presentation. We have a symmetric monoidal category $\CPM$ of generalized quantum processes over qubits. The objects are the sets of linear operators of the form $\mathcal{M}_{2^n\times 2^n}\left(\mathbb{C}\right)$ representing systems of $n$ qubits. The morphisms are the linear maps that are completely positive. Among those maps only the trace preserving ones correspond to real physical transformations, we write this subcategory $\UCPM$. The state of an $n$-qubit system is a  density matrix i.e. a map $\mathbb{C}\to \mathcal{M}_{2^n\times 2^n}\left(\mathbb{C}\right)$,
which is positive semi-definite Hermitian and has unit trace.
Using the Dirac notations $\ket 0 := \scalebox{0.8}{$\begin{pmatrix}
\end{pmatrix}$}$, $\ket 1:= \scalebox{0.8}{$\begin{pmatrix}
\end{pmatrix}$}$, $\bra 0  := \scalebox{1}{$\begin{pmatrix}
\end{pmatrix}$}$, and $\bra 1  := \scalebox{1}{$\begin{pmatrix}
\end{pmatrix}$}$, the two classical states of a qubit are the density matrices  $\ket0 \bra 0$ and $\ket1 \bra 1$.

The monoidal product is the tensor product of vector spaces $\mathcal{M}_{2^n\times 2^n}\left(\mathbb{C}\right)\otimes\mathcal{M}_{2^m\times 2^m}\left(\mathbb{C}\right)\simeq\mathcal{M}_{2^{n+m}\times 2^{n+m}}\left(\mathbb{C}\right)$. The symmetry maps are the exchange maps $\rho \otimes \nu \mapsto \nu \otimes \rho$. We denote $f^\dagger$ the Hermitian adjoint of a completely positive map. A map is said to be an isometry if $f^\dagger \circ f=id$.
A quantum process is said to be $\textbf{pure}$ if it is of the form $\rho \mapsto V\rho V^\dagger$ with $V\in \mathcal{M}_{2^{m}\times 2^{n}}\left(\mathbb{C}\right)$. A measurement which maps  $\rho$ to $\ket{0}\bra{0}\rho\ket{0}\bra{0}+\ket{1}\bra{1}\rho\ket{1}\bra{1}$, is an example of non-pure evolution.
In $\CPM$, we can also represent post-selected measurements, those are non-physical processes where we assert that a measurement gave a chosen outcome. For instance, choosing the  outcome $\ket{0}\bra{0}$   corresponds to the post-selected measurement
$\rho \mapsto \bra{0}\rho\ket{0}$.

Let the discard map be $\ground\df \rho \mapsto Tr(\rho)$, which corresponds to measuring a qubit and forgetting the result. A quantum evolution $f$ is causal if $\ground \circ f= \ground$. Intuitively, causal evolutions are side-effect free.

This discard map is not pure and can even be seen as the essence of all impurity in the following sense: for any completely positive map $f:A\to B$ there is a system $C$ and a pure map $p:A\to B\otimes C$ such that $f=\left(id_B\otimes\ground_C\right) \circ p$. In this situation $p$ is said to be a purification of $f$. Purifications are not unique, but they are in fact unique up to isometries:

Given two purifications $p:A\to B\otimes C$ and $p':A\to B\otimes C'$ of the same completely positive map $f:A\to B$, either there is an isometry $v:C\to C'$ such that $p'=\left(id_A \otimes v \right)\circ p$, or there is an isometry $v':C'\to C$ such that $p=\left(id_A \otimes v' \right)\circ p'$.

§.§ Quantum Gates

We represent the maps of $\UCPM$ as gates in circuits. This is an example of graphical language that will be formally defined in the next section. The composition corresponds to plugging gates and the tensor product to putting them side by side. Note that usually quantum circuits cannot represent $\CPM$ in full generality. But other graphical languages like the ZX-calculus have been designed for this. We only present a few gates, taken both from the quantum circuits and ZX-calculus, that we will use in examples.

\[\begin{array}{rclcrcl}
\tikzfig{ket0}&= & \ket{0}\bra{0} &\qquad  & \tikzfig{terre}&=& \rho \mapsto Tr(\rho)\\[0.3cm]
\tikzfig{mix-}&=&\frac{1}{2}\scalebox{0.8}{$\begin{pmatrix}
\end{pmatrix}$}&&\tikzfig{bra0}&=&\rho \mapsto \bra{0}\rho\ket{0}
\end{array}\]

The first gate takes no input and produces the pure state $\ket{0}\bra{0}$. The second is the discard map and the third produces the maximally mixed 1-qubit state. The fourth gate is the post-selected measurement selecting the outcome $\ket{0}\bra{0}$. We also have gates acting on more than one qubit:

\[\tikzfig{bellp-2} ~=~ \frac{1}{2}\scalebox{0.8}{$\begin{pmatrix}
\end{pmatrix}$}\qquad\quad \tikzfig{cswap} ~=~ \rho \otimes \nu  \mapsto \nu \otimes \rho \]

\[\tikzfig{cnot}~=~\rho\mapsto \scalebox{0.8}{$\begin{pmatrix}
\end{pmatrix}$}\rho \scalebox{0.8}{$\begin{pmatrix}
\end{pmatrix}$}\]

The first state is a Bell pair. This state is  entangled, meaning it cannot be written as the tensor product of two one-qubit states. We can even say that it is the maximally entangled state in the sense that discarding one qubit of the pair turns the other into the maximally mixed state. The swap exchanges two qubits and the CNot gate is a pure map acting as $\ket{x}\otimes \ket{y}\mapsto\ket{x}\otimes \ket{x\oplus y}$ on the computational basis. We are now ready to provide concrete examples of quantum computation with memory.

§.§ Quantum Computation with Memory

In order to go beyond quantum computation acting on a finite register of qubits, it is natural to consider streams of qubits: we consider a global clock, such that at each clock tick some qubits are input. For allowing interactions across clock ticks, like applying a CNot on two qubits input at distinct clock ticks, a memory mechanics is required to store a qubit and intuitively wait for another qubit to be available. Quantum channels with memory, introduced by Kretschmann and Werner [8],  can be informally depicted as follows:[In [8], the authors mainly consider the case of a clock without initialization, i.e., clock ticks in $\mathbb Z$ rather than $\NN_{\geq 1}$]

Thus the behavior of the computer at clock tick $k>0$ is a quantum process $f_k: A_k \otimes M_{k-1} \to B_k \otimes M_k$, with $M_0\df \mathbb{C}$. Following the terminology for such processes in the  classical case [9], we call such collection of processes
a stateful morphism sequence. We give the example of a cascade of CNots gates (see Fig. <ref>). At first clock tick the memory is initialized with $\ket{0}\bra{0}$. At each subsequent clock tick, a CNot is applied, the control qubit being the memory qubit and the target being the input qubit. Finally, the memory qubit is output and the input qubit is stored in the memory.
The corresponding stateful morphism sequence is:

In practice, one cannot access the whole infinite computation at once, but only what has been computed up to some clock tick $k$. To stop the computation of a stateful morphism at clock tick $k$, we discard the memory system $M_k$ and obtain, by plugging the memories, a process $\bigotimes\limits_{i=1}^{k} A_i \to \bigotimes\limits_{i=1}^{k} B_i$ called the finite approximation at clock tick $k$. For the cascade of CNot the sequence of finite approximations is:

cnc2   cnc3   cnc4   cnc5

$1$   $2$   $3$   $k$

A stateful morphism sequence leads to a unique sequence of finite approximations. However, two different stateful morphism sequences can have the same sequence of finite approximations, they are then said to be observationally equivalent. In Section IV, we characterize  the observationally equivalent stateful morphism sequences.

§.§ Finite Approximations and Causality

Another important question is to characterize the sequence of finite approximations that can be produced by a stateful morphism sequence. A first guess is that there are exactly the sequences for which the behavior at clock tick $k$ does not depend on what happens at the clock ticks $k'>k$. In other words, the present only depends on the past and not on the future.
More formally, given a sequence of finite approximations $(f_k)_{k>0}$ with $f_k:A_1\otimes \ldots \otimes A_k\to B_1\otimes \ldots \otimes B_k$, the condition is, for any $k>0$,

\[\tikzfig{monotone_q} \quad = \quad \tikzfig{monotone_q2}\]

This condition is called causality in the classical setting [9], and one-way signaling in the context of categorical quantum mechanics [20] since causality has a different meaning (see section <ref>). This condition is also at the heart of the quantum channels with memory in [8].

This one-way signaling condition characterizes the sequences of finite approximations produced by sequences of causal stateful morphisms. In particular, this notion is well adapted to $\UCPM$ where all morphisms are  causal. However, we aim at considering sequences of non-causal  stateful morphisms, like in $\CPM$. As a consequence, we need to introduce a weaker monotonicity condition to cover the non-causal case.   Useful examples of non-causal evolutions are the post-selected quantum evolutions.

In post-selected quantum mechanics the present can  depend on the future in a very specific way. It might happen that waiting gives us more information on a given state, for example turning a mixed state into a pure one. An example is given by the following post-selection protocol (see Example <ref> in Section <ref> for a pictorial description using a delayed trace): at each clock tick, a post-selected measurement of the memory is performed (except at the very first clock tick), then a new Bell pair is produced. One of the qubit of the pair is directly output while the other one is stored in the memory.
The corresponding stateful morphism sequence is:

Notice that we have  $\tikzfig{bell-meas-1}=\tikzfig{bell-meas}$, indeed the post-selected measurement is actually implemented by a linear map, hence the scalar $\tikzfig{scal-}=1/2$ which is witnessing the fact that an actual measurement produces this particular outcome with probability $1/2$.

The finite approximations of this protocol are:

bell1-   bell2-   bell3-   bell4-

$1$   $2$   $3$   $k$

We see
that if we stop at tick $k$, we have no information on the $k^\text{th}$ output, which is the maximally mixed state. However at tick $k+1$, the post-selection will force the $k^\text{th}$ output to be $\ket{0}\bra{0}$. In a sense, the future can refine the present. To formalize this we use the Loewner order defined on density matrices as $\rho \sqsubseteq \nu$ if $\nu - \rho$ is positive semi-definite. It can be extended naturally to maps by $f\sqsubseteq g$ if $g-f$ is completely positive. The Loewner order characterizes what it means for a state to be more precise than another.
Since the morphisms of $\CPM$ can also be trace increasing, we consider a lax-version of the Loewner order:
$f\preceq g$ if $\exists \lambda > 0$ such that $f\sqsubseteq \lambda g$. We will show in Section <ref> that the monotone sequences of finite approximations, i.e., such that $\forall k>0$,

\[\tikzfig{monotone_q} \quad  \preceq \quad \tikzfig{monotone_q2}\]

are exactly the ones that approximate the stateful morphism sequences in $\CPM$.

§.§ Regularity and Finite Memory

Among all the possible stateful morphism sequences, we  focus on the regular ones, i.e., those that are eventually constant: a stateful morphism sequence $(f_k)_{k>0}$ is regular if $\exists n, \forall k>n, f_k=f_n$. Notice in particular that regular stateful morphism sequences use a bounded amount of memory. Hence, it represents quantum computations acting on an unbound number of inputs but with a finite memory. This model is not a universal model of quantum computation, but it is an interesting  fragment to explore, and an intermediate scale model potentially easier to implement than a universal quantum computer using technologies which will be available in a near future.

Intuitively,  regular  stateful morphism sequences can be finitely described as they are eventually constant. In the next section, we introduce a graphical construction which turns any graphical language equipped with a discard, and acting on finite registers, into a graphical language for regular   stateful morphism sequences, i.e., in the quantum case, a language for representing and reasoning about finite-memory quantum stream computation.

§ THE COLORED GRAPHICAL LANGUAGE $\STREAM$

In this section we define the syntax of our language. We first set the string diagram notation and then, starting with a graphical language $\G$ describing computations we define a colored prop $\Stream$ which depicts computation with memory.

§.§ String Diagrams

We use the framework of props. A prop is a small symmetric strict monoidal category whose monoid of objects is freely spanned by one element denoted $1$. Representing the tensor additively, every object is then of the form $1+\cdots+1$ and therefore denoted $n$. The unit of the tensor is $0$. The categories $\UCPM$ and $\CPM$ from the previous section are equivalent to props[$\UCPM$ and $\CPM$ can be turned into props by defining the objects to be natural numbers and the morphisms $n\to m$ to be the linear maps $\mathcal M_{2^n\times 2^n}(\mathbb C) \to\mathcal M_{2^m\times 2^m}(\mathbb C)$.]. A colored prop is a small symmetric strict monoidal category whose monoid of objects is freely spanned by a set $C$ of colors. Each object can then be written as a list $c_1 + \cdots +c_k$ of colors. The string diagram notation represents arrows as boxes with colored wires as inputs and outputs. Given a $\{\blue,\red,\green,\orange\}$-colored prop $\textbf{P}$ with the arrows $F:\blue+\red \to \green+\orange$, $G:\blue\to\red$, $H:\red\to \green$ and the swap map $\sigma_{\blue,\red}: \blue+\red \to \red +\blue$ we write:

$\tikzfig{ord0}$     $\tikzfig{comp}$     $\tikzfig{tens}$     $\tikzfig{swap}$

$F$     $H\circ G$     $G\otimes H$     $\sigma_{\blue,\red}$

We say that a colored prop has a compact structure when for each color $\red$ there are two arrows $\tikzfig{cup} :0\to \red+\red$ and $\tikzfig{cap}: \red+\red \to 0$, satisfying the following equations:

The monochromatic prop $\CPM$ admits a compact structure but not $\UCPM$. Referring to string diagrams we will often say graphical language for a monochromatic prop and colored graphical language for a colored prop. We write $\Gamma \vdash D=K$ when we can rewrite the diagram $D$ into the diagram $K$ using the rewriting rules $\Gamma$.

To define the finite approximations, we need a way to express the loss of the data stored in the memory when we stop the computation, in other words we need a discard map.

A discard prop is a prop $\textbf{P}$ where we fix a discard map $\Terre{1}:1\to 0$. We denote $\Terre{0}\df id_0$ and $\Terre{a+b}\df \Terre{a}\otimes\Terre{b}$.

In a discard prop a morphism $C:a\to b$ is said to be causal if: $\tikzfig{cdist0}= \tikzfig{cdist1}$.

In what follows we consider only monochromatic discard props. $\UCPM$ and $\CPM$ are both discard. In $\UCPM$ all maps are causal while in $\CPM$ the causal maps are exactly the ones from $\UCPM$. Let $\G$ be a monochromatic discard graphical language defined by generators and equations. We build a colored graphical language $\Stream$ representing stream transformers.

§.§ Type System

The colors of the colored prop $\Stream$ are given by:

$C \df ~1~ | ~\omega~ | ~\D C$

A way to interpret the types is to consider a global clock that starts at the beginning of the computation. The $1$ type represents the basic data processed by $\G$. We keep in $\Stream$ all the generators and equations of $\G$. This yields an inclusion functor $\iota:\G\to \Stream$ that we will keep implicit most of the time. A wire of type $1$ sends one unit of data at tick $0$ and nothing after. The tensor unit is denoted $0$.

The $\omega$ type represents a stream of basic data. A wire of type $\omega$ sends one unit of data at each tick. We write $n\omega$ for a stream of $n$-tuples of data, i.e., $\omega+\ldots +\omega$ $n$-times, with the convention $1\omega\df \omega$ and $0\omega\df 0$. For each generator $G:n\to m$ in $\G$ we define a generator $\omega g: n\omega \to m\omega$ in $\Stream$. This gives a functor $\omega: \G \to \Stream$.

The delay modality $\D$ can be applied to any color to produce a delayed color. We write $\D^n C$ for the color $C$ delayed $n$ times: $\D^0 C = C$, $\D^n 0\df 0$ and $\D^{n+1} C = \D(\D^n C)$. A wire of type $\D^n 1$ sends one unit of data at tick $n$ but nothing before or after that tick. A wire of type $\D^n \omega$ sends nothing until tick $n+1$ and then sends one unit of data at each tick. The delay modality is extended to tensors of colors by setting $\D (S+T)=\D S + \D T$. For each generator $g:a\to b$ we have a delayed generator $\D g: \D a \to \D b$. This then extends to an endofunctor $\D: \Stream \to \Stream$.

We see that $\G$ is a subcategory of $\Stream$ in various ways given by the functors $\D^n \circ \iota :\G\to \Stream$ and $\D^n \circ \omega :\G\to \Stream$.

As an example of how the type system works, a finite stream of size $3$ sending two units of data at each tick for the first $3$  ticks would have type: $1+1+\D 1 + \D 1 + \D^2 1 + \D^2 1= 2+ \D 2 + \D^2 2$. Here we see that the tensor is used to encode at the same time spatial and temporal juxtaposition.

§.§ Initialization and Derivative

To manipulate streams we add to $\Stream$ two dual operators:

$\tikzfig{diff}:\omega \to 1+\D\omega\quad$   $\quad\tikzfig{init}:1+\D\omega \to \omega$

stream derivative     stream initialization

The derivative decomposes a stream into one data at first tick and a delayed stream which corresponds to the usual stream derivative. The initialization takes a delayed stream and adds a bit of data at the beginning to make it undelayed. They interact according to:

$\tikzfig{elim0}\stackrel{\left(\triangleright\triangleleft\right)}{=}\tikzfig{elim1}$ and $\tikzfig{exp0}\stackrel{\left(\triangleleft\triangleright\right)}{=}\tikzfig{exp1}$.

They also satisfy a distribution rule with all the delayed omega generators:

The dual equation $\left(\blacktriangleleft\right)$ for derivatives is also true and follows from $\left(\triangleleft\triangleright\right)$, $\left(\triangleright\triangleleft\right)$ and $\left(\blacktriangleright\right)$. Like all generators in $\Stream$, initialization and derivative admit delayed versions of types $\D^n\omega \to \D^n 1+\D^{n+1}\omega$ and $\D^n 1+\D^{n+1}\omega \to \D^n \omega$ satisfying the same equations. Those generators and equations are similar to the ones used in the scalable notations of [7]. There, such triangles were used to represent finite spatial juxtaposition of data while our generators deal with infinite temporal juxtaposition.

Example of quantum circuit stream diagram with no input/output. This diagram has side effects. At each clock tick the scalar $\tikzfig{scal-}= 1/2$ is produced.

\[\tikzfig{exa1}~\stackrel{\left(\triangleleft\triangleright\right)}{=}~\tikzfig{exa2}~\stackrel{\left(\blacktriangleleft\right)}{=}~\tikzfig{exa3}~\stackrel{\left(\blacktriangleright\right)}{=}~\tikzfig{exa4}\]

§.§ Delayed Trace

An important ingredient to the construction is the delayed trace. It is not strictly speaking a new generator but a constructor similar to the trace in traced monoidal categories. Given a map $D:a+ \D c \to b+c$ we can trace it to construct a new map $\Dtr{c}{a,b}{D}: a\to b$ represented by:

It allows a process to take as an input at tick $k+1$ one of its own outputs at tick $k$. In other words it allows to represent the memories of a stateful morphism sequence. It satisfies the following trace-like axioms:

$\tikzfig{tracenat0}=\tikzfig{tracenat1}$     $\tikzfig{tracenat2}=\tikzfig{tracenat3}$

$\tikzfig{tracenat4}=\tikzfig{tracenat5}$     $\tikzfig{tracenat6}=\tikzfig{tracenat7}$

The axiom for the tensor unit is here a tautology: $\Dtr{0}{a,b}{D}=D$. For typing reason we cannot obtain the identity if we trace the swap. Instead we get the delay: $\tikzfig{delay1}: c\to \D c$.

$\tikzfig{delay1}\df \tikzfig{delay0}$

The delay holds its input at tick $k$ and releases it at tick $k+1$. When $\G$ has a symmetric compact structure we can recover the delayed trace from the delay:

The protocol described in Section <ref> can be depicted as follows.  At each clock tick, a post-selected measurement of the memory is performed and a new Bell pair is produced. One of the qubit of the pair is directly output while the other one is stored in the memory.

\[\tikzfig{Bell-stream}=\tikzfig{Bell-stream-2}=\tikzfig{Bell-stream-3}\]

§.§ Causal Maps

Another axiom of the trace that we do not have is the analog of dinaturality. In fact this would imply that everything commutes with the delay:

0.8$\tikzfig{kom_3}=\tikzfig{kom_2} \Rightarrow \tikzfig{kom_1}=\tikzfig{kom_0}$

Intuitively, it does not make any difference if we apply $K$ on the memory data
at tick $k$ or at tick $k+1$. We want this to be true only if $K$ has no side effect, otherwise, we would identify processes that are not observationally equivalent, e.g., a process that diverges at tick 3 with a process that diverges at tick 4. Thus we require this from swaps, derivatives and initializations:

0.8$\tikzfig{delaydist0}\stackrel{\left(\triangleleft\right)}{=} \tikzfig{delaydist1}\qquad \tikzfig{delaydist2}\stackrel{\left(\triangleright\right)}{=}\tikzfig{delaydist3}$

0.8$\tikzfig{sidist0}\stackrel{\left(\sigma\right)}{=} \tikzfig{sidist1}$

and from all causal maps $C$ of $\G$:

0.8$\tikzfig{cdist0}= \tikzfig{cdist1}\quad \Rightarrow\quad \tikzfig{dcom2}=\tikzfig{dcom3}$ $\quad\left(\ground\right)$.

Note that the swaps coming from $\G$ are causal by definition and thus $(\sigma)$ follows from $(\ground)$. However, some swaps like the one between $1$ and $\omega$ do not come from morphisms of $\G$, hence the need for the axiom $(\sigma)$. Using the upcoming rule $(\D_{\mathbb{N}})$, we are able to derive the same equation with $\D^n \omega C$ instead of $\D^n \iota C$.

The rules defined so far can be used to unfold the first step of the cascade of CNots:

\[\tikzfig{CNot-casc-1} \stackrel{\left(\triangleleft\triangleright\right)}{=} \tikzfig{CNot-casc-2} \stackrel{\left(\blacktriangleright\right)}{=} \tikzfig{CNot-casc-3}\]

\[\stackrel{\UCPM}{=} \tikzfig{CNot-casc-4}\stackrel{\left(\triangleright\right)}{=}\tikzfig{CNot-casc-5}\]

§.§ Idempotents

Another identification we want to make with respect to observational equivalence concerns idempotents. Indeed, if an idempotent is applied on the memory data at tick $k$ then applying it again at tick $k+1$ has no effect at all. So it is possible to send a copy of an idempotent through the delay.

0.75$\tikzfig{pidist0}= \tikzfig{pidist1} \Rightarrow \tikzfig{pdcom2}=\tikzfig{pdcom3}$ $\quad\left(\pi\right)$

Using the upcoming rule $(\D_{\mathbb{N}})$, we are able to derive the same equation with $\D^n \omega \pi$ instead of $\D^n \iota \pi$. We note that the axiom $(\pi)$ implies:

Causal and idempotent morphisms are not the only two kind of morphisms that interact with the delay in some way. However, because of our completeness result (<ref>), we know that we can derive all those interactions from the present axioms.

§.§ Coinduction

We now introduce the final elements of the streamed prop construction. We denote by $\AX$ all the axioms that have been presented so far: $\left(\triangleright\right)$, $\left(\triangleleft\right)$, $\left(\blacktriangleright\right)$, $\left(\blacktriangleleft\right)$, $\left(\triangleright\triangleleft\right)$, $\left(\triangleleft\triangleright\right)$, $\left(\sigma\right)$, $\left({\ground}\right)$, $\left(\pi\right)$, and the four trace-like axioms.

To obtain the final axiomatization of $\Stream$ we quotient by a coinduction meta rule. Given two sequences of diagrams $\left(S_i\right)_{i\in\mathbb{N}}$ and $\left(T_j\right)_{j\in\mathbb{N}}$ in $\Stream$:

\hypo{\forall n\in \mathbb{N}\qquad \AX, \left[\D S_{n+1}= \D T_{n+1}\right] \vdash S_n =T_n}
\infer1[$\left(\D_\mathbb{N}\right)$]{\AX  \vdash S_0=T_0}
\end{prooftree}$

In practice we will use a weaker form which corresponds to the constant case where for all $i,j\in \mathbb{N}$, $S_i=S$ and $T_j =T$:

\hypo{\AX, \left[\D S= \D T\right] \vdash S =T}
\infer1[$\left(\D\right)$]{\AX  \vdash S=T}
\end{prooftree}$

Note that the weak form is also equivalent to the strong one in the case of eventually constant sequences of diagrams.
We provide an example of the coinduction principle in action.

We can show that discarding is the same as storing forever in a memory:

By applying $\left(\D\right)$ to show the equality, we can assume that its delayed version holds.

Note that we use the fact that the discard map is causal in the last step.

With a similar proof we can also derive the rules $\left({\ground}\right)$ and $\left(\pi\right)$ for the $\omega$ generators. Our definition of $\Stream$ is now complete.

§ $\STREAM$ AND STATEFUL MORPHISM SEQUENCES

We aim to describe every diagram $D\in\Stream$ with stateful morphism sequences, i.e., a sequence of diagrams of $\G$, the k$^\text{th}$ diagram of the sequence representing the behavior of $D$ at clock tick $k$.

§.§ Stateful Morphism Sequences

We start by defining the stateful morphism sequences over $\G$.

A stateful morphism sequence $f$ over a prop $\G$ is given by three sequences of objects $\left(a_i\right)_{1\leq i}$, $\left(b_i\right)_{1\leq i}$ and $\left(m_i\right)_{0\leq i}$ with $m_0\df 0$ together with a sequence of maps $f_i: a_i \otimes m_{i-1} \to b_i\otimes m_i$ with $1\leq i$. $f_i$ is called the $i$th layer of $f$.

A stateful morphism sequence $f$ can be (informally) depicted as follows: Layers are separated by dash lines and we connect in red the memory of consecutive layers.

\[\tikzfig{gmap0}\]

Following [9] we define a category $\textup{St}(\G)$ of stateful morphism sequences over $\G$. The objects are the sequences $\left(a_i\right)_{1\leq i}$ of objects in $\G$. When the types match, $g\circ f$ and $f \otimes g$ are defined as:

$(g\circ f)_k= \tikzfig{compseq-}\qquad(f\otimes  g)_k= \tikzfig{comptens-}$

We define a delay operator on stateful sequence morphism as $\left(\D f\right)_1 \df id_0$ and $\left(\D f\right)_k \df f_{k-1}$.

Clearly, all diagrams in $\Stream$ being finite we cannot represent arbitrary sequences. In fact we will see that we can only represent   $\RegStSeq{\G}$, the subcategory of $\textup{St}\left(\G\right)$  restricted to  regular stateful morphism sequences in which we consider only eventually constant sequences.

§.§ Finite Approximations

A finite aproximation sequence over a discard prop $\G$ is given by two sequences of objects $\left(a_i\right)_{1\leq i}$ and $\left(b_i\right)_{1\leq i}$, together with a sequence of maps $f_k: \bigotimes\limits_{i=1}^k a_i \to \bigotimes\limits_{i=1}^k b_i$. $f_k$ is called the $k^\text{th}$ approximation of $f$. We postpone to Definition <ref> the precise conditions that those sequences must satisfy.
Given a stateful morphism sequence we define its finite approximation sequence $\textup{FA}(f)$ by:

There is also a category $\textup{FA}(\G)$ of finite approximation sequences over $\G$ where composition and tensor are defined approximation-wise. We have a symmetric monoidal functor $\textup{FA}:\textup{St}(\G) \to \textup{FA}(\G)$. Two stateful sequences with the same image by $\textup{FA}$ are said to be observationally equivalent. We design $\Stream$ towards the goal to be universal and complete for $\textup{FA}(\G)$. we will see that while we do not achieve this goal in full generality, we can get close enough in some particular cases.

§.§ Stratified Types

There are more types in $\Stream$ than in $\RegStSeq{\G}$. We need to quotient in order to obtain a correspondence. A type in $\Stream$ is a list of colors of two kinds: $\D^k 1$ and $\D^k \omega$. We call the degree of a type the highest delay appearing in it. A type $a$ of degree $d$ is said to be stratified if it is of the form: $a=\sum_{i=0}^{d} \D^i n_i + \D^{d} n_{d+1}\omega$, i.e., colors are sorted by increasing delays with at the end the $\omega$ colors, all having the largest delay. Note that some $n_i$ might be $0$. Given a stratified type $a$ of degree $d$ we define the rising $\delta^k a$ with $k\geq d$ as:

$\delta^k a\df \sum_{i=0}^{d} \D^i n_i + \sum_{j=d}^{k} \D^{j} n_{d+1} + \D^{k} n_{d+1}\omega$.

Note that $\delta^d a = a$. $\delta^k a$ is a stratified type of degree $k$ if $a$ contains $\omega$ types and $d$ otherwise. We say that two types are disjoint if there is no tick when they both send data. Formally, we inductively define a disjointness symmetric relation $*$ on types as: $0*a\Leftrightarrow a\neq 0$, $\D^i 1 * \D^j 1 \Leftrightarrow i\neq j$ ,$\D^i 1 * \D^j \omega \Leftrightarrow i< j$ and $a*(b+c) \Leftrightarrow \left(a*b\right) \land \left(a*c\right)$. A disjoint swap is a swap $a+b\to b+a$ between disjoint types, i.e., such that $a*b$.

The category of disjoint maps is defined as the wide subcategory of $\Stream$ spanned by initializations, derivatives and disjoint swaps. Note that the subcategory of disjoint maps is a groupoid since all generators are invertible and their inverses are also disjoint maps. The disjoint maps do not modify anything about the processing of data but are graphical bureaucracy that we need to quotient.

Given a type $a$ of degree $d$. There is always a disjoint map $a\to \overline{a}$, where $\overline{a}$ is stratified of degree $d$, as well as a disjoint map $\overline{a}\to \delta^k\overline{a}$ for each $k\geq d$. And if there is a disjoint map $a\to b$ then it is unique and there is a $k$ such that $\delta^k \overline{a}=\delta^k\overline{b}$.

We define the equivalence relation $\sim_s$ on types as $a\sim_s b$ whenever there exists a (necessarily unique) disjoint map $a\to b$. So if $a\sim_s c$ and $b\sim_s d$ then there is a natural bijection between $\Stream(a,b)$ and $\Stream(c,d)$ whose components are the disjoint maps $a\to c$ and $b\to d$. This implies that we have a well defined monoidal category $\quot{\Stream}{\sim_s}$. We write $D\sim_s D'$ whenever two diagrams are identified by this quotient.

For any type $a$ of degree $d$ the equivalence class of $a$ for $\sim_s$ is simply the set $\{b~|~ \exists k, \delta^k\overline{b} = \delta^k \overline{a} \}$. Those equivalence classes are in bijection with the ultimately constant sequences of types in $\G$. Thus, the objects of $\quot{\Stream}{\sim_s}$ and $\RegStSeq{\G}$ are in bijection.

We define the functor $G:\RegStSeq{\G}\to \quot{\Stream}{\sim_s}$ from the functor $\RegStSeq{\G}\to \Stream$ by mapping the sequence of objects in $\G$ eventually constant from tick $d$ to the corresponding stratified type of degree $d$ in $\Stream$. A stateful morphism sequence is then mapped to a diagram as follows:

0.7$\tikzfig{gmap0}\mapsto \tikzfig{gmap1}$

In fact all diagrams of $\quot{\Stream}{\sim_s}$ can be written in such form.

$G:\RegStSeq{\G}\to \quot{\Stream}{\sim_s}$ is full.

§.§ Correspondence with $\quot{\RegStSeq{\G}}{\equiv}$

We add the following rewriting rules $\equiv$ to $\RegStSeq{\G}$ to match the rewriting rules of $\Stream$. We define $D \equiv D'$ as:

\[ \CM,\IM \vdash D = D' \]

with $\vdash$ admitting the usual deduction rules of a congruence[The rules for reflexivity, symmetry, and transitivity, together with the preservation under contexts of the form $(S \otimes -)$, $(- \otimes S)$, $(S \circ -)$ and $(- \circ S)$.] together with the coinduction rule:

\hypo{\forall n\in \mathbb{N}\qquad \Gamma, \left[\D S_{n+1}= \D T_{n+1}\right] \vdash S_n =T_n}
\infer1[$\left(\D_\mathbb{N}\right)$]{\Gamma \vdash S_0=T_0}
\end{prooftree}$

and with the axioms $\CM$ and $\IM$ being the following, for $c$ causal and $\pi$ idempotent:

$\CM \vdash \tikzfig{conggr0} = \tikzfig{conggr1}$

$\IM \vdash \tikzfig{congpi0} = \tikzfig{congpi1}$

We write $\quot{\RegStSeq{\G}}{\equiv}$ for the quotient $\RegStSeq{\G}$ by this congruence.

$f\equiv g \Leftrightarrow G(f)=G(g)$

This implies that $G$ factorizes into the projection $\RegStSeq{\G}\to \quot{\RegStSeq{\G}}{\equiv}$ followed by a full and faithful functor $\mathfrak{G}:\quot{\RegStSeq{\G}}{\equiv}\to\quot{\Stream}{\sim_s}$.

It follows that we can completely characterize $\Stream$ by the $\equiv$ relation on stateful morphism sequences.

For any discard monochromatic prop $\G$:

§ THE SEMANTICS OF $\STREAM$

In this section, we define the semantics of our language $\Stream$. We assume given a semantics $\sem{-} : \G \to \C$ of $\G$, and will extend it into a semantics $\sembis{-}$ for diagrams of $\Stream$.  The semantics of $D \in \Stream$  will be its finite approximation sequences, i.e., a sequence of morphisms of $\C$, with the $k^\text{th}$ morphism corresponding to the computations done up until the $k^\text{th}$ tick of the clock. We prove that our semantics is sound. We also prove universality and completeness up to some  additional requirements on $\G$ and $\C$.

§.§ Discard Category

The only required assumption for the definition of $\Stream$ is that $\G$ is a discard prop. We expect the category $\C$ to enjoy the same property. As a consequence, we introduce a straightforward extension of the notion of discard prop to the symmetric monoidal case:

A discard category is a symmetric monoidal category $(\C,\otimes,I)$ together with, for every object $A$, a discard map $\Terre{A} : A \to I$ such that $\Terre{I} = \id_{I}$ and $\Terre{A \otimes B} = \Terre{A} \otimes \Terre{B}$.

We write $\C_{\textup{causal}}$ its subcategory of causal morphisms, i.e., morphisms $f$ such that $\Terre{B} \circ f = \Terre{A}$. We say that a monoidal functor $\mathcal{F}$ between discard categories is discard-preserving if $\mathcal{F}(\Terre{A}) = \Terre{\mathcal{F}(A)}$. We say that it is discard-reflecting if whenever $\mathcal{F}(f) = \Terre{\mathcal{F}(A)}$ we have $f = \Terre{A}$. Those properties are equivalent to $\mathcal{F}$ respectively preserving or reflecting causal morphisms.

From now on, we assume that $\C$ is a discard category and the functor $\sem{-}$ is monoidal and discard-preserving, as those properties are required for soundness. For completeness, we will additionally expect $\sem{-}$ to be discard-reflecting.

§.§ Semantics

To define the semantics of a diagram $D \in \Stream(a,b)$, we rely on the fact that $\quot{\Stream}{\sim_s}$ and $\quot{\RegStSeq{\G}}{\equiv}$ are equivalent categories (Theorem <ref>), and write $\partial D$ the equivalence class of stateful morphism sequences associated to $\quot{D}{\sim_s}$. We then apply $\sem{-}$ to each layer:
we write $\sem{-}^{\textup{St}}$ for the functor from $\quot{\RegStSeq{\G}}{\equiv}$ to $\quot{\RegStSeq{\C}}{\equiv}$ which simply applies $\sem{-}$ to every layer of the sequence. This functor inherits all the properties of $\sem{-}$, and is in particular monoidal and discard-preserving.

We then collect all the operations happening up until the $k^\text{th}$ tick for $k \geq 1$. For $\alpha = (\alpha_n)_{n \geq 1} \in \RegStSeq{\C}(A,B)$ we define its $k$-th finite approximation $\fa{\alpha}_k \in \C(\fa{A}_k,\fa{B}_k)$ as follows:

\[ \fa{A}_k \df A_1 \otimes \dots \otimes A_k \qquad  \fa{\alpha}_k  \df \tikzfig{onion_from_strat_bis}\]

We note that while stateful morphism sequences of a diagram are defined up to the observational equivalence $\equiv$, $\fa{-}_k$ is sound with respect to this congruence:

Whenever $\alpha \equiv \beta$, for every $k \geq 1$ we have $\fa{\alpha}_k = \fa{\beta}_k$. So $\fa{-}_k$ can be seen as a functor from $\quot{\RegStSeq{\C}}{\equiv}$ to $\C$.

We then collect all of the $(\fa{\alpha}_k)_{k \geq 1}$ into a morphism $\fa{\alpha}$ of the category of morphism sequences $\Seq$ defined below, which we will later refine into the category of finite approximation sequences $\Onion$.

For $\C$ a discard category, we define the discard category of sequences of $\C$, written $\Seq$, as follows:

* Its objects are sequences $(A_k)_{k \geq 1}$ with $A_k\in \textup{Obj}(\C)$.

* Its morphisms are sequences  $(f_k)_{k \geq 1}$ such that $f_k \in \C(A_k,B_k)$

* The composition (resp. monoidal product, resp. discard) is the composition (resp. monoidal product, resp. discard) component-wise.

Using Lemma <ref>, we can now define $\sembis{-}$ as the composition of previously defined functors:

\[ \sembis{-} \df \fa{\sem{\parsem[]{-}}^{\textup{St}}} : \Stream \to \Seq \]

It is a discard-preserving monoidal functor.

§.§ Examples

$D \qquad\qquad \sembis{D}_1 \qquad\qquad \sembis{D}_2 \qquad\qquad \sembis{D}_k$

Semantics of Generators

To illustrate this semantics, we detail in Fig. <ref> the semantics of five special cases: the $\iota$-morphisms, the $\omega$-morphisms, the delayed morphisms, the stream initialization, the $\iota$-delay and the $\omega$-delay. The second case covers one of our first examples in $\CPM$ (see Example <ref>): the measure applied to a completely mixed state, seen as an $\omega$-morphism. At each tick of the clock, it will generate another instance of mixed stated followed by measure, which is the scalar $1/2$. At the $k$-th tick, we then have:

$\sembis{\tikzfig{exa1}}_k = \left(\frac{1}{2}\right)^k$

§.§ Universality

While this semantics is sound, $\Seq$ contains significantly more behaviors than $\Stream$, as $\Seq$ does not constrain any relation between the states of the computation at ticks $k$ and $k+1$. To obtain universality, we need to restrict $\Seq$ to a more realistic category. As presented previously in <ref> in the quantum case, we start by adding a condition of monotonicity:

* An object $(A_k)_{k \geq 1}$ is monotone if for every $k \geq 1$, there exists an object $A'_k$ of $\C$ such that $A_{k+1} = A_k \otimes A'_k$.

* A morphism $(g_k)_{k \geq 1}$ is monotone if for every $k \geq 1$, we have

$\tikzfig{monotone_q} \preceq \tikzfig{monotone_q2}$

for $\preceq$ defined below.

Decreasing along $\preceq$ means adding additional observable effects. In particular, whenever $\C$ is the category $\UCPM$, or any other category in which every morphism is causal, then $\preceq$ is nothing but  the equality. In the general case, we take $\preceq$ to be the following:

For $f,g \in \C(A,B)$, we have $f \preceq g$ whenever there exist $g_0 \in \C(A,B \otimes X)$ and $f_0 \in \C(X,I)$ such that

$f = \tikzfig{g0_f0} \qquad \qquad g = \tikzfig{g0_ground}$

In the case of $\C = \CPM$, $\preceq$ is tightly linked to the Loewner order, as we have

\[ f \preceq g \iff \exists \lambda > 0, (g - \lambda \cdot f) \in \CPM \]

We note that without additional restrictions on $\C$, $\preceq$ might not be transitive. To ensure transitivity, we require for $\C$ to have a notion of pseudo-purification, which is a generalization of the notion of purification in the quantum case. From a programming point of view, each time the morphism is “dumping” some information through the use of a discard, we want to intercept this discard map and instead output that information on a secondary output so that they can be used for later computations.

In a discard category $(\C,\otimes,I,\Terre{})$, a morphism $p \in \C(A,B \otimes X)$ is said to be a pseudo-purification of $f \in \C(A,B)$, and we write $p \in \Pure(f)$, if for every $g \in \C(A,B \otimes Y)$

\[ f = \tikzfig{purification_G} \implies \exists c \text{ causal}, g = \tikzfig{p_c} \]

In particular, whenever $p \in \Pure(f)$ we always have

\[ f = \tikzfig{purification} \]

and given two pseudo-purifications $p_1,p_2 \in \Pure(F)$ there exist two causal morphisms $c_1$ and $c_2$ such that

\[ p_1 = \tikzfig{p2_c2} \qquad p_2 = \tikzfig{p1_c1} \]

The uniqueness of pseudo-purification up to a causal morphism is an analogue to Stinespring's dilation (Theorem <ref>), that we adapted to account for the possible absence of a notion of isometry.

A discard category $(\C,\otimes,I,\Terre{})$ is said to be pseudo-purifiable whenever every morphism has a pseudo-purification, and moreover for $f_1 \in \C(A_1,B_1 \otimes C)$, $f_2 \in \C(C \otimes A_2,B_2)$, $p_1 \in \Pure(f_1)$ and $ p_2 \in \Pure(f_2)$ we have:

\[\tikzfig{purification_comp3} \in \Pure\left(\tikzfig{F_G_compo_tenseur}\right) \]

In particular for $C = I$ we obtain that:

\[\tikzfig{purification_tensor2} \in \Pure(f_1 \otimes f_2) \]

In a pseudo-purifiable category $(\C,\otimes,I,\Terre{})$, $\preceq$ is transitive, is preserved under composition and monoidal product, hence forms a pre-order enrichment of $\C$.

The categories $\CPM$ and $\UCPM$ are pseudo-purifiable categories. Moreover, every purification (for the usual notion of purity, see Section <ref>) is a pseudo-purification.

Not every pseudo-purification in $\CPM$, is a purification. Indeed, a purification of $\id_I$ is any isometric (so pure and causal) states $q \in \CPM(I,A)$, while every causal state (pure or not) is a valid pseudo-purification of $\id_I$.

Every cartesian category $(\C,\times,I)$ is pseudo-purifiable, and for every $f \in \C(A,B)$, the pairing $(f,\id_A) \in \C(A,B \times A)$ is one of the pseudo-purifications of $f$.

With monotonicity defined, we are one step closer to universality. However, monotone sequences still contain behaviors that are not captured by our language. More precisely, monotone sequences contain behaviors that would be representable by an infinitely-sized diagram, but cannot be represented in our finitary language. We restrict ourselves to regular monotone sequences, which we call finite approximations and define as follows:

For $\C$ a pseudo-purifiable category, we define the discard category of finite approximation sequences $\Onion$ as $\Seq$ restricted to

* Objects $(A_k)_{k \geq 1}$ that are monotone (see above) and regular, i.e., there exists $n \geq 1$ and $A'$ such that for all $k \geq n$ we have $A_k = A_n \otimes A'^{\otimes (k-n)}$.

* Morphisms $(g_k)_{k \geq 1}$ that are monotone (see above) and regular, i.e., there exists $n \geq 1$, $g^{\textup{irreg}} \in \C(A_n,B_n \otimes M)$ and $g^{\textup{reg}} \in \C(M \otimes A',B' \otimes M)$ such that for all $k \geq n$

$g_k = \tikzfig{regularity_g}$.

For every $f \in \Stream$, $\sembis{f} \in \Onion$.

If $\C$ is pseudo-purifiable and the functor $\sem{-} : \G \to \C$ is full, then $\sembis{-} : \Stream \to \Onion$ is full too.

§.§ Completeness

The discard allows us to discard “future computation” and only keep what happens before a given tick. However, in the proof of completeness, we will need to act dually and have a way to undo the first computations to only keep what happens in later ticks. Ideally, we would want morphisms to be surjections (or epimorphisms), as a surjection $f$ satisfies the following:

\[g \circ f = h\circ f \iff g = h\]

Unfortunately, the category $\CPM$ contains non-surjective morphisms, and even contains morphisms that cannot be decomposed into a surjection followed by an injection[Though if one allows every Hilbert space instead of restricting ourselves to only Hilbert spaces of dimension a power of two, every morphism becomes decomposable.]. However, for $f \in \CPM(A,B)$ a morphism corresponding to a pure quantum computation, there always is an idempotent morphism $\pi$ (the projector over the image of $f$) such that:

\[g \circ f = h \circ f \iff g \circ \pi = h \circ \pi\]

We formalize a slight generalization of this property in the concept of morphism with shadows.

In a symmetric monoidal category $(\C,\otimes,I)$ a morphism with shadows is a morphism $f \in \C(A,B)$ such that for every isomorphism $\iota: B \cong B_0 \otimes B_1$, there exists an idempotent morphism $\pi : B_1 \to B_1$, called shadow of $f$, such that:

$\forall g,h,\quad\begin{matrix} \tikzfig{shadow_f_g} = \tikzfig{shadow_f_h} \\ \iff \\ \tikzfig{shadow_pi_g} = \tikzfig{shadow_pi_h}  \end{matrix}$

A pseudo-purifiable category is said to be a shadow pseudo-purifiable category if every morphism has at least one pseudo-purification which is a morphism with shadows.

The idea of using idempotent morphisms to characterize the image of morphisms is already present in range categories (see [21]), but we chose here a definition much more tailored to our needs than the strict structure of range categories.

The categories $\CPM$ and $\UCPM$ are shadow pseudo-purifiable. In fact, all the morphisms that are pure quantum computations are morphisms with shadows.

If $\C$ is a shadow pseudo-purifiable category and the functor $\sem{-} : \G \to \C$ is faithful and discard-reflecting, then $\sembis{-}$ is faithful too.

This follows from the faithfulness of

\[ \Stream \xrightarrow{\partial} \quot{\RegStSeq{\G}}{\equiv} \xrightarrow{\sem{-}^{\textup{St}}} \quot{\RegStSeq{\C}}{\equiv} \xrightarrow{\fa{-}} \Onion \]

§ APPLICATIONS

§.§ The ZX-calculus

The ZX-calculus is known to be universal and complete for various fragments of quantum mechanics [22, 23, 24], including the most general case: the ZX-calculus – equipped with a discard map – is  universal and complete for $\CPM$ [2]. Furthermore Lemmas <ref> and <ref> give us that $\CPM$ is a pseudo-purifiable shadow category. As a consequence ZX$^\omega$ is universal and complete for monotone regular sequences over $\CPM$. Similar results hold for variants of the ZX-calculus like the ZW- or the ZH-calculi which are also universal and complete for $\CPM$ [2]. On the other hand, quantum circuits, equipped with a discard map, are universal for $\UCPM$ but no axiomatization is known to be complete.

§.§ The Fragment $\Stream_0$ of Initialized Delays

Using delayed trace for process with memory is not a new idea. It has appeared in various context [17, 9, 25, 10], usually in the cartesian case and with an initialized delayed trace restricting the expressivity to sequences which are regular from the beginning. In this subsection we present the fragment of our language that corresponds to this situation and then in the following subsections compare our results to selected examples from the literature providing an overview of the generality of our construction and its limitations.

In $\Stream$, the need for delayed types $\D^{n+1} \omega$ arises from the fact that the delay morphism on streams takes as an input a stream but outputs a stream with an undefined behavior for the first tick. However, adding delayed types $\D^{n+1} \omega$ is not the only solution to this problem. Indeed, most preexisting works instead chose to use an initialized delay. Those initialized delays can be encoded in $\Stream$ as follows: given $a$ a type of $\G$ and $F \in \G(0,a)$ we define the delay initialized by $F$ as:

\[ \tikzfig{memcell} \df \tikzfig{memcell_def} \]

We note that in the cartesian case, every morphism $F \in \C(0,a)$ can be decomposed into a product of morphisms on $\C(0,1)$, so one only needs to define the initialized delayed trace on single wires rather than collection of those.

We consider $\Stream_0$ the sublanguage of $\Stream$ where every delay has to be initialized:

* Most of the objects of $\Stream$ are unnecessary, we only take

\[\textup{Obj}(\Stream_0) \df \{ n \cdot \omega ~|~n \in \NN\} = \omega(\textup{Obj}(\G))\]

* $\Stream_0$ is a prop, with for generators the morphisms $\omega(D)$ for $D$ a morphism of $\G$, and the delayed trace initialized by $F \in \G(0,c)$:

\[\Dtri{F}{\omega(c)}{a,b}{D} \in \Stream_0(a,b) \text{ for } D \in \Stream_0(a+\omega(c),b+\omega(c)) \]

The stateful morphism sequences associated to $\Stream_0$ are sequences $(f_k)_{k \geq 1}$ for which the regularity condition starts at the second tick: $\forall k \geq 2, f_k = f_2$.
Similarly, on the semantics side, the corresponding finite approximations $(f_k)_{k \geq 1}$ are regular starting from the first tick:

\[ f_k = \tikzfig{regularity_imm} \]

Note that all diagrams in $\Stream_0$ can be rewritten into the form:

We don't claim any universality or completness result for this fragment.

§.§ Quantum Channels with Memory

The first inspiration of this work was the quantum channels with memory of [8]. This corresponds to the case where we take $\G$ to be the category of quantum circuits with discard. There are still no known complete finite axiomatizations of the full language. Assuming a free axiomatization matching the semantics in $\UCPM$ we can construct $\Stream$. $\UCPM$ is a pseudo-purifiable discard shadow category thus $\Stream_0$ is complete and universal for monotone finite approximations regular from tick $2$. $\UCPM$ is also a semi-cartesian category, meaning that all its morphisms are causal. In such situation, we can significantly simplify  the definition of $\Stream$ by fusing the $\left({\ground}\right)$ and $\left(\pi\right)$ rules. Moreover, the order $\preceq$ then collapses to the identity, leading to a clear interpretation of the monotone sequences as processes where the present does not depend on the future.

Applying quantum mechanics to those stream transformers usually requires infinite-dimensionalal Hilbert spaces. In [8], quasi local algebras are used to represent those processes in the Heisenberg picture, a quantum analog of the predicate transformer point of view. The authors require from their channels a causality condition that matches precisely our monotonicity requirement. The main difference with our work is that they consider streams on $\mathbb{Z}$ (so an infinity of ticks happened before the tick $1$) while we consider streams on $\mathbb{N}_{\geq 1}$.

However, given a fixed quantum state for the ticks $(-\infty,0]$, their condition of translational invariance corresponds to our condition of regularity on finite approximations. They obtain a structure theorem that corresponds precisely to the general form of diagrams in $\Stream_0$.

§.§ The Cartesian Case

The stateful morphism sequences were first defined by [9] in the cartesian case. A cartesian category is always pseudo-purifiable and semi-cartesian.

In [9], the authors build a category very similar to $\Stream_0$ by quotienting stateful morphism sequences by an observational equivalence relation corresponding to ours in the cartesian case. They define the exact same initialized delayed trace and study in more details the category of stateful sequences of morphisms. However they do not show any universality or completeness results, focusing instead on differentiability.

Note that taking $\G$ to be boolean circuits with semantics in Set (which is a cartesian shadow category) we can deduce from $[9]$ that $\Stream_0$ has the expressive power of Mealy machines. In this direction, further work will focus on understanding exactly which kind of synchronous circuits can be represented by our construction in connection to the work of [25].

§.§ Signal Flow Graphs

Another work  similar to ours is the work of [17] on signal flow graphs. Similarly to [8], they consider streams on $\mathbb{Z}$ while we consider streams on $\mathbb{N}_{\geq 1}$. There is however another major difference in approach: they represent streams and their operations as a whole (using power series) rather than through their finite approximations. This leads to a set of axioms incompatible to ours, in particular the rule (S5) of their Definition 3 would translate to the following:

\[ \tikzfig{unsound_rule} \stackrel{\text{(S5)}}{=} \tikzfig{identity}\]

which is unsound for finite approximations. Indeed, the left hand side is interpreted by us as follows: the information $i$ received at the tick $n$ is not immediately output, instead the system generates a “blank” output (the transposed of $\Terre{}$), which retroactively changed to be equal to $i$ at tick $n+1$. This behavior is fundamentally non-causal, but is expected as the co-unit of a compact closure is not a causal morphism.

However, when considering the fragment $\mathbb{SF}$ of circuits that only contain initialized guarded traces (which they call feedbacks), we recover a correspondence. In fact their calculus seems to be exactly $\Stream_0$ when we take $\G$ to be the graphical language $\mathbb{HA}$.

Taking the same example as in their paper, we can describe the Fibonacci sequence as a morphism of $\Stream_0$, with $\G$ being the prop of linear operations on tuples of integers:

where $\bfup{0} \in \G(0,1)$ being the integer zero, white dots representing the addition and black dots representing the copy.
On the input stream $1,0,0$, etc this circuit will output the Fibonacci sequence $0,1,1,2,3$, etc.

Another interesting connection with this line of work is to take $\G$ to be $\mathbb{IH}$, a graphical calculus which have been shown to be complete for linear relations [26]. The order relation $\preceq$ then coincides with the subspace relation for vector spaces.

More work has still to be done along this line to unravel all the connections between the two formalisms.

§ ACKNOWLEDGMENT

This work is funded by ANR-17-CE25-0009 SoftQPro, ANR-17-CE24-0035 VanQuTe,
PIA-GDN/Quantex, and LUE/UOQ. This research is also supported by the project NEASQC funded from the European Union’s Horizon 2020
research and innovation programme (grant agreement No 951821).

[1]
R. Vilmart, “A near-optimal axiomatisation of ZX-calculus for pure qubit
quantum mechanics,” in Proceedings of the 34th Annual ACM/IEEE
Symposium on Logic in Computer Science (LICS), 2019. [Online]. Available:

[2]
T. Carette, E. Jeandel, S. Perdrix, and R. Vilmart, “Completeness of graphical
languages for mixed states quantum mechanics,” in International
Colloquium on Automata, Languages, and Programming (ICALP'19), 2019.

[3]
R. Duncan, A. Kissinger, S. Perdrix, and J. van de Wetering, “Graph-theoretic
Simplification of Quantum Circuits with the ZX-calculus,”
Quantum, vol. 4, p. 279, Jun. 2020. [Online]. Available:

[4]
A. Kissinger and J. van de Wetering, “Reducing the number of non-Clifford
gates in quantum circuits,” Physical Review A, vol. 102, no. 2, p.
022406, 2020.

[5]
M. Hanks, M. P. Estarellas, W. J. Munro, and K. Nemoto, “Effective compression
of quantum braided circuits aided by ZX-calculus,” Phys. Rev. X,
vol. 10, p. 041030, Nov 2020. [Online]. Available:

[6]
N. de Beaudrap and D. Horsman, “The ZX calculus is a language for surface
code lattice surgery,” Quantum, vol. 4, p. 218, Jan. 2020.
[Online]. Available: <https://doi.org/10.22331/q-2020-01-09-218>

[7]
T. Carette, D. Horsman, and S. Perdrix, “SZX-calculus: Scalable graphical
quantum reasoning,” in MFCS 2019-44th International Symposium on
Mathematical Foundations of Computer Science, vol. 138, 2019, pp. 55–1.

[8]
D. Kretschmann and R. F. Werner, “Quantum channels with memory,”
Physical Review A, vol. 72, no. 6, p. 062323, 2005.

[9]
D. Sprunger and S.-y. Katsumata, “Differentiable causal computations via
delayed trace,” in 2019 34th Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS).1em plus 0.5em minus 0.4emIEEE, 2019,
pp. 1–12.

[10]
M. Román, “Comb diagrams for discrete-time feedback,” arXiv
preprint arXiv:2003.06214, 2020.

[11]
A. Kissinger and D. Quick, “A First-order Logic for String Diagrams,” in
6th Conference on Algebra and Coalgebra in Computer Science (CALCO
2015), ser. Leibniz International Proceedings in Informatics (LIPIcs), L. S.
Moss and P. Sobocinski, Eds., vol. 35.1em plus 0.5em minus 0.4emDagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015,
pp. 171–189. [Online]. Available:

[12]
S. Abramsky and C. Heunen, “H*-algebras and nonunital frobenius algebras:
First steps in infinite-dimensional categorical quantum mechanics,” in
Clifford Lectures, AMS Proceedings of Symposia in Applied Mathematics,
vol. 71, 2012.

[13]
B. Coecke and C. Heunen, “Pictures of complete positivity in arbitrary
dimension,” Information and Computation, vol. 250, pp. 50–58, 2016.

[14]
S. Gogioso and F. Genovese, “Infinite-dimensional categorical quantum
mechanics,” in Proceedings 13th International Conference on
Quantum Physics and Logic, Glasgow, Scotland, 6-10 June 2016, ser.
Electronic Proceedings in Theoretical Computer Science, R. Duncan and
C. Heunen, Eds., vol. 236.1em plus 0.5em minus 0.4emOpen
Publishing Association, 2017, pp. 51–69.

[15]
B. Schumacher and R. F. Werner, “Reversible quantum cellular automata,”
arXiv preprint quant-ph/0405174, 2004.

[16]
P. Arrighi, V. Nesme, and R. Werner, “Unitarity plus causality implies
localizability,” Journal of Computer and System Sciences, vol. 77,
no. 2, pp. 372–378, 2011.

[17]
F. Bonchi, P. Sobociński, and F. Zanasi, “A categorical semantics of
signal flow graphs,” in International Conference on Concurrency
Theory.1em plus 0.5em minus 0.4emSpringer, 2014, pp. 435–450.

[18]
M. A. Nielsen and I. Chuang, “Quantum computation and quantum information,”

[19]
W. F. Stinespring, “Positive functions on C*-algebras,” Proceedings
of the American Mathematical Society, vol. 6, no. 2, pp. 211–216, 1955.

[20]
A. Kissinger and S. Uijlen, “A categorical semantics for causal structure,”
in 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
(LICS).1em plus 0.5em minus 0.4emIEEE, 2017, pp. 1–12.

[21]
R. Cockett, X. Guo, and P. Hofstra, “Range categories i: General theory,”
Theory and Applications of Categories [electronic only], vol. 26, 01

[22]
M. Backens, “The ZX-calculus is complete for stabilizer quantum mechanics,”
New Journal of Physics, vol. 16, no. 9, p. 093021, sep 2014. [Online].
Available: <https://doi.org/10.1088%2F1367-2630%2F16%2F9%2F093021>

[23]
E. Jeandel, S. Perdrix, and R. Vilmart, “A complete axiomatisation of the
ZX-calculus for Clifford+T quantum mechanics,” in Proceedings of
the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
(LICS).1em plus 0.5em minus 0.4emACM, 2018, pp. 559–568.

[24]
A. Hadzihasanovic, K. F. Ng, and Q. Wang, “Two complete axiomatisations of
pure-state qubit quantum computing,” in Proceedings of the 33rd Annual
ACM/IEEE Symposium on Logic in Computer Science, ser. LICS '18.1em
plus 0.5em minus 0.4emNew York, NY, USA: ACM, 2018, pp. 502–511.
[Online]. Available: <http://doi.acm.org/10.1145/3209108.3209128>

[25]
D. R. Ghica, A. Jung, and A. Lopez, “Diagrammatic semantics for digital
circuits,” in 26th EACSL Annual Conference on Computer Science Logic
(CSL 2017).1em plus 0.5em minus 0.4emSchloss
Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.

[26]
F. Zanasi, “Interacting hopf algebras: the theory of linear systems,”
arXiv preprint arXiv:1805.03032, 2018.

§.§ Equivalence of $\Stream$ and $\RegStSeq{\G}$

Given a type $a$ of degree $d$. There is always a disjoint map $a\to \overline{a}$, where $\overline{a}$ is stratified of degree $d$, as well as a disjoint map $\overline{a}\to \delta^k\overline{a}$ for each $k\geq d$. And if there is a disjoint map $a\to b$ then it is unique and there is a $k$ such that $\delta^k \overline{a}=\delta^k\overline{b}$.

Given any type $a$ of degree $d$ we can always use derivatives to construct a map $a\to a'$ where all $\omega$ colors in $a'$ are delayed $d$ times. Then we can use disjoint swaps to reorder each colors and construct a disjoint map $a'\to \overline{a}$ where $\overline{a}$ is stratified of degree $d$. Furthermore using derivatives we can construct a disjoint map $\overline{a}\to \delta^k\overline{a}$ for any $k\geq d$.

Let $a$ and $b$ be respectively of degree $l_a$ and $l_b$ and let $k\df \max(l_a,l_b)$. We assume there is a disjoint map $f:a\to b$. We now there are disjoint maps of types $a\to \delta^k\overline{a}$ and $b\to \delta^k\overline{b}$. Those maps being invertible, there is a bijection between disjoint maps $a\to b$ and disjoint maps $\delta^k\overline{a}\to \delta^k\overline{b}$. So we just have to show that the map $f':\delta^k\overline{a}\to \delta^k\overline{b}$ is unique. Using the equations $(\triangleleft\triangleright)$, $(\triangleright\triangleleft)$ and the naturality of the swaps we can rewrite $f'=i\circ \sigma \circ d$ where $i$ is made only of initializations, $d$ only made of derivatives and $\sigma$ is a disjoint permutation. Since $i$ and $d$ cannot change the order of the colors and since the colors are already well ordered in $\delta^k\overline{a}$ and $\delta^k\overline{b}$ the disjoint permutation $\sigma$ can only be the identity. $\delta^k\overline{a}$ and $\delta^k\overline{b}$ having the same degree $k$ we deduce that $i=d^{-1}$. So $\delta^k\overline{a}=\delta^k\overline{b}$ and $f'=id_{\delta^k\overline{a}}$. It follows that $f$ is the unique disjoint map $a\to b$.

$G:\textup{RegSt}\left(\G\right)\to \quot{\Stream}{\sim_s}$ is full.

Let $D:a\to b$ be a diagram of $\Stream$ where $a$ and $b$ are stratified types. Let $d$ be the biggest integer such that there is a wire of type $\D^d 1$ or $\D^d \omega$ appearing in $D$. The degree of $a$ and $b$ must be less than $d$ so there is a diagram $D':\delta^d a\to \delta^d b$ such that $D\sim_s D'$.

Using the axioms of delayed trace we take them out of the diagrams to obtain something of the form:

We use $\left(\triangleleft \triangleright\right)$ and $\left(\triangleright\right)$ until all the delayed trace on types $\D^{k+1}\omega$ and $\D^{k}\omega$ becomes on types
$\D^{d+1}\omega$ and $\D^{d}\omega$.

$\tikzfig{nf0}\stackrel{\left(\triangleleft \triangleright\right)}{=}\tikzfig{nf1}\stackrel{\left(\triangleright\right)}{=}\tikzfig{nf2}$

Then since $d$ was the biggest delay appearing in the diagram before we know that all the delayed trace on types $\D^{k}\omega$ are in the situation:

Now using $\left(\triangleleft \triangleright\right)$ on all wires of type $\D^k\omega$ with $k<d$, and then using $\left(\blacktriangleright\right)$ and $\left(\blacktriangleleft\right)$ we can ensure that the only generators of the form $\D^k\omega G$ are in fact of the form $\D^d \omega G$.

0.8$\tikzfig{nf4}\stackrel{\left(\triangleleft \triangleright\right)}{=}\tikzfig{nf5}\stackrel{\left(\blacktriangleright\right)}{=}\tikzfig{nf6}$

Then applying $\left(\triangleright \triangleleft\right)$ we remove all the remaining wires of type $\D^k\omega $ with $k<d$. Now the only $\D^k\omega $ wires in the diagrams are the $\D^{d}\omega$ and the $\D^{d+1}\omega$ in the delayed trace, so there are no derivations left in the diagram and the only initialisations left are the one connected to delayed traces. We can now group together the generators $\D^k \iota g$ and $\D^d \omega g$ of same type. This gives a diagram of the form:

Which is the image of a regular stateful morphism sequence. So for each diagram $D$ there is a diagram $D'$ such that $D\sim_s D'$ and $D'$ is the image of a stateful morphism sequence. In other words, $G:\textup{RegSt}\left(\G\right)\to \quot{\Stream}{\sim_s}$ is full.

$f\equiv g \Leftrightarrow G(f)=G(g)$

We want to prove

\[ \AX \vdash G(f) = G(g) \iff \CM,\IM \vdash f = g\]

For that, we simply match the set of derivation trees on the left hand side to the set of derivation trees on the right hand side.
We first look at the deduction rules, which are the rules of a congruence (reflexivity, symmetry, transitivity, composition, monoidal product) plus the coinduction rule. There is a one-to-one correspondence between the rules on both side, relying on $G(\D f) = \D G(f)$ for the correspondence between the two coinduction rules. We just need to match the axioms:

* All the axioms of $\AX$ but $(\ground),(\pi),(\sigma)$ correspond to tautologies.

* $(\ground)$ is exactly matched to $\CM$.

* $(\pi)$ is exactly matched to $\IM$.

* $(\sigma)$ correspond to either a tautology or $\CM$ depending on whether the permuted types are disjoints or not.

§.§ Pseudo-Purifiable and Shadow Categories

In a pseudo-purifiable category $(\C,\otimes,I,\Terre{})$, $\preceq$ is transitive, is preserved under composition and monoidal product, hence forms a pre-order enrichment of $\C$.

The preservation under composition and monoidal product are direct to prove. For the transitivity, we assume that $f \preceq g \preceq h$. Using the definition of $\preceq$, we obtain $f_0,g_0,g_1,h_1$ such that:

$f = \tikzfig{g0_f0} \qquad \qquad g = \tikzfig{g0_ground}$

$g = \tikzfig{h1_g1} \qquad \qquad h = \tikzfig{h1_ground}$

We then take $f_0',g_0',g_1',h_1'$ pseudo-purifications of $f_0,f_0,g_1,h_1$. In particular, we have $g_0' \in \Pure(g)$. Since $\C$ is pseudo-purifiable, we know that we also have

\[ \tikzfig{h1_g1_pure} \in \Pure(g) \]

Using uniqueness of pseudo-purifications up to a causal morphism, we know that there exists $c$ causal such that:

\[ g_0' = \tikzfig{h1_g1_pure_c} \]

It follows that

\[ f = \tikzfig{h1_g1_pure_c_f0} \]

Hence $f \preceq h$.

The categories $\CPM$ and $\UCPM$ are pseudo-purifiable categories. Moreover, every purification (for the usual notion of purity, see Section <ref>) is a pseudo-purification.

We start by showing the second property. We consider a purification of $f$, which is a decomposition $f = (\id \otimes \Terre{}) \circ p$ with $p$ a pure quantum computation, and want to prove that $p \in \Pure(f)$. In other words, for every $g$ such that $f = (\id \otimes \Terre{}) \circ g$, we have to find a causal morphism $c$ such that $g = (\id \otimes c) \circ p$.

To do so, we purify $g$ into $g = (\id \otimes \Terre{}) \circ q$, with $q$ a pure quantum computation. We note that both $p$ and $q$ are purifications of $f$, so using <ref>, we know that there exists an isometry $v$ such that $q = (\id \otimes v) \circ p$ or and isometry $v'$ such that $p = (\id \otimes v') \circ q$.

In the former case, we have $g = (\id \otimes \Terre{}) \circ q = (\id \otimes \Terre{}) \circ  (\id \otimes v) \circ p$, so we can take $c = \Terre{} \circ v$, which is causal.

In the latter case, we use the fact that every isometry can be seen as an injection followed by a change of basis, and decompose the isometry $v' \in \CPM(A,B)$ with $\dim(A) = 2^n$ and $\dim(B) = 2^{n+k}$ into $v' = u \circ (\id \otimes \ket{0^k})$ for some unitary $u$. So we have
$(\id_A \otimes \Terre{\CC^{2^k}}) \circ u^\dagger \circ v' = \id_A$, and it follows that:

\[ g = (\id \otimes \Terre{}) \circ (\id_A \otimes \Terre{\CC^{2^k}}) \circ u^\dagger \circ p\]

We can take $c = (\id \otimes \Terre{}) \circ (\id_A \otimes \Terre{\CC^{2^k}}) \circ u^\dagger$, which is causal.

We now want to prove that $\CPM$ and $\UCPM$ are pseudo-purifiable. Since every morphism has a purification, and every purification has a pseudo-purification, then every morphism has a pseudo-purification. In fact, the set of pseudo-purifications of $f$ is exactly the set of morphisms $g$ that are linked to a purification $p$ in both following ways:

* $g$ can be decomposed into $g = (\id \otimes c) \circ p$ with $c$ a causal morphism

* $p$ can be decomposed into $p = (\id \otimes c') \circ g$ with $c'$ a causal morphism

Using this characterisation, and the fact that purity is preserved under composition and tensor, the preservation of pseudo-purification under composition is direct, hence $\CPM$ and $\UCPM$ are pseudo-purifiable categories.

Every cartesian category $(\C,\times,I)$ is pseudo-purifiable, and for every $f \in \C(A,B)$, the pairing $(f,\id_A) \in \C(A,B \times A)$ is one of the pseudo-purifications of $f$.

We will show that for $f \in \C(A,B)$, $\Pure(f)$ is exactly the set of $(f,g)$ with $g \in \C(A,C)$ left-invertible, i.e., there exists $h \in \C(C,A)$ such that $h \circ g = \id_A$. We take $f,g,h$ as such.

We consider a morphism $p \in \C(A,B \times X)$ such that $(A \times \Terre{X}) \circ p = f$. Since $\C$ is a cartesian category, we know that there exists $f',g'$ such that $p = (f',g')$, and we immediately have $f = f'$. We have

\[ p = (f,g') = (B \times (g' \circ h)) \circ (f,g) \]

Since very morphism is causal, $g' \circ h$ is causal, and it follows that $(f,g)$ is indeed a pseudo-purification of $f$. The stability of pseudo-purifications under composition is direct.

The categories $\CPM$ and $\UCPM$ are shadow pseudo-purifiable. In fact, all the morphisms that are pure quantum computations are shadowful morphisms.

While a simpler proof exists for $\CPM$, we present here a proof that holds for both $\CPM$ and $\UCPM$. This means that we cannot take the shadows $\pi$ to be orthonormal projectors, as orthonormal projectors are not trace preserving (except for the identity).

We start by treating the special case of the zero morphism $0_{A,B} \in \CPM(A,B)$. The morphism $0_{B_1,B_1} \in \CPM(B_1,B_1)$ is always a valid shadow, hence $0_{A,B}$ is shadowful.

As isomorphisms are pure quantum computation, to prove that all the pure quantum computations are shadowful, it is enough to prove the following: for $f \in \CPM(A,B_0 \otimes B_1)$ which is a pure quantum computation and not the zero morphism, there exists $\pi \in \UCPM(B_1,B_1)$ such that:

$\forall g,h,\quad\begin{matrix} \tikzfig{shadow_simple_f_g} = \tikzfig{shadow_simple_f_h} \\ \iff \\ \tikzfig{shadow_simple_pi_g} = \tikzfig{shadow_simple_pi_h}  \end{matrix}$

To do so, we proceed as follows.
Since $f$ is a pure quantum computation, we can consider its corresponding morphism $F \in \bfup{Hilb}(A,B_0 \otimes B_1)$. We consider its image $\textup{im}_{B_1}(F)$ projected on $B_1$, which is a subspace of $B_1$, and a non-trivial one as $f$ is not the zero morphism. We choose an orthonormal basis $(\beta_1,\dots,\beta_k)$ of $\textup{im}_{B_1}(F)$ (with $k \geq 1$), and complete it into an orthonormal basis $(\beta_1,\dots,\beta_n)$ of $B_1$.
We define the morphism $P \in \bfup{Hilb}(B_1,B_1 \otimes B_1)$ as the unique linear operator such that

\[ \forall 1 \leq i \leq k, P(\beta_i) = \beta_i \otimes \beta_1 \]

\[ \forall k+1 \leq i \leq n, P(\beta_i) = \beta_1 \otimes \beta_i \]

Since $P$ is isometric, it corresponds to a morphism $p \in \UCPM(B_1,B_1 \otimes B_1)$, we now define $\pi := (B_1 \otimes \Terre{B_1}) \circ p$. Intuitively, $\pi$ projects everything which is not in the image of $f$ to $\beta_1$, while being the identity on the image of $f$. Formally, each of the $\beta_i$ corresponds to a pure morphism $b_i \in \UCPM(I,B_1)$ and we have

\[\forall 1 \leq i \leq k, \pi \circ b_i = b_i \]

\[\forall  k+1 \leq i \leq n, \pi \circ b_i = b_1 \]

The morphism $\pi$ is idempotent, and since $\pi \circ f = f$, the upward direction of our equivalence is immediate. Proving the downward direction is more complex.

We consider $g,h$ morphisms of $\CPM$ such that

\[ \tikzfig{shadow_simple_f_g} = \tikzfig{shadow_simple_f_h}\]

Using <ref>, we know that we can find pseudo-purifications which are pure quantum computations, so let $g',h'$ be such pseudo-purifications. Since $f$ is already pure, we can use <ref> on $g' \circ f$ and $h' \circ f$, and find an isometry $v$ such that $(\id \otimes v) \circ g' \circ f = h' \circ f$, or an isometry $v'$ such that $g' \circ f = (\id \otimes v) \circ h' \circ f$. Without loss of generality, we assume we have the former.

We write $F,G',H',V$ for the morphisms of $\bfup{Hilb}$ corresponding to $f,g',h'$ and $v$ respectively. We have:

&  \tikzfig{shadow_simple_f_g}& =& \tikzfig{shadow_simple_f_h} \\&&\Downarrow&\\
& \tikzfig{shadow_simple_f_g_prime} &=& \tikzfig{shadow_simple_f_h_prime}  \\&&\Downarrow&\\
& \tikzfig{shadow_simple_f_g_prime_Hilb} &=& \tikzfig{shadow_simple_f_h_prime_Hilb}  \\&&\Downarrow&\\
\forall 1 \leq i \leq k,&  \tikzfig{shadow_simple_beta_g} &=& \tikzfig{shadow_simple_beta_h} \\&&\Downarrow&\\
\forall 1 \leq i \leq k,& \tikzfig{shadow_simple_beta_pi_g} &=& \tikzfig{shadow_simple_beta_pi_h} \\&&\Downarrow&\\
%	\end{matrix}$}\\
%	\scalebox{0.9}{$\begin{matrix}
\forall 1 \leq i \leq n,& \tikzfig{shadow_simple_beta_pi_g} &=& \tikzfig{shadow_simple_beta_pi_h} \\&&\Downarrow&\\
& \tikzfig{shadow_simple_p_g_Hilb} &=& \tikzfig{shadow_simple_p_h_Hilb} \\&&\Downarrow&\\
& \tikzfig{shadow_simple_p_g} &=& \tikzfig{shadow_simple_p_h} \\&&\Downarrow&\\
& \tikzfig{shadow_simple_pi_g} &=& \tikzfig{shadow_simple_pi_h} \\
\end{matrix}$

§.§ Soundness

We note that $\CM,\IM \vdash \alpha = \beta$ means by definition $\alpha \equiv \beta$.

Whenever $\CM,\IM \vdash \alpha = \beta$, for every $k \geq 1$ we have $\fa{\alpha}_k = \fa{\beta}_k$

For $n \geq 0$ with define the congruence “equal up until the $n$-th tick” $\approx_n$ on $\RegStSeq{\C}$ as follows:

\[ \alpha \approx_n \beta \iff \forall k \leq n, \fa{\alpha}_k = \fa{\beta}_k \]

In particular we always have $\alpha \approx_0 \beta$. The property we are trying to prove is equivalent to:

\[\forall n \geq 0, \left[\CM,\IM \vdash \alpha = \beta\right] \implies \alpha \approx_n \beta \]

The start by showing that the axioms $\CM$ and $\IM$ are indeed sound:

*  Moving a causal from the $k$-th layer to the $(k+1)$-th layer trivially preserve all the finite approximations but the $k$-th one. Looking at the $k$-th finite approximation, and we observe the following:

$\begin{matrix} \fa{\alpha}_k &=& \tikzfig{onion_from_strat_bis_plus_causal}\\
&= & \tikzfig{onion_from_strat_bis} & = & \fa{\beta}_k \end{matrix}$

*  Duplicating an idempotent from the $k$-th layer to the $(k+1)$-th layer does not change any of the associated finite approximations.

We now show that whenever $\Gamma \vdash \alpha = \beta$, if for all $\left[ \alpha' = \beta'\right] \in \Gamma$ we have $\alpha' \approx_{n} \beta'$ then we have $\alpha \approx_{n} \beta$.

We take a derivation sequence of $\Gamma \vdash \alpha = \beta$, and proceed by induction on this derivation sequence.

* The initialisation is the axiom rule $\Gamma \vdash \alpha = \beta$ with $\left[ \alpha = \beta\right] \in \Gamma$. The result is immediate.

* The reflexivity, symmetry, transitivity rules are trivial, and the composition and tensor rules correspond to the fact that $\fa{-}_k$ is a monoidal functor.

* We now consider the coinduction rule

$(\forall k \geq 0) \qquad  \Gamma,\left[\D \alpha^{(k+1)} = \D \beta^{(k+1)}\right] \vdash \alpha^{(k)} = \beta^{(k)}$
$\Gamma \vdash \alpha^{(0)} = \beta^{(0)}$

We want to show that if for every $\left[ \alpha' = \beta'\right] \in \Gamma$ we have $\alpha' \approx_{n} \beta'$, then we have $\alpha^{(0)} \approx_n \beta^{(0)}$ for all $n \geq 0$.

We assume that we indeed have for every $\left[ \alpha' = \beta'\right] \in \Gamma$ we have $\alpha' \approx_{n} \beta'$.
By induction hypothesis we know that if  $\D \alpha^{(k+1)} \approx_{n} \D \beta^{(k+1)}$ for some $k \geq 0$ and $n \geq 0$, then $\alpha^{(k)} \approx_{n} \beta^{(k)}$, which implies $\D \alpha^{(k)} \approx_{n+1} \D \beta^{(k)}$. Hence by chaining this property, we obtain that for any $k \geq 0$, $n \geq 0$:
\[ \D \alpha^{(k+1)} \approx_{n} \D \beta^{(k+1)} \implies  \alpha^{(0)} \approx_{n+k} \beta^{(0)} \]

Applying it with $n = 0$, and using the fact that $\approx_{0}$ is the total relation, we obtain for all $k \geq 0$

\[ \alpha^{(0)} \approx_{k} \beta^{(0)} \]

§.§ Universality

In this subsection, we prove the fullness of $\fa{-}$.

If $\C$ is pseudo-purifiable, then the functor $\fa{-} : \RegStSeq{\C} \to \Onion$ is full.

We take $(f_k)_{k \geq 1} \in \Onion(\fa{A},\fa{B})$. By regularity, there is a $n$ and a $f^{\textup{ref}}$ and $f^{\textup{irreg}}$ such that for every $k \geq n$ we have

$f_k = \tikzfig{regularity}$

Since $\C$ is pseudo-purifiable, we can pseudo-purify its morphisms, so for every $k \geq 1$ we write $p(f_k)$ for an arbitrarily chosen pseudo-purification of $f_k$.

We want to build $\alpha \in \RegStSeq{\C}(A,B)$ such that $\fa{\alpha}=(f_k)_{k \geq 1}$. We build $\alpha$ inductively, ensuring that at all rank $k < n$ we have that

\[ p(f_k)= \tikzfig{open_onion_from_strat}  \]

This ensures that we always have

\[ f_k = \tikzfig{onion_from_strat_bis} \]

* Initialisation: we simply take $\alpha_1 = p(f_1)$.

* Irregular part: We assume that for $k < n-1$ we have $\alpha_1,\dots,\alpha_k$ already defined and satisfying the hypothesis. By monotonicity, we know that we have

$\tikzfig{monotone_succ} \preceq \tikzfig{monotone_pred}$

So using the definition of $\preceq$ we have $g \in \C(\fa{A}_{k+1},\fa{B}_k \otimes Y)$ and $h \in \C(Y,I)$ such that

$\tikzfig{mono_succ} = \tikzfig{mono_dec_succ}$

$\tikzfig{mono_dec_pred} = \tikzfig{mono_pred}$

In those equation, we consider stateful morphisms $h \in \C(\text{In} \otimes M, \textup{Out} \otimes M')$ which we represent by having the initial state $M$ and final state $M'$ “vertical” while the standard input and output are “horizontal”. While this could be formalise in the context of a double category, we only use it here as a diagrammatic notation: we read diagrams from up/left to right/down.

We choose $p(g)$ and $p(h)$ two pseudo-purifications of respectively $g$ and $h$, and we obtain the following:

$\tikzfig{pure_mono_succ} = \tikzfig{pure_dec_succ}$

$\tikzfig{pure_dec_pred} = \tikzfig{pure_mono_pred}$

Using uniqueness of pseudo-purification up to a causal morphism, we obtain two causal morphisms $c$ and $d$ such that

$\tikzfig{pure_mono_succ_bis} = \tikzfig{pure_dec_succ_bis}$

$\tikzfig{pure_dec_pred_bis} = \tikzfig{pure_mono_pred_bis}$

It follows that

$\tikzfig{pure_mono_succ_bis} = \tikzfig{pure_recap}$

We then define $\alpha_{k+1} =  c \circ (\id \otimes p(h)) \circ d$. By construction, it satisfies the hypothesis.

* Regular part: for $k \geq n$ we simply take $\alpha_k = f^{\textup{reg}}$.

By construction, we have $\fa{\alpha} = (f_k)_{k \geq 1}$, hence $\fa{-}$ is full.

§.§ Completeness

In this subsection, we prove the completeness of $\fa{-}$. We start by a few lemmas.

In a category $\C$, if $\pi : X \to X$ is a shadow of a shadowful morphism $f \in \C(A,B \otimes X)$ then

\[ (\id_B \otimes \pi) \circ f = f \]

Using the definition of a shadowful morphism, we obtain

\[ (\id_B \otimes \pi) \circ f = f \iff \pi \circ \pi = \pi \]

In a pseudo-purifiable category, if $f \in \C(A,B)$, $g \in \C(A,B \otimes X)$, $p \in \Pure(g)$, and

\[f = \tikzfig{purification_G}\]

then we have $p \in \Pure(f)$.

Since $f$ is $g$ composed with the discard, then a pseudo-purification of $G$ composed with a pseudo-purification of $\Terre{X}$ gives a pseudo-purification of $f$. The identity morphism $\id_X$ is a pseudo-purification of $\Terre{X}$.

If $\C$ is a shadow pseudo-purifiable category, whenever $\fa{\alpha} = \fa{\beta}$ there exists $\alpha',\beta'$ such that $\fa{\alpha'} = \fa{\beta'}$ and

\[ \CM,\IM,[\D \alpha' = \D \beta'] \vdash \alpha = \beta \]

We take $\alpha,\beta \in \RegStSeq{\C}(A,B)$ such that $\fa{\alpha} = \fa{\beta}$. We take $p(\alpha_1)$ a shadowful pseudo-purification of $\alpha_1$, and $p(\beta_1)$ a shadowful pseudo-purification of $\beta_1$. Using Lemma <ref>, we note that $p(\alpha_1)$ is also a pseudo-purification of $f_1$, and so is $p(\beta_1)$. So using uniqueness of the pseudo-purification up to a causal morphisms, there exists $c$ causal such that:

$\tikzfig{compl_a1} = \tikzfig{compl_pa1g} \qquad \tikzfig{compl_b1} = \tikzfig{compl_pa1Cg}$

Since $\C$ is a shadow category, we write $\pi$ for the (idempotent) shadow of $p(\alpha_1)$, and from Lemma <ref> we have

$\tikzfig{compl_a1} = \tikzfig{compl_pa1PIg} \qquad \tikzfig{compl_b1} = \tikzfig{compl_pa1PICg}$

Using the fact that the discard is causal and $\pi$ is idempotent, we can rewrite $\alpha$ using $\IM$ and $\CM$ as follows:

$\alpha = \tikzfig{compl_a_exp} \equiv \tikzfig{compl_a_eq} = (\id_{B_1} \otimes \D \alpha') \circ \gamma'$

where $\alpha'$ and $\gamma'$ are defined as follows:

$\tikzfig{compl_c_prime} \df \tikzfig{compl_c_prime_def} \qquad \tikzfig{compl_a_prime} \df \tikzfig{compl_a_prime_def} $

Similarly, using the fact that $\C$ and the discard are causal and $\pi$ is idempotent, we can rewrite $\beta$ using $\IM$ and $\CM$ as follows:

$\beta = \tikzfig{compl_b_exp} \equiv \tikzfig{compl_b_eq} = (\id_{B_1} \otimes \D \beta') \circ \gamma'$

where $\gamma'$ is defined above and $\beta'$ is defined as follows:

$\tikzfig{compl_b_prime} \df \tikzfig{compl_b_prime_def}$

So we found $\alpha',\beta',\gamma'$ such that

\[\CM,\IM \vdash \alpha = (\id_{B_1} \otimes \D \alpha') \circ \gamma'\]

\[\CM,\IM \vdash \beta = (\id_{B_1} \otimes \D \beta') \circ \gamma' \]

This means that

\[ \CM,\IM, \left[\D \alpha' = \D \beta'\right] \vdash \alpha = \beta \]

We still need to prove that $\fa{\alpha'} = \fa{\beta'}$. Since $\fa{\alpha} = \fa{\beta}$ and $\fa{-}$ is sound with respect to $\CM$ and $\IM$ (Lemma <ref>) we know that we have:

$\fa{\tikzfig{compl_a_eq_bis}} = \fa{\tikzfig{compl_b_eq_bis}}$

Since $\pi$ is a shadow of $p(\alpha_1)$, then it is equivalent to:

$\fa{\tikzfig{compl_a_prime_def}} = \fa{\tikzfig{compl_b_prime_def}}$

hence $\fa{\alpha'} = \fa{\beta'}$

Whenever $\fa{\alpha} = \fa{\beta}$ we have $\CM,\IM \vdash \alpha = \beta$.

We chain the use of lemma <ref> and obtain two sequences $\alpha^{(n)}$ and $\beta^{(n)}$ such that $\alpha^{(0)} = \alpha$, $\beta^{(0)}= \beta$ and for all $n \geq 0$ we have

\[ \CM,\IM,[\D \alpha^{(n+1)} = \D \beta^{(n+1)}] \vdash \alpha^{(n)} = \beta^{(n)} \]

Using the coinduction rule this implies
\[\CM,\IM \vdash \alpha = \beta\]