A lambda calculus for density matrices with classical and probabilistic controls

TL;DR

This paper introduces two quantum lambda calculi using density matrices, enabling formal reasoning about quantum data and mixed states with classical and probabilistic controls.

Contribution

It presents two novel quantum lambda calculi, $ ho$ and $ ho^ullet$, for modeling quantum data and mixed states within a formal lambda calculus framework.

Findings

Provides formal semantics for density matrix-based quantum programs

Defines two calculi capturing classical control and mixed quantum states

Lays groundwork for reasoning about quantum algorithms in lambda calculus

Abstract

In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, $\lambda_\rho$, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, $\lambda_\rho^\circ$, take advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.

Tables

Table 1. Table 1: Grammar of terms of λ ρ subscript 𝜆 𝜌 \lambda_{\rho} .

	$t$	$:=x\mid \lambda x.t\mid tt$	(Standard lambda calculus)
		$\mid {\rho }^n\mid U^{n}t\mid {\pi }^{n}t\mid t\otimes t$	(Quantum postulates)
		$\mid (b^m,{\rho }^n)\mid \mathrm{𝗅𝖾𝗍𝖼𝖺𝗌𝖾}x=r\mathrm{𝗂𝗇}\{t,\dots ,t\}$	(Classical control)

Table 2. Table 2: Rewrite system for λ ρ subscript 𝜆 𝜌 \lambda_{\rho} .

	$(\lambda x.t)r$	${⟶}_{1}t\left[r/x\right]$
	$U^m{\rho }^n$	${⟶}_1\rho _{}^{\prime }{}_{}{}^n$	$\text{with }\rho _{}^{\prime }{}_{}{}^n=\overline{U^m}{\rho }^n{\overline{U^m}}^{†}$
	${\pi }^m{\rho }^n$	${⟶}_{p_i}(i,{\rho }_i^n)$	$\text{with }\{\begin{array}{c}{p}_i=\mathrm{𝗍𝗋}\left({\overline{{\pi }_i}}^{†}\overline{{\pi }_i}{\rho }^n\right)\\ {\rho }_i^n=\frac{\overline{{\pi }_i}{\rho }^n{\overline{{\pi }_i}}^{†}}{p_i}\end{array}$
	$\rho \otimes {\rho }^{\prime }$	${⟶}_1{\rho }^{\prime \prime }$	$\text{with }{\rho }^{\prime \prime }=\rho \otimes {\rho }^{\prime }$
	$\mathrm{𝗅𝖾𝗍𝖼𝖺𝗌𝖾}x=(b^m,{\rho }^n)\mathrm{𝗂𝗇}\{t_0,\dots ,t_{2^m-1}\}$	${⟶}_1{t}_{b^m}\left[{\rho }^n/x\right]$

Table 3. Table 3: Type system for λ ρ subscript 𝜆 𝜌 \lambda_{\rho} .

$A:=n\mid (m,n)\mid A⊸A$

Table 4. Table 4: Interpretation of types

	$⟦n⟧$	$={𝒟}_n$
	$⟦(m,n)⟧$	$={𝒟}_n$
	$⟦A⊸B⟧$	$=\{f\mid \forall e\in ⟦A⟧,\forall b\in {\mathbb{N}}^{\epsilon }\text{ s.t. }P(b,A),$
		$\mathrm{𝗍𝗋𝖽}\left(f(b,e)\right)\subseteq ⟦B⟧,𝗐\left(f(b,e)\right)=1\text{ and }P(f(b,e),B)\}$

Table 5. Table 5: Interpretation of terms

	${⟦x⟧}_{\theta }$	$=\left\{(1,b,e)\right\}\text{ where }\theta \left(x\right)=(b,e)$
	${⟦\lambda x.t⟧}_{\theta }$	$=\left\{(1,\epsilon ,(𝖻,𝖾)\mapsto {⟦t⟧}_{\theta ,x=(𝖻,𝖾)})\right\}$
	${⟦tr⟧}_{\theta }$
	${⟦{\rho }^n⟧}_{\theta }$	$=\left\{(1,\epsilon ,{\rho }^n)\right\}$
	${⟦U^{n}t⟧}_{\theta }$	$=\{(p_i,\epsilon ,\overline{U^n}{\rho }_i{\overline{U^n}}^{†})\mid {⟦t⟧}_{\theta }={\left\{(p_i,b_i,{\rho }_i)\right\}}_i\}$
	${⟦{\pi }^{m}t⟧}_{\theta }$	$=\{(p_j\mathrm{𝗍𝗋}\left({\overline{{\pi }_i}}^{†}\overline{{\pi }_i}{\rho }_j\right),i,\frac{\overline{{\pi }_i}{\rho }_j{\overline{{\pi }_i}}^{†}}{\mathrm{𝗍𝗋}\left({\overline{{\pi }_i}}^{†}\overline{{\pi }_i}{\rho }_j\right)})\mid {⟦t⟧}_{\theta }={\left\{(p_j,b_j,{\rho }_j)\right\}}_j\}$
	${⟦t\otimes r⟧}_{\theta }$
	${⟦(b^m,{\rho }^n)⟧}_{\theta }$	$=\left\{(1,b^m,{\rho }^n)\right\}$

Table 6. Table 6: Grammar of terms of λ ρ ∘ superscript subscript 𝜆 𝜌 \lambda_{\rho}^{\circ} .

	$t$	$:=x\mid \lambda x.t\mid tt$	(Standard lambda calculus)
		$\mid {\rho }^n\mid U^{n}t\mid {\pi }^{n}t\mid t\otimes t$	(Quantum postulates)
		$\mid \sum _{i=1}^n{p}_i{t}_i\mid {\mathrm{𝗅𝖾𝗍𝖼𝖺𝗌𝖾}}^{\circ }x=r\mathrm{𝗂𝗇}\{t,\dots ,t\}$	(Probabilistic control)

Table 7. Table 7: Rewrite system of λ ρ ∘ superscript subscript 𝜆 𝜌 \lambda_{\rho}^{\circ} .

	$(\lambda x.t)r$	$\rightsquigarrow t\left[r/x\right]$
	${\mathrm{𝗅𝖾𝗍𝖼𝖺𝗌𝖾}}^{\circ }x={\pi }^m{\rho }^n\mathrm{𝗂𝗇}\{t_0,\dots ,t_{2^m}-1\}$	$\rightsquigarrow \sum _i{p}_i{t}_i\left[{\rho }_i^n/x\right]$	$\text{with }\{\begin{array}{c}{\rho }_i^n=\frac{\overline{{\pi }_i}{\rho }^n{\overline{{\pi }_i}}^{†}}{p_i}\\ p_i=\mathrm{𝗍𝗋}\left({\overline{{\pi }_i}}^{†}\overline{{\pi }_i}{\rho }^n\right)\end{array}$
	$U^m{\rho }^n$	$\rightsquigarrow \rho _{}^{\prime }{}_{}{}^n$	$\text{with }\overline{U^m}{\rho }^n{\overline{U^m}}^{†}=\rho _{}^{\prime }{}_{}{}^n$
	$\rho \otimes {\rho }^{\prime }$	$\rightsquigarrow {\rho }^{\prime \prime }$	$\text{with }{\rho }^{\prime \prime }=\rho \otimes {\rho }^{\prime }$
	$\sum _i{p}_i{\rho }_i$	$\rightsquigarrow {\rho }^{\prime }$	$\text{with }{\rho }^{\prime }=\sum _i{p}_i{\rho }_i$
	$\sum _i{p}_{i}t$	$\rightsquigarrow t$
	$\left(\sum _i{p}_i{t}_i\right)r$	$\rightsquigarrow \sum _i{p}_i\left(t_{i}r\right)$

Table 8. Table 8: Type system for λ ρ ∘ superscript subscript 𝜆 𝜌 \lambda_{\rho}^{\circ} .

$A:=n\mid (m,n)\mid A⊸A$

Equations

$$\lambda x.t{⟶}_p\lambda x.rt{⟶}_{p}rts{⟶}_{p}rst{⟶}_{p}rst{⟶}_{p}srt{⟶}_{p}r{U}^{n}t{⟶}_p{U}^{n}rt{⟶}_{p}r$$

$${\pi }^{n}t{⟶}_p{\pi }^{n}rt{⟶}_{p}rt\otimes s{⟶}_{p}r\otimes st{⟶}_{p}rs\otimes t{⟶}_{p}s\otimes rt{⟶}_{p}r$$

$$\mathsf{letcase}x=t\mathsf{in}\{s_0,\dots ,s_n\}{⟶}_p\mathsf{letcase}x=r\mathsf{in}\{s_0,\dots ,s_n\}t{⟶}_{p}r$$

$$\Gamma ,x:A⊢x:A\Gamma ⊢\lambda x.t:A⊸B\Gamma ,x:A⊢t:B\Gamma ,\Delta ⊢tr:B\text{lx@proof@logical@and}\Gamma ⊢t:A⊸B\Delta ⊢r:A$$

$$\Gamma ⊢{\rho }^n:n\Gamma ⊢U^{m}t:n\Gamma ⊢t:n\Gamma ⊢{\pi }^{m}t:(m,n)\Gamma ⊢t:n\Gamma ,\Delta ⊢t\otimes r:n+m\text{lx@proof@logical@and}\Gamma ⊢t:n\Delta ⊢r:m$$

$$\Gamma ⊢(b^m,{\rho }^n):(m,n)\Gamma ⊢\mathsf{letcase}x=r\mathsf{in}\{t_0,\dots ,t_{2^m-1}\}:A\text{lx@proof@logical@and}x:n⊢t_0:A\dots x:n⊢t_{2^m-1}:A\Gamma ⊢r:(m,n)$$

$$\lambda x.\mathsf{letcase}y={\pi }^2({\mathsf{H}}^1({\mathsf{Cnot}}^2(x\otimes {\beta }_{00})))\mathsf{in}\{y,{\mathsf{Z}}_{3}y,{\mathsf{X}}_{3}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\}$$

$$⊢\lambda x.\mathsf{letcase}y={\pi }^2({\mathsf{H}}^1({\mathsf{Cnot}}^2(x\otimes {\beta }_{00})))\mathsf{in}\{y,{\mathsf{Z}}_{3}y,{\mathsf{X}}_{3}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\}:1⊸3x:1⊢\mathsf{letcase}y={\pi }^2({\mathsf{H}}^1({\mathsf{Cnot}}^2(x\otimes {\beta }_{00})))\mathsf{in}\{y,{\mathsf{Z}}_{3}y,\mathsf{X}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\}:3\text{lx@proof@logical@and}y:3⊢y:3y:3⊢{\mathsf{Z}}_{3}y:3y:3⊢y:3y:3⊢{\mathsf{X}}_{3}y:3y:3⊢y:3y:3⊢{\mathsf{Z}}_3{\mathsf{X}}_{3}y:3y:3⊢{\mathsf{X}}_{3}y:3y:3⊢y:3x:1⊢{\pi }^2({\mathsf{H}}^1({\mathsf{Cnot}}^2(x\otimes {\beta }_{00}))):(2,3)x:1⊢{\mathsf{H}}^1({\mathsf{Cnot}}^2(x\otimes {\beta }_{00})):3x:1⊢{\mathsf{Cnot}}^2(x\otimes {\beta }_{00}):3x:1⊢x\otimes {\beta }_{00}:3\text{lx@proof@logical@and}x:1⊢x:1⊢{\beta }_{00}:2$$

$$\left[\rho \right]$$

$$\left[(\mathsf{b},\mathsf{e})\mapsto [[t{]]}_{\theta ,x=(\mathsf{b},\mathsf{e})}\right]$$

$$\text{llparenthesis}t{\text{rrparenthesis}}_{\theta }$$

$$\text{llparenthesis}t[r/x]{\text{rrparenthesis}}_{\theta }=\sum _i{p}_i\text{llparenthesis}t{\text{rrparenthesis}}_{\theta ,x=(b_i,e_i)}$$

$${\mathsf{letcase}}^{\circ }x={\pi }^m{\rho }^n\mathsf{in}\{x,\dots ,x\}⇝\sum _i{p}_i{\rho }_i^n⇝{\rho }^{\prime }$$

$$\lambda x.t⇝\lambda x.rt⇝rts⇝rst⇝rst⇝srt⇝r{U}^{n}t⇝U^{n}rt⇝r$$

$${\pi }^{n}t⇝{\pi }^{n}rt⇝rt\otimes s⇝r\otimes st⇝rs\otimes t⇝s\otimes rt⇝r$$

$$\sum _{i=1}^n{p}_i{t}_i⇝\sum _{i=1}^n{p}_i{r}_i{t}_j⇝r_j$$

$${\mathsf{letcase}}^{\circ }x=t\mathsf{in}\{s_0,\dots ,s_{2^m-1}\}⇝{\mathsf{letcase}}^{\circ }x=r\mathsf{in}\{s_0,\dots ,s_{2^m-1}\}t⇝r$$

$$\Gamma ,x:A⊩x:A\Gamma ⊩\lambda x.t:A⊸B\Gamma ,x:A⊩t:B\Gamma ,\Delta ⊩tr:B\text{lx@proof@logical@and}\Gamma ⊩t:A⊸B\Delta ⊩r:A$$

$$\Gamma ⊩{\rho }^n:n\Gamma ⊩U^{m}t:n\Gamma ⊩t:n\Gamma ⊩{\pi }^{m}t:(m,n)\Gamma ⊩t:n\Gamma ,\Delta ⊩t\otimes r:n+m\text{lx@proof@logical@and}\Gamma ⊩t:n\Delta ⊩r:m$$

$$\Gamma ⊩{\mathsf{letcase}}^{\circ }x=r\mathsf{in}\{t_0,\dots ,t_{2^m-1}\}:A\text{lx@proof@logical@and}x:n⊩t_0:A\dots x:n⊩t_{2^m-1}:A\Gamma ⊩r:(m,n)$$

$$\Gamma ⊩\sum _{i=1}^n{p}_i{t}_i:A\text{lx@proof@logical@and}\Gamma ⊩t_1:A\dots \Gamma ⊩t_n:A\sum _{i=1}^n{p}_i=1$$

$${\rho }_0^3=\rho \otimes {\beta }_{00},{\rho }_1^3=(\mathsf{Cnot}\otimes I){\rho }_0^3,\text{and}{\rho }_2^3=(\mathsf{H}\otimes I\otimes I){\rho }_1^3$$

$$(\lambda x.\mathsf{letcase}y={\pi }^2({\mathsf{H}}^1({\mathsf{Cnot}}^2(x\otimes {\beta }_{00})))\mathsf{in}\{y,{\mathsf{Z}}_{3}y,{\mathsf{X}}_{3}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\})\rho$$

$${⟶}_1\mathsf{letcase}y={\pi }^2({\mathsf{H}}^1({\mathsf{Cnot}}^2(\rho \otimes {\beta }_{00})))\mathsf{in}\{y,{\mathsf{Z}}_{3}y,{\mathsf{X}}_{3}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\}$$

$${⟶}_1\mathsf{letcase}y={\pi }^2({\mathsf{H}}^1({\mathsf{Cnot}}^2{\rho }_0^3))\mathsf{in}\{y,{\mathsf{Z}}_{3}y,{\mathsf{X}}_{3}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\}$$

$${⟶}_1\mathsf{letcase}y={\pi }^2({\mathsf{H}}^1{\rho }_1^3)\mathsf{in}\{y,{\mathsf{Z}}_{3}y,{\mathsf{X}}_{3}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\}$$

$${⟶}_1\mathsf{letcase}y={\pi }^2{\rho }_2^3\mathsf{in}\{y,{\mathsf{Z}}_{3}y,{\mathsf{X}}_{3}y,{\mathsf{Z}}_3{\mathsf{X}}_{3}y\}$$

$$\text{eqref}eq:last⇝p_0\rho +p_1{\mathsf{Z}}_3{\rho }_{31}^3+p_2{\mathsf{X}}_3{\rho }_{32}^3+p_3{\mathsf{Z}}_3{\mathsf{X}}_3{\rho }_{33}^3{⇝}^{\ast }\sum _{i=0}^3{p}_i{\rho }_{30}^3⇝(\sum _{i=0}^3{p}_i)\rho ⇝\rho$$

$$[[\sum _i{p}_i{t}_i{]]}_{\theta }=\{(p_i{q}_{ij},b_{ij},e_{ij})\mid [[t_i{]]}_{\theta }=\{(q_{ij},b_{ij},e_{ij}){\}}_j\}$$

$$w$$

$$v$$

$$w$$

$$v$$

$$\begin{array}{rl}(\mathsf{letcase}y={\pi }^1|+⟩⟨+|\mathsf{in}\{\lambda x.x,\lambda x.\mathsf{letcase}w={\pi }^1|+⟩& ⟨+|\mathsf{in}\{w,w\}\})\\ & (\mathsf{letcase}z={\pi }^1\rho \mathsf{in}\{z,z\})\end{array}$$

Full text

1 Introduction

In the last decade several quantum extensions to lambda calculus have been investigated, e.g. [22, 21, 18, 30, 6, 5, 10]. In all of those approaches, the language chosen to represent the quantum state are vectors in a Hilbert space. However, an alternative formulation of quantum mechanics can be made using density matrices. Density matrices provide a way to describe a quantum system in which the state is not fully known. More precisely, density matrices describe quantum systems in a mixed state, that is, a statistical set of several quantum states. All the postulates of quantum mechanics can be described in such a formalism, and hence, also quantum computing can be done using density matrices.

The first postulate states that a quantum system can be fully described by a density matrix $\rho$, which is a positive operator with trace ($\mathsf{tr}$) one. If a system is in state $\rho_{i}$ with probability $p_{i}$, then the density matrix of the system is $\sum_{i}p_{i}\rho_{i}$. The second postulate states that the evolution of a quantum system $\rho$ is described with a unitary operator $U$ by $U\rho U^{\dagger}$, where $U^{\dagger}$ is the adjoint operator of $U$. The third postulate states that the measurement is described by a set of measurement operators $\{\pi_{i}\}_{i}$ with $\sum_{i}\pi_{i}^{\dagger}\pi_{i}=\mathsf{I}$, so that the output of the measurement is $i$, with probability $\mathsf{tr}(\pi_{i}^{\dagger}\pi_{i}\rho)$, leaving the sate of the system as $\frac{\pi_{i}\rho\pi_{i}^{\dagger}}{\mathsf{tr}(\pi_{i}^{\dagger}\pi_{i}\rho)}$. The fourth postulate states that from two systems $\rho$ and $\rho^{\prime}$, the composed one can be described by the tensor product of those $\rho\otimes\rho^{\prime}$.

Naturally, if we want to use the output of a measurement as a condition in the classical control, we need to know that output. However, density matrices can still be used as a way to compare processes before running them. For example the process of tossing a coin, and according to its result, applying Z or not to a balanced superposition, and the process of tossing a coin and not looking at its result, may look quite different in most quantum programming languages. Yet both processes output the same density matrix, and so they are indistinguishable.

In [19], Selinger introduced a language of quantum flow charts, and an interpretation of his language into a CPO of density matrices. After this paper, the language of density matrices has been widely used in quantum programming, e.g. [9, 14, 13, 24, 27]. Indeed, the book “Foundations of Quantum Programming” [26] is entirely written in the language of density matrices. Yet, as far as we know, no lambda calculus for density matrix have been proposed.

Apart from the distinction of languages by how they treat the quantum states (vectors in a Hilbert space or density matrices), we also can distinguish the languages on how the control is considered: either quantumly or classically. The idea of quantum data / classical control stated by Selinger in [19] induced a quantum lambda calculus in this paradigm [21]. Later, this calculus was the base to construct the programming language Quipper [15], an embedded, scalable, functional programming language for quantum computing. The concept of quantum data / classical control declares that quantum computers will run in a specialized device attached to a classical computer, and it is the classical computer which will instruct the quantum computer what operations to perform over which qubits, and then read the classical result after a measurement. It is a direct consequence from the observation that quantum circuits are classical (i.e. one cannot superpose circuits or measure them). Several studies have been done under this paradigm, e.g. [2, 15, 18, 21, 30].

Dually to the quantum data / classical control paradigm, there is what we can call the quantum data and control paradigm. The idea is to provide a computational definition of the notions of vector space and bilinear functions. In the realm of quantum walks, quantum control is not uncommon (e.g. [3, 1]). Also, several high-level languages on quantum control have been proposed in the past (e.g. [2, 28, 29, 8]), however, up to now, no complete lambda-calculus with quantum control have been proposed. We benefit, though, from the long line of works in this direction [6, 5, 4, 7, 12].

In this paper, we propose a quantum extension to the lambda calculus, $\lambda_{\rho}$, in the quantum data / classical control paradigm, where the quantum data is given by density matrices, as first suggested by Selinger’s interpretation of quantum flow charts [19]. Then, we propose a modification of such a calculus, called $\lambda_{\rho}^{\circ}$, in which we generalise the density matrices to the classical control: That is, after a measurement, we take all the possible outcomes in a kind of generalised density matrix of arbitrary terms. The control does not become quantum, since it is not possible to superpose programs in the quantum sense. However, we consider the density matrix of the mixed state of programs arising from a measurement. Therefore, this can be considered as a kind of probabilistic control, or even another way, perhaps weaker, of quantum control.

Outline of the Paper.

In Section 2 we introduce the typed calculus $\lambda_{\rho}$, which manipulates density matrices, and we give two interpretations of the calculus. One where the terms are interpreted into a generalisation of mixed states, and another where the terms are interpreted into density matrices. Then we prove some properties of those interpretations. In Section 3 we introduce a modification of $\lambda_{\rho}$, called $\lambda_{\rho}^{\circ}$, where the output of a measurement produce a sum with all the possible outputs. We then extend the interpretation of $\lambda_{\rho}$ to accommodate $\lambda_{\rho}^{\circ}$, and prove its basic properties. In Section 4 we prove the Subject Reduction (Theorem 4.1) and Progress (Theorem 4.2) properties for both calculi. In Section 5 we give two interesting examples, in both calculi. Finally, in Section 6, we conclude and discuss some future work.

2 Classical-control calculus with probabilistic

rewriting

2.1 Definitions

The grammar of terms, given in Table 1, have been divided in three categories.

Standard lambda calculus terms: Variables from a set $\mathsf{Vars}$, abstractions and applications. 2. 2.

The four postulates of quantum mechanics, with the measurement postulate restricted to measurements in the computational basis111A generalisation to any arbitrary measurement can be considered in a future, however, for the sake of simplicity in the classical control, we consider only measurements in the computational basis, which is a common practice in quantum lambda calculi [18, 20, 21, 30, 16, 10].: $\rho^{n}$ to represent the density matrix of a quantum system. $U^{n}t$ to describe its evolution. $\pi^{n}t$ to measure it. $t\otimes t$ to describe the density matrix of a composite system (that is, a non entangled system composed of two subsystems). 3. 3.

Two constructions for the classical control: a pair $(b^{m},\rho^{n})$, where $b^{m}$ is the output of a measurement in the computational basis and $\rho^{n}$ is the resulting density matrix, and the conditional $\mathsf{letcase}$ construction reading the output of the measurement.

The rewrite system, given in Table 2, is described by the relation $\longrightarrow_{p}$, which is a probabilistic relation where $p$ is the probability of occurrence. If $U^{m}$ is applied to $\rho^{n}$, with $m\leq n$, we write $\overline{U^{m}}$ for $U^{m}\otimes I^{n-m}$. Similarly, we write $\overline{\pi^{m}}$ when we apply this measurement operator to $\rho^{n}$ for $\{\pi_{0}\otimes I^{n-m},\dots,\pi_{2^{m}-1}\otimes I^{n-m}\}$. If the unitary $U^{m}$ needs to be applied, for example, to the last $m$ qubits of $\rho^{n}$ instead of the first $m$, we will need to use the unitary transformation $I^{n-m}\otimes U^{m}$ instead. And if it is applied to the qubits $k$ to $k+m$, then, we can use $\overline{I^{k-1}\otimes U^{m}}$.

This rewrite system assumes that after a measurement, the result is known. However, since we are working with density matrices we could also provide an alternative rewrite system where after a measurement, the system turns into a mixed state. We left this possibility for Section 3.

The type system, including the grammar of types and the derivation rules, is given in Table 3. The type system is affine, so variables can be used at most once, forbiding from cloning a density matrix.

Example 1

The teleportation algorithm, while it is better described by pure states, can be expressed in the following way:

Let $\beta_{00}=\frac{1}{2}(|00\rangle\langle 00|+|00\rangle\langle 11|+|11\rangle\langle 00|+|11\rangle\langle 11|)$. Then, the following term expresses the teleportation algorithm.

[TABLE]

where $\mathsf{Z}_{3}=I\otimes I\otimes\mathsf{Z}^{1}$ and $\mathsf{X}_{3}=I\otimes I\otimes\mathsf{X}^{1}$.

The type derivation is as follows.

[TABLE]

2.2 Interpretation

We give two interpretations for terms. One, noted by $\llparenthesis\cdot\rrparenthesis$, is the interpretation of terms into density matrices and functions upon them, and the other, noted by $\llbracket\cdot\rrbracket$, is a more fine-grained interpretation, interpreting terms into a generalisation of mixed states. In particular, we want $\llbracket\pi^{n}\rho^{n}\rrbracket\!=\!\{(\mathsf{tr}(\pi_{i}^{\dagger}\pi_{i}\rho^{n}),\frac{\pi_{i}\rho^{n}\pi_{i}^{\dagger}}{\mathsf{tr}(\pi_{i}^{\dagger}\pi_{i}\rho^{n})})\}_{i}$, while $\llparenthesis\pi^{n}\rho\rrparenthesis=\sum_{i}\pi_{i}\rho^{n}\pi_{i}^{\dagger}$. However, since the $\mathsf{letcase}$ construction needs also to distinguish each possible result of a measurement, we will carry those results in the interpretation $\llbracket\cdot\rrbracket$, making it a set of triplets instead of a set of tuples.

Let $\mathbb{N}^{\varepsilon}=\mathbb{N}_{0}\cup\{\varepsilon\}$, so terms are interpreted into sets of triplets $(p,b,e)$ with $p\in\mathbb{R}_{+}^{\leq 1}$, representing the probability, $b\in\mathbb{N}^{\varepsilon}$, representing the output of a measurement if it occurred, and $e\in\llbracket A\rrbracket$ for some type $A$ and an interpretation $\llbracket\cdot\rrbracket$ on types yet to define. In addition, we consider that the sets $\{\dots,(p,b,e),(q,b,e),\dots\}$ and $\{\dots,(p+q,b,e),\dots\}$ are equal. Finally, we define the weight function as $\mathsf{w}{(\{(p_{i},b_{i},e_{i})\}_{i})}=\sum_{i}p_{i}$. We are interested in sets $S$ such that $\mathsf{w}{(S)}=1$.

The interpretation of types is given in Table 4. $\mathcal{D}_{n}$ is the set of density matrices of $n$-qubits, that is $\mathcal{D}_{n}=\{\rho\mid\rho\in\mathcal{M}^{+}_{2^{n}\times 2^{n}}\textrm{ such that }\mathsf{tr}(\rho)=1\}$, where $\mathcal{M}^{+}_{2^{n}\times 2^{n}}$ is the set of positive matrices of size $2^{n}\times 2^{n}$. $P(b,A)$ is the following property: $[A=(m,n)\implies b\neq\varepsilon]$. We also establish the convention that $P(\{(p_{i},b_{i},e_{i})\}_{i},A)=\bigwedge_{i}P(b_{i},A)$. Finally, we write $\mathsf{trd}({S})=\{e\mid(p,b,e)\in S\}$.

Let $E=\bigcup_{A\in\mathsf{Types}}\llbracket A\rrbracket$. We denote by $\theta$ to a valuation $\mathsf{Vars}\to\mathbb{N}^{\varepsilon}\times E$. Then, we define the interpretation of terms with respect to a given valuation $\theta$ in Table 5.

Definition 1

$\theta\vDash\Gamma$ if and only if, for all $x:A\in\Gamma$, $\theta(x)=(b,e)$ with $e\in\llbracket A\rrbracket$, and $P(b,A)$.

Lemma 1 states that a term with type $(m,n)$ will be the result of a measurement, and hence, its interpretation will carry the results $b_{i}\neq\varepsilon$.

Lemma 1

Let $\Gamma\vdash t:(m,n)$, $\theta\vDash\Gamma$, and $\llbracket t\rrbracket_{\theta}$ be well-defined. Then, $\llbracket t\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$ with $b_{i}\neq\varepsilon$ and $e_{i}\in\mathcal{D}_{n}$.

Proof

By induction on the type derivation (cf. Appendix 0.A.1).∎

Lemma 2 states that the interpretation of a typed term is well-defined.

Lemma 2

If $\Gamma\vdash t:A$ and $\theta\vDash\Gamma$, then $\mathsf{w}{(\llbracket t\rrbracket_{\theta})}=1$, and $\mathsf{trd}({\llbracket t\rrbracket_{\theta}})\subseteq\llbracket A\rrbracket$.

Proof

By induction on $t$ (cf. Appendix 0.A.2).∎

Since the interpretation $\llbracket\cdot\rrbracket$ of a term is morally a mixed state, the interpretation $\llparenthesis\cdot\rrparenthesis$, which should be the density matrix of such a state, is naturally defined using the interpretation $\llbracket\cdot\rrbracket$.

Definition 2

Let $e\in\llbracket A\rrbracket$ for some $A$, $\theta$ a valuation, and $t$ be a term such that $\llbracket t\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$. We state the convention that $(\mathsf{b},\mathsf{e})\mapsto\sum_{i}p_{i}e_{i}=\sum_{i}p_{i}((\mathsf{b},\mathsf{e})\mapsto e_{i})$. We define $\left[{e}\right]$ and $\llparenthesis t\rrparenthesis_{\theta}$ by mutual recursion as follows:

[TABLE]

Lemma 3 (Substitution)

Let $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$, then

[TABLE]

Proof

By induction on $t$. However, we enforce the hypothesis by also showing that if $\llbracket t\rrbracket_{\theta,x=(b_{i},e_{i})}\!=\!\{(q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{j}$, then $\llbracket t[r/x]\rrbracket_{\theta}\!=\!\{(p_{i}q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{ij}$. We use five auxiliary results (cf. Appendix 0.A.3).∎

Theorem 2.1 shows how the interpretation $\llparenthesis\cdot\rrparenthesis$ of a term relates to all its reducts.

Theorem 2.1

If $\Gamma\vdash t:A$, $\theta\vDash\Gamma$ and $t\longrightarrow_{p_{i}}r_{i}$, with $\sum_{i}p_{i}=1$, then $\llparenthesis t\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis r_{i}\rrparenthesis_{\theta}$.

Proof

By induction on the relation $\longrightarrow_{p}$ (cf. Appendix 0.A.4).∎

3 Probabilistic-control calculus with no-probabilistic

rewriting

3.1 Definitions

In the previous sections we have presented an extension to lambda calculus to handle density matrices. The calculus could have been done using just vectors, because the output of a measurement is not given by the density matrix of the produced mixed state, instead each possible output is given with its probability. In this section, we give an alternative presentation, named $\lambda_{\rho}^{\circ}$, where we can make the most of the density matrices setting.

In Table 6 we give a modified grammar of terms for $\lambda_{\rho}^{\circ}$ in order to allow for linear combination of terms. We follow the grammar of the algebraic lambda-calculi [6, 7, 23].

The new rewrite system is given by the non-probabilistic relation $\rightsquigarrow$, described in Table 7. The measurement does not reduce, unless it is the parameter of a $\mathsf{letcase}^{\circ}$. Therefore, if only a measurement is needed, we can encode it as:

[TABLE]

where $\rho^{\prime}=\sum_{i}\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}$. The rationale is that in this version of the calculus, we can never look at the result of a measurement. It will always produce the density matrix of a mixed-state. As a consequence, the $\mathsf{letcase}^{\circ}$ constructor rewrites to a sum of terms.

The type system for $\lambda_{\rho}^{\circ}$, including the grammar of types and the derivation rules, is given in Table 8. The only difference with the type system of $\lambda_{\rho}$ (cf. Table 3), is that rule $\mathsf{ax}_{\mathsf{am}}$ is no longer needed, since $(b^{m},\rho^{n})$ is not in the grammar of $\lambda_{\rho}^{\circ}$, and there is a new rule ($+$) typing the generalised mixed states. We use the symbol $\Vdash$ for $\lambda_{\rho}^{\circ}$ to distinguish it from $\vdash$ used in $\lambda_{\rho}$.

Example 2

The teleportation algorithm expressed in $\lambda_{\rho}$ in Example 1, is analogous for $\lambda_{\rho}^{\circ}$, only changing the term $\mathsf{letcase}$ by $\mathsf{letcase}^{\circ}$. Also, the type derivation is analogous. The difference is in the reduction. Let $\rho$ be the density matrix of a given quantum state (mixed or pure). Let

[TABLE]

The trace of the teleportation of $\rho$ in $\lambda_{\rho}$ is the following:

[TABLE]

From (1), there are four possible reductions. For $i=0,1,2,3$, let $p_{i}=\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho^{3}_{2})$ and $\rho^{3}_{3i}=\frac{\overline{\pi_{i}}\rho^{3}_{2}\overline{\pi_{i}}^{\dagger}}{p_{i}}$. Then,

• •

$\eqref{eq:last}\longrightarrow_{p_{0}}\mathsf{letcase}\ y=(0,\rho^{3}_{30})\ \mathsf{in}\ \{y,\mathsf{Z}_{3}y,\mathsf{X}_{3}y,\mathsf{Z}_{3}\mathsf{X}_{3}y\}\longrightarrow_{1}\rho^{3}_{30}=\rho$.

• •

$\eqref{eq:last}\longrightarrow_{p_{1}}\mathsf{letcase}\ y=(1,\rho^{3}_{31})\ \mathsf{in}\ \{y,\mathsf{Z}_{3}y,\mathsf{X}_{3}y,\mathsf{Z}_{3}\mathsf{X}_{3}y\}\longrightarrow_{1}\mathsf{Z}_{3}\rho^{3}_{31}\longrightarrow_{1}\rho$.

• •

$\eqref{eq:last}\longrightarrow_{p_{2}}\mathsf{letcase}\ y=(2,\rho^{3}_{32})\ \mathsf{in}\ \{y,\mathsf{Z}_{3}y,\mathsf{X}_{3}y,\mathsf{Z}_{3}\mathsf{X}_{3}y\}\longrightarrow_{1}\mathsf{X}_{3}\rho^{3}_{32}\longrightarrow_{1}\rho$.

• •

$\eqref{eq:last}\longrightarrow_{p_{3}}\mathsf{letcase}\ y=(3,\rho^{3}_{33})\ \mathsf{in}\ \{y,\mathsf{Z}_{3}y,\mathsf{X}_{3}y,\mathsf{Z}_{3}\mathsf{X}_{3}y\}\longrightarrow_{1}\mathsf{Z}_{3}\mathsf{X}_{3}\rho^{3}_{33}\longrightarrow_{1}\rho$.

On the other hand, the trace of the same term, in $\lambda_{\rho}^{\circ}$, would be analogous until (1), just using $\rightsquigarrow$ instead of $\longrightarrow_{1}$. Then:

[TABLE]

3.2 Interpretation

The interpretation of $\lambda_{\rho}$ given in Section 2.2 considers already all the traces. Hence, the interpretation of $\lambda_{\rho}^{\circ}$ can be obtained from a small modification of it. We only need to drop the interpretation of the term that no longer exists, $(b^{m},\rho^{n})$, and add an interpretation for the new term $\sum_{i}p_{i}t_{i}$ as follows:

[TABLE]

The interpretation of $\mathsf{letcase}^{\circ}$ is the same as the interpretation of $\mathsf{letcase}$.

Then, we can prove a theorem (Theorem 3.1) for $\lambda_{\rho}^{\circ}$ analogous to Theorem 2.1.

We need the following auxiliary Lemmas.

Lemma 4

If $\Gamma\Vdash t:A$ and $\theta\vDash\Gamma$, then $\llparenthesis\sum_{i}p_{i}t_{i}\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis t_{i}\rrparenthesis_{\theta}$

Proof

Let $\llbracket t_{i}\rrbracket_{\theta}=\{(q_{ij},b_{ij},e_{ij})\}_{j}$. Then, we have $\llparenthesis\sum_{i}p_{i}t_{i}\rrparenthesis_{\theta}=\sum_{ij}p_{i}q_{ij}e_{ij}=\sum_{i}p_{i}\sum_{j}q_{ij}e_{ij}=\sum_{i}p_{i}\llparenthesis t_{i}\rrparenthesis_{\theta}$. ∎

Lemma 5

Let $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$, then $\llparenthesis t[r/x]\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis t\rrparenthesis_{\theta,x=(b_{i},e_{i})}$.

Proof

The proof of the analogous Lemma 3 in $\lambda_{\rho}$ follows by induction on $t$. Since the definition of $\llbracket\cdot\rrbracket$ is the same for $\lambda_{\rho}$ than for $\lambda_{\rho}^{\circ}$, we only need to check the only term of $\lambda_{\rho}^{\circ}$ which is not a term of $\lambda_{\rho}$: $\sum_{j}q_{j}t_{j}$. Using Lemma 4, and the induction hypothesis, we have $\llparenthesis(\sum_{j}q_{j}t_{j})[r/x]\rrparenthesis_{\theta}=\llparenthesis\sum_{j}q_{j}(t_{j}[r/x])\rrparenthesis_{\theta}=\sum_{j}q_{j}\llparenthesis t_{j}[r/x]\rrparenthesis_{\theta}=\sum_{j}q_{j}\sum_{i}p_{i}\llparenthesis t_{j}\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{i}p_{i}\llparenthesis\sum_{j}q_{j}t_{j}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. ∎

Theorem 3.1

If $\Gamma\Vdash t:A$, $\theta\vDash\Gamma$ and $t\rightsquigarrow r$, then $\llparenthesis t\rrparenthesis_{\theta}=\llparenthesis r\rrparenthesis_{\theta}$.

Proof

By induction on the relation $\rightsquigarrow$. Rules $(\lambda x.t)r\rightsquigarrow t[r/x]$, $U^{m}\rho^{n}\rightsquigarrow\rho^{\prime}$ and $\rho\otimes\rho^{\prime}\rightsquigarrow\rho^{\prime\prime}$ are also valid rules for relation $\longrightarrow_{1}$, and hence the proof of these cases are the same than in Theorem 2.1. ∎

4 Subject Reduction and Progress

In this section we state and prove the subject reduction and progress properties on both, $\lambda_{\rho}$ and $\lambda_{\rho}^{\circ}$ (Theorems 4.1 and 4.2 respectively).

Lemma 6 (Weakening)

• •

If $\Gamma\vdash t:A$ and $x\notin FV(t)$, then $\Gamma,x:B\vdash t:A$.

• •

If $\Gamma\Vdash t:A$ and $x\notin FV(t)$, then $\Gamma,x:B\Vdash t:A$.

Proof

By a straightforward induction on the derivation of $\Gamma\vdash t:A$ and on $\Gamma\Vdash t:A$.∎

Lemma 7 (Strengthening)

• •

If $\Gamma,x:A\vdash t:B$ and $x\notin FV(t)$, then $\Gamma\vdash t:B$.

• •

If $\Gamma,x:A\Vdash t:B$ and $x\notin FV(t)$, then $\Gamma\Vdash t:B$.

Proof

By a straightforward induction on the derivation of $\Gamma,x:A\vdash t:B$ and $\Gamma,x:A\Vdash t:B$.∎

Lemma 8 (Substitution)

• •

If $\Gamma,x:A\vdash t:B$ and $\Delta\vdash r:A$ then $\Gamma,\Delta\vdash t[r/x]:B$.

• •

If $\Gamma,x:A\Vdash t:B$ and $\Delta\Vdash r:A$ then $\Gamma,\Delta\Vdash t[r/x]:B$.

Proof

By induction on $t$ (cf. Appendix 0.C.1). ∎

Theorem 4.1 (Subject reduction)

• •

If $\Gamma\vdash t:A$, and $t\longrightarrow_{p}r$, then $\Gamma\vdash r:A$.

• •

If $\Gamma\Vdash t:A$, and $t\rightsquigarrow r$, then $\Gamma\Vdash r:A$.

Proof

By induction on the relations $\longrightarrow_{p}$ and $\rightsquigarrow$ (cf. Appendix 0.C.2). ∎

Definition 3 (Values)

• •

A value in $\lambda_{\rho}$ is a term $v$ defined by the following grammar:

[TABLE]

• •

A value in $\lambda_{\rho}^{\circ}$ (or value∘) is a term $v$ defined by the following grammar:

[TABLE]

Lemma 9

If $v$ is a value, then there is no $t$ such that $v\longrightarrow_{p}t$ for any $p$. 2. 2.

If $v$ is a value∘, then there is no $t$ such that $v\rightsquigarrow t$.

Proof

By induction on $v$ in both cases (cf. Appendix 0.C.3).∎

Theorem 4.2 (Progress)

If $\vdash t:A$, then either $t$ is a value or there exist $n$, $p_{1},\dots,p_{n}$, and $r_{1},\dots,r_{n}$ such that $t\longrightarrow_{p_{i}}r_{i}$. 2. 2.

If $\Vdash t:A$ and $A\neq(m,n)$, then either $t$ is a value∘* or there exists $r$ such that $t\rightsquigarrow r$.*

Proof

We relax the hypotheses and prove the theorem for open terms as well. That is:

If $\Gamma\vdash t:A$, then either $t$ is a value, there exist $n$, $p_{1},\dots,p_{n}$, and $r_{1},\dots,r_{n}$ such that $t\longrightarrow_{p_{i}}r_{i}$, or $t$ contains a free variable, and $t$ does not rewrite. 2. 2.

If $\Gamma\Vdash t:A$, then either $t$ is a value∘, there exists $r$ such that $t\rightsquigarrow r$, or $t$ contains a free variable, and $t$ does not rewrite.

In both cases, we proceed by induction on the type derivation (cf. Appendix 0.C.4).∎

5 Examples

Example 3

Consider the following experiment: Measure some $\rho$ and then toss a coin to decide whether to return the result of the measurement, or to give the result of tossing a new coin.

The experiment in $\lambda_{\rho}$.

This experiment can be implemented in $\lambda_{\rho}$ as follows:

[TABLE]

Trace:

We give one possible probabilistic trace. Notice that, by using different strategies, we would get different derivation trees. We will not prove confluence in this setting (cf. [11] for a full discussion on the notion of confluence of probabilistic rewrite systems), but we conjecture that such a property is meet.

We use the following notations:

[TABLE]

Using this notation, the probabilistic trace is given by the tree in Table 9. Therefore, with probability $\frac{5}{8}$ we get $|0\rangle\langle 0|$, and with probability $\frac{3}{8}$ we get $|1\rangle\langle 1|$. Thus, the density matrix of this mixed state is $\frac{5}{8}|0\rangle\langle 0|+\frac{3}{8}|1\rangle\langle 1|$.

Typing:

[TABLE]

[TABLE]

[TABLE]

Interpretation:

[TABLE]

Then,

[TABLE]

Hence,

[TABLE]

The experiment in $\lambda_{\rho}^{\circ}$.

In $\lambda_{\rho}^{\circ}$, the example becomes:

[TABLE]

Trace:

In this case the trace is not a tree, because the relation $\rightsquigarrow$ is not probabilistic. We use the same $\rho$ as before: $\frac{3}{4}|0\rangle\langle 0|+\frac{\sqrt{3}}{4}|1\rangle\langle 0|+\frac{\sqrt{3}}{4}|0\rangle\langle 1|+\frac{1}{4}|1\rangle\langle 1|$.

[TABLE]

Typing and Interpretation:

Since $t$ does not contain sums, its typing is analogous to the term in $\lambda_{\rho}$, as well as the interpretation.

Example 4

In [17, p 371] there is an example of the freedom in the operator-sum representation by showing two quantum operators, which are actually the same. One is the process of tossing a coin and, according to its results, applying $I$ or $Z$ to a given qubit The second is the process performing a projective measurement with unknown outcome to the same qubit. These operations can be encoded in $\lambda_{\rho}$ by:

[TABLE]

with $\pi^{1}=\{|0\rangle\langle 0|,|1\rangle\langle 1|\}$.

Let us apply those operators to the qubit $\rho=\frac{3}{4}|0\rangle\langle 0|+\frac{\sqrt{3}}{4}|0\rangle\langle 1|+\frac{\sqrt{3}}{4}|1\rangle\langle 0|+\frac{1}{4}|1\rangle\langle 1|$. We can check that the terms $O_{1}\rho$ and $O_{2}\rho$ have different interpretations $\llbracket\cdot\rrbracket$. Let $\rho^{-}=\mathsf{Z}\rho\mathsf{Z}^{\dagger}$, then

[TABLE]

However, they have the same interpretation $\llparenthesis\cdot\rrparenthesis$.

[TABLE]

The trace of $O_{1}\rho$ is given in Table 10, and the trace of $O_{2}\rho$ in Table 11.

The first term produces $\rho$, with probability $\frac{1}{2}$, and $\rho^{-}$, with probability $\frac{1}{2}$, while the second term produces either $|0\rangle\langle 0|$ with probability $\frac{3}{4}$ or $|1\rangle\langle 1|$, with probability $\frac{1}{4}$.

However, if we encode the same terms in $\lambda_{\rho}^{\circ}$, we can get both programs to produce the same density matrix:

[TABLE]

The traces of $O^{\circ}_{1}\rho$ and $O^{\circ}_{2}\rho$ are as follow:

[TABLE]

6 Conclusions

In this paper we have presented the calculus $\lambda_{\rho}$, which is a quantum data / classical control extension to the lambda calculus where the data is manipulated by density matrices. The main importance of this calculus is its interpretation into density matrices, which can equate programs producing the same density matrices. Then, we have given a second calculus, $\lambda_{\rho}^{\circ}$, where the density matrices are generalised to accommodate arbitrary terms, and so, programs producing the same density matrices, rewrite to such a matrix, thus, coming closer to its interpretation. The control of $\lambda_{\rho}^{\circ}$ is not classical nor quantum, however it can be seen as a weaker version of the quantum control approach. It is indeed not classical control because a generalised density matrix of terms is allowed ($\sum_{i}p_{i}t_{i}$). It is not quantum control because superposition of programs are not allowed (indeed, the previous sum is not a quantum superposition since all the $p_{i}$ are positive and so no interference can occur). However, it is quantum in the sense that programs in a kind of generalised mixed-states are considered. We preferred to call it probabilistic control.

As depicted in Example 4, the calculus $\lambda_{\rho}^{\circ}$ allows to represent the same operator in different ways. Understanding when two operators are equivalent is important from a physical point of view: it gives insights on when two different physical processes produce the same dynamics. To the best of our knowledge, it is the first lambda calculus for density matrices.

Future work and open questions

As pointed out by Bǎdescu and Panangaden [8], one of the biggest issues with quantum control is that it does not accommodate well with traditional features from functional programming languages like recursion. Ying [25] went around this problem by introducing a recursion based on second quantisation. Density matrices are DCPOs with respect to the Löwner order. Is the form of weakened quantum control suggested in this paper monotone? Can it be extended with recursion? Could this lead to a concrete quantum programming language, like Quipper [15]?

All these open questions are promising new lines of research that we are willing to follow. In particular, we have four ongoing works trying to answer some of these questions:

• •

The most well studied quantum lambda calculus is, without doubt, Selinger-Valiron’s $\lambda_{q}$ [21]. Hence, we are working on the mutual simulations between $\lambda_{\rho}$ and $\lambda_{q}$, and between $\lambda_{\rho}^{\circ}$ and a generalisation of $\lambda_{q}$ into mixed states.

• •

We are also working on a first prototype of an implementation of $\lambda_{\rho}^{\circ}$.

• •

We are studying extensions to both $\lambda_{\rho}$ and $\lambda_{\rho}^{\circ}$ with recursion and with polymorphism.

• •

Finally, we are studying a more sophisticated denotational semantics for both calculi than the one given in this paper. We hope such a semantics to be adequate and fully abstract.

Acknowledgements

We want to thank the anonymous reviewer for some important references and suggestions on future lines of work.

Appendix 0.A Detailed Proofs of Section 2.2

0.A.1 Proof of Lemma 1

By induction on the type derivation.

• •

Let $\Gamma,x:(m,n)\vdash x:(m,n)$ as a consequence of rule $\mathsf{ax}$. Since $\theta\vDash\Gamma,x:(m,n)$, we have $\theta(x)=(b,e)$ with $e\in\mathcal{D}_{n}$ and $b\neq\varepsilon$. Hence, $\llbracket x\rrbracket_{\theta}=\{(1,b,e)\}$.

• •

Let $\Gamma,\Delta\vdash tr:(m,n)$ as a consequence of $\Gamma\vdash t:\vec{A}\multimap(m,n)$, $\Delta\vdash r:A$ and rule $\multimap_{e}$. Since $\theta\vDash\Gamma,\Delta$, we have $\theta\vDash\Gamma$. Since $\llbracket tr\rrbracket_{\theta}$ is well-defined, we have $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$, $\llbracket t\rrbracket_{\theta}=\{(q_{j},b^{\prime}_{j},f_{j})\}_{i}$, and $f_{j}(b_{i},e_{i})=\{(h_{ijk},b_{ijk}^{\prime\prime},g_{ijk})\}_{k}$, and hence $\llbracket tr\rrbracket_{\theta}=\{(p_{i}q_{j}h_{ijk},b^{\prime\prime}_{ijk},g_{ijk})\}_{ijk}$. By the induction hypothesis, $f_{i}\in\llbracket\vec{A}\multimap(m,n)\rrbracket$, so, by definition, $b_{ijk}^{\prime\prime}\neq\varepsilon$ and $g_{ijk}\in\mathcal{D}_{n}$.

• •

Let $\Gamma\vdash\pi^{m}t:(m,n)$ as a consequence of $\Gamma\vdash t:n$ and rule $\mathsf{m}$. Then we have that $\llbracket\pi^{m}t\rrbracket_{\theta}$ is equal to $\{p_{j}\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho_{j}),i,\frac{\overline{\pi_{i}}\rho_{j}\overline{\pi_{i}}^{\dagger}}{\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho_{j})}\mid\llbracket t\rrbracket_{\theta}=\{(p_{j},\varepsilon,\rho_{j})\}_{j}\}$, with $i\neq\varepsilon$. Notice that $\frac{\overline{\pi_{i}}\rho_{j}\overline{\pi_{i}}^{\dagger}}{\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho_{j})}\in\mathcal{D}_{n}$.

• •

Let $\Gamma\vdash(b^{m},\rho^{n}):(m,n)$ as a consequence of rule $\mathsf{ax}_{\mathsf{am}}$. Then, $\llbracket(b^{m},\rho^{n})\rrbracket_{\theta}=\{(1,b^{m},\rho^{n})\}$. Notice that $\rho^{n}\in\mathcal{D}_{n}$.

• •

Let $\Gamma\vdash\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m^{\prime}}-1}\}:(m,n)$ as a consequence of $x:n^{\prime}\vdash t_{k}:(m,n)$, for $k=0,\dots,2^{m^{\prime}}-1$, $\Gamma\vdash r:(m^{\prime},n^{\prime})$ and rule $\mathsf{lc}$. Since $\llbracket\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m^{\prime}}-1}\}\rrbracket_{\theta}$ is well-defined, $\llbracket r\rrbracket_{\theta}\!=\{(p_{i},b_{i},\rho_{i}^{n})\}_{i}$, $\llbracket t_{i}\rrbracket_{\theta,x=(\varepsilon,\rho_{i}^{n})}=\{(q_{ij},b_{ij}^{\prime},e_{ij})\}_{j}$ and $\llbracket\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m^{\prime}}-1}\}\rrbracket_{\theta}\!=\!\{(p_{i}q_{ij},b_{ij}^{\prime},e_{ij})\}_{ij}$. By the induction hypothesis, $b_{ij}^{\prime}\neq\varepsilon$ and $e_{ij}\in\mathcal{D}_{n}$. ∎

0.A.2 Proof of Lemma 2

By induction on $t$.

• •

Let $t=x$. Then $x:A\in\Gamma$. $\llbracket x\rrbracket_{\theta}=\{(1,b,e)\}$, with $\theta(x)=(b,e)$. Since $\theta\vDash\Gamma$ we have $e\in\llbracket A\rrbracket$.

• •

Let $t=\lambda x.r$. Then $A=B\multimap C$, $\Gamma,x:B\vdash r:C$ and $\llbracket\lambda x.r\rrbracket_{\theta}=\{(1,\varepsilon,(\mathsf{b},\mathsf{e})\mapsto\llbracket r\rrbracket_{\theta,x=(\mathsf{b},\mathsf{e})})\}$. Let $e\in\llbracket B\rrbracket$ and $b\in\mathbb{N}^{\varepsilon}$ such that $P(b,B)$. Then, since $\theta\vDash\Gamma$, we have $\theta,x=(b,e)\vDash\Gamma,x:B$. Hence, by the induction hypothesis, $\mathsf{trd}({\llbracket r\rrbracket_{\theta,x=(b,e)}})\subseteq\llbracket C\rrbracket$. Therefore, $(\mathsf{b},\mathsf{e})\mapsto\llbracket r\rrbracket_{\theta,x=(\mathsf{b},\mathsf{e})}\in\llbracket B\multimap C\rrbracket$.

• •

Let $t=rs$. Then $\Gamma=\Gamma_{1},\Gamma_{2}$, with $\Gamma_{1}\vdash r:B\multimap A$ and $\Gamma_{2}\vdash s:B$. Since $\theta\vDash\Gamma$, we have $\theta\vDash\Gamma_{1}$ and $\theta\vDash\Gamma_{2}$, so by the induction hypothesis, $\llbracket s\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$, $\sum_{i}p_{i}=1$ and $e_{i}\in\llbracket B\rrbracket$. Similarly, $\llbracket r\rrbracket_{\theta}=\{(q_{j},b^{\prime}_{j},f_{j})\}_{j}$, $\sum_{j}q_{j}=1$ and $f_{j}\in\llbracket B\multimap A\rrbracket$. Let $f_{j}(b_{i},e_{i})=\{(h_{ijk},b_{ijk}^{\prime\prime},g_{ijk})\}_{k}$. Then, $\llbracket rs\rrbracket_{\theta}=\{(p_{i}q_{j}h_{ijk},b_{ijk}^{\prime\prime},g_{ijk})\}_{ijk}$. By Lemma 1, we have $P(b,B)$, so by definition of $\llbracket B\multimap A\rrbracket$, we have $\{g_{ijk}\}=\mathsf{trd}({f_{j}(b_{i},e_{i})})\subseteq\llbracket A\rrbracket$ and $\mathsf{w}{(f_{j}(b_{i},e_{i}))}=1$. Notice that $\sum_{ijk}p_{i}q_{j}h_{ijk}=\sum_{i}p_{i}\sum_{j}q_{j}\sum_{k}h_{ijk}=1$.

• •

Let $t=\rho^{n}$. Then $A=n$ and $\llbracket\rho^{n}\rrbracket_{\theta}=\{(1,\varepsilon,\rho^{n})\}$. Notice that $\rho^{n}\in\mathcal{D}_{n}=\llbracket A\rrbracket$.

• •

Let $t=U^{m}r$. Then $A=n$ and $\Gamma\vdash r:n$. By the induction hypothesis, $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},\rho^{n}_{i})\}_{i}$, with $\sum_{i}p_{i}=1$ and $\rho^{n}_{i}\in\mathcal{D}_{n}$. Then, $\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger}\in\mathcal{D}_{n}=\llbracket A\rrbracket$, and $\llbracket U^{m}r\rrbracket_{\theta}=\{(p_{i},\varepsilon,\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger})\}$.

• •

Let $t=\pi^{m}r$. Then $A=(m,n)$ and $\Gamma\vdash r:n$. By the induction hypothesis, $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},\rho^{n}_{i})\}_{i}$, with $\sum_{i}p_{i}=1$ and $\rho^{n}_{i}\in\mathcal{D}_{n}$. Let $\pi^{m}=\{\pi_{j}\}_{j}$, and $q_{ij}=\mathsf{tr}(\overline{\pi_{j}}^{\dagger}\overline{\pi_{j}}\rho^{n}_{i})$. So,$\sum_{j}q_{ij}=1$. Let $\rho^{n}_{ij}=\frac{\overline{\pi_{j}}\rho^{n}_{i}\overline{\pi_{j}}^{\dagger}}{q_{ij}}\in\mathcal{D}_{n}=\llbracket(m,n)\rrbracket$. Then, we have $\llbracket\pi^{m}r\rrbracket_{\theta}=\{(p_{i}q_{ij},j,\rho^{n}_{ij})\}_{ij}$. Notice that $\sum_{ij}p_{i}q_{ij}=\sum_{i}p_{i}\sum_{j}q_{ij}=1$.

• •

Let $t=r\otimes s$. Then $A=n+m$ and $\Gamma=\Gamma_{1},\Gamma_{2}$, with $\Gamma_{1}\vdash r:n$ and $\Gamma_{2}\vdash s:m$. Since $\theta\vDash\Gamma$, we have $\theta\vDash\Gamma_{1}$ and $\theta\vDash\Gamma_{2}$. Then, by the induction hypothesis, $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},\rho^{n}_{i})\}_{i}$, with $\sum_{i}p_{i}=1$ and $\rho^{n}_{i}\in\mathcal{D}_{n}$. Similarly, $\llbracket s\rrbracket_{\theta}=\{(q_{j},b^{\prime}_{j},\rho^{m}_{j})\}_{j}$, with $\sum_{j}q_{j}=1$ and $\rho^{m}_{j}\in\mathcal{D}_{m}$. Hence, $\llbracket r\otimes s\rrbracket_{\theta}=\{(p_{i}q_{j},\varepsilon,\rho^{n}_{i}\otimes\rho^{m}_{j})\}_{ij}$. Notice that $\rho^{n}_{i}\otimes\rho^{m}_{j}\in\mathcal{D}_{n+m}$, and $\sum_{ij}p_{i}q_{j}=\sum_{i}p_{i}\sum_{j}q_{j}=1$.

• •

Let $t=(b^{m},\rho^{n})$. Then $A=(m,n)$ and $\llbracket(b^{m},\rho^{n})\rrbracket_{\theta}=\{(1,b^{m},\rho^{n})\}$, with $\rho^{n}\in\mathcal{D}_{n}=\llbracket A\rrbracket$.

• •

Let $t=\mathsf{letcase}\ x=r\ \mathsf{in}\ \{s_{0},\dots,s_{2^{m}-1}\}$. Then, $x:n\vdash s_{k}:A$, for $k=0,\dots,2^{m}-1$, and $\Gamma\vdash r:(m,n)$. Hence, by the induction hypothesis, $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},\rho_{i}^{n})\}_{i}$ with $\rho_{i}^{n}\in\mathcal{D}_{n}$ and $\sum_{i}p_{i}=1$. By Lemma 1, $b_{i}\neq\varepsilon$, so $\theta,x=(\varepsilon,\rho_{i}^{n})\vDash x:n$ and hence, by the induction hypothesis, $\llbracket s_{b_{i}}\rrbracket_{\theta,x=(\varepsilon,\rho_{i}^{n})}=\{(q_{ij},b_{ij}^{\prime},e_{ij})\}_{j}$, with $\sum_{j}q_{ij}=1$ and $e_{ij}\in\llbracket A\rrbracket$. Hence, $\llbracket\mathsf{letcase}\ x=r\ \mathsf{in}\ \{s_{0},\dots,s_{2^{m}-1}\}\rrbracket_{\theta}=\{(p_{i}q_{ij},b_{ij}^{\prime},e_{ij})\}_{ij}$. Notice that i $\sum_{ij}p_{i}q_{ij}=\sum_{i}p_{i}\sum_{j}q_{ij}=1$. ∎

0.A.3 Proof of

Lemma 3

We need the next four lemmas and the corollary as auxiliary results.

Lemma 10

If $\Gamma\vdash t:A\multimap B$ and $\theta\vDash\Gamma$, then we have $\llparenthesis t\rrparenthesis_{\theta}=\sum_{i}p_{i}((\mathsf{b},\mathsf{e})\mapsto\llparenthesis r_{i}\rrparenthesis_{\theta,x=(\mathsf{b},\mathsf{e})})$. ∎

Lemma 11

If $\llparenthesis t\rrparenthesis_{\theta}=\sum_{i}p_{i}((\mathsf{b},\mathsf{e})\mapsto\llparenthesis r_{i}\rrparenthesis_{\theta^{\prime},x=(\mathsf{b},\mathsf{e})})$ and $\llbracket s\rrbracket_{\theta}=\{(q_{j},b_{j},e_{j})\}_{j}$, then we have $\llparenthesis ts\rrparenthesis_{\theta}=\sum_{ij}p_{i}q_{j}\llparenthesis r_{i}\rrparenthesis_{\theta^{\prime},x=(b_{j},e_{j})}$ ∎

Corollary 1

If $\llparenthesis t\rrparenthesis_{\theta}\!=\sum_{i}p_{i}((\mathsf{b},\mathsf{e})\mapsto\llparenthesis r_{i}\rrparenthesis_{\theta^{\prime},x=(\mathsf{b},\mathsf{e})})$ and $\llparenthesis s\rrparenthesis_{\theta}=\sum_{j}q_{j}e_{j}$, then $\llparenthesis ts\rrparenthesis_{\theta}\!=\sum_{ij}p_{i}q_{j}\llparenthesis r_{i}\rrparenthesis_{\theta^{\prime},x=(\varepsilon,e_{j})}$ ∎

Lemma 12

If $\Gamma\vdash t:n$ and $\theta\vDash\Gamma$, then $\llparenthesis U^{m}t\rrparenthesis_{\theta}=\overline{U^{m}}\llparenthesis t\rrparenthesis_{\theta}\overline{U^{m}}^{\dagger}$ and $\llparenthesis\pi^{m}t\rrparenthesis_{\theta}=\sum_{i}\overline{\pi_{i}}\llparenthesis t\rrparenthesis_{\theta}\overline{\pi_{i}}^{\dagger}$. ∎

Lemma 13

If $\Gamma\vdash t:n$, $\Delta\vdash r:m$ and $\theta\vDash\Gamma,\Delta$, then $\llparenthesis t\otimes r\rrparenthesis_{\theta}=\llparenthesis t\rrparenthesis_{\theta}\otimes\llparenthesis r\rrparenthesis_{\theta}$. ∎

Proof of Lemma 3.

We proceed by induction on $t$, however, we enforce the hypothesis by also showing that if $\llbracket t\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{j}$, then $\llbracket t[r/x]\rrbracket_{\theta}=\{(p_{i}q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{ij}$.

• •

Let $t=x$. $\llparenthesis x[r/x]\rrparenthesis_{\theta}=\llparenthesis r\rrparenthesis_{\theta}=\sum_{i}p_{i}[e_{i}]=\sum_{i}p_{i}\llparenthesis x\rrparenthesis_{\theta,x=(b_{i},e_{i})}$.

Notice that $\llbracket x\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(1,b_{i},e_{i})\}$ and $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$.

• •

Let $t=y$. Let $\theta(y)=(b^{\prime},f)$. Then, $\llparenthesis y[r/x]\rrparenthesis_{\theta}=\llparenthesis y\rrparenthesis_{\theta}=f=\llparenthesis y\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{i}p_{i}\llparenthesis y\rrparenthesis_{\theta,x=(b_{i},e_{i})}$.

Notice that $\llbracket y\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(1,b^{\prime},f)\}=\{(p_{i},b^{\prime},f^{\prime})\}_{i}=\llbracket y[r/x]\rrbracket_{\theta}$.

• •

Let $t=\lambda y.s$. Then, using the induction hypothesis, we have $\llparenthesis(\lambda y.s)[r/x]\rrparenthesis_{\theta}=\llparenthesis\lambda y.s[r/x]\rrparenthesis_{\theta}=\!(\mathsf{b},\mathsf{e})\!\mapsto\!\llparenthesis s[r/x]\rrparenthesis_{\theta,y=(\mathsf{b},\mathsf{e})}=\!(\mathsf{b},\mathsf{e})\!\mapsto\!\sum_{i}p_{i}\llparenthesis s\rrparenthesis_{\theta,y=(\mathsf{b},\mathsf{e}),x=(b_{i},e_{i})}=\sum_{i}p_{i}((\mathsf{b},\mathsf{e})\mapsto\llparenthesis s\rrparenthesis_{\theta,y=(\mathsf{b},\mathsf{e}),x=(b_{i},e_{i})})=\sum_{i}p_{i}\llparenthesis\lambda y.s\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Notice that $\lambda y.s$ cannot have type $n$ or $(m,n)$.

• •

Let $t=s_{1}s_{2}$

• –

Let $x\in FV(s_{1})$. By Lemma 10, we have $\llparenthesis s_{1}\rrparenthesis_{\theta,x=(b_{i},e_{i})}\!=\sum_{j}q_{ij}((\mathsf{b},\mathsf{e})\mapsto\llparenthesis s^{\prime}_{ij}\rrparenthesis_{\theta,x=(b_{i},e_{i}),y=(\mathsf{b},\mathsf{e})})$. Then, by the induction hypothesis, $\llparenthesis s_{1}[r/x]\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{1}\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{ij}p_{i}q_{ij}((\mathsf{b},\mathsf{e})\mapsto\llparenthesis s^{\prime}_{ij}\rrparenthesis_{\theta,x=(b_{i},e_{i}),y=(\mathsf{b},\mathsf{e})})$. Let $\llbracket s_{2}\rrbracket_{\theta}$ $=\{(h_{k},b^{\prime}_{k},f_{k})\}_{k}$. Hence, by Lemma 11, we have that $\llparenthesis s_{1}[r/x]s_{2}\rrparenthesis_{\theta}$ $=\sum_{ijk}p_{i}q_{ij}h_{k}\llparenthesis s^{\prime}_{ij}\rrparenthesis_{\theta,x=(b_{i},e_{i}),y=(b^{\prime}_{k},f_{k})}$. Since $x\notin FV(s_{2})$, we also have that $\llbracket s_{2}\rrbracket_{\theta,x=(b_{i},e_{i})}=\llbracket s_{2}\rrbracket_{\theta}$, so, also by Lemma 11, we have $\llparenthesis s_{1}s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{jk}q_{ij}h_{k}\llparenthesis s^{\prime}_{ij}\rrparenthesis_{\theta,x=(b_{i},e_{i}),y=(b^{\prime}_{k},f_{k})}$. Therefore, we have $\llparenthesis(s_{1}s_{2})[r/x]\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{1}s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Since $s^{\prime}_{ij}$ is smaller than $s_{1}$, the induction hypothesis applies, and so, if $\llbracket s^{\prime}_{ij}\rrbracket_{\theta,x=(b_{i},e_{i}),y=(b^{\prime}_{k},f_{k}))}=\{(q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{j}$, then $\llbracket s^{\prime}_{ij}[r/x]\rrbracket_{\theta,y=(b^{\prime}_{k},f_{k})}=\{(p_{i}q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{ij}$.

• –

Let $x\in FV(s_{s})$. By Lemma 10, we have $\llparenthesis s_{1}\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{j}q_{j}(\mathsf{b},\mathsf{e})\mapsto\llparenthesis s^{\prime}_{ij}\rrparenthesis_{\theta,x=(b_{i},e_{i}),y=(\mathsf{b},\mathsf{e})}$. By Corollary 1, we have that $\llparenthesis s_{1}s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{j}q_{j}\llparenthesis s^{\prime}_{ij}\rrparenthesis_{\theta,x=(b_{i},e_{i}),y=(\varepsilon,\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})})}$. By the induction hypothesis, we have $\llparenthesis s_{2}[r/x]\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Since $x\notin FV(s_{2}[r/x])$, we have $\llparenthesis s_{2}[r/x]\rrparenthesis_{\theta}=\llparenthesis s_{2}[r/x]\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Therefore, by Corollary 1, we have $\llparenthesis s_{1}s_{2}[r/x]\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{ij}p_{i}q_{j}\llparenthesis s_{ij}^{\prime}\rrparenthesis_{\theta,x=(b_{i},e_{i}),y=(\varepsilon,\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})})}$

$=\sum_{i}p_{i}\llparenthesis s_{1}s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Since $s^{\prime}_{ij}$ is smaller than $s_{1}$, the induction hypothesis applies, and therefore, if

$\llbracket s^{\prime}_{ij}\rrbracket_{\theta,x=(b_{i},e_{i}),y=(\varepsilon,\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})})}=\{(q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{j}$, then $\llbracket s^{\prime}_{ij}[r/x]\rrbracket_{\theta,y=(\varepsilon,\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})})}=\{(p_{i}q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{ij}$.

• •

Let $t=\rho^{n}$. $\llparenthesis\rho^{n}[r/x]\rrparenthesis_{\theta}=\llparenthesis\rho^{n}\rrparenthesis_{\theta}=\rho^{n}=\llparenthesis\rho^{n}\rrparenthesis_{\theta,x=(b_{i},e_{i})}=\sum_{i}p_{i}\llparenthesis\rho^{n}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. In addition, $\llbracket\rho^{n}\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(1,\varepsilon,\rho^{n})\}=\{(p_{i},\varepsilon,\rho^{n})\}_{i}=\llbracket\rho^{n}[r/x]\rrbracket_{\theta}$.

• •

Let $t=U^{m}s$. By the induction hypothesis, $\llparenthesis s[r/x]\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. By Lemma 12, $\llparenthesis U^{m}s[r/x]\rrparenthesis_{\theta}=\overline{U^{m}}\llparenthesis s[r/x]\rrparenthesis_{\theta}\overline{U^{m}}^{\dagger}=\overline{U^{m}}\sum_{i}p_{i}\llparenthesis s\rrparenthesis_{\theta,x=(b_{i},e_{i})}\overline{U^{m}}^{\dagger}$ $=\sum_{i}p_{i}\overline{U^{m}}\llparenthesis s\rrparenthesis_{\theta,x=(b_{i},e_{i})}\overline{U^{m}}^{\dagger}=\sum_{i}p_{i}\llparenthesis U^{m}s\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Let $\llbracket s\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij},b_{ij},\rho_{ij})\}_{j}$, then $\llbracket U^{m}s\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij},\varepsilon,\overline{U^{m}}\rho_{ij}\overline{U^{m}})\}_{j}$. In addition, by the induction hypothesis, we have $\llbracket s[r/x]\rrbracket_{\theta}=\{(p_{i}q_{ij},b_{ij},\rho_{ij})\}_{ij}$, therefore $\llbracket(U^{m}s)[r/x]\rrbracket_{\theta}=\llbracket U^{m}s[r/x]\rrbracket_{\theta}=\{(p_{i}q_{ij},\varepsilon,\overline{U^{m}}\rho_{ij}\overline{U^{m}})\}_{ij}$.

• •

Let $t=\pi^{m}s$. By the induction hypothesis, $\llparenthesis s[r/x]\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. By Lemma 12, $\llparenthesis\pi^{m}s[r/x]\rrparenthesis_{\theta}=\sum_{j}\overline{\pi_{j}}\llparenthesis s[r/x]\rrparenthesis_{\theta}\overline{\pi_{j}}^{\dagger}=\!\sum_{j}\overline{\pi_{j}}\sum_{j}p_{i}\llparenthesis s\rrparenthesis_{\theta,x=(b_{i},e_{i})}\overline{\pi_{j}}^{\dagger}$ $=\sum_{i}p_{i}\sum_{j}\overline{\pi_{j}}\llparenthesis s\rrparenthesis_{\theta,x=(b_{i},e_{i})}\overline{\pi_{j}}^{\dagger}=\sum_{i}p_{i}\llparenthesis\pi^{m}s\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Let $\llbracket s\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij},b_{ij},\rho_{ij})\}_{j}$, then $\llbracket\pi^{m}s\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij}\mathsf{tr}(\overline{\pi_{k}}^{\dagger}\overline{\pi_{k}}\rho_{ij}),k,\frac{\overline{\pi_{k}}\rho_{ij}\overline{\pi_{k}}}{\mathsf{tr}(\overline{\pi_{k}}^{\dagger}\overline{\pi_{k}}\rho_{ij})})\}_{jk}$. By the induction hypothesis, $\llbracket s[r/x]\rrbracket_{\theta}=\{(p_{i}q_{ij},b_{ij},\rho_{ij})\}_{ij}$, therefore, we have $\llbracket(\pi^{m}s)[r/x]\rrbracket_{\theta}=\llbracket\pi^{m}s[r/x]\rrbracket_{\theta}=\{(p_{i}q_{ij}\mathsf{tr}(\overline{\pi_{k}}^{\dagger}\overline{\pi_{k}}\rho_{ij}),k,\frac{\overline{\pi_{k}}\rho_{ij}\overline{\pi_{k}}}{\mathsf{tr}(\overline{\pi_{k}}^{\dagger}\overline{\pi_{k}}\rho_{ij})})\}_{ijk}$.

• •

Let $t=s_{1}\otimes s_{2}$, with $x\in FV(s_{1})$. By the induction hypothesis, $\llparenthesis s_{1}[r/x]\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{1}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$, and notice that, since $x\notin FV(s_{2})$, we have $\llparenthesis s_{2}\rrparenthesis_{\theta}=\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Therefore, by Lemma 13, $\llparenthesis s_{1}[r/x]\otimes s_{2}\rrparenthesis_{\theta}\!=\!\llparenthesis s_{1}[r/x]\rrparenthesis_{\theta}\otimes\llparenthesis s_{2}\rrparenthesis_{\theta}=(\sum_{i}p_{i}\llparenthesis s_{1}\rrparenthesis_{\theta,x=(b_{i},e_{i})})\otimes\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}\!=\!\sum_{i}p_{i}\llparenthesis s_{1}\rrparenthesis_{\theta,x=(b_{i},e_{i})}\otimes\llparenthesis s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$ $=\sum_{i}p_{i}\llparenthesis s_{1}\otimes s_{2}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$, where the last step is due to Lemma 13 as well. Note that if $\llbracket s_{1}\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij},b_{ij},\rho_{ij})\}_{j}$, and $\llbracket s_{2}\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(h_{k},b^{\prime}_{k},\rho^{\prime}_{k})\}_{k}$, we have $\llbracket s_{1}\otimes s_{i}\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij}h_{k},\varepsilon,\rho_{ij}\otimes\rho^{\prime}_{k})\}_{kj}$. By the induction hypothesis $\llbracket s_{1}[r/x]\rrbracket_{\theta}=\{(p_{i}q_{ij},b_{ij},\rho_{ij})\}_{ij}$, and so $\llbracket(s_{1}\otimes s_{2})[r/x]\rrbracket_{\theta}=\llbracket s_{1}[r/x]\otimes s_{2}\rrbracket_{\theta}=\{(p_{i}q_{ij}h_{k},\varepsilon,\rho_{ij}\otimes\rho^{\prime}_{k})\}_{ijk}$.

• •

Let $t=(b^{m},\rho^{n})$. $\llparenthesis(b^{m},\rho^{n})[r/x]\rrparenthesis_{\theta}=\llparenthesis(b^{m},\rho^{n})\rrparenthesis_{\theta}=\rho^{n}=\llparenthesis(b^{m},\rho^{n})\rrparenthesis_{\theta,x=(b_{i},e_{i})}$ $=\sum_{i}p_{i}\llparenthesis(b^{m},\rho^{n})\rrparenthesis_{\theta,x=(b_{i},e_{i})}$. Moreover, $\llbracket(b^{m},\rho^{n})\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(1,b^{m},\rho^{n})\}=\{(p_{i},b^{m},\rho^{n})\}_{i}=\llbracket(b^{m},\rho^{n}[r/x])\rrbracket_{\theta}=\llbracket(b^{m},\rho^{n})[r/x]\rrbracket_{\theta}$.

• •

Let $t=\mathsf{letcase}\ y=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$. Let $\llbracket s\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij},b^{\prime}_{ij},\rho_{ij})\}_{j}$. Then, by the induction hypothesis, $\llbracket s[r/x]\rrbracket_{\theta}=\{p_{i}q_{ij},b^{\prime}_{ij},\rho_{ij}\}_{ij}$. Let, forall $i$ and $j$, $\llbracket t_{b^{\prime}_{ij}}\rrbracket_{\theta,x=(b_{i},e_{i}),y=(\varepsilon,\rho_{ij})}=\{(h_{ijk},b^{\prime\prime}_{ijk},f_{ijk})\}_{k}$. Hence, we have that $\llbracket\mathsf{letcase}\ y=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij}h_{ijk},b^{\prime\prime}_{ijk},f_{ijk}\}_{jk}$ and also $\llbracket\mathsf{letcase}\ y=s[r/x]\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrbracket_{\theta}=\{(p_{i}q_{ij}h_{ijk},b^{\prime\prime}_{ijk},f_{ijk})\}_{ijk}$. Therefore, we have $\llparenthesis\mathsf{letcase}\ y=s[r/x]\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis\mathsf{letcase}\ y=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrparenthesis_{\theta,x=(b_{i},e_{i})}$ ∎

0.A.4 Proof of Theorem 2.1

By induction on the relation $\longrightarrow_{p}$.

• •

$(\lambda x.t)r\longrightarrow_{1}t[r/x]$. We have $\llbracket\lambda x.t\rrbracket_{\theta}=\{1,\varepsilon,(\mathsf{b},\mathsf{e})\mapsto\llbracket t\rrbracket_{\theta,x=(\mathsf{b},\mathsf{e})})\}$. By Lemma 2, we have $\llbracket r\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$ with $\sum_{i}p_{i}=1$, and $\llbracket t\rrbracket_{\theta,x=(b_{i},e_{i})}=\{(q_{ij},b^{\prime}_{ij},g_{ij})\}_{j}$. Therefore, we have that $\llbracket(\lambda x.t)r\rrbracket_{\theta}=\{(p_{i}q_{ij},b^{\prime}_{ij},g_{ij})\}_{ij}$, and $\llparenthesis(\lambda x.t)r\rrparenthesis_{\theta}=\sum_{ij}p_{i}q_{ij}g_{ij}$ which, by Lemma 3, is equal to $\llparenthesis t[r/x]\rrparenthesis_{\theta}$.

• •

$\mathsf{letcase}\ x=(b^{m},\rho^{n})\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\longrightarrow_{1}t_{b^{m}}[\rho^{n}/x]$. Then, we have that $\llbracket\mathsf{letcase}\ x=(b^{m},\rho^{n})\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrbracket_{\theta}=\llbracket t_{b^{m}}\rrbracket_{\theta,x=(\varepsilon,\rho^{n})}$. Therefore, we have that $\llparenthesis\mathsf{letcase}\ x=(b^{m},\rho^{n})\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrparenthesis_{\theta}=\llparenthesis t_{b^{m}}\rrparenthesis_{\theta,x=(\varepsilon,\rho^{n})}$. Since $\llbracket\rho^{n}\rrbracket_{\theta}=\{(1,\varepsilon,\rho^{n})\}$, we have, by Lemma 3, $\llparenthesis t_{b^{m}}\rrparenthesis_{\theta,x=(\varepsilon,\rho^{n})}=\llparenthesis t_{b^{m}}[\rho^{n}/x]\rrparenthesis_{\theta}$.

• •

$U^{m}\rho^{n}\longrightarrow_{1}\rho^{\prime n}$, with $\rho^{\prime n}=\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger}$. Then $\llbracket U^{m}\rho^{n}\rrbracket_{\theta}=\{(1,\varepsilon,\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger})\}$ $=\llbracket\rho^{\prime n}\rrbracket_{\theta}$, so $\llparenthesis U^{m}\rho^{n}\rrparenthesis_{\theta}=\rho^{\prime n}=\llparenthesis\rho^{\prime n}\rrparenthesis_{\theta}$.

• •

$\pi^{n}\rho^{n}\longrightarrow_{p_{i}}(i^{m},\rho_{i}^{n})$, with $p_{i}=\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho^{n})$ and $\rho_{i}^{n}=\frac{\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}}{p_{i}}$. We have $\llbracket\pi^{m}\rho^{n}\rrbracket_{\theta}=\{(p_{i},i,\rho_{i}^{n})\}_{i}$. Hence, $\llparenthesis\pi^{m}\rho^{n}\rrparenthesis_{\theta}=\sum_{i}p_{i}\rho_{i}^{n}=\sum_{i}p_{i}\llparenthesis\rho_{i}^{n}\rrparenthesis_{\theta}$.

• •

$\rho_{1}\otimes\rho_{2}\longrightarrow_{1}\rho$, with $\rho=\rho_{1}\otimes\rho_{2}$. We have $\llbracket\rho_{1}\otimes\rho_{2}\rrbracket_{\theta}=\{(1,\varepsilon,\rho)\}$, so $\llparenthesis\rho_{1}\otimes\rho_{2}\rrparenthesis_{\theta}=\rho=\llparenthesis\rho\rrparenthesis_{\theta}$.

• •

Contextual cases: Let $s\longrightarrow_{p_{i}}s_{i}$. Then

• –

$\lambda x.s\longrightarrow_{p_{i}}\lambda x.s_{i}$. By the induction hypothesis, $\llparenthesis s\rrparenthesis_{\theta^{\prime}}=\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta^{\prime}}$, for all $\theta^{\prime}\vDash\Gamma,x:A$. Then, $\llparenthesis\lambda x.s\rrparenthesis_{\theta}=(\mathsf{b},\mathsf{e})\mapsto\llparenthesis s\rrparenthesis_{\theta,x=(\mathsf{b},\mathsf{e})}=(\mathsf{b},\mathsf{e})\mapsto\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta,x=(\mathsf{b},\mathsf{e})}=\sum_{i}p_{i}((\mathsf{b},\mathsf{e})\mapsto\llparenthesis s_{i}\rrparenthesis_{\theta,x=(\mathsf{b},\mathsf{e})})=\sum_{i}p_{i}\llparenthesis\lambda x.s_{i}\rrparenthesis_{\theta}$.

• –

$ts\longrightarrow_{p_{i}}ts_{i}$. By the induction hypothesis, $\llparenthesis s\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}$. Then, we have $\llbracket ts\rrbracket_{\theta}=\{(p_{i}q_{j}h_{ijk},b^{\prime\prime}_{ijk},g_{ijk})\}_{ijk}$, with $\llbracket s\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$, $\llbracket t\rrbracket_{\theta}=\{(q_{j},b^{\prime}_{j},f_{j})\}_{j}$, and $f_{j}(b_{i},e_{i})=\{(h_{ijk},b^{\prime\prime}_{ijk},g_{ijk})\}_{k}$. Hence, $\llparenthesis ts\rrparenthesis_{\theta}=\sum_{ijk}p_{i}q_{j}h_{ijk}g_{ijk}=\sum_{i}p_{i}(\sum_{jk}q_{j}h_{ijk}g_{ijk})=\sum_{i}p_{i}\llparenthesis ts_{i}\rrparenthesis_{\theta}$

• –

$st\longrightarrow_{p_{i}}s_{i}t$. By the induction hypothesis, $\llparenthesis s\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}$. Then, we have $\llbracket st\rrbracket_{\theta}=\{(q_{j}p_{i}h_{jik},b^{\prime\prime}_{jik},g_{jik})\}_{jik}$, with $\llbracket t\rrbracket_{\theta}=\{(q_{j},b^{\prime}_{j},f_{j})\}_{j}$, $\llbracket s\rrbracket_{\theta}=\{(p_{i},b_{i},e_{i})\}_{i}$, and $e_{i}(b_{j},f_{j})=\{(h_{jik},b^{\prime\prime}_{jik},g_{jik})\}_{k}$. Hence, $\llparenthesis st\rrparenthesis_{\theta}=\sum_{jik}q_{j}p_{i}h_{jik}g_{jik}=\sum_{i}p_{i}(\sum_{jk}q_{j}h_{ijk}g_{ijk})=\sum_{i}p_{i}\llparenthesis s_{i}t\rrparenthesis_{\theta}$

• –

$U^{m}s\longrightarrow_{p_{i}}U^{m}s_{i}$. By the induction hypothesis, $\llparenthesis s\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}$. By Lemma 12, we have $\llparenthesis U^{m}s\rrparenthesis_{\theta}=\overline{U^{m}}\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}\overline{U^{m}}^{\dagger}=\sum_{i}p_{i}\overline{U^{m}}\llparenthesis s_{i}\rrparenthesis_{\theta}\overline{U^{m}}^{\dagger}$ $=\sum_{i}p_{i}\llparenthesis U^{m}s_{i}\rrparenthesis_{\theta}$.

• –

$\pi^{m}s\longrightarrow_{p_{i}}r=\pi^{m}s_{i}$. By the induction hypothesis, $\llparenthesis s\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}$. By Lemma 12, we have $\llparenthesis\pi^{m}s\rrparenthesis_{\theta}=\overline{\pi_{j}}\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}\overline{\pi_{j}}^{\dagger}=\sum_{i}p_{i}\overline{\pi_{j}}\llparenthesis s_{i}\rrparenthesis_{\theta}\overline{\pi_{j}}^{\dagger}=\sum_{i}p_{i}\llparenthesis\pi^{m}s_{i}\rrparenthesis_{\theta}$.

• –

$t\otimes s\longrightarrow_{p_{i}}r=t\otimes s_{i}$. By the induction hypothesis, $\llparenthesis s\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}$. By Lemma 13, $\llparenthesis t\otimes s\rrparenthesis_{\theta}=\llparenthesis t\rrparenthesis_{\theta}\otimes\llparenthesis s\rrparenthesis_{\theta}=\llparenthesis t\rrparenthesis_{\theta}\otimes(\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta})=\sum_{i}p_{i}\llparenthesis t\rrparenthesis_{\theta}\otimes\llparenthesis s_{i}\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis t\otimes s_{i}\rrparenthesis_{\theta}$.

• –

$s\otimes t\longrightarrow_{p_{i}}r=s_{i}\otimes t$. Analogous to previous case.

• –

$\mathsf{letcase}\ x=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\longrightarrow_{p_{i}}\mathsf{letcase}\ x=s_{i}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$. By the induction hypothesis, we have that $\llparenthesis s\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis s_{i}\rrparenthesis_{\theta}$. Let $\llbracket s\rrbracket_{\theta}=\{(p_{i},b_{i},\rho_{i})\}_{i}$ and $\llbracket t_{b_{i}}\rrbracket_{\theta,x=(\varepsilon,\rho_{i})}=\{(q_{ij},b^{\prime}_{ij},e_{ij})\}_{j}$, then, $\llparenthesis\mathsf{letcase}\ x=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrparenthesis_{\theta}=\sum_{ij}p_{i}q_{ij}e_{ij}=\sum_{i}p_{i}(\sum_{j}q_{ij}e_{ij})$ Notice that $\sum_{j}q_{ij}e_{ij}=\llparenthesis\mathsf{letcase}\ x=s_{i}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrparenthesis_{\theta}$. ∎

Appendix 0.B Detailed Proofs of Section 3.2

0.B.1 Proof of Theorem 3.1

By induction on the relation $\rightsquigarrow$. Rules $(\lambda x.t)r\rightsquigarrow t[r/x]$, $U^{m}\rho^{n}\rightsquigarrow\rho^{\prime}$ and $\rho\otimes\rho^{\prime}\rightsquigarrow\rho^{\prime\prime}$ are also valid rules for relation $\longrightarrow_{1}$, and hence the proof of these cases are the same than in Theorem 2.1.

Remaining cases:

• •

$\mathsf{letcase}^{\circ}\ x=\pi^{m}\rho^{n}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rightsquigarrow\sum_{i}p_{i}t_{i}[\rho^{\prime}/x]$, with $p_{i}=\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho^{n})$ and $\rho^{\prime}=\frac{\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}}{p_{i}}$. Since the interpretation of $\mathsf{letcase}^{\circ}$ coincides with the interpretation of $\mathsf{letcase}$, and $\mathsf{letcase}\ x=\pi^{m}\rho^{n}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\longrightarrow_{p_{i}}t_{i}[\rho^{\prime}/x]$, we can conclude by Theorem 2.1, and Lemma 4 that $\llparenthesis\mathsf{letcase}^{\circ}\ x=\pi^{m}\rho^{n}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis t_{i}[\rho^{\prime}/x]\rrparenthesis_{\theta}=\llparenthesis\sum_{i}p_{i}{t_{i}[\rho^{\prime}/x]}\rrparenthesis_{\theta}$.

• •

$\sum_{i}p_{i}\rho_{i}\rightsquigarrow\rho^{\prime}$, with $\rho^{\prime}=\sum_{i}p_{i}\rho_{i}$. $\llparenthesis\sum_{i}p_{i}\rho_{i}\rrparenthesis_{\theta}=\sum_{i}p_{i}\rho_{i}=\llparenthesis\rho^{\prime}\rrparenthesis_{\theta}$.

• •

$\sum_{i}p_{i}t\rightsquigarrow t$. Let $\llbracket t\rrbracket_{\theta}=\{(q_{j},b_{j},e_{j})\}_{j}$. Then, $\llbracket\sum_{i}p_{i}t\rrbracket_{\theta}=\{(p_{i}q_{j},b_{j},e_{j})\}_{ij}$ and so, $\llparenthesis\sum_{i}p_{i}t\rrparenthesis_{\theta}=\sum_{ij}p_{i}q_{j}e_{j}=(\sum_{i}p_{i})\sum_{j}q_{j}e_{j}=\sum_{j}q_{j}e_{j}=\llparenthesis t\rrparenthesis_{\theta}$.

• •

$(\sum_{i}p_{i}t_{i})r\rightsquigarrow\sum_{i}p_{i}(t_{i}r)$. Let $\llbracket t_{i}\rrbracket_{\theta}=\{(q_{ij},b_{ij},f_{ij})\}_{j}$, $\llbracket r\rrbracket_{\theta}=\{(h_{k},b^{\prime}_{k},e_{k})\}_{k}$, and $f_{ij}(b^{\prime}_{k},e_{k})=\{(\ell_{ijkh},b^{\prime\prime}_{ijkh},g_{ijkh})\}_{h}$. Then, we have that $\llbracket t_{i}r\rrbracket_{\theta}$ is equal to $\{(q_{ij}h_{k}\ell_{ijkh},b^{\prime\prime}_{ijkh},g_{ijkh})\}_{jkh}$, and $\llparenthesis\sum_{i}p_{i}(t_{i}r)\rrparenthesis_{\theta}=\sum_{jkh}p_{i}q_{ij}h_{k}\ell_{ijkh}g_{ijkh}$. On the other hand, $\llbracket\sum_{i}p_{i}t_{i}\rrbracket_{\theta}=\{(p_{i}q_{ij},b_{ij},f_{ij})\}_{ij}$, and so $\llbracket(\sum_{i}p_{i}t_{i})r\rrbracket_{\theta}=\{\!(p_{i}q_{ij}h_{k}\ell_{ijkh},b^{\prime\prime}_{ijkh},g_{ijkh})\!\}_{ijkh}$. Hence, $\llparenthesis(\sum_{i}\!p_{i}t_{i})r\rrparenthesis_{\theta}\!=\!\sum_{jkh}p_{i}q_{ij}h_{k}\ell_{ijkh}g_{ijkh}$ $=\llparenthesis\sum_{i}p_{i}(t_{i}r)\rrparenthesis_{\theta}$.

• •

Contextual cases: Only two cases need to be checked. All the other cases are analogous to those of the proof of Theorem 2.1.

• –

Let $\sum_{i}p_{i}t_{i}\rightsquigarrow\sum_{i}p_{i}r_{i}$, where $t_{j}\rightsquigarrow r_{j}$ and $\forall i\neq j$, $t_{i}=r_{i}$. By the induction hypothesis, $\llparenthesis t_{j}\rrparenthesis_{\theta}=\llparenthesis r_{j}\rrparenthesis_{\theta}$. Hence, using Lemma 4, $\llparenthesis\sum_{i}p_{i}t_{i}\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis t_{i}\rrparenthesis_{\theta}=\sum_{i}p_{i}\llparenthesis r_{i}\rrparenthesis_{\theta}=\llparenthesis\sum_{i}p_{i}r_{i}\rrparenthesis_{\theta}$.

• –

Let $\mathsf{letcase}^{\circ}\ x=t\ \mathsf{in}\ \{s_{0},\dots,s_{n}\}\rightsquigarrow\mathsf{letcase}^{\circ}\ x=r\ \mathsf{in}\ \{s_{0},\dots,s_{n}\}$, where $t\rightsquigarrow r$. Let $\llbracket t\rrbracket_{\theta}=\{(p_{i},b_{i},\rho_{i})\}_{i}$ and $\llbracket s_{b_{i}}\rrbracket_{\theta,x=(\varepsilon,\rho_{i})}=\{(q_{ij},b^{\prime}_{ij},e_{ij})\}_{j}$, then $\llparenthesis\mathsf{letcase}^{\circ}\ x=t\ \mathsf{in}\ \{s_{0},\dots,s_{2^{m}-1}\}\rrparenthesis_{\theta}=\sum_{ij}p_{i}q_{ij}e_{ij}$.

On the other hand, let $\llbracket r\rrbracket_{\theta}=\{(h_{k},b^{\prime\prime}_{k},\rho^{\prime}_{k})\}_{k}$. By the induction hypothesis, $\sum_{k}h_{k}\rho^{\prime}_{k}=\sum_{i}p_{i}\rho_{i}$. We conclude by inversion that $h_{i}=p_{i}$ and $\rho^{\prime}_{i}=\rho_{i}$, which prove the case. ∎

Appendix 0.C Detailed Proofs of Section 4

0.C.1 Proof of Lemma 8

By induction on $t$. The only difference between $\lambda_{\rho}$ and $\lambda_{\rho}^{\circ}$ are in terms $(b^{m},\rho^{n})$, which is not present in $\lambda_{\rho}^{\circ}$, and $\sum_{i}p_{i}t_{i}$, which is not present in $\lambda_{\rho}$. Hence, we can prove both calculi at the same time. We use $\vdash$ generically to refer also to $\Vdash$ where it is also valid.

• •

Let $t=x$. Then $B=A$. By Lemma 6, $\Gamma,\Delta\vdash r:A$. Notice that $t[r/x]=r$.

• •

Let $t=y$. Then, by Lemmas 6 and 7, $\Gamma,\Delta\vdash y:B$. Notice that $t[r/x]=y$.

• •

Let $t=\lambda y.s$. Then $B=C\multimap D$ and, by inversion, $\Gamma,x:A,y:C\vdash s:D$. Then, by the induction hypothesis, $\Gamma,y:C,\Delta\vdash s[r/x]:D$, so, by rule $\multimap_{i}$, $\Gamma,\Delta\vdash\lambda y.(s[r/x]):C\multimap D$. Notice that $\lambda y.(s[r/x])=(\lambda y.s)[r/x]$.

• •

Let $t=t_{1}t_{2}$. Then $\Gamma,x:A=\Gamma_{1},\Gamma_{2}$, with $\Gamma_{1}\vdash t_{1}:C\multimap B$ and $\Gamma_{2}\vdash t_{2}:C$.

• –

If $x:A\in\Gamma_{1}$, then, by the induction hypothesis $\Gamma_{1}\setminus\{x:A\},\Delta\vdash t_{1}[r/x]:C\multimap B$, so by rule $\multimap_{e}$, $\Gamma_{1}\setminus\{x:A\},\Gamma_{2},\Delta\vdash t_{1}[r/x]t_{2}:B$. Notice that $\Gamma_{1}\setminus\{x:A\},\Gamma_{2}=\Gamma$ and $t_{1}[r/x]t_{2}=(t_{1}t_{2})[r/x]$.

• –

If $x:A\in\Gamma_{2}$, then, by the induction hypothesis $\Gamma_{2}\setminus\{x:A\},\Delta\vdash t_{2}[r/x]:C$, so by rule $\multimap_{e}$, $\Gamma_{1},\Gamma_{2}\setminus\{x:A\},\Delta\vdash t_{1}(t_{2}[r/x]):B$. Notice that $\Gamma_{1},\Gamma_{2}\setminus\{x:A\}=\Gamma$ and $t_{1}(t_{2}[r/x])=(t_{1}t_{2})[r/x]$.

• •

Let $t=\rho^{n}$. Then $B=n$. By Lemmas 6 and 7, $\Gamma,\Delta\vdash\rho^{n}:n$. Notice that $t[r/x]=\rho^{n}$.

• •

Let $t=U^{m}s$. Then $B=n$ and $\Gamma,x:A\vdash s:n$. Then, by the induction hypothesis, $\Gamma,\Delta\vdash s[r/x]:n$. So, by rule $u$, $\Gamma,\Delta\vdash U^{m}(s[r/x]):n$. Notice that $U^{m}(s[r/x])=(U^{m}s)[r/x]$.

• •

Let $t=\pi^{m}s$. Then $B=(m,n)$ and $\Gamma,x:A\vdash s:n$. Then, by the induction hypothesis, $\Gamma,\Delta\vdash s[r/x]:n$. So, by rule $m$, $\Gamma,\Delta\vdash\pi^{m}(s[r/x]):(m,n)$. Notice that $\pi^{m}(s[r/x])=(\pi^{m}s)[r/x]$.

• •

Let $t=t_{1}\otimes t_{2}$. Then $B=n_{1}+n_{2}$, $\Gamma,x:A=\Gamma_{1},\Gamma_{1}$ with $\Gamma_{i}\vdash t_{i}:n_{i}$ for $i=1,2$. Let $x:A\in\Gamma_{i}$ for some $i=1,2$. Then, by the induction hypothesis, $\Gamma_{i}\setminus\{x:A\},\Delta\vdash t_{i}[r/x]$, so by rule $\otimes$, either $\Gamma,\Delta\vdash t_{1}[r/x]\otimes t_{2}:n_{1}+n_{2}$, or $\Gamma,\Delta\vdash t_{1}\otimes t_{2}[r/x]:n_{1}+n_{2}$. In the first case, notice that $t_{1}[r/x]\otimes t_{2}=(t_{1}\otimes t_{2})[r/x]$, and in the second, $t_{1}\otimes t_{2}[r/x]=(t_{1}\otimes t_{2})[r/x]$.

• •

Let $t=(b^{m},\rho^{n})$. Then $B=(m,n)$. By Lemmas 6 and 7, $\Gamma,\Delta\vdash(b^{m},\rho^{n}):(m,n)$. Notice that $t[r/x]=(b^{m},\rho^{n})$.

• •

Let $t=\sum_{i}p_{i}t_{i}$. Then $\Gamma,x:A\Vdash t_{i}:B$ and so, by the induction hypothesis, $\Gamma,\Delta\Vdash t_{i}[r/x]:B$. Therefore, by rule $+$, $\Gamma,\Delta\Vdash\sum_{i}p_{i}t_{i}[r/x]:B$.

• •

Let $t=\mathsf{letcase}\ y=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$. $y:n\vdash t_{i}:B$, for $i=0,\dots,2^{m}-1$, and, $\Gamma\vdash s:(m,n)$. By the induction hypothesis, $\Gamma,\Delta\vdash s[r/x]:(m,n)$. So, by rule $\mathsf{lc}$, $\Gamma,\Delta\vdash\mathsf{letcase}\ y=s[r/x]\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\!\!:B$. Notice that $\mathsf{letcase}\ y=s[r/x]\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}=(\mathsf{letcase}\ y=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\})[r/x]$.∎

0.C.2 Proof of Theorem 4.1

By induction on the relations $\longrightarrow_{p}$ and $\rightsquigarrow$.

• •

Let $t=(\lambda x.t^{\prime})s$, $r=t^{\prime}[r/s]$ and $p=1$. Then $\Gamma\vdash(\lambda x.t^{\prime})s:A$, so, $\Gamma_{1}\vdash\lambda x.t^{\prime}:B\multimap A$ and $\Gamma_{2}\vdash s:B$, with $\Gamma=\Gamma_{1},\Gamma_{2}$. Hence, $\Gamma_{1},x:B\vdash t^{\prime}:A$, and so, by Lemma 8, $\Gamma\vdash t^{\prime}[s/x]:A$.

• •

Let $t=\mathsf{letcase}\ x=(b^{m},\rho^{n})\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$, $r=t_{b^{m}}[\rho^{n}/x]$ and $p=1$. Then, by inversion, $x:n^{\prime}\vdash t_{i}:A$, for $i=0,\dots,2^{m}-1$, and $\Gamma\vdash(b^{m},\rho^{n}):(m^{\prime},n^{\prime})$. So, by inversion again, $m^{\prime}=m$ and $n^{\prime}=n$. By rule $\mathsf{ax}_{\rho}$, $\Gamma\vdash\rho^{n}:n$. Hence, by Lemma 8, $\Gamma\vdash t_{b^{m}}[\rho^{n}/x]:A$.

• •

Let $t=U^{m}\rho^{n}$, $r={\rho^{\prime}}^{n}$ and $p=1$, with ${\rho^{\prime}}^{n}=\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger}$. Then $A=n$. By rule $\mathsf{ax}_{\rho}$, $\Gamma\vdash{\rho^{\prime}}^{n}:n$.

• •

Let $t=\pi^{m}\rho^{n}$, $r=(i^{m},\rho_{i}^{n})$, with $\rho_{i}^{n}=\frac{\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}}{p}$ and $p=\mathsf{tr}(\overline{\pi_{1}}^{\dagger}\overline{\pi_{i}}\rho^{n})$. Then $B=(m,n)$. By rule $\mathsf{m}$, $\Gamma\vdash(i^{m},\rho_{i}^{n}):(m,n)$.

• •

Let $t=\rho_{1}^{n}\otimes\rho_{2}^{m}$ and $r=\rho$, with $\rho=\rho_{1}^{n}\otimes\rho_{2}^{m}$. Then, $A=n+m$, with $\vdash\rho_{1}^{n}:n$ and $\vdash\rho_{2}^{m}:m$. Since $\rho$ is a density matrix of $(n+m)$-qubits, $\vdash\rho:n+m$.

• •

Contextual cases: Let $s\longrightarrow_{p}s^{\prime}$, then

• –

Consider $t=\lambda x.s$ and $r=\lambda x.s^{\prime}$. Then $A=B\multimap C$ and $\Gamma,x:B\vdash s:C$. So, by the induction hypothesis, $\Gamma,x:B\vdash s^{\prime}:C$ and by rule $\multimap_{i}$, $\Gamma\vdash\lambda x.s^{\prime}:B\multimap C$.

• –

Consider $t=t^{\prime}s$ and $r=t^{\prime}s^{\prime}$. Then $\Gamma=\Gamma_{1},\Gamma_{2}$, with $\Gamma_{1}\vdash t^{\prime}:B\multimap A$ and $\Gamma_{2}\vdash s:B$. By the induction hypothesis, $\Gamma_{2}\vdash s^{\prime}:B$, so by rule $\multimap_{e}$, $\Gamma\vdash t^{\prime}s^{\prime}:A$.

• –

Consider $t=st^{\prime}$ and $r=s^{\prime}t^{\prime}$. Then $\Gamma=\Gamma_{1},\Gamma_{2}$, with $\Gamma_{1}\vdash s:B\multimap A$ and $\Gamma_{2}\vdash t^{\prime}:B$. By the induction hypothesis, $\Gamma_{1}\vdash s^{\prime}:B\multimap A$, so by rule $\multimap_{e}$, $\Gamma\vdash s^{\prime}t^{\prime}:A$.

• –

Consider $t=U^{m}s$ and $r=U^{m}s^{\prime}$. Then $A=n$ and $\Gamma\vdash s:n$. By the induction hypothesis $\Gamma\vdash s^{\prime}:n$, so by rule $\mathsf{u}$, $\Gamma\vdash U^{m}s^{\prime}:n$.

• –

Consider $t=\pi^{m}s$ and $r=\pi^{m}s^{\prime}$. Then $A=n$ and $\Gamma\vdash s:n$. By the induction hypothesis $\Gamma\vdash s^{\prime}:n$, so by rule $\mathsf{m}$, $\Gamma\vdash\pi^{m}s^{\prime}:n$.

• –

Consider $t=t^{\prime}\otimes s$ and $r=t^{\prime}\otimes s^{\prime}$. Then $A=n+m$ and $\Gamma=\Gamma_{1},\Gamma_{2}$, with $\Gamma_{1}\vdash t^{\prime}:n$ and $\Gamma_{2}\vdash s:m$. By the induction hypothesis $\Gamma_{2}\vdash s^{\prime}:m$, so by rule $\otimes$, $\Gamma\vdash t^{\prime}\otimes s^{\prime}:n+m$.

• –

Consider $t=s\otimes t^{\prime}$ and $r=s^{\prime}\otimes t^{\prime}$. Then $A=n+m$ and $\Gamma=\Gamma_{1},\Gamma_{2}$, with $\Gamma_{1}\vdash s:n$ and $\Gamma_{2}\vdash t^{\prime}:m$. By the induction hypothesis $\Gamma_{2}\vdash s^{\prime}:m$, so by rule $\otimes$, $\Gamma\vdash t^{\prime}\otimes s^{\prime}:n+m$.

• –

Consider $t=\mathsf{letcase}\ x=s\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$ and $r=\mathsf{letcase}\ x=s^{\prime}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$. Then $x:n\vdash t_{i}:A$ for $i=0,\dots,2^{m}-1$, and $\Gamma\vdash s:(m,n)$. So, by the induction hypothesis, $\Gamma\vdash s^{\prime}:(m,n)$ and by rule $\mathsf{lc}$, $\Gamma\vdash\mathsf{letcase}\ x=s^{\prime}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}:A$.∎ 2. 2.

• •

Let $t=(\lambda x.t^{\prime})s$ and $r=t^{\prime}[s/x]$. Analogous to the same rule in $\lambda_{\rho}$.

• •

Let $t=\mathsf{letcase}^{\circ}\ x=\pi^{m}\rho^{n}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}}-1\}$ and $r=\sum_{i}p_{i}t_{i}[\rho^{n}_{i}/x]$, with $\rho_{i}^{n}=\frac{\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}}{p_{i}}$ and $p_{i}=\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho^{n})$. Then $\Gamma\Vdash\pi^{m}\rho^{n}:(m,n)$ and $x:n\Vdash t_{i}:A$. By Lemma 8, $\Gamma\Vdash t_{i}[\rho_{i}^{n}/x]:A$, then, by rule $+$, $\Gamma\Vdash\sum_{i}p_{i}t_{i}[\rho_{i}^{n}/x]:A$.

• •

Let $t=U^{m}\rho^{n}$ and $r={\rho^{\prime}}^{n}$, with $\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger}={\rho^{\prime}}^{n}$. Analogous to the same rule in $\lambda_{\rho}$.

• •

Let $t=\rho_{1}^{n}\otimes\rho^{m}_{2}$ and $r=\rho$, with $\rho=\rho_{1}^{n}\otimes\rho_{2}^{m}$. Analogous to the same rule in $\lambda_{\rho}$.

• •

Let $t=\sum_{i}p_{i}\rho_{i}$ and $r=\rho^{\prime}$, with $\rho^{\prime}=\sum_{i}p_{i}\rho_{i}$. Then, $\Gamma\Vdash\sum_{i}p_{i}\rho_{i}:n$, and by rule $\mathsf{ax}_{\rho}$, $\Gamma\Vdash\rho^{\prime}:n$.

• •

Let $t=\sum_{i}p_{i}r$. Then, $\Gamma\Vdash r:A$.

• •

Let $t=(\sum_{i}p_{i}t_{i})r$ and $\sum_{i}p_{i}(t_{i}r)$. Then, $\Gamma=\Gamma_{1},\Gamma_{2}$, $\Gamma_{1}\Vdash t_{i}:B\multimap A$ and $\Gamma_{2}\Vdash r:B$. Therefore, by rule $\multimap_{e}$, $\Gamma_{1},\Gamma_{2}\Vdash t_{i}r:A$, and by rule $+$, $\Gamma_{1},\Gamma_{2}\Vdash\sum_{i}p_{i}(t_{i}r):A$.

• •

Contextual cases. All the contextual cases are analogous to the same rules in $\lambda_{\rho}$, except for the contextual rule of $\sum$: Consider $t=\sum_{i}p_{i}t_{i}$ and $r=\sum_{i}p_{i}r_{i}$, with $t_{j}\rightsquigarrow r_{j}$, and $\forall i\neq j$, $t_{i}=r_{i}$. By inversion, $\Gamma\Vdash t_{i}:A$. By the induction hypothesis, $\forall i$, $\Gamma\Vdash r_{i}:A$. Then, by rule $+$, $\Gamma\Vdash\sum_{i}p_{i}r_{i}$. ∎

0.C.3 Proof of Lemma 9

We proceed by induction on $v$.

• •

Let $v=x$. Then we are done, since variables do not rewrite.

• •

Let $v=\lambda x.v^{\prime}$. By the induction hypothesis, $v^{\prime}$ does not rewrite, and so $v$ neither does.

• •

Let $v=w_{1}\otimes w_{2}$. By the induction hypothesis, nor $w_{1}$ nor $w_{2}$ rewrite, and the only rule rewriting a $\otimes$ in head position needs both $w_{1}$ and $w_{2}$ to be density matrices, which are not according to the grammar.

• •

Let $v=\rho^{n}$. Then we are done, since density matrices are constants and do not rewrite.

• •

Let $v=(b^{m},\rho^{n})$. Then we are done, since pairs are constants and do not rewrite. 2. 2.

We proceed by induction on $v$. The only difference with the previous case is that the last term is not present, and a new term is introduced. Hence, let $v=\sum_{i}p_{i}w_{i}$. The only possible rewrite would be if there were some $w_{i}=w_{j}$, which is explicitly excluded from the grammar. So, this term does not rewrite ∎

0.C.4 Proof of Theorem 4.2

We relax the hypotheses and prove the theorem for open terms as well. That is:

If $\Gamma\vdash t:A$, then either $t$ is a value, there exist $n$, $p_{1},\dots,p_{n}$, and $r_{1},\dots,r_{n}$ such that $t\longrightarrow_{p_{i}}r_{i}$, or $t$ contains a free variable, and $t$ does not rewrite. 2. 2.

If $\Gamma\Vdash t:A$, then either $t$ is a value∘, there exists $r$ such that $t\rightsquigarrow r$, or $t$ contains a free variable, and $t$ does not rewrite.

The proofs proceeds as follows.

We proceed by induction on the derivation of $\vdash t:A$.

• •

Let $\Gamma,x:A\vdash x:A$ as a consequence of rule $\mathsf{ax}$. Then, we are done since $x$ is a free variable and does not rewrite.

• •

Let $\Gamma\vdash\lambda x.t:A\multimap B$ as a consequence of $\Gamma,x:A\vdash t:B$ and rule $\multimap_{i}$. Then, by the induction hypothesis, either

• –

$t$ is not a value and there exist $n$, $p_{1},\dots,p_{n}$ and $r_{1},\dots,r_{n}$ such that $t\longrightarrow_{p_{i}}r_{i}$, which case $\lambda x.t\longrightarrow_{p_{i}}\lambda x.r_{i}$;

• –

$t$ is a value, in which case $\lambda x.t$ is a value as well; or

• –

$t$ contains a free variable, and $t$ does not rewrite, in which case the same happens to $\lambda x.t$.

• •

Let $\Gamma,\Delta\vdash tr:B$ as a consequence of $\Gamma\vdash t:A\multimap B$, $\Delta\vdash r:A$ and rule $\multimap_{e}$. Then, by the induction hypothesis, one of the following cases happens:

• –

There exist $n$, $p_{1},\dots,p_{n}$, and $t_{1},\dots,t_{n}$ such that $t\longrightarrow_{p_{i}}t_{i}$, in which case $tr\longrightarrow_{p_{i}}t_{i}r$.

• –

There exist $n$, $p_{1},\dots,p_{n}$ and $r_{1},\dots,r_{n}$ such that $r\longrightarrow_{p_{i}}r_{i}$, in which case $tr\longrightarrow_{p_{i}}tr_{i}$.

• –

$t$ is a value and $r$ does not rewrite. The only values which can be typed by $A\multimap B$ are:

$t=x$, in which case $xr$ contains a free variable and does not rewrite.

• *

$t=\lambda x.v$, in which case $(\lambda x.v)r\longrightarrow_{1}v[r/x]$.

• –

$t$ is not a value, contains a free variable, and does not rewrite, and $r$ does not rewrite, in which case $tr$ contains a free variable and does not rewrite.

• •

Let $\Gamma\vdash\rho^{n}:n$ as a consequence of rule $\mathsf{ax_{\rho}}$. Then, we are done since $\rho^{n}$ is a value.

• •

Let $\Gamma\vdash U^{m}t:n$ as a consequence of $\Gamma\vdash t:n$ and rule $\mathsf{u}$. Then, by the induction hypothesis, one of the following cases happens:

• –

$t$ is a value. The only values which can be typed by $n$ are:

$t=x$, in which case $U^{m}x$ contains a free variable and does not rewrite.

• *

$t=\bigotimes x_{i}$, in which case $U^{m}\bigotimes x_{i}$ contains free variables and does not rewrite.

• *

$t=\rho^{n}$, in which case $U^{m}\rho^{n}\longrightarrow_{1}\rho^{\prime}$, with $\rho^{\prime}=\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger}$.

• –

There exist $n$, $p_{1},\dots,p_{n}$ and $t_{1},\dots,t_{n}$ such that $t\longrightarrow_{p_{i}}t_{i}$, in which case $U^{m}t\longrightarrow_{p_{i}}t_{i}$;

• –

$t$ contains a free variable and does not rewrite, in which case the same is true for $U^{m}t$.

• •

Let $\Gamma\vdash\pi^{m}t:(m,n)$ as a consequence of $\Gamma\vdash t:n$ and rule $\mathsf{m}$. Then, by the induction hypothesis, one of the following cases happens:

• –

$t$ is a value. The only values which can be typed by $n$ are:

$t=x$, in which case $\pi^{m}x$ contains a free variable and does not rewrite.

• *

$t=\bigotimes x_{i}$, in which case $\pi^{m}\bigotimes x_{i}$ contains free variables and does not rewrite.

• *

$t=\rho^{n}$, in which case $\pi^{m}\rho^{n}\longrightarrow_{p_{i}}(i,\rho_{i}^{n})$, with $p_{i}=\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho^{n})$ and $\rho_{i}^{n}=\frac{\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}}{p_{i}}$.

• –

There exist $n$, $p_{1},\dots,p_{n}$ and $t_{1},\dots,t_{n}$ such that $t\longrightarrow_{p_{i}}t_{i}$, in which case $\pi^{m}t\longrightarrow_{p_{i}}t_{i}$;

• –

$t$ contains a free variable and does not rewrite, in which case the same is true for $\pi^{m}t$.

• •

Let $\Gamma,\Delta,\vdash t\otimes r:n+m$ as a consequence of $\Gamma\vdash t:n$, $\Delta\vdash r:m$ and rule $\otimes$. Then, by the induction hypothesis, one of the following happens:

• –

There exist $k$, $p_{1},\dots,p_{n}$, and $t_{1},\dots,t_{k}$ such that $t\longrightarrow_{p_{i}}t_{i}$, in which case $t\otimes r\longrightarrow_{p_{i}}t_{i}\otimes r$.

• –

There exist $k$, $p_{1},\dots,p_{n}$, and $r_{1},\dots,r_{k}$ such that $r\longrightarrow_{p_{i}}r_{i}$, in which case $t\otimes r\longrightarrow_{p_{i}}t\otimes r_{i}$.

• –

$t$ is a value and $r$ does not rewrite. The only values which can be typed by $n$ are:

$t=x$, then $t\otimes r$ contains a free variable and does not rewrite.

• *

$t=\bigotimes x_{i}$, then $t\otimes r$ contains free variables and does not rewrite.

• *

$t=\rho^{n}$, then:

• ·

If $r=\rho^{m}$, $t\otimes r\longrightarrow_{1}\rho^{\prime}$, with $\rho^{\prime}=\rho^{n}\otimes\rho^{m}$.

• ·

If $r$ contains a free variable and does not rewrite, then the same is true for $t\otimes r$.

• –

$t$ contains a free variable and does not rewrite, and $r$ does not rewrite, in which case $t\otimes r$ contains a free variable and does not rewrite.

• •

Let $\Gamma\vdash(b^{m},\rho^{n}):(m,n)$ as a consequence of rule $\mathsf{ax}_{\mathsf{am}}$. Then, we are done since $(b^{m},\rho^{n})$ is a value.

• •

Let $\Gamma\vdash\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}:A$ as a consequence of $x:n\vdash t_{i}:A$ for $i=0,\dots,2^{m}-1$, $\Gamma\vdash r:(m,n)$, and rule $\mathsf{lc}$. By the induction hypothesis, the possible cases for $r$ are:

• –

$r$ is a value. The possible values which can be typed by $(m,n)$ are:

$r=y$, in which case $\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$ contains a free variable and does not reduce.

• *

$r=(b^{m},\rho^{n})$, in which case $\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\longrightarrow_{1}t_{b^{m}}[\rho^{n}/x]$.

• –

There exist $k$, $p_{1},\dots,p_{k}$, and $r_{1},\dots,r_{k}$ such that $r\longrightarrow_{p_{i}}r_{i}$, and $\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\!\longrightarrow_{p_{i}}\!\mathsf{letcase}\ x=r_{i}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$.

• –

$r$ contains a free variable and does not rewrite, in which case the same is true for $\mathsf{letcase}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$. 2. 2.

We proceed by induction on the derivation of $\Gamma\Vdash t:A$.

• •

Let $\Gamma,x:A\Vdash x:A$ as a consequence of rule $\mathsf{ax}$. Then, we are done since $x$ is a free variable and does not rewrite.

• •

Let $\Gamma\Vdash\lambda x.t:A\multimap B$ as a consequence of $\Gamma,x:A\Vdash t:B$ and rule $\multimap_{i}$. Then, by the induction hypothesis, either

• –

$t$ is not a value∘ and there exists $r$ such that $t\rightsquigarrow r$, which case $\lambda x.t\rightsquigarrow\lambda x.r$;

• –

$t$ is a value∘, in which case $\lambda x.t$ is a value∘ as well; or

• –

$t$ contains a free variable, and $t$ does not rewrite, in which case the same happens to $\lambda x.t$.

• •

Let $\Gamma,\Delta\Vdash tr:B$ as a consequence of $\Gamma\Vdash t:A\multimap B$, $\Delta\Vdash r:A$ and rule $\multimap_{e}$. Then, by the induction hypothesis, one of the following cases happens:

• –

There exists $t^{\prime}$ such that $t\rightsquigarrow t^{\prime}$, in which case $tr\rightsquigarrow t^{\prime}r$.

• –

There exists $r^{\prime}$ such that $r\rightsquigarrow r^{\prime}$, in which case $tr\rightsquigarrow tr^{\prime}$.

• –

$t$ is a value∘ and $r$ does not rewrite. The only values∘ which can be typed by $A\multimap B$ are:

$t=x$, in which case $xr$ contains a free variable and does not rewrite.

• *

$t=\lambda x.v$, in which case $(\lambda x.v)r\rightsquigarrow v[r/x]$.

• *

$t=\sum_{i}p_{i}t_{i}$, where $\Gamma\Vdash t_{i}:A\multimap B$. Then, $tr\rightsquigarrow\sum_{i}p_{i}(t_{i}r)$.

• –

$t$ is not a value∘, contains a free variable, and does not rewrite, and $r$ does not rewrite, in which case, if $t$ is not a sum, $tr$ contains a free variable and does not rewrite. If $t=\sum_{i}p_{i}t_{i}$ is a sum, $tr\rightsquigarrow\sum_{i}p_{i}(t_{i}r)$.

• •

Let $\Gamma\Vdash\rho^{n}:n$ as a consequence of rule $\mathsf{ax_{\rho}}$. Then, we are done since $\rho^{n}$ is a value∘.

• •

Let $\Gamma\Vdash U^{m}t:n$ as a consequence of $\Gamma\Vdash t:n$ and rule $\mathsf{u}$. Then, by the induction hypothesis, one of the following cases happens:

• –

$t$ is a value∘. Since $\lambda x.v$ cannot be typed by $n$, the only values∘ that can be typed by $n$ are either $\rho^{n}$, or they contain free variables:

Let $t=\rho^{n}$, then $U^{m}\rho^{n}\rightsquigarrow\rho^{\prime}$, with $\rho^{\prime}=\overline{U^{m}}\rho^{n}\overline{U^{m}}^{\dagger}$.

• *

Let $t$ contain a free variable. Notice that it can only be either a free variable by itself, a tensor of values∘ containing free variables, or a linear combination of different values∘ containing free variables. In any case, $t$ contains a free variable and does not rewrite. Hence, $U^{m}t$ contains a free variable and does not rewrite.

• –

There exists $r$ such that $t\rightsquigarrow r$, in which case $U^{m}t\rightsquigarrow r$;

• –

$t$ contains a free variable and does not rewrite, in which case the same is true for $U^{m}t$.

• •

Let $\Gamma\Vdash\pi^{m}t:(m,n)$ as a consequence of $\Gamma\Vdash t:n$ and rule $\mathsf{m}$. Then, by the induction hypothesis, one of the following cases happens:

• –

$t$ is a value∘. Since $\lambda x.v$ cannot be typed by $n$, the only values∘ that can be typed by $n$ are either $\rho^{n}$, or they contain free variables:

Let $t=\rho^{n}$, then $\pi^{m}\rho^{n}\rightsquigarrow\rho^{\prime}$, with $\rho^{\prime}=\sum_{i}\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}$.

• *

Let $t$ contain a free variable. Notice that it can only be either a free variable by itself, a tensor of values∘ containing free variables, or a linear combination of different values∘ containing free variables. In any case, $t$ contains a free variable and does not rewrite. Hence, $\pi^{m}t$ contains a free variable and does not rewrite.

• –

There exists $r$ such that $t\rightsquigarrow r$, in which case $\pi^{m}t\rightsquigarrow r$;

• –

$t$ contains a free variable and does not rewrite, in which case the same is true for $\pi^{m}t$.

• •

Let $\Gamma,\Delta,\Vdash t\otimes r:n+m$ as a consequence of $\Gamma\Vdash t:n$, $\Delta\Vdash r:m$ and rule $\otimes$. Then, by the induction hypothesis, one of the following happens:

• –

There exists $t^{\prime}$ such that $t\rightsquigarrow t^{\prime}$, in which case $t\otimes r\rightsquigarrow t^{\prime}\otimes r$.

• –

There exists $r^{\prime}$ such that $r\rightsquigarrow r^{\prime}$, in which case $t\otimes r\rightsquigarrow t\otimes r^{\prime}$.

• –

$t$ is a value∘ and $r$ does not rewrite. The only values∘ that can be typed by $n$ are either $\rho^{n}$, or they contain free variables.

Let $t=\rho^{n}$, then:

• ·

If $r=\rho^{m}$, $t\otimes r\rightsquigarrow\rho^{\prime}$, with $\rho^{\prime}=\rho^{n}\otimes\rho^{m}$.

• ·

If $r$ contains a free variable and does not rewrite, then the same is true for $t\otimes r$.

• *

Let $t$ contain a free variable. Then $t\otimes r$ contains a free variable and does not rewrite.

• –

$t$ contains a free variable and does not rewrite, and $r$ does not rewrite, in which case $t\otimes r$ contains a free variable and does not rewrite.

• •

Let $\Gamma\Vdash\mathsf{letcase}^{\circ}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}:A$ as a consequence of $x:n\Vdash t_{i}:A$ for $i=0,\dots,2^{m}-1$, $\Gamma\Vdash r:(m,n)$, and rule $\mathsf{lc}$. By the induction hypothesis, the possible cases for $r$ are:

• –

$r$ is a value∘. The only possible values∘ that can be typed by $(m,n)$ are variables or linear combination of variables. In any case, we have that $\mathsf{letcase}^{\circ}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$ contains at least a free variable and does not rewrite.

• –

There exists $r^{\prime}$ such that $r\rightsquigarrow r^{\prime}$, in which case, we have to distinguish two cases:

$r\neq\pi^{m}\rho^{n}$, and therefore $\mathsf{letcase}^{\circ}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rightsquigarrow\mathsf{letcase}^{\circ}\ x=r^{\prime}\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$.

• *

$r=\pi^{m}\rho^{n}$, and therefore $\mathsf{letcase}^{\circ}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}\rightsquigarrow\sum_{i}p_{i}t_{i}[\rho^{n}_{i}/x]$, where $p_{i}=\mathsf{tr}(\overline{\pi_{i}}^{\dagger}\overline{\pi_{i}}\rho^{n})$ and $\rho_{i}^{n}=\frac{\overline{\pi_{i}}\rho^{n}\overline{\pi_{i}}^{\dagger}}{p_{i}}$.

• –

$r$ contains a free variable and does not rewrite, in which case the same is true for $\mathsf{letcase}^{\circ}\ x=r\ \mathsf{in}\ \{t_{0},\dots,t_{2^{m}-1}\}$.

• •

Let $\Gamma\Vdash\sum_{i}p_{i}t_{i}:A$ as a consequence of $\Gamma\Vdash t_{i}:A$, $\sum_{i}p_{i}=1$, and rule $+$. If $\sum_{i}p_{i}t_{i}$ is a value∘, then we are done. If it is not a value, then one of the following cases is true:

• –

$t_{j}=t_{k}$ for some $j\neq k$, in which case $\sum_{i}p_{i}t_{i}\rightsquigarrow(\sum_{i\neq j,k}p_{i}t_{i})+(p_{j}+p_{k})t_{j}$.

• –

At least one $t_{i}$ is not a value. By the induction hypothesis, if $t_{i}$ is not a value, either it rewrites, or it contains a free variable and does not rewrite. If at least one $t_{i}$ rewrites, then $\sum_{i}p_{i}t_{i}$ rewrites. If none of these rewrites and at least one contains a free variable, then $\sum_{i}p_{i}t_{i}$ does not rewrite and contain a free variable. ∎