# Two linearities for quantum computing in the lambda calculus

Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi

► To cite this version:

Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi. Two linearities for quantum computing in the lambda calculus. BioSystems, 2019. hal-02909128

HAL Id: hal-02909128

https://inria.hal.science/hal-02909128

Submitted on 30 Jul 2020

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Two linearities for quantum computing
in the lambda calculus☆,☆☆

Alejandro Díaz-Caro<sup>a,b</sup>, Gilles Dowek<sup>c</sup>, Juan Pablo Rinaldi<sup>d</sup>

<sup>a</sup>CONICET-UBA, ICC, Pabellón 1, Ciudad Universitaria, Buenos Aires, Argentina.

<sup>b</sup>Universidad Nacional de Quilmes, R. Sáenz Peña 352, Bernal, BA, Argentina

<sup>c</sup>Inria, LSV, ENS Paris-Saclay, 61, avenue du Président Wilson, Cachan, France

<sup>d</sup>Universidad Nacional de Rosario, Pellegrini 250, Rosario, SF, Argentina

**Abstract**

We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.

**Keywords:** quantum computing, lambda-calculus, algebraic linearity, linear logic, measurement

**1. Introduction**

Extending λ-calculus into a programming language for quantum computing requires to add, besides the usual abstraction and application symbols, a sum and a product to build linear combinations of terms, and a tensor-product like symbol to include datatypes composed of several qubits. Yet, mixing all the constructs in a naive way leads to a too powerful calculus where non linear, that is non physical functions, can be defined. For instance, in λ-calculus, applying the term λx.(x ⊗ x), that expresses a non-linear function for some convenient definition of ⊗, to a term u yields the term (λx.(x ⊗ x))u, that reduces to u ⊗ u. But “cloning” this vector u is forbidden in quantum computing. Various quantum λ-calculi address this problem in different ways.

<footnote>☆This paper extends a paper presented at TPNC’17 by the first two authors [1] and the third author *Licenciatura’s* thesis [2].</footnote>

<footnote>☆☆Partially supported by the ECOS Project A17C03 QuCa, PICT-PRH 2015-1208, and the Laboratoire International Associé SINFIN.</footnote>

<footnote>Email addresses: adiazcaro@icc.fcen.uba.ar (Alejandro Díaz-Caro), gilles.dowek@ens-paris-saclay.fr (Gilles Dowek), juampi.rinaldi@gmail.com (Juan Pablo Rinaldi)</footnote>
One way is to forbid the construction of the term $\lambda x.(x \otimes x)$ using a typing system inspired from linear logic [3, 4], leading to logic-linear calculi [5, 6, 7, 8, 9]. Another is to define the operational semantics in such a way that every $\lambda$-term represents a linear function. The term $\lambda x.(x \otimes x)$, for instance, expresses the linear function that maps $|0\rangle$ to $|0\rangle \otimes |0\rangle$ and $|1\rangle$ to $|1\rangle \otimes |1\rangle^1$. This leads to restrict beta-reduction to the case where $u$ is a base vector (in the computational basis) and to add the linearity rule $f(u + v) \rightarrow (fu +fv)$, leading to algebraic-linear calculi [10, 11, 12, 13, 14].

Each solution has its advantages and drawbacks. For example, let $t?u:v$ be the conditional statement on $|0\rangle$ and $|1\rangle$. Interpreting $\lambda$-terms as algebraic-linear functions permits to reduce the term $(\lambda x.x?|0\rangle\cdot|1\rangle)(\alpha. |0\rangle + \beta. |1\rangle)$ to $(\alpha.(\lambda x.x?|0\rangle\cdot|1\rangle)|0\rangle + \beta.(\lambda x x?|0\rangle\cdot|1\rangle)|1\rangle)$ then to $(\alpha. |1\rangle + \beta. |0\rangle)$, instead of reducing it to the term $(\alpha. |0\rangle + \beta. |1\rangle)?|0\rangle\cdot|1\rangle$ that would be blocked. This explains that this linearity rule, that is systematic in the algebraic-linear languages cited above, is also present for the condition in [5] (the so-called **if** $\circ$ operator).

However, interpreting all $\lambda$-terms as linear functions forbids to extend the calculus with non-linear operators, such as measurement. For instance, the term $(\lambda x.\pi x)(|0\rangle + |1\rangle)$, where $\pi$ represents a measurement in the computational basis, would reduce to $((\lambda x.\pi x)|0\rangle + (\lambda x.\pi x)|1\rangle)$, while it should reduce to $|0\rangle$ with probability $\frac{1}{2}$ and to $|1\rangle$ with probability $\frac{1}{2}$.

In this paper, we propose a way to unify the two approaches, distinguishing duplicable and non-duplicable data by their type, like in the logic-linear calculi; and interpreting $\lambda$-terms as linear functions, like in the algebraic-linear calculi, when they expect duplicable data. We illustrate this idea with an example of such a calculus.

In this calculus, a qubit has type $\mathbb{B}$ when it is in the computational basis, hence duplicable (a non-linear term in the sense of linear logic), and $S(\mathbb{B})^2$ when it is a superposition, hence non-duplicable (a linear term in the sense of linear logic). Hence, we can distinguish a basis term, from a term in the span of such a basis. We could also state that the term $|0\rangle \otimes (|0\rangle + |1\rangle)$ has type $\mathbb{B} \otimes S(\mathbb{B})$. However, giving this type to this term and the type $S(\mathbb{B} \otimes \mathbb{B})$ to the term $(|0\rangle \otimes |0\rangle + |0\rangle \otimes |1\rangle)$ would jeopardize the subject reduction property as, using the bilinearity of the tensor product, the former should develop to the latter. This dilemma is not specific to quantum computing as computing is often a non-reversible process where some information is lost. For instance, if we express, in its type, that the term $(X-1)(X-2)$ is a product of two polynomials, developing it to $X^2 - 3X + 2$ does not preserve this type. Therefore, instead of a bilinear tensor product, we will use $n$-ary Cartesian products, so the term $|0\rangle \times (|0\rangle + |1\rangle)$ has type $\mathbb{B} \times S(\mathbb{B})$, and to move from this type to $S(\mathbb{B} \times \mathbb{B})$ we use an explicit cast. Notice that, if $\mathbb{B}$ is a set of vectors and $S(A)$ is the span of the set $A$, then $S(\mathbb{B} \times \mathbb{B})$ is isomorphic to $S(\mathbb{B}) \otimes S(\mathbb{B})$. Hence, the term

<footnote n="1">¹Where $|x\rangle$ is the Dirac notation for vectors, with $|0\rangle = (\begin{matrix} 1 \\ 0 \end{matrix}) \in \mathbb{C}^2$ and $|1\rangle = (\begin{matrix} 0 \\ 1 \end{matrix}) \in \mathbb{C}^2$, so $\{|0\rangle, |1\rangle\}$ is an orthonormal basis of $\mathbb{C}^2$, called here the "computational basis".</footnote>

<footnote n="2">²$S$ for superposition and also for the Span of $\mathbb{B}$.</footnote>
$|0\rangle \times (|0\rangle + |1\rangle)$ has type $\mathbb{B} \times S(\mathbb{B})$ and it cannot be reduced. But the term $\uparrow |0\rangle \times (|0\rangle + |1\rangle)$, where $\uparrow$ is used as a mark to allow casting, has type $S(\mathbb{B} \times \mathbb{B})$ and can be developed to $(|0\rangle \times |0\rangle + |0\rangle \times |1\rangle)$.

This language permits expressing quantum algorithms with a very precise information about the nature of the data processed by these algorithms.

*Outline of the paper.* Section 2 introduces some basic notations and concepts of quantum computing. In Section 3 we introduce the calculus, without product. In Section 4 we extend the language with a *n*-ary Cartesian product for multiple-qubits systems. In Section 5 we state and prove the Subject Reduction property. In Section 6 we state and prove the Strong Normalization property. Then, in Section 7 we provide a straightforward interpretation of the calculus considering base types as sets of vectors, and types $S(\cdot)$ as vector spaces. In Section 8 we express two non-trivial example in our calculus: the Deutsch algorithm and the Teleportation algorithm, demonstrating the expressivity of the proposed language. Finally, in Section 9, we conclude. There are also two appendices, Appendix D and Appendix E, which have more details of the examples given in Section 8.

## 2. Basics notions of quantum computing

This section does not intend to introduce a full description of quantum computing, the interested reader can find actual introductions to this area in many textbooks, e.g. [15, 16]. This section only intends to introduce some basic notations and concepts.

In quantum computation, data is expressed by normalised vectors in Hilbert spaces. For our purpose, this means that the vector spaces are defined over complex numbers and come with a norm and a notion of orthogonality. The smallest space usually considered is the space of *qubits*. This space is the two-dimensional vector space $\mathbb{C}^2$, and it comes with a chosen orthonormal basis denoted by $\{|0\rangle, |1\rangle\}$. A qubit (or quantum bit) is a normalised vector $\alpha|0\rangle + \beta|1\rangle$, where $|\alpha|^2 + |\beta|^2 = 1$. To denote an unknown qubit $\psi$ it is common to write $|\psi\rangle$. A two-qubits vector is a normalised vector in $\mathbb{C}^2 \otimes \mathbb{C}^2$, that is, a normalised vector generated by the orthonormal basis $\{|00\rangle, |01\rangle, |10\rangle, |11\rangle\}$, where $|xy\rangle$ stands for $|x\rangle \otimes |y\rangle$. In the same way, a *n*-qubits vector is a normalised vector in $(\mathbb{C}^2)^n$ (or $\mathbb{C}^N$ with $N = 2^n$). Also common is the notation $\langle\psi|$ for the transposed, conjugate of $|\psi\rangle$, e.g. if $|\psi\rangle = [\alpha_1, \alpha_2, \dots, \alpha_n]^T$, then $\langle\psi| = [\alpha_1^*, \alpha_2^*, \dots, \alpha_n^*]$ where for any $\alpha \in \mathbb{C}$, $\alpha^*$ denotes its conjugate.

The operators on qubits that are considered in this paper are the *quantum gates*, that is, unitary operators. An *unitary operator* is an invertible linear function preserving the norm and the orthogonality of vectors. The *adjoint* of a given operator $U$ is denoted by $U^\dagger$, and the unitary condition imposes that $U^\dagger U = \text{Id}$. These functions are linear, and so it is enough to describe their action on the base vectors. Another way to describe these functions would be by matrices, and then the adjoint is just its conjugate transpose. A set of
universal quantum gates is the set cnot, $R_{\pi/4}$ and had, which can be defined as follows:

**The cnot gate.** The controlled-not is a two-qubits gate which only changes the second qubit if the first one is $|1\rangle$:

$$ cnot |0x\rangle = |0x\rangle $$

$$ cnot |1x\rangle = |1\rangle \otimes not |x\rangle $$

where not $|0\rangle = |1\rangle$ and not $|1\rangle = |0\rangle$.

**The $R_{\pi/4}$ gate.** The $R_{\pi/4}$ gate is a single-qubit gate that modifies the phase of the qubit:

$$ R_{\pi/4} |0\rangle = |0\rangle $$

$$ R_{\pi/4} |1\rangle = e^{i\pi/4} |1\rangle $$

where $\pi/4$ is the phase shift.

**The H gate.** The Hadamard gate is a single-qubit gate which produces a 45 degree rotation of the basis:

$$ H |0\rangle = \frac{1}{\sqrt{2}} |0\rangle + \frac{1}{\sqrt{2}} |1\rangle $$

$$ H |1\rangle = \frac{1}{\sqrt{2}} |0\rangle - \frac{1}{\sqrt{2}} |1\rangle $$

To make these gates act in higher-dimension qubits, they can be put together with the bilinear symbol $\otimes$. For example, to make the Hadamard gate act only in the first qubit of a two-qubits register, it can be taken to $H \otimes Id$, and to apply a Hadamard gate to both qubits, just $H \otimes H$.

An important restriction, which has to be taken into account if a calculus pretends to encode quantum computing, is the so called no-cloning theorem [17]:

**Theorem 2.1 (No cloning).** There is no linear operator such that, given any qubit $|\phi\rangle \in \mathbb{C}^N$, can clone it. That is, it does not exist any unitary operator $U$ and fixed $|\psi\rangle \in \mathbb{C}^N$ such that $U |\psi\phi\rangle = |\phi\phi\rangle$.

**PROOF.** Assume there exists such an operator $U$, so given any $|\phi\rangle$ and $|\phi\rangle$ one has $U |\psi\phi\rangle = |\phi\phi\rangle$ and also $U |\psi\phi\rangle = |\phi\phi\rangle$. Then

$$ \langle U\phi\psi|U\psi\phi\rangle = \langle\phi\phi|\phi\phi\rangle \quad (1) $$

where $\langle U\phi\psi|$ is the conjugate transpose of $U |\psi\phi\rangle$. However, notice that the left side of equation (1) can be rewritten as

$$ \langle\phi\psi|U^\dagger U |\psi\phi\rangle = \langle\phi\psi|\psi\phi\rangle = \langle\phi|\phi\rangle $$
While the right side of equation (1) can be rewritten as

$$ \langle\varphi|\phi\rangle\langle\varphi|\phi\rangle = \langle\varphi|\phi\rangle^2 $$

So $\langle\varphi|\phi\rangle = \langle\varphi|\phi\rangle^2$, which implies either $\langle\varphi|\phi\rangle = 0$ or $\langle\varphi|\phi\rangle = 1$, none of which can be assumed in the general case, since $|\varphi\rangle$ and $|\phi\rangle$ were picked as random qubits. $\square$

The implication of this theorem in the design choices of a calculus is that it must be forbidden to allow functions duplicating arbitrary arguments. However, notice that this does not forbid cloning some specific qubit states. Indeed, for example the qubits $|0\rangle$ and $|1\rangle$ can be cloned without much effort by using the cnot gate: $cnot|00\rangle = |00\rangle$ and $cnot|10\rangle = |11\rangle$. In this sense, the imposed restriction is not a resources-aware restriction à la linear logic [3]. It is a restriction that forbids us from creating a ‘universal cloning machine’, but still allows us to clone any given known term.

Another operation considered on qubits is the measurement. A projector is an operator of the form $|\phi\rangle\langle\phi|$. For example, in the canonical base $\{|0\rangle, |1\rangle\}$ of $\mathbb{C}^2$, $P_0 = |0\rangle\langle0|$ is a projector and $P_1 = |1\rangle\langle1|$ is another projector, with respect to such a base. Indeed,

$$ \begin{aligned} P_0(\alpha |0\rangle + \beta |1\rangle) &= \alpha P_0 |0\rangle + \beta P_0 |1\rangle \\ &= \alpha |0\rangle \langle0|0\rangle + \beta |0\rangle \langle0|1\rangle \\ &= \alpha |0\rangle \\ P_1(\alpha |0\rangle + \beta |1\rangle) &= \alpha P_1 |0\rangle + \beta P_1 |1\rangle \\ &= \alpha |1\rangle \langle1|0\rangle + \beta |1\rangle \langle1|1\rangle \\ &= \beta |1\rangle \end{aligned} $$

With these projectors we can define the measurement operators $M_0$ and $M_1$ as

$$ M_i |\psi\rangle = \frac{P_i |\psi\rangle}{\sqrt{\langle\psi| P_i |\psi\rangle}} $$

For example,

$$ \begin{aligned} M_0(\alpha |0\rangle + \beta |1\rangle) &= \frac{P_0(\alpha |0\rangle + \beta |1\rangle)}{\sqrt{(\alpha^* \langle0| + \beta^* \langle1|)P_0(\alpha |0\rangle + \beta |1\rangle)}} \\ &= \frac{\alpha |0\rangle}{\sqrt{(\alpha^* \langle0| + \beta^* \langle1|)(\alpha |0\rangle)}} \\ &= \frac{\alpha |0\rangle}{\sqrt{|\alpha|^2 \langle0|0\rangle + \beta^* \alpha \langle1|0\rangle}} \\ &= \frac{\alpha |0\rangle}{\sqrt{|\alpha|^2}} = \frac{\alpha}{|\alpha|} |0\rangle \equiv {}^3|0\rangle \end{aligned} $$
$$ \Psi := \mathbb{B} \mid S(\Psi) $$

Qubit types (Q)

$$ A := \Psi \mid \Psi \Rightarrow A \mid S(A) $$

Types (T)

<caption>**Table 1:** First grammar of types, without product.</caption>

$$ b := x \mid \lambda x^{\Psi}.t \mid |0\rangle \mid |1\rangle $$

Base terms (B)

$$ v := b \mid (v + v) \mid \vec{0}_{S(A)} \mid \alpha.v $$

Values (V)

$$ t := v \mid tt \mid (t + t) \mid \pi t \mid ?t \cdot t \mid \alpha.t $$

Terms (Λ)

<caption>**Table 2:** First grammar of terms, without product.</caption>

The quantum measurement is defined in terms of sets of measurements op-
erators. For example, in the canonical base {|0⟩, |1⟩}, the set {M₀, M₁} is a
quantum measurement. When it acts on a qubit |φ⟩, it will apply the operator
Mᵢ, with probability ⟨ψ|Pᵢ|ψ⟩.

**3. No cloning, superpositions and measurement**

The grammar of types is defined in Table 1 and the grammar of terms in
Table 2, where $\alpha \in \mathbb{C}$.

Terms are variables, abstractions, applications, two constants for base qubits
(|0⟩ and |1⟩), linear combinations of terms (built with addition and product by
a scalar, addition being commutative and associative), a family of constants for
the null vectors, one for each type of the form S(A), (0̄S(A)), and an if-then-
else construction (?t·t) deciding on base vectors. We use the notation t?r·s for
(?r·s)t, so making ?r·s a function, which applied to a term t produces "if t then
r else s", when t is a basis term. We also include a symbol π for measurement
in the computational basis.

The grammar is split into base terms (non-superposed values), general values,
and general terms. Types are also split into qubit types and general types.

The set of free variables of a term *t* is defined as usual in the λ-calculus and denoted by *FV*(*t*). We use [α.]*t* as a notation to refer indistinctly to α.t and to *t*. We use -*t* as a shorthand notation for -1.t, and (*t* − *r*) as a shorthand notation for (*t* + (−*r*)). The term (*t* − *t*) will have type *S*(*A*), and reduce to 0̄S(*A*), which is not a base term.

<footnote n="3">³The scalar $\frac{\alpha}{|\alpha|}$ is known as a *phase* and can be ignored, so only $|0\rangle$ remains.</footnote>
<figure><img src="image_2.png" /><figcaption>**Table 3:** First subtyping relation, without product.</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>**Table 4:** First type system, without product.</figcaption></figure>

An important property of this calculus is that types $S(\cdot)$ are linear types. Indeed, those correspond to superpositions, and so no duplication is allowed on them. Instead, at this tensor-free stage, a type without an $S(\cdot)$ on head position is a non-linear type, such as $\mathbb{B}$, which correspond to base terms, i.e. terms that can be cloned. A non-linear function is allowed to be applied to a linear argument, for example, $\lambda x^{\mathbb{B}}.(fxx)$ can be applied to $(\frac{1}{\sqrt{2}}|0\rangle + \frac{1}{\sqrt{2}}|1\rangle)$, however, it distributes in the following way: $(\lambda x^{\mathbb{B}}.(fxx))(\frac{1}{\sqrt{2}}|0\rangle + \frac{1}{\sqrt{2}}|1\rangle) \rightarrow (\frac{1}{\sqrt{2}}(\lambda x^{\mathbb{B}}.(fxx))|0\rangle + \frac{1}{\sqrt{2}}(\lambda x^{\mathbb{B}}.(fxx))|1\rangle) \rightarrow (\frac{1}{\sqrt{2}}(f|0\rangle|0\rangle) + \frac{1}{\sqrt{2}}(f|1\rangle|1\rangle)).$

Hence, the beta reduction occurs only when the type of the argument is the same as the type expected by the abstraction. Thus, the rewrite system depends on types. For this reason, we describe first the type system, and only then the rewrite system.

A type $A$ will be interpreted as a set of vectors and $S(A)$ as the vector space generated by the span of such a set (cf. Section 7). Hence, we naturally have $A \subseteq S(A)$ and $S(S(A)) = S(A)$. Therefore, we also define a subtyping relation on types (cf. Table 3). The type system is given in Table 4, where contexts $\Gamma$ and $\Delta$ have a disjoint support.

**Remarks:** Rule $Ax$ allows typing variables only with qubit types. Hence, the system is first-order and only qubits can be passed as arguments (more when the rewrite system is presented). Rule $Ax_0$ types the null vector as a non-base
term, because the null vector cannot belong to the base of any vector space. Rules $Ax_{|0\rangle}$ and $Ax_{|1\rangle}$ type the base qubits with the base type $\mathbb{B}$.

Thanks to rule $\leq$ the term $|0\rangle$ has type $\mathbb{B}$ and also the more general type $S(\mathbb{B})$. Note that $((|0\rangle + |0\rangle) - |0\rangle)$ has type $S(\mathbb{B})$ and reduces to $|0\rangle$ which has the same type $S(\mathbb{B})$. Reducing this term to $|0\rangle$ of type $\mathbb{B}$ would not preserve its type. Moreover, this type would contain information impossible to compute, because the value $|0\rangle$ is not the result of a measurement, but of an interference.

Rule $S_I^\alpha$ states that a term multiplied by a scalar is not a base term. Even if the scalar is just a phase, we must type the term with an $S(\cdot)$ type, because our measurement operator will remove any scalars, so having the scalar means that it has not been measured yet. Rule $S_I^+$ is the analog for sums to the previous rule. Rule $S_E$ is the elimination of the superposition, which is achieved by measuring (using the $\pi$ operator).

Notice that $?t \cdot r$ is typed as a non-linear function by rule If, and so, the if-then-else linearly distributes over superpositions, e.g.

$$ \begin{aligned} (\alpha. |0\rangle + \beta. |1\rangle)?t \cdot r &= (?t \cdot r)(\alpha. |0\rangle + \beta. |1\rangle) \\ &\rightarrow^* \alpha. (?t \cdot r)|0\rangle + \beta. (?t \cdot r)|1\rangle \\ &= \alpha. |0\rangle?t \cdot r + \beta. |1\rangle?t \cdot r \\ &\rightarrow^* \alpha \cdot r + \beta \cdot t \end{aligned} $$

Rule $\Rightarrow_{ES}$ is the elimination for superpositions, corresponding to the linear distribution. Notice that the type of the argument is a superposition of the argument expected by the abstraction $(S(\Psi) \text{ vs. } \Psi)$. Also, the abstraction is allowed to be a superposition. If, for example, we want to apply the sum of functions $(f + g)$ to the base argument $|0\rangle$, we would obtain the superposition $(f|0\rangle + g|0\rangle)$. The typing is as follows:

$$ \frac{\vdash f : \mathbb{B} \Rightarrow A \quad \vdash g : \mathbb{B} \Rightarrow A \quad S_I^+ \quad \overline{\vdash |0\rangle : \mathbb{B}} \quad Ax_{|0\rangle}}{\vdash (f+g) : S(\mathbb{B} \Rightarrow A) \quad \overline{\vdash |0\rangle : S(\mathbb{B})} \quad \leq \quad \Rightarrow_{ES}} \quad \overline{\vdash |0\rangle : \mathbb{B}} \quad Ax_{|0\rangle} $$

which reduces to

$$ \frac{\vdash f : \mathbb{B} \Rightarrow A \quad \overline{\vdash |0\rangle : \mathbb{B}} \quad Ax_{|0\rangle} \quad \Rightarrow_E \quad \vdash g : \mathbb{B} \Rightarrow A \quad \overline{\vdash |0\rangle : \mathbb{B}} \quad Ax_{|0\rangle}}{\vdash f |0\rangle : A \quad \overline{\vdash g |0\rangle : A} \quad \Rightarrow_E \quad \overline{\vdash (f |0\rangle + g |0\rangle) : S(A)} \quad S_I^+} $$

Similarly, a linear function $(\vdash f : \mathbb{B} \Rightarrow A)$ applied to a superposition $(|0\rangle + |1\rangle)$ reduces to a superposition $(f|0\rangle + f|1\rangle)$. The typing is as follows:

$$ \frac{\vdash f : \mathbb{B} \Rightarrow A \quad \overline{\vdash |0\rangle : \mathbb{B}} \quad Ax_{|0\rangle} \quad \overline{\vdash |1\rangle : \mathbb{B}} \quad Ax_{|1\rangle}}{\vdash f : S(\mathbb{B} \Rightarrow A) \quad \overline{\vdash (|0\rangle + |1\rangle) : S(\mathbb{B})} \quad S_I^+} \quad \Rightarrow_{ES} \quad \overline{\vdash f(|0\rangle + |1\rangle) : S(A)} $$
is that cloning after measurement is not a problem, since we already know the state to be cloned: It would be enough to prepare a second system in the same state.

The group If-then-else contains the tests over the base qubits $|0\rangle$ and $|1\rangle$.

The first three of the linear distribution rules (those marked with subindex r), are the rules that are used when a non-linear abstraction is applied to a linear argument (that is, when an abstraction expecting a base term is given a superposition). In these cases the beta reductions cannot be used since the side conditions on types are not met. Hence, these distributivity rules apply instead.

For example, let us give more details in the reduction sequence on the example given at the beginning of this Section.

$$ (\lambda x^{\mathbb{B}}.(fxx))(\frac{1}{\sqrt{2}}|0\rangle + \frac{1}{\sqrt{2}}|1\rangle) \\ \xrightarrow{\langle \mathrm{lin}_r^+ \rangle} ((\lambda x^{\mathbb{B}}.(fxx))\frac{1}{\sqrt{2}}|0\rangle + (\lambda x : \mathbb{B} (fxx))\frac{1}{\sqrt{2}}|1\rangle) \\ \xrightarrow{\langle \mathrm{lin}_r^0 \rangle^2} (\frac{1}{\sqrt{2}}.(\lambda x^{\mathbb{B}}.(fxx))|0\rangle + \frac{1}{\sqrt{2}}.(\lambda x^{\mathbb{B}}.(fxx))|1\rangle) \\ \xrightarrow{\langle \mathrm{lin}_r^\beta \rangle^2} (\frac{1}{\sqrt{2}}.f|0\rangle|0\rangle + \frac{1}{\sqrt{2}}.f|1\rangle|1\rangle) $$

Notice that in Rule $(\mathrm{lin}_r^0)$, the term needs to be reduced to $\tilde{0}_{S(\mathrm{min}(A))}$. Indeed, if we just reduce $t\tilde{0}_{S(\mathbb{B})}$ to $\tilde{0}_{S(A)}$, there is a problem of subject reduction: $t$ having type $\mathbb{B} \Rightarrow A$ do not implies it has no other type, for example, $\mathbb{B} \Rightarrow B$, and so, reducing to $\tilde{0}_{S(A)}$ would break subject reduction since $\tilde{0}_{S(A)}$ does not have necesarilly type $S(B)$. On the contrary, we can prove (cf. Lemmas 5.4 and 5.6) that if $t$ has types $\mathbb{B} \Rightarrow A$ and $\mathbb{B} \Rightarrow B$, then $\mathrm{min}(A) \preceq B$, and so subject reduction is preserved.

The remaining rules in this group deal with a superposition of functions. For example, rule $(\mathrm{lin}_r^+)$ is the sum of functions: A superposition is a sum, therefore, if an argument is given to a sum of functions, it needs to be given to each function in the sum. We use a weak reduction strategy (i.e. reduction occurs only on closed terms), hence the argument $v$ on this rule is closed, otherwise, it could not be typed. For example $x : S(\mathbb{B}), t : \mathbb{B} \Rightarrow \mathbb{B}, u : \mathbb{B} \Rightarrow \mathbb{B} \vdash (t+u)x : S(\mathbb{B})$ is derivable, but $x : S(\mathbb{B}), t : \mathbb{B} \Rightarrow \mathbb{B}, u : \mathbb{B} \Rightarrow \mathbb{B} \vdash (tx + ux) : S(\mathbb{B})$ is not.

The vector space axioms rules are the directed axioms of vector spaces [10, 14]. The rule $(\mathrm{zero}_S)$ ensures that each vector space have only one null vector. The Modulo AC rules are not proper rewrite rules, but express that we consider the symbol $+$ to be associative and commutative, and hence our rewrite system is *rewrite modulo AC* [18]. As a consequence, the parenthesis are not needed and we may use the notation $\sum_{i=1}^n t_i$. (for example, in rule (proj)).

Rule (proj) is the projection over weighted associative pairs, that is, the projection over a generalization of multisets where the multiplicities are given by complex numbers. This reduction rule is the only one with a probability
different from 1, and it is given by the square of the modulus of the weights$^4$, implementing this way the quantum measurement over the computational basis.

Remark, to conclude, that this calculus can represent only pure states, and not mixed states. For example, let $\mathbb{Z}$ be an encoding for the quantum $\mathbb{Z}$ gate (cf. Section 8), $|+\rangle = \frac{1}{\sqrt{2}}(|0\rangle + |1\rangle)$, and $|-\rangle = \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle)$. The terms $(\lambda x : S(\mathbb{B}) (\lambda y : y?(\mathbb{Z}x) \cdot x)(\pi|+\rangle))|+\rangle$ and $(\lambda x : S(\mathbb{B}) \pi(x))|+\rangle$ may be considered equivalent if taking into account the density matrix representation of mixed states. Indeed, the first reduces either to $|+\rangle$ or $|-\rangle$, with probability $\frac{1}{2}$ each, while the second reduces to $|0\rangle$ or to $|1\rangle$, with probability $\frac{1}{2}$ each. The sets of pure states $\{(\frac{1}{2}, |+\rangle), (\frac{1}{2}, |-\rangle)\}$ and $\{(\frac{1}{2}, |0\rangle), (\frac{1}{2}, |1\rangle)\}$ have both density matrix $\frac{I}{2}$, and hence are indistinguishable. However, once the result of the measure is known, the pure states can be distinguished. A different approach, using density matrices, can be seen in [19], however such a calculus has a linear type system, and no algebraic reduction occurs.

## 4. Multi-qubit systems: Tensor products

One postulate of quantum mechanics determines how to compose several quantum systems. This way, the Hilbert space of a multi-qubit system is the tensor product between single-qubit Hilbert spaces. If $|\psi\rangle \in \mathcal{H}_1$ and $|\phi\rangle \in \mathcal{H}_2$ represent the states of two quantum systems, the state of the full system composed by those two is $|\psi\rangle \otimes |\phi\rangle \in \mathcal{H}_1 \otimes \mathcal{H}_2$. In particular, if we chose bases $\mathcal{B}_1$ and $\mathcal{B}_2$ of $\mathcal{H}_1$ and $\mathcal{H}_2$ respectively, we can write $|\psi\rangle = \sum_{i \in \mathcal{B}_1} \alpha_i |i\rangle$ and $|\phi\rangle = \sum_{j \in \mathcal{B}_2} \beta_j |j\rangle$, and so $|\psi\rangle \otimes |\phi\rangle = \sum_{i \in \mathcal{B}_1} \sum_{j \in \mathcal{B}_2} \alpha_i \beta_j |i\rangle \otimes |j\rangle = \sum_{i \in \mathcal{B}_1} \sum_{j \in \mathcal{B}_2} \alpha_i \beta_j |ij\rangle$. The last equality can be seen as a matter of notation, but also it is clear that $|i\rangle \otimes |j\rangle \simeq |i\rangle \times |j\rangle$, and so $\mathcal{H}_1 \otimes \mathcal{H}_2 \simeq \text{Span}(\mathcal{B}_1 \times \mathcal{B}_2)$. Therefore, since we already introduced a symbol for the span of a type, and basis types, we only need to introduce an associative Cartesian product to our calculus in order to recover the tensor product. For example, the term $|0\rangle \times (\frac{1}{\sqrt{2}}|0\rangle + \frac{1}{\sqrt{2}}|1\rangle)$ have type $\mathbb{B} \times S(\mathbb{B})$, while $(\frac{1}{\sqrt{2}}|0\rangle \times |0\rangle + \frac{1}{\sqrt{2}}|0\rangle \times |1\rangle)$ have type $S(\mathbb{B} \times \mathbb{B})$. Therefore, the distributivity of linear combinations over tensor products is not trivially tracked in the type system, and so an explicit cast between types is also added: The term $|0\rangle \times (\frac{1}{\sqrt{2}}|0\rangle + \frac{1}{\sqrt{2}}|1\rangle)$ does not rewrite to $(\frac{1}{\sqrt{2}}|0\rangle \times |0\rangle + \frac{1}{\sqrt{2}}|0\rangle \times |1\rangle)$, but the term $\uparrow_{\ell} |0\rangle \times (\frac{1}{\sqrt{2}}|0\rangle + \frac{1}{\sqrt{2}}|1\rangle)$ does, where $\uparrow_{\ell}$ casts the type $S(\mathbb{B} \times S(\mathbb{B}))$ into the type $S(\mathbb{B} \times \mathbb{B})$.

The grammar of types is given in Table 6, where the Cartesian product is added to each level. The new level “base qubit types” ($\mathbf{B}$) is needed since the abstractions with variables in $\mathbf{B}$ are the non-linear ones. We will use the following notation: $\mathbb{B}^n = \mathbb{B} \times \cdots \times \mathbb{B}$ ($n$-times). Hence, $\mathbf{B} = \{\mathbb{B}^n \mid n > 0\}$. Also, we may use the notation $A \times S(\mathbb{B}^0) = A$.

The grammar of terms is given in Table 7.

<footnote>$^4$We speak about weights and not amplitudes, since the vector may not have norm 1. The projection rule normalizes the vector while reducing.</footnote>
$\mathfrak{B} := \mathbb{B} | \mathfrak{B} \times \mathfrak{B}$ Base qubit types (B)

$\Psi := \mathfrak{B} | S(\Psi) | \Psi \times \Psi$ Qubit types (Q)

$A := \Psi | \Psi \Rightarrow A | S(A) | A \times A$ Types (T)

<caption>**Table 6:** Grammar of types.</caption>

b := x | $\lambda x^{\Psi}$.t | $|0\rangle$ | $|1\rangle$ | $b \times b$ Base terms (B)
v := b | $(v + v)$ | $\vec{0}_{S(A)}$ | $\alpha.v$ | $v \times v$ Values (V)
t := v | $tt$ | $(t + t)$ | $\pi_j t$ | $?t \cdot t$ | $\alpha.t$ Terms (A)
$|t \times t|$ head $t$ | tail $t$ | $\Uparrow_r t$ | $\Uparrow_\ell t$

<caption>**Table 7:** Grammar of terms.</caption>

Each level in the term grammar (base terms, values and general terms) is extended with the tensor of the terms in such a level. The primitives head and tail are added to the general terms. The projector $\pi$ is generalized to $\pi_j$, where the subindex $j$ stands for the number of qubits to be measured, which are those in the first $j$ positions. Notice that it is always possible to do a swap between qubits and so place the qubits to be measured at the beginning. For instance, $\lambda x^{\mathfrak{B} \times \mathfrak{B}}.tail \ x \times head \ x$. Finally, an explicit type cast of a term $t$ ($\Uparrow_r t$ and $\Uparrow_\ell t$) is included in the general terms. We may use just $\Uparrow$ to refer to any of $\Uparrow_r$ or $\Uparrow_\ell$. As the product is associative, we also may use the notation $\prod_{i=1}^n t_i$ and $\prod_{i=1}^n A_i$ for associative Cartesian products.

The subtyping relation is also updated to include Cartesian products, and it is given in Table 8.

$$ \begin{array}{ccc} \underline{A \preceq A} & \underline{A \preceq B \quad B \preceq C} & \underline{A \preceq B} \\ \hline \underline{A \preceq S(A)} & \underline{S(S(A)) \preceq S(A)} & \underline{\Psi \Rightarrow A \preceq \Psi \Rightarrow B} \\ \hline \underline{A \preceq B} & \underline{A \preceq B \quad A \times C \preceq B \times C} & \underline{A \preceq B \quad C \times A \preceq C \times B} \\ \hline \underline{S(A) \preceq S(B)} & & \end{array} $$

<caption>**Table 8:** Subtyping relation.</caption>

The updated type system, given in Table 9, includes all the typing rules given in the previous section, plus the rules for tensor, for cast, and an updated
<figure><img src="image_4.png" /><figcaption>**Table 9:** Type system.</figcaption></figure>

rule $S_E$.

Rules $Ax$, $Ax_0$, $Ax_{|0}$, $Ax_{|1}$, $\leq$, $S_I^\alpha$, $S_I^+$, If, $\Rightarrow_I$, $\Rightarrow_E$ and $\Rightarrow_{ES}$ remain unchanged. Rule $S_E$ types the generalized projection: we force the term to be measured to be typed with a type of the form $S(\mathbb{B}^n)$, and then, after measuring the first $j$ qubits, the new type becomes $\mathbb{B}^j \times S(\mathbb{B}^{n-j})$, that is, we remove the superposition mark $S(\cdot)$ from the first $j$ types in the tensor product. Rules $W$ and $C$ are updated only to act on types $\mathbb{B}^n$ instead of just $\mathbb{B}$.

Rules $\times_I$, $\times_{E_r}$, and $\times_{E_l}$ are the standard introduction and eliminations for lists, however, the elimination is only allowed on terms with type $\mathbb{B}^n$ (basis qubits). Rules $\uparrow_r$ and $\uparrow_\ell$ type the castings. We only need to allow to cast a superposed type into a superposed tensor product, thanks to the subtyping relation. Indeed, for example, to cast $t \times (r + s)$ from type $A \times S(B)$ to type $S(A \times B)$, we can use the subtyping first to assign the type $S(A \times S(B))$ to $t \times (r + s)$.

To update the rewrite system, we need to update the function `min` to include products, as follows.

$$ 
\begin{align*}
\min(\mathbb{B}) &= \mathbb{B} \\
\min(\Psi \Rightarrow A) &= \Psi \Rightarrow \min(A) \\
\min(A \times B) &= \min(A) \times \min(B) \\
\min(S(A)) &= \min(A)
\end{align*}
$$

The updated rewrite system is given in Table 10. It includes all the rules
from Table 5 plus the rules for lists: (head) and (tail) and the typing casts rules, which normalize superpositions to sums of base terms, while update the types.

The rule (proj) has been updated to account for multiple qubits systems. It normalizes (as in norm 1) the scalars on the obtained term. The call-by-base beta rule ($\beta_b$), and the contextual rule admitting reducing the argument on an application for the call-by-base abstraction are updated to allow for abstractions expecting arguments of type $\mathbb{B}^n$ instead of just $\mathbb{B}$ (that is, any base qubit type).

The first six rules in the group typing casts—($dist_r^+$), ($dist_r^\alpha$), and ($dist_r^0$), and their analogous ($dist_i^+$), ($dist_i^\alpha$), and ($dist_i^0$)—deal with the distributivity of sums, scalar product and null vector respectively. If we ignore the type cast $\Uparrow$ on each rule, these rules are just distributivity rules. For example, rule ($dist_r^+$) acts on the term $(r + s) \times u$, distributing the sum with respect to the tensor product, producing $(r \times u + s \times u)$ (distribution to the right). However, the term $(r + s) \times u$ may have type $S(A) \times B$, $S(A) \times S(B)$ or $S(A \times B)$, while, among those, the term $(r \times u + s \times u)$ can only have type $S(A \times B)$. Hence, we cannot reduce the first term to the second without losing subject reduction. Instead, we need to cast the term explicitly to the valid type in order to reduce.

The next two rules, ($dist_\Uparrow^+$) and ($dist_\Uparrow^\alpha$), distribute the cast over sums and scalars. For example $\Uparrow_r ((\alpha. |0\rangle) \times |0\rangle + (\beta. |0\rangle) \times |1\rangle)$ reduces by rule ($dist_\Uparrow^+$) to $(\Uparrow_r (\alpha. |1\rangle) \times |0\rangle + \Uparrow_r (\beta. |0\rangle) \times |1\rangle)$, and hence, the distributivity rule can act. The last two rules in the group, ($neut_\Uparrow^+$) and ($neut_\Uparrow^\alpha$), remove the cast when it is not needed anymore. For example

$$ \begin{aligned} \Uparrow_r (\alpha.\beta. |0\rangle) \times |1\rangle &\xrightarrow{(\mathrm{dist}_\Uparrow^\alpha)} \alpha. \Uparrow_r (\beta. |0\rangle) \times |1\rangle \\ &\xrightarrow{(\mathrm{dist}_\Uparrow^\alpha)} \alpha.\beta. \Uparrow_r |0\rangle \times |1\rangle \\ &\xrightarrow{(\mathrm{neut}_\Uparrow^\alpha)} \alpha.\beta. |0\rangle \times |1\rangle \end{aligned} $$

The measurement rule (proj) is updated to measure the first $j$ qubits. Hence, a $n$-qubits in normal form (that is, a sum of products of qubits with or without a scalar in front), for example, the term

$$ 2.(|0\rangle \times |1\rangle \times |1\rangle) + |0\rangle \times |1\rangle \times |0\rangle + 3.(|1\rangle \times |1\rangle \times |1\rangle) $$

can be measured and will produce a $n$-qubits where the first $j$ qubits are the same and the remaining are untouched, with its scalars changed to have norm 1. In this 3-qubits example, measuring the first two can produce either

$$ |0\rangle \times |1\rangle \times \left( \frac{2}{\sqrt{5}} \cdot |1\rangle + \frac{1}{\sqrt{5}} \cdot |0\rangle \right) $$

or

$$ |1\rangle \times |1\rangle \times (1. |1\rangle) $$

The probability of producing the first is $\frac{|2|^2}{(|2|^2+|1|^2+|3|^2)} + \frac{|1|^2}{(|2|^2+|1|^2+|3|^2)} = \frac{5}{14}$ and the probability of producing the second is $\frac{|3|^2}{(|2|^2+|1|^2+|3|^2)} = \frac{9}{14}$.

Remark, to conclude, that since the calculus presented in this paper is call-by-base for the functions expecting a non-linear argument, it avoids a well-known
<table><caption>**Table 10:** Rewrite system.</caption>
  <tbody>
    <tr>
      <td>Beta</td>
      <td>If b has type <i>B</i><sup>n</sup> and b &isin; <i>B</i>, (&lambda;x<sup><i>B</i><sup>n</sup></sup>.t)b &rarr;<sub>(1)</sub> (b/x)t<br>If u has type <i>S</i>(<i>&Psi;</i>), (&lambda;x<sup><i>S</i>(<i>&Psi;</i>)</sup>.t)u &rarr;<sub>(1)</sub> (u/x)t</td>
      <td>(&beta;<sub>b</sub>)<br>(&beta;<sub>n</sub>)</td>
    </tr>
    <tr>
      <td>If</td>
      <td>|1>?&tau;.r &rarr;<sub>(1)</sub> t<br>|0>?&tau;.r &rarr;<sub>(1)</sub> r</td>
      <td>(if<sub>1</sub>)<br>(if<sub>0</sub>)</td>
    </tr>
    <tr>
      <td>Linear distribution</td>
      <td>If t has type <i>B</i><sup>n</sup> &rarr; A, t(u + v) &rarr;<sub>(1)</sub> (tu + tv)<br>If t has type <i>B</i><sup>n</sup> &rarr; A, t(&alpha;.u) &rarr;<sub>(1)</sub> &alpha;.tu<br>If t has type <i>B</i><sup>n</sup> &rarr; A, t&vec;<sub><i>S</i>(<i>B</i><sup>n</sup>)</sub> &rarr;<sub>(1)</sub> &vec;<sub><i>S</i>(min(A))</sub><br>(t + u)v &rarr;<sub>(1)</sub> (tv + uv)<br>(&alpha;.t)u &rarr;<sub>(1)</sub> &alpha;.tu<br>&vec;<sub><i>S</i>(<i>B</i><sup>n</sup>=A)</sub>t &rarr;<sub>(1)</sub> &vec;<sub><i>S</i>(min(A))</sub></td>
      <td>(lin<sub>r</sub><sup>+</sup>)<br>(lin<sub>r</sub><sup>&alpha;</sup>)<br>(lin<sub>r</sub><sup>0</sup>)<br>(lin<sub>r</sub><sup>+</sup>)<br>(lin<sub>r</sub><sup>&alpha;</sup>)<br>(lin<sub>r</sub><sup>0</sup>)</td>
    </tr>
    <tr>
      <td>Vector space axioms</td>
      <td>(&vec;<sub><i>S</i>(A)</sub> + t) &rarr;<sub>(1)</sub> t<br>1.t &rarr;<sub>(1)</sub> t<br>If t has type A, 0.t &rarr;<sub>(1)</sub> &vec;<sub><i>S</i>(min(A))</sub><br>&alpha;. &vec;<sub><i>S</i>(A)</sub> &rarr;<sub>(1)</sub> &vec;<sub><i>S</i>(min(A))</sub><br>&alpha;.(&beta;t) &rarr;<sub>(1)</sub> (&alpha;&beta;).t<br>&alpha;.(t + u) &rarr;<sub>(1)</sub> (&alpha;.t + &alpha;.u)<br>(&alpha;.t + &beta;t) &rarr;<sub>(1)</sub> (&alpha; + &beta;).t<br>(&alpha;.t + t) &rarr;<sub>(1)</sub> (&alpha; + 1).t<br>(t + t) &rarr;<sub>(1)</sub> 2.t<br>If A &ne; min(A), then &vec;<sub><i>S</i>(A)</sub> &rarr;<sub>(1)</sub> &vec;<sub><i>S</i>(min(A))</sub></td>
      <td>(neutral)<br>(unit)<br>(zero<sub>&alpha;</sub>)<br>(zero)<br>(prod)<br>(&alpha;dist)<br>(fact)<br>(fact<sup>1</sup>)<br>(fact<sup>2</sup>)<br>(zero<sub>S</sub>)</td>
    </tr>
    <tr>
      <td>=</td>
      <td>(t + r) =<sub>AC</sub> (r + t)<br>((t + r) + s) =<sub>AC</sub> (t + (r + s))</td>
      <td>(comm)<br>(assoc)</td>
    </tr>
    <tr>
      <td>Lists</td>
      <td>If h &ne; u &times; v and h &isin; <i>B</i>, head h &times; t &rarr;<sub>(1)</sub> h<br>If h &ne; u &times; v and h &isin; <i>B</i>, tail h &times; t &rarr;<sub>(1)</sub> t</td>
      <td>(head)<br>(tail)</td>
    </tr>
    <tr>
      <td>Typing casts</td>
      <td>&Uarr;<sub>r</sub> (r + s) &times; u &rarr;<sub>(1)</sub> (&Uarr;<sub>r</sub> r &times; u + &Uarr;<sub>r</sub> s &times; u)<br>&Uarr;<sub>&ell;</sub> u &times; (r + s) &rarr;<sub>(1)</sub> (&Uarr;<sub>&ell;</sub> u &times; r + &Uarr;<sub>&ell;</sub> u &times; s)<br>&Uarr;<sub>r</sub> (&alpha;.r) &times; u &rarr;<sub>(1)</sub> &alpha; &Uarr;<sub>r</sub> r &times; u<br>&Uarr;<sub>&ell;</sub> u &times; (&alpha;.r) &rarr;<sub>(1)</sub> &alpha; &Uarr;<sub>r</sub> u &times; r<br>If u has type <i>B</i>, &Uarr;<sub>r</sub> &vec;<sub><i>S</i>(A)</sub> &times; u &rarr;<sub>(1)</sub> &vec;<sub><i>S</i>(min(A&times;B))</sub><br>If u has type <i>A</i>, &Uarr;<sub>&ell;</sub> u &times; &vec;<sub><i>S</i>(B)</sub> &rarr;<sub>(1)</sub> &vec;<sub><i>S</i>(min(A&times;B))</sub><br>&Uarr; (t + u) &rarr;<sub>(1)</sub> (&Uarr; t + &Uarr; u)<br>&Uarr; (&alpha;.t) &rarr;<sub>(1)</sub> &alpha; &Uarr; t<br>If u &isin; <i>B</i>, &Uarr;<sub>r</sub> u &times; v &rarr;<sub>(1)</sub> u &times; v<br>If v &isin; <i>B</i>, &Uarr;<sub>&ell;</sub> u &times; v &rarr;<sub>(1)</sub> u &times; v</td>
      <td>(dist<sub>r</sub><sup>+</sup>)<br>(dist<sub>r</sub><sup>+</sup>)<br>(dist<sub>r</sub><sup>&alpha;</sup>)<br>(dist<sub>r</sub><sup>&alpha;</sup>)<br>(dist<sub>r</sub><sup>0</sup>)<br>(dist<sub>r</sub><sup>0</sup>)<br>(dist<sub>r</sub><sup>+</sup>)<br>(dist<sub>r</sub><sup>&alpha;</sup>)<br>(neut<sub>r</sub><sup>+</sup>)<br>(neut<sub>r</sub><sup>&ell;</sup>)</td>
    </tr>
    <tr>
      <td>Projection</td>
      <td>&pi;<sub>j</sub>(&sum;<sub>i=1</sub><sup>n</sup> [&alpha;<sub>i</sub>.] &prod;<sub>h=1</sub><sup>m</sup> b<sub>hi</sub>) &rarr;<sub>(p)</sub> (&prod;<sub>h=1</sub><sup>j</sup> b<sub>hk</sub>) &times; &sum;<sub>i&isin;P</sub> (<sup>&alpha;<sub>i</sub></sup>&frasl;<sub>&radic;<span style="text-decoration:overline;">&sum;<sub>r&isin;P</sub> |&alpha;<sub>r</sub>|<sup>2</sup></span></sup>) &prod;<sub>h=j+1</sub><sup>m</sup> b<sub>hi</sub></td>
      <td>(proj)</td>
    </tr>
    <tr>
      <td>Contextual rules</td>
      <td>If t &rarr;<sub>(p)</sub> u, then<br>tv &rarr;<sub>(p)</sub> uv<br>&alpha;.t &rarr;<sub>(p)</sub> &alpha;.u<br>v &times; t &rarr;<sub>(p)</sub> v &times; u<br>head t &rarr;<sub>(p)</sub> head u<br>&lambda;x<sup><i>B</i><sup>n</sup></sup>.v)t &rarr;<sub>(p)</sub> (&lambda;x<sup><i>B</i><sup>n</sup></sup>.v)u<br>&pi;<sub>j</sub>t &rarr;<sub>(p)</sub> &pi;<sub>j</sub>u<br>&Uarr;<sub>r</sub> t &rarr;<sub>(p)</sub> &Uarr;<sub>r</sub> u<br>tail t &rarr;<sub>(p)</sub> tail u<br>(t + v) &rarr;<sub>(p)</sub> (u + v)<br>t &times; v &rarr;<sub>(p)</sub> u &times; v<br>&Uarr;<sub>&ell;</sub> t &rarr;<sub>(p)</sub> &Uarr;<sub>&ell;</sub> u<br>t&rcdot;s &rarr;<sub>(p)</sub> u&rcdot;s</td>
      <td></td>
    </tr>
  </tbody>
  <tfoot>
    <tr>
      <td colspan="3">All the terms are considered to be closed (i.e. reduction is weak).</td>
    </tr>
  </tfoot>
</table>
problem in others λ-calculi with a linear logic type system including modalities.
To illustrate this problem, consider the following typing judgment:

$$y : S(\mathbb{B}) \vdash (\lambda x^{\mathbb{B}}.x \times x)(\pi y) : S(\mathbb{B}) \times S(\mathbb{B})$$

If we allow to β-reduce this term, we would obtain $(\pi y) \times (\pi y)$ which is not typable in the context $y : S(\mathbb{B})$. A standard solution to this problem is illustrated in [20], where the terms that can be cloned are distinguished by a mark, and used in a let construction, while non-clonable terms are used in λ abstractions. Since this term will not beta reduce in our calculus, but project first, the problem is not present neither in our case.

## 5. Subject reduction

Thanks to the explicit casts, the resulting system has the Subject Reduction property (Theorem 5.12), that is, the typing is preserved by weak-reduction (i.e. reduction on closed terms). The proof of this theorem is not trivial, specially due to the complexity of the system itself.

The two main lemmas in the proof, the generation lemma (Lemma 5.7) and the substitution lemma (Lemma 5.11), are stated below, together with a few paradigmatic cases of the proof.

We denote by $|\Gamma|$ to the multiset of types in $\Gamma$. For example,

$$|x : \mathbb{B}, y : \mathbb{B}, z : S(\mathbb{B})| = \{\mathbb{B}, \mathbb{B}, S(\mathbb{B})\}$$

**Lemma 5.1.** If $A \preceq \mathbb{B}^n$, then $A = \mathbb{B}^n$

*PROOF.* By rule inspection.

**Lemma 5.2.** If $S(A) \preceq B$, then there exists $C$ such that $B = S(C)$

*PROOF.* Straightforward induction on the definition of $\preceq$.

**Lemma 5.3.** If $S^n(A \times B) \preceq C$, then there exist $m, D, E$ such that $C = S^m(D \times E)$ with $A \preceq D$ and $B \preceq E$.

*PROOF.* By induction on the derivation of $S^n(A \times B) \preceq C$.

**Lemma 5.4.** For any type $A$, we have $\min(A) \preceq A$.

*PROOF.* By cases over $A$.

**Lemma 5.5.** If $A \preceq B$, then $\min(A) = \min(B)$.

*PROOF.* By induction on the derivation of $A \preceq B$.

**Lemma 5.6.** If $\Gamma \vdash t : A$ and $\Gamma \vdash t : B$, then $\min(A) = \min(B)$.
PROOF. Let $\pi$ be the derivation tree of $\Gamma \vdash t : A$ and $\pi'$ the derivation tree of $\Gamma \vdash t : B$, we proceed by induction on $|\pi| + |\pi'|$, where $|\cdot|$ is the size of the derivation tree.

We only give three case.

• If $t = (r + s)$ and both derivations end with rule $S_I^+$, then $A = S(A')$, $B = S(B')$, $\Gamma_1 \vdash r : A'$, $\Gamma_2 \vdash s : A'$, $\Gamma_1 \vdash r : B'$, and $\Gamma_2 \vdash s : B'$ where $\Gamma_1$ is defined only on $FV(r)$ and $\Gamma_2$ on $FV(s)$. By the induction hypothesis, $\min(A') = \min(B')$, hence, $\min(A) = \min(B)$.

• If $t = rs$, $\pi$ ends with $\Rightarrow_E$ and $\pi'$ with $\Rightarrow_{ES}$, then $\Gamma_1 \vdash r : \Psi \Rightarrow A$, $\Gamma_2 \vdash s : \Psi$, $\Gamma_1 \vdash r : S(\Psi' \Rightarrow A')$, and $\Gamma_2 \vdash s : S(\Psi')$, with $B = S(A')$. By the induction hypothesis, $\Psi \Rightarrow \min(A) = \Psi' \Rightarrow \min(A')$, hence $\min(A) = \min(A') = \min(B)$.

• If $\pi$ ends with rule $\leq$, then $\Gamma \vdash t : A'$ with $A' \leq A$. By the induction hypothesis, we have $\min(A') = \min(B)$, and by Lemma 5.5, $\min(A') = \min(A)$. Hence, $\min(A) = \min(B)$. $\square$

**Lemma 5.7 (Generation lemmas).**

• If $\Gamma \vdash x : A$, then $x : \Psi \in \Gamma$, $|\Gamma| \setminus \{\Psi\} \subseteq B$, and $\Psi \leq A$.

• If $\Gamma \vdash \tilde{O}_{S(B)} : A$, then $S(B) \leq A$ and $|\Gamma| \subseteq B$.

• If $\Gamma \vdash |0\rangle : A$, then $\mathbb{B} \leq A$ and $|\Gamma| \subseteq B$.

• If $\Gamma \vdash |1\rangle : A$, then $\mathbb{B} \leq A$ and $|\Gamma| \subseteq B$.

• If $\Gamma \vdash \alpha.t : A$, then $\Gamma' \vdash t : B$, with $\Gamma' \subseteq \Gamma$, $|\Gamma \setminus \Gamma'| \subseteq B$ and $S(B) \leq A$.

• If $\Gamma \vdash (t+u) : A$, then $\Gamma_1 \vdash t : B$ and $\Gamma_2 \vdash u : B$, with $S(B) \leq A$ and $\Gamma_1 \cup \Gamma_2 \subseteq \Gamma$, $|\Gamma \setminus (\Gamma_1 \cup \Gamma_2)| \subseteq B$.

• If $\Gamma \vdash \pi_j t : A$, then $\Gamma' \vdash t : S(\mathbb{B}^n)$, with $\Gamma' \subseteq \Gamma$, $|\Gamma \setminus \Gamma'| \subseteq B$ and $\mathbb{B}^j \times S(\mathbb{B}^{n-j}) \leq A$.

• If $\Gamma \vdash ?t \cdot r : A$, then $\Gamma \vdash t : B$, $\Gamma \vdash r : B$, with $\mathbb{B} \Rightarrow B \leq A$ and $|\Gamma| \subseteq B$. Moreover, the derivation trees of $\Gamma \vdash t : B$ and $\Gamma \vdash r : B$ are strictly smaller than the derivation tree of $\Gamma \vdash ?t \cdot r : A$.

• If $\Gamma \vdash \lambda x^\Psi.t : A$, then $\Gamma'', x : \Psi \vdash t : B$, with $\Gamma' \subseteq \Gamma$, $\Psi \Rightarrow B \leq A$ and $|\Gamma \setminus \Gamma'| \subseteq B$. Moreover, the derivation tree of $\Gamma'', x : \Psi \vdash t : B$ is strictly smaller than the derivation tree of $\Gamma \vdash \lambda x^\Psi.t : A$.

• If $\Gamma \vdash tu : A$, then one of the following possibilities happens:

- $\Gamma_1 \vdash t : \Psi \Rightarrow B$ and $\Gamma_2 \vdash u : \Psi$, with $B \leq A$, or

- $\Gamma_1 \vdash t : S(\Psi \Rightarrow B)$ and $\Gamma_2 \vdash u : S(\Psi)$, with $S(B) \leq A$.

In both cases, $\Gamma_1 \cup \Gamma_2 \subseteq \Gamma$ and $|\Gamma| \setminus |\Gamma_1 \cup \Gamma_2| \subseteq B$.
* If $\Gamma \vdash t \times u : A$, then $\Gamma_1 \vdash t : B$ and $\Gamma_2 \vdash u : C$, with $\Gamma_1 \cup \Gamma_2 \subseteq \Gamma$, $|\Gamma \setminus (\Gamma_1 \cup \Gamma_2)| \subseteq B$ and $B \times C \preceq A$.

* If $\Gamma \vdash \text{head } t : A$, then $\Gamma' \vdash t : \mathbb{B}^n$, with $\Gamma' \subseteq \Gamma$, $|\Gamma \setminus \Gamma'| \subseteq B$ and $\mathbb{B} \preceq A$.

* If $\Gamma \vdash \text{tail } t : A$, then $\Gamma' \vdash t : \mathbb{B}^n$, with $\Gamma' \subseteq \Gamma$, $|\Gamma \setminus \Gamma'| \subseteq B$ and $\mathbb{B}^{n-1} \preceq A$.

* If $\Gamma \vdash \Uparrow_r t : A$, then $\Gamma' \vdash t : S(S(B) \times C)$, with $\Gamma' \subseteq \Gamma$, $|\Gamma \setminus \Gamma'| \subseteq B$ and $S(B \times C) \preceq A$.

* If $\Gamma \vdash \Uparrow_l t : A$, then $\Gamma' \vdash t : S(B \times S(C))$, with $\Gamma' \subseteq \Gamma$, $|\Gamma \setminus \Gamma'| \subseteq B$ and $S(B \times C) \preceq A$.

**PROOF.** First notice that if $\Gamma \vdash t : A$ is derivable, then $\Delta \vdash t : B$ is derivable, with $\Gamma \subseteq \Delta$ and $|\Delta \setminus \Gamma| \subseteq B$ (because of rule W) and $A \preceq B$, (because of rule $\preceq$). Notice also that those are the only typing rules changing the sequent without changing the term on the sequent. Rules $\Rightarrow_E$ and $\Rightarrow_{ES}$ and are straightforward to check. All the other rules are syntax directed: one rule for each term. Therefore, the lemma is proven by a straightforward rule by rule analysis.

With an analogous reasoning, the condition on the derivation trees stated in cases $\Gamma \vdash ?t \cdot r : A$ and $\Gamma \vdash \lambda x^\Psi.t : A$ are also straightforward. $\square$

**Corollary 5.8 (Simplification).**

1. If $\vdash (t+u) : A$, then $\vdash t : A$ and $\vdash u : A$.

2. If $\vdash (t+u) : A$, then $A = S(B)$.

3. If $\vdash \alpha.t : A$, then $\vdash t : A$.

4. If $\vdash \alpha.t : A$, then $\vdash \beta.t : A$.

5. If $\vdash \alpha.t : A$, then $A = S(B)$.

**PROOF.** Cf. Appendix A. $\square$

**Corollary 5.9.** If $b \in \mathbb{B}$ and $\vdash b : S(A)$, then $\vdash b : A$.

**PROOF.** By cases analysis on b. Cf. Appendix A. $\square$

**Lemma 5.10.** If $\Gamma \vdash t : A$ and $FV(t) = \emptyset$, then $|\Gamma| \subseteq B$.

**PROOF.** If $FV(t) = \emptyset$ then $\vdash t : A$. If $\Gamma \neq \emptyset$, the only way to derive $\Gamma \vdash t : A$ is by using rule W to form $\Gamma$, hence $|\Gamma| \subseteq B$. $\square$

**Lemma 5.11 (Substitution lemma).** Let $FV(u) = \emptyset$, then if $\Gamma, x : \Psi \vdash t : A$, $\Delta \vdash u : \Psi$, where if $\Psi = \mathbb{B}^n$ then $u \in \mathbb{B}$, we have $\Gamma, \Delta \vdash (u/x)t : A$.

**PROOF.** Notice that due to Lemma 5.10, $|\Delta| \subseteq B$, hence, it suffices to consider $\Delta = \emptyset$. By structural induction on t. Cf. Appendix A. $\square$

Since the strategy is weak, subject reduction is proven for closed terms.

**Theorem 5.12 (Subject reduction on closed terms).** For any closed terms $t$ and $u$ and type $A$, if $t \rightarrow^{(p)} u$ and $\vdash t : A$, then $\vdash u : A$.

**PROOF.** By induction on the rewrite relation. Cf. Appendix A. $\square$
## 6. Strong normalization

In this section we adapt Tait's proof of strong normalization of the simply typed lambda calculus to show the same property in our calculus.

Let $|t|$ be the size of the longest reduction sequence started in $t$ and $\mathbf{SN} = \{t \mid |t| < \infty\}$. Also, let $t$ of type $A$, then $\mathbf{Red}(t) = \{r : A \mid t \to_{(p)} r\}$. Notice that Theorem 5.12 proves the Subject Reduction only for closed terms, that is why the definition of $\mathbf{Red}(t)$ requires a condition on types.

**Definition 6.1.** We define the following measure $||t||$ on terms:

$$ \begin{align*} ||x|| &= 0 & ||tu|| &= (3||t|| + 2)(3||u|| + 2) \\ ||\vec{0}_{S(A)}|| &= 0 & ||t \times u|| &= ||t|| + ||u|| \\ |||0⟩⟩ &= 0 & ||\text{head } t|| &= ||t|| + 1 \\ |||1⟩⟩ &= 0 & ||\text{tail } t|| &= ||t|| + 1 \\ ||\lambda x^{\Psi}.t|| &= ||t|| & ||\pi_j t|| &= ||t|| \\ ||(t + r)|| &= ||t|| + ||r|| + 2 & ||?t \cdot r|| &= ||t|| + ||r|| \\ ||\alpha.t|| &= 2||t|| + 1 & ||\Uparrow t|| &= ||t|| \end{align*} $$

**Lemma 6.2.** If $t \to_{(1)} r$ by any of the rules in the groups linear distribution, vector space axioms or lists, or their contextual closure, then $||r|| \ge ||t||$. Moreover, $||r|| = ||t||$ if and only if the rule is (zeroS).

**PROOF.** By induction and rule by rule analysis. Cf. Appendix B. $\square$

**Lemma 6.3.** If for every $i \in \{1, \dots, n\}$ we have $r_i \in \mathbf{SN}$, then $\sum_{i=1}^n [\alpha.]r_i \in \mathbf{SN}$.

**PROOF.** By induction on the lexicographic order of $(\sum_{i=1}^n |r_i|, ||\sum_{i=1}^n [\alpha.]r_i||)$. Cf. Appendix B. $\square$

**Lemma 6.4.** If $t \in \mathbf{SN}$, then $\pi_j t \in \mathbf{SN}$.

**PROOF.** By induction on $|t|$. Cf. Appendix B. $\square$

From now on, $\sum_{i=1}^0 t_i = \vec{0}_{S(A)}$ where $A$ can be determined by the context.

As usual, we associate to each type $A$ a set of strongly normalising terms $(A]$. However, since reduction depends on types, these sets must be sets of typed terms, otherwise we would need to consider ill-typed reductions, which would make the proof more complex.

**Definition 6.5.** For each type $A$ we define a set of strongly normalising terms as follows:

$$ \begin{align*} (\mathbb{B}] &= \{t : S(\mathbb{B}) \mid t \in \mathbf{SN}\} \\ (A \times B] &= \{t : S(S(A) \times S(B)) \mid t \in \mathbf{SN}\} \\ (\Psi \Rightarrow A] &= \{t : S(\Psi \Rightarrow A) \mid \forall r \in (\Psi], \text{tr} \in (A]\} \\ (S(A)] &= \{t : S(A) \mid t \in \mathbf{SN}\} \end{align*} $$
We define a set of neutral terms (Definition 6.6), in order to prove that for every type, its interpretation have the so-called CR3 property (Lemma 6.7), that is, the closure by anti-reduction of neutral terms. Such a property will be useful to prove the adequacy lemma (Lemma 6.9).

**Definition 6.6.** The set of neutral terms ($\mathcal{N}$) is defined by the following grammar:

$$n := tt \mid head \ t \mid tail \ t$$

where $t$ is any term produced by the grammar from Table 7.

**Lemma 6.7.** For all $A$, the following properties hold:

(CR1) If $t \in (A)$, then $t \in \mathbf{SN}$.

(CR2) If $t \in (A)$, then $\mathrm{Red}(t) \subseteq (A)$.

(CR3) If $t \in \mathcal{N}$, $t$ has the same type as all the terms in $(A)$, and $\mathrm{Red}(t) \subseteq (A)$ then $t \in (A)$.

(HAB) For all $x^A$, $x \in (A)$.

(LIN1) If $t \in (A)$ and $r \in (A)$, then $t + r \in (A)$.

(LIN2) If $t \in (A)$ then $\alpha.t \in (A)$.

(NULL) $\vec{\emptyset}_{S(A)} \in (A)$

PROOF. By induction over $A$. Cf. Appendix B. $\square$

**Lemma 6.8.** If $A \preceq B$ then $(A) \subseteq (B)$.

PROOF. By induction on the relation $\preceq$. Cf. Appendix B. $\square$

Let $\theta$ be a substitution of variables by terms. We write $\theta \vdash \Gamma$ if for every $x : A \in \Gamma$, $\theta(x) \in (A)$.

**Lemma 6.9 (Adequacy).** If $\Gamma \vdash t : A$ and $\theta \vdash \Gamma$ then $\theta(t) \in (A)$.

PROOF. By induction in the derivation of $\Gamma \vdash t : A$. Cf. Appendix B. $\square$

**Theorem 6.10 (Strong normalization).** If $\Gamma \vdash t : A$ then $t \in \mathbf{SN}$.

PROOF. By Lemma 6.9, if $\theta \vdash \Gamma$, then $\theta(t) \in (A)$. By Lemma 6.7 (CR1), $(A) \subseteq \mathbf{SN}$. Finally, by Lemma 6.7 (HAB), $\vdash \Gamma$, hence $t \in \mathbf{SN}$. $\square$
## 7. Interpretation

We consider vector spaces equipped with a canonical base, and subsets of such spaces.

Let $E$ and $F$ be two vector spaces with canonical bases $B = \{\vec{b}_i | i \in I\}$ and $C = \{\vec{c}_j | j \in J\}$. The tensor product $E \otimes F$ of $E$ and $F$ is the vector space of canonical base $\{\vec{b}_i \times \vec{c}_j | i \in I \text{ and } j \in J\}$, where $\vec{b}_i \times \vec{c}_j$ is the ordered pair formed with the vector $\vec{b}_i$ and the vector $\vec{c}_j$. The operation $\otimes$ is extended to the vectors of $E$ and $F$ by making pairs bilinear: $(\sum_i \alpha_i \cdot \vec{b}_i) \otimes (\sum_j \beta_j \cdot \vec{c}_j) = \sum_{ij} \alpha_i \cdot \beta_j \cdot (\vec{b}_i \times \vec{c}_j)$.

Let $E$ and $F$ be two vector spaces equipped with bases $B$ and $C$, and $S$ and $T$ be two subsets of $E$ and $F$ respectively, we define the set $S \times T$, subset of the vector space $E \otimes F$, as follows: $S \times T = \{\vec{u} \times \vec{v} | \vec{u} \in S, \vec{v} \in T\}$. Remark that $E \times F$ differs from $E \otimes F$. For instance, if $E$ and $F$ are $\mathbb{C}^2$ equipped with the base $\{\vec{i}, \vec{j}\}$, then $E \times F$ contains $\vec{i} \times \vec{i}$ and $\vec{j} \times \vec{j}$ but not $\vec{i} \times \vec{i} + \vec{j} \times \vec{j}$, that is not a Cartesian product of two vectors of $\mathbb{C}^2$. Let $E$ be a vector space equipped with a base $B$, and $S$ a subset of $E$. We write $S(S)$ for the vector space over $\mathbb{C}$ generated by the span of $S$, that is, containing all the linear combinations of elements of $S$. Hence, if $E$ and $F$ are two vector spaces of bases $B$ and $C$ then $E \otimes F = S(B) \otimes S(C) = S(B \times C)$.

Let $S$ and $T$ be two sets. We write $S \to T$ for the vector space of formal linear combination of functions from $S$ to $T$. The set $S \Rightarrow T$ the set of the functions from $S$ to $T$ is a subset—and even a basis—of this vector space. Note that if $S$ and $T$ are two sets, then $S \to T = S(S \Rightarrow T)$.

To each type we associate the subset of some vector space

$$ 
\begin{align*}
[\mathbb{B}] &= \{(\begin{smallmatrix} 1 \\ 0 \end{smallmatrix}), (\begin{smallmatrix} 0 \\ 1 \end{smallmatrix})\}, \text{ a subset of } \mathbb{C}^2 \\
[\Psi \Rightarrow A] &= [\Psi] \Rightarrow [A] \\
[A \times B] &= [A] \times [B] \\
[S(A)] &= S[A]
\end{align*}
$$

Remark that $[S(\mathbb{B} \times \mathbb{B})] = S([\mathbb{B}] \times [\mathbb{B}]) \simeq [\mathbb{B}] \otimes [\mathbb{B}] = \mathbb{C}^2 \otimes \mathbb{C}^2 = \mathbb{C}^4$.

If $\Gamma = x_1 : \Psi_1, \dots, x_n : \Psi_n$ is a context, then a $\Gamma$-valuation is a function mapping each $x_i$ to $[\Psi_i]$.

We now would associate to each term $t$ of type $A$ an element $[t]$ of $[A]$. But as our calculus is probabilistic, due to the presence of a measurement operator, we must associate to each term a set of elements of $[A]$.

Let $t$ be a term of type $A$ in $\Gamma$ and $\phi$ a $\Gamma$-valuation. We define the interpretation of $t$, $[t]_{\phi}$ as follows.

$$ 
\begin{align*}
[\dot{x}]_{\phi} &= \phi x \\
[\lambda x^{\Psi}.t]_{\phi} &= \{f \mid \forall a \in [\Psi], fa \in [t]_{\phi, x \mapsto [\Psi]}\} \\
[\dot{|0}]_{\phi} &= \{(\begin{smallmatrix} 1 \\ 0 \end{smallmatrix})\} \\
[\dot{|1}]_{\phi} &= \{(\begin{smallmatrix} 0 \\ 1 \end{smallmatrix})\}
\end{align*}
$$
$$[t \times u]_{\phi} = [t]_{\phi} \times [u]_{\phi}$$

$$[\langle t + u \rangle]_{\phi} = \{a + b \mid a \in [t]_{\phi} \text{ and } b \in [u]_{\phi}\}$$

$$[\alpha.t]_{\phi} = \{\alpha.a \mid a \in [t]_{\phi}\}$$

$$[\vec{0}_{S(B)}]_{\phi} = \{\vec{0}\}, \text{ the null vector of the vector space } [[S(B)]]$$

$$[tu]_{\phi} = \begin{cases} \left\{ \sum_{i \in I} \alpha_i.g_i(a) \mid \sum_{i \in I} \alpha_i.g_i \in [t]_{\phi}, a \in [u]_{\phi} \right\} & \text{If } \Gamma \vdash t : \Psi \Rightarrow A \\ \left\{ \sum_{i \in I} \sum_{j \in J} \alpha_i.\beta_j.g_i(c_j) \mid \sum_{i \in I} \alpha_i.g_i \in [t]_{\phi}, \sum_{j \in J} \beta_j.c_j \in [u]_{\phi} \right\} & \text{If } \Gamma \vdash t : S(\Psi \Rightarrow A) \end{cases}$$

$$[\pi_j t]_{\phi} = \{ \prod_{h=1}^{j} b_{hk} \times \sum_{i \in P} \left( \frac{\alpha_i}{\sqrt{\sum_{r \in P} |\alpha_r|^2}} \right) \prod_{h=j+1}^{m} b_{hi} \mid \forall i \in P, \forall h, b_{hi} = b_{hk} \}$$

$$\text{where } [t]_{\phi} = \{ \sum_{i=1}^{n} \prod_{h=1}^{m} b_{hi} \} \text{ with } b_{hi} = \begin{pmatrix} 0 \\ 1 \end{pmatrix} \text{ or } \begin{pmatrix} 1 \\ 0 \end{pmatrix}$$

$$[?t.r]_{\phi} = \{f \mid \forall a \in [\mathbb{B}], fa = \begin{cases} [t]_{\phi} & \text{If } a = \begin{pmatrix} 0 \\ 1 \end{pmatrix} \\ [r]_{\phi} & \text{If } a = \begin{pmatrix} 1 \\ 0 \end{pmatrix} \end{cases} \}$$

$$[\text{head } t]_{\phi} = \{a_1 \mid \prod_{i=1}^{n} a_i \in [t]_{\phi}, a_1 \in [\mathbb{B}]\}$$

$$[\text{tail } t]_{\phi} = \{ \prod_{i=2}^{n} a_i \mid \prod_{i=1}^{n} a_i \in [t]_{\phi}, a_1 \in [\mathbb{B}] \}$$

$$[\Uparrow t]_{\phi} = [t]_{\phi}$$

**Lemma 7.1.** If $A \preceq B$, then $[A] \subseteq [B]$.

**PROOF.** By induction on the relation $\preceq$. Cf. Appendix C. $\square$

**Lemma 7.2.** If $\Gamma \vdash t : A$ and $\phi, x \mapsto S, y \mapsto S$ is a $\Gamma$-valuation, then $[t]_{\phi, x \mapsto S, y \mapsto S} = [(x/y)t]_{\phi, x \mapsto S}$.

**PROOF.** By induction on $t$. Cf. Appendix C. $\square$

**Theorem 7.3.** If $\Gamma \vdash t : A$, and $\phi$ is a $\Gamma$-valuation. Then $[t]_{\phi} \subseteq [A]$.

**PROOF.** By induction on the typing derivation. Cf. Appendix C. $\square$

**Theorem 7.4.** If $\Gamma \vdash t : A$, $\phi$ is a $\Gamma$-valuation, and $t \rightarrow_{(p_i)} r_i$, with $\sum_i p_i = 1$, then $[t]_{\phi} = \bigcup_i [r_i]_{\phi}$.

**PROOF.** We proceed by induction on the rewrite relation.

($\beta_b$) and ($\beta_n$) Let $\vdash (\lambda x^{\Psi}.t)u : A$, with $\vdash u : \Psi$, where, if $\Psi = \mathbb{B}^n$, then $u \in \mathcal{B}$. Then by Lemma 5.7, one of the following possibilities happens:
1. $\vdash \lambda x^\Psi.t : \Psi' \Rightarrow B$ and $\vdash u : \Psi'$, with $B \preceq A$. Thus, $\llbracket (\lambda x^\Psi.t)u \rrbracket_\phi = \{f(a) \mid a \in \llbracket u \rrbracket_\phi\} \subseteq \llbracket t \rrbracket_{\phi, x \mapsto \llbracket \Psi \rrbracket}$.

2. $\vdash \lambda x^\Psi.t : S(\Psi' \Rightarrow B)$ and $\vdash u : S(\Psi')$, with $S(B) \preceq A$. Thus, $\llbracket (\lambda x^\Psi.t)u \rrbracket_\phi = \{\sum_{j \in J} \beta_j.f(c_j) \mid \sum_{j \in J} \beta_j.c_j \in \llbracket u \rrbracket_\phi\} \subseteq \llbracket t \rrbracket_{\phi, x \mapsto \llbracket \Psi \rrbracket}$.

In any case, by Lemma 7.2, $\llbracket t \rrbracket_{\phi, x \mapsto \llbracket \Psi \rrbracket} = \llbracket (u/x)t \rrbracket_\phi$.

**Other cases** All the remaining cases are straightforward by the algebraic nature of the interpretation. □

## 8. Examples

In this section we show that our language is expressive enough to express the Deutsch algorithm (Section 8.1) and the Teleportation algorithm. (Section 8.2).

### 8.1. Deutsch algorithm

The Deutsch algorithm tests whether the binary function $f$ implemented by the oracle $U_f$ is constant ($f(0) = f(1)$) or balanced ($f(0) \neq f(1)$). The algorithm is as follows: it starts with a qubit in state $|0\rangle$ and another in state $|1\rangle$, and applies Hadamard gates to both. Then it applies the $U_f$ operator, followed by a Hadamard and a measurement to the first qubit. When the function is constant, the first qubit ends in $|0\rangle$, when it is balanced, it ends in $|1\rangle$.

The Hadamard gate ($H$) produces $\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle)$ when applied to $|0\rangle$ and $\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle)$ when applied to $|1\rangle$. Hence, it can be implemented with the if-then-else construction: $H = \lambda x^\mathbb{B} \cdot \frac{1}{\sqrt{2}} \cdot (|0\rangle + (x?(-|1\rangle) \cdot |1\rangle))$. Notice that the abstracted variable has a base type (i.e. non-linear). Hence, if $H$ is applied to a superposition, say $(\alpha. |0\rangle + \beta. |1\rangle)$, it reduces, as expected, in the following way:

$$H(\alpha. |0\rangle + \beta. |1\rangle) \xrightarrow{\text{($\text{lin}_\gamma^+$)}}_{(1)} (H\alpha. |0\rangle + H\beta. |1\rangle) \xrightarrow{\text{($\text{lin}_\gamma^\alpha$)}}_{(1)}^2 (\alpha.H |0\rangle + \beta.H |1\rangle)$$

and then is applied to the base terms. We define $H_1$ as the function taking a two-qubits system and applying $H$ to the first. $H_1 = \lambda x^{\mathbb{B} \times \mathbb{B}} \cdot ((H(\text{head } x)) \times (\text{tail } x))$. Similarly, $H_{\text{both}}$ applies $H$ to both qubits.

$$H_{\text{both}} = \lambda x^{\mathbb{B} \times \mathbb{B}} \cdot ((H(\text{head } x)) \times (H(\text{tail } x)))$$

The gate $U_f$ is called *oracle*, and it is defined by $U_f|xy\rangle = |x, y \oplus f(x)\rangle$ where $\oplus$ is the addition modulo 2. In order to implement it, we need the *not* gate, which can be implemented similarly to the Hadamard gate:

$$\text{not} = \lambda x^{\mathbb{B}} \cdot (x?|0\rangle \cdot |1\rangle)$$

Then, the $U_f$ gate is implemented by:

$$U_f = \lambda x^{\mathbb{B} \times \mathbb{B}} \cdot ((\text{head } x) \times ((\text{tail } x)?(\text{not } (f(\text{head } x)))) \cdot (f(\text{head } x))))$$

where $f$ is a given term of type $\mathbb{B} \Rightarrow \mathbb{B}$.
<figure><img src="image_5.png" /><figcaption>Figure 1: Teleportation circuit</figcaption></figure>

Finally, the Deutsch algorithm combines all the previous definitions:

$$ \text{Deutsch}_f = \pi_1 (\hat{\uparrow}_r \text{H}_1 (\text{U}_f \hat{\uparrow}_\ell \hat{\uparrow}_r \text{H}_{\text{both}} (|0\rangle \times |1\rangle))) $$

The casts after the Hadamards are needed to fully develop the qubits and then be able to use it as an argument of a non-linear abstraction (i.e. an abstraction expecting for base terms and so linear-distributing over superpositions). The Deutsch_f term is typed, as expected, by $\vdash$ Deutsch_f : $\mathbb{B} \times S(\mathbb{B})$.

This term, on the identity function, reduces as follows:

$$ \text{Deutsch}_{id} \rightarrow_{(1)}^* \pi_1 \left( \frac{1}{\sqrt{2}} \cdot |1\rangle \times |0\rangle - \frac{1}{\sqrt{2}} \cdot |1\rangle \times |1\rangle \right) \rightarrow_{(\text{proj})} |1\rangle \times \left( \frac{1}{\sqrt{2}} \cdot |0\rangle - \frac{1}{\sqrt{2}} \cdot |1\rangle \right) $$

The trace on this reduction and the type derivation are given in Appendix D.

## 8.2. Teleportation algorithm

The circuit for this algorithm is given in Figure 1.

The cnot gate, which applies not to the second qubit only when the first qubit is $|1\rangle$, can be implemented with an if-then-else construction as follows:

$$ \text{cnot} = \lambda x^{\mathbb{B} \times \mathbb{B}} \cdot ((\text{head } x) \times ((\text{head } x)?(\text{not } (\text{tail } x)) \cdot (\text{tail } x))) $$

We define $H_1^3$ to apply $H$ to the first qubit of a three-qubit system.

$$ H_1^3 = \lambda x^{\mathbb{B} \times \mathbb{B} \times \mathbb{B}} \cdot ((\text{H } (\text{head } x)) \times (\text{tail } x)) $$

Remark that the only difference with $H_1$ is the type of the abstracted variable. In addition, we need to apply cnot to the two first qubits, so we define $\text{cnot}_1^3$ as

$$ \text{cnot}_1^3 = \lambda x^{\mathbb{B} \times \mathbb{B} \times \mathbb{B}} \cdot ((\text{cnot } (\text{head } x \times (\text{head tail } x))) \times (\text{tail tail } x)) $$

The Z gate returns $|0\rangle$ when it receives $|0\rangle$, and $-|1\rangle$ when it receives $|1\rangle$. Hence, it can be implemented by:

$$ Z = \lambda x^{\mathbb{B}} \cdot (x(?(-|1\rangle) \cdot |0\rangle)) $$

The Bob side of the algorithm will apply Z and/or not according to the bits it receives from Alice. Hence, for any $\vdash U : \mathbb{B} \Rightarrow S(\mathbb{B})$ or $\vdash U : \mathbb{B} \Rightarrow \mathbb{B}$, we define
$U^{(b)}$ to be the function which depending on the value of a base qubit $b$ applies the $U$ gate or not:

$$U^{(b)} = (\lambda x^{\mathbb{B}}.\lambda y^{\mathbb{B}}.(x?Uy·y)) b$$

Alice and Bob parts of the algorithm are defined separately:

$$\text{Alice} = \lambda x : S(\mathbb{B}) \times S(\mathbb{B} \times \mathbb{B})(\pi_2(\upharpoonright_r H_1^3 (\text{cnot}_{12}^3 \upharpoonright \ell \upharpoonright_r x)))$$

Notice that before passing to $\text{cnot}_{12}^3$ the parameter of type $S(\mathbb{B}) \times S(\mathbb{B} \times \mathbb{B})$, we need to fully develop the term using the two casts, and again, after the Hadamard gate. Bob side is implemented by

$$\text{Bob} = \lambda x^{\mathbb{B} \times \mathbb{B}}.(Z^{(\text{head } x)}(\text{not}^{(\text{head tail } x)}(\text{tail tail } x)))$$

The teleportation is applied to an arbitrary qubit and to the following Bell state

$$\beta_{00} = (\frac{1}{\sqrt{2}}. |0\rangle \times |0\rangle + \frac{1}{\sqrt{2}}. |1\rangle \times |1\rangle)$$

and it is defined by:

$$\text{Teleportation} = \lambda q^{S(\mathbb{B})}.(\text{Bob}(\upharpoonright_{\ell} \text{Alice} (q \times \beta_{00})))$$

This term is typed, as expected, by: $\vdash$ Teleportation : $S(\mathbb{B}) \Rightarrow S(\mathbb{B})$ and applying the teleportation to any superposition $(\alpha. |0\rangle + \beta. |1\rangle)$ will reduce, as expected, to $(\alpha. |0\rangle + \beta. |1\rangle)$. The trace on this reduction and the type derivation are given in Appendix E.

## 9. Conclusion

In this paper we have proposed a way to unify logic-linear and algebraic-linear quantum $\lambda$-calculi, by interpreting $\lambda$-terms as linear functions when they expect duplicable data and as non-linear ones when they do not, and illustrated this idea with the definition of a calculus.

This calculus is first-order in the sense that variables do not have functional types. In a higher-order version we should expect abstractions to be clonable. But, allowing cloning abstractions allows cloning superpositions, by hiding them inside. For example, $\lambda x^{\mathbb{B}} \Rightarrow \mathbb{B}.(\frac{1}{\sqrt{2}}. |0\rangle + \frac{1}{\sqrt{2}}. |1\rangle)$. It has been argued [10, 13] that what is cloned is not the superposition but a function that creates the superposition, because we had no way there to create such an abstraction from an arbitrary superposition. The situation is different in the calculus presented in this paper as the term $\lambda x^{S(\mathbb{B})}.\lambda y^{\mathbb{B}}.x$ precisely takes any term $t$ of type $S(\mathbb{B})$ and returns the term $\lambda y^{\mathbb{B}}.t$. So, a cloning machine could be constructed by encapsulating any superposition $t$ under a lambda, which transform it into a basis term, so a clonable term. Extending this calculus to the higher-order will require characterizing precisely the abstractions that can be taken as arguments, not allowing to duplicate functions creating superpositions.
Acknowledgements

We would like to thank Eduardo Bonelli, Octavio Malherbe, Luca Paolini, Simona Ronchi della Rocca and Luca Roversi for interesting comments and suggestions in an early draft of this work.

References

[1] A. Díaz-Caro, G. Dowek, Typing quantum superpositions and measurement, in: C. Martín-Vide, R. Neruda, M. A. Vega-Rodríguez (Eds.), Theory and Practice of Natural Computing (TPNC 2017), Vol. 10687 of Lecture Notes in Computer Science, Springer, Cham, 2017, pp. 281–293.

[2] J. P. Rinaldi, Demostrando normalización fuerte sobre una extensión cuántica del lambda cálculo, Master's thesis, Universidad Nacional de Rosario, Argentina, (to be defended) (2018).

[3] J.-Y. Girard, Linear logic, Theoretical Computer Science 50 (1987) 1–102.

[4] S. Abramsky, Computational interpretations of linear logic, Theoretical Computer Science 111 (1) (1993) 3–57.

[5] T. Altenkirch, J. Grattage, A functional quantum programming language, in: Proceedings of LICS 2005, IEEE, 2005, pp. 249–258.

[6] P. Selinger, B. Valiron, Quantum lambda calculus, in: S. Gay, I. Mackie (Eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 2009, Ch. 9, pp. 135–172.

[7] A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, B. Valiron, Quipper: a scalable quantum programming language, ACM SIGPLAN Notices (PLDI’13) 48 (6) (2013) 333–342.

[8] M. Pagani, P. Selinger, B. Valiron, Applying quantitative semantics to higher-order quantum computing, ACM SIGPLAN Notices (POPL’14) 49 (1) (2014) 647–658.

[9] M. Zorzi, On quantum lambda calculi: a foundational perspective, Mathematical Structures in Computer Science 26 (7) (2016) 1107–1195.

[10] P. Arrighi, G. Dowek, Linear-algebraic lambda-calculus, Logical Methods in Computer Science 13 (1:8) (2017).

[11] P. Arrighi, A. Díaz-Caro, A System F accounting for scalars, Logical Methods in Computer Science 8 (1:11) (2012).

[12] A. Díaz-Caro, B. Petit, Linearity in the non-deterministic call-by-value setting, in: L. Ong, R. de Queiroz (Eds.), Proceedings of WoLLIC 2012, Vol. 7456 of LNCS, 2012, pp. 216–231.
[13] P. Arrighi, A. Díaz-Caro, B. Valiron, The vectorial lambda-calculus, Information and Computation 254 (1) (2017) 105–139.

[14] A. Assaf, A. Díaz-Caro, S. Perdrix, C. Tasson, B. Valiron, Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus, Logical Methods in Computer Science 10 (4:8) (2014).

[15] M. Nielsen, I. Chuang, Quantum Computation and Quantum Information, Cambridge University Press., 2000.

[16] G. Jaeger, Quantum information: An overview, Springer, 2007.

[17] W. K. Wootters, W. H. Zurek, A single quantum cannot be cloned, Nature 299 (1982) 802–803.

[18] G. E. Peterson, M. E. Stickel, Complete sets of reductions for some equational theories, Journal of the ACM 28 (2) (1981) 233–264.

[19] A. Díaz-Caro, A lambda calculus for density matrices with classical and probabilistic controls, in: B.-Y. E. Chang (Ed.), Programming Languages and Systems (APLAS 2017), Vol. 10695 of Lecture Notes in Computer Science, Springer, Cham, 2017, pp. 448–467.

[20] A. Barber, Dual intuitionistic linear logic, Tech. Rep. ECS-LFCS-96-347, The Laboratory for Foundations of Computer Science, University of Edinburgh (1996).
# Appendix A. Detailed proofs of Section 5 (Subject reduction)

## Corollary 5.8 (Simplification).

1. If $\vdash (t+u) : A$, then $\vdash t : A$ and $\vdash u : A$.

2. If $\vdash (t+u) : A$, then $A = S(B)$.

3. If $\vdash \alpha.t : A$, then $\vdash t : A$.

4. If $\vdash \alpha.t : A$, then $\vdash \beta.t : A$.

5. If $\vdash \alpha.t : A$, then $A = S(B)$.

## PROOF.

1. By Lemma 5.7, $\vdash t : B$ and $\vdash u : B$, with $B \preceq S(B) \preceq A$, then, we conclude by rule $\preceq$.

2. By Lemma 5.7, $\vdash t : C$ and $\vdash u : C$, with $C \preceq S(C) \preceq A$, but then, by Lemma 5.2, $A = S(B)$ for some type $B$.

3. By Lemma 5.7, $\vdash t : B$, with $S(B) \preceq A$, then, we conclude by rule $\preceq$.

4. By Lemma 5.7, $\vdash t : B$, with $S(B) \preceq A$, then we conclude by rules $S_I^\alpha$ and $\preceq$.

5. By Lemma 5.7, $\vdash t : C$ with $S(C) \preceq A$, but then, by Lemma 5.2, $A = S(B)$ for some type $B$. $\square$

**Corollary 5.9.** If $b \in \mathcal{B}$ and $\vdash b : S(A)$, then $\vdash b : A$.

PROOF. We proceed by cases on $b$.

* Let $b = \lambda x^\Psi.t$. Then, by Lemma 5.7, $x : \Psi \vdash t : B$, with $\Psi \Rightarrow B \preceq S(A)$, and so $\Psi \Rightarrow B \preceq A$, and we conclude by rule $\preceq$.

* Let $b = |0\rangle$. Then, by Lemma 5.7, $\mathcal{B} \preceq S(A)$, hence $\mathcal{B} \preceq A$ and we conclude by rule $\preceq$.

* Let $b = |1\rangle$. Analogous to previous case.

* Let $b = b_1 \times b_2$. Then, by Lemma 5.7, $\vdash b_1 : B_1, \vdash b_2 : B_2$, and $B_1 \times B_2 \preceq S(A)$. Hence, $B_1 \times B_2 \preceq A$ and we conclude by rule $\preceq$. $\square$

**Lemma 5.11 (Substitution lemma).** Let $FV(u) = \emptyset$, then if $\Gamma, x : \Psi \vdash t : A$, $\Delta \vdash u : \Psi$, where if $\Psi = \mathcal{B}^n$ then $u \in \mathcal{B}$, we have $\Gamma, \Delta \vdash (u/x)t : A$.

PROOF. Notice that due to Lemma 5.10, $|\Delta| \subseteq \mathcal{B}$, hence, it suffices to consider $\Delta = \emptyset$. We proceed by structural induction on $t$.

The set of terms be divided in the following groups:

$$ \text{unclassified} := x \mid \lambda x^\Psi.t $$

$$ \text{arity}^0 := \tilde{\emptyset}_{S(A)} \mid |0\rangle \mid |1\rangle $$

$$ \text{arity}^1(r) := \pi_j r \mid \alpha.r \mid \text{head } r \mid \text{tail } r \mid \Uparrow_r t \mid \Uparrow_\ell t $$

$$ \text{arity}^2(r)(s) := rs \mid (r+s) \mid r \times s \mid ?r \cdot s $$

Hence, we can consider the terms by groups:
$t = x$. By Lemma 5.7, $|\Gamma| \subseteq \mathbf{B}$ and $\Psi \preceq A$. Since $(u/x)x = u$, we have $\vdash (u/x)x : \Psi$. Hence, since $\Psi \preceq A$, by rule $\preceq$, $\vdash (u/x)x : A$. Finally, since $|\Gamma| \subseteq \mathbf{B}$, by rule W, we have $\Gamma \vdash (u/x)x : A$.

$t = y \neq x$. By Lemma 5.7, $y : \Psi' \in \Gamma$, $(|\Gamma| \cup \{\Psi\}) \setminus \{\Psi'\} \subseteq \mathbf{B}$ and $\Psi' \preceq A$. Hence, by rule $\preceq$, $y : \Psi' \vdash y : A$. Since $|\Gamma| \subseteq \mathbf{B}$, by rule W, we have $\Gamma \vdash y : A$. Finally, since $(u/x)y = y$, we have $\Gamma \vdash (u/x)y : A$.

$t = \lambda y \Psi'.v$. Without loss of generality, assume $y$ is does not appear free in $u$. By Lemma 5.7, $\Gamma', y : \Psi' \vdash v : B$, with $\Gamma' \subseteq \Gamma \cup \{x : \Psi\}$, $\Psi' \Rightarrow B \preceq A$ and $(|\Gamma| \cup \{\Psi\}) \setminus |\Gamma'| \subseteq \mathbf{B}$. By the induction hypothesis, $\Gamma'', y : \Psi' \vdash (u/x)v : B$, with $\Gamma'' = \Gamma' \setminus \{x : \Psi\}$. Notice that if $x : \Psi \in \Gamma'$, the induction hypothesis applies directly, in other case, $\Psi \in \mathbf{B}$ and so by rule W the context can be enlarged to include $x : \Psi$, hence the induction hypothesis applies in any case. Therefore, by rule $\Rightarrow_I$, $\Gamma'' \vdash \lambda y \Psi'.(u/x)v : \Psi' \Rightarrow B$. Since $\Psi' \Rightarrow B \preceq A$, by rule $\preceq$, $\Gamma'' \vdash \lambda y \Psi'.(u/x)v : A$. Hence, since $|\Gamma| \setminus |\Gamma''| \subseteq \mathbf{B}$, by rule W, $\Gamma \vdash \lambda y \Psi'.(u/x)v : A$. Since $y$ does not appear free in $u$, $\lambda y \Psi'.(u/x)v = (u/x)(\lambda y \Psi'.v)$. Therefore, $\Gamma \vdash (u/x)(\lambda y \Psi'.v) : A$.

**arity⁰ terms** All of these terms are typed by an axiom with a type *B* which, by Lemma 5.7, *B* *≤* *A*. Also, by the same Lemma, *|Γ, x : Ψ|* ⊆ *B*. So, we can type with the axiom, and empty context, $\vdash \text{arity}^0 : B$, and so, by rule W, $\Gamma \vdash \text{arity}^0 : B$. Notice that $\text{arity}^0 = (u/x)\text{arity}^0$. We conclude by rule $\preceq$.

**arity¹(r) terms** By Lemma 5.7, $\Gamma' \vdash r : B$, such that by a derivation tree $T$, $\Gamma' \vdash \text{arity}^1(r) : C$, where $\Gamma' \subseteq (\Gamma \cup \{x : \Psi\})$, $(|\Gamma| \cup \Psi) \setminus |\Gamma'| \subseteq \mathbf{B}$ and $C \preceq A$. If $x : \Psi \notin \Gamma'$, then $\Psi = B$ and so we can extend $\Gamma'$ with $x : \Psi$. Hence, in any case, by the induction hypothesis, $\Gamma' \setminus \{x : \Psi\} \vdash (u/x)r : C$. Then, using the derivation tree $T$, $\Gamma' \setminus \{x : \Psi\} \vdash \text{arity}^1((u/x)r) : C$. Notice that $\text{arity}^1((u/x)r) = (u/x)\text{arity}^1(r)$. We conclude by rules $W$ and $\preceq$.

**arity²(r)(s) terms** By Lemma 5.7, $\Gamma_1 \vdash r : C$ and $\Gamma_2 \vdash s : D$, such that by a typing rule R, $\Gamma_1, \Gamma_2 \vdash \text{arity}^2(r)(s) : E$, with $E \preceq A$, and where $(\Gamma_1 \cup \Gamma_2) \subseteq (\Gamma \cup \{x : \Psi\})$ and $(|\Gamma| \cup \Psi) \setminus (|\Gamma_1| \cup |\Gamma_2|) \subseteq \mathbf{B}$. Therefore, if $x : \Psi \notin \Gamma_i$, $i = 1, 2$, we can extend $\Gamma_i$ with $x : \Psi$ using rule W. Hence, by the induction hypothesis, $\Gamma_1 \setminus \{x : \Psi\} \vdash (u/x)r : C$ and $\Gamma_2 \setminus \{x : \Psi\} \vdash (u/x)s : D$. So, by rule R, $\Gamma_1 \setminus \{x : \Psi\}, \Gamma_2 \setminus \{x : \Psi\} \vdash \text{arity}^2((u/x)r)((u/x)s) : E$. Notice that $\text{arity}^2((u/x)r)((u/x)s) = (u/x)\text{arity}^2(r)(s)$. We conclude by rules $W$ and $\preceq$. □

**Theorem 5.12 (Subject reduction on closed terms).** For any closed terms $t$ and $u$ and type $A$, if $t \rightarrow_{(p)} u$ and $\vdash t : A$, then $\vdash u : A$.

**PROOF.** We proceed by induction on the rewrite relation.

(β_b) and (β_n) Let $\vdash (\lambda x \Psi.t)u : A$, with $\vdash u : \Psi$, where, if $\Psi = \mathbb{B}^n$, then $u \in \mathcal{B}$. Then by Lemma 5.7, one of the following possibilities happens:
1. $\vdash \lambda x^\Psi.t : \Psi' \Rightarrow B$ and $\vdash u : \Psi'$, with $B \preceq A$, or

2. $\vdash \lambda x^\Psi.t : S(\Psi' \Rightarrow B)$ and $\vdash u : S(\Psi')$, with $S(B) \preceq A$.

Thus, in any case, by Lemma 5.7 again, $x : \Psi \vdash t : C$, with, in case 1, $\Psi \Rightarrow C \preceq \Psi' \Rightarrow B$ and in case 2, $\Psi \Rightarrow C \preceq S(\Psi' \Rightarrow B)$. Hence, $\Psi = \Psi'$ and in the first case $C \preceq B \preceq A$, while in the second, $C \preceq B \preceq S(B) \preceq A$, so, in general $C \preceq A$. Since $\vdash u : \Psi$, where if $\Psi = \mathbb{B}^n$, then $u \in \mathbb{B}$, by Lemma 5.11, $\vdash (u/x)t : C$, and by rule $\preceq$, $\vdash (u/x)t : A$.

(if₁) Let $\vdash |1\rangle?u \cdot v : A$. Then, by Lemma 5.7, one of the following possibilities happens:

* $\vdash ?u \cdot v : \Psi \Rightarrow B$ and $\vdash |1\rangle : \Psi$, with $B \preceq A$. Then, by Lemma 5.7 again, $\vdash u : C$, $\vdash v : C$ and $\mathbb{B} \Rightarrow C \preceq \Psi \Rightarrow B$. Hence, $\Psi = \mathbb{B}$ and $C \preceq B \preceq A$.

* $\vdash ?u \cdot v : S(\Psi \Rightarrow B)$ and $\vdash |1\rangle : S(\Psi)$, with $S(B) \preceq A$. Then, by Lemma 5.7 again, $\vdash u : C$, $\vdash v : C$ and $\mathbb{B} \Rightarrow C \preceq S(\Psi \Rightarrow B)$. Hence, $\Psi = \mathbb{B}$ and $C \preceq B \preceq S(B) \preceq A$.

So, by rule $\preceq$, $\vdash u : A$.

(if₀) Analogous to case (if₁).

(lin<sub>r</sub><sup>+</sup>) Let $\vdash t(u + v) : A$, with $\vdash t : \mathbb{B}^n \Rightarrow B$. Then, by Lemma 5.7, one of the following cases happens:

1. $\vdash t : \Psi \Rightarrow C$ and $\vdash (u + v) : \Psi$, with $C \preceq A$. However, since $\vdash t : \mathbb{B}^n \Rightarrow B$, we have $\Psi \in \mathbb{B}$, which is impossible due to Corollary 5.8.

2. $\vdash t : S(\Psi \Rightarrow C)$ and $\vdash (u + v) : S(\Psi)$, with $S(C) \preceq A$. Then, by Corollary 5.8, $\vdash u : S(\Psi)$ and $\vdash v : S(\Psi)$. Hence,

$$ \frac{\frac{\vdash t : S(\Psi \Rightarrow C) \quad \vdash u : S(\Psi) \quad \Rightarrow_{ES}}{\vdash tu : S(C)} \quad \frac{\vdash t : S(\Psi \Rightarrow C) \quad \vdash v : S(\Psi) \quad \Rightarrow_{ES}}{\vdash tv : S(C)} \quad S_I^+}{\frac{\vdash (tu + tv) : S(S(C))}{\vdash (tu + tv) : A} \preceq} \Rightarrow_{ES} $$

(lin<sub>r</sub><sup>α</sup>) Let $\vdash t(\alpha.u) : A$, with $\vdash t : \mathbb{B}^n \Rightarrow B$. Then, by Lemma 5.7, one of the following cases happens:

1. $\vdash t : \Psi \Rightarrow C$ and $\vdash \alpha.u : \Psi$, with $C \preceq A$. However, since $\vdash t : \mathbb{B}^n \Rightarrow B$, we have $\Psi \in \mathbb{B}$, which is impossible due to Corollary 5.8.

2. $\vdash t : S(\Psi \Rightarrow C)$ and $\vdash \alpha.u : S(\Psi)$, with $S(C) \preceq A$. Then, by Corollary 5.8, $\vdash u : S(\Psi)$. Hence,

$$ \frac{\frac{\vdash t : S(\Psi \Rightarrow C) \quad \vdash u : S(\Psi) \quad \Rightarrow_{ES}}{\vdash tu : S(C)} \quad \frac{S_I^\alpha}{\vdash \alpha.tu : S(S(C))} \quad \Rightarrow_{ES}}{\vdash \alpha.tu : A} \preceq $$
(lin<sub>r</sub><sup>0</sup>) Let $\vdash t \vec{0}_{S(\mathbb{B}^n)} : A$, with $\vdash t : \mathbb{B}^n \Rightarrow B$. Then, by Lemma 5.7, one of the following cases happens:

1. $\vdash t : \Psi \Rightarrow C$ and $\vdash \vec{0}_{S(\mathbb{B}^n)} : \Psi$, with $C \preceq A$. Then, by Lemma 5.7 again, $S(\mathbb{B}^n) \preceq \Psi$. However, since $\vdash t : \mathbb{B}^n \Rightarrow B$, $\Psi \in \mathbf{B}$, which is impossible by Lemma 5.2.

2. $\vdash t : S(\Psi \Rightarrow C)$ and $\vdash \vec{0}_{S(\mathbb{B}^n)} : S(\Psi)$, with $S(C) \preceq A$. By rule $Ax_0$, $\vdash \vec{0}_{S(\min(B))} : S(\min(B))$. Since $\vdash t : \mathbb{B}^n \Rightarrow B$ and $\vdash t : S(\Psi \Rightarrow C)$, by Lemma 5.6, we have $\min(\mathbb{B}^n \Rightarrow B) = \min(S(\Psi \Rightarrow C))$, so $\min(B) = \min(C)$. Then, by Lemma 5.4, $\min(B) = \min(C) \preceq C$, then $S(\min(B)) \preceq S(C) \preceq A$, so we conclude by rule $\preceq$.

(lin<sub>l</sub><sup>+</sup>) Let $\vdash (t+u)v : A$. Then by Lemma 5.7, one of the following cases happens:

1. $\vdash (t+u) : \Psi \Rightarrow B$, which is impossible by Corollary 5.8.

2. $\vdash (t+u) : S(\Psi \Rightarrow B)$ and $\vdash v : S(\Psi)$, with $S(B) \preceq A$. Then, by Corollary 5.8, $\vdash t : S(\Psi \Rightarrow B)$ and $\vdash u : S(\Psi \Rightarrow B)$. Hence,

$$ \frac{\frac{\vdash t : S(\Psi \Rightarrow B) \quad \vdash v : S(\Psi)}{\vdash tv : S(B)} \Rightarrow_{ES} \frac{\vdash u : S(\Psi \Rightarrow B) \quad \vdash v : S(\Psi)}{\vdash uv : S(B)} S_I^+}{\frac{\vdash (tv + uv) : S(S(B))}{\vdash (tv + uv) : A} \preceq} \Rightarrow_{ES} $$

(lin<sub>l</sub><sup>α</sup>) Let $\vdash (\alpha.t)u : A$. Then, by Lemma 5.7, one of the following cases happens:

1. $\vdash \alpha.t : \Psi \Rightarrow B$, which is impossible by Corollary 5.8.

2. $\vdash \alpha.t : S(\Psi \Rightarrow B)$ and $\vdash u : S(\Psi)$, with $S(B) \preceq A$. Then, by Corollary 5.8, $\vdash t : S(\Psi \Rightarrow B)$. Hence,

$$ \frac{\frac{\vdash t : S(\Psi \Rightarrow B) \quad \vdash u : S(\Psi)}{\vdash tu : S(B)} \Rightarrow_{ES} \frac{\vdash \alpha.tu : S(S(B))}{\vdash \alpha.tu : A} S_I^\alpha}{\preceq} $$

(lin<sub>l</sub><sup>0</sup>) Let $\vdash \vec{0}_{S(\mathbb{B} \Rightarrow B)}t : A$. Then, by Lemma 5.7, one of the following cases happens:

1. $\vdash \vec{0}_{S(\mathbb{B} \Rightarrow B)} : \Psi \Rightarrow C$ and $\vdash t : \Psi$, with $C \preceq A$. Then, by Lemma 5.7 again, $S(\mathbb{B} \Rightarrow B) \preceq \Psi \Rightarrow C$, which is impossible by Lemma 5.2.

2. $\vdash \vec{0}_{S(\mathbb{B} \Rightarrow B)} : S(\Psi \Rightarrow C)$ and $\vdash t : S(\Psi)$, with $S(C) \preceq A$. By Lemma 5.7 again, $S(\mathbb{B} \Rightarrow B) \preceq S(\Psi \Rightarrow C)$. By Lemma 5.6, $\min(\mathbb{B} \Rightarrow B) = \min(\Psi \Rightarrow C)$, so $\min(B) = \min(C)$, and by Lemma 5.4, $\min(C) \preceq C$, hence, $\min(B) \preceq C$, and then $S(\min(B)) \preceq S(C) \preceq A$. By rule $Ax_0$, $\vdash \vec{0}_{S(\min(B))} : S(\min(B))$, hence we conclude by rule $\preceq$.
(neutral) Let $\vdash (\vec{0}_{S(A)} + t) : A$. Then, by Corollary 5.8, $\vdash t : A$.

(unit) Let $\vdash 1.t : A$. Then, by Corollary 5.8, $\vdash t : A$.

(zero_α) Let $\vdash 0.t : A$, with $\vdash t : B$. Then, we must show that $\vdash \vec{0}_{S(\min(B))} : A$. By Lemma 5.7, $\vdash t : C$ and $S(C) \preceq A$. By Lemma 5.6, $\min(B) = \min(C)$. By Lemma 5.4, $\min(C) \preceq C$. Therefore, $S(\min(B)) = S(\min(C)) \preceq S(C) \preceq A$. By rule $Ax_0$, $\vdash \vec{0}_{S(\min(B))} : S(\min(B))$, hence we conclude by rule $\preceq$.

(zero) Let $\vdash \alpha.\vec{0}_{S(B)} : A$. By Lemma 5.7, $\vdash \vec{0}_{S(B)} : C$ with $S(C) \preceq A$. Then, by Lemma 5.7 again, $S(B) \preceq C$. In addition, by Lemma 5.4, $\min(B) \preceq B$. Therefore, $S(\min(B)) \preceq S(B) \preceq C \preceq S(C) \preceq A$. Since, by rule $Ax_0$, $\vdash \vec{0}_{S(\min(B))} : S(\min(B))$, we conclude by rule $\preceq$ that $\vdash \vec{0}_{S(\min(B))} : A$.

(prod) Let $\vdash \alpha.(\beta.t) : A$. By Corollary 5.8, $\vdash \beta.t : A$. Then, by Corollary 5.8 again, $\vdash (\alpha \times \beta).t : A$.

(αdist) Let $\vdash \alpha.(t+u) : A$. By Lemma 5.7, $\vdash (t+u) : B$, with $S(B) \preceq A$. Then, by Corollary 5.8, $\vdash t : B$ and $\vdash u : B$. Hence, by rule $S_I^\alpha$, $\vdash \alpha.t : S(B)$ and $\vdash \alpha.u : S(B)$. We conclude by rules $S_I^+$ and $\preceq$.

(fact) Let $\vdash (\alpha.t + \beta.t) : A$. By Corollary 5.8, $\vdash \alpha.t : A$. Then, by Corollary 5.8 again, $\vdash (\alpha + \beta).t : A$.

(fact¹) Let $\vdash (\alpha.t + t) : A$. By Corollary 5.8, $\vdash \alpha.t : A$. Then, by Corollary 5.8 again, $\vdash (\alpha + 1).t : A$.

(fact²) Let $\vdash (t+t) : A$. By Lemma 5.7, $\vdash t : B$, with $S(B) \preceq A$. Then, by rule $S_I^\alpha$, $\vdash 2.t : S(B)$. We conclude by rule $\preceq$.

(zeros) Let $\vdash \vec{0}_{S(A)} : B$. Then, by Lemma 5.7, $S(A) \preceq B$. By Lemma 5.4, $\min(A) \preceq A$, hence $S(\min(A)) \preceq S(A)$. By rule $Ax_0$, $\vdash \vec{0}_{S(\min(A))} : S(\min(A))$, and since $S(\min(A)) \preceq S(A) \preceq B$, we conclude by rule $\preceq$.

(comm) Let $\vdash (u+v) : A$. By Lemma 5.7, $\vdash u : B$ and $\vdash v : B$, with $S(B) \preceq A$. So,

$$ \frac{\frac{\vdash v : B \quad \vdash u : B}{\vdash (v+u) : S(B)} S_I^+}{\vdash (v+u) : A} \preceq $$

(assoc) Let $\vdash ((u+v)+w) : A$. By Lemma 5.7, $\vdash (u+v) : B$ and $\vdash w : B$, with $S(B) \preceq A$. Then, by Corollary 5.8, $\vdash u : B$ and $\vdash v : B$. Hence,

$$ \frac{\frac{\vdash u : B \quad \vdash v : B \quad \vdash w : B}{\vdash (u+v) : S(B)} S_I^+}{\vdash (u+(v+w)) : S(S(B)) S_I^+} \preceq \frac{\vdash (u+(v+w)) : A}{\vdash (u+(v+w)) : A} \preceq $$
(head) Let $\vdash \text{head}(v \times u) : A$, with $v \neq t_1 \times t_2$. Hence, by Lemma 5.7, $\vdash v \times u : \mathbb{B}^n$, with $\mathbb{B} \preceq A$. Then, by Lemma 5.7 again, $\vdash v : B$ and $\vdash u : C$, with $B \times C \preceq \mathbb{B}^n$. Lemma 5.1 $B \times C = \mathbb{B}^n$, so $B = \mathbb{B}^m$. Since $v \in \mathcal{V}$, by Lemma 5.7, $B$ is not a product, and so $B = \mathbb{B} \preceq A$. Therefore, we conclude by rule $\preceq$.

(tail) Analogous to case (head).

(dist_r^+) Let $\vdash \uparrow_r ((r+s) \times u) : A$. By Lemma 5.7, $S(B \times C) \preceq A$ and $\vdash (r+s) \times u : S(S(B) \times C)$. Then, by the same Lemma, $\vdash (r+s) : D$ and $\vdash u : E$, with $D \times E \preceq S(S(B) \times C)$, so by Lemma 5.3, there exists $F, G, n$ such that $S(S(B) \times C) = S^n(F \times G)$ and $D \preceq F$ and $E \preceq G$. Therefore, $n=1$ and $S(B) \times C = F \times G$. Since $\vdash (r+s) : D$, by Lemma 5.7, there exists $H$ such that $S(H) \preceq D$, so by transitivity $S(H) \preceq F$. Then, by Lemma 5.2, $F$ has the form $S(I)$. Therefore, neither $F$ nor $S(B)$ are products, and hence $S(B) = F$ and $C = G$. Hence, $D \preceq S(B)$ and $E \preceq C$, and hence, $\vdash (r+s) : S(B)$ and $\vdash u : C$. Then, by Corollary 5.8, $\vdash r : S(B)$ and $\vdash s : S(B)$. Therefore,

$$ \frac{\frac{\begin{array}{c} \vdash r : S(B) \quad \vdash u : C \\ \vdash r \times u : S(B) \times C \end{array}}{\begin{array}{c} \vdash r \times u : S(S(B) \times C) \\ \vdash \uparrow_r (r \times u) : S(B \times C) \end{array}} \times_I \quad \frac{\begin{array}{c} \vdash s : S(B) \quad \vdash u : C \\ \vdash s \times u : S(B) \times C \end{array}}{\begin{array}{c} \vdash s \times u : S(S(B) \times C) \\ \vdash \uparrow_r (s \times u) : S(B \times C) \end{array}} \times_I \quad \frac{\begin{array}{c} \preceq \\ \uparrow_r \end{array}}{S_I^+} \quad \frac{\begin{array}{c} \vdash (\uparrow_r (r \times u) + \uparrow_r (s \times u)) : S(S(B \times C)) \\ \vdash (\uparrow_r (r \times u) + \uparrow_r (s \times u)) : A \end{array}}{\preceq} $$

(dist_l^+) Analogous to case (dist_r^+).

(dist_r^\alpha) Let $\vdash \uparrow_r ((\alpha.r) \times u) : A$. By Lemma 5.7, $S(B \times C) \preceq A$, and $\vdash ((\alpha.r) \times u) : S(S(B) \times C)$. Then, by the same Lemma, $\vdash \alpha.r : D$ and $\vdash u : E$, with $D \times E \preceq S(S(B) \times C)$, so by Lemma 5.3, there exists $F, G, n$ such that $S(S(B) \times C) = S^n(F \times G)$ and $D \preceq F$ and $E \preceq G$. Therefore, $n=1$ and $S(B) \times C = F \times G$. Since $\vdash \alpha.r : D$, by Lemma 5.7, there exists $H$ such that $S(H) \preceq D$, so by transitivity $S(H) \preceq F$. Then, by Lemma 5.2, $F$ has the form $S(I)$. Therefore, neither $F$ nor $S(B)$ are products, and hence $S(B) = F$ and $C = G$. Hence, $D \preceq S(B)$ and $E \preceq C$, so by rule $\preceq$, $\vdash \alpha.r : S(B)$ and $\vdash u : C$. By Corollary 5.8, $\vdash r : S(B)$. Therefore,

$$ \frac{\frac{\begin{array}{c} \vdash r : S(B) \quad \vdash u : C \\ \vdash r \times u : S(B) \times C \end{array}}{\begin{array}{c} \vdash r \times u : S(S(B) \times C) \\ \vdash \uparrow_r (r \times u) : S(B \times C) \end{array}} \times_I \quad \frac{\begin{array}{c} \preceq \\ \uparrow_r \end{array}}{S_I^\alpha} \quad \frac{\begin{array}{c} \vdash \alpha. \uparrow_r (r \times u) : S(S(B \times C)) \\ \vdash \alpha. \uparrow_r (r \times u) : A \end{array}}{\preceq} $$

(dist_l^\alpha) Analogous to case (dist_r^\alpha).
(dist_r^0) Let $\vdash \Uparrow_r (\vec{0}_{S(B)} \times u) : A$. By Lemma 5.7, $S(B \times C) \preceq A$. By lemma 5.4, $\min(B \times C) \preceq B \times C$, hence, $S(\min(B \times C)) \preceq S(B \times C)$. By rule $Ax_0$, $\vdash \vec{0}_{S(\min(B \times C))} : S(\min(B \times C))$. Hence, since $S(\min(B \times C)) \preceq S(B \times C) \preceq A$, we conclude by rule $\preceq$.

(dist_l^0) Analogous to case $(dist_r^0)$.

(dist_\uparrow^+) Let $\vdash \Uparrow (t+u) : A$. Then, by Lemma 5.7, $S(C \times D) \preceq A$, $\vdash \Uparrow t : S(C \times D)$ and $\vdash \Uparrow u : S(C \times D)$. We conclude by rules $S_I^+$ and $\preceq$.

(dist_\uparrow^\alpha) Let $\vdash \Uparrow (\alpha.t) : A$. Then, by Lemma 5.7, $S(C \times D) \preceq A$, and $\vdash \Uparrow t : S(C \times D)$. We conclude by rules $S_I^\alpha$ and $\preceq$.

(neut_\uparrow^r) Let $\vdash \Uparrow_r (b \times r) : A$, with $b \in B$. Then, by Lemma 5.7, $\vdash b \times r : S(S(B) \times C)$ and $S(B \times C) \preceq A$. Then, by Lemma 5.7 again, $\vdash b : D$ and $\vdash r : E$, with $D \times E \preceq S(S(B) \times C)$. Without lost of generality, let $b = \prod_{i=1}^n b_i$ where each $b_i$ is not a product. Then, by Lemma 5.7, $\vdash b_i : D_i$ with $\prod_{i=1}^n D_i \preceq D$, and, by the same lemma, $D_i$ are not products. Therefore, $D_1 \times \prod_{i=2}^n D_i \times E \preceq S(S(B) \times C)$, so by Lemma 5.3, there exists $F, G, n$ such that $S(S(B) \times C) = S^n(F \times G)$ and $D_1 \preceq F$ and $\prod_{i=1}^n D_i \times E \preceq G$. Therefore, $n=1$ and $S(B) \times C = F \times G$. Since $D_1$ is not a product, $F$ is not a product. Hence, since neither $F$ nor $S(B)$ are products, we have $S(B) = F$ and $C = G$. $D_1 \preceq S(B)$ and $\prod_{i=2}^n D_i \times E \preceq C$, hence, $\vdash b_1 : S(B)$ and $\vdash \prod_{i=2}^n b_i \times r : \prod_{i=2}^n D_i \times E$. Therefore, by Corollary 5.9, $\vdash b_1 : B$, and so, by rule $\times_I$, $\vdash b \times r : B \times C$, and by rule $\preceq$, $\vdash b \times r : S(B \times C)$.

(neut_\uparrow^l) Analogous to case $(neut_r^l)$.

(proj) Let $\vdash \pi_j(\sum_{i=1}^n [\alpha_i.] \prod_{h=1}^m b_{hi}) : A$. Then, by Lemma 5.7, we have that $B^j \times S(B^{m'-1}) \preceq A$. Hence, we have the derivation from Figure A.2.

**Contextual rules** Let $t \rightarrow_{(p)} uv$. Then,

(tv $\rightarrow_{(p)}$ uv) Let $\vdash tv : A$. By Lemma 5.7, one of the following cases happens:

* $\vdash t : \Psi \Rightarrow B$ and $\vdash v : \Psi$, with $B \preceq A$. Then, by the induction hypothesis, $\vdash u : \Psi \Rightarrow B$. We conclude by rules $\Rightarrow_E$ and $\preceq$.

* $\vdash t : S(\Psi \Rightarrow B)$ and $\vdash v : S(\Psi)$, with $S(B) \preceq A$. Then, by the induction hypothesis, $\vdash u : S(\Psi \Rightarrow B)$. We conclude by rules $\Rightarrow_{ES}$ and $\preceq$.

((λx^B.v)t $\rightarrow_{(p)}$ (λx^B.v)u) Let $\vdash (\lambda x^B.v)t : A$. By Lemma 5.7, one of the following cases happens:

* $\vdash (\lambda x^B.v) : \Psi \Rightarrow B$ and $\vdash t : \Psi$, with $B \preceq A$. Then, by the induction hypothesis, $\vdash u : \Psi$. We conclude by rules $\Rightarrow_E$ and $\preceq$.

* $\vdash (\lambda x^B.v) : S(\Psi \Rightarrow B)$ and $\vdash t : S(\Psi)$, with $S(B) \preceq A$. Then, by the induction hypothesis, $\vdash u : S(\Psi)$. We conclude by rules $\Rightarrow_{ES}$ and $\preceq$.
<figure><img src="image_6.png" /><figcaption>**Figure A.2:** Derivation from case (proj) on Theorem 5.12.</figcaption></figure>

((t + v) →$_{(p)}$ (u + v)) Let t (t + v) : A. By Lemma 5.7, t : B and
v : B, with S(B) ≤ A. Then, by the induction hypothesis, u : B.
We conclude by rules S<sub>I</sub><sup>+</sup> and ≤.

(α.t →<sub>(p)</sub> α.u) Let α.t : A. By Lemma 5.7, t : S(B), with S(B) ≤ A.
Then, by the induction hypothesis, t : S(B). We conclude by rules
S<sub>I</sub><sup>α</sup> and ≤.

(π_j t →<sub>(p)</sub> π_j u) Let π_j t : A. By Lemma 5.7, t : S(ℝ^n), and ℝ^j × S(ℝ^{n-j}) ≤ A Then, by the induction hypothesis, u : S(ℝ^n). We conclude by rules S_E and ≤.

(t × v →<sub>(p)</sub> u × v) Let t × v : A. By Lemma 5.7, t : B and v : C,
with B × C ≤ A. Then, by the induction hypothesis, u : B. We
conclude by rules ×<sub>I</sub> and ≤.

$(v \times t \rightarrow_{(p)} v \times u)$ Analogous to previous case.

$(\Uparrow_r t \rightarrow_{(p)} \Uparrow_r u)$ Let $\vdash \Uparrow_r t : A$. By Lemma 5.7, $\vdash t : S(S(B) \times C)$, and $S(B \times C) \preceq A$. Then, by the induction hypothesis, $\vdash u : S(S(B) \times C)$, and so, by rule $\Uparrow_r$, $\vdash \Uparrow_r u : S(B \times C)$. We conclude by rule $\leq$.

$(\Uparrow_\ell t \rightarrow_{(p)} \Uparrow_\ell u)$ Let $\vdash \Uparrow_\ell t : A$. By Lemma 5.7, $\vdash t : S(S(B) \times C)$, and $S(B \times C) \preceq A$. Then, by the induction hypothesis, $\vdash u : S(S(B) \times C)$, and so, by rule $\Uparrow_\ell$, $\vdash \Uparrow_\ell u : S(B \times C)$. We conclude by rule $\leq$.
(head $t \to_{(p)} head u$) Let $\vdash head t : A$. By Lemma 5.7, $\vdash t : \mathbb{B}^n$, with $\mathbb{B} \preceq A$. Then, by the induction hypothesis, $\vdash u : \mathbb{B}^n$. We conclude by rules $\times_{Er}$ and $\preceq$.

(tail $t \to_{(p)} tail u$) Let $\vdash tail t : A$. By Lemma 5.7, $\vdash t : \mathbb{B}^n$, with $\mathbb{B}^{n-1} \preceq A$. Then, by the induction hypothesis, $\vdash u : \mathbb{B}^n$. We conclude by rules $\times_{Er}$ and $\preceq$. $\square$

## Appendix B. Detailed proofs of Section 6 (Strong normalisation)

**Lemma 6.2.** If $t \to_{(1)} r$ by any of the rules in the groups linear distribution, vector space axioms or lists, or their contextual closure, then $||r|| \ge ||t||$. Moreover, $||r|| = ||t||$ if and only if the rule is (zeroS).

**PROOF.** By induction and rule by rule analysis:

$$(\text{lin}_r^+): t(u + v) \to_{(1)} tu + tv.$$

$$
\begin{align*}
||t(u + v)|| &= (3||t|| + 2)(3||u + v|| + 2) \\
&= (3||t|| + 2)(3(2 + ||u|| + ||v||) + 2) \\
&= (3||t|| + 2)(8 + 3||u|| + 3||v||) \\
&= 4(3||t|| + 2) + (3||t|| + 2)(4 + 3||u|| + 3||v||) \\
&= 12||t|| + 8 + (3||t|| + 2)(4 + 3||u|| + 3||v||) \\
&= 12||t|| + 8 + (3||t|| + 2)((3||u|| + 2) + (3||v|| + 2)) \\
&= 12||t|| + 8 + (3||t|| + 2)(3||u|| + 2) + (3||t|| + 2)(3||v|| + 2) \\
&= 12||t|| + 8 + ||tu|| + ||tv|| \\
&= 12||t|| + 6 + ||tu + tv|| \\
&> ||tu + tv||
\end{align*}
$$

$$(\text{lin}_r^\alpha): t(\alpha.u) \to_{(1)} \alpha.tu$$

$$
\begin{align*}
||t(\alpha.u)|| &= (3||t|| + 2)(3||\alpha.u|| + 2) \\
&= (3||t|| + 2)(3(1 + 2||u||) + 2) \\
&= (3||t|| + 2)(6||u|| + 5) \\
&= 3||t|| + 2 + (3||t|| + 2)(6||u|| + 4) \\
&= 3||t|| + 2 + 2(3||t|| + 2)(3||u|| + 2) \\
&= 3||t|| + 2 + 2||tu|| \\
&= 3||t|| + 1 + ||\alpha.tu|| \\
&> ||\alpha.tu||
\end{align*}
$$

$$(\text{lin}_r^0): t\vec{0}_{S(\mathbb{B})} \to_{(1)} \vec{0}_{S(\min(A))}$$

$$||t\vec{0}_{S(\mathbb{B})}|| = (3||t|| + 2)(3||\vec{0}_{S(\mathbb{B})}|| + 2) > 0 = ||\vec{0}_{S(\min(A))}||$$
$$ (\mathrm{lin}_l^+): (t+u)v \to_{(1)} tv + uv $$

$$
\begin{align*}
\|(t+u)v\| &= (3\|t+u\| + 2)(3\|v\| + 2) \\
&= (3(2 + \|t\| + \|u\|) + 2)(3\|v\| + 2) \\
&= (3\|t\| + 3\|u\| + 8)(3\|v\| + 2) \\
&= (3\|t\| + 3\|u\| + 4)(3\|v\| + 2) + 4(3\|v\| + 2) \\
&= ((3\|t\| + 3\|u\| + 4)(3\|v\| + 2) + 2) + 12\|v\| + 6 \\
&= \|tv + uv\| + 12\|v\| + 6 \\
&> \|tv + uv\|
\end{align*}
$$

$$ (\mathrm{lin}_l^\alpha): (\alpha.t)u \to_{(1)} \alpha.tu $$

$$
\begin{align*}
\| (\alpha.t)u \| &= (3\|\alpha.t\| + 2)(3\|u\| + 2) \\
&= (3(1 + 2\|t\|) + 2)(3\|u\| + 2) \\
&= (6\|t\| + 5)(3\|u\| + 2) \\
&= (6\|t\| + 4)(3\|u\| + 2) + (3\|u\| + 2) \\
&= 2(3\|t\| + 2)(3\|u\| + 2) + 3\|u\| + 2 \\
&= \|\alpha.tu\| + 3\|u\| + 1 \\
&> \|\alpha.tu\|
\end{align*}
$$

$$ (\mathrm{lin}_l^0): \vec{0}_{S(\mathbb{B}\Rightarrow A)} t \to_{(1)} \vec{0}_{S(\min(A))} $$

$$ \|\vec{0}_{S(\mathbb{B}\Rightarrow A)} t\| = (3\|\vec{0}_{S(\mathbb{B}\Rightarrow A)}\| + 2)(3\|t\| + 2) = 6\|t\| + 4 > 0 = \|\vec{0}_{S(\min(A))}\| $$

$$ (\text{neutral}): \vec{0}_{S(A)} + t \to_{(1)} t $$

$$ \|\vec{0}_{S(A)} + t\| = 2 + \|\vec{0}_{S(A)}\| + \|t\| = 2 + \|t\| > \|t\| $$

$$ (\text{unit}): 1.t \to_{(1)} t $$

$$ \|1.t\| = 1 + 2\|t\| > \|t\| $$

$$ (\text{zero}_\alpha): 0.t \to_{(1)} \vec{0}_{S(\min(A))} $$

$$ \|0.t\| = 1 + 2\|t\| > 0 = \|\vec{0}_{S(\min(A))}\| $$

$$ (\text{zero}): \alpha.\vec{0}_{S(A)} \to_{(1)} \vec{0}_{S(\min(A))} $$

$$ \|\alpha.\vec{0}_{S(A)}\| = 1 + 2\|\vec{0}_{S(A)}\| = 1 > 0 = \|\vec{0}_{S(\min(A))}\| $$

$$ (\text{prod}): \alpha.(\beta.t) \to_{(1)} (\alpha \times \beta).t $$

$$
\begin{align*}
\|\alpha.(\beta.t)\| &= 1 + 2\|\beta.t\| \\
&= 1 + 2(1 + 2\|t\|) \\
&= 3 + 4\|t\| \\
&> 1 + 2\|t\| \\
&= \|(\alpha \times \beta).t\|
\end{align*}
$$
(αdist): α(t + u) → (1) (α.t + α.u)

$$
\begin{align*}
||\alpha.(t+u)|| &= 1 + 2||t+u|| \\
&= 5 + 2||t|| + 2||u|| \\
&= 3 + ||\alpha.t|| + ||\alpha.u|| \\
&= 1 + ||\alpha.t + \alpha.u|| \\
&> ||\alpha.t + \alpha.u||
\end{align*}
$$

(fact): α.t + β.t → (1) (α + β).t

$$
\begin{align*}
||\alpha.t + \beta.t|| &= 2 + ||\alpha.t|| + ||\beta.t|| \\
&= 4 + 4||t|| \\
&> 1 + 2||t|| \\
&= ||(\alpha + \beta).t||
\end{align*}
$$

(fact¹): α.t + t → (1) (α + 1).t

$$
\begin{align*}
||\alpha.t + t|| &= 2 + ||\alpha.t|| + ||t|| \\
&= 3 + 3||t|| \\
&> 1 + 2||t|| \\
&= ||(\alpha + 1).t||
\end{align*}
$$

(fact²): t + t → (1) 2.t

$$
||t + t|| = 2 + 2||t|| > 1 + 2||t|| = ||2.t||
$$

(zeroS): $\vec{0}_{S(A)} \to_{(1)} \vec{0}_{S(\min(A))}$

$$
||\vec{0}_{S(A)}|| = 0 = ||\vec{0}_{S(\min(A))}||
$$

(head): head t × r → (1) t

$$
||\text{head } t \times r|| = 1 + ||t \times r|| = 1 + ||t|| + ||r|| > ||t||
$$

(tail): tail t × r → (1) r

$$
||\text{tail } t \times r|| = 1 + ||t \times r|| = 1 + ||t|| + ||r|| > ||r||
$$

**Contextual rules:** If $t \to_{(1)} r$, then, by the induction hypothesis, $||t|| \ge ||r||$, and hence, $||C[t]|| \ge ||C[r]||$, where $C[\cdot]$ is a context with one hole. $\square$

**Lemma 6.3.** If for every $i \in \{1, \dots, n\}$ we have $r_i \in \mathbf{SN}$, then $\sum_{i=1}^n [\alpha.]r_i \in \mathbf{SN}$.
PROOF. Induction on the lexicographic order of $(\sum_{i=1}^n |r_i|, ||\sum_{i=1}^n [\alpha.]r_i||)$ to show that $\text{Red}(\sum_{i=1}^n [\alpha.]r_i) \subseteq \text{SN}$. Let $t \in \text{Red}(\sum_{i=1}^n [\alpha.]r_i)$. The possibilities are:

* $t = \sum_{i=1}^n [\alpha.]s_i$ where for all $i \neq k$, $s_i = r_i$ and $r_k \to_{(p)} s_k$. Since $\sum_{i=1}^n |s_i| < \sum_{i=1}^n |r_i|$, we conclude by the induction hypothesis.

* $t = \sum_{i=1}^n s_i$ where for all $i \neq k$, $s_i = [\alpha.]r_i$ and $\alpha_k \cdot r_k \to_{(1)} s_k$. Then, the reduction $\alpha_k \cdot r_k \to_{(1)} s_k$, is by one of the following rules: (unit), (zero$_\alpha$), (zero), (prod), or (alphaDist). In any of these cases $\sum_{i=1}^n |s_i| \le \sum_{i=1}^n |r_i|$ and, by Lemma 6.2, $||t|| < ||\sum_{i=1}^n [\alpha.]r_i||$. Hence, we conclude by the induction hypothesis.

* $t = \sum_{i \neq j} [\alpha.]r_i + ([\alpha_j] + [\alpha_k])r_j$, where $r_j = r_k$ (rule (fact), (fact¹), or (fact²)). In this case $(\sum_{i \neq j} |r_i|) + |r_j| \le \sum_i |r_i|$ and by Lemma 6.2, $||t|| < ||\sum_{i=1}^n [\alpha.]r_i||$. Hence, we conclude by the induction hypothesis. $\square$

**Lemma 6.4.** If $t \in \text{SN}$, then $\pi_j t \in \text{SN}$.

PROOF. We show by induction on $|t|$ that $\text{Red}(\pi_j t) \subseteq \text{SN}$. Let $r \in \text{Red}(\pi_j t)$. The possibilities are:

* $r = \pi_j t'$ where $t \to_{(p)} t'$. Since $|t'| < |t|$ and $t' \in \text{SN}$, we conclude by the induction hypothesis.

* $r = \prod_{h=1}^j b_{hk} \times \sum_{i \in P} \left( \frac{\alpha_i}{\sqrt{\sum_{r \in P} |\alpha_r|^2}} \right) \prod_{h=j+1}^m b_{hi}$, $t = \sum_{i=1}^n [\alpha.] \prod_{h=1}^m b_{hi}$. Any sequence starting on $r$ will only use vector space axioms rules, which, by Lemma 6.2 reduce the size of the term, except for (zero$_S$), which anyway can be used only a finite number of times. Therefore, $r \in \text{SN}$. $\square$

**Lemma 6.7.** For all $A$, the following properties hold:

(CR1) If $t \in (A)$, then $t \in \text{SN}$.

(CR2) If $t \in (A)$, then $\text{Red}(t) \subseteq (A)$.

(CR3) If $t \in \mathcal{N}$, $t$ has the same type as all the terms in $(A)$, and $\text{Red}(t) \subseteq (A)$ then $t \in (A)$.

(HAB) For all $x^A$, $x \in (A)$.

(LIN1) If $t \in (A)$ and $r \in (A)$, then $t+r \in (A)$.

(LIN2) If $t \in (A)$ then $\alpha.t \in (A)$.

(NULL) $\vec{0}_{S(A)} \in (A)$

PROOF. We proceed by induction over $A$.

* Let $A = \mathbb{B}$.
**CR1** Let $t \in (\mathbb{B})$. By definition, $(\mathbb{B}) \subseteq \mathbb{SN}$, so $t \in \mathbb{SN}$.

**CR2** Let $t \in (\mathbb{B})$. By definition, $(\mathbb{B}) \subseteq \mathbb{SN}$, so $t \in \mathbb{SN}$ and $\text{Red}(t) \subseteq \mathbb{SN}$. Furthermore, since $t \in (\mathbb{B})$, we have $t : S(\mathbb{B})$. Let $r \in \text{Red}(t)$, then $r : S(\mathbb{B})$. Therefore, by definition, $\text{Red}(t) \subseteq (\mathbb{B})$.

**CR3** Let $t \in \mathcal{N}$ and $t : S(\mathbb{B})$ where $\text{Red}(t) \subseteq (\mathbb{B})$. Since $\text{Red}(t) \subseteq (\mathbb{B}) \subseteq \mathbb{SN}$, we have $t \in \mathbb{SN}$. Therefore, by definition, $t : (\mathbb{B})$.

**HAB** Since $x^{\mathbb{B}} \in \mathbb{SN}$ and $x^{\mathbb{B}} : \mathbb{B} \preceq S(\mathbb{B})$, we have, by definition, $x^{\mathbb{B}} \in (\mathbb{B})$.

**LIN1** Since $t \in (\mathbb{B})$ and $r \in (\mathbb{B})$, we have, by definition of $(\mathbb{B})$, that $t : S(\mathbb{B})$, $r : S(\mathbb{B})$, $t \in \mathbb{SN}$ and $r \in \mathbb{SN}$. Then, $t+r : S(S(\mathbb{B})) \preceq S(\mathbb{B})$ and, by Lemma 6.3, $t+r \in \mathbb{SN}$. Therefore, by definition, $t+r \in (\mathbb{B})$.

**LIN2** Since $t \in (\mathbb{B})$, we have, by definition of $(\mathbb{B})$ that $t : S(\mathbb{B})$ and $t \in \mathbb{SN}$. Then, $\alpha.t : S(S(\mathbb{B})) \preceq S(\mathbb{B})$ and, by Lemma 6.3, $\alpha.t \in \mathbb{SN}$. Therefore, by definition, $\alpha.t \in (\mathbb{B})$.

**NULL** Since $\vec{0}_{S(\mathbb{B})} : S(\mathbb{B})$ and $\vec{0}_{S(\mathbb{B})} \in \mathbb{SN}$, we have by definition of $(\mathbb{B})$ that $\vec{0}_{S(\mathbb{B})} \in (\mathbb{B})$.

* Let $A = B \times C$

**CR1** Since $t \in (B \times C)$, we have by definition that $t \in \mathbb{SN}$.

**CR2** Since $t \in (B \times C)$, we have $t : S(S(B) \times S(C))$. Let $t' \in \text{Red}(t)$. Since $t' \in \text{Red}(t)$, we have that $t' : S(S(B) \times S(C))$. On the other hand, since $t \in (B \times C)$, we have that $t \in \mathbb{SN}$. Then, $t' \in \mathbb{SN}$. Therefore, by definition, $t' \in (B \times C)$, which means $\text{Red}(t) \subseteq (B \times C)$.

**CR3** Let $t \in \mathcal{N}$ and $t : S(S(B) \times S(C))$ where $\text{Red}(t) \subseteq (B \times C)$. Since $(B \times C) \subseteq \mathbb{SN}$, we have $t \in \mathbb{SN}$. Therefore, by definition, $t \in (B \times C)$.

**HAB** Since $x^{B \times C} : B \times C \preceq S(S(B) \times S(C))$ and $x^{B \times C} \in \mathbb{SN}$, we have by definition that $x^{B \times C} \in (B \times C)$.

**LIN1** Since $t \in (B \times C)$, we have that $t : S(S(B) \times S(C))$ and $t \in \mathbb{SN}$. Similarly, we have that $r : S(S(B) \times S(C))$ and $r \in \mathbb{SN}$. Then, $t+r : S(S(B) \times S(C))$ and, by Lemma 6.3, $t+r \in \mathbb{SN}$. Therefore, by definition, $t+r \in (B \times C)$.

**LIN2** Since $t \in (B \times C)$, we have that $t : S(S(B) \times S(C))$ and $t \in \mathbb{SN}$. Then, $\alpha.t : S(S(S(B) \times S(C))) \preceq S(S(B) \times S(C))$ and, by Lemma 6.3, $\alpha.t \in \mathbb{SN}$. Therefore, by definition, $\alpha.t \in (B \times C)$.

**NULL** Since $\vec{0}_{S(B \times C)} : S(B \times C) \preceq S(S(B) \times S(C))$ and $\vec{0}_{S(B \times C)} \in \mathbb{SN}$, we have by definition that $\vec{0}_{S(B \times C)} \in (B \times C)$.

* Let $A = \Psi \Rightarrow B$

**CR1** Given $t \in (\Psi \Rightarrow B)$, we want to show that $t \in \mathbb{SN}$. Let $r \in (\Psi)$ (note that by induction hypothesis (HAB), such $r$ exists). By definition, we have that $tr \in (\mathbb{B})$. And by induction hypothesis, we have that $tr \in \mathbb{SN}$, which means, $|tr|$ is finite. And since $|t| \le |tr|$, we have that $|t|$ is finite, and therefore, $t \in \mathbb{SN}$.
**CR2** Given $t \in (\Psi \Rightarrow B])$, we want to show that Red($t$) $\subseteq (\Psi \Rightarrow B)$, which means that given $t' \in \text{Red}(t)$, $t' \in (\Psi \Rightarrow B]$. By definition of $(\Psi \Rightarrow B]$, this is the same as showing that $t' : S(\Psi \Rightarrow B)$ and, for all $r \in (\Psi]$, $t'r \in (B]$. Since $t \in (\Psi \Rightarrow B]$, we have by definition that, for all $r \in (\Psi]$, $tr \in (B]$. And by induction hypothesis, this implies that, for all $r \in (\Psi]$, Red($tr$) $\subseteq (B]$. In particular, given $t' \in \text{Red}(t)$, we have that, for all $r \in (\Psi]$, $t'r \in \text{Red}(tr) \subseteq (B]$. And since $t \in (\Psi \Rightarrow B]$, we have by definition that $t : S(\Psi \Rightarrow B)$. Since $t' \in \text{Red}(t)$, we have that $t' : S(\Psi \Rightarrow B)$.

**CR3** Given $t \in \mathcal{N}$ and $t : S(\Psi \Rightarrow \mathbb{B})$ where Red($t$) $\subseteq (\Psi \Rightarrow B]$, we want to show that $t \in (\Psi \Rightarrow B]$. By definition, this is the same than showing that for all $r \in (\Psi]$, $tr \in (B]$. By induction hypothesis, it suffices to show that for all $r \in (\Psi]$, Red($tr$) $\in (B]$. Notice that if $r \in (\Psi]$, then $r : S(\Psi)$, and since $t : S(\Psi \Rightarrow B)$, we have $tr : S(B)$. Let $r \in (\Psi]$. By induction hypothesis (CR1), we have that $r \in \mathbb{SN}$, which means $|r|$ exists. Therefore, we can proceed by induction (2) over $(|r|, ||r||)$. We analyze the reducts of $tr$:

- $tr \to t'r$ where $t \to t'$ Since $t' \in \text{Red}(t)$, we have that $t' \in (\Psi \Rightarrow B]$. And since $r \in (\Psi]$, we have by definition that $t'r \in (B]$.

- $tr = (?u.v)r \to (?u.v)r'$ where $r \to r'$ Since $r \in (\Psi]$, we have by induction hypothesis (CR2) that $r' \in (\Psi]$. And since $|r'| < |r|$, we have by induction hypothesis (2) that $(?u.v)r' \in (B]$.

- $tr = t(r_1 + r_2) \to tr_1 + tr_2$ Since $|r_1| \le |r|$ and, by Lemma 6.2, $||r_1|| < ||r||$, we have by induction hypothesis (2) that $tr_1 \in (B]$. Similarly, we have that $tr_2 \in (B]$. Therefore, by Lemma 6.7 (LIN1), we have that $tr_1 + tr_2 \in (B]$.

- $tr = t(\alpha.r_1) \to \alpha.tr_1$ Since $|r_1| \le |r|$ and, by Lemma 6.2, $||r_1|| < ||r||$, we have by induction hypothesis (2) that $tr_1 \in (B]$. Therefore, by Lemma 6.7 (LIN2), we have that $\alpha.tr_1 \in (B]$.

- $tr = t\bar{0}_{S(\Psi)} \to \bar{0}_{S(\min(B))}$ By Lemma 6.7 (NULL), we have that $\bar{0}_{S(\min(B))} \in (\min(B))$. By Lemma 5.4, $\min(B) \le B$, and $\bar{0}_{S(\min(B))} \in \mathbb{SN}$, hence, by definition, $\bar{0}_{S(\min(B))} \in (B]$.

**HAB** By definition of $(\Psi \Rightarrow B]$, and since $x^{\Psi \Rightarrow B} : S(\Psi \Rightarrow B)$, it suffices to show that, for all $t \in (\Psi]$, we have that $x^{\Psi \Rightarrow B}t \in (B]$. Let $t \in (\Psi]$. Since $x^{\Psi \Rightarrow B}t \in \mathcal{N}$, it suffices to show that Red($x^{\Psi \Rightarrow B}t$) $\subseteq (B]$. Since $t \in (\Psi]$, we have by induction hypothesis (CR1) that $t \in \mathbb{SN}$. Therefore, we can proceed by induction (2) over $(|t|, ||t||)$. We analyze the possible reducts of $x^{\Psi \Rightarrow B}t$:

- $x^{\Psi \Rightarrow B}t = x^{\Psi \Rightarrow B}(t_1 + t_2) \to x^{\Psi \Rightarrow B}t_1 + x^{\Psi \Rightarrow B}t_2$ Since $|t_1| \le |t|$ and, by Lemma 6.2, $||t_1|| < ||t||$, we have by induction hypothesis (2) that $x^{\Psi \Rightarrow B}t_1 \in (B]$. Similarly, we have that $x^{\Psi \Rightarrow B}t_2 \in (B]$. Therefore, by induction hypothesis (LIN1), we have that $x^{\Psi \Rightarrow B}t_1 + x^{\Psi \Rightarrow B}t_2 \in (B]$.
- $x^{\Psi \Rightarrow B}t = x^{\Psi \Rightarrow B}(\alpha.t_1) \rightarrow \alpha.x^{\Psi \Rightarrow B}t_1$ Since $|t_1| \le |t|$ and, by Lemma 6.2, $||t_1|| < ||t||$, we have by induction hypothesis (2) that $x^{\Psi \Rightarrow B}t_1 \in (\mathcal{B})$. Therefore, by induction hypothesis (LIN2), we have that $\alpha.x^{\Psi \Rightarrow B}t_1 \in (\mathcal{B})$.

- $x^{\Psi \Rightarrow B}t = x^{\Psi \Rightarrow B}(\bar{\mathcal{O}}_{S(\Psi)}}) \rightarrow \bar{\mathcal{O}}_{S(\min(B))}$. By induction hypothesis (NULL), we have that $\bar{\mathcal{O}}_{S(\min(B))} \in (\min(B))$. By Lemma 5.4, $\min(B) \subseteq B$, and $\bar{\mathcal{O}}_{S(\min(B))} \in \mathbf{SN}$, hence, by definition, $\bar{\mathcal{O}}_{S(\min(B))} \in (\mathcal{B})$.

**LIN1** By definition of $(\Psi \Rightarrow B)$, it suffices to show that $t+r: S(\Psi \Rightarrow B)$ and, for all $s \in (\Psi)$, $(t+r)s \in (B)$. Since $t \in (\Psi \Rightarrow B)$ and $r \in (\Psi \Rightarrow B)$, we have that $t: S(\Psi \Rightarrow B)$, $r: S(\Psi \Rightarrow B)$ and, for all $s \in (\Psi)$, $ts \in (B)$ and $rs \in (B)$. Therefore, $t+r: S(S(\Psi \Rightarrow B)) \subseteq S(\Psi \Rightarrow B)$ and $(t+r)s: S(B)$. It remains to show that, for all $s \in (\Psi)$, $(t+r)s \in (B)$. Since $(t+r)s \in \mathcal{N}$ and, by type derivation, $(t+r)s: S(B)$, we have by induction hypothesis (CR3) that it is sufficient to show that, for all $s \in (\Psi)$, $\text{Red}((t+r)s) \subseteq (B)$. Since $ts \in (B)$, $rs \in (B)$, $y s \in (\Psi)$, we have by induction hypothesis (CR1) that $t \in \mathbf{SN}$, $r \in \mathbf{SN}$, $y s \in \mathbf{SN}$. Therefore, we can proceed by induction (2) over $(|t| + |r| + |s|, ||(t+r)s||)$. We analyze the possible reducts of $(t+r)s$:

- $(t+r)s \rightarrow (t'+r)s$ where $t \rightarrow t'$ Since $|t'| < |t|$, we have by induction hypothesis that $(t'+r)s \in (B)$.

- $(t+r)s \rightarrow (t+r')s$ where $r \rightarrow r'$ Analogous to the previous case.

- $(t+r)(s_1 + s_2) \rightarrow (t+r)s_1 + (t+r)s_2$ Since $|s_1| \le |s|$ and $||(t+r)s_1|| < ||(t+r)s||$, we have by induction hypothesis (2) that $(t+r)s_1 \in (B)$. Similarly, we have that $(t+r)s_2 \in (B)$. Therefore, by induction hypothesis, we have that $(t+r)s_1 + (t+r)s_2 \in (B)$.

- $(t+r)(\alpha.s_1) \rightarrow \alpha.(t+r)s_1$ Since $|s_1| \le |s|$ and $||(t+r)s_1|| < ||(t+r)s||$, we have by induction hypothesis (2) that $(t+r)s_1 \in (B)$. Therefore, by induction hypothesis (LIN2), we have that $\alpha.(t+r)s_1 \in (B)$.

- $(t+r)\bar{\mathcal{O}}_{S(\Psi)} \rightarrow \bar{\mathcal{O}}_{S(\min(B))}$ By induction hypothesis (NULL), we have that $\bar{\mathcal{O}}_{S(\min(B))} \in (\min(B))$. By Lemma 5.4, $\min(B) \subseteq B$, and $\bar{\mathcal{O}}_{S(\min(B))} \in \mathbf{SN}$, hence, by definition, $\bar{\mathcal{O}}_{S(\min(B))} \in (B)$.

- $(t+r)s \rightarrow ts + rs$ Since $ts \in (B)$ and $rs \in (B)$, we have by induction hypothesis that $ts + rs \in (B)$.

**LIN2** By definition of $(\Psi \Rightarrow B)$, it suffices to show that $\alpha.t: S(\Psi \Rightarrow B)$ and, for all $s \in (\Psi)$, $(\alpha.t)s \in (B)$. Since $t \in (\Psi \Rightarrow B)$, we have that $t: S(\Psi \Rightarrow B)$ and, for all $s \in (\Psi)$, $ts \in (B)$. Therefore, $\alpha.t: S(S(\Psi \Rightarrow B)) \subseteq S(\Psi \Rightarrow B)$ and $(\alpha.t)s: S(B)$. It remains to show that, for all $s \in (\Psi)$, $(\alpha.t)s \in (B)$. Since $(\alpha.t)s \in \mathcal{N}$, we have by induction hypothesis (CR3) that it is sufficient to show that, for all $s \in (\Psi)$, $\text{Red}((\alpha.t)s) \subseteq (B)$. Since $ts \in (B)$ and $s \in (\Psi)$,
we have by induction hypothesis (CR1) that $t \in \mathbf{SN}$ and $s \in \mathbf{SN}$. Therefore, we can proceed by induction (2) over $(|t| + |s|, ||(\alpha.t)s||)$. We analyze the possible reducts of $(\alpha.t)s$:

- $(\alpha.t)s \to (\alpha.t')s$ where $t \to t'$ Since $|t'| < |t|$, we have by induction hypothesis (2) that $(\alpha.t')s \in (\mathcal{B})$.

- $(\alpha.t)s = (\alpha.t)(s_1+s_2) \to (\alpha.t)s_1+(\alpha.t)s_2$ Since $|t|+|s_1| \le |t|+|s|$ and $||(\alpha.t)s_1|| < ||(\alpha.t)s||$, we have by induction hypothesis that $(\alpha.t)s_1 \in (\mathcal{B})$. Similarly, $(\alpha.t)s_2 \in (\mathcal{B})$. Therefore, by induction hypothesis (LIN1), $(\alpha.t)s_1 + (\alpha.t)s_2 \in (\mathcal{B})$.

- $(\alpha.t)s = (\alpha.t)(\beta.s_1) \to \beta.(\alpha.t)s_1$ Since $|t| + |s_1| \le |t| + |s|$ and $||(\alpha.t)s_1|| < ||(\alpha.t)s||$, we have by induction hypothesis (2) that $(\alpha.t)s_1 \in (\mathcal{B})$. Therefore, by induction hypothesis, $\beta.(\alpha.t)s_1 \in (\mathcal{B})$.

- $(\alpha.t)s = (\alpha.t)\vec{0}_{S(\Psi)} \to \vec{0}_{S(\min(B))}$ By induction hypothesis (NULL), we have that $\vec{0}_{S(\min(B))} \in (\min(B))$. By Lemma 5.4, $\min(B) \preceq B$, and $\vec{0}_{S(\min(B))} \in \mathbf{SN}$, hence, by definition, $\vec{0}_{S(\min(B))} \in (\mathcal{B})$.

- $(\alpha.t)s \to \alpha.ts$ Since $ts \in (\mathcal{B})$, we have by induction hypothesis that $\alpha.ts \in (\mathcal{B})$.

**NULL** We want to show that $\vec{0}_{S(\Psi \Rightarrow B)} \in (\Psi \Rightarrow B)$. By definition of $(\Psi \Rightarrow B)$, this is equivalent to showing that, for all $t \in (\Psi)$, $\vec{0}_{S(\Psi \Rightarrow B)}t \in (\mathcal{B})$. Since $\vec{0}_{S(\Psi \Rightarrow B)}t \in \mathcal{N}$ and $\vec{0}_{S(\Psi \Rightarrow B)}t : S(B)$, we have by induction hypothesis (CR3) that this is equivalent to showing that $\text{Red}(\vec{0}_{S(\Psi \Rightarrow B)}t) \subseteq (\mathcal{B})$. Since the only possible reduct of $\vec{0}_{S(\Psi \Rightarrow B)}t$ is $\vec{0}_{S(\min(B))}$, it suffices to show that $\vec{0}_{S(\min(B))} \in (\mathcal{B})$. By induction hypothesis, we have that $\vec{0}_{S(\min(B))} \in (\min(B))$. By Lemma 5.4, $\min(B) \preceq B$, and $\vec{0}_{S(\min(B))} \in \mathbf{SN}$, hence, by definition, $\vec{0}_{S(\min(B))} \in (\mathcal{B})$.

* Let $A = S(B)$

**CR1** Since $t \in (S(B))$, we have by definition that $t \in \mathbf{SN}$.

**CR2** Given $t \in (S(B))$, we want to show that $\text{Red}(t) \subseteq (S(B))$. By definition, $t \in \mathbf{SN}$, and so, $\text{Red}(t) \subseteq \mathbf{SN}$. Therefore, $\text{Red}(t) \subseteq (S(B))$.

**CR3** Given $t \in \mathcal{N}$ where $t : S(B)$ and $\text{Red}(t) \subseteq (S(B))$, we want to show that $t \in (S(B))$. By definition, $\text{Red}(t) \subseteq (S(B)) \subseteq \mathbf{SN}$, and so, $t \in \mathbf{SN}$. Therefore, by definition, $t \in (S(B))$.

**HAB** Since $x^{S(B)} : S(B)$ and $x^{S(B)} \in \mathbf{SN}$, we have by definition that $x^{S(B)} \in (S(B))$.

**LIN1** Since $t \in (S(B))$ and $r \in (S(B))$, we have by definition of $(S(B))$ that $t : S(B)$, $r : S(B)$, $t \in \mathbf{SN}$ and $r \in \mathbf{SN}$. Therefore, $t+r : S(S(B)) \preceq S(B)$ and, by Lemma 6.3, $t+r \in \mathbf{SN}$. Therefore, by definition, $t+r \in (S(B))$.
**LIN2** Since $t \in (\|S(B)\|)$, we have by definition of $\|(S(B))\|$ that $t : S(B)$ and $t \in \math{SN}$. Then, $\alpha.t : S(S(B)) \preceq S(B)$ and $\alpha.t \in \math{SN}$. Therefore, by definition, $\alpha.t \in \|(S(B))\|$.

**NULL** We want to show $\vec{\math{O}}_{S(S(B))} \in \|(S(B))\|$. Since $\vec{\math{O}}_{S(S(B))} : S(S(B)) \preceq S(B)$ and $\vec{\math{O}}_{S(S(B))} \in \math{SN}$, we have by definition that $\vec{\math{O}}_{S(S(B))} \in \|(S(B))\|$. $\square$

**Lemma 6.8.** If $A \preceq B$ then $(A] \subseteq (B]$).

**PROOF.** We proceed by induction on the relation $\preceq$.

* $A \preceq A$. Trivial by the reflexivity of set inclusion.

* $\frac{A \preceq B \quad B \preceq C}{A \preceq C}$. Trivial by the transitivity of set inclusion.

* $A \preceq S(A)$. Let $t \in (A]$. By definition, $t : S(A) \preceq S(S(A))$. And by Lemma 6.7 (CR1), $t \in \math{SN}$. Therefore, by definition, $t \in \|(S(A))\|$.

* $\overline{S(S(A))} \preceq \overline{S(A)}$. Let $t \in \|(S(S(A))\|)$. By definition, $t : S(S(A)) \preceq S(A)$ and $t \in \math{SN}$. Therefore, by definition, $t \in \|(S(A))\|$.

* $\frac{A \preceq B}{\Psi \Rightarrow A \preceq \Psi \Rightarrow B}$. Let $t \in (\Psi \Rightarrow A]$. By definition, $t : S(\Psi \Rightarrow A)$ and, for all $r \in (\Psi]$, $tr \in (A] \subseteq (B]$. And since $A \preceq B$, $t : S(\Psi \Rightarrow A) \preceq S(\Psi \Rightarrow B)$. Therefore, by definition, $t \in (\Psi \Rightarrow B]$.

* $\frac{A \preceq B}{S(A) \preceq S(B)}$. Let $t \in \|(S(A))\|$. By definition, $t : S(A)$ and $t \in \math{SN}$. And since $A \preceq B$, we have $t : S(A) \preceq S(B)$. Therefore, by definition, $t \in \|(S(B))\|$.

* $\frac{A \preceq B}{A \times C \preceq B \times C}$. Let $t \in (A \times C]$. By definition, $t \in \math{SN}$ and $t : S(S(A)) \times S(S(C))$. And since $A \preceq B$, we have that $S(A) \preceq S(B)$, and so, $t : S(S(B)) \times S(C)$. Therefore, by definition, $t \in (B \times C]$.

* $\frac{A \preceq B}{A \times C \preceq B \times C}$. Analogous to the previous case. $\square$

**Lemma 6.9 (Adequacy).** If $\Gamma \vdash t : A$ and $\theta \models \Gamma$ then $\theta(t) \in (A]$.

**PROOF.** By induction in the derivation of $\Gamma \vdash t : A$. We proceed by cases.

* $\overline{x^\Psi \vdash x : \Psi}$. Since $\theta \models x^\Psi$, we have $\theta(x) \in (\Psi]$.

* $\overline{\vdash \vec{\math{O}}_{S(A)} : S(A)}$ $Ax_{\vec{\math{O}}}$. By Lemma 6.7 (NULL) and Lemma 6.8, $\theta(\vec{\math{O}}_{S(A)}) = \vec{\math{O}}_{S(A)} \in \|(S(A))\|$.
• $\vdash_{|0\rangle} : \mathbb{B} \quad Ax_{|0\rangle}$. By definition, $\theta(|0\rangle) = |0\rangle \in \mathbb{SN}$. And since $|0\rangle : S(\mathbb{B})$, we have by definition that $|0\rangle \in (\mathbb{B})$.

• $\vdash_{|1\rangle} : \mathbb{B} \quad Ax_{|1\rangle}$. Analogous to the previous case.

• $\Gamma \vdash t : A \quad S_I^\alpha$. By the induction hypothesis, $\theta(t) \in (\mathbb{A})$, and by Lemma 6.7 (LIN2), $\alpha.\theta(t) = \theta(\alpha.t) \in (\mathbb{A})$. Finally, by Lemma 6.8, $\theta(\alpha.t) \in (S(A))$.

• $\Gamma \vdash t : A \quad \Delta \vdash u : A \quad S_I^+$. By the induction hypothesis, $\theta_1(t) \in (\mathbb{A})$ and $\theta_2(u) \in (\mathbb{A})$, with $\theta_1 \models \Gamma$ and $\theta_2 \models \Delta$. Then, since $\Gamma$ and $\Delta$ are disjoint, $\theta_1 \cup \theta_2(t+u) = \theta_1(t) + \theta_2(u)$. And by Lemma 6.7 (LIN1), $\theta_1(t) + \theta_2(u) \in (\mathbb{A})$. Therefore, by Lemma 6.8, $\theta_1(t) + \theta_2(u) \in (S(A))$.

• $\frac{\Gamma \vdash t : S(\mathbb{B}^n)}{\Gamma \vdash \pi_j t : \mathbb{B}^j \times S(\mathbb{B}^{n-j})} \quad S_E$. We want to show that if $\theta \models \Gamma$, then $\theta(\pi_j t) = \pi_j \theta(t) \in (\mathbb{B}^j \times S(\mathbb{B}^{n-j}))$. By definition, it suffices to show that $\pi_j \theta(t) : S(S(\mathbb{B}^j) \times S(\mathbb{B}^{n-j}))$ and $\pi_j \theta(t) \in \mathbb{SN}$. By induction hypothesis, $\theta(t) \in (S(\mathbb{B}^n))$, which implies that $\theta(t) : S(S(\mathbb{B}^n)) \preceq S(\mathbb{B}^n)$. Therefore, $\pi_j \theta(t) : \mathbb{B}^j \times S(\mathbb{B}^{n-j}) \preceq S(S(\mathbb{B}^j) \times S(\mathbb{B}^{n-j}))$. On the other hand, since $\theta(t) \in (S(\mathbb{B}^n)) \subseteq \mathbb{SN}$, we have by Lemma 6.4 that $\pi_j \theta(t) \in \mathbb{SN}$. Therefore, $\pi_j \theta(t) \in (\mathbb{B}^j \times S(\mathbb{B}^{n-j}))$.

• $\frac{\Gamma \vdash t : A \quad A \preceq B}{\Gamma \vdash t : B} \preceq$. By the induction hypothesis $\theta(t) \in (\mathbb{A})$, and by Lemma 6.8, $(\mathbb{A}) \subseteq (\mathbb{B})$.

• $\frac{\Gamma \vdash t : A \quad \Gamma \vdash r : A}{\Gamma \vdash ?t.r : \mathbb{B} \Rightarrow A}$. If we want to show that if $\theta \models \Gamma$, then $\theta(?t.r) = ?\theta(t) \cdot \theta(r) \in (\mathbb{B} \Rightarrow A)$. By definition, this is equivalent to showing that $?\theta(t) \cdot \theta(r) : S(\mathbb{B} \Rightarrow A)$ and, for all $s \in (\mathbb{B})$, $s?\theta(t) \cdot \theta(r) \in (\mathbb{A})$. By induction hypothesis, we have that $\theta(t) \in (\mathbb{A})$ and $\theta(r) \in (\mathbb{A})$, which implies that $\theta(t) : S(A)$ and $\theta(r) : S(A)$. Therefore, $?\theta(t) \cdot \theta(r) : \mathbb{B} \Rightarrow S(A) \preceq S(\mathbb{B} \Rightarrow A)$ and $s?\theta(t) \cdot \theta(r) : S(A)$. And since $s?\theta(t) \cdot \theta(r) \in \mathcal{N}$ (because such a term is actually an application), we have by Lemma 6.7 (CR3) that it suffices to show that $\mathrm{Red}(s?\theta(t) \cdot \theta(r)) \subseteq (\mathbb{A})$.

We proceed by induction (2) over $(|s|, ||s?\theta(t) \cdot \theta(r)||)$. We analyze each of the reducts of $s?\theta(t) \cdot \theta(r)$:

- $s?\theta(t) \cdot \theta(r) \to u?\theta(t) \cdot \theta(r)$ where $s \to u$
  Since $|u| < |s|$, we have by induction hypothesis (2) that $u?\theta(t) \cdot \theta(r) \in (\mathbb{A})$.

- $s?\theta(t) \cdot \theta(r) \to \theta(t)$ where $s = |1\rangle$
  By induction hypothesis, $\theta(t) \in (\mathbb{A})$.
- $s?\theta(t) \cdot \theta(r) \to \theta(r)$ where $s = |0\rangle$
By induction hypothesis, $\theta(r) \in (\mathcal{A})$.

- $s?\theta(t) \cdot \theta(r) = (s_1 + s_2)?\theta(t) \cdot \theta(r) \to s_1?\theta(t) \cdot \theta(r) + s_2?\theta(t) \cdot \theta(r)$
Since $|s_1| \le |s|$ and $||s_1?\theta(t) \cdot \theta(r)|| < ||s?\theta(t) \cdot \theta(r)||$, we have by induction hypothesis (2) that $s_1?\theta(t) \cdot \theta(r) \in (\mathcal{A})$. Similarly, $s_2?\theta(t) \cdot \theta(r) \in (\mathcal{A})$. Therefore, by Lemma 6.7 (LIN1), $s_1?\theta(t) \cdot \theta(r) + s_2?\theta(t) \cdot \theta(r) \in (\mathcal{A})$.

- $s?\theta(t) \cdot \theta(r) = (\alpha.s_1)?\theta(t) \cdot \theta(r) \to \alpha.s_1?\theta(t) \cdot \theta(r)$
Since $|s_1| \le |s|$ and $||s_1?\theta(t) \cdot \theta(r)|| < ||s?\theta(t) \cdot \theta(r)||$, we have by induction hypothesis (2) that $s_1?\theta(t) \cdot \theta(r) \in (\mathcal{A})$. Therefore, by Lemma 6.7 (LIN2), $\alpha.s_1?\theta(t) \cdot \theta(r) \in (\mathcal{A})$.

- $s?\theta(t) \cdot \theta(r) = \vec{0}_{S(\mathbb{B})}?\theta(t) \cdot \theta(r) \to \vec{0}_{S(A)}$
By Lemma 6.7 (NULL), $\vec{0}_{S(A)} \in (\mathcal{A})$.

• $\Gamma, x : \Psi \vdash t : A \Rightarrow_I$. We want to show that if $\theta' \models \Gamma$, then $\theta'(\lambda x^\Psi.t) = (\lambda x^\Psi.\theta'(t)) \in (\Psi \Rightarrow A)$, which is equivalent to showing that $(\lambda x^\Psi.\theta'(t)) : S(\Psi \Rightarrow A)$ and, for all $r \in (\Psi)$, $(\lambda x^\Psi.\theta'(t))r \in (\mathcal{A})$.

By induction hypothesis, $\theta(t) \in (\mathcal{A})$, which implies that $\theta(t) : S(A)$. Therefore, $(\lambda x^\Psi.\theta'(t)) : \Psi \Rightarrow S(A) \subseteq S(\Psi \Rightarrow A)$ and $(\lambda x^\Psi.\theta'(t))r : S(A)$. And since $(\lambda x^\Psi.\theta'(t))r \in \mathcal{N}$, Lemma 6.7 (CR3) tells us that if $\text{Red}((\lambda x^\Psi.\theta'(t))r) \subseteq (\mathcal{A})$, then $(\lambda x^\Psi.\theta'(t))r \in (\mathcal{A})$. We are going to show that in fact $\text{Red}((\lambda x^\Psi.\theta'(t))r) \subseteq (\mathcal{A})$.

Since $r \in (\Psi)$, we have by Lemma 6.7 (CR2) that $r \in \mathcal{SN}$. Therefore, we can proceed by induction (2) over $|r|, ||(\lambda x^\Psi.\theta'(t))r||$. We analyze each of the reducts of $(\lambda x^\Psi.\theta'(t))r$:

- $(\lambda x^\Psi.\theta'(t))r \to \theta'(t)[r/x]$
We want to show that $\theta'(t)[r/x] \in (\mathcal{A})$. By definition, $\theta'(t)[r/x] = \theta(t)$, and by induction hypothesis, $\theta(t) \in (\mathcal{A})$. Therefore, $\theta'(t)[r/x] \in (\mathcal{A})$.

- $(\lambda x^\Psi.\theta'(t))r \to (\lambda x^\Psi.\theta'(t))r'$ where $r \to r'$
By induction hypothesis (2), $(\lambda x^\Psi.\theta'(t))r' \in (\mathcal{A})$.

- $(\lambda x^\Psi.\theta'(t))r = (\lambda x^\Psi.\theta'(t))(r_1 + r_2) \to (\lambda x^\Psi.\theta'(t))r_1 + (\lambda x^\Psi.\theta'(t))r_2$
Since $|r_1| \le |r|$ and $||(\lambda x^\Psi.\theta'(t))r_1|| < ||(\lambda x^\Psi.\theta'(t))r||$, we have by induction hypothesis (2) that $(\lambda x^\Psi.\theta'(t))r_1 \in (\mathcal{A})$. Similarly, we have that $(\lambda x^\Psi.\theta'(t))r_2 \in (\mathcal{A})$. Therefore, by Lemma 6.7 (LIN1), we have that $(\lambda x^\Psi.\theta'(t))r_1 + (\lambda x^\Psi.\theta'(t))r_2 \in (\mathcal{A})$.

- $(\lambda x^\Psi.\theta'(t))r = (\lambda x^\Psi.\theta'(t))(\alpha.r_1) \to \alpha.(\lambda x^\Psi.\theta'(t))r_1$
Since $|r_1| \le |r|$ and $||(\lambda x^\Psi.\theta'(t))r_1|| < ||(\lambda x^\Psi.\theta'(t))r||$, we have by induction hypothesis (2) that $(\lambda x^\Psi.\theta'(t))r_1 \in (\mathcal{A})$. Therefore, by Lemma 6.7 (LIN2), we have that $\alpha.(\lambda x^\Psi.\theta'(t))r_1 \in (\mathcal{A})$.

- $(\lambda x^\Psi.\theta'(t))r = (\lambda x^\Psi.\theta'(t))\vec{0}_{S(\mathbb{B}^n)} \to \vec{0}_{S(A)}$
By Lemma 6.7 (NULL), we have that $\vec{0}_{S(A)} \in (\mathcal{A})$.
• $\frac{\Gamma \vdash t : \Psi \Rightarrow A \quad \Delta \vdash u : \Psi}{\Gamma, \Delta \vdash tu : A} \Rightarrow_E$ We must show that if $\theta \models \Gamma, \Delta$, then $\theta(tu) \in (\mathcal{A})$. Since $\Gamma$ and $\Delta$ are disjoint, we have that $\theta(tu) = (\theta_1 \cup \theta_2)(tu) = \theta_1(t)\theta_2(u)$, where $\theta_1 \models \Gamma$ and $\theta_2 \models \Delta$. Therefore, it suffices to show that $\theta_1(t)\theta_2(u) \in (\mathcal{A})$. By induction hypothesis and definition of $(\Psi \Rightarrow A)$, we have that $\theta_1(t)\theta_2(u) \in (\mathcal{A})$.

• $\frac{\Gamma \vdash t : S(\Psi \Rightarrow A) \quad \Delta \vdash u : S(\Psi)}{\Gamma, \Delta \vdash tu : S(A)} \Rightarrow_{ES}$. We want to show that if $\theta \models \Gamma, \Delta$, then $\theta(tu) \in (S(A))$. Since $\Gamma$ and $\Delta$ are disjoint, we have that $\theta(tu) = (\theta_1 \cup \theta_2)(tu) = \theta_1(t)\theta_2(u)$, where $\theta_1 \models \Gamma$ and $\theta_2 \models \Delta$. Therefore, it suffices to show that $\theta_1(t)\theta_2(u) \in (S(A))$. Since $\theta_1(t) \in (S(\Psi \Rightarrow A))$ and $\theta_2(u) \in (S(\Psi))$, we have by definition that $\theta_1(t) : S(\Psi \Rightarrow A)$ and $\theta_2(u) : S(\Psi)$. Therefore, $\theta_1(t)\theta_2(u) : S(A)$. On the other hand, we need to show that $\theta_1(t)\theta_2(u) \in \mathbf{SN}$. To do that, it is sufficient to show that $\mathrm{Red}(\theta_1(t)\theta_2(u)) \subseteq \mathbf{SN}$. Since $\theta_1(t) \in (S(\Psi \Rightarrow A)) \subseteq \mathbf{SN}$ and $\theta_2(u) \in (S(\Psi)) \subseteq \mathbf{SN}$, we can proceed by induction (2) over $|(\theta_1(t)| + |\theta_2(u)|, ||\theta_1(t)\theta_2(u)||)$. We analyze the possible reducts of $\theta_1(t)\theta_2(u)$:

- $\theta_1(t)\theta_2(u) \to t'\theta_2(u)$ where $\theta_1(t) \to t'$
Since $|t'| < |\theta(t)|$, we have by induction hypothesis (2) that $t'\theta_2(u) \in \mathbf{SN}$.

- $\theta_1(t)\theta_2(u) \to \theta_1(t)u'$ where $\theta_2(u) \to u'$
Analogous to the previous case.

- $\theta_1(t)\theta_2(u) = (\lambda x^{\mathbb{B}^n} . t_1)\theta_2(u) \to t_1[\theta_2(u)/x]$ 
Since $\theta_1(t) = (\lambda x^{\mathbb{B}^n} . t_1) : S(\Psi \Rightarrow A)$, we have by Lemma 5.7 that $t_1 : A$ with a smaller derivation tree. Then, by induction hypothesis (Adequacy), we have that $t_1 \in (\mathcal{A})$, and therefore, by Lemma 6.7 (CR1), we have that $t_1 \in \mathbf{SN}$.

- $\theta_1(t)\theta_2(u) = (\lambda x^{S(\Psi)} . t_1)\theta_2(u) \to t_1[\theta_2(u)/x]$ 
Analogous to the previous case.

- $\theta_1(t)\theta_2(u) = |1\rangle?t_1 \cdot t_2 \to t_1$
Since $\theta_1(t) = (?t_1 \cdot t_2) : S(\Psi \Rightarrow A)$, we have by Lemma 5.7 that $t_1 : A$ with a smaller derivation tree. Then, by induction hypothesis (Adequacy), we have that $t_1 \in (\mathcal{A})$, and therefore, by Lemma 6.7 (CR1), we have that $t_1 \in \mathbf{SN}$.

- $\theta_1(t)\theta_2(u) = |0\rangle?t_1 \cdot t_2 \to t_2$
Analogous to the previous case.

- $\theta_1(t)\theta_2(u) = \theta_1(t)(u_1 + u_2) \to \theta_1(t)u_1 + \theta_1(t)u_2$
Since $|u_1| \le |\theta_2(u)|$ and, by Lemma 6.2, $||\theta_1(t)u_1|| < ||\theta_1(t)\theta_2(u)||$, we have by induction hypothesis (2) that $\theta_1(t)u_1 \in \mathbf{SN}$. Similarly, we have that $\theta_1(t)u_2 \in \mathbf{SN}$. Therefore, by Lemma 6.3, we have that $\theta_1(t)u_1 + \theta_1(t)u_2 \in \mathbf{SN}$.
- $\theta_1(t)\theta_2(u) = (t_1 + t_2)\theta_2(u) \to t_1\theta_2(u) + t_2\theta_2(u)$
Analogous to the previous case.

- $\theta_1(t)\theta_2(u) = \theta_1(t)(\alpha.u_1) \to \alpha.\theta_1(t)u_1$
Since $|u_1| \le |\theta_2(u)|$ and, by Lemma 6.2, $||\theta_1tu_1|| < ||\theta_1t\theta_2(u)||$, we have by induction hypothesis (2) that $\theta_1(t)u_1 \in \mathbf{SN}$. Therefore, by Lemma 6.3, we have that $\alpha.\theta_1(t)u_1 \in \mathbf{SN}$.

- $\theta_1(t)\theta_2(u) = (\alpha.t_1)\theta_2(u) \to \alpha.t_1\theta_2(u)$
Analogous to the previous case.

- $\theta_1(t)\theta_2(u) = \theta_1(t)\vec{0}_{S(\mathbb{B}^n)} \to \vec{0}_{S(A)}$
By definition, $\vec{0}_{S(A)} \in (\mathcal{S}(A)) \subseteq \mathbf{SN}$.

- $\theta_1(t)\theta_2(u) = \vec{0}_{S(\mathbb{B}^n \to A)}\theta_2(u) \to \vec{0}_{S(A)}$
Analogous to the previous case.

- $\Gamma \vdash t : A \qquad W$. By definition of $\theta$, we have that if $\theta \models \Gamma, x^{\mathbb{B}^n}$, then
$\theta \models \Gamma$. And by induction hypothesis, $\theta(t) \in (\mathcal{A})$.

- $\Gamma, x : \mathbb{B}^n, y : \mathbb{B}^n \vdash t : A \qquad C$. By definition, $\theta'(t[x/y]) = \theta(t)$. And by induction hypothesis, $\theta(t) \in (\mathcal{A})$. Therefore, $\theta'(t[x/y]) \in (\mathcal{A})$.

- $\Gamma \vdash t : A \qquad \Delta \vdash u : B \qquad \times_I$. Since $\Gamma$ and $\Delta$ are disjoint, $\theta(t \times u) = (\theta_1 \cup \theta_2)(t \times u) = \theta_1(t) \times \theta_2(u)$, where $\theta_1 \models \Gamma$ and $\theta_2 \models \Delta$. Therefore, it suffices to show that $\theta_1(t) \times \theta_2(u) \in (\mathcal{A} \times B)$.
Since $\theta_1(t) \in (\mathcal{A})$, we have by definition that $\theta_1(t) : S(A)$ and, by Lemma 6.7 (CR1), $\theta_1(t) \in \mathbf{SN}$. Similarly, $\theta_2(u) : S(B)$ and $\theta_2(u) \in \mathbf{SN}$.
Then, $\theta_1(t) \times \theta_2(u) : S(A) \times S(B) \subseteq S(S(A) \times S(B))$ and $\theta_1(t) \times \theta_2(u) \in \mathbf{SN}$.
Therefore, by definition of $(\mathcal{A} \times B)$, $\theta_1(t) \times \theta_2(u) \in (\mathcal{A} \times B)$.

- $\Gamma \vdash t : \mathbb{B}^n \qquad \times_{Er}$. Since $\mathit{head} t : \mathbb{B}$, we have by Lemma 5.11 that $\theta(\mathit{head} t) = \mathit{head} \theta(t) : \mathbb{B} \subseteq S(\mathbb{B})$. And by induction hypothesis, $\theta(t) \in (\mathbb{B}^n) \subseteq \mathbf{SN}$. Then, $\mathit{head} \theta(t) \in \mathbf{SN}$. Therefore, by definition, $\mathit{head} \theta(t) \in (\mathbb{B})$.

- $\Gamma \vdash tail t : \mathbb{B}^{n-1} \qquad \times_{El}$. Since tail $t : \mathbb{B}^n$, we have by Lemma 5.11 that $\theta(tail t) = tail \theta(t) : \mathbb{B}^n = \mathbb{B} \times \mathbb{B}^{n-1} \subseteq S(S(\mathbb{B}) \times S(\mathbb{B}^{n-1}))$. Furthermore, by induction hypothesis, $\theta(t) \in (\mathbb{B}^n)$, and by Lemma 6.7 (CR1), $\theta(t) \in \mathbf{SN}$. Then, tail $\theta(t) \in \mathbf{SN}$.
Therefore, by definition, tail $\theta(t) \in (\mathbb{B})$.

- $\Gamma \vdash t : S(S(A) \times B) \qquad \Uparrow_r$. Por definicin de $(S(S(A) \times B))$, tenemos que $\theta(t) : S(S(A) \times B)$ y $\theta(t) \in \mathbf{SN}$.
Entonces, $\Uparrow_r \theta(t) : S(A \times B)$ y $\Uparrow_r \theta(t) \in \mathbf{SN}$. Por lo tanto, $\Uparrow_r \theta(t) \in (S(A \times B))$, que es lo que queramos mostrar.
• $\frac{\Gamma \vdash t : S(A \times S(B))}{\Gamma \vdash \Uparrow_t t : S(A \times B)} \Uparrow_t$. Analogous to the previous case. $\square$

**Appendix C. Detailed proofs of Section 7 (Interpretation)**

**Lemma 7.1.** If $A \preceq B$, then $[[A]] \subseteq [[B]]$.

**PROOF.** We proceed by induction on the relation $\preceq$.

• $[[A]] \subseteq [[A]]$ by the reflexivity of set inclusion.

• Let $A \preceq B$ and $B \preceq C$. By the induction hypothesis, $[[A]] \subseteq [[B]]$ and $[[B]] \subseteq [[C]]$. Then $[[A]] \subseteq [[C]]$ by the transitivity of set inclusion.

• $[[A]] \subseteq S[[A]] = [[S(A)]]$.

• $[[S(S(A))]] = S(S[[A]]) = S[[A]] = [[S(A)]]$.

• Let $A \preceq B$ and $[[A]] \subseteq [[B]]$. Then,

$$ \begin{align*} - [[\Psi \Rightarrow A]] &= [[\Psi]] \Rightarrow [[A]] \\ &= \{f \mid \forall a \in [[\Psi]], fa \in [[A]]\} \\ &\subseteq \{f \mid \forall a \in [[\Psi]], fa \in [[B]]\} \\ &= [[\Psi]] \Rightarrow [[B]] \\ &= [[\Psi \Rightarrow B]] \end{align*} $$

$$ \begin{align*} - [[A \times C]] &= [[A]] \times [[C]] \\ &= \{a \times c \mid a \in [[A]], c \in [[C]]\} \\ &\subseteq \{b \times c \mid b \in [[B]], c \in [[C]]\} \\ &= [[B]] \times [[C]] \\ &= [[B \times C]] \end{align*} $$

• $[[C \times A]] \subseteq [[C \times B]]$ by an analogous reasoning to the previous one.

$$ - [[S(A)]] = S[[A]] \subseteq S[[B]] = [[S(B)]] \quad \square $$

**Lemma 7.2.** If $\Gamma \vdash t : A$ and $\phi, x \mapsto S, y \mapsto S$ is a $\Gamma$-valuation, then $[[t]]_{\phi, x \mapsto S, y \mapsto S} = [[(x/y)t]]_{\phi, x \mapsto S}$.

**PROOF.** We proceed by induction on $t$.

**Independent cases.** The cases where $t$ does not includes $x$ nor $y$ and the denotation does not depends on the valuation, are trivial. Those cases are: $|0\rangle$, $|1\rangle$, $\tilde{0}_{S(A)}$ and $?\cdot$.

Let $t = x$. Then, $[[x]]_{\phi, x \mapsto S, y \mapsto S} = S = [[x]]_{\phi, x \mapsto S}$.

Let $t = y$. Then, $[[y]]_{\phi, x \mapsto S, y \mapsto S} = S = [[x]]_{\phi, x \mapsto S}$.

Let $t = z$. Then, $[[z]]_{\phi, x \mapsto S, y \mapsto S} = \phi z = [[z]]_{\phi, x \mapsto S}$.
Let $t = \lambda z^\Psi . r$. Then,

$$
\begin{align*}
\llbracket \lambda z^\Psi . r \rrbracket_{\phi, x \mapsto S, y \mapsto S} &= \{ f \mid \forall a \in \llbracket \Psi \rrbracket, fa \in \llbracket r \rrbracket_{\phi, x \mapsto S, y \mapsto S, z \mapsto \Psi} \} \\
\text{(by IH)} &= \{ f \mid \forall a \in \llbracket \Psi \rrbracket, fa \in \llbracket (x/y)r \rrbracket_{\phi, x \mapsto S, z \mapsto \Psi} \} \\
&= \llbracket \lambda z^\Psi . (x/y)r \rrbracket_{\phi, x \mapsto S} \\
&= \llbracket (x/y)\lambda z^\Psi . r \rrbracket_{\phi, x \mapsto S}
\end{align*}
$$

Let $t = r \times s$. Then,

$$
\begin{align*}
\llbracket r \times s \rrbracket_{\phi, x \mapsto S, y \mapsto S} &= \llbracket r \rrbracket_{\phi, x \mapsto S, y \mapsto S} \times \llbracket s \rrbracket_{\phi, x \mapsto S, y \mapsto S} \\
\text{(by IH)} &= \llbracket (x/y)r \rrbracket_{\phi, x \mapsto S} \times \llbracket (x/y)s \rrbracket_{\phi, x \mapsto S} \\
&= \llbracket (x/y)r \times (x/y)s \rrbracket_{\phi, x \mapsto S} \\
&= \llbracket (x/y)(r \times s) \rrbracket_{\phi, x \mapsto S}
\end{align*}
$$

Let $t = (r + s)$. Then,

$$
\begin{align*}
\llbracket (r+s) \rrbracket_{\phi, x \mapsto S, y \mapsto S} &= \{a+b \mid a \in \llbracket r \rrbracket_{\phi, x \mapsto S, y \mapsto S}, b \in \llbracket s \rrbracket_{\phi, x \mapsto S, y \mapsto S}\} \\
\text{(by IH)} &= \{a+b \mid a \in \llbracket (x/y)r \rrbracket_{\phi, x \mapsto S}, b \in \llbracket (x/y)s \rrbracket_{\phi, x \mapsto S}\} \\
&= \llbracket ((x/y)r + (x/y)s) \rrbracket_{\phi, x \mapsto S} \\
&= \llbracket (x/y)(r+s) \rrbracket_{\phi, x \mapsto S}
\end{align*}
$$

Let $t = \alpha.r.$ Then,

$$
\begin{align*}
\llbracket \alpha.r \rrbracket_{\phi, x \mapsto S, y \mapsto S} &= \{ \alpha.a \mid a \in \llbracket r \rrbracket_{\phi, x \mapsto S, y \mapsto S} \} \\
\text{(by IH)} &= \{ \alpha.a \mid a \in \llbracket (x/y)r \rrbracket_{\phi, x \mapsto S} \} \\
&= \llbracket \alpha.(x/y)r \rrbracket_{\phi, x \mapsto S} \\
&= \llbracket (x/y)\alpha.r \rrbracket_{\phi, x \mapsto S}
\end{align*}
$$

Let $t = rs$. Then,

$$
\begin{align*}
& \llbracket rs \rrbracket_{\phi, x \mapsto S, y \mapsto S} \\
&= \begin{cases}
\{ \sum_{i \in I} \alpha_i g_i(a) \mid \sum_{i \in I} \alpha_i g_i \in \llbracket r \rrbracket_{\phi, x \mapsto S, y \mapsto S}, a \in \llbracket s \rrbracket_{\phi, x \mapsto S, y \mapsto S} \} & \text{If } A = \Psi \Rightarrow B \\
\{ \sum_{i \in I} \sum_{j \in J} \alpha_i \beta_j g_i(c_j) \mid \sum_{i \in I} \alpha_i g_i \in \llbracket r \rrbracket_{\phi, x \mapsto S, y \mapsto S}, \sum_{j \in J} \beta_j c_j \in \llbracket s \rrbracket_{\phi, x \mapsto S, y \mapsto S} \} & \text{If } A = S(\Psi \Rightarrow B) \\
\end{cases} \\
\text{(by IH)} \\
&= \begin{cases}
\{ \sum_{i \in I} \alpha_i g_i(a) \mid \sum_{i \in I} \alpha_i g_i \in \llbracket (x/y)r \rrbracket_{\phi, x \mapsto S}, a \in \llbracket (x/y)s \rrbracket_{\phi, x \mapsto S} \} & \text{If } A = \Psi \Rightarrow B \\
\{ \sum_{i \in I} \sum_{j \in J} \alpha_i \beta_j g_i(c_j) \mid \sum_{i \in I} \alpha_i g_i \in \llbracket (x/y)r \rrbracket_{\phi, x \mapsto S}, \sum_{j \in J} \beta_j c_j \in \llbracket (x/y)s \rrbracket_{\phi, x \mapsto S} \} & \text{If } A = S(\Psi \Rightarrow B) \\
\end{cases} \\
&= \llbracket (x/y)r(x/y)s \rrbracket_{\phi, x \mapsto S} \\
&= \llbracket (x/y)(rs) \rrbracket_{\phi, x \mapsto S}
\end{align*}
$$
Let $t = \pi_j r$. Then,

$$[[\pi_j r]]_{\phi, x \mapsto S, y \mapsto S} = \{ \prod_{h=1}^{j} b_{hk} \times \sum_{i \in P} \left( \frac{\alpha_i}{\sqrt{\sum_{r \in P} |\alpha_r|^2}} \right)^{\prod_{h=j+1}^{m} b_{hi}} \mid \forall i \in P, \forall h, b_{hi} = b_{hk} \}$$

with $[[r]]_{\phi, x \mapsto S, y \mapsto S} = \{\sum_{i=1}^{n} [\alpha_i] \prod_{h=1}^{m} b_{hi}\}$ where $b_{hi} = \binom{1}{0}$ or $\binom{1}{0}$.

By the induction hypothesis, $[[x/y)r]]_{\phi, x \mapsto S} = [[r]]_{\phi, x \mapsto S, y \mapsto S}$, hence,

$$[[x/y)(\pi_j r)]_{\phi, x \mapsto S} = [[\pi_j((x/y)r)]_{\phi, x \mapsto S} = [[\pi_j r]]_{\phi, x \mapsto S, y \mapsto S}$$

Let $t = \text{head } r$. Then,

$$[[\text{head } r]]_{\phi, x \mapsto S, y \mapsto S} = \{a_1 \mid \prod_{i=1}^{n} a_i \in [[t]]_{\phi, x \mapsto S, y \mapsto S}, a_1 \in [[\mathbb{B}]]\}$$

$$\begin{align*}
(\text{by IH}) &= \{a_1 \mid \prod_{i=1}^{n} a_i \in [[(x/y)t]]_{\phi, x \mapsto S}, a_1 \in [[\mathbb{B}]]\} \\
&= [[\text{head } (x/y)r]]_{\phi, x \mapsto S} \\
&= [[(x/y)(\text{head } r)]]_{\phi, x \mapsto S}
\end{align*}$$

Let $t = \text{tail } r$. Then,

$$[[\text{tail } r]]_{\phi, x \mapsto S, y \mapsto S} = \{ \prod_{i=2}^{n} a_i \mid \prod_{i=1}^{n} a_i \in [[t]]_{\phi, x \mapsto S, y \mapsto S}, a_1 \in [[\mathbb{B}]] \}$$

$$\begin{align*}
(\text{by IH}) &= \{ \prod_{i=2}^{n} a_i \mid \prod_{i=1}^{n} a_i \in [[(x/y)t]]_{\phi, x \mapsto S}, a_1 \in [[\mathbb{B}]] \} \\
&= [[\text{tail } (x/y)r]]_{\phi, x \mapsto S} \\
&= [[(x/y)(\text{tail } r)]]_{\phi, x \mapsto S}
\end{align*}$$

Let $t = \Uparrow r$ Then,

$$\begin{align*}
[[\Uparrow r]]_{\phi, x \mapsto S, y \mapsto S} &= [[r]]_{\phi, x \mapsto S, y \mapsto S} \\
(\text{by IH}) &= [[(x/y)r]]_{\phi, x \mapsto S} \\
&= [[\Uparrow (x/y)r]]_{\phi, x \mapsto S} \\
&= [[(x/y) \Uparrow r]]_{\phi, x \mapsto S}
\end{align*}$$

□

**Theorem 7.3.** If $\Gamma \vdash t : A$, and $\phi$ is a $\Gamma$-valuation. Then $[[t]]_{\phi} \subseteq [[A]}$.

PROOF. We proceed by induction on the typing derivation.

* $x : \Psi \vdash x : \Psi$ Axiom. Then, $[[x]]_{\phi} = \phi x = [[\Psi]]$.
• $\overline{\vdash_{\vec{0}_{S(A)}} : S(A)}$ $Ax_0$. Then, $[\vec{0}_{S(A)}]_\phi = \{\vec{0}\} \subset S[A] = [S(A)]$.

• $\overline{\vdash_{|0\rangle} : \mathbb{B}}$ $Ax_{|0\rangle}$. Then, $[[0\rangle]_\phi = \{(\begin{smallmatrix} 1 \\ 0 \end{smallmatrix})\} \subset \{(\begin{smallmatrix} 1 \\ 0 \end{smallmatrix}), (\begin{smallmatrix} 0 \\ 1 \end{smallmatrix})\} = [\mathbb{B}]$.

• $\overline{\vdash_{|1\rangle} : \mathbb{B}}$ $Ax_{|1\rangle}$. Then, $[[1\rangle]_\phi = \{(\begin{smallmatrix} 0 \\ 1 \end{smallmatrix})\} \subset \{(\begin{smallmatrix} 1 \\ 0 \end{smallmatrix}), (\begin{smallmatrix} 0 \\ 1 \end{smallmatrix})\} = [\mathbb{B}]$.

• $\frac{\Gamma \vdash t : A \quad A \preceq B}{\Gamma \vdash t : B} \preceq$.

Then, by the induction hypothesis, $[[t]]_\phi \subseteq [A]$ and by Lemma 7.1, $[[A]] \subseteq [[B]$, hence, $[[t]]_\phi \subseteq [[B]]$.

• $\frac{\Gamma \vdash t : A}{\Gamma \vdash \alpha.t : S(A)} S_I^\alpha$.

Then, by the induction hypothesis, $[[t]]_\phi \subseteq [A]$. Hence, $[[\alpha.t]]_\phi = \{\alpha.a \mid a \in [[t]]_\phi\} \subseteq \{\alpha.a \mid a \in [[A]]\} \subseteq S[A] = [S(A)]$.

• $\frac{\Gamma \vdash t : A \quad \Gamma \vdash r : A}{\Gamma \vdash ?t.r : \mathbb{B} \Rightarrow A}$ If.

Then, since by the induction hypothesis, $[[t]]_\phi \in [A]$ and $[[r]]_\phi \in [A]$, we have

$$ \begin{gathered} [[?t.r]]_\phi = \{f \mid \forall a \in [\mathbb{B}], fa = \begin{cases} [t]_\phi & \text{If } a = (\begin{smallmatrix} 0 \\ 1 \end{smallmatrix}) \\ [r]_\phi & \text{If } a = (\begin{smallmatrix} 1 \\ 0 \end{smallmatrix}) \end{cases} \} \\ \subset [\mathbb{B}] \Rightarrow [A] = [\mathbb{B} \Rightarrow A]. \end{gathered} $$

• $\frac{\Gamma, x : \Psi \vdash t : A}{\Gamma \vdash \lambda x^\Psi.t : \Psi \Rightarrow A} \Rightarrow_I$.

Then, by the induction hypothesis, $[[t]]_{\phi,x \mapsto [\Psi]} \subseteq [A]$. Hence,

$$ \begin{align*} [[\lambda x^\Psi.t]]_\phi &= \{f \mid \forall a \in [\Psi], fa \in [[t]]_{\phi,x \mapsto [\Psi]}\} \\ &\subseteq \{f \mid \forall a \in [\Psi], fa \in [A]\} \\ &= [\Psi] \Rightarrow [A] = [\Psi \Rightarrow A]. \end{align*} $$

• $\frac{\Gamma \vdash t : \Psi \Rightarrow A \quad \Delta \vdash u : \Psi}{\Gamma, \Delta \vdash tu : A} \Rightarrow_E$.

Then, by the induction hypothesis $[[t]]_{\phi_\Gamma} \subseteq [\Psi] \Rightarrow [A]$ and $[[u]]_{\phi_\Delta} \subseteq [\Psi]$, where $\phi = \phi_\Gamma, \phi_\Delta$. Then,

$$ \begin{align*} [[tu]]_\phi &= \{\sum_{i \in I} \alpha_i.g_i(a) \mid \sum_{i \in I} \alpha_i.g_i \in [t]_\phi \text{ and } a \in [u]_\phi\} \\ &\subseteq \{\sum_{i \in I} \alpha_i.g_i(a) \mid \sum_{i \in I} \alpha_i.g_i \in [\Psi] \Rightarrow [A] \text{ and } a \in [\Psi]\}. \end{align*} $$

Since $[[\Psi]] \Rightarrow [A]$ is a set of functions (and not a linear combination of them), $I$ is a singleton and so this set is equal to $\{fa \mid f \in [\Psi] \Rightarrow [A] \text{ and } a \in [\Psi]\} \subseteq [A]$.
$$ \bullet \frac{\Gamma \vdash t : S(\Psi \Rightarrow A) \quad \Delta \vdash u : S(\Psi)}{\Gamma, \Delta \vdash tu : S(A)} \Rightarrow_{ES}. $$

Then, by the induction hypothesis $[[t]]_{\phi_{\Gamma}} \subseteq S([\Psi] \Rightarrow [[A]])$ and $[[u]]_{\phi_{\Delta}} \subseteq S([\Psi])$. Then,

$$ \begin{align*} [[tu]]_{\phi} &= \{ \sum_{i \in I} \sum_{j \in J} \alpha_i \cdot \beta_j g_i(c_j) \mid \sum_{i \in I} \alpha_i \cdot g_i \in [[t]]_{\phi} \text{ and } \sum_{j \in J} \beta_j \cdot c_j \in [[u]]_{\phi} \} \\ &\subseteq \{ \sum_{i \in I} \sum_{j \in J} \alpha_i \cdot \beta_j \cdot g_i(c_j) \mid \sum_{i \in I} \alpha_i \cdot g_i \in S([\Psi] \Rightarrow [[A]]) \text{ and } \sum_{j \in J} \beta_j \cdot c_j \in S([\Psi]) \} \\ &= \{ \sum_{i \in I} \sum_{j \in J} \alpha_i \cdot \beta_j \cdot g_i(c_j) \mid g_i \in [\Psi] \Rightarrow [[A]] \text{ and } c_j \in [\Psi] \} \\ &\subseteq S([A]) = [S(A)] \end{align*} $$

$$ \bullet \frac{\Gamma \vdash t : A \quad \Delta \vdash u : A}{\Gamma, \Delta \vdash (t+u) : S(A)} S_I^+. $$

Then, by the induction hypothesis $[[t]]_{\phi_{\Gamma}} \subseteq [[A]]$ and $[[u]]_{\phi_{\Delta}} \subseteq [[A]]$, with $\phi = \phi_{\Gamma}, \phi_{\Delta}$. Then, $\llbracket (t+u) \rrbracket_{\phi} = \{a+b \mid a \in [[t]]_{\phi} \text{ and } b \in [[u]]_{\phi}\} \subseteq \{a+b \mid a,b \in [[A]]\} \subseteq S([A]) = [S(A)]$.

$$ \bullet \frac{\Gamma \vdash t : S(\mathbb{B}^n)}{\Gamma \vdash \pi_j t : \mathbb{B}^j \times S(\mathbb{B}^{n-j})} S_E. $$

Then, by the induction hypothesis, $[[t]]_{\phi} \subseteq [S(\mathbb{B}^n)] = \mathbb{C}^{2^n}$. By definition,

$$ [[\pi_j t]]_{\phi} = \{ \prod_{h=1}^{j} b_{hk} \times \sum_{i \in P} \left( \frac{\alpha_i}{\sqrt{\sum_{r \in P} |\alpha_r|^2}} \right) \prod_{h=j+1}^{n} b_{hi} \mid \forall i \in P, \forall h, b_{hi} = b_{hk} \} $$

where $[[t]]_{\phi} = \{\sum_{i=1}^{n} [\alpha_i] \prod_{h=1}^{n} b_{hi}\}$, with $b_{hi} \in [\mathbb{B}]$, and $\forall i \in P, \forall h, b_{hi} = b_{hk}$. Then, $[[\pi_j t]]_{\phi} \subseteq [\mathbb{B}]^n \times [\mathbb{B}^{n-j}] = [\mathbb{B}^n \times \mathbb{B}^{n-j}]$.

$$ \bullet \frac{\Gamma \vdash t : A}{\Gamma, x : \mathbb{B}^n \vdash t : A} W. $$

Then, by the induction hypothesis, $[[t]]_{\phi} \subseteq [[A]]$, where $\phi$ is a $\Gamma$-valuation. Notice that any $\phi'$ that is a $(\Gamma, x : \mathbb{B}^n)$-valuation is also a $\Gamma$-valuation. Then, $[[t]]_{\phi'} \subseteq [[A]]$.

$$ \bullet \frac{\Gamma, x : \mathbb{B}^n, y : \mathbb{B}^n \vdash t : A}{\Gamma, x : \mathbb{B}^n \vdash (x/y)t : A} C. $$

Then, by the induction hypothesis, $[[t]]_{\phi} \subseteq [[A]]$, where $\phi$ is a $(\Gamma, x : \mathbb{B}^n, y : \mathbb{B}^n)$-valuation. Let $\phi'$ be a $(\Gamma, x : \mathbb{B}^n)$-valuation, then, by Lemma 7.2, $\llbracket (x/y)t \rrbracket_{\phi'} \subseteq [[A]]$.

$$ \bullet \frac{\Gamma \vdash t : A \quad \Delta \vdash u : B}{\Gamma, \Delta \vdash t \times u : A \times B} \times_I. $$

Then, by the induction hypothesis, $[[t]]_{\phi_{\Gamma}} \subseteq [[A]]$ and $[[u]]_{\phi_{\Delta}} \subseteq [[B]]$. Then, $[[t, u]]_{\phi_{\Gamma}, \phi_{\Delta}} = [[t]]_{\phi_{\Gamma}, \phi_{\Delta}} \times [[u]]_{\phi_{\Gamma}, \phi_{\Delta}} = [[t]]_{\phi_{\Gamma}} \times [[u]]_{\phi_{\Delta}} \subseteq [[A]] \times [[B]] = [[A \times B]]$.
• $\frac{\Gamma \vdash t : \mathbb{B}^n}{\Gamma \vdash \text{head } t : \mathbb{B}} \times_{Er.}$

Then, by the induction hypothesis, $[[t]]_\phi \subseteq [[\mathbb{B}^n]] = [[\mathbb{B}]] \times [[\mathbb{B}^{n-1}]] = \{a \times b \mid a \in [[\mathbb{B}]], b \in [[\mathbb{B}^{n-1}]]\}$. So, $[[\text{head } t]]_\phi = \{a \mid a \times b \in [[t]]_\phi, a \in [[\mathbb{B}]]\} = \{a \mid a \times b \in \{a' \times b' \mid a' \in [[\mathbb{B}]], b' \in [[\mathbb{B}^{n-1}]]\}\} = \{a \mid a \in [[\mathbb{B}]]\} = [[\mathbb{B}]]$.

• $\frac{\Gamma \vdash t : \mathbb{B}^n}{\Gamma \vdash \text{tail } t : \mathbb{B}^{n-1}} \times_{El.}$

Then, by the induction hypothesis, $[[t]]_\phi \subseteq [[\mathbb{B}^n]] = [[\mathbb{B}]] \times [[\mathbb{B}^{n-1}]] = \{a \times b \mid a \in [[\mathbb{B}]], b \in [[\mathbb{B}^{n-1}]]\}$. So, $[[\text{tail } t]]_\phi = \{\prod_{i=2}^n a_i \mid \prod_{i=1}^n a_i \in [[t]]_\phi, a_1 \in [[\mathbb{B}]]\} = \{\prod_{i=2}^n a_i \mid \prod_{i=1}^n a_i \in \{a' \times b' \mid a' \in [[\mathbb{B}]], b' \in [[\mathbb{B}^{n-1}]]\}\} = \{b \mid b \in [[\mathbb{B}^{n-1}]]\} = [[\mathbb{B}^{n-1}]]$.

• $\frac{\Gamma \vdash t : S(S(A) \times B)}{\Gamma \vdash \hat{\uparrow}_r t : S(A \times B)} \hat{\uparrow}_r$

Then, by the induction hypothesis, $[[\hat{\uparrow}_r t]]_\phi = [[t]]_\phi \subseteq [[S(S(A) \times B)]] = S(S[[A]] \times [[B]]) = S([A] \times [[B]]) = [[S(A \times B)]]$.

• $\frac{\Gamma \vdash t : S(A \times S(B))}{\Gamma \vdash \hat{\uparrow}_\ell t : S(A \times B)} \hat{\uparrow}_\ell$. This case is analogous to the previous one. $\square$

## Appendix D. Trace and typing of the Deutsch algorithm

We may use $|q_1\rangle \cdots |q_n\rangle$ as a shorthand notation for $|q_1\rangle \times \cdots \times |q_n\rangle$. The full trace of Deutsch$_{id}$ is given below.

$$
\begin{align*}
\text{Deutsch}_{id} \\
&= \pi_1 (\hat{\uparrow}_r H_1 (U_f \hat{\uparrow}_\ell \hat{\uparrow}_r (H_{both} |01\rangle))) \\
&\xrightarrow{\text{($\beta_k$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \hat{\uparrow}_r ((H(\text{head } |01\rangle)) \times (H(\text{tail } |01\rangle))))) \\
&\xrightarrow{\text{($\text{head}$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \hat{\uparrow}_r ((H|0\rangle) \times (H(\text{tail } |01\rangle))))) \\
&\xrightarrow{\text{($\text{tail}$)}} \pi_1 \hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \hat{\uparrow}_r ((H|0\rangle) \times (H|1\rangle))) \\
&\xrightarrow{\text{($\beta_k^2$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \hat{\uparrow}_r (\frac{1}{\sqrt{2}}(|0\rangle + (|0\rangle?(-|1\rangle)\cdot|1\rangle)) \times \frac{1}{\sqrt{2}}(|0\rangle + (|1\rangle?(-|1\rangle)\cdot|1\rangle))))) \\
&\xrightarrow{\text{($i_0$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \hat{\uparrow}_r (\frac{1}{\sqrt{2}}(|0\rangle + |1\rangle) \times \frac{1}{\sqrt{2}}(|0\rangle + (|1\rangle?(-|1\rangle)\cdot|1\rangle))))) \\
&\xrightarrow{\text{($i_1$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \hat{\uparrow}_r (\frac{1}{\sqrt{2}}(|0\rangle + |1\rangle) \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle))))) \\
&\xrightarrow{\text{($\text{dist}^\alpha$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \frac{1}{\sqrt{2}} \hat{\uparrow}_r ((|0\rangle + |1\rangle) \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle))))) \\
&\xrightarrow{\text{($\text{dist}^+_1$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \frac{1}{\sqrt{2}} (\hat{\uparrow}_r |0\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle) + \hat{\uparrow}_r |1\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle))))) \\
&\xrightarrow{\text{($\text{neut}^\uparrow$)}} \pi_1 (\hat{\uparrow}_r H_1 (U_{id} \hat{\uparrow}_\ell \frac{1}{\sqrt{2}} (|0\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle) + |1\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle)))))
\end{align*}
$$
$$
\xrightarrow{\text{(dist}^{\alpha})} \pi_1 (\hat{\pi}_r H_1 (U_{id} \frac{1}{\sqrt{2}} \cdot \hat{\pi}_\ell (|0\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle) + |1\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle))))
$$

$$
\xrightarrow{\text{(dist}^{+})} \pi_1 (\hat{\pi}_r H_1 (U_{id} \frac{1}{\sqrt{2}} \cdot (\hat{\pi}_\ell (|0\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle)) + \hat{\pi}_\ell (|1\rangle \times \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle))))
$$

$$
\xrightarrow{\text{(dist}^{\alpha})^2} \pi_1 (\hat{\pi}_r H_1 (U_{id} \frac{1}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot \hat{\pi}_\ell (|0\rangle \times (|0\rangle - |1\rangle)) + \frac{1}{\sqrt{2}} \cdot \hat{\pi}_\ell (|1\rangle \times (|0\rangle - |1\rangle))))
$$

$$
\xrightarrow{(\alpha \text{dist})} \pi_1 (\hat{\pi}_r H_1 (U_{id} (\frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} \cdot \hat{\pi}_\ell (|0\rangle \times (|0\rangle - |1\rangle)) + \frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} \cdot \hat{\pi}_\ell (|1\rangle \times (|0\rangle - |1\rangle))))
$$

$$
\xrightarrow{(\text{prod})} \pi_1 (\hat{\pi}_r H_1 (U_{id} (\frac{1}{2} \cdot \hat{\pi}_\ell (|0\rangle \times (|0\rangle - |1\rangle)) + \frac{1}{2} \cdot \hat{\pi}_\ell (|1\rangle \times (|0\rangle - |1\rangle))))
$$

$$
\xrightarrow{(\text{dist}^{+})^2} \pi_1 (\hat{\pi}_r H_1 (U_{id} (\frac{1}{2} \cdot (\hat{\pi}_\ell |00\rangle + \hat{\pi}_\ell |0\rangle \times (-|1\rangle)) + \frac{1}{2} \cdot (\hat{\pi}_\ell |10\rangle + \hat{\pi}_\ell |1\rangle \times (-|1\rangle))))
$$

$$
\xrightarrow{(\text{dist}^{\alpha})^2} \pi_1 (\hat{\pi}_r H_1 (U_{id} (\frac{1}{2} \cdot (\hat{\pi}_\ell |00\rangle - \hat{\pi}_\ell |01\rangle) + \frac{1}{2} \cdot (\hat{\pi}_\ell |10\rangle - \hat{\pi}_\ell |11\rangle)))
$$

$$
\xrightarrow{(\text{neut}^{\hat{\pi}})} \pi_1 (\hat{\pi}_r H_1 (U_{id} (\frac{1}{2} \cdot (|00\rangle - |01\rangle) + \frac{1}{2} \cdot (|10\rangle - |11\rangle))))
$$

$$
\xrightarrow{(\text{lin}^{+})} \pi_1 (\hat{\pi}_r H_1 (U_{id} \frac{1}{2} \cdot (|00\rangle - |01\rangle) + U_{id} \frac{1}{2} \cdot (|10\rangle - |11\rangle)))
$$

$$
\xrightarrow{(\text{lin}^{\alpha})^2} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot U_{id}(|00\rangle - |01\rangle) + \frac{1}{2} \cdot U_{id}(|10\rangle - |11\rangle)))
$$

$$
\xrightarrow{(\text{lin}^{+})^2} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot (U_{id} |00\rangle + U_{id} (-|01\rangle)) + \frac{1}{2} \cdot (U_{id} |10\rangle + U_{id} (-|11\rangle))))
$$

$$
\xrightarrow{(\text{lin}^{\alpha})^2} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot (U_{id} |00\rangle - U_{id} |01\rangle) + \frac{1}{2} \cdot (U_{id} |10\rangle - U_{id} |11\rangle)))
$$

$$
\xrightarrow{\text{(dist)}} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot ((\text{head} |00\rangle) \times ((\text{tail} |00\rangle)?(\text{not}(\text{id}(\text{head} |00\rangle))) \cdot (\text{id}(\text{head} |00\rangle))) \\
\qquad - U_{id} |01\rangle) + \frac{1}{2} \cdot (U_{id} |10\rangle - U_{id} |11\rangle)))
$$

$$
\xrightarrow{(\text{head})^3} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot (|0\rangle \times ((\text{tail} |00\rangle)?(\text{not}(\text{id} |0\rangle))) \cdot (\text{id} |0\rangle)) \\
\qquad - U_{id} |01\rangle) + (\frac{1}{2} \cdot (U_{id} |10\rangle - U_{id} |11\rangle)))
$$

$$
\xrightarrow{(\text{tail})} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot (|0\rangle \times (|0\rangle?(\text{not}(\text{id} |0\rangle))) \cdot (\text{id} |0\rangle)) \\
\qquad - U_{id} |01\rangle) + (\frac{1}{2} \cdot (U_{id} |10\rangle - U_{id} |11\rangle)))
$$

$$
\xrightarrow{(\text{id}_0)} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot (|0\rangle \times (\text{id} |0\rangle) - U_{id} |01\rangle) + \frac{1}{2} \cdot (U_{id} |10\rangle - U_{id} |11\rangle)))
$$

$$
\xrightarrow{(\text{id}_1)} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot (|00\rangle - U_{id} |01\rangle) + \frac{1}{2} \cdot (U_{id} |10\rangle - U_{id} |11\rangle)))
$$

$$
\xrightarrow{*} \pi_1 (\hat{\pi}_r H_1 (\frac{1}{2} \cdot (|00\rangle - |01\rangle) + \frac{1}{2} \cdot (|11\rangle - |10\rangle)))
$$

$$
\xrightarrow{(\text{lin}^{+})} \pi_1 (\hat{\pi}_r (H_1 \frac{1}{2} \cdot (|00\rangle - |01\rangle) + H_1 \frac{1}{2} \cdot (|11\rangle - |10\rangle)))
$$
$$
\begin{align*}
\xrightarrow{\text{(lin}^\alpha\text{)}_1^2} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot \mathbf{H}_1(|00\rangle - |01\rangle) + \frac{1}{2} \cdot \mathbf{H}_1(|11\rangle - |10\rangle))) \\
\xrightarrow{\text{(lin}^+\text{)}_1^2} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot (\mathbf{H}_1|00\rangle + \mathbf{H}_1(-|01\rangle)) + \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle + \mathbf{H}_1(-|10\rangle))) \\
\xrightarrow{\text{(lin}^\alpha\text{)}_1^2} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot (\mathbf{H}_1|00\rangle - \mathbf{H}_1|01\rangle) + \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle))) \\
\xrightarrow{\text{(b}^\alpha\text{)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\mathbf{H}(\text{head}|00\rangle)) \times (\text{tail}|00\rangle) - \mathbf{H}_1|01\rangle) + \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle))) \\
\xrightarrow{\text{(head)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\mathbf{H}|0\rangle) \times (\text{tail}|00\rangle) - \mathbf{H}_1|01\rangle) + \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle))) \\
\xrightarrow{\text{(tail)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\mathbf{H}|0\rangle) \times |0\rangle - \mathbf{H}_1|01\rangle) + \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle))) \\
\xrightarrow{\text{(b}^\beta\text{)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\frac{1}{\sqrt{2}} \cdot (|0\rangle + |0\rangle)(-|1\rangle)|1\rangle)) \times |0\rangle - \mathbf{H}_1|01\rangle) + \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle))) \\
\xrightarrow{\text{(if}^\alpha\text{)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle)) \times |0\rangle - \mathbf{H}_1|01\rangle) + \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle))) \\
\xrightarrow{\text{(dist}^+\text{)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\frac{1}{\sqrt{2}} \cdot |0\rangle + \frac{1}{\sqrt{2}} \cdot |1\rangle) \times |0\rangle - \mathbf{H}_1|01\rangle) + \hat{\mu}_r \frac{1}{2} \cdot (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle)) \\
\xrightarrow{\text{(dist}^\alpha\text{)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\frac{1}{\sqrt{2}} \cdot |0\rangle + \frac{1}{\sqrt{2}} \cdot |1\rangle) \times |0\rangle) - \hat{\mu}_r \mathbf{H}_1|01\rangle) \\
& + \frac{1}{2} \cdot \hat{\mu}_r (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle)) \\
\xrightarrow{\text{(dist}^+\text{)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\hat{\mu}_r (\frac{1}{\sqrt{2}} \cdot |0\rangle) \times |0\rangle + \hat{\mu}_r (\frac{1}{\sqrt{2}} \cdot |1\rangle) \times |0\rangle) - \hat{\mu}_r \mathbf{H}_1|01\rangle) \\
& + \frac{1}{2} \cdot \hat{\mu}_r (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle)) \\
\xrightarrow{\text{(neut}^\alpha\text{)}_1} \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot ((\frac{1}{\sqrt{2}} \cdot |00\rangle + \frac{1}{\sqrt{2}} \cdot |10\rangle) - \hat{\mu}_r \mathbf{H}_1|01\rangle) + \frac{1}{2} \cdot \hat{\mu}_r (\mathbf{H}_1|11\rangle - \mathbf{H}_1|10\rangle)) \\
\xrightarrow{*}_1 \pi_1 & (\hat{\mu}_r (\frac{1}{2} \cdot (((\frac{1}{\sqrt{2}} \cdot |00\rangle + \frac{1}{\sqrt{2}} \cdot |10\rangle) + (-\frac{1}{\sqrt{2}} \cdot |01\rangle - \frac{1}{\sqrt{2}} \cdot |11\rangle)) \\
& + ((\frac{1}{\sqrt{2}} \cdot |01\rangle - \frac{1}{\sqrt{2}} \cdot |11\rangle) + (-\frac{1}{\sqrt{2}} \cdot |00\rangle + \frac{1}{\sqrt{2}} \cdot |10\rangle))))
\end{align*}
$$
$$ \frac{\overline{\vdash |0\rangle : \mathbb{B}} \quad Ax_{|0\rangle} \quad \overline{\vdash |1\rangle : \mathbb{B}} \quad Ax_{|1\rangle} \quad \text{If} \quad \overline{x : \mathbb{B} \vdash x : \mathbb{B}}}{\overline{\vdash ?|0\rangle \cdot |1\rangle : \mathbb{B} \Rightarrow \mathbb{B}}} \quad Ax \quad \Rightarrow_E \quad \frac{x : \mathbb{B} \vdash x?|0\rangle \cdot |1\rangle : \mathbb{B}}{\vdash \text{not} : \mathbb{B} \Rightarrow \mathbb{B}} \quad \Rightarrow_I \quad (D.3) $$

$$ \frac{\overline{(D.3) \quad \vdash \text{not} : \mathbb{B} \Rightarrow \mathbb{B}} \quad \overline{y : \mathbb{B}^2 \vdash y : \mathbb{B}^2} \quad Ax \quad \Rightarrow_E \quad \overline{y : \mathbb{B}^2 \vdash f (\text{head } y) : \mathbb{B}} \quad Ax \quad \Rightarrow_E \quad \overline{y : \mathbb{B}^2 \vdash f (\text{head } y) : \mathbb{B}} \quad Ax}}{\overline{y : \mathbb{B}^2 \vdash \text{not } (f (\text{head } y)) : \mathbb{B}} \quad \overline{y : \mathbb{B}^2 \vdash f (\text{head } y) : \mathbb{B}} \quad \text{If} \quad \overline{x : \mathbb{B}^2 \vdash x : \mathbb{B}^2} \quad Ax \quad \Rightarrow_E \quad x : \mathbb{B}^2 \vdash \text{tail } x : \mathbb{B}^2 \quad Ax} \quad \Rightarrow_E \quad \frac{\overline{x : \mathbb{B}^2, y : \mathbb{B}^2 \vdash (\text{tail } x)?(\text{not } (f (\text{head } y))) \cdot (f (\text{head } y)) : \mathbb{B}} \quad C}{\overline{y : \mathbb{B}^2 \vdash (\text{tail } y)?(\text{not } (f (\text{head } y))) \cdot (f (\text{head } y)) : \mathbb{B}} \quad (D.4)} $$

$$ \frac{\overline{\overline{x : \mathbb{B}^2 \vdash x : \mathbb{B}^2} \quad Ax \quad \times_{E_r}}}{\overline{x : \mathbb{B}^2 \vdash \text{head } x : \mathbb{B}} \quad \times_{E_r}} \quad \overline{\overline{y : \mathbb{B}^2 \vdash (\text{tail } y)?(\text{not } (f (\text{head } y})) \cdot (f (\text{head } y)) : \mathbb{B}} \quad C \quad \times_I}} \quad \overline{x : \mathbb{B}^2, y : \mathbb{B}^2 \vdash (\text{head } x) \times (\text{tail } y)?(\text{not } (f (\text{head } y})) \cdot f (\text{head } y) : \mathbb{B}^2} \quad C \quad \Rightarrow_I \quad \overline{\vdash U_f : \mathbb{B}^2 \Rightarrow \mathbb{B}^2} \quad \Rightarrow_I \quad (D.5) $$

$$ \frac{\overline{(D.1) \quad \vdash \mathbf{H} : \mathbb{B} \Rightarrow S(\mathbb{B})}}{\overline{x : \mathbb{B}^2 \vdash \mathbf{H} (\text{head } x) : S(\mathbb{B})}} \quad \overline{x : \mathbb{B}^2 \vdash x : \mathbb{B}^2} \quad Ax \quad \Rightarrow_E \quad \overline{y : \mathbb{B}^2 \vdash \mathbf{H} (\text{tail } y) : S(\mathbb{B})} \quad Ax \quad \Rightarrow_E \quad \overline{y : \mathbb{B}^2 \vdash y : \mathbb{B}^2} \quad Ax \quad \Rightarrow_E \quad \overline{\vdash |0\rangle : \mathbb{B}} \quad Ax_{|0\rangle} \quad \overline{\vdash |1\rangle : \mathbb{B}} \quad Ax_{|1\rangle} \quad \Rightarrow_I \quad \overline{x : \mathbb{B}^2 \vdash (\mathbf{H} (\text{head } x)) \times (\mathbf{H} (\text{tail } y)) : S(\mathbb{B}) \times S(\mathbb{B})} \quad C \quad \Rightarrow_I \quad \overline{\vdash \mathbf{H}_{\text{both}} : \mathbb{B}^2 \Rightarrow S(\mathbb{B}) \times S(\mathbb{B})} \quad \overline{\vdash |01\rangle : \mathbb{B}^2} \quad \Rightarrow_E \quad \overline{\vdash \mathbf{H}_{\text{both}} |01\rangle : S(\mathbb{B}) \times S(\mathbb{B})} \quad (D.6) $$
$$
\frac{(D.2)}{\begin{array}{c} \vdash H_1 : \mathbb{B}^2 \Rightarrow S(\mathbb{B}) \times \mathbb{B} \\ \vdash H_1 : S(\mathbb{B}^2 \Rightarrow S(\mathbb{B}) \times \mathbb{B}) \end{array}} \preceq \frac{(D.5)}{\begin{array}{c} \vdash U_f : \mathbb{B}^2 \Rightarrow \mathbb{B}^2 \\ \vdash U_f : S(\mathbb{B}^2 \Rightarrow \mathbb{B}^2) \end{array}} \preceq \frac{(D.6)}{\begin{array}{c} \vdash H_{\text{both}} |01\rangle : S(\mathbb{B}) \times S(\mathbb{B}) \\ \vdash H_{\text{both}} |01\rangle : S(S(\mathbb{B}) \times S(\mathbb{B})) \\ \vdash \hat{\uparrow}_r H_{\text{both}} |01\rangle : S(\mathbb{B} \times S(\mathbb{B})) \\ \vdash \hat{\uparrow}_\ell \hat{\uparrow}_r H_{\text{both}} |01\rangle : S(\mathbb{B}^2) \end{array}} \preceq \hat{\uparrow}_r \hat{\uparrow}_\ell \\
\frac{\begin{array}{c} \vdash H_1 (U_f \hat{\uparrow}_\ell \hat{\uparrow}_r H_{\text{both}} |01\rangle) : S(S(\mathbb{B}) \times \mathbb{B}) \\ \vdash \hat{\uparrow}_r H_1 (U_f \hat{\uparrow}_\ell \hat{\uparrow}_r H_{\text{both}} |01\rangle) : S(\mathbb{B}^2) \end{array}}{\begin{array}{c} \hat{\uparrow}_r \\ S_E \end{array}} \Rightarrow_{ES} \frac{\begin{array}{c} \vdash U_f (\hat{\uparrow}_\ell \hat{\uparrow}_r H_{\text{both}} |01\rangle) : S(\mathbb{B}^2) \\ \vdash Deutsch_f : \mathbb{B} \times S(\mathbb{B}) \end{array}}
$$

Appendix E. Trace and typing of the Teleportation algorithm

The full trace of Teleportation $(\alpha. |0\rangle + \beta. |1\rangle)$ is given below.

$$
\begin{align*}
\text{Teleportation } (\alpha. |0\rangle + \beta. |1\rangle) \\
&= (\lambda q^{S(\mathbb{B})}. \text{Bob } \hat{\uparrow}_{\ell} \text{ (Alice } (q \times \beta_{00}))) (\alpha. |0\rangle + \beta. |1\rangle) \\
&\xrightarrow{\text{-(}\beta_n\text{)}} \text{Bob } \hat{\uparrow}_{\ell} \text{ (Alice } ((\alpha. |0\rangle + \beta. |1\rangle) \times \beta_{00})) \\
&\xrightarrow{\text{-(}\beta_n^\dagger\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. |0\rangle + \beta. |1\rangle) \times \beta_{00}))) \\
&\xrightarrow{\text{-(dist}^+\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. |0\rangle \times \beta_{00}) + \hat{\uparrow}_r (\beta. |1\rangle \times \beta_{00})))) \\
&\xrightarrow{\text{-(dist}^-\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. |0\rangle \times \beta_{00}) + \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\beta. |1\rangle \times \beta_{00})))) \\
&\xrightarrow{\text{-(dist}^\alpha\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. |0\rangle \times \beta_{00}) + \hat{\uparrow}_{\ell} \hat{\uparrow}_r (|1\rangle \times \beta_{00})))) \\
&\xrightarrow{\text{-(neu}\hat{\uparrow}_r\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. |0\rangle \times \beta_{00}) + \hat{\uparrow}_{\ell} \hat{\uparrow}_r (|1\rangle \times \beta_{00})))) \\
&\xrightarrow{\text{-(dist}^\beta\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. |0\rangle \times \beta_{00}) + \beta. \hat{\uparrow}_{\ell} (|1\rangle \times \beta_{00})))) \\
&\xrightarrow{\text{-(dist}^+\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. |0\rangle \times (\frac{1}{\sqrt{2}}. |00\rangle) \\
&\qquad + (\hat{\uparrow}_{\ell} (|0\rangle \times \frac{1}{\sqrt{2}}. |11\rangle)))) \\
&\qquad + \beta. (\hat{\uparrow}_{\ell} (|1\rangle \times (\frac{1}{\sqrt{2}}. |00\rangle) \\
&\qquad + (\hat{\uparrow}_{\ell} (|1\rangle \times \frac{1}{\sqrt{2}}. |11\rangle)))))) \\
&\xrightarrow{\text{-(dist}^\alpha\text{)}} \text{Bob } \hat{\uparrow}_{\ell} (\pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3 \hat{\uparrow}_{\ell} \hat{\uparrow}_r (\alpha. (\frac{1}{\sqrt{2}}. \hat{\uparrow}_{\ell} |000\rangle + \frac{1}{\sqrt{2}}. \hat{\uparrow}_{\ell} |011\rangle) \\
&\qquad + \beta. (\frac{1}{\sqrt{2}}. \hat{\uparrow}_{\ell} |100\rangle + \frac{1}{\sqrt{2}}. \hat{\uparrow}_{\ell} |111\rangle))))
\end{align*}
$$
$$ \xrightarrow{(\text{neut}\uparrow)_{(1)}^4} \text{Bob} \quad \begin{aligned} \hat{\ell} \left( \pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3) \left( \begin{aligned}[t] & \alpha \left( \frac{1}{\sqrt{2}} \cdot |000\rangle + \frac{1}{\sqrt{2}} \cdot |011\rangle \right) \\ & + \beta \left( \frac{1}{\sqrt{2}} \cdot |100\rangle + \frac{1}{\sqrt{2}} \cdot |111\rangle \right) \end{aligned} \right) \right) \end{aligned} $$

$$ \xrightarrow{(\alpha \text{dist})_{(1)}^2} \text{Bob} \quad \begin{aligned} \hat{\ell} \left( \pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3) \left( \begin{aligned}[t] & \alpha \frac{1}{\sqrt{2}} \cdot |000\rangle + \alpha \frac{1}{\sqrt{2}} \cdot |011\rangle \\ & + (\beta \frac{1}{\sqrt{2}} \cdot |100\rangle + \beta \frac{1}{\sqrt{2}} \cdot |111\rangle) \end{aligned} \right) \right) \end{aligned} $$

$$ \xrightarrow{(\text{prod})_{(1)}^4} \text{Bob} \quad \begin{aligned} \hat{\ell} \left( \pi_2(\hat{\uparrow}_r H_1^3(\text{cnot}_{12}^3) \left( \begin{aligned}[t] & \frac{\alpha}{\sqrt{2}} \cdot |000\rangle + \frac{\alpha}{\sqrt{2}} \cdot |011\rangle \\ & + (\frac{\beta}{\sqrt{2}} \cdot |100\rangle + \frac{\beta}{\sqrt{2}} \cdot |111\rangle) \end{aligned} \right) \right) \end{aligned} $$

$$ \xrightarrow{(\text{lin}^+_{(1)})^3} \text{Bob} \quad \begin{aligned} \hat{\ell} \left( \pi_2(\hat{\uparrow}_r H_1^3 \left( \begin{aligned}[t] & \frac{\alpha}{\sqrt{2}} \cdot |000\rangle + \text{cnot}_{12}^3 \frac{\alpha}{\sqrt{2}} \cdot |011\rangle \\ & + (\text{cnot}_{12}^3 \frac{\beta}{\sqrt{2}} \cdot |100\rangle + \text{cnot}_{12}^3 \frac{\beta}{\sqrt{2}} \cdot |111\rangle) \end{aligned} \right) \right) \end{aligned} $$

$$ \xrightarrow{(\text{lin}^{-\alpha}_{(1)})^4} \text{Bob} \quad \begin{aligned} \hat{\ell} \left( \pi_2(\hat{\uparrow}_r H_1^3 \left( \begin{aligned}[t] & \frac{\alpha}{\sqrt{2}} \cdot \text{cnot}_{12}^3 |000\rangle + \frac{\alpha}{\sqrt{2}} \cdot \text{cnot}_{12}^3 |011\rangle \\ & + (\frac{\beta}{\sqrt{2}} \cdot \text{cnot}_{12}^3 |100\rangle + \frac{\beta}{\sqrt{2}} \cdot \text{cnot}_{12}^3 |111\rangle) \end{aligned} \right) \right) \end{aligned} $$

$$ \xrightarrow{(\beta \text{ dist})_{(1)}^4} \text{Bob} \quad \begin{aligned} \hat{\ell} \left( \pi_2(\hat{\uparrow}_r H_1^3 \left( \begin{aligned}[t] & \frac{\alpha}{\sqrt{2}} \cdot \left( \text{cnot (head } |000\rangle \times \text{ (head tail } |000\rangle) \right) \times \text{ (tail tail } |000\rangle) \\ & + \frac{\alpha}{\sqrt{2}} \cdot \left( \text{cnot (head } |011\rangle \times \text{ (head tail } |011\rangle) \right) \times \text{ (tail tail } |011\rangle) \end{aligned} \right) \right. \\ \left. + (\frac{\beta}{\sqrt{2}} \cdot \left( \text{cnot (head } |100\rangle \times \text{ (head tail } |100\rangle) \right) \times \text{ (tail tail } |100\rangle) \right. \\ \left. + \frac{\beta}{\sqrt{2}} \cdot \left( \text{cnot (head } |111\rangle \times \text{ (head tail } |111\rangle) \right) \times \text{ (tail tail } |111\rangle) \right) \right) \end{aligned} $$

$$ \xrightarrow{(\text{tail})_{(1)}^{12}} \text{Bob} \quad \begin{aligned} \hat{\ell} \left( \pi_2(\hat{\uparrow}_r H_1^3 \left( \begin{aligned}[t] & \frac{\alpha}{\sqrt{2}} \cdot \left( \text{cnot (head } |000\rangle \times \text{ (head } |00\rangle) \right) \times \left( |0\rangle \right) \\ & + \frac{\alpha}{\sqrt{2}} \cdot \left( \text{cnot (head } |011\rangle \times \text{ (head } |11\rangle) \right) \times \left( |1\rangle \right) \\ & + (\frac{\beta}{\sqrt{2}} \cdot \left( \text{cnot (head } |100\rangle \times \text{ (head } |00\rangle) \right) \times \left( |0\rangle \right) \\ & + \frac{\beta}{\sqrt{2}} \cdot \left( \text{cnot (head } |111\rangle \times \text{ (head } |11\rangle) \right) \times \left( |1\rangle \right) \end{aligned} \right) \right) \end{aligned} $$
$$
\begin{align*}
\xrightarrow{\text{(head)}^8} \text{(1)} \quad \text{Bob} \quad \hat{\pi}_\ell \left( \pi_2(\hat{\pi}_r H_1^3 \left( \begin{aligned}[t] & \left(\frac{\alpha}{\sqrt{2}}\right) \cdot \left( \text{cnot } |00\rangle \right) \times (|0\rangle) \\ & + \left(\frac{\alpha}{\sqrt{2}}\right) \cdot \left( \text{cnot } |01\rangle \right) \times (|1\rangle) \end{aligned} \right) \right) \right. \\
\qquad \left. + \left(\frac{\beta}{\sqrt{2}}\right) \cdot \left( \text{cnot } |10\rangle \right) \times (|0\rangle) \right. \\
\qquad \left. + \left(\frac{\beta}{\sqrt{2}}\right) \cdot \left( \text{cnot } |11\rangle \right) \times (|1\rangle) \right) \right)
\end{align*}
$$

$$
\begin{align*}
\xrightarrow{\text{(}\beta_k\text{)}^4} \text{(1)} \quad \text{Bob} \quad \hat{\pi}_\ell \left( \pi_2(\hat{\pi}_r H_1^3 \left( \begin{aligned}[t] & \left(\frac{\alpha}{\sqrt{2}}\right) \cdot \left( \text{head } |00\rangle \right) \times \left( \text{head } |00\rangle \right) \cdot \left( \text{not(tail } |00\rangle \right) \cdot \left( \text{tail } |00\rangle \right)) \times |0\rangle \\ & + \left(\frac{\alpha}{\sqrt{2}}\right) \cdot \left( \text{head } |01\rangle \right) \times \left( \text{head } |01\rangle \right) \cdot \left( \text{not(tail } |01\rangle \right) \cdot \left( \text{tail } |01\rangle \right)) \times |1\rangle \\ & + \left(\frac{\beta}{\sqrt{2}}\right) \cdot \left( \text{head } |10\rangle \right) \times \left( \text{head } |10\rangle \right) \cdot \left( \text{not(tail } |10\rangle \right) \cdot \left( \text{tail } |10\rangle \right)) \times |0\rangle \\ & + \left(\frac{\beta}{\sqrt{2}}\right) \cdot \left( \text{head } |11\rangle \right) \times \left( \text{head } |11\rangle \right) \cdot \left( \text{not(tail } |11\rangle \right) \cdot \left( \text{tail } |11\rangle \right)) \times |1\rangle \end{aligned} \right) \right)
\end{align*}
$$

$$
\begin{align*}
\xrightarrow{\text{(head)}^8} \text{(1)} \quad \text{Bob} \quad \hat{\pi}_\ell \left( \pi_2(\hat{\pi}_r H_1^3 \left( \begin{aligned}[t] & \left(\frac{\alpha}{\sqrt{2}}\right) \cdot \left( (|0\rangle \times (|0\rangle \cdot (\text{not(tail }|00\rangle \cdot (\text{tail }|00\rangle \rangle \times |0\rangle) \right. \\ & \left. + \frac{\alpha}{\sqrt{2}} \cdot \left( (|0\rangle \times (|0\rangle \cdot (\text{not(tail }|01\rangle \cdot (\text{tail }|01\rangle \rangle \times |1\rangle) \right. \\ & \left. + \frac{\beta}{\sqrt{2}} \cdot \left( (|1\rangle \times (|1\rangle \cdot (\text{not(tail }|10\rangle \cdot (\text{tail }|10\rangle \rangle \times |0\rangle) \right. \\ & \left. + \frac{\beta}{\sqrt{2}} \cdot \left( (|1\rangle \times (|1\rangle \cdot (\text{not(tail }|11\rangle \cdot (\text{tail }|11\rangle \rangle \times |1\rangle \right) \end{aligned} \right) \right) \right) \right) \right) \right)
\end{align*}
$$

$$
\begin{align*}
\xrightarrow{\text{(ifq)}^2} \text{(1)} \quad \text{Bob} \quad \hat{\pi}_\ell \left( \pi_2(\hat{\pi}_r H_1^3 \left( \begin{aligned}[t] & \left(\frac{\alpha}{\sqrt{2}}\right) \cdot \left( (|0\rangle \times (|0\rangle \cdot (\text{not(tail }|00\rangle \cdot (\text{tail }|00\rangle \rangle \times |0\rangle) \right. \\ & \left. + \frac{\alpha}{\sqrt{2}} \cdot \left( (|0\rangle \times (|0\rangle \cdot (\text{not(tail }|01\rangle \cdot (\text{tail }|01\rangle \rangle \times |1\rangle) \right. \\ & \left. + \frac{\beta}{\sqrt{2}} \cdot \left( (|1\rangle \times (\text{not(tail }|10\rangle \rangle) \times |0\rangle) \right. \\ & \left. + \frac{\beta}{\sqrt{2}} \cdot \left( (|1\rangle \times (\text{not(tail }|11\rangle \rangle) \times |1\rangle) \right) \end{aligned} \right) \right) \right) \right)
\end{align*}
$$

$$
\begin{align*}
\xrightarrow{\text{(ifq)}^2} \text{(1)} \quad \text{Bob} \quad \hat{\pi}_\ell \left( \pi_2(\hat{\pi}_r H_1^3 \left( \begin{aligned}[t] & \left(\frac{\alpha}{\sqrt{2}}\right) \cdot \left( (|0\rangle \times (\text{tail }|00\rangle) \times |0\rangle \right. \\ & + \frac{\alpha}{\sqrt{2}} \cdot \left( (|0\rangle \times (\text{tail }|01\rangle) \times |1\rangle \right) \\ & + \frac{\beta}{\sqrt{2}} \cdot \left( (|1\rangle \times (\text{not(tail }|10\rangle) \rangle \times |0\rangle) \right. \\ & + \frac{\beta}{\sqrt{2}} \cdot \left( (|1\rangle \times (\text{not(tail }|11\rangle) \rangle \times |1\rangle) \right) \end{aligned} \right) \right)
\end{align*}
$$
$$
\begin{align*}
\xrightarrow{\text{(ta(i))}^4} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r H_1^3(\left(\left(\frac{\alpha}{\sqrt{2}}\cdot\left(\langle 0|\times|0\rangle\right)\times|0\rangle\right)\right.}} \\
\qquad \qquad \qquad \qquad \left. + \frac{\alpha}{\sqrt{2}}\cdot\left(\langle 0|\times|1\rangle\right)\times|1\rangle\right)) \\
\qquad \qquad \qquad \qquad \left. + \left(\frac{\beta}{\sqrt{2}}\cdot\left(\langle 1|\times(\text{not }|0\rangle)\right)\times|0\rangle\right)\right. \\
\qquad \qquad \qquad \qquad \left. + \frac{\beta}{\sqrt{2}}\cdot\left(\langle 1|\times(\text{not }|1\rangle)\right)\times|1\rangle\right))\right))
\end{align*}
$$

$$
\begin{align*}
\xrightarrow{\text{(}\beta_k^2\text{)}} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r H_1^3(\left(\left(\frac{\alpha}{\sqrt{2}}\cdot\langle 0|\times|0\rangle\times|0\rangle\right)\right.}} \\
\qquad \qquad \qquad \qquad \left. + \frac{\alpha}{\sqrt{2}}\cdot\langle 0|\times|1\rangle\times|1\rangle\right)) \\
\qquad \qquad \qquad \qquad \left. + \left(\frac{\beta}{\sqrt{2}}\cdot\langle 1|\times(\langle 0|?|0\rangle\cdot|1\rangle)\times|0\rangle\right)\right. \\
\qquad \qquad \qquad \qquad \left. + \frac{\beta}{\sqrt{2}}\cdot\langle 1|\times(\langle 1|?|0\rangle\cdot|1\rangle)\times|1\rangle\right))\right))
\end{align*}
$$

$$
\begin{align*}
\xrightarrow{\text{(i\ell)}} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r H_1^3(\left(\left(\frac{\alpha}{\sqrt{2}}\cdot\langle 0|\times|0\rangle\times|0\rangle\right)\right.}} \\
\qquad \qquad \qquad \qquad \left. + \frac{\alpha}{\sqrt{2}}\cdot\langle 0|\times|1\rangle\times|1\rangle\right)) \\
\qquad \qquad \qquad \qquad \left. + \left(\frac{\beta}{\sqrt{2}}\cdot\langle 1|\times|1\rangle\times|1\rangle\right)\right. \\
\qquad \qquad \qquad \qquad \left. + \frac{\beta}{\sqrt{2}}\cdot\langle 1|\times(\langle 1|?|0\rangle\cdot|1\rangle)\times|1\rangle\right))\right))
\end{align*}
$$

$$
\xrightarrow{\text{(i\ell)}} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r H_1^3(\left(\left(\frac{\alpha}{\sqrt{2}}\cdot|000\rangle + \frac{\alpha}{\sqrt{2}}\cdot|011\rangle\right) + \left(\frac{\beta}{\sqrt{2}}\cdot|110\rangle + \frac{\beta}{\sqrt{2}}\cdot|101\rangle\right)\right)))
$$

$$
\xrightarrow{\text{(lin}_r^+)^3} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r ((H_1^3(\frac{\alpha}{\sqrt{2}}|000\rangle) + H_1^3(\frac{\alpha}{\sqrt{2}}|011\rangle)) + (H_1^3(\frac{\beta}{\sqrt{2}}|110\rangle) + H_1^3(\frac{\beta}{\sqrt{2}}|101\rangle))))
$$

$$
\xrightarrow{\text{(lin}^\alpha\text{)}} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r ((\frac{\alpha}{\sqrt{2}} \cdot H_1^3|000\rangle + \frac{\alpha}{\sqrt{2}} \cdot H_1^3|011\rangle) + (\frac{\beta}{\sqrt{2}} \cdot H_1^3|110\rangle + \frac{\beta}{\sqrt{2}} \cdot H_1^3|101\rangle))))
$$

$$
\xrightarrow{\text{(}\beta_k^4\text{)}} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r ((\frac{\alpha}{\sqrt{2}}\cdot((H(\text{head }|000\rangle) \times (\text{tail }|000\rangle) + \frac{\alpha}{\sqrt{2}}\cdot((H(\text{head }|011\rangle) \times (\text{tail }|011\rangle) \\
\qquad + (\frac{\beta}{\sqrt{2}}\cdot((H(\text{head }|110\rangle) \times (\text{tail }|110\rangle) + \frac{\beta}{\sqrt{2}}\cdot((H(\text{head }|101\rangle) \times (\text{tail }|101\rangle))))
$$

$$
\xrightarrow{\text{(head)}} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r ((\frac{\alpha}{\sqrt{2}}\cdot((H|0\rangle \times (\text{tail }|000\rangle) + \frac{\alpha}{\sqrt{2}}\cdot((H|0\rangle \times (\text{tail }|011\rangle) \\
\qquad + (\frac{\beta}{\sqrt{2}}\cdot((H|1\rangle \times (\text{tail }|110\rangle) + \frac{\beta}{\sqrt{2}}\cdot((H|1\rangle \times (\text{tail }|101\rangle))))
$$

$$
\xrightarrow{\text{(ta(i))}^4} \text{(1)} \quad \text{Bob} \quad \hat{\mu}_\ell (\pi_2(\hat{\mu}_r ((\frac{\alpha}{\sqrt{2}}\cdot((H|0\rangle \times |00\rangle) + \frac{\alpha}{\sqrt{2}}\cdot((H|0\rangle \times |11\rangle) \\
\qquad + (\frac{\beta}{\sqrt{2}}\cdot((H|1\rangle \times |10\rangle) + \frac{\beta}{\sqrt{2}}\cdot((H|1\rangle \times |01\rangle))))
$$
$$
\begin{aligned}
\xrightarrow{\left(\frac{\beta}{2}\right)^4}_{(1)} \text{Bob} & \hat{\ell}(\pi_2(\hat{\Gamma}_r (\frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + (|0\rangle?(-|1\rangle) \cdot |1\rangle)) \times |00\rangle \\
& + \frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + (|0\rangle?(-|1\rangle) \cdot |1\rangle)) \times |11\rangle \\
& + (\frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + (|1\rangle?(-|1\rangle) \cdot |1\rangle)) \times |10\rangle \\
& + \frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + (|1\rangle?(-|1\rangle) \cdot |1\rangle)) \times |01\rangle)))
\end{aligned}
$$

$$
\begin{aligned}
\xrightarrow{\left(\frac{\Gamma q}{2}\right)^2}_{(1)} \text{Bob} & \hat{\ell}(\pi_2(\hat{\Gamma}_r ((\frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |00\rangle \\
& + \frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |11\rangle))) \\
& + (\frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + (|1\rangle?(-|1\rangle) \cdot |1\rangle)) \times |10\rangle \\
& + \frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + (|1\rangle?(-|1\rangle) \cdot |1\rangle)) \times |01\rangle))))
\end{aligned}
$$

$$
\begin{aligned}
\xrightarrow{\left(\frac{\Gamma q}{2}\right)^2}_{(1)} \text{Bob} & \hat{\ell}(\pi_2(\hat{\Gamma}_r ((\frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |00\rangle \\
& + (\frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle) \times |10\rangle) + \frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |11\rangle))) \\
& + (\frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle) \times |10\rangle) + \frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle) \times |01\rangle))))
\end{aligned}
$$

$$
\begin{aligned}
\xrightarrow{\left(\frac{\text{dist}}{2}\right)^3}_{(1)} \text{Bob} & \hat{\ell}(\pi_2((\hat{\Gamma}_r \frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |00\rangle) + \hat{\Gamma}_r \frac{\alpha}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |11\rangle))) \\
& + (\hat{\Gamma}_r \frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle) \times |10\rangle) + \hat{\Gamma}_r \frac{\beta}{\sqrt{2}} \cdot (\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle) \times |01\rangle)))
\end{aligned}
$$

$$
\begin{aligned}
\xrightarrow{\left(\frac{\text{dist}}{2}\right)^4}_{(1)} \text{Bob} & \hat{\ell}(\pi_2((\frac{\alpha}{\sqrt{2}} \cdot \hat{\Gamma}_r (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |00\rangle) + \frac{\alpha}{\sqrt{2}} \cdot \hat{\Gamma}_r (\frac{1}{\sqrt{2}} \cdot (|0\rangle + |1\rangle) \times |11\rangle))) \\
& + (\frac{\beta}{\sqrt{2}} \cdot \hat{\Gamma}_r (\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle) \times |10\rangle) + \frac{\beta}{\sqrt{2}} \cdot \hat{\Gamma}_r (\frac{1}{\sqrt{2}} \cdot (|0\rangle - |1\rangle) \times |01\rangle)))
\end{aligned}
$$

$$
\begin{aligned}
\xrightarrow{\left(\frac{\text{dist}}{2}\right)^4}_{(1)} \text{Bob} & \hat{\ell}(\pi_2((\frac{\alpha}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} \cdot \hat{\Gamma}_r (|0\rangle + |1\rangle) \times |00\rangle) + \frac{\alpha}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} \cdot \hat{\Gamma}_r (|0\rangle + |1\rangle) \times |11\rangle)) \\
& + (\frac{\beta}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} \cdot \hat{\Gamma}_r (|0\rangle - |1\rangle) \times |10\rangle) + \frac{\beta}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} \cdot \hat{\Gamma}_r (|0\rangle - |1\rangle) \times |01\rangle)))
\end{aligned}
$$

$$
\begin{aligned}
\xrightarrow{\left(\text{prod}\right)^4}_{(1)} \text{Bob} & \hat{\ell}(\pi_2((\frac{\alpha}{2} \cdot \hat{\Gamma}_r (|0\rangle + |1\rangle) \times |00\rangle + \frac{\alpha}{2} \cdot \hat{\Gamma}_r (|0\rangle + |1\rangle) \times |11\rangle)) \\
& + (\frac{\beta}{2} \cdot \hat{\Gamma}_r (|0\rangle - |1\rangle) \times |10\rangle + \frac{\beta}{2} \cdot \hat{\Gamma}_r (|0\rangle - |1\rangle) \times |01\rangle)))
\end{aligned}
$$

$$
\begin{aligned}
\xrightarrow{\left(\frac{\text{dist}}{2}\right)^4}_{(1)} \text{Bob} & \hat{\ell}(\pi_2((\frac{\alpha}{2} \cdot (\hat{\Gamma}_r |000\rangle + \hat{\Gamma}_r |100\rangle) + \frac{\alpha}{2} \cdot (\hat{\Gamma}_r |011\rangle + \hat{\Gamma}_r |111\rangle))) \\
& + (\frac{\beta}{2} \cdot (\hat{\Gamma}_r |010\rangle + \hat{\Gamma}_r (-|110\rangle) + \frac{\beta}{2} \cdot (\hat{\Gamma}_r |001\rangle + \hat{\Gamma}_r (-|101\rangle))))
\end{aligned}
$$
$$ \xrightarrow{(\text{dist}_\epsilon^\alpha)^2} \text{Bob} \quad \begin{aligned} \hat{\mu}_\ell & \left( \pi_2\left(\left(\frac{\alpha}{2} \cdot (\hat{\mu}_r |000\rangle + \hat{\mu}_r |100\rangle) + \frac{\alpha}{2} \cdot (\hat{\mu}_r |011\rangle + \hat{\mu}_r |111\rangle)\right) \right. \\ & \qquad \left. + \left(\frac{\beta}{2} \cdot (\hat{\mu}_r |010\rangle - \hat{\mu}_r |110\rangle) + \frac{\beta}{2} \cdot (\hat{\mu}_r |001\rangle - \hat{\mu}_r |101\rangle)\right) \right) \end{aligned} $$

$$ \xrightarrow{(\text{neut}_\epsilon^\alpha)^8} \text{Bob} \quad \begin{aligned} \hat{\mu}_\ell & \left( \pi_2\left(\left(\frac{\alpha}{2} \cdot (|000\rangle + |100\rangle) + \frac{\alpha}{2} \cdot (|011\rangle + |111\rangle)\right) \right. \\ & \qquad \left. + \left(\frac{\beta}{2} \cdot (|010\rangle - |110\rangle) + \frac{\beta}{2} \cdot (|001\rangle - |101\rangle)\right) \right) \end{aligned} $$

$$ \xrightarrow{(\text{dist})^4} \text{Bob} \quad \begin{aligned} \hat{\mu}_\ell & \left( \pi_2\left(\left(\frac{\alpha}{2} \cdot |000\rangle + \frac{\alpha}{2} \cdot |100\rangle\right) + \left(\frac{\alpha}{2} \cdot |011\rangle + \frac{\alpha}{2} \cdot |111\rangle\right) \right. \right. \\ & \qquad \left. + \left(\frac{\beta}{2} \cdot |010\rangle + \frac{\beta}{2} \cdot (-|110\rangle)\right) + \left(\frac{\beta}{2} \cdot |001\rangle + \frac{\beta}{2} \cdot (-|101\rangle)\right) \right) \end{aligned} $$

$$ \xrightarrow{(\text{prod})^2} \text{Bob} \quad \begin{aligned} \hat{\mu}_\ell & \left( \pi_2\left(\left(\frac{\alpha}{2} \cdot |000\rangle + \frac{\alpha}{2} \cdot |100\rangle\right) + \left(\frac{\alpha}{2} \cdot |011\rangle + \frac{\alpha}{2} \cdot |111\rangle\right) \right. \right. \\ & \qquad \left. + \left(\frac{\beta}{2} \cdot |010\rangle - \frac{\beta}{2} \cdot |110\rangle\right) + \left(\frac{\beta}{2} \cdot |001\rangle - \frac{\beta}{2} \cdot |101\rangle\right) \right) \end{aligned} $$

$$ =_{AC} \text{Bob} \quad \begin{aligned} \hat{\mu}_\ell & \left( \pi_2\left(\left(\frac{\alpha}{2} \cdot |000\rangle + \frac{\beta}{2} \cdot |001\rangle\right) + \left(\frac{\alpha}{2} \cdot |011\rangle + \frac{\beta}{2} \cdot |010\rangle\right) \right. \right. \\ & \qquad \left. + \left(\frac{\alpha}{2} \cdot |100\rangle - \frac{\beta}{2} \cdot |101\rangle\right) + \left(\frac{\alpha}{2} \cdot |111\rangle - \frac{\beta}{2} \cdot |110\rangle\right) \right) \end{aligned} $$

The next rewrite step following rule (proj), may produce one of the following four results probability $\frac{1}{4}$ each:

$$ (00) \quad \text{Bob} \quad \hat{\mu}_\ell |00\rangle \times (\alpha. |0\rangle + \beta. |1\rangle) $$

$$ (01) \quad \text{Bob} \quad \hat{\mu}_\ell |01\rangle \times (\alpha. |1\rangle + \beta. |0\rangle) $$

$$ (10) \quad \text{Bob} \quad \hat{\mu}_\ell |01\rangle \times (\alpha. |0\rangle - \beta. |1\rangle) $$

$$ (11) \quad \text{Bob} \quad \hat{\mu}_\ell |11\rangle \times (\alpha. |1\rangle - \beta. |0\rangle) $$

So, in general, Bob $\hat{\mu}_\ell |xy\rangle \times (\alpha. |z\rangle + [-] \beta. |w\rangle)$. Then,

$$ \text{Bob} \quad \hat{\mu}_\ell |xy\rangle \times (\alpha. |z\rangle + [-] \beta. |w\rangle) $$

$$ \xrightarrow{(\text{dist})^+} \text{Bob} \left( \hat{\mu}_\ell |xy\rangle \times \alpha. |z\rangle + \hat{\mu}_\ell |xy\rangle \times [-] \beta. |w\rangle \right) $$

$$ \xrightarrow{(\text{dist})^\alpha} \text{Bob} \left( \alpha. \hat{\mu}_\ell |xyz\rangle + [-] \beta. \hat{\mu}_\ell |xyw\rangle \right) $$

$$ \xrightarrow{(\text{neut})^\alpha} \text{Bob} \left( \alpha. |xyz\rangle + [-] \beta. |xyw\rangle \right) $$

$$ \xrightarrow{(\text{lin})^+} \text{Bob} \left( \alpha. |xyz\rangle + \text{Bob} [-] \beta. |xyw\rangle \right) $$

$$ \xrightarrow{(\text{lin})^\alpha} \text{Bob} \left( \alpha. \text{Bob} |xyz\rangle + [-] \beta. \text{Bob} |xyw\rangle \right) $$

$$ \xrightarrow{(\beta_1)} \text{Bob} \left( \alpha. Z^{\text{head}|xyz\rangle} (\text{not}^{\text{head tail}|xyz\rangle} (\text{tail tail } |xyz\rangle) + [-] \beta. Z^{\text{head}|xyw\rangle} (\text{not}^{\text{head tail}|xyw\rangle} (\text{tail tail } |xyw\rangle) \right) $$

$$ \xrightarrow{(\text{tail})^6} \text{Bob} \left( \alpha. Z^{\text{head}|xyz\rangle} (\text{not}^{\text{head}|yz\rangle} (|z\rangle) + [-] \beta. Z^{\text{head}|xyw\rangle} (\text{not}^{\text{head}|yw\rangle} (|w\rangle) \right) $$

$$ \xrightarrow{(\text{head})^4} \text{Bob} \left( \alpha. Z^{|x\rangle} (\text{not}^{|y\rangle} |z\rangle) + [-] \beta. Z^{|x\rangle} (\text{not}^{|y\rangle} |w\rangle) \right) $$

$$ \xrightarrow{(\beta_2)} \text{Bob} \left( \alpha. Z^{|x\rangle} (|y\rangle?\text{not}|z\rangle|z\rangle) + [-] \beta. Z^{|x\rangle} (|y\rangle?\text{not}|w\rangle|w\rangle) \right) $$

Cases:
$$
(00) \quad (\alpha.Z^{|0\rangle}(|0\rangle?\text{not}|0\rangle|0\rangle) + \beta.Z^{|0\rangle}(|0\rangle?\text{not}|1\rangle|1\rangle)) \\
\xrightarrow{\text{(if}_0^2} (\alpha.Z^{|0\rangle}|0\rangle + \beta.Z^{|0\rangle}|1\rangle) \\
\xrightarrow{\text{(\beta}_0^4} (\alpha.|0\rangle?(Z|0\rangle)|0\rangle + \beta.|0\rangle?(Z|1\rangle)|1\rangle) \\
\xrightarrow{\text{(if}_0^2} (\alpha.|0\rangle + \beta.|1\rangle)
$$

$$
(01) \quad (\alpha.Z^{|0\rangle}(|1\rangle?\text{not}|1\rangle|1\rangle) + \beta.Z^{|0\rangle}(|1\rangle?\text{not}|0\rangle|0\rangle)) \\
\xrightarrow{\text{(if}_1^2} (\alpha.Z^{|0\rangle}(\text{not}|1\rangle) + \beta.Z^{|0\rangle}(\text{not}|0\rangle)) \\
\xrightarrow{\text{(\beta}_1^4} (\alpha.Z^{|0\rangle}(|1\rangle?|0\rangle|1\rangle) + \beta.Z^{|0\rangle}(|0\rangle?|0\rangle|1\rangle)) \\
\xrightarrow{\text{(if}_3^2} (\alpha.Z^{|0\rangle}|0\rangle + \beta.Z^{|0\rangle}(|0\rangle?|0\rangle|1\rangle)) \\
\xrightarrow{\text{(if}_0^2} (\alpha.Z^{|0\rangle}|0\rangle + \beta.Z^{|0\rangle}|1\rangle) \\
\xrightarrow{\text{(\beta}_1^4} (\alpha.|0\rangle?(Z|0\rangle)|0\rangle + \beta.|0\rangle?(Z|1\rangle)|1\rangle) \\
\xrightarrow{\text{(if}_0^2} (\alpha.|0\rangle + \beta.|1\rangle)
$$

$$
(10) \quad (\alpha.Z^{|1\rangle}(|0\rangle?\text{not}|0\rangle|0\rangle) - \beta.Z^{|1\rangle}(|0\rangle?\text{not}|1\rangle|1\rangle)) \\
\xrightarrow{\text{(if}_0^2} (\alpha.Z^{|1\rangle}|0\rangle - \beta.Z^{|1\rangle}|1\rangle) \\
\xrightarrow{\text{(\beta}_0^4} (\alpha.|1\rangle?(Z|0\rangle)|0\rangle - \beta.|1\rangle?(Z|1\rangle)|1\rangle) \\
\xrightarrow{\text{(if}_1^2} (\alpha.Z^{|0\rangle} - \beta.Z^{|1\rangle}) \\
\xrightarrow{\text{(\beta}_1^2} (\alpha.|0\rangle?(-|1\rangle)|0\rangle - \beta.|1\rangle?(-|1\rangle)|0\rangle) \\
\xrightarrow{\text{(if}_0^2} (\alpha.|0\rangle - \beta.|1\rangle?(-|1\rangle)|0\rangle) \\
\xrightarrow{\text{(if}_3^2} (\alpha.|0\rangle - \beta.(-|1\rangle)) \\
\xrightarrow{(\text{prod})} (\alpha.|0\rangle + \beta.|1\rangle)
$$

$$
(11) \quad (\alpha.Z^{|1\rangle}(|1\rangle?\text{not}|1\rangle|1\rangle) - \beta.Z^{|1\rangle}(|1\rangle?\text{not}|0\rangle|0\rangle)) \\
\xrightarrow{\text{(if}_1^2} (\alpha.Z^{|1\rangle}(\text{not}|1\rangle) - \beta.Z^{|1\rangle}(\text{not}|0\rangle)) \\
\xrightarrow{\text{(\beta}_1^2} (\alpha.Z^{|1\rangle}(|1\rangle?|0\rangle|1\rangle) - \beta.Z^{|1\rangle}(|0\rangle?|0\rangle|1\rangle)) \\
\xrightarrow{\text{(if}_3^2} (\alpha.Z^{|1\rangle}|0\rangle - \beta.Z^{|1\rangle}(|0\rangle?|0\rangle|1\rangle)) \\
\xrightarrow{\text{(if}_0^2} (\alpha.Z^{|1\rangle}|0\rangle - \beta.Z^{|1\rangle}|1\rangle) \\
\xrightarrow{\text{(\beta}_1^4} (\alpha.|1\rangle?(Z|0\rangle)|0\rangle - \beta.|1\rangle?(Z|1\rangle)|1\rangle) \\
\xrightarrow{\text{(if}_1^2} (\alpha.Z^{|0\rangle} + \beta.Z^{|1\rangle}) \\
\xrightarrow{\text{(\beta}_1^2} (\alpha.|0\rangle?(-|1\rangle)|0\rangle - \beta.|1\rangle?(-|1\rangle)|0\rangle) \\
\xrightarrow{\text{(if}_0^2} (\alpha.|0\rangle - \beta.|1\rangle?(-|1\rangle)|0\rangle) \\
\xrightarrow{\text{(if}_3^2} (\alpha.|0\rangle - \beta.(-|1\rangle)) \\
\xrightarrow{(\text{prod})} (\alpha.|0\rangle + \beta.|1\rangle)
$$

Hence, in every case, Teleportation $(\alpha. |0\rangle + \beta. |1\rangle) \xrightarrow{(*) (\alpha. |0\rangle + \beta. |1\rangle)$ as expected.