# A feasible and unitary quantum programming language

ALEJANDRO DÍAZ-CARO, Universidad de Buenos Aires-CONICET, ICC, Buenos Aires, Argentina and Universidad Nacional de Quilmes, DCyT, Bernal, Argentina

EMMANUEL HAINRY, ROMAIN PÉCHOUX, and MÁRIO SILVA, Université de Lorraine, CNRS, Inria, LORIA, F54000 Nancy, France

We introduce a novel quantum programming language featuring higher-order programs and quantum control flow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeing both unitarity and polynomial-time normalization. Unitarity is achieved by using a special modality for superpositions while requiring orthogonality among superposed terms. Polynomial-time normalization is achieved using a linear-logic-based type discipline employing Barber and Plotkin duality along with a specific modality to account for potential duplications. This type discipline also guarantees that derived values have polynomial size. Our language seamlessly combines the two modalities: quantum circuit programs uphold unitarity, and all programs are evaluated in polynomial time, ensuring their feasibility.

**ACM Reference Format:**

Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux, and Mário Silva. 2024. A feasible and unitary quantum programming language. 1, 1 (March 2024), 47 pages. https://doi.org/XXXXXXX.XXXXXXX

# 1 INTRODUCTION

## 1.1 Motivation

*Classical control vs quantum control.* Quantum programming languages can be classified into two primary categories based on their control flow handling. On the one hand, *classical control* [Selinger 2004] involves quantum operations executed on a specialized device within a classical computer. The classical computer manages program execution by instructing which quantum operation to apply to specific qubits. This approach resembles circuit description languages that use high-level operations on quantum circuits, with examples such as the quantum lambda calculus [Selinger and Valiron 2006], Quipper [Green et al. 2013], and Qwire [Paykin et al. 2017]. Ensuring physical implementability typically involves constraints and linearity-based type systems on quantum data to maintain essential quantum physics properties such as the no-cloning theorem [Wooters and Zurek 1982]. Notably, this category accommodates models like QRAM [Knill 1996].

On the other hand, *quantum control* [Díaz-Caro 2021] allows programming quantum operations based on quantum data, a fundamental concept in quantum computing. For example, the CNOT operation governs the application of a NOT operation based on a control qubit. More advanced examples like the Quantum Switch [Procopio et al. 2015; Rubino et al. 2017] have gained popularity, enabling the application of two operations in different orders based on a control qubit.

While both categories offer equivalent computational power, quantum control provides a more natural approach, allowing programs to be “fully quantum” with operational control flow over

Partially funded by the French-Argentinian IRP SINFIN. Díaz-Caro is also funded by PICT 2021-I-A-00090 and 2019-1272, and PIP 11220200100368CO.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

© 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM XXXX-XXXX/2024/3-ART

https://doi.org/XXXXXXX.XXXXXXX
quantum data. Programming languages like QML [Altenkirch and Grattage 2005], Lambda-$S_1$ [Díaz-Caro and 2022], and Qunity [Voichick et al. 2023] fall into this category. These programs must overcome significant constraints to ensure physical implementability, particularly in terms of efficient compilation into quantum circuits or low-level models like QRAM.

**Unitarity.** One major issue in quantum control is ensuring unitarity, a fundamental property of quantum systems that maintains the total probability of all possible outcomes over time. Quantum gates in circuits are represented by unitary maps, preserving $\ell^2$-norm and orthogonality. However, representing quantum data as linear combinations in a Hilbert space leads to a problem: programs must have an $\ell^2$-norm of 1 (i.e., must lie in the unitary sphere) to be physically realizable, often requiring orthogonality among program branches. This property is generally not preserved by program semantics, leading to the need to restrict programs to those satisfying unitarity. The question of ensuring this restriction through type systems has been first explored by [Altenkirch and Grattage 2005] to some extent, and more recently by [Díaz-Caro et al. 2019b], characterizing superpositions and isometries with realizability techniques [Miquel 2011; Van Oosten 2008]. In this realizability model, types are interpreted as subsets of a vector space's unit sphere, with all typed terms preserving the $\ell^2$-norm, and quantum data expressed as superpositions of classical data types. The corresponding typing discipline, that is in a way the dual to Intuitionistic Linear Logic [Girard and Lafont 1987; Hyland and de Paiva 1993], has been introduced in [Díaz-Caro and Malherbe 2022] to delineate a programming language for unitarity called Lambda-$S_1$.

**Feasibility.** While unitarity is essential for quantum program implementability, it is insufficient. Feasibility [Gurevich 1983] (or tractability), the property that a program can be executed within reasonable time and space-constraints, is equally crucial. Compiling quantum programs to low-level models, like quantum circuits, requires imposing restrictions on qubit count, gate count, and error rates. Achieving feasibility involves studying program computational complexity, typically related to polynomial-depth uniform circuit families. Yao's Theorem [Yao 1993] links such families to Bounded-error Quantum Polynomial time (BQP) [Bernstein and Vazirani 1997], a quantum analogue of the probabilistic complexity class BPP. Feasibility has deep roots in classical complexity, leading to fields like descriptive complexity [Immerman 1999] and implicit computational complexity [Péchoux 2020] characterizing complexity classes logically and through programming languages.

Previous work [Dal Lago et al. 2010], based on light linear logic [Girard 1998], characterizes polynomial time in quantum lambda calculus. However, no type system currently ensures quantum program feasibility with quantum control. Thus, a major problem in quantum computing is to develop programming languages with quantum control, typed in such a way as to ensure both unitarity and feasibility of the programmed functions, so that they have a physical implementation that does not break the laws of quantum mechanics, and can (at least in principle) be efficiently compiled into a circuit.

## 1.2 Contribution

We present PUNQ, a typed quantum programming language with quantum control addressing unitarity and feasibility. Quantum control employs a quantum conditional inspired by QML [Altenkirch and Grattage 2005], producing superposed outputs from superposed inputs. Unitarity is achieved via a variant of Lambda-$S_1$ [Díaz-Caro and Malherbe 2022], introducing a modality $\#A$ for superpositions, addressing quantum no-cloning. This modality marks non-duplicable types, treating superpositions of type $\#A$ linearly. Only terms of types distinct from $\#A$ can be duplicated. For example, $\#B$ denotes superpositions of Booleans (qubits), and realizers of $\#B \to \#B$ represent single-qubit
quantum gates. Feasibility is ensured by a variant of the Dual Light Affine Logic type system (DLAL) [Baillot and Terui 2009], employing a modality § to account for potential duplication and a duality à la [Barber and Plotkin 1996], with two arrows corresponding to a non-linear context and a linear context, respectively. In this setting, linear arrows are strictly linear to preserve unitarity and non-linear arrows cannot be applied to superpositions, thus, ensuring the no-cloning principle of quantum mechanics.

The main contributions of this paper are:

* a new typed programming language with quantum control that enjoys subject reduction (Theorem 3.3) and progress (Theorem 3.4),

* a soundness result (Theorem 5.6) showing that typable linear maps over qubits encode isometries and unitary operators when dimensions match,

* a completeness result (Theorem 5.7) stating that any isometry can be encoded by a PUNQ program,

* a non-separability result (Theorem 5.8): there is no linear map that can separate qubits,

* a feasibility result (Theorem 6.12), ensuring polynomial time normalization and polynomially bounded size of normal forms,

* a complexity result for type checking over three fragments of PUNQ (Theorem 7.7). We identify two fragments in which we can check orthogonality in polytime and one in which it is potentially undecidable (Lemma 7.6), and give examples of the expressivity of each fragment.

In summary, PUNQ can be viewed as the first feasible and physically realistic quantum programming language with quantum control. We provide several simple examples to illustrate our results: towards completeness, we show that standard one and two-qubit gates can be simulated by programs (Examples 4.2, 4.3, and 4.4), we provide the encoding of a simple quantum teleportation protocol (Example 4.5) illustrating that soundness can be used to certify unitarity, we also provide a quantum random walk algorithm (Example 4.6) illustrating polynomial time normalization.

## 1.3 Related Work

*Quantum control and unitarity.* QML [Altenkirch and Grattage 2005] was the pioneering language to introduce a quantum if-statement, enabling superposition in branches based on the superposition in the if-statement guard. The $ℓ^2$-norm preservation is ensured through a semantic notion of validity: an if-statement is valid when its branches are orthogonal, effectively reducing the two branches to orthogonal values. Another approach for handling quantum control and superpositions, which is less semantics-driven, is the introduction of Lineal [Arrighi and Dowek 2017]. It is an untyped lambda calculus extended with superpositions of terms. Lineal strictly covers measurement-free quantum programs, as it does not involve orthogonality checks and does not enforce superpositions to have norm 1. However, it treats function application linearly, providing a generalization of the QML if-statement. Lambda-$S_1$ [Díaz-Caro et al. 2019b; Díaz-Caro and Malherbe 2022], as well as the current work, can be seen as the $ℓ^2$-norm preserving restriction of Lineal. Lambda-$S$ [Díaz-Caro et al. 2019a; Díaz-Caro and Malherbe 2023], a preliminary version of this typing discipline, does not ensure unitarity but includes measurements. Qunity [Voichick et al. 2023] enforces the no-cloning property using constrained sharing, allowing duplicated variables to produce only entangled states in a basis-dependent way. While this ensures that well-typed programs in Qunity have a quantum circuit representation, the typing does not guarantee any resource bound, neither on the time complexity of the programs, nor on the size of the compiled circuit. There have also been attempts [Ying 2016] to define a notion of “quantum alternation” allowing measurements to be quantum-controlled, where the resulting system is not monotone
<figure><img src="image_1.png" /><figcaption>Fig. 1. Quantum search algorithm.</figcaption></figure>

with respect to the Löowner order and, hence, cannot be considered to be a physically feasible concept [Badescu and Panangaden 2015]. An alternative approach in [Yuan et al. 2023] characterizes unitarity using a model based on injective semantics. Complementary approaches following the ZX-calculus research line provide graphical languages for quantum control with quantum tests [Chardonnet 2023; Chardonnet et al. 2022]. Currently, none of the mentioned systems can guarantee the feasibility of their programs in terms of complexity or resource requirements.

*Quantum complexity classes.* Programming-language-based characterizations of well-known complexity classes have been deeply studied in the field of Implicit Computational Complexity (see [Péchoux 2020] for a survey). To mention a few of them, [Bellantoni and Cook 1992] provided the first implicit (i.e., where the complexity bound does not need to be explicited by the programmer) characterization of polynomial time and [Gaboardi et al. 2008] is the first lambda-calculus characterization of polynomial space. Although a great deal of work has been done in this field over the last three decades, only a small number of it has focused on the quantum paradigm. The paper [Dal Lago et al. 2010] characterizes BQP on the quantum lambda-calculus. However, due to the presence of unrestricted measurement, this classically-controlled system cannot guarantee unitarity. Finally, [Hainry et al. 2023; Yamakami 2020] provide two characterizations of FBQP with quantum control which are restricted to first-order.

## 1.4 Illustrating Example: Grover's Quantum Search Algorithm

As an example of a PUNQ program, we will consider the algorithm for quantum search [Grover 1996]. We are given a function $f: \{0, 1\}^n \to \{0, 1\}$ such that, for exactly one input $w \in \{0, 1\}^n$, we have that $f(w) = 1$. In the classical case, finding $w$ among $N \triangleq 2^n$ possibilities has average complexity $O(N)$, whereas using Grover's algorithm for quantum search, the value of $w$ can be found with high probability with only $O(\sqrt{N})$ operations (see Figure 1).

Let $\mathbb{B}$ be the type of Booleans. For $n \ge 1$, define the type of tuples of bits as $\mathbb{B}^{n+1} \triangleq \mathbb{B} \times \mathbb{B}^n$ with $\mathbb{B}^1 \triangleq \mathbb{B}$. The type $\#\mathbb{B}$ corresponds to qubits and $\#(\mathbb{B}^n)$, with $n \ge 1$, is the type of a tuple of $n$ (possibly entangled) qubits. For example, a superposition $|\pm\rangle \triangleq \frac{1}{\sqrt{2}} \cdot |0\rangle \pm \frac{1}{\sqrt{2}} \cdot |1\rangle$ has type $\#\mathbb{B}$ and, given a string $x = x_1 \dots x_n \in \{0, 1\}^n$, the tensor product state $|x\rangle \triangleq |x_1\rangle \otimes \dots \otimes |x_n\rangle$ can be encoded by a term of type $\#(\mathbb{B}^n)$.

We will now describe a PUNQ term encoding the algorithm for Grover search in the case $n = 2$. A very basic component is the Hadamard transformation

$$ H \triangleq \lambda x. \text{if } x \text{ then } |+\rangle \text{else } |-\rangle: \#\mathbb{B} \to \#\mathbb{B}, $$

described in more detail in Example 4.2. Intuitively, the type $\#(\mathbb{B}^n) \to \#(\mathbb{B}^n)$ corresponds to linear maps (unitary gates) over $n \ge 1$ qubits. The if construction assigns the first case to state $|0\rangle$ and
the second to $|1\rangle$. Therefore, for $\alpha, \beta \in \mathbb{C}$, we have the reduction

$$H (\alpha | 0 \rangle + \beta | 1 \rangle) \rightsquigarrow \alpha \cdot \text{if } |0\rangle \text{ then } |+\rangle \text{ else } |1\rangle + \beta \cdot \text{if } |1\rangle \text{ then } |+\rangle \text{ else } |1\rangle \rightsquigarrow \alpha \cdot |+\rangle + \beta \cdot |-\rangle$$

We can then easily design a term applying the Hadamard gate to two qubits

$$H_2 \triangleq \lambda z.\text{let } (x, y) = z \text{ in } (H x, H y) : \#(\mathbb{B}^2) \to \#(\mathbb{B}^2).$$

We can likewise define the phase shift operator $P$, where $P|x\rangle \triangleq -|x\rangle$ for all $x \neq 0^n$ and $P|0^n\rangle \triangleq |0^n\rangle$. For $n=2$, we can encode $P$ by the term Phase : $\#(\mathbb{B}^2) \to \#(\mathbb{B}^2)$:

$$\text{Phase} \triangleq \lambda z.\text{let } (x, y) = z \text{ in if } x \text{ then (if } y \text{ then } (|0\rangle, |0\rangle) \text{ else } -1 \cdot (|0\rangle, |1\rangle) \text{ else } -1 \cdot (|1\rangle, y)$$

We will consider an oracle for $f$ given by a unitary $O$ where $O|x\rangle \triangleq (-1)^{f(x)}|x\rangle$, for all $x \in \{0,1\}^n$, i.e., where the oracle acts as the identity for all basis states except for $w$, on which it performs a phase shift of -1. This represents a unitary gate of dimension $n$, and therefore there exists a PUNQ term, say Oracle, with type $\#(\mathbb{B}^n) \to \#(\mathbb{B}^n)$, that encodes it. We may now define the Grover iteration step in the algorithm:

$$\text{Grover} \triangleq \lambda x.H_2(\text{Phase}(H_2(\text{Oracle } x))) : \#(\mathbb{B}^2) \to \#(\mathbb{B}^2).$$

In order to iterate the Grover step, we use the Church numeral encoding $\underline{n} \triangleq \lambda f.\lambda x.f^n(x)$ with type $\underline{N} \triangleq \forall X.(X \to X) \Rightarrow \S(X \to X)$. The type of Church numerals makes use of two extra constructs: a non-linear arrow $\Rightarrow$, whose input cannot be quantum data (superpositions), so that PUNQ programs preserve the laws of quantum mechanics (e.g. no-cloning); a modality $\S$ from Girard's light linear logic [Girard 1998], accounting for possible duplication in a term.

This term can be applied to our term Grover with the substitution $X = \#(\mathbb{B}^2)$. Notice that it does not break no-cloning as it roughly corresponds to a term of type $(\#(\mathbb{B}^2) \to \#(\mathbb{B}^2)) \Rightarrow \S(\#(\mathbb{B}^2) \to \#(\mathbb{B}^2))$, whose input can be duplicated. Indeed, the input here is a quantum gate of type $(\#(\mathbb{B}^2) \to \#(\mathbb{B}^2))$ which does not constitute quantum data.

As such, we obtain the final term:

$$\text{Search} \triangleq \lambda m.\lambda x.(m \text{ Grover})(H_2 x) : \underline{N} \to \S\#(\mathbb{B}^2) \to \S\#(\mathbb{B}^2).$$

The term Search $\underline{m} : \S\#(\mathbb{B}^2) \to \S\#(\mathbb{B}^2)$ simulates a precise run of $m$ iterations and produces as output a possibly entangled two-qubit state – which is indeed the output before we perform any measurements.

The non-trivial properties ensured by our type discipline on the above term are the following:

* By Theorem 5.6, for any given integer $m$, since the term Search $\underline{m}$ has type $\S\#(\mathbb{B}^2) \to \S\#(\mathbb{B}^2)$, it represents a unitary transformation with algebraic coefficients (we will later put a restriction on complex numbers to avoid the consideration of non-computable numbers), which can therefore be physically implemented in a quantum circuit, such as Figure 1.

* By Theorem 6.12 (Polynomial time normalization) the PUNQ type discipline ensures that the typed term Search $\underline{m}(|0\rangle, |0\rangle) : \S\#(\mathbb{B}^2)$ reduces to a normal form $\sum_{i,j \in \{0,1\}} \alpha_{ij} \cdot (|i\rangle, |j\rangle)$ in a number of steps that is polynomial on the original size of the term (in this case, the number of Grover iterations is linear on the parameter $m$ given – for a more elaborate iteration example, see Example 4.6). Notice that this property remains valid for any (possibly entangled) pair encoding a two-qubit state given as input.

# 2 A PROGRAMMING LANGUAGE WITH QUANTUM CONTROL

## 2.1 Syntax

PUNQ (short for Polytime UNitary Quantum language) is a programming language with syntax defined by the grammar in Figure 2. A term can take the form of a variable $x$, a bit $|0\rangle$ or $|1\rangle$,
(Terms) $T \ni t := x \mid |0\rangle \mid |1\rangle \mid \text{if } t \text{ then } \vec{t} \text{ else } \tilde{t} \mid \lambda x.\tilde{t} \mid t \ t \ (t, t) \mid \text{let } (x, y) = t \ \text{in } \tilde{t}$

(Superpositions) $S \ni \vec{t} := t \mid \vec{0} \mid \alpha \cdot \vec{t} \mid \vec{t} + \tilde{t}$

(Basis values) $BV \ni v := |0\rangle \mid |1\rangle \mid \lambda x.\tilde{t} \mid (v, v)$

(Values) $V \ni \vec{v} := v \mid \vec{0} \mid \alpha \cdot \vec{v} \mid \vec{v} + \tilde{v}$

<caption>Fig. 2. Syntax of PUNQ programs.</caption>

a conditional statement, an abstraction, an application, a pair, or a pair destructor. We denote the set of terms as $T$, and the terms are denoted by $r$, $s$, $t_1$, $t_2$, and so on. A superposition can be either a term $t$, the null vector $\vec{0}$, the product $\alpha \cdot \vec{t}$ of a superposition $\vec{t}$ with an algebraic number $\alpha \in \mathbb{Q}$ [Adleman et al. 1997], or the sum $\vec{t}_1 + \vec{t}_2$ of two superpositions. We represent the set of superpositions as $S$, and superpositions themselves are denoted by $\vec{r}$, $\vec{s}$, $\vec{t}_1$, $\vec{t}_2$, and so forth. In essence, terms correspond to objects that can reduce classically, possibly to a superposition, while superpositions represent quantum computations. We define the sets $BV$ and $V$ as the sets of basis values and values, respectively. Basis values are a subset of terms in normal form, and values are superpositions of basis values. We use $v$, $w$, $v_1$, $v_2$, and so on for basis values, while $\vec{v}$, $\vec{w}$, $\vec{v}_1$, $\vec{v}_2$, and so on, denote values.

A variable is free in a superposition if it is not bound by an abstraction or a pair destructor. We denote the set of free variables in the superposition $\vec{t}$ as $FV(\vec{t})$. A superposition is closed if it contains no free variables. Given a set $S$ of superpositions, we define $S_c$ as the set of closed superpositions within $S$. A PUNQ program is a closed superposition in $S_c$ that can be assigned a type according to the type discipline presented in Section 3.

The size of a superposition $\vec{t}$, denoted $|\vec{t}|$, is the maximal size of its superposed terms. Formally,

$$ 
\begin{array}{l@{\qquad}l}
|x| \triangleq 1 & |t_1 \ t_2| = |(t_1, t_2)| \triangleq |t_1| + |t_2| + 1 \\
| |0\rangle | \triangleq 1 & |\text{let } (x, y) = t \ \text{in } \vec{t}| \triangleq 1 + |t| + |\vec{t}| \\
| |1\rangle | \triangleq 1 & |\vec{0}| \triangleq 0 \\
| \text{if } t \ \text{then } \vec{t}_1 \ \text{else } \vec{t}_2| \triangleq 1 + |t| + \max(|\vec{t}_1|, |\vec{t}_2|) & |\alpha \cdot \vec{t}| \triangleq |\vec{t}| \\
& |\vec{t}_1 + \vec{t}_2| \triangleq \max(|\vec{t}_1|, |\vec{t}_2|)
\end{array}
$$

The set $S$ of superpositions has the structure of a vector space and, consequently, we define an
equivalence relation $\equiv$ on $S$ as follows:

$$ 
\begin{array}{l@{\qquad}l}
\vec{t}_1 + \vec{t}_2 \equiv \vec{t}_2 + \vec{t}_1 & (\vec{t}_1 + \vec{t}_2) + \vec{t}_3 \equiv \vec{t}_1 + (\vec{t}_2 + \vec{t}_3) \\
\vec{0} + \vec{t} \equiv \vec{t} & 0 \cdot \vec{t} \equiv \vec{0} \\
1 \cdot \vec{t} \equiv \vec{t} & \alpha \cdot (\beta \cdot \vec{t}) \equiv \alpha\beta \cdot \vec{t} \\
\alpha \cdot \vec{t} + \beta \cdot \vec{t} \equiv (\alpha + \beta) \cdot \vec{t} & \alpha \cdot (\vec{t}_1 + \vec{t}_2) \equiv \alpha \cdot \vec{t}_1 + \alpha \cdot \vec{t}_2
\end{array}
$$

This also implies that the summation symbol $\Sigma$ can be used unambiguously. A superposition $\vec{t}$
is in canonical form if it is either $\vec{0}$ or $\vec{t} = \sum_{i=1}^n \alpha_i \cdot t_i$, where $\forall i \neq j$, $t_i \neq t_j$, and $\forall i, \alpha_i \neq 0$. The
canonical form of a superposition $\vec{t}$ is unique, modulo associativity and commutativity. We denote
the set of canonical forms as CF. We also define the syntactic sugar given in Figure 3.

## 2.2 Operational Semantics

The semantics of PUNQ programs is defined by the rewrite relation $\rightsquigarrow \subseteq S_c \times S_c$, given in Figure 4.
We denote its reflexive and transitive closure as $\rightsquigarrow^*$.
if $\sum_{i=1}^{n} \alpha_i \cdot s_i$ then $\vec{r}_1$ else $\vec{r}_2 \triangleq \sum_{i=1}^{n} \alpha_i \cdot \text{if } s_i$ then $\vec{r}_1$ else $\vec{r}_2$

$$s \left( \sum_{i=1}^{n} \alpha_i \cdot t_i \right) \triangleq \sum_{i=1}^{n} \alpha_i \cdot s \, t_j$$

$$\left( \sum_{i=1}^{n} \alpha_i \cdot s_i, \sum_{j=1}^{m} \beta_j \cdot t_j \right) \triangleq \sum_{i=1}^{n} \sum_{j=1}^{m} \alpha_i \beta_j \cdot (s_i, t_j)$$

$$\text{let } (x, y) = \sum_{i=1}^{n} \alpha_i \cdot s_i \text{ in } \vec{r} \triangleq \sum_{i=1}^{n} \alpha_i \cdot (\text{let } (x, y) = s_i \text{ in } \vec{r})$$

<figure><img src="image_2.png" /><figcaption>Fig. 4. Semantics of PUNQ programs.</figcaption></figure>

It is important to emphasize that the syntactic sugar defined in Figure 3 is used in the reduction rules (If+), (App), (Appv), (Pair), (Pairv), and (Let+) to simplify notations. For instance, the reduction of rule (If+) can be written as

$$\frac{t \rightsquigarrow \sum_i \alpha_i \cdot s_i}{\text{if } t \text{ then } \vec{r}_1 \text{ else } \vec{r}_2 \rightsquigarrow \sum_i \alpha_i \cdot \text{if } s_i \text{ then } \vec{r}_1 \text{ else } \vec{r}_2} \quad (\text{If}_+)$$

Therefore, reductions through $\rightsquigarrow$ do not generate terms or superpositions that are not syntactically valid. Another crucial point to note is that the relation $\rightsquigarrow$ is constrained to canonical forms in rule (Sup) to prevent the reduction of a superposition in the form $v + 0 \cdot t$, where $t \in \mathbf{T}$, $v \in \mathbf{V}$, as it is true that $v + 0 \cdot t \equiv v$ and, as a result, $v + 0 \cdot t$ should not reduce.

The semantics of PUNQ is call-by-value. Since there is an established strategy, the confluence of this calculus is trivial. The normal forms are closed values and they are unique modulo the equivalence relation $\equiv$.
## 3 A TYPE SYSTEM FOR UNITARITY AND POLYTIME NORMALIZATION

In this section, we introduce a type system ensuring that typable closed superpositions:

* encode unitary transformations on the type of circuits over qubits (i.e., linear functions from qubits to qubits) (Section 5);

* normalize in time polynomial in their size, exhibiting only polynomial growth on the size of the superposition (Section 6).

The typing discipline is created by mixing the unitary-ensuring type system of Lambda-$S_1$ [Díaz-Caro and Malac 2022] together with the polytime strong normalization properties of the DLAL [Baillot and Terui 2009] type system.

### 3.1 Types, Judgments, and Environments

The set $T$ of types in PUNQ is generated by the following grammars:

$$ 
\begin{array}{ll}
(\text{PUNQ types}) & T \ni A, B, C, \dots := X \mid A \dasharrow A \mid A \Rightarrow A \mid A \times A \mid Q \mid \$A \mid \forall X.A \\
(\text{Ground types}) & Q, R, S, \dots := \mathbb{B} \mid \sharp Q \mid \$Q \mid Q \times Q
\end{array}
$$

We use $A, B, C$, and so on for PUNQ types, and $Q, R, S, \dots$ for ground types. Types include type variables $X$, a basic type $\mathbb{B}$ for bits, a linear arrow $\dasharrow$, an intuitionistic arrow $\Rightarrow$, a type construct $\times$ for pairs corresponding to the tensor product of linear logic (we do not use the tensor notation of linear logic to avoid confusion as pairs only correspond to separable states), a modality $\sharp$ for superpositions, a modality $\$A$ as a marker for possible duplication, and polymorphism. The set of closed types is denoted as $T_c$. Ground types $Q$ represent all types that can be inhabited by tuples of qubits. Intuitively, objects of type $\sharp Q$ are unitary superpositions of elements of type $Q$ and hence cannot be cloned (i.e., duplicated). For example, $\sharp \mathbb{B}$ is the type of a unitary superposition of bits, i.e., qubits. Qubits correspond to values whose canonical forms are of the shape $\alpha \cdot |0\rangle + \beta \cdot |1\rangle$, with $\alpha, \beta \in \overline{\mathbb{Q}}$ and $|\alpha|^2 + |\beta|^2 = 1$. We write $A^n$, with $n \ge 1$, as a shorthand for $A \times \dots \times A$, $n$ times. The type $\sharp(\mathbb{B}^n) \dasharrow \sharp(\mathbb{B}^n)$ corresponds to quantum circuits over $n$ qubits. Finally, a type of the form $\sharp \mathbb{B} \Rightarrow A$, for any type $A$, will be disallowed by the typing discipline as $\Rightarrow$ is not linear and hence could involve duplication or deletion of the input.

A *typing environment* $\Gamma$ is a mapping from variables to closed types in $T_c$ and is sometimes written as $x_1 : A_1, \dots, x_n : A_n$. The notation $\Gamma, \Delta$ represents the disjoint union of the typing environments $\Gamma$ and $\Delta$. We write as $FV(\Gamma)$ the set of free type variables appearing in $\Gamma$.

*Typing judgments* are of the form $\Gamma; \Delta \vdash \vec{t} : A$, where $\Gamma$ and $\Delta$ are disjoint typing environments, $\vec{t}$ is a superposition, and $A$ is a type. Here, $\Gamma$ is referred to as the *exponential context*, and $\Delta$ is the *linear context*.

### 3.2 Orthogonality

We define the inner product $\langle -| - \rangle : V_c \times V_c \to \overline{\mathbb{Q}}$ over closed values as

$$ \left\langle \sum_{i=1}^{n} \alpha_i \cdot v_i \mid \sum_{j=1}^{m} \beta_j \cdot w_j \right\rangle \triangleq \sum_{i=1}^{n} \sum_{j=1}^{m} \overline{\alpha_i \beta_j} \delta_{v_i, w_j}, \qquad \langle \vec{v} | \vec{0} \rangle = \langle \overline{0} | \vec{v} \rangle \triangleq 0, $$

where $\delta_{x,y}$ is the Kronecker delta that is equal to 1 if $x = y$ and 0 otherwise. Notice that inner product is obviously preserved by the equivalence relation $\equiv$ on the vector space of values. Hence $V_c$ is a Hilbert space as $\ell^2(V_c) = V_c$.

Type checking a superposition will require that we are able to test orthogonality between terms. This is straightforward to do for values in normal form, but we may also face the situation where
<table><caption>Fig. 5. Subtyping relation.</caption><tr><td>A' &le; A<br>A &rarr; B &le; A' &rarr; B'</td><td>B &le; B'<br>A &rarr; B &le; A' &rarr; B'</td><td>A' &le; A<br>A &rarr; B &le; A' &rarr; B'</td><td>B &le; B'<br>A &times; B &le; A' &times; B'</td><td>A &le; B<br>S &le; S'<br>A &le; B<br>&forall;X.A &le; &forall;X.B</td></tr><tr><td>A &le; A</td><td>Q &le; &#8455;Q</td><td>#&#8455;Q &le; &#8455;Q</td><td>Q &le; &#8455;!(Q)</td><td>A &le; B<br>B &le; C<br>&forall;X.A &le; &forall;X.<br>A &le; C</td></tr></table>

a term correctly represents a superposition, and yet it is not fully reduced, such as the term $\frac{1}{\sqrt{2}}(\lambda x.x)|0\rangle + \frac{1}{\sqrt{2}}|1\rangle$. Therefore, we use the following definition of orthogonality between terms.

**Definition 3.1 (Orthogonality).** The orthogonality relation $\perp \subseteq S_c \times S_c$ is defined as $\vec{t} \perp \vec{s}$ if and only if $\vec{t} \rightsquigarrow^* \vec{v}$, $\vec{s} \rightsquigarrow^* \vec{w}$ and $\langle \vec{v} | \vec{w} \rangle = 0$.

For a given typing environment $\Gamma$, let $\sigma_{\Gamma}$ denote a type-preserving substitution of variables in $\Gamma$ by closed basis values. The orthogonality relation can be extended to any two superpositions $\vec{t}, \vec{s} \in S$ such that $\Gamma; \Delta \vdash \vec{t} : A$ and $\Gamma; \Delta \vdash \vec{s} : A$ by defining $(\vec{t} \perp_A^{\Gamma, \Delta} \vec{s}) \text{ iff } \forall \sigma_{\Gamma \cup \Delta}, \vec{t} \sigma_{\Gamma \cup \Delta} \perp_A \vec{s} \sigma_{\Gamma \cup \Delta}$.

## 3.3 Type System

We introduce a bang function on types, which the type system utilizes to remove the # modalities when they correspond to a non-linear use.

**Definition 3.2 (Bang function).** The function $! : T \to T$ is an endomorphism on types defined as

$$ 
\begin{aligned}
! (X) &\triangleq X & ! (\mathbb{B}) &\triangleq \mathbb{B} \\
! (A \to B) &\triangleq A \to B & ! (A \Rightarrow B) &\triangleq A \Rightarrow B \\
! (A \times B) &\triangleq ! (A) \times ! (B) & ! (\# Q) &\triangleq ! (Q) \\
! (\# A) &\triangleq \# (A) & ! (\forall X.A) &\triangleq \forall X. ! (A)
\end{aligned}
$$

This function is reminiscent of the bang modality in linear logic [Girard 1987] because it transforms a non-clonable type (non-duplicable type, e.g., superposition) into a clonable type (duplicable type). Therefore, it corresponds to withdrawing # modalities. For instance, $! (\# \mathbb{B}) = \mathbb{B}$ represents the type of bits and is clonable. Similarly, $! (\# \mathbb{B} \to \# \mathbb{B}) = \# \mathbb{B} \to \# \mathbb{B}$ is the type of unitary maps on qubits (see Theorem 5.6), which is clonable by default.

The subtyping relation $\leq \subseteq T \times T$ is defined in Figure 5. The intuition behind this relation is as follows: if a type $Q$ is considered as the base of a vector space for its values, then $\#Q$ results in the intersection of the span of $A$ with the unitary sphere, that is, complex linear combinations of objects of type $A$ with unit norm. Therefore, $\leq$ corresponds to set inclusion, and it holds that $Q \leq \#Q$ and $\#Q = \#\#Q$. Additionally, it can be shown that $\#Q \times \#R \leq \#(! (Q) \times ! (R))$, implying the desirable property that the vector space of separable qubits $\#\mathbb{B} \times \#\mathbb{B}$ is included in the vector space of 2 qubits $\#(\mathbb{B} \times \mathbb{B})$.

Since the ! function will only be used in the double arrow in rule introduction ($\Rightarrow_i$) on the left of that arrow, the double arrow carries all the information about whether the ! function was applied. Therefore, ! is not treated as a modality and appears implicitly in type substitution. Given a type $C$ and a variable $X$, let $[C/X]$ represent the type substitution $\sigma^+$. It is inductively defined on types
(up to α-renaming) as follows:

$$
\begin{align*}
\sigma^k(Y) &\triangleq Y, \text{ with } Y \neq X, & \sigma^k(A \Rightarrow B) &\triangleq \sigma^-(A) \Rightarrow \sigma^+(B), \\
\sigma^+(X) &\triangleq C, & \sigma^k(\#Q) &\triangleq \#\sigma^k(Q), \\
\sigma^-(X) &\triangleq !\langle C \rangle, & \sigma^k(\S A) &\triangleq \S\sigma^k(A), \\
\sigma^k(\mathbb{B}) &\triangleq \mathbb{B}, & \sigma^k(A \times B) &\triangleq \sigma^k(A) \times \sigma^k(B), \\
\sigma^k(A \to B) &\triangleq \sigma^k(A) \to \sigma^k(B), & \sigma^k(\forall Y.A) &\triangleq \forall Y.\sigma^k(A),
\end{align*}
$$

where $k \in \{+, -\}$ and $!$ is the bang function from Definition 3.2. This ensures that non-clonability is preserved on inputs to non-linear applications, e.g., $(X \Rightarrow X)[\#\mathbb{B}/X] = \sigma^{-}(X) \Rightarrow \sigma^{+}(X) = !([\#\mathbb{B}]) \Rightarrow \#\mathbb{B} = \mathbb{B} \Rightarrow \#\mathbb{B}$.

The typing rules are provided in Figure 6. PUNQ is the set of typable closed superpositions in $S_c$.

Several key points are worth highlighting: (i) The ! function is employed in rule (⇒ᵢ) to ensure the no-cloning property. (ii) In rule (⇒ₑ), the notation [z : C] indicates that the variable z is optional: it can either appear in both the hypothesis and the conclusion of the rule or not at all. The variable z is then passed to the exponential context in the conclusion of the rule. Consequently, qubits are treated linearly following the DLAL type discipline, and they cannot be cloned by side effect. For instance, if z is of type #B, then λz.t s is of type B ⇒ B, as per rule (⇒ᵢ). (iii) Rules (if#) and (#i) are the only two rules that make use of the orthogonality predicate ⊥A ⊆ T_c × T_c. (iv) Rule (#i) disallows superposing arrow types. (v) Rule (∀ₑ) utilizes the type substitution [B/X].

PUNQ enjoys the following standards properties.

**THEOREM 3.3 (SUBJECT REDUCTION).** If; ⊢ ⃗t : A and ⃗t ↛ ⃗r, then; ⊢ ⃗r : A.

**PROOF.** By induction on the relation ↛. The full proof, including the needed substitution lemma, is given in Appendix A.1. □

**THEOREM 3.4 (PROGRESS).** If; ⊢ ⃗t : A, then either ⃗t ↛ ⃗r for some ⃗r or ⃗t ∈ V.

**PROOF.** By induction on the structure of ⃗t. Full proof given in Appendix A.1. □

## 3.4 Intuitions

Most rules in Figure 6 are reminiscent of the typing discipline of Dual Light Affine Logic [Baillot and Terui 2009], extended with multiplicative pairs (cf. Figure 10). The weakening rule (W) and contraction rule (C) are limited to exponential contexts since discarding or duplicating a qubit would break unitarity. In our setting, the typing rules are linear in the linear context.

Rule (≡) guarantees a type preservation property on the vector space of superpositions. This rule is crucial for subject reduction. Indeed, terms of a typable superposition must have a norm of 1 (by rule (#i)), preventing a superposition of the form $\frac{1}{2} \cdot t + \frac{1}{2} \cdot t$ from typing, even though it may be obtained as a reduct of the operational semantics. An alternative approach could have been restricting the relation ↛ to pairs of canonical forms in $S_c/≡ \times S_c/≡$ and evaluating arbitrary superpositions only using their canonical representative.

Rule (≤) is the subtyping rule, allowing the system to handle entangled datatypes.

The typing rules (if) and (if#) are additive rules for conditionals on type A controlled by classical data B and quantum data #B, respectively. In this latter case, the conditional evaluates to a superposition of conditionals, as per rule (If+) in Figure 4. Hence, the result has type #A.

The typing rules for linear and intuitionistic arrows resemble those in [Barber and Plotkin 1996], with the additional requirement that the introduction and elimination of the intuitionistic arrow,
$$ \frac{\Gamma; \Delta \vdash \vec{t} : A}{\Gamma, \Gamma'; \Delta \vdash \vec{t} : A} (W) $$

$$ \frac{\Gamma, x : B, y : B; \Delta \vdash \vec{t} : A}{\Gamma, x : B; \Delta \vdash \vec{t}[x/y] : A} (C) $$

$$ \frac{\Gamma; \Delta \vdash \vec{t} : A \quad \vec{t} \equiv \vec{s}}{\Gamma; \Delta \vdash \vec{s} : A} (\equiv) $$

$$ \frac{\Gamma; \Delta \vdash \vec{t} : A \quad A \leq B}{\Gamma; \Delta \vdash \vec{t} : B} (\leq) $$

$$ \overline{; x : A \vdash x : A} (Ax) $$

$$ \overline{; \vdash |0\rangle : \mathbb{B}} (0) $$

$$ \overline{; \vdash |1\rangle : \mathbb{B}} (1) $$

$$ \frac{\Gamma; \Delta \vdash t : \#\mathbb{B} \quad \Gamma'; \Delta' ; \vdash \vec{s}_1 : Q \quad \Gamma'; \Delta' ; \vdash \vec{s}_2 : Q \quad \vec{s}_1 \perp^{\Gamma'; \Delta'} \vec{s}_2}{\Gamma, \Gamma'; \Delta, \Delta' \vdash \text{ if } t \text{ then } \vec{s}_1 \text{ else } \vec{s}_2 : \#Q} (\text{if}\#) $$

$$ \frac{\Gamma; \Delta \vdash \vec{t} : A}{\Gamma; \delta \Delta \vdash \vec{t} : \delta A} (\delta_i) $$

$$ \frac{\Gamma; \Delta \vdash t : \mathbb{B} \quad \Gamma'; \Delta' \vdash \vec{s}_1 : A \quad \Gamma'; \Delta' \vdash \vec{s}_2 : A}{\Gamma, \Gamma'; \Delta \vdash \text{ if } t \text{ then } \vec{s}_1 \text{ else } \vec{s}_2 : A} (\text{if}) $$

$$ \frac{\Gamma; \Delta \vdash s : \delta B \quad \Gamma'; \Delta' ; \vdash x : \delta B \vdash t : A}{\Gamma, \Gamma'; \Delta, \Delta' \vdash t[s/x] : A} (\delta_e) $$

$$ \frac{\Gamma; \Delta \vdash \vec{t} : A \quad X \notin \mathit{FV}(\Gamma, \Delta)}{\Gamma; \Delta \vdash \vec{t} : \forall X.A} (\forall_i) $$

$$ \frac{\forall i, \Gamma; \Delta \vdash \vec{t}_i : Q \quad \forall j \neq k, \vec{t}_j \perp^{\Gamma; \Delta} \vec{t}_k \quad \sum_{i=1}^{n} |\alpha_i|^2 = 1}{\Gamma; \Delta \vdash \sum_{i=1}^{n} \alpha_i \cdot \vec{t}_i : \#Q} (\#_i) $$

$$ \frac{\Gamma; \Delta, x : A \vdash \vec{t} : B}{\Gamma; \Delta \vdash \lambda x. \vec{t} : A \vdash B} (\neg\neg_i) $$

$$ \frac{\Gamma; \Delta \vdash t : A \dashv B \quad \Gamma'; \Delta' \vdash s : A}{\Gamma, \Gamma'; \Delta, \Delta' \vdash t s : B} (\neg\neg_e) $$

$$ \frac{\Gamma, x : A; \Delta \vdash \vec{t} : B}{\Gamma; \Delta \vdash \lambda x. \vec{t} : ! (A) \Rightarrow B} (\Rightarrow_i) $$

$$ \frac{\Gamma; \Delta \vdash t : A \Rightarrow B \quad ; [z : C] \vdash s : A}{\Gamma, [z : C] ; \Delta \vdash t s : B} (\Rightarrow_e) $$

$$ \frac{\Gamma; \Delta \vdash t : A \quad \Gamma'; \Delta' \vdash s : B}{\Gamma, \Gamma'; \Delta, \Delta' \vdash (t, s) : A \times B} (\times_i) $$

$$ \frac{\Gamma; \Delta \vdash t : A \times B \quad \Gamma'; \Delta' ; x : A, y : B \vdash \vec{s} : C}{\Gamma, \Gamma'; \Delta, \Delta' \vdash \text{let } (x, y) = t \text{ in } \vec{s} : C} (\times_e) $$

$$ \frac{\Gamma; \Delta \vdash t : \#(Q \times R) \quad \Gamma'; \Delta' ; x : \#Q, y : \#R \vdash \vec{s} : S}{\Gamma, \Gamma'; \Delta, \Delta' \vdash \text{let } (x, y) = t \text{ in } \vec{s} : \#S} (\times_e\#) $$

<caption>Fig. 6. Typing rules for PUNQ programs.</caption>

rules ($\Rightarrow_i$) and ($\Rightarrow_e$), can only be performed on “banged” data. The bang function ensures that the resulting type is copyable (or clonable) by turning a qubit into a bit, $!((\#\mathbb{B})) = \mathbb{B}$, propagating over pairs, and not changing applications. For instance, $!((\#\mathbb{B}) \dashv \#\mathbb{B}) = \#\mathbb{B} \dashv \#\mathbb{B}$, as it is safe to copy a quantum gate. Therefore, the intuitionistic arrow explicitly forbids values as inputs, and types of the form $\#A \Rightarrow B$ are uninhabited.

The pair constructor and separable pair destructor are typed using the multiplicative rules ($\times_i$) and ($\times_e$), following the encoding of [Baillot and Terui 2009]. Rule ($\times_e\#$) is the rule for the quantum pair destructor, allowing the handling of a superposition of pairs, hence a possibly entangled state. In this setting, the pair can be viewed as the tensor product used in quantum computing. Variables $x$ and $y$ are typed by $\#Q$ and $\#R$ to preserve unitarity. Note that this typing rule can be extended
to superpositions as follows:

$$ \frac{\Gamma_1; \Delta_1 \vdash \sum_i \alpha_i \cdot t_i : \#(Q \times R) \quad \Gamma_2; \Delta_2, x : \#Q, y : \#R \vdash \vec{s} : S \quad (\vec{x}_{e\#})}{\Gamma_1, \Gamma_2; \Delta_1, \Delta_2 \vdash \sum_i \alpha_i \cdot \text{let } (x, y) = t_i \text{ in } \vec{s} : \#S} $$

Rule $(\vec{x}_{e\#})$ can be simulated using rules $(x_{e\#})$ and $(\#_i)$ but has the advantage of providing a more flexible typing discipline and simplifying the orthogonality requirements of rule $(\#_i)$. Indeed, orthogonality is tested on subterms $t_i$ rather than on terms let $(x, y) = t_i$ in $\vec{s}$.

DLAL characterizes the complexity class FPTIME [Baillot and Terui 2009] by imposing constraints on the use of the contraction rule in proofs and introducing a new modality § in rules $(\#_i)$ and $(\#_e)$ to address some of these limitations. Broadly speaking, the modality § serves as a marker for objects resulting from iterations that cannot be further iterated. Using this construct limits the number of iterations possible in proofs and, consequently, the complexity of the system. Specifically, DLAL enforces a design principle known as stratification by restricting the introduction and elimination of the modality §. This stratification is not sufficient on its own to characterize polynomial time (it provides a characterization of elementary time [Girard 1998]) and this is the reason why rule $(\Rightarrow_e)$ is restricted to at most one open variable.

Rule $(\#_i)$ is the introduction rule for superpositions. A superposition of objects can be created under the conditions that they share the same type, are pairwise orthogonal according to the predicate $\perp_A$, that the norm of the generated superposition $\sum_{i=1}^n |\alpha_i|^2$ equals 1, and that the type A is not an arrow type. Implicit in this rule is the fact that the construction of superpositions is limited to complex amplitudes $\alpha_i$ that are polytime approximable, a set which we denote by $\overline{\mathbb{Q}}$ throughout the paper. When considering quantum computations restricted to some polytime complexity class, it is standard to include such restrictions since, for instance, intractable problems could be encoded into transition amplitudes [Adleman et al. 1997; Bernstein and Vazirani 1997].

Our notion of orthogonality is that of [Díaz-Caro and Malherbe 2022], where the superposition of functions is disallowed. It is treated more realistically than in [Díaz-Caro et al. 2019b], where the superposition of functions is allowed, but it is generally not a function.

# 4 EXAMPLES

We may now consider some examples of typing judgements in PUNQ which correspond to different tools in quantum computation. Informally, a term $t$ is said to represent a unitary operator if, when applied to another term encoding some superposition, the application reduces to what would be the PUNQ representation of the output of the operator. A precise definition of *representing a quantum gate or a unitary operator* is given in Section 5.2.

## 4.1 Superpositions

To demonstrate the typing of a superposition we will consider the example of the X-basis states $|\pm\rangle \triangleq \frac{1}{\sqrt{2}} \cdot |0\rangle \pm \frac{1}{\sqrt{2}} \cdot |1\rangle$, also called the *plus* and *minus* states, which correspond to the unit-norm eigenstates of the Pauli-X operator.

The conditions in the typing rule $(\#_i)$ correspond to checking that the basis terms have the correct type (i.e. since we are interested in typing a qubit state, these terms should be either booleans or qubits), that they are mutually orthogonal, and that the resulting state has unit norm.

*Example 4.1 (X-basis states).* The one-qubit states $|\pm\rangle$ have type $\#\mathbb{B}$.

$$ \pi_{\pm} \triangleq \frac{\overline{\vdash |0\rangle : \mathbb{B}} \quad (0) \quad \overline{\vdash |1\rangle : \mathbb{B}} \quad (1) \quad |0\rangle \perp |1\rangle \quad \left|\frac{1}{\sqrt{2}}\right|^2 + \left|\pm \frac{1}{\sqrt{2}}\right|^2 = 1}{\vdash \frac{1}{\sqrt{2}} \cdot |0\rangle \pm \frac{1}{\sqrt{2}} \cdot |1\rangle : \#\mathbb{B}} \quad (\#_i) $$
with types $\#(\mathbb{B}^2) \to \#(\mathbb{B}^2)$ and $\#(\mathbb{B}^3) \to \#(\mathbb{B}^3)$, respectively. The final term can be obtained, representing the full operation as depicted in Figure 7:

$$ \text{telep} \triangleq \lambda z.\text{let} (q, w) = z \text{ in } (\text{let } (x, y) = \text{Bell } w \text{ in Bob (Alice } (q, x), y)) : \#(\mathbb{B}^3) \to \#(\mathbb{B}^3). $$

## 4.5 Iteration

So far we have only considered examples of constant-time operations. We will now turn to iteration in PUNQ which is inherited from the DLAL typing system.

Gate iteration stands at the intersection of the DLAL and the Lambda-$S_1$ typing systems and is an example of the versatility that PUNQ can provide in safely mixing the two systems. As a toy example, consider the quantum random walk [Childs et al. 2003; Kempe 2003] as an illustrating example for polytime iteration. This technique is known to provide a quantum speedup over its classical analog in different applications [Ambainis 2003] and an illustrative circuit is provided in Figure 8b.

In PUNQ, as in DLAL, we can implement Church numerals with the following type and syntax:

$$ \mathbb{N} \triangleq \forall X.(X \to X) \Rightarrow \S(X \to X) \qquad \underline{\underline{\phantom{\lambda f.\lambda x.f(f(\dots(f x)\dots))}}} \quad (n \text{ times}). $$

For instance, we have that $\underline{\underline{2}} \triangleq \lambda f.\lambda x.f(f x)$, which can be derived with type $\mathbb{N}$. DLAL is complete for polynomial time, and indeed, for any polynomial $P(n) = n^{2d}$, there is a DLAL term poly with type $\mathbb{N} \to \S^{2d}\mathbb{N}$ that simulates it [Baillot and Terui 2009, Proposition 11], which can also be derived in PUNQ. We will now use the Church encoding from DLAL to perform gate iteration in the example of a quantum random walk.

**Example 4.6 (Quantum random walk).** We define the R and L operators, for some set of $K$ nodes, correspond to “taking a step” in one direction or another in a given structure. For instance, if we consider a closed loop, we consider the unitary operators corresponding to a “right” step and a “left” step (see Figure 8a):

$$ R |i\rangle \triangleq |i+1 \pmod{K}\rangle \quad \text{and} \quad L |i\rangle \triangleq |i-1 \pmod{K}\rangle, \quad i \in \{0, \dots, K-1\}, $$

where the basis state $|i\rangle$ corresponds to the particle in node $i$. For $k = \lceil \log(K-1) \rceil$, the operators R and L correspond to unitary operators in the space $\overline{\mathbb{Q}}^{2k} \to \overline{\mathbb{Q}}^{2k}$, and therefore by Theorem 5.7 we show there exist corresponding PUNQ terms, say R and L, of type $\#(\mathbb{B}^k) \to \#(\mathbb{B}^k)$ that simulate them. A single step of the quantum walk can then be done with the following term:

$$ \text{step} \triangleq \lambda z.\text{let} (x, y) = z \text{ in } (\text{if } H x \text{ then } (|0\rangle, L y) \text{ else } (|1\rangle, R y)) : \#(\mathbb{B}^{k+1}) \to \#(\mathbb{B}^{k+1}) $$

where $x$ corresponds to the coin qubit deciding the direction of the step, on which we continuously apply the Hadamard gate. Since these terms correspond to an endomorphism, we may use the Church encoding of numerals to perform an iteration of step. For instance, this allows us to define an abstraction that takes in an integer input and iterates step precisely that number of times. Let walk $\triangleq \lambda m.\lambda x.(m \text{ step}) x$, which has type $\mathbb{N} \to \S^m(\mathbb{B}^{k+1}) \to \S^m(\mathbb{B}^{k+1})$ with the following derivation, where $A = \#(\mathbb{B}^{k+1})$:

$$ \begin{array}{c} \vdots \\ \frac{\begin{array}{l} ; x : A, F : A \to A \vdash F x : A \\ \phantom{; x : A, F : } (\S_i) \\ \phantom{; x : A, F : } \end{array}}{; x : \S A, F : \S(A \to A) \vdash F x : \S A} \\ \\ \frac{\begin{array}{l} \overline{\begin{array}{c} m : \mathbb{N} \vdash m : \mathbb{N} \\ \phantom{m : \mathbb{N} \vdash m : \mathbb{N}} (\Lambda x) \\ \phantom{m : \mathbb{N} \vdash m : \mathbb{N}} \end{array}} (\forall_e) \\ \overline{\begin{array}{c} m : \mathbb{N} \vdash m : (A \to A) \Rightarrow \S(A \to A) \\ \phantom{m : \mathbb{N} \vdash m : (A \to A)} (\Lambda_e) \\ \phantom{m : \mathbb{N} \vdash m : (A \to A)} \end{array}} ; \vdash \text{step} : A \to A \\ \overline{\begin{array}{c} m : \mathbb{N} \vdash m \text{ step} : \S(A \to A) \\ \phantom{m : \mathbb{N} \vdash m \text{ step} : } (\Lambda_e) \\ \phantom{m : \mathbb{N} \vdash m \text{ step} : } \end{array}} (\Rightarrow_e) \\ \\ \frac{\begin{array}{l} \overline{\begin{array}{c} m : \mathbb{N}, x : \S A \vdash (m \text{ step}) x : \S A \\ \phantom{m : \mathbb{N}, x : \S A \vdash } (\neg_i) \\ \phantom{m : \mathbb{N}, x : \S A \vdash } \end{array}} \\ \overline{\begin{array}{c} m : \mathbb{N} \vdash \lambda x.(m \text{ step}) x : \S A \to \S A \\ \phantom{m : \mathbb{N} \vdash \lambda x.(m \text{ step}) x : } (\neg_i) \\ \phantom{m : \mathbb{N} \vdash \lambda x.(m \text{ step}) x : } \end{array}} ; \vdash \text{walk} : \mathbb{N} \to \S A \to \S A \\ \overline{\phantom{m : \mathbb{N} \vdash \lambda x.(m \text{ step}) x : \S A \to \S A}} \end{array}} (C) \end{array} $$
<figure><img src="image_3.png" /><figcaption>Fig. 8. Polytime quantum random walk.</figcaption></figure>

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

For any $\underline{n}$ of type $\mathbb{N}$ we have that walk $\underline{n} \rightsquigarrow^* \lambda x$. (step(step ... (step $x$) ...)) where step is applied $n$ times. Similarly, using the term poly encoding a polynomial $P$, we can construct an abstraction taking in an integer $n$ that iterates step a number $P(n)$ of times:

$$ \text{pwalk} \triangleq \lambda n.\lambda x.((\text{poly } n) \text{ step}) x : \mathbb{N} \to \S^{2d+1}\#(\mathbb{B}^{k+1}) \to \S^{2d+1}\#(\mathbb{B}^{k+1}). $$

## 4.6 No-Cloning and No-Deleting

In order to allow for cloning of variable while ensuring general good behavior for qubits, PUNQ incorporates different features of the DLAL and Lambda-$\mathcal{S}_1$ typing systems.

While DLAL exhibits full weakening (see Figure 10), there is a separation in the context between variables that may appear at most once (linear context) and more than once (exponential context), which then gets carried over into different types of abstractions. In Lambda-$\mathcal{S}_1$, on the other hand, we find a single context for typing judgements, and weakening is only allowed on so-called “flat types”, where a type is restricted in its use of superpositions.

In PUNQ, the difference between the linear and exponential contexts captures the difference between allowed and disallowed treatment of qubits (or superpositions more generally), which then get resolved when creating the abstraction. Consider the following simple example of how PUNQ sensibly allows qubits to be the output of cloning, but not the input.

**Example 4.7 (Qubits made from cloning).** With two instances of rule (A$x$) and one use of $(x_i)$, it is straightforward to obtain the typing judgement; $x : \#\mathbb{B}, y : \#\mathbb{B} \vdash (x, y) : \#\mathbb{B} \times \#\mathbb{B}$. Now, moving $x$ and $y$ into the exponential context using rule (§$_i$) we obtain $x : \#\mathbb{B}, y : \#\mathbb{B}; \vdash (x, y) : \S(\#\mathbb{B} \times \#\mathbb{B})$ where we are now allowed to contract $x$ and $y$ using rule (C) and thus obtain $x : \#\mathbb{B}; \vdash (x, x) : \S(\#\mathbb{B} \times \#\mathbb{B})$.

Though it seems as if the validity of this typing judgement allows for cloning of the $x$ variable representing a qubit, when we take the final step in closing the term, we must use rule ($\Rightarrow_i$), since $x$ appears in the exponential context. Combined with the fact that $!(\#\mathbb{B}) = \mathbb{B}$, we obtain $\vdash \lambda x. (x, x) : \mathbb{B} \Rightarrow \S(\#\mathbb{B} \times \#\mathbb{B})$. Notice that this abstraction does not represent qubit cloning, but rather an operator that creates a pair of qubits using a boolean value that it takes as input to choose in which state the qubits should be.

In Section 5 we will show that PUNQ preserves unitarity over qubit maps in the same way as Lambda-$\mathcal{S}_1$ (Theorem 5.6), where in cases in which the number of qubits increases, the PUNQ term must behave as an isometry. Likewise, no term exists that represents a map that decreases the number of qubits, which would constitute qubit deletion. A consequence of this fact is that we may not reset qubits to some pre-fixed value, as shown in the following example.
*Example 4.8 (Constant output zero)*. To create a lambda abstraction in which the input qubit does not appear in the expression, the variable must be introduced via weakening, which is limited to the exponential context. For instance, using rules (0), (≤), and (W) we may obtain the typing judgement $x : \mathbb{H}\mathbb{B}; \vdash |0\rangle : \mathbb{H}\mathbb{B}$. Applying rule (⇒ᵢ) to create the abstraction, we obtain ; ⊢ λx.|0⟩ : $\mathbb{B} \Rightarrow \mathbb{H}\mathbb{B}$, which corresponds to “forgetting” a boolean input and giving as output a qubit in state zero.

# 5 UNITARITY

In PUNQ, we have adopted the Lambda-$S_1$ typing discipline to ensure that linear maps over qubits, i.e., terms of type $\mathbb{H}\mathbb{B} \to \mathbb{H}\mathbb{B}$, encode unitary operators. The proof of unitarity in [Díaz-Caro and Malherbe 2022] employs the realizability techniques developed in [Díaz-Caro et al. 2019b], which we will tailor to our setting. The major differences include a straightforward extension to tuples of qubits – demonstrating unitarity for types $\#(\mathbb{B}^n) \to \#(\mathbb{B}^n)$ – and the incorporation of DLAL constructs: the modality $\S$, the intuitionistic arrow $\Rightarrow$, as well as polymorphism. All the proofs omitted in this section are fully developed in Appendix A.2.

## 5.1 Realizability

The base of a closed value $\vec{v} \in V_c$ is defined as the set of its basis values in $BV_c$:

$$ \text{base}(v) \triangleq \{v\} $$

$$ \text{base}(\vec{0}) \triangleq \emptyset $$

$$ \text{base}(\alpha \cdot \vec{v}) \triangleq \text{base}(\vec{v}), \text{ if } \alpha \neq 0, \emptyset \text{ otherwise.} $$

$$ \text{base}(\vec{v}_1 + \vec{v}_2) \triangleq \text{base}(\vec{v}_1) \cup \text{base}(\vec{v}_2) $$

Given a set $S$ of closed values in a vector space $V_c$, the span (span) and base (b) of $S$ are defined as:

$$ \text{span}(S) \triangleq \left\{ \sum_{i=1}^{n} \alpha_i \cdot \vec{v}_i : n \geq 0, \alpha_1, \dots, \alpha_n \in \overline{\mathbb{Q}}, \vec{v}_1, \dots, \vec{v}_n \in S \right\} \subseteq V_c $$

$$ \mathfrak{b}S \triangleq \bigcup_{\vec{v} \in S} \text{base}(\vec{v}) \subseteq BV_c $$

We first define the realizability predicate for a superposition $\vec{t}$ and set of closed values $S \subseteq V_c$, written $\vec{t} \models_S S$ that is true if and only if $\vec{t} \rightsquigarrow^* \vec{v}$ for some $\vec{v} \in S$. The set of realizers of $S$ is then defined as $\{\vec{t} \in S_c : \vec{t} \models S\}$.

Let $S_1 \subseteq V_c$ be the set of unit values, that is, $S_1 \triangleq \{\vec{v} \in V_c : |\langle\vec{v}|\vec{v}\rangle|^2 = 1\}$. Given a function $\tau$ from type variables to subsets of $S_1$, the unitary semantics $[\cdot]_\tau : \mathcal{T} \to \mathcal{P}(S_1)$ is defined in Figure 9 by induction on types.

$$ \begin{align*} [X]_\tau &\triangleq \tau(X), & [A \to B]_\tau &\triangleq \{\lambda x.\vec{t} : \forall \vec{v} \in [A]_\tau, (\lambda x.\vec{t})\vec{v} \models [B]_\tau\}, \\ [B]_\tau &\triangleq \{|0\rangle, |1\rangle\}, & [A \Rightarrow B]_\tau &\triangleq \{\lambda x.\vec{t} : \forall v \in b[A]_\tau, (\lambda x.\vec{t})v \models [B]_\tau\}, \\ [\#A]_\tau &\triangleq \text{span}([A]_\tau) \cap S_1, & [A \times B]_\tau &\triangleq \{(\vec{v}, \vec{w}) : \vec{v} \in [A]_\tau, \vec{w} \in [B]_\tau\}, \\ [\$A]_\tau &\triangleq [A]_\tau, & [\forall X.A]_\tau &\triangleq \bigcap_{R \subseteq S_1} [A]_\tau \cup \{X \to R\}. \end{align*} $$

<caption>Fig. 9. Unitary semantics $[\cdot]_\tau : \mathcal{T} \to \mathcal{P}(S_1)$.</caption>

The following property of the definition of ! (Definition 3.2) clarifies the nature of $\mathfrak{b}$ and the role of ! in erasing superposition.
**LEMMA 5.1.** Let $A \in \mathbb{T}_s$, then $\llbracket ! (A) \rrbracket_0 = b \llbracket A \rrbracket_0$.

**PROOF.** By induction on $A \in \mathbb{T}_s$. The full proof is given in Appendix A.2. $\square$

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

The unitary semantics of a typing context $\Gamma$ with respect to $\tau$, called the *unitary semantics* of $\Gamma$ and written $\llbracket \Gamma \rrbracket_\tau$, is defined as

$$ \llbracket \Gamma \rrbracket_\tau \triangleq \{ \sigma \text{ substitution : } \mathrm{dom}(\sigma) = \mathrm{dom}(\Gamma) \text{ and } \forall x \in \mathrm{dom}(\sigma), \sigma(x) \in \llbracket \Gamma(x) \rrbracket_\tau \}. $$

We define $\vec{t}\langle\sum_i \alpha_i \cdot v_i/x\rangle \triangleq \sum_i \alpha_i \cdot \vec{t}[v_i/x]$. The notation $\vec{t}\langle\sigma\rangle$ is also used for any substitution $\sigma$. We say that a typing judgment $\Gamma; \Delta \vdash \vec{t} : A$ is valid when $\mathrm{dom}(\Delta) \subseteq \mathrm{FV}(\vec{t}) \subseteq \mathrm{dom}(\Gamma, \Delta)$ and $\vec{t}\langle\sigma\rangle \models \llbracket A \rrbracket_\tau$ for all $\sigma$ and $\tau$ such that $\sigma \in \llbracket \Gamma, \Delta \rrbracket_\tau$. A typing rule is valid when the validity of its premises implies the validity of its conclusion.

**LEMMA 5.2.** Let $A, B \in \mathbb{T}$ and $\tau$ defined in $\mathrm{FV}(A, B)$. Then, $\llbracket A[B/X] \rrbracket_\tau = \llbracket A \rrbracket_{\tau \cup \{X \mapsto \llbracket B \rrbracket_\tau\}}$.

**PROOF.** By induction on $A \in \mathbb{T}$. The full proof is given in Appendix A.2. $\square$

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

**THEOREM 5.3.** *The typing rules in Figure 6 are valid.*

**PROOF.** We have to check each rule with respect to the definition of typing judgement. To exemplify, we give the case of rule ($\to_o$). The proof for the remaining rules is given in Appendix A.2.

Suppose that $\Gamma; \Delta, x : A \vdash \vec{t} : B$ is a valid judgment. Then since $(\mathrm{dom}(\Delta) \cup \{x\}) \subseteq \mathrm{FV}(\vec{t})$ we have $\mathrm{dom}(\Delta) \subseteq \mathrm{FV}(\lambda x. \vec{t})$. Similarly, since $\mathrm{FV}(\vec{t}) \subseteq (\mathrm{dom}(\Gamma, \Delta) \cup \{x\})$ it is also true that $\mathrm{FV}(\lambda x. \vec{t}) \subseteq \mathrm{dom}(\Gamma, \Delta)$. For any $\sigma \in \llbracket \Gamma, \Delta \rrbracket_\tau$, we have that $(\lambda x. \vec{t})\langle\sigma\rangle = \lambda x. \vec{t}\langle\sigma\rangle$, since $x \notin \mathrm{dom}(\sigma)$. For all $\vec{v} \in \llbracket A \rrbracket_\tau$, we observe that $(\vec{t}\langle\sigma\rangle)\langle\vec{v}/x\rangle = \vec{t}\langle\sigma, \{\vec{v}/x\}\rangle \models \llbracket B \rrbracket_\tau$, since $\sigma, \{\vec{v}/x\} \in \llbracket \Gamma, x : A \rrbracket_\tau$. Therefore, $(\lambda x. \vec{t})\langle\sigma\rangle \models \llbracket A \to B \rrbracket_\tau$. $\square$

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

## 5.2 Isometries over Qubits

*Definition 5.4 (Isometry and unitarity).* An operator $\mathcal{F} : \overline{\mathbb{Q}}^{2^n} \to \overline{\mathbb{Q}}^{2^k}$ is isometric if it preserves the inner product, i.e., if $\langle \mathcal{F}(u)|\mathcal{F}(v)\rangle = \langle u|v\rangle$, $\forall u, v \in \overline{\mathbb{Q}}^{2^n}$. Furthermore, if $\mathcal{F} : \overline{\mathbb{Q}}^{2^n} \to \overline{\mathbb{Q}}^{2^k}$ is isometric then $\mathcal{F}$ is *unitary*.

To simplify notation, for $i = 0, \dots, 2^n - 1$, let $|i\rangle \triangleq (|i_1\rangle, (|i_2\rangle, \dots, (|i_{n-1}\rangle, |i_n\rangle) \dots))$, where $i_1 \dots i_n$ is the binary representation of $i$. We show that any linear application between qubit terms must preserve orthogonality and the norm of basis states.

**LEMMA 5.5.** For any $\vec{t} \in \mathrm{PUNQ}$ and any $k \ge n$ for $k, n \in \mathbb{N} - \{0\}$,

$$ \vec{t} \in \llbracket \#(\mathbb{B}^n) \to \#(\mathbb{B}^k) \rrbracket_0 \iff \begin{cases} \forall i = 0, \dots, 2^n - 1, \exists \vec{v}_i \in \llbracket \#(\mathbb{B}^k) \rrbracket_0 \text{ such that } \vec{t} |i\rangle \rightsquigarrow^* \vec{v}_i, \text{ and} \\ \vec{v}_i \perp_{\#(\mathbb{B}^k)} \vec{v}_j, \forall i \neq j. \end{cases} $$

**PROOF.** The proof is given in Appendix A.2. $\square$

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

This property will allow us to show that closed superpositions of qubit applications behave as isometric operators. Let $\lfloor - \rfloor$ be the linear map from closed values of type $\#(\mathbb{B}^n)$ to $\overline{\mathbb{Q}}^{2^n}$ defined by $\lfloor \sum_{i=0}^{2^n-1} \alpha_i \cdot |i\rangle \rfloor \triangleq (\alpha_0 \cdots \alpha_{2^n-1})^T \in \overline{\mathbb{Q}}^{2^n}$. A closed superposition $\vec{t} \in S_c$ of type $\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)$ represents an operator $\mathcal{F} : \overline{\mathbb{Q}}^{2^n} \to \overline{\mathbb{Q}}^{2^k}$ if, for all values $\vec{v}$ of type $\#(\mathbb{B}^n)$ and $\vec{w}$ of type $\#(\mathbb{B}^k)$, it holds that $\vec{t} \vec{v} \rightsquigarrow^* \vec{w}$ if and only if $\mathcal{F}(\lfloor \vec{v} \rfloor) = \lfloor \vec{w} \rfloor$.

By linearity of $\to_o$, preserving the norm of the basis states is enough to show that an abstraction represents an isometry. Moreover, when the dimensions $n$ and $k$ match the abstraction represents a unitary operator.
**THEOREM 5.6 (SOUNDNESS).** For any closed superposition $\lambda x.\tilde{t} \in [[\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)]]_0$ and any $k, n \in \mathbb{N} - \{0\}$, the following hold:

(1) If $k \ge n$, then $\lambda x.\tilde{t}$ represents an isometry in $\overline{\mathbb{Q}}^{2n} \to \overline{\mathbb{Q}}^{2k}$,

(2) If $k = n$, then $\lambda x.\tilde{t}$ represents a unitary operator in $\overline{\mathbb{Q}}^{2n} \to \overline{\mathbb{Q}}^{2n}$.

Furthermore, if $k < n$, then the type is uninhabited.

**PROOF.** Let $\| \cdot \|$ and $\cdot^\dagger$ represent the typical vector norm and the conjugate transpose, respectively.

1) Let $\lambda x.\tilde{t} \in [[\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)]]_0$. Then, from Lemma 5.5, for $i = 0, \dots, 2^n - 1$, there exist $\vec{v}_i \in [[\#(\mathbb{B}^k)]]_0$ such that $\tilde{t}[|i\rangle/x] \rightsquigarrow^* \vec{v}_i$ with $\langle\vec{v}_i|\vec{v}_j\rangle = 0$, for $i \ne j$. Let $\mathcal{V}: \overline{\mathbb{Q}}^{2n} \to \overline{\mathbb{Q}}^{2k}$ be the linear operator defined by $\mathcal{V}([|i\rangle]) = [\tilde{v}_i]$, for each $i = 0, \dots, 2^n - 1$. By the linearity of the calculus we have that $\lambda x.\tilde{t}$ represents the operator $\mathcal{V}$. Moreover, $\mathcal{V}$ is isometric by Definition 5.4 since $\|\vec{v}_i\| = 1$ and $[\tilde{v}_i]^\dagger \cdot [\tilde{v}_j] = 0$, for $0 \le i \ne j \le 2^n - 1$.

2) The case ($k = n$) is easy to show, since from the case ($k \ge n$) the term $\lambda x.\tilde{t}$ must represent some isometric operator that in this case is also dimension-preserving, so by Definition 5.4 it must also be unitary. Let us now show that the type $\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)$ is uninhabited for $k < n$. We will consider an argument by contradiction. Let us start with a typable and closed abstraction $\lambda x.\tilde{t} \in [[\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)]]_0$. Then, let us define the values $\vec{v}_i \in [[\#(\mathbb{B}^k)]]_0$ satisfying $(\lambda x.\tilde{t}) |i\rangle \rightsquigarrow^* \vec{v}_i$. Since there are $2^n$ such $\vec{v}_i$, they must not be linearly independent, meaning that there is a choice of $\beta_i \in \overline{\mathbb{Q}}$ such that $\sum_{i=1}^{2^n} \beta_i \cdot \vec{v}_i = \overline{0}$ and not all values $\beta_i$ are zero. Then, we may define the superposition $\vec{s} = \sum_i \frac{\beta_i}{\sqrt{\sum_i |\beta_i|^2}} \cdot |i\rangle \in [[\#(\mathbb{B}^n)]]_0$ for which $(\lambda x.\tilde{t}) \vec{s} \rightsquigarrow^* \overline{0} \notin [[\#(\mathbb{B}^k)]]_0$. This concludes the proof. $\square$

Notice that, since we have that $[[\mathbb{S}A]_\tau \triangleq [[A]_\tau]$ in the unitary semantics, the result of Theorem 5.6 also applies to terms $\lambda x.\tilde{t}$ obtained from duplication and therefore having a type that contains the $\mathbb{S}$ symbol, since $[[\mathbb{S}^a\#(\mathbb{B}^n) \to \mathbb{S}^b\#(\mathbb{B}^k)]]_0 = [[\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)]]_0$.

**THEOREM 5.7 (COMPLETENESS).** For any isometry $\mathcal{I}: \overline{\mathbb{Q}}^{2n} \to \overline{\mathbb{Q}}^{2k}$, with $k \ge n \ge 1$, there exists a closed superposition $\lambda x.\tilde{t} \in S_c$ of type $\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)$ that represents $\mathcal{I}$.

**PROOF.** Constructive proof given in Appendix A.2. $\square$

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

On top of satisfying unitarity, PUNQ also satisfies another natural property of quantum computation, which is that qubits may occupy entangled states and that there is no operation that disentangles any general state.

**THEOREM 5.8 (NON-SEPARABILITY).** For any $n, k \in \mathbb{N} - \{0\}$, the type $\#(\mathbb{B}^{n+k}) \to (\#(\mathbb{B}^n) \times \#(\mathbb{B}^k))$ is uninhabited.

**PROOF.** Proof in Appendix A.2. $\square$

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

# 6 POLYTIME NORMALIZATION

In this section, we show that PUNQ preserves the polytime strong normalization properties of DLAL [Baillot and Terui 2009], when adapted to the context of quantum computation. For that purpose, we define an encoding from superpositions in PUNQ to sets of DLAL terms and show that the polynomial time strong normalization of each of the terms in this set implies the polytime normalization of the initial PUNQ program. All the proofs omitted in this section are fully developed in Appendix A.3.
<figure><img src="image_11.png" /><figcaption>Fig. 10. Dual Light Affine Logic (DLAL).</figcaption></figure>

## 6.1 Dual Light Affine Logic

DLAL terms [Baillot and Terui 2009] are a strict subset of System F [Girard 1972; Reynolds 1974] that can be typed with respect to the rules of Figure 10. The set $\mathcal{S}$ of types in DLAL is the set produced by the following grammar:

$$A := X \mid A \to A \mid A \Rightarrow A \mid \$A \mid \forall X.A,$$

and can be viewed as a subset of $\mathcal{T}$. The notion of typing environments $\Gamma, \Delta$ are defined in a standard way. For a given set of DLAL terms $S$, we write $\Gamma; \Delta \vdash_{\text{DLAL}} S : A$ if $\forall t \in S$, the derivation of $\Gamma; \Delta \vdash t : A$ can be obtained in DLAL.

The size of a DLAL term $t$, denoted $|t|$, is defined as the number of its symbols, and the size of a set of terms $S$, noted $|S|$, is defined as the biggest size of a term $t \in S$, i.e., $|S| \triangleq \max\{|t| \mid t \in S\}$. The reason for this choice is that superpositions in PUNQ will be encoded as sets of terms in DLAL, which in a sense will encode the set of base terms present in the superposition. Since in PUNQ the size of a term is the maximum size appearing in a superposition, this choice ensures that we capture the correct notion of polynomial size of the final term.

The following theorem implies both a polynomial bound on the reduction length and a polynomial bound on the size of each term obtained during the reduction in the DLAL system.

**THEOREM 6.1 (POLYNOMIAL TIME STRONG NORMALIZATION [BAILLOT AND TERUI 2009, THM. 8]).**
If $\Gamma; \Delta \vdash_{\text{DLAL}} t : A$, then there exists a constant $d$, referred to as the depth of $t$, such that $t$ reduces to its normal form in at most $O(|t|^{2d})$ reduction steps and within a time complexity of $O(|t|^{2d+2})$ on a deterministic Turing machine. This result holds independently of the chosen reduction strategy.

Given two sets of DLAL terms $S$ and $\mathcal{T}$, we write $S \to \mathcal{T}$ if $\mathcal{T} = \{t \mid s \in S \wedge (s \to t \lor s \leftrightarrow)\}$, meaning that the set $\mathcal{T}$ is obtained from $S$ by attempting to apply a single reduction step. Therefore, if the term is already normalized it remains in the set. Let $\to^n$ be the $n$-fold transitive closure of $\to$, i.e., if $S_0 \to \dots \to S_n$ then $S_0 \to^n S_n$. We also write $S \to^n \mathcal{T}$ if there exists $k \le n$ such that $S \to^k \mathcal{T}$. Termination is defined as reaching a point where all terms in the set are in normal form, i.e., $S \downarrow^n$ if $S \to^n \mathcal{T}$ and $\mathcal{T} \to \mathcal{T}$. Similarly, we write $S \downarrow^{\le n}$ for termination in at most $n$ steps.
**COROLLARY 6.2.** For any type $A \in \mathbb{T}$, there is a polynomial $P_A \in \mathbb{N}[X]$ such that, if $\Gamma; \Delta \vdash_{\text{DLAL}} S : A$, then $S \downarrow \stackrel{\leq P_A(|S|)}{\leq}$ and, for each $\mathcal{T}$ satisfying $S \to^n \mathcal{T}$ for some $n \in \mathbb{N}$, $|\mathcal{T}| \leq P_A(|S|)$.

Notice that the polynomial $P_A$ can be explicitly computed and only depends on $A$ as the depth of a term is a function of its type (see [Baillot and Terui 2009]). Furthermore, Corollary 6.2 applies for any reduction strategy, so we may fix the strategy to be call-by-value for our purposes.

## 6.2 Encoding of PUNQ in DLAL

In order to prove PUNQ's polynomial time normalization, we will give a translation from PUNQ terms into sets of DLAL terms. We will then show that, for the PUNQ terms of interest (i.e. those that are typable), their reduction length in PUNQ is upperbounded by the maximum reduction length in its translation. Given that this encoding will only increase polynomially the size of the term, this will provide a polynomial upper bound in the reduction of PUNQ terms.

We extend the DLAL syntax with the term $*$, which will represent the encoding of $\vec{0}$, and the following typing rule ensuring that $*$ has any type:

$$ \vdash * : \forall X.X \quad (*) $$

We will call this extension of the DLAL syntax and typing system DLAL$_*$.$ Since $*$ does not reduce in any way, the polytime termination result in Theorem 6.1 and its corollary also apply to DLAL$_*$.

Given two sets of terms $S, \mathcal{T}$, let $S \mathcal{T}$ be syntactic sugar for the set $\{s \mid s \in S \wedge t \in \mathcal{T}\}$. We now define formally the map $\langle \cdot, \cdot \rangle : \text{PUNQ} \to \mathcal{P}(\text{DLAL}_*)$ in Figure 11 and the type encoding $(\cdot)^* : \mathbb{T} \to \mathbb{S}$ in Figure 12. This encoding is extended to contexts as follows: $\Gamma^* \triangleq \{x_i : (A_i)^* \mid x_i : A_i \in \Gamma\}$.

Such an encoding does not require that the set of DLAL terms perfectly simulate the corresponding PUNQ term, but it must contain enough of the structure of the original term to provide a valid upper bound in its number of reduction steps. As such, the type encoding $(\cdot)^*$ in Figure 12 can be seen as a “dequantization” of the type (i.e. removing quantum superposition) combined with translation into DLAL types that correspond to the basic PUNQ types, such as the encoding of pairs and booleans.

The term translation $\langle \cdot, \cdot \rangle$ from PUNQ terms to sets of DLAL$_*$ terms is standard, with a few exceptions. In DLAL, a term encoding the conditional “if $t$ then $t_1$ else $t_2$” would be typed multiplicatively, requiring disjoint contexts for $t_1$ and $t_2$. However, for the purpose of guaranteeing unitarity, the conditional is typed additively in PUNQ (i.e., the two contexts are the same). To handle this difference, we rewrite the conditional such that the branches have no open linear variables, which allows for a correct typing derivation in DLAL$_*$. This transformation in general requires that we use information on the derivation of the term, but this is handled implicitly in the translation. For some natural number $k$, we define the notation $\lambda x_{[1..k]} \vec{t} \triangleq \lambda x_1 \lambda x_2 \dots \lambda x_k \vec{t}$. Similarly, when $\vec{t}$ contains $k$ instances of a free variable $x$, we denote by $\vec{t}_{[x:1..k]}$ the term $\vec{t}$ where each occurrence of $x$ is replaced by $x_i$, for $i = 1, \dots, k$. For instance, for $\vec{t} = \lambda y.x(x y)$, we have $\vec{t}_{[x:1..k]} = \lambda y.x_1(x_2 y)$.

Also of note is the translation of the abstraction “$\lambda x.\vec{t}$”, where we perform a linearization of the lambda abstraction, separating all the repeated instances of $x$ with separate variables, labeled $x_i$. Likewise, in the application case “$t_1 t_2$”, we repeat the encoding of $t_2$ the appropriate number of times. This is encoded in a function $\eta : \text{PUNQ} \to \{0, 1, \dots\}$, encoding the number of times the first input is repeated. This ensures that generated set of DLAL terms will account for all possible branches contained in the original PUNQ term (see Example 6.11). For instance, $\eta(\lambda x.x) = 1$ since $x$ is not duplicated, and $\eta((\lambda x.x)(\lambda f.\lambda y. f f y)) = 2$ since once the term reduces to the value $\lambda f.\lambda y. f f y$, the input $f$ appears twice in the term.
$$ (|\vec{0}|) \triangleq \{*\} \qquad (|x|) \triangleq \{x\} \qquad (|0\rangle) \triangleq \{\lambda x.\lambda y.x\} \qquad (|1\rangle) \triangleq \{\lambda x.\lambda y.y\} $$

$$ (\text{if } t \text{ then } t_1 \text{ else } t_2) \triangleq (|t|) \lambda x_{[1..k]}.(|t_1|) \lambda x_{[1..k]}.(|t_2|) \quad x_1 \dots x_k, \\ \text{with } \Gamma; x_1 : A_1, \dots, x_k : A_k \vdash t_1, t_2 : B $$

$$ (\text{let } (x, y) = t_1 \text{ in } t_2) \triangleq (|t_1|) (\lambda x.\lambda y.(|t_2|)) \qquad (|\alpha \cdot \vec{t}|) \triangleq (|\vec{t}|), \text{ if } \alpha \neq 0, \{*\} \text{ otherwise} $$

$$ (|\vec{t}_1 + \vec{t}_2|) \triangleq (|\vec{t}_1|) \cup (|\vec{t}_2|) \qquad (|t_1 \ t_2|) \triangleq (\dots (|t_1| (|t_2|)) (|t_2|) \dots (|t_2|)) \quad (\eta(t_1) \text{ times}) $$

$$ (|t_1, t_2|) \triangleq \lambda x.(x (|t_1|) (|t_2|)) \qquad (|\lambda x.\vec{t}|) \triangleq \lambda x_{[1..k]}.(|\vec{t}_{[x:1..k]}|), \quad k = \eta(\lambda x.\vec{t}) $$

<caption>Fig. 11. $(|\cdot|) : \text{PUNQ} \to \mathcal{P}(\text{DLAL}_*)$.</caption>

$$ \begin{array}{ll} (X)^* \triangleq X & (\mathbb{B})^* \triangleq \forall X.(X \to X \to X) \\ (A_1 \to A_2)^* \triangleq (A_1)^* \to (A_2)^* & (A_1 \Rightarrow A_2)^* \triangleq (A_1)^* \Rightarrow (A_2)^* \\ (A_1 \times A_2)^* \triangleq \forall X.((A_1)^* \to (A_2)^* \to X) \to X) & (\#Q)^* \triangleq (Q)^* \\ (\S A)^* \triangleq \S(A)^* & (\forall X.A)^* \triangleq \forall X.(A)^* \end{array} $$

<caption>Fig. 12. $()^* : \mathbb{T} \to \mathbb{S}$.</caption>

Let us now look at a few properties of the type encoding $()^*$. A first property we may notice is that the type encoding does not change if we first transform a type into its clonable version, i.e. when we apply the ! function.

**LEMMA 6.3.** For any $A \in \mathbb{T}$, we have that $(! (A))^* = A^*$.

**PROOF.** By induction on the structure of A. □

Similarly, a useful fact is that the encoding is preserved by PUNQ subtyping.

**LEMMA 6.4.** For any $A, B \in \mathbb{T}$, if $A \le B$ then $A^* = B^*$.

**PROOF.** By inspection of the rules in Figure 5. □

Regarding the term translation $(|\cdot|)$, we can check that it is preserved by the equivalence relation $\equiv$ in PUNQ, modulo the presence of the term $^*$.

**Definition 6.5.** Let $S, \mathcal{T}$ be two sets. Then $S \sqsubseteq \mathcal{T}$ if $S \subseteq \mathcal{T} \cup \{^*\}$. We also define $\mathcal{T} \simeq S$ if $\mathcal{T} \subseteq S$ and $S \subseteq \mathcal{T}$.

**LEMMA 6.6.** If $\vec{t} \equiv \vec{r}$, then $(|\vec{t}|) \approx (|\vec{r}|)$.

**PROOF.** By inspection of the equivalence relation. The full proof is given in Appendix A.3. □

We now turn to the normalization behavior of each term in the set corresponding to a given translation. First, we may notice that every term in a translation has the same type, which corresponds to the type given by the $()^*$. Notice also that, though not explicitly stated, the notion of depth of a typing derivation [Baillot and Terui 2009] is asymptotically preserved by the translation.
**LEMMA 6.7.** $\Gamma; \Delta \vdash \vec{t} : A$ implies $\Gamma^*; \Delta^* \vdash_{\text{DLAL}} (|\vec{t}|) : A^*.$

**PROOF.** By induction on the derivation of $\Gamma; \Delta \vdash \vec{t} : A$. The full proof is given in Appendix A.3. $\square$

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

Another important detail is that the encoding increase the size of the original PUNQ term only polynomially and is therefore an appropriate way to connect the complexity of the two systems.

**LEMMA 6.8.** For any $A \in \mathbb{T}$, there exists a polynomial $P_A$ such that, for any $\vec{t}$ where $\vdash \vec{t} : A$, the following holds $|(|\vec{t}|)| = O(P_A(|\vec{t}|))$.

**PROOF.** By induction on the structure of $\vec{t}$. The full proof is given in Appendix A.3. $\square$

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

To demonstrate how this translation guarantees polynomial-time termination in PUNQ, we consider the relation between the reduction of a PUNQ term $\vec{t}$ and the reduction of its translation $|(|\vec{t}|)|$. Given our choice of translation, a term in PUNQ will correspond to a set in DLAL containing not only all basis states present in any superposition, but also all possible branchings in the program.

We now show that a reduction in PUNQ corresponds to at least one reduction over its encoding in DLAL. Notice first that, once we reach a value in PUNQ, its DLAL translation will not reduce.

**LEMMA 6.9.** For any $\vec{v} \in V_c$, we have that $|(|\vec{v}|)|$ does not reduce.

**PROOF.** By induction on the structure of $\vec{v}$. The full proof is given in Appendix A.3. $\square$

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

Now we consider the central lemma for the proof of Theorem 6.12.

**LEMMA 6.10.** For any $\vec{t} \in \text{PUNQ}$, $\vec{t} \rightsquigarrow \vec{r}$ implies $|(|\vec{r}|)| \subseteq \bigcup_{n>0} \{S_n \mid (|\vec{t}|) \to^n S_n\}$.

**PROOF.** By induction on relation $\rightsquigarrow$. The full proof is given in Appendix A.3. $\square$

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

**Example 6.11 (Two Hadamards).** Let $\vec{t} = (\underline{2} \text{ H})|0\rangle$, having PUNQ type $\#\mathbb{B}$, correspond to applying twice the Hadamard gate (Example 4.2) to state $|0\rangle$. We denote by $S_0$ its translation into a set of DLAL terms, and, for all $n > 0$, let $S_n$ be the set such that $S_0 \to^n S_n$. Let $tt \triangleq \lambda x.\lambda y.x$ and $ff \triangleq \lambda x.\lambda y.y$ be a shorthand notation for the boolean encoding in DLAL. First, we translate the Hadamard term. Notice that, since $|+\rangle$ and $|-\rangle$ are closed terms, we do not need to add any new variables in the translation of the if ($\cdot$) then ($\cdot$) else ($\cdot$). The translation is then:

$$ (|H\rangle) = \lambda x. (|\text{if } x \text{ then } |+\rangle \text{ else } |-\rangle) = \lambda x.x (|+\rangle) (|-\rangle) = \lambda x.x \{\text{ff, tt}\} \{\text{ff, tt}\}, $$

which corresponds to the set of 4 terms $\{\lambda x.x \ b_1 \ b_2 \mid b_1, b_2 \in \{\text{ff, tt}\}\}$. The translation of $\vec{t}$ corresponds to 16 DLAL terms, all of which have type $(\#\mathbb{B})^* = \S(\forall X.X \dashv X \dashv X)$ in DLAL$_*$:

$$ (|\vec{t}|) = S_0 = \{(\lambda f_1.\lambda f_2.\lambda q.f_1(f_2 q) (\lambda x.x \ b_1 \ b_2) (\lambda x.x \ b_3 \ b_4)) \ tt \mid b_i \in \{\text{ff, tt}\}\}. $$

This set reduces in 7 steps, according to the following progression:

$$ S_1 = \{(\lambda f_2.\lambda q.(\lambda x.x \ b_1 \ b_2)(f_2 q) (\lambda x.x \ b_3 \ b_4)) \ tt \mid b_i \in \{\text{ff, tt}\}\} $$

$$ S_2 = \{(\lambda q.(\lambda x.x \ b_1 \ b_2) (\lambda x.x \ b_3 \ b_4) q) \ tt \mid b_i \in \{\text{ff, tt}\}\} $$

$$ S_3 = \{(\lambda x.x \ b_1 \ b_2) (\lambda x.x \ b_3 \ b_4) \ tt \mid b_i \in \{\text{ff, tt}\}\} $$

$$ S_4 = \{(\lambda x.x \ b_1 \ b_2) (\text{tt} \ b_3 \ b_4) \mid b_i \in \{\text{ff, tt}\}\} $$

$$ S_5 = \{(\lambda x.x \ b_1 \ b_2) \ b_3 \mid b_i \in \{\text{ff, tt}\}\} $$

$$ S_6 = \{b_3 \ b_1 \ b_2 \mid b_i \in \{\text{ff, tt}\}\} $$

$$ S_7 = \{\text{ff, tt}\} $$
In PUNQ, $\vec{t}$ reduces to a value in 6 steps. Defining $\vec{r}_i$ as $\vec{r}_0 \triangleq \vec{t}$ and $\vec{r}_i \rightsquigarrow \vec{r}_{i+1}$, we have

$$
\begin{align*}
\vec{r}_1 &= (\lambda x. H H x) |0\rangle & (|\vec{r}_1|) &= S_2 \\
\vec{r}_2 &= H H |0\rangle & (|\vec{r}_2|) &= S_3 \\
\vec{r}_3 &= H (\text{if } |0\rangle \text{ then } |+\rangle \text{ else } |-\rangle) & (|\vec{r}_3|) &= S_4 \\
\vec{r}_4 &= 1/\sqrt{2} \cdot H |0\rangle + 1/\sqrt{2} \cdot H |1\rangle & (|\vec{r}_4|) &= S_5 \\
\vec{r}_5 &= 1/\sqrt{2} \cdot \text{if } |0\rangle \text{ then } |+\rangle \text{ else } |-\rangle + 1/\sqrt{2} \cdot \text{if } |1\rangle \text{ then } |+\rangle \text{ else } |-\rangle & (|\vec{r}_5|) &= S_6 \\
\vec{r}_6 &= |0\rangle & (|\vec{r}_6|) &= \{tt\} \subseteq S_7
\end{align*}
$$

Notice that the PUNQ term was not perfectly simulated since $f \ddot{f}$ also appears in $S_7$. However, in every step of the reduction $\vec{r}_0 \rightsquigarrow \vec{r}_6$, we find the translation of $\vec{r}_i$ in a further reduction of $S_0$, which suffices to bound the number of steps until achieving normalization.

The previous results allow us to conclude that, like DLAL, PUNQ ensures polytime normalization.

**THEOREM 6.12 (POLYNOMIAL TIME NORMALIZATION).** For any $A \in \mathbb{T}_c$, there is a polynomial $P_A \in \mathbb{N}[X]$ such that, for any PUNQ superposition $\vec{t}$ with type A, $\vec{t}$ reduces to a value $\vec{v}$ in at most $O(P_A(|\vec{t}|)$ reduction steps and $|\vec{v}| = O(P_A(|\vec{t}|))$.

**PROOF.** Let $\vec{t} \in \text{PUNQ}$ such that $\Gamma; \Delta \vdash \vec{t} : A$. Then, by Lemma 6.7, $\Gamma^*; \Delta^* \vdash_{\text{DLAL}_*} (|\vec{t}|) : A^*$ holds and each term $t_i \in (|\vec{t}|)$ has size at most $O(|\vec{t}|)$. By Corollary 6.2, there is a polynomial $P_{A^*} \in \mathbb{N}[X]$ such that every DLAL$_*$ term $t_i \in (|\vec{t}|)$ can be reduced in $N \triangleq O(P_{A^*}(|t_i|))$ steps. Since the size $|t_i|$ of DLAL$_*$ terms is bounded by $P_A(|\vec{t}|)$, from Lemma 6.8, we have $N = O(P_{A^*}(P_A(|\vec{t}|)))$. Therefore all the terms in $(|\vec{t}|)$ reduce in polynomial time on the size of $\vec{t}$. As shown in Lemma 6.10, each reduction step in PUNQ corresponds to at least one reduction step applied to all the (non-normalized) terms in its translation into DLAL$_*$, we conclude that $\vec{t}$ must reduce to normal form in at most $N$ steps. $\square$

# 7 TYPE CHECKING

In this section we discuss type checking in PUNQ, which corresponds to the following problem.

*Definition 7.1 (Type checking).* We define the problem of type checking in PUNQ, denoted CHK, as follows. Given $\vec{t} \in S_c$ and $A \in \mathbb{T}_c$, CHK($\vec{t}$, A) is true if and only if $; \vdash \vec{t} : A$ can be derived.

*Preliminaries.* Let PTIME be the set of decision problems solvable by a deterministic Turing machine running in polynomial time and, given an oracle C, let us denote by PTIME$^C$ the set of decision problems that can be determined by a polytime deterministic oracle Turing machine with oracle C, which can be easily extended to the case where C is a complexity class. Finally, the class $\Pi_1^0$ of the arithmetical hierarchy is defined as $\Pi_1^0 \triangleq \{\psi \mid \exists \phi \in \text{REC}, \forall \vec{x}. (\psi(\vec{x}) \Leftrightarrow \forall \vec{y}. \phi(\vec{x}, \vec{y}))\}$, where $\vec{x}, \vec{y}$ are variables with values belonging to enumerable sets, $\psi$ and $\phi$ are formulas in the language of first-order arithmetic, and REC is the class of recursive sets (decidable problems) [Odifreddi 1992].

*Orthogonality criteria.* Outside of checking orthogonality in rules (if $\#\mu$) and ($\#\mu_i$), PUNQ type checking is no more complicated than that of DLAL, which is decidable in polynomial time [Baillot and Terui 2009]. This is because the complexity added by the Lambda-$S_1$ typing discipline (modulo orthogonality checking) corresponds to that of a simply typed lambda calculus, where type checking can be done efficiently [Mairson 2004]. Therefore, if one has access to an oracle for checking orthogonality between terms, then type checking in PUNQ can be done efficiently.
*Definition 7.2.* Let $\varphi$ be an oracle for orthogonality between PUNQ terms, where, for all $\vec{t}, \vec{s} \in S$, and contexts $\Gamma, \Delta$, we have $\varphi(\vec{t}, \vec{s}, \Gamma, \Delta) \triangleq 0 \iff \vec{t} \perp^{\Gamma;\Delta} \vec{s}$.

**LEMMA 7.3.** *CHK* ∈ PTIME<sup>*q*</sup>.

We will address the complexity of type checking in three fragments of the PUNQ language, defined by their orthogonality criteria. The first two fragments only require access to the syntax of the term, whereas the last one takes in as input a “candidate type” used to bound the time needed to check orthogonality. Notice that, since we only check orthogonality in cases where we also check the type – rules (if<sub>Φ</sub>) and (if<sub>*i*</sub>), this does not lead to a loss of generality.

*Definition 7.4.* We define the following three criteria for orthogonality over superpositions.

* ORTHO<sub>0</sub> : $S \times S \to \{0, 1\}$ defined as

$$ \mathrm{ORTHO}_{0}(\vec{t}, \vec{s}) \triangleq \begin{cases} 0, & \text{if } \vec{t} \perp \vec{s}, \\ 1, & \text{otherwise.} \end{cases} $$

* ORTHO<sub>×</sub> : $S \times S \to \{0, 1\}$ defined as

$$ \mathrm{ORTHO}_{\times}(\vec{t}, \vec{s}) \triangleq \begin{cases} \mathrm{ORTHO}_{\times}(t_1, s_1) \cdot \mathrm{ORTHO}_{\times}(t_2, s_2), & \text{if } \vec{t} = (t_1, t_2) \text{ and } \vec{s} = (s_1, s_2), \\ \mathrm{ORTHO}_{\emptyset}(\vec{t}, \vec{s}), & \text{otherwise.} \end{cases} $$

* ORTHO<sub>untyped</sub> : $S \times S \times \mathbb{T} \to \{0, 1\}$ defined as follows. Let $FV(\vec{t}) \cup FV(\vec{s}) = x_1, \dots, x_n$.

$$ \mathrm{ORTHO}_{\mathrm{untyped}}(\vec{t}, \vec{s}, Q) \triangleq 1 - \prod_{\vec{v}_1, \dots, \vec{v}_n \in V_c} \mathrm{PERP}(\vec{t} \langle \vec{v}_1 / x_1, \dots, \vec{v}_n / x_n \rangle, \vec{s} \langle \vec{v}_1 / x_1, \dots, \vec{v}_n / x_n \rangle, Q), $$
with $\mathrm{PERP} : S_c \times S_c \times \mathbb{T} \to \{0, 1\}$ defined as

$$ \mathrm{PERP}(\vec{t}_1, \vec{t}_2, Q) \triangleq 1 \iff \vec{t}_1, \vec{t}_2 \rightsquigarrow \vec{w}_1, \vec{w}_2 \in [[Q]]_0 \text{ and } \mathrm{ORTHO}_0(\vec{w}_1, \vec{w}_2) = 0. $$

For $\mathcal{X} \in \{\emptyset, \times, \mathrm{untyped}\}$, we denote by $CHK_{\mathcal{X}}$ set of terms that can be typed in PUNQ using $ORTHO_{\mathcal{X}}$ as definition of orthogonality.

In $ORTHO_0$, orthogonality is defined only over closed terms. Notice, for instance, that the Hadamard and Z gates (Examples 4.2 and 4.3) only employ this orthogonality, and therefore $H, Z \in CHK_0$. In $ORTHO_\times$, we only detect orthogonality via closed terms in a pair structure, for instance by checking that $(|0\rangle, x)$ is orthogonal to $(|1\rangle, y)$ over any possible variable substitutions on $x$ and $y$. This is used in the case of the CNOT gate (Example 4.4) and the circuit for teleportation which employs it (Example 4.5), and so CNOT, telep $\in CHK_\times$. In $ORTHO_{\mathrm{untyped}}$, we check over all possible value substitutions – even those where the value used does not have the correct type – check if the term reduces into the correct type and, if so, test its orthogonality.

**LEMMA 7.5.** $CHK_0 \subseteq CHK_\times \subseteq CHK_{\mathrm{untyped}} \subseteq CHK$.

$ORTHO_0$ and $ORTHO_\times$ can be verified efficiently, and therefore ensure that type checking can be done in polytime. However, we conjecture that general orthogonality is undecidable.

**LEMMA 7.6.** $ORTHO_0, ORTHO_\times \in PTIME$, and $ORTHO_{\mathrm{untyped}} \in \Pi_1^0$.

**PROOF.** Proof given in Appendix A.4. □

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

The proof of Lemma 7.6 rests also on the choice of $\overline{Q}$ for the amplitudes in PUNQ, where comparisons can be done efficiently [Halava et al. 2005, Proposition 2.2]. Furthermore, since type checking is done classically, we must bound the complexity of reducing terms to check their orthogonality in the classical Turing machine model (see Appendix A.4).
**THEOREM 7.7.** $\text{CHK}_\emptyset, \text{CHK}_\times \in \text{PTIME}$ and $\text{CHK}_{\text{untyped}} \in \text{PTIME}^{\Pi_1^0}$.

**PROOF.** From Lemmas 7.3 and 7.6. □

# 8 CONCLUSIONS AND FUTURE WORK

We have introduced PUNQ, a new quantum programming language with quantum control capabilities. PUNQ stands out as the first feasible language with quantum control. Supporting higher-order programs, the language boasts a robust type system ensuring both unitarity and polynomial-time normalization. To conclude, we claim PUNQ is a pioneering language, seamlessly combining theoretical depth with practical applicability in the realm of quantum computing. Plenty of interesting questions remain open:

* *Extending quantum control.* So far, in PUNQ, we have limited superpositions to ground types, i.e., non functional types such as qubits. Extending superpositions to functional types, e.g., $\#(A \to B)$ or $\#(A \Rightarrow B)$, would allow for natural characterizations of experiments in indefinite causal order such as the quantum switch [Procopio et al. 2015; Rubino et al. 2017]. This question is also interesting for polymorphism, since the lists of type A in DLAL, $\forall X.(A \to X \to X) \Rightarrow \S(X \to X)$, cannot be superposed in PUNQ.

* *Orthogonality criteria.* Extending the tractable criteria for orthogonality given in Section 7 to allow for more expressivity in the oracle-free case.

* *Circuit compilation.* Limiting quantum programs to polynomial time in a quantum Turing machine corresponds to a limitation to uniform quantum circuits [Yao 1993]. However, direct compilation strategies that preserve polynomial time are not trivial [Hainry et al. 2023]. In this vein, it would be interesting to show a compilation strategy that would assign a polysize circuit representation of any PUNQ term that corresponds to a unitary transformation.

# REFERENCES

* Leonard M. Adleman, Jonathan DeMarrais, and Ming-Deh A. Huang. 1997. Quantum Computability. *SIAM J. Comput.* 26, 5 (1997), 1524–1540. https://doi.org/10.1137/S0097539795293639

* Thorsten Altenkirch and Jonathan Grattage. 2005. A Functional Quantum Programming Language. In *LICS 2005*. IEEE Computer Society, 249–258. https://doi.org/10.1109/LICS.2005.1

* Andris Ambainis. 2003. Quantum walks and their algorithmic applications. *International Journal of Quantum Information* 01, 04 (2003), 507–518. https://doi.org/10.1142/S0219749903000383

* Pablo Arrighi and Gilles Doweck. 2017. Lineal: A linear-algebraic Lambda-calculus. *Logical Methods in Computer Science* 13, 1 (2017), 1–33. https://doi.org/10.23638/LMCS-13(1:8)2017

* Costin Badescu and Prakash Panangaden. 2015. Quantum Alternation: Prospects and Problems. In *QPL 2015 (EPTCS, Vol. 195)*, Chris Heunen, Peter Selinger, and Jamie Vicary (Eds.). Open Publishing Association, 33–42. https://doi.org/10.4204/EPTCS.195.3

* Patrick Baillot and Kazushige Terui. 2009. Light types for polynomial time computation in lambda calculus. *Information and Computation* 207, 1 (2009), 41–62. https://doi.org/10.1016/j.ic.2008.08.005

* Andrew Barber and Gordon Plotkin. 1996. *Dual intuitionistic linear logic*. University of Edinburgh, Department of Computer Science, Edinburgh, UK.

* Stephen J. Bellantoni and Stephen A. Cook. 1992. A New Recursion-Theoretic Characterization of the Polytime Functions. *Computational Complexity* 2 (1992), 97–110. https://doi.org/10.1007/BF01201998

* Charles H. Bennett, Gilles Brassard, Claude Crépeau, Richard Jozsa, Asher Peres, and William K. Wootters. 1993. Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. *Physical Review Letters* 70, 13 (1993), 1895–1899. https://doi.org/10.1103/PhysRevLett.70.1895

* Ethan Bernstein and Umesh Vazirani. 1997. Quantum Complexity Theory. *SIAM J. Comput.* 26, 5 (1997), 1411–1473. https://doi.org/10.1137/S0097539796300921

* Kostia Chardonnet. 2023. *Towards a Curry-Howard Correspondence for Quantum Computation*. Ph. D. Dissertation. Université Paris-Saclay. https://theses.hal.science/tel-03959403

* Kostia Chardonnet, Marc de Visme, Benoît Valiron, and Renaud Vilmart. 2022. The Many-Worlds Calculus. Preprint at arXiv. http://arxiv.org/abs/2206.10234
Andrew M. Childs, Richard Cleve, Enrico Deotto, Edward Farhi, Sam Gutmann, and Daniel A. Spielman. 2003. Exponential algorithmic speedup by a quantum walk. In Proceedings of the thirty-fifth annual ACM symposium on Theory of computing. ACM. https://doi.org/10.1145/780542.780552

Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. 2010. Quantum implicit computational complexity. Theoretical Computer Science 411, 2 (2010), 377-409. https://doi.org/10.1016/j.tcs.2009.07.045

Alejandro Díaz-Caro. 2021. A quick overview on the quantum control approach to the lambda calculus. In Proceedings of the 16th Workshop on Logical and Semantic Frameworks with Applications (LSFA'21) (Electronic Proceedings in Theoretical Computer Science, Vol. 357), Mauricio Ayala-Rincón and Eduardo Bonelli (Eds.). Open Publishing Association, 1-17. https://doi.org/10.4204/EPTCS.357.1

Alejandro Díaz-Caro, Gilles Dowek, and Juan Pablo Rinaldi. 2019a. Two linearities for quantum computing in the lambda calculus. BioSystems 186 (2019), 104012. https://doi.org/10.1016/j.biosystems.2019.104012 Postproceedings of TPNC 2017.

Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron. 2019b. Realizability in the Unitary Sphere. In LICS 2019. IEEE, 1-13. https://doi.org/10.1109/LICS.2019.8785834

Alejandro Díaz-Caro and Octavio Malherbe. 2022. Quantum Control in the Unitary Sphere: Lambda-$S_1$ and its Categorical Model. Logical Methods in Computer Science 18, 3 (2022), 1-32. https://doi.org/10.46298/lmcs-18(3:32)2022

Alejandro Díaz-Caro and Octavio Malherbe. 2023. A concrete model for a typed linear algebraic lambda calculus. To appear in Mathematical Structures in Computer Science. https://arxiv.org/abs/1806.09236

Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca. 2008. A logical account of PSPACE. In POPL 2008. ACM, 121-131. https://doi.org/10.1145/1328438.1328456

Jean-Yves Girard. 1972. Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur. https://apisemanticscholar.org/CorpusID:117631778

Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science 50 (1987), 1-102. https://doi.org/10.1016/0304-3975(87)90045-4

Jean-Yves Girard. 1998. Light Linear Logic. Information and Computation 143, 2 (1998), 175-204. https://doi.org/10.1006/inco.1998.2700

Jean-Yves Girard and Yves Lafont. 1987. Linear Logic and Lazy Computation. In TAPSOFT '87 (Lecture Notes in Computer Science, Vol. 250). Springer, 52-66. https://doi.org/10.1007/BFb0014972

Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. Quipper: a scalable quantum programming language. In PLDI 2013. ACM, 333-342. https://doi.org/10.1145/2491956.2462177

Lov K. Grover. 1996. A fast quantum mechanical algorithm for database search. In Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing (Philadelphia, Pennsylvania, USA) (STOC '96). Association for Computing Machinery, New York, NY, USA, 212-219. https://doi.org/10.1145/237814.237866

Yuri Gurevich. 1983. Algebras of Feasible Functions. In FOCS 1983. IEEE Computer Society, 210-214. https://doi.org/10.1109/SFCS.1983.5

Emmanuel Hainry, Romain Péchoux, and Mário Silva. 2023. A Programming Language Characterizing Quantum Polynomial Time. In FoSSaCS 2023 (Lecture Notes in Computer Science, Vol. 13992). Springer, 156-175. https://doi.org/10.1007/978-3-031-30829-1_8

Vesa Halava, Tero Harju, Mika Hirvensalo, and Juhani Karhumäki. 2005. Skolem's Problem - On the Border between Decidability and Undecidability. Technical Report 683.

Martin Hyland and Valeria de Paiva. 1993. Full Intuitionistic Linear Logic (extended abstract). Annals of Pure and Applied Logic 64, 3 (1993), 273-291. https://doi.org/10.1016/0168-0072(93)90146-5

Neil Immerman. 1999. Descriptive complexity. Springer, New York, NY, USA. https://doi.org/10.1007/978-1-4612-0539-5

Julia Kempe. 2003. Quantum random walks: An introductory overview. Contemporary Physics 44, 4 (jul 2003), 307-327. https://doi.org/10.1080/00107151031000110776

Emmanuel Knill. 1996. Conventions for quantum pseudocode. Technical Report LA-UR 96-2724. Los Alamos National Laboratory. http://arxiv.org/abs/2211.02559

Harry G. Mairson. 2004. Linear lambda calculus and PTIME-completeness. Journal of Functional Programming 14, 6 (2004), 623-633. https://doi.org/10.1017/S0956796804005131

Alexandre Miquel. 2011. A survey of classical realizability. In TLCA 2011 (Lecture Notes in Computer Science, Vol. 6690). Springer, 1-2. https://doi.org/10.1007/978-3-642-21691-6_1

Piergiorgio Odifreddi. 1992. Classical recursion theory: The theory of functions and sets of natural numbers. Elsevier, Amsterdam, The Netherlands.

Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. In POPL 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 846-858. https://doi.org/10.1145/3009837.3009894

Romain Péchoux. 2020. Implicit computational complexity: Past and Future. Habilitation à diriger des recherches. Université de Lorraine. https://hal.univ-lorraine.fr/tel-02978986
Lorenzo M. Procopio, Amir Moqanaki, Mateus Araújo, Fabio Costa, Irati Alonso Calafell, Emma G. Dowd, Deny R. Hamel, Lee A. Rozema, Časlav Brukner, and Philip Walther. 2015. Experimental superposition of orders of quantum gates. *Nature communications* 6 (2015), 7913. https://doi.org/10.1038/ncomms8913

John C. Reynolds. 1974. Towards a theory of type structure. In *Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974* (Lecture Notes in Computer Science, Vol. 19), Bernard J. Robinet (Ed.). Springer, 408-423. https://doi.org/10.1007/3-540-06859-7_148

Giulia Rubino, Lee A. Rozema, Adrien Feix, Mateus Araújo, Jonas M. Zeuner, Lorenzo M. Procopio, Časlav Brukner, and Philip Walther. 2017. Experimental verification of an indefinite causal order. *Science advances* 3, 3 (2017), e1602589. https://doi.org/10.1126/sciadv.1602589

Peter Selinger. 2004. Towards a quantum programming language. *Mathematical Structures in Computer Science* 14, 4 (2004), 527-586. https://doi.org/10.1017/S0960129504004256

Peter Selinger and Benoît Valiron. 2006. A lambda calculus for quantum computation with classical control. *Mathematical Structures in Computer Science* 16, 3 (2006), 527-552. https://doi.org/10.1017/S0960129506005238

Jaap Van Oosten (Ed.). 2008. *Realizability: an introduction to its categorical side*. Elsevier, Amsterdam, The Netherlands.

Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. 2023. Qunity: A Unified Language for Quantum and Classical Computing. *Proceedings of the ACM on Programming Languages* 7, POPL (2023), 921-951. https://doi.org/10.1145/3571225

William K. Wooters and Wojciech H. Zurek. 1982. A Single Quantum Cannot be Cloned. *Nature* 299 (1982), 802-803. https://doi.org/10.1038/299802a0

Tomoyuki Yamakami. 2020. A Schematic Definition of Quantum Polynomial Time Computability. *The Journal of Symbolic Logic* 85, 4 (2020), 1546-1587. https://doi.org/10.1017/jsl.2020.45

Andrew Chi-Chih Yao. 1993. Quantum Circuit Complexity. In *FOCS 1993*. IEEE Computer Society, 352-361. https://doi.org/10.1109/SFCS.1993.366852

Mingsheng Ying. 2016. *Foundations of quantum programming*. Morgan Kaufmann, Burlington, MA, USA.

Charles Yuan, Agnes Villanyi, and Michael Carbin. 2023. Quantum Control Machine: The Limits of Quantum Programs as Data. Preprint at arXiv. http://arxiv.org/abs/2304.15000
# A PROOFS

## A.1 Proofs of Section 3

LEMMA A.1 (SUBSTITUTION LEMMA). For any two contexts $\Gamma, \Delta$, the following hold:

(1) If $\Gamma, x : A; \Delta \vdash \vec{t} : B$ and $; [z : C] \vdash \vec{u} : A$ then $[z : C], \Gamma; \Delta \vdash \vec{t}[\vec{u}/x] : B$.

(2) If $\Gamma; \Delta_1, x : A \vdash \vec{t} : B$ and $\Delta_2 \vdash \vec{u} : A$ then $\Gamma; \Delta_1, \Delta_2 \vdash \vec{t}[\vec{u}/x] : B$.

PROOF. By structural induction on $t$.

For 1, consider:

* If $\vec{t} = x$, then by a generation lemma we have that $\Delta = \emptyset$ and for some type $\vec{t}$ we have that $A = \text{\textsection}^{a_s}T$ and $\text{\textsection}^b\text{\textsection}\{\text{\textsection}, \text{\textsection}\}^{a_\#}a_sT \le B$, for $a_\#$, $a_s$, $b \ge 0$. By another generation lemma we have that if $; [z : C] \vdash u : \text{\textsection}^{a_s}T$ then we also have $; [z : C] \vdash u : \{\text{\textsection}, \text{\textsection}\}^{a_\#}a_sT$ and by $\text{\textsection}_i$ and $\text{\textsection}_i$ and finally by $\le$ we obtain $[z; C]; \vdash u : B$, after which context $\Gamma$ can be added via W.

* Let $\vec{t} = \lambda y.\vec{s}$. Then we consider two possible cases:

- $\Gamma, x : A; y : C, \Delta \vdash \vec{s} : D$ and $C \to D \le B$. By induction hypothesis we have that $[z : C], \Gamma; y : C, \Delta \vdash \vec{s}[u/x] : D$ and by rule $\to_i$ we obtain $[z : C], \Gamma; \Delta \vdash \lambda y.\vec{s}[u/x] : C \to D$ as intended. Notice in this case that $\vec{t}[y/x] = (\lambda y.\vec{s})[u/x] = \lambda y.(\vec{s}[u/x])$.

- $\Gamma, x : A, y : C, \Delta \vdash \vec{s} : D$ and $C \Rightarrow D \le B$. Similarly to the first case, by applying the induction hypothesis and rule $\Rightarrow_i$ we obtain $[z : C], \Gamma; \Delta \vdash \lambda y.\vec{s}[u/x] : C \Rightarrow D$.

* $\vec{t} = s r$. Let us consider two cases:

- $\Gamma_1; \Delta_1 \vdash s : C \to D$ and $\Gamma_2; \Delta_2 \vdash r : C$, with $D \le B$, where the contexts are such that $(\Gamma_1, \Gamma_2) = (\Gamma, x : A)$ and $(\Delta_1, \Delta_2) = \Delta$. Let us take the case where $\Gamma_1 = (x : A, \Gamma'_1)$. Then by induction hypothesis we have that $\Gamma'_1; \Delta_1 \vdash s[u/x] : C \to D$. By rule $\to_i$ we can obtain $\Gamma'_1, \Gamma_2; \Delta_1, \Delta_2 \vdash s[u/x]\vec{r} : D$, as desired. Notice that $(s\vec{r})[u/x] = s[u/x]\vec{r}$ in this case. The case where $x : A \in \Gamma_2$ is analogous.

- $\Gamma_1; \Delta_1 \vdash s : C \Rightarrow D$ and $\Gamma_2; \Delta_2 \vdash r : C$, with $D \le B$, where the contexts are such that $(\Gamma_1, \Gamma_2) = (\Gamma, x : A)$ and $(\Delta_1, \Delta_2) = \Delta$. This can be treated similarly to the previous case.

* Let $\vec{t} = if s$ then $\vec{p}_1$ else $\vec{p}_2$. Consider two cases:

- $\Gamma_1; \Delta_1 \vdash s : \mathbb{B}$ and $\Gamma_2; \Delta_2 \vdash (\vec{p}_1 \perp \vec{p}_2) : C$ such that $C \le B$, with $(\Gamma_1, \Gamma_2) = (\Gamma, x : A)$. If $x : A \in \Gamma_1$ then applying the induction hypothesis on $s$ gives the desired result. If $\Gamma_2 = (x : A, \Gamma'_2)$, then by induction hypothesis, we have that $\Gamma'_2; \Delta_2 \vdash (\vec{p}[u/x] \perp \vec{p}[u/x]) : C$. Notice that $\Gamma'_2; \Delta_2 \vdash \vec{p}[u/x] \perp \vec{p}[u/x]$ by definition of orthogonality for open superpositions: that they remain orthogonal for any substitution of open variables by closed superpositions. In particular this means that they remain orthogonal in partial substitutions by open superpositions, since if not we could find a total substitution that would be non-orthogonal. We can apply rule if and obtain $\Gamma_1, \Gamma'_2; \Delta_1, \Delta_2 \vdash$ if $s$ then $\vec{p}_1[u/x]$ else $\vec{p}_2[u/x]$ as intended.

- Case where $\Gamma_1; \Delta_1 \vdash s : \text{\textsection}\mathbb{B}$ is analogous.

* Let $\vec{t} = (t_1, t_2)$, in which case $\Gamma_1; \Delta_1 \vdash t_1 : B_1$ and $\Gamma_2; \Delta_2 \vdash t_2 : B_2$ with $(\Gamma_1, \Gamma_2) = (\Gamma, x : A)$ and $(\Delta_1, \Delta_2) = \Delta$ and $B_1 \times B_2 \le B$. Assume that $\Gamma_1 = (\Gamma'_1, x : A)$, then, by induction hypothesis, $\Gamma'_1; \Delta_1 \vdash t_1[u/x] : B_1$ and so by rule $\times_i$ we have that $\Gamma'_1, \Gamma_2; \Delta \vdash (t_1[u/x], t_2) : B$, which is our desired result. The case where $\Gamma_2 = (\Gamma'_2, x : A)$ is analogous.

* If $\vec{t} = (\text{let } (x_1, x_2) = r \text{ in } \vec{s})$, then consider two options:

- $\Gamma_1; \Delta_1 \vdash r : C \times D$ and $\Gamma_2, x_1 : C, x_2 : D; \Delta_2 \vdash \vec{s} : E$ such that $E \le B$, with $(\Gamma_1, \Gamma_2) = (\Gamma, x : A)$ and $(\Delta_1, \Delta_2) = \Delta$. Assume that $\Gamma_1 = (\Gamma'_1, x : A)$. Then, by induction hypothesis, $\Gamma'_1; \Delta_1 \vdash r[u/x] : C \times D$ and so by rule $\times_{e_1}$ we have that $\Gamma'_1, \Gamma_2; \Delta \vdash \text{let } (x_1, x_2) = r[u/x]$ in $\vec{s} : E$. Notice that in this case $(\Gamma'_1, \Gamma_2) = \Gamma$ and that let $(x_1, x_2) = r[u/x]$ in $\vec{s}$ is $(\text{let } (x_1, x_2) = r \text{ in } \vec{s})[u/x]$. The case where $\Gamma_2 = (\Gamma'_2, x : A)$ is analogous, and so is the case for rule $\times_{e_2}$.
- $\Gamma_1; \Delta_1 \vdash r : \#(C \times D)$ and $\Gamma_2, x_1 : \#C, x_2 : \#D; \Delta_2 \vdash \vec{s} : E$ such that $\#E \le B$. This case can also be treated via the induction hypothesis.

For 2, consider:

* If $\vec{t} = x$, by a generation lemma we have that $\Delta_1 = \emptyset$ and that for some type $\vec{t}$ we have $A = \text{§}^{a_\S}T$ and $B = \{\#\}, \text{§}^{a_\S}\}^{a_\S}T$. From; $\Delta_2 \vdash u : \text{§}^{a_\S}T$ we can also derive; $\Delta_2 \vdash u : B$ by the fact that $\#_i$ does not alter the context. By W we obtain $\Gamma$; $\Delta_2 \vdash u : B$ as desired.

* Let $\vec{t} = \lambda y.\vec{s}$. Then we consider two possible cases:

- $\Gamma; x : A, y : C, \Delta_1 \vdash \vec{s} : D$ and $C \to D \le B$. By induction hypothesis we have that $\Gamma$; $\Delta_1, y : C, \Delta_2 \vdash \vec{s}[u/x] : D$ and by rule $\to_i$ we obtain $\Gamma$; $\Delta_1, \Delta_2 \vdash \lambda y.\vec{s}[u/x] : C \to D$ as intended. Notice in this case that $\vec{t}[y/x] = (\lambda y.\vec{s})[u/x] = \lambda y.(\vec{s}[u/x])$.

- $\Gamma, y : C; x : A, \Delta_1 \vdash \vec{s} : D$ and $C \Rightarrow D \le B$. Similarly to the first case, by applying the induction hypothesis and rule $\Rightarrow_i$ we obtain $\Gamma$; $\Delta_1, \Delta_2 \vdash \lambda y.\vec{s}[u/x] : C \Rightarrow D$.

* $\vec{t} = s r$. Let us consider two cases:

- $\Gamma_1; \Delta_{1,1} \vdash s : C \to D$ and $\Gamma_2; \Delta_{1,2} \vdash r : C$, with $D \le B$, where the contexts are such that $(\Gamma_1, \Gamma_2) = \Gamma$ and $(\Delta_{1,1}, \Delta_{1,2}) = (\Delta_1, x : A)$. Let us take the case where $\Delta_{1,1} = (x : A, \Delta'_{1,1})$. Then by induction hypothesis we have that $\Gamma_1; \Delta'_{1,1} \vdash s[u/x] : C \to D$. By rule $\to_i$ we can obtain $\Gamma_1, \Gamma_2; \Delta'_{1,1}, \Delta_{1,2} \vdash s[u/x]\vec{r} : D$, as desired. Notice that $(s\vec{r})[u/x] = s[u/x]\vec{r}$ in this case. The case where $x : A \in \Delta_{1,2}$ is analogous.

- $\Gamma_1; \Delta_{1,1} \vdash s : C \Rightarrow D$ and $\Gamma_2; \Delta_2 \vdash r : C$, with $D \le B$, can be treated similarly to the previous case.

* Let $\vec{t} = \text{if } s \text{ then } \vec{p}_1 \text{ else } \vec{p}_2$. Consider two cases:

- $\Gamma_1; \Delta_{1,1} \vdash s : \mathbb{B}$ and $\Gamma_2; \Delta_{1,2} \vdash (\vec{p}_1 \perp \vec{p}_2) : C$ such that $C \le B$, with $(\Gamma_1, \Gamma_2) = \Gamma$. If $x : A \in \Delta_{1,1}$ then applying the induction hypothesis on $s$ gives the desired result. If $\Delta_{1,2} = (x : A, \Delta'_{1,2})$, then by induction hypothesis, we have that $\Gamma_2; \Delta'_{1,2} \vdash (\vec{p}[u/x] \perp \vec{p}[u/x]) : C$. We can apply rule if and obtain $\Gamma_1, \Gamma'_2; \Delta_1, \Delta_2 \vdash \text{if } s \text{ then } \vec{p}_1[u/x]$ else $\vec{p}_2[u/x]$ as intended.

- Case where $\Gamma_1; \Delta_{1,1} \vdash s : \#\mathbb{B}$ is analogous.

* Let $\vec{t} = (t_1, t_2)$, in which case $\Gamma_1; \Delta_{1,1} \vdash t_1 : B_1$ and $\Gamma_2; \Delta_2 \vdash t_2 : B_2$ with $(\Gamma_1, \Gamma_2) = \Gamma$ and $(\Delta_{1,1}, \Delta_{1,2}) = (\Delta_1, x : A)$ and $B_1 \times B_2 \le B$. Assume that $\Delta_{1,1} = (\Delta'_{1,1}, x : A)$, then, by induction hypothesis, $\Gamma_1; \Delta'_{1,1} \vdash t_1[u/x] : B_1$ and so by rule $\times_i$ we have that $\Gamma; \Delta'_{1,1}, \Delta_{1,2} \vdash (t_1[u/x], t_2) : B$, which is our desired result. The case where $\Delta_{1,2} = (\Delta'_{1,2}, x : A)$ is analogous.

* If $\vec{t} = (\text{let } (x_1, x_2) = r \text{ in } \vec{s})$, then consider two options:

- $\Gamma_1; \Delta_{1,1} \vdash r : C \times D$ and $\Gamma_2, x_1 : C, x_2 : D; \Delta_{1,2} \vdash \vec{s} : E$ such that $E \le B$, with $(\Gamma_1, \Gamma_2) = \Gamma$ and $(\Delta_{1,1}, \Delta_{1,2}) = \Delta_1$. Assume that $\Delta_{1,1} = (\Delta'_{1,1}, x : A)$. Then, by induction hypothesis, $\Gamma_1; \Delta'_{1,1} \vdash r[u/x] : C \times D$ and so by rule $\times_{e_1}$ we have that $\Gamma; \Delta'_{1,1}, \Delta_{1,2} \vdash \text{let } (x_1, x_2) = r[u/x]$ in $\vec{s} : E$. Notice that in this case let $(x_1, x_2) = r[u/x]$ in $\vec{s}$ is (let $(x_1, x_2) = r$ in $\vec{s})[u/x]$. The case where $\Delta_{1,2} = (\Delta'_{1,2}, x : A)$ is analogous, and so is the case for rule $\times_{e_2}$.

- $\Gamma_1; \Delta_1 \vdash r : \#(C \times D)$ and $\Gamma_2, x_1 : \#C, x_2 : \#D; \Delta_2 \vdash \vec{s} : E$ such that $\#E \le B$. This case can also be treated via the induction hypothesis.

□

**THEOREM 3.3 (SUBJECT REDUCTION).** If; $\vdash \vec{t} : A$ and $\vec{t} \rightsquigarrow \vec{r}$, then; $\vdash \vec{r} : A$.

**PROOF.** By induction on the relation $\rightsquigarrow$.

* $\vec{t}$ is a value. Then, since $\vec{t}$ does not reduce, there is no $\vec{r}$ satisfying the condition and the theorem is trivially satisfied. In the next items assume $v$ is a value, if not then apply induction hypothesis to $v$.

* $\vec{t} = (\lambda x.\vec{p}) v$ and therefore $\vec{r} = \vec{p}[v/x]$. Then, from; $\vdash \vec{t} : A$ we consider two cases:
- ; $\vdash$ $\lambda x.\vec{p} : B \Rightarrow A$, with $x : B$; $\vdash \vec{p} : A$ and ; $\vdash v : B$. Then by the substitution lemma we have that ; $\vdash \vec{p}[v/x] : A$ which is the desired conclusion.

- ; $\vdash \lambda x.\vec{p} : B \sim\to A$, with $x : B$; $\vdash \vec{p} : A$ and ; $\vdash v : B$. Substitution lemma provides the desired result.

* $\vec{t} = \mathbf{if} \ v \ \mathbf{then} \ \vec{p} \ \mathbf{else} \ \vec{s} : A$.

If ; $\vec{t}$ then rule if implies that $\vec{p} \perp_A \vec{s}$. There are two cases:

(1) $v = |0\rangle$, and therefore $t \rightsquigarrow \vec{p}$ and the conclusion follows,

(2) $v = |1\rangle$, and $t \rightsquigarrow \vec{s}$ and the conclusion also follows.

Analogous case where we used rule if_‡.

* $\vec{t} = \mathbf{let} \ (x, y) = (v, w) \ \mathbf{in} \ \vec{s}$, then consider 3 cases:

(1) We used $\times_{e_1}$ and so from ; $\vec{t} : A$ we have that ; $\vdash (v, w) : B \times C$ and ; $x : B, y : C \vdash \vec{s} : A$. This means that ; $\vdash v : B$ and ; $\vdash w : C$ and therefore by applying the substitution lemma twice we obtain ; $\vdash \vec{s}[v/x, w/y] : A$ as desired.

(2) Similar case to $\times_{e_2}$.

(3) Similar case for $\times_{e_\#}$.

□

**THEOREM 3.4 (PROGRESS).** If ; $\vec{t} : A$, then either $\vec{t} \rightsquigarrow \vec{r}$ for some $\vec{r}$ or $\vec{t} \in V$.

**PROOF.** By induction on the structure of $\vec{t}$.

* $\vec{t} = x$. Cannot be typed with a closed context.

* $\vec{t} = |0\rangle$. This is a value.

* $\vec{t} = |1\rangle$. This is a value.

* $\vec{t} = \mathbf{if} \ r \ \mathbf{then} \ \vec{s}_0 \ \mathbf{else} \ \vec{s}_1$. Since $r$ must be a boolean, either $r \rightsquigarrow \vec{r}'$ and therefore $\vec{t} \rightsquigarrow \vec{r}'$ then $\vec{s}_0$ else $\vec{s}_1$ by rule (If_+), or by induction hypothesis $r$ must be a value and therefore either $r = |0\rangle$ or $r = |1\rangle$. In any of these two cases, $\vec{t}$ reduces, either by (If_0) or (If_1).

* $\vec{t} = \lambda x.\vec{p}$ is a value.

* $\vec{t} = s \ r$. We consider the three cases.

(1) $r$ is not a value. By the induction hypothesis, $r \rightsquigarrow \vec{r}'$ and by rule (App), $\vec{t} \rightsquigarrow s \vec{r}'$.

(2) $r$ is a value and $s$ is not. By the induction hypothesis, $s \rightsquigarrow \vec{s}'$ and by rule (App_√), $\vec{t} \rightsquigarrow \vec{s}' \ r$.

(3) Both $r$ and $s$ are values. Therefore $s = \lambda x.\vec{p}$ for some $\vec{p}$ and by rule (Abs) we have that $\vec{t} = (\lambda x.\vec{p}) \ r \rightsquigarrow \vec{p}[s/x]$.

* $\vec{t} = (s, r)$. We consider the two possible cases where $\vec{t}$ is not a value:

(1) $s$ is a value and $r$ is not, in which case by the induction hypothesis $r \rightsquigarrow \vec{r}'$ and therefore by rule (Pair_√) we have that $\vec{t} \rightsquigarrow (s, \vec{r}')$.

(2) $s$ is not a value, in which case by the induction hypothesis $s \rightsquigarrow \vec{s}'$ and therefore by rule (Pair) we have that $\vec{t} \rightsquigarrow (\vec{s}', r)$.

* $\vec{t} = \mathbf{let} \ (x, y) = s \ \mathbf{in} \ \vec{r}$. Consider two cases:

(1) $s$ is a value of the form $(v, w)$, in which case by rule (Let), we have $\vec{t} \rightsquigarrow \vec{r}[v/x, w/y]$.

(2) $s$ is not a value and therefore by the induction hypothesis $s \rightsquigarrow \vec{s}'$ and we have that $\vec{t} \rightsquigarrow \mathbf{let} \ (x, y) = \vec{s}' \ \mathbf{in} \ \vec{r}$.

* $\vec{t} = \vec{0}$. This is a value.

* $\vec{t} = \alpha \cdot \vec{s}$, in which case either $\vec{s}$ is a value and therefore $\vec{t}$ is also a value, or $\vec{s} \rightsquigarrow \vec{s}'$ and by rule (Sup), $\vec{t} \rightsquigarrow \alpha \cdot \vec{s}$.

* $\vec{t} = \vec{s} + \vec{r}$, and by rule (Sup) if $\vec{s}$ or $\vec{r}$ are not values then $\vec{t}$ also reduces.

□
## A.2 Proofs of Section 5

LEMMA 5.1. Let $A \in \mathbb{T}_s$, then $\llbracket!(A)\rrbracket_0 = b\llbracket A\rrbracket_0$.

PROOF. First we state the following straightforward properties.

(1) For any set $S \subseteq \mathcal{B}\mathcal{V}_c$, we have $S = bS$.

(2) For any set $S \subseteq \mathcal{V}_c$, we have $bS = b\operatorname{span}(S)$.

(3) For any set $S \subseteq \mathcal{B}\mathcal{V}_c$, we have $S = S \cap S_1$.

Then we proceed by induction on the structure of simple types.

* If $A = \mathbb{B}$, then $!(A) =!(\mathbb{B}) = \mathbb{B}$. Hence

$$ \llbracket!(A)\rrbracket_0 = \llbracket\mathbb{B}\rrbracket_0 =^{(1)} b\llbracket\mathbb{B}\rrbracket_0 = b\llbracket A\rrbracket_0 $$

* If $A = B \to C$, then $!(A) =!(B \to C) = B \to C$. Hence,

$$ \llbracket!(A)\rrbracket_0 = \llbracket!(B \to C)\rrbracket_0 = \llbracket B \to C\rrbracket_0 =^{(1)} b\llbracket B \to C\rrbracket_0 = b\llbracket A\rrbracket_0 $$

* If $A = B \Rightarrow C$, then $!(A) =!(B \Rightarrow C) = B \Rightarrow C$. Hence,

$$ \llbracket!(A)\rrbracket_0 = \llbracket!(B \Rightarrow C)\rrbracket_0 = \llbracket B \Rightarrow C\rrbracket_0 =^{(1)} b\llbracket B \Rightarrow C\rrbracket_0 = b\llbracket A\rrbracket_0 $$

* If $A = B \times C$, then $!(A) =!(B) \times !(C)$. Hence,

$$ \begin{aligned} \llbracket!(A)\rrbracket_0 &= \llbracket!(B) \times !(C)\rrbracket_0 = \{(\vec{v}, \vec{w}) : \vec{v} \in \llbracket!(B)\rrbracket_0, \vec{w} \in \llbracket!(C)\rrbracket_0\} \\ &=^{(\mathrm{IH})} \{(\vec{v}, \vec{w}) : \vec{v} \in b\llbracket B\rrbracket_0, \vec{w} \in b\llbracket C\rrbracket_0\} = b\{(\vec{v}, \vec{w}) : \vec{v} \in \llbracket B\rrbracket_0, \vec{w} \in \llbracket C\rrbracket_0\} \\ &= b(\llbracket B \times C\rrbracket_0) = b\llbracket A\rrbracket_0 \end{aligned} $$

* If $A = \#B$, then $!(A) =!(\#B) =!(B)$. Hence,

$$ \begin{aligned} \llbracket!(A)\rrbracket_0 &= \llbracket!(B)\rrbracket_0 =^{(\mathrm{IH})} b\llbracket B\rrbracket_0 =^{(2)} b\operatorname{span}(\llbracket B\rrbracket_0) =^{(3)} b\operatorname{span}(\llbracket B\rrbracket_0) \cap S_1 \\ &=^{(3)} b(\operatorname{span}(\llbracket B\rrbracket_0) \cap S_1) = b\llbracket \#B\rrbracket_0 = b\llbracket A\rrbracket_0 \end{aligned} $$

* If $A = \%B$, then $!(A) =!(\%B) =!(B)$. Hence,

$$ \llbracket!(A)\rrbracket_0 = \llbracket\%!(B)\rrbracket_0 = \llbracket!(B)\rrbracket_0 =^{(\mathrm{IH})} b\llbracket B\rrbracket_0 = b\llbracket\%B\rrbracket_0 = b\llbracket A\rrbracket_0 $$

LEMMA 5.2. Let $A, B \in \mathbb{T}$ and $\tau$ defined in $\mathrm{FV}(A, B)$. Then, $\llbracket A[B/X]\rrbracket_{\tau} = \llbracket A\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}}$.

PROOF. By induction on A.

* If $A = X$, then $A[B/X] = B$. Hence,

$$ \llbracket A[B/X]\rrbracket_{\tau} = \llbracket B\rrbracket_{\tau} = \llbracket X\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} = \llbracket A\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} $$

* If $A = Y \neq X$, then $A[B/X] = Y$. Hence,

$$ \llbracket A[B/X]\rrbracket_{\tau} = \llbracket Y\rrbracket_{\tau} = \tau(Y) = (\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\})(Y) = \llbracket Y\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} = \llbracket A\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} $$

* If $A = \mathbb{B}$, then $A[B/X] = \mathbb{B}$. Hence,

$$ \llbracket A[B/X]\rrbracket_{\tau} = \llbracket \mathbb{B}\rrbracket_{\tau} = \{\vert 0\vert, \vert 1\vert\} = \llbracket \mathbb{B}\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} = \llbracket A\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} $$

* If $A = C \to D$, then $A[B/X] = C[B/X] \to D[B/X]$. Hence,

$$ \begin{aligned} \llbracket A[B/X]\rrbracket_{\tau} &= \llbracket C[B/X] \to D[B/X]\rrbracket_{\tau} = \{\lambda x.\vec{t} : \vec{v} \in \llbracket C[B/X]\rrbracket_{\tau}, \vec{t}\langle\vec{v}/x\rangle \models \llbracket D[B/X]\rrbracket_{\tau}\} \\ &=^{(\mathrm{IH})} \{\lambda x.\vec{t} : \vec{v} \in \llbracket C\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}}, \vec{t}\langle\vec{v}/x\rangle \models \llbracket D\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}}\} \\ &= \llbracket C \to D\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} = \llbracket A\rrbracket_{\tau \cup \{X \mapsto \llbracket B\rrbracket_{\tau}\}} \end{aligned} $$
• If $A = C \Rightarrow D$, then $A[B/X] = C[B/X] \Rightarrow D[B/X]$. Hence,

$$ 
\begin{align*}
\llbracket A[B/X] \rrbracket_{\tau} &= \llbracket C[B/X] \Rightarrow D[B/X] \rrbracket_{\tau} = \{\lambda x. \vec{t} : \vec{v} \in \flat \llbracket C[B/X] \rrbracket_{\tau}, \vec{t}[\vec{v}/x] \models \llbracket D[B/X] \rrbracket_{\tau} \} \\
&= \text{(IH)} \quad \{\lambda x. \vec{t} : \vec{v} \in \flat \llbracket C \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}, \vec{t}[\vec{v}/x] \models \llbracket D \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\} \} \\
&= \llbracket C \Rightarrow D \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\} = \llbracket A \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}
\end{align*}
$$

• If $A = C \times D$, then $A[B/X] = C[B/X] \times D[B/X]$. Hence,

$$ 
\begin{align*}
\llbracket A[B/X] \rrbracket_{\tau} &= \llbracket C[B/X] \times D[B/X] \rrbracket_{\tau} = \{(\vec{v}, \vec{w}) : \vec{v} \in \llbracket C[B/X] \rrbracket_{\tau}, \vec{w} \in \llbracket D[B/X] \rrbracket_{\tau} \} \\
&= \text{(IH)} \quad \{(\vec{v}, \vec{w}) : \vec{v} \in \llbracket C \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}, \vec{w} \in \llbracket D \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}, \} \\
&= \llbracket C \times D \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\} = \llbracket A \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}
\end{align*}
$$

• If $A = \sharp C$, then $A[B/X] = \sharp C[B/X]$. Hence,

$$ 
\begin{align*}
\llbracket A[B/X] \rrbracket_{\tau} &= \llbracket \sharp C[B/X] \rrbracket_{\tau} = \operatorname{span}(\llbracket C[B/X] \rrbracket_{\tau}) \cap S_1 \\
&= \text{(IH)} \operatorname{span}(\llbracket C \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}) \cap S_1 = \llbracket \sharp C \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\} = \llbracket A \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}
\end{align*}
$$

• If $A = \$ C$, then $A[B/X] = \$ C[B/X]$. Hence,

$$ 
\begin{align*}
\llbracket A[B/X] \rrbracket_{\tau} &= \llbracket \$ C[B/X] \rrbracket_{\tau} = \llbracket C[B/X] \rrbracket_{\tau} \\
&= \text{(IH)} \quad \llbracket C \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\} = \llbracket \$ C \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\} = \llbracket A \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}
\end{align*}
$$

• If $A = \forall Y.C$, then $A[B/X] = \forall Y.C[B/X]$. Hence,

$$ 
\begin{align*}
\llbracket A[B/X] \rrbracket_{\tau} &= \llbracket \forall Y.C[B/X] \rrbracket_{\tau} = \bigcap_{R \subseteq S_1} \llbracket C[B/X] \rrbracket_{\tau} \cup \{Y \mapsto R\} \\
&= \text{(IH)} \bigcap_{R \subseteq S_1} \llbracket C \rrbracket_{\tau} \cup \{Y \mapsto R, X \mapsto \llbracket B \rrbracket_{\tau}\} = \llbracket \forall Y.C \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\} = \llbracket A \rrbracket_{\tau} \cup \{X \mapsto \llbracket B \rrbracket_{\tau}\}
\end{align*}
$$

□

THEOREM 5.3. The typing rules in Figure 6 are valid.

PROOF.

(W) Assume that $\Gamma; \Delta \vdash \vec{t} : A$ is a valid typing judgment. Then $\operatorname{dom}(\Delta) \subseteq \operatorname{FV}(\vec{t}) \subseteq \operatorname{dom}(\Gamma, \Delta)$, and $\vec{t}\langle\sigma\rangle \models A$, for any $\sigma \in \llbracket \Gamma, \Delta \rrbracket_{\tau}$. Given a variable $x$ with type $B$ such that $x \notin \operatorname{dom}(\Gamma, \Delta)$, we have that $\operatorname{dom}(\Delta) \subseteq \operatorname{FV}(\vec{t}) \subseteq \operatorname{dom}(\Gamma, \Delta) \cup \{x\}$. Now, for any substitution $\sigma \in \llbracket \Gamma, \Delta, \{x : B\} \rrbracket_{\tau}$, we have that $\sigma = \sigma_0\langle\vec{v}/x\rangle$ for some $\sigma_0 \in \llbracket \Gamma, \Delta \rrbracket_{\tau}$ and $\vec{v} \models B$. Then,

$$ \vec{t}\langle\sigma\rangle = \vec{t}[\vec{v}/x]\langle\sigma_0\rangle = \vec{t}\langle\sigma_0\rangle \models A, $$

since $\sigma_0 \in \llbracket \Gamma, \Delta \rrbracket_{\tau}$ and $x \notin \operatorname{FV}(\vec{t})$.

(C) The premise being valid, this means that $\operatorname{dom}(\Delta) \subseteq \operatorname{FV}(\vec{t}) \subseteq \operatorname{dom}(\Gamma, \Delta) \cup \{x, y\}$ and for all $\sigma \in \llbracket \Gamma, \Delta, \{x : B, y : B\} \rrbracket_{\tau}$ we have that $\vec{t}\langle\sigma\rangle \models A$. It is clear that $\operatorname{FV}(\vec{t}[x/y]) \subseteq \operatorname{dom}(\Gamma, \Delta) \cup \{x\}$. For any $\sigma \in \llbracket \Gamma, \Delta, \{x : B\} \rrbracket_{\tau}$, $\sigma = \sigma_0\langle\vec{v}/x\rangle$ for some $\sigma_0 \in \llbracket \Gamma, \Delta \rrbracket_{\tau}$ and some value $\vec{v} \in \llbracket B \rrbracket_{\tau}$. Therefore,

$$ 
\begin{align*}
(\vec{t}[x/y])\langle\sigma\rangle &= (\vec{t}[x/y])\langle x/\vec{v}, \sigma_0 \rangle = (\vec{t}[x/y][\vec{v}/x])\langle\sigma_0\rangle \\
&= (\vec{t}[\vec{v}/x][x/y])\langle\sigma_0\rangle = (\vec{t}[\vec{v}/x][\vec{v}/y])\langle\sigma_0\rangle \\
&= \vec{t}\langle\vec{v}/x, \vec{v}/y, \sigma_0\rangle \models A,
\end{align*}
$$

since $\langle\vec{v}/x, \vec{v}/y, \sigma_0\rangle \in \llbracket \Gamma, \Delta, \{x : B, y : B\} \rrbracket_{\tau}$.

(≡) By associativity of the substitution.

(≤) By definition of subtyping.
(ax) We have that $\text{dom}(\Delta) = \{x\} = \text{FV}(x)$ and $\text{dom}(\Gamma) = \tau$. For any substitution $\sigma \in [[x:A]_\tau$, we have $\sigma = \{\vec{v}/x\}$ for some $\vec{v} \in [[A]_\tau]$. Therefore $x\langle\sigma\rangle = x\langle\vec{v}/x\rangle = \vec{v} \models [[A]_\tau]$.

(0) The rule is valid since $\text{FV}(|0\rangle) = \emptyset$ and $|0\rangle \in [[\mathbb{B}]_\emptyset]$ by definition.

(1) Similar to (0).

(if) Supposing that the premises are valid, we obtain:

(1) $\text{dom}(\Delta_1) \subseteq \text{FV}(t) \subseteq \text{dom}(\Gamma_1, \Delta_1)$ and $t\langle\sigma\rangle \models [[\mathbb{B}]_\emptyset]$ for all $\sigma \in [[\Gamma_1, \Delta_1]_\tau]$.

(2) $\text{dom}(\Delta_2) \subseteq \text{FV}(\vec{r}) \subseteq \text{dom}(\Gamma_2, \Delta_2)$ and $\vec{r}\langle\sigma\rangle \models [[A]_\tau]$ for all $\sigma \in [[\Gamma_2, \Delta_2]_\tau]$.

(3) $\text{dom}(\Delta_2) \subseteq \text{FV}(\vec{s}) \subseteq \text{dom}(\Gamma_2, \Delta_2)$ and $\vec{s}\langle\sigma\rangle \models [[A]_\tau]$ for all $\sigma \in [[\Gamma_2, \Delta_2]_\tau]$.

From (1)-(3) we have that $\text{dom}(\Delta_1, \Delta_2) \subseteq \text{FV}(\text{if } t \text{ then } \vec{r} \text{ else } \vec{s}) \subseteq \text{dom}(\Gamma_1, \Delta_1, \Gamma_2, \Delta_2)$. Given $\sigma \in [[\Gamma_1, \Delta_1, \Gamma_2, \Delta_2]]_\tau$, then $\sigma = \sigma_1\sigma_2$ for $\sigma_i \in [[\Gamma_i, \Delta_i]]_\tau$, and we have that

$$ \begin{aligned} & (\text{if } t \text{ then } \vec{r} \text{ else } \vec{s})\langle\sigma\rangle \\ &= (\text{if } t \text{ then } \vec{r} \text{ else } \vec{s})\langle\sigma_1\rangle\langle\sigma_2\rangle \\ &= \text{if } t\langle\sigma_1\rangle \text{ then } \vec{r}\langle\sigma_2\rangle \text{ else } \vec{s}\langle\sigma_2\rangle. \end{aligned} $$

Since $\sigma_1 \in [[\Gamma_1, \Delta_1]]_\tau$ we have that $t\langle\sigma_1\rangle \models [[\mathbb{B}]_\emptyset]$ from (1). Therefore we can consider two cases:

$$ - t\langle\sigma_1\rangle \rightsquigarrow |0\rangle \text{ such that} $$

$$ \begin{aligned} & (\text{if } t \text{ then } \vec{r} \text{ else } \vec{s})\langle\sigma\rangle \\ &= \text{if } t\langle\sigma_1\rangle \text{ then } \vec{r}\langle\sigma_2\rangle \text{ else } \vec{s}\langle\sigma_2\rangle \\ \rightsquigarrow & \text{ if } |0\rangle \text{ then } \vec{r}\langle\sigma_2\rangle \text{ else } \vec{s}\langle\sigma_2\rangle \\ \rightsquigarrow & \vec{r}\langle\sigma_2\rangle \models [[A]_\tau] \end{aligned} $$

using (2) and the fact that $\sigma_2 \in [[\Gamma_2, \Delta_2]]_\tau$. The second case is similar:
$- t\langle\sigma_1\rangle \rightsquigarrow |1\rangle$ such that

$$ \begin{aligned} & (\text{if } t \text{ then } \vec{r} \text{ else } \vec{s})\langle\sigma\rangle \\ &= \text{if } t\langle\sigma_1\rangle \text{ then } \vec{r}\langle\sigma_2\rangle \text{ else } \vec{s}\langle\sigma_2\rangle \\ \rightsquigarrow & \text{ if } |1\rangle \text{ then } \vec{r}\langle\sigma_2\rangle \text{ else } \vec{s}\langle\sigma_2\rangle \\ \rightsquigarrow & \vec{s}\langle\sigma_2\rangle \models [[A]_\tau]. \end{aligned} $$

(if#) From the premises we deduce:

(1) $\text{dom}(\Delta_1) \subseteq \text{FV}(\vec{t}) \subseteq \text{dom}(\Gamma_1, \Delta_1)$ and $\vec{t}\langle\sigma\rangle \models [[\#\mathbb{B}]_\emptyset]$ for all $\sigma \in [[\Gamma_1, \Delta_1]_\tau]$.

(2) $\text{dom}(\Delta_2) \subseteq \text{FV}(\vec{r}) \subseteq \text{dom}(\Gamma_2, \Delta_2)$ and $\vec{r}\langle\sigma\rangle \models [[Q]_\tau]$ for all $\sigma \in [[\Gamma_2, \Delta_2]_\tau]$.

(3) $\text{dom}(\Delta_2) \subseteq \text{FV}(\vec{s}) \subseteq \text{dom}(\Gamma_2, \Delta_2)$ and $\vec{s}\langle\sigma\rangle \models [[Q]_\tau]$ for all $\sigma \in [[\Gamma_2, \Delta_2]_\tau]$.

(4) For all $\sigma \in [[\Gamma_2, \Delta_2]]_\tau$, we have that $\vec{r}\langle\sigma\rangle \rightsquigarrow \vec{v}$ and $\vec{s}\langle\sigma\rangle \rightsquigarrow \vec{w}$ such that $\langle\vec{v}, \vec{w}\rangle = 0$.

Similarly to (if), we have that $\text{dom}(\Delta_1, \Delta_2) \subseteq \text{FV}(\text{if } t \text{ then } \vec{r} \text{ else } \vec{s}) \subseteq \text{dom}(\Gamma_1, \Delta_1, \Gamma_2, \Delta_2)$ and, given a $\sigma \in [[\Gamma_1, \Delta_1, \Gamma_2, \Delta_2]]_\tau$, then $\sigma = \sigma_1\sigma_2$ for $\sigma_i \in [[\Gamma_i, \Delta_i]]_\tau$, and we have that

$$ \begin{aligned} & (\text{if } t \text{ then } \vec{r} \text{ else } \vec{s})\langle\sigma\rangle \\ &= (\text{if } t \text{ then } \vec{r} \text{ else } \vec{s})\langle\sigma_1\rangle\langle\sigma_2\rangle \\ &= \text{if } t\langle\sigma_1\rangle \text{ then } \vec{r}\langle\sigma_2\rangle \text{ else } \vec{s}\langle\sigma_2\rangle. \end{aligned} $$
From (1) and the fact that $\sigma_1 \in [\Gamma_1, \Delta_1]_\tau$ we deduce $t\langle\sigma_1\rangle \models \#\mathbb{B}$ and therefore $t\langle\sigma_1\rangle \rightsquigarrow$
$\alpha \cdot |0\rangle + \beta \cdot |1\rangle$, for $\alpha, \beta \in \overline{\mathbb{Q}}$ such that $|\alpha|^2 + |\beta|^2 = 1$. Therefore,

$$
\begin{align*}
& (\text{if } t \text{ then } \vec{r} \text{ else } \vec{s}) \langle \sigma \rangle \\
&= \text{if } t \langle \sigma_1 \rangle \text{ then } \vec{r} \langle \sigma_2 \rangle \text{ else } \vec{s} \langle \sigma_2 \rangle \\
&\rightsquigarrow^* \text{ if } (\alpha \cdot |0\rangle + \beta \cdot |1\rangle) \text{ then } \vec{r} \langle \sigma_2 \rangle \text{ else } \vec{s} \langle \sigma_2 \rangle \\
&= \alpha \cdot (\text{if } |0\rangle \text{ then } \vec{r} \langle \sigma_2 \rangle \text{ else } \vec{s} \langle \sigma_2 \rangle) + \beta \cdot (\text{if } |1\rangle \text{ then } \vec{r} \langle \sigma_2 \rangle \text{ else } \vec{s} \langle \sigma_2 \rangle) \\
&\rightsquigarrow^* \alpha \cdot \vec{r} \langle \sigma_2 \rangle + \beta \cdot \vec{s} \langle \sigma_2 \rangle \\
&\rightsquigarrow^* \alpha \cdot \vec{v} + \beta \cdot \vec{w} \models [\#Q]_\tau
\end{align*}
$$

derived from (2)-(4) and the fact that $\sigma_2 \in [\Gamma_2, \Delta_2]_\tau$.

(→ᵢ) Suppose that $\Gamma; \Delta, x : A \vdash \vec{t} : B$ is a valid judgment. Then since $(\mathrm{dom}(\Delta) \cup \{x\}) \subseteq \mathrm{FV}(\vec{t})$
we have $\mathrm{dom}(\Delta) \subseteq \mathrm{FV}(\lambda x.\vec{t})$. Similarly, since $\mathrm{FV}(\vec{t}) \subseteq (\mathrm{dom}(\Gamma, \Delta) \cup \{x\})$ it is also true
that $\mathrm{FV}(\lambda x.\vec{t}) \subseteq \mathrm{dom}(\Gamma, \Delta)$. For any $\sigma \in [\Gamma, \Delta]_\tau$, we have that $(\lambda x.\vec{t})\langle\sigma\rangle = \lambda x.\vec{t}\langle\sigma\rangle$, since
$x \notin \mathrm{dom}(\sigma)$. For all $\vec{v} \in [A]_\tau$, we observe that $(\vec{t}\langle\sigma\rangle)\langle\vec{v}/x\rangle = \vec{t}\langle\sigma, \{\vec{v}/x\}\rangle \models [B]_\tau$, since
$\sigma, \{\vec{v}/x\} \in [\Gamma, x : A]_\tau$. Therefore, $(\lambda x.\vec{t})\langle\sigma\rangle \models [A \to B]_\tau$.

(⇒ᵢ) Suppose that $\Gamma, x : A; \Delta \vdash t : B$ is a valid judgment. Then $\mathrm{dom}(\Delta) \subseteq \mathrm{FV}(t) \subseteq \mathrm{dom}(\Gamma, \{x : A\}, \Delta)$. We can therefore conclude that $\mathrm{dom}(\Delta) \subseteq \mathrm{FV}(\lambda x.t) \subseteq \mathrm{dom}(\Gamma, \Delta)$. Given $\sigma \in [\Gamma, \Delta]_\tau$ we want to show that $(\lambda x.t)\langle\sigma\rangle \models [\mathbf{!}(A) \Rightarrow B]_\tau$. Since $x \notin \mathrm{dom}(\sigma)$, we have $(\lambda x.t)\langle\sigma\rangle = \lambda x.(t\langle\sigma\rangle)$, and for all values $\vec{v} \in [A]_\tau$, we have that

$$
t\langle\sigma\rangle\langle\vec{v}/x\rangle = t\langle\sigma, \{\vec{v}/x\}\rangle \models [B]_{\tau}
$$

from the premise. Since $b[A]_\tau \subseteq [A]_\tau$, we have that $(\lambda x.t)\langle\sigma\rangle \models [\mathbf{!}(A) \Rightarrow B]_\tau$.

(→ₑ) Suppose that both judgments $\Gamma_1; \Delta_1 \vdash t : A \to B$ and $\Gamma_2; \Delta_2 \vdash \vec{r} : A$ are valid, meaning that:
- $\mathrm{dom}(\Delta_1) \subseteq \mathrm{FV}(t) \subseteq \mathrm{dom}(\Gamma_1, \Delta_1)$ and $t\langle\sigma\rangle \models [A \to B]_\tau$ for all $\sigma \in [\Gamma_1, \Delta_1]_\tau$.
- $\mathrm{dom}(\Delta_2) \subseteq \mathrm{FV}(\vec{r}) \subseteq \mathrm{dom}(\Gamma_2, \Delta_2)$ and $\vec{r}\langle\sigma\rangle \models [A]_\tau$ for all $\sigma \in [\Gamma_2, \Delta_2]_\tau$.
This implies that $\mathrm{dom}(\Delta_1, \Delta_2) \subseteq \mathrm{FV}(t\vec{r}) \subseteq \mathrm{dom}(\Gamma_1, \Delta_1, \Gamma_2, \Delta_2)$. Given $\sigma \in [\Gamma_1, \Delta_1, \Gamma_2, \Delta_2]_\tau$, then
$\sigma = \sigma_1\sigma_2$ for $\sigma_i \in [\Gamma_i, \Delta_i]_\tau$, and from $\mathrm{FV}(t) \cap \mathrm{dom}(\sigma_2) = \mathrm{FV}(\vec{r}) \cap \mathrm{dom}(\sigma_1) = \emptyset$, then

$$
(t \vec{r}) \langle \sigma \rangle = (t \vec{r}) \langle \sigma_1 \rangle \langle \sigma_2 \rangle = (t \langle \sigma_1 \rangle \vec{r}) \langle \sigma_2 \rangle = t \langle \sigma_1 \rangle \vec{r} \langle \sigma_2 \rangle,
$$

and so we conclude that $(t \vec{r}) \langle \sigma \rangle = t \langle \sigma_1 \rangle \vec{r} \langle \sigma_2 \rangle \models [B]_\tau$, by the application of realizers [Díaz-Caro et al. 2019b, Lemma A.4].

(⇒ₑ) Assuming the premises are valid, we have that
- $\mathrm{dom}(\Delta) \subseteq \mathrm{FV}(t) \subseteq \mathrm{dom}(\Gamma, \Delta)$ and $t\langle\sigma\rangle \models [\mathbf{!}(A) \Rightarrow B]_\tau$ for all $\sigma \in [\Gamma, \Delta]_\tau$.
- $\mathrm{FV}(r) = \{z\}$ and $r\langle\sigma\rangle \models \mathbf{!}A$ for all $\sigma \in [z : C]_\tau$.

We can directly conclude that $\mathrm{dom}(\Delta) \subseteq \mathrm{FV}(t) \subseteq \mathrm{dom}(\Gamma, \Delta) \cup \{z\}$. From the fact that $z \notin \mathrm{dom}(\Gamma, \Delta)$, we have that for any $\sigma \in [\Gamma, \Delta, \{z : C\}]_\tau$, $\sigma = \sigma_1\sigma_2$ for $\sigma_1 \in [\Gamma, \Delta]_\tau$ and $\sigma_2 \in [\{z : C\}]_\tau$. Therefore

$$
(t r)\langle\sigma\rangle = (t r)\langle\sigma_1\rangle\langle\sigma_2\rangle = t\langle\sigma_1\rangle r\langle\sigma_2\rangle \models [B]_\tau,
$$

by the application of realizers.

$(\times_i)$ Assuming that $\Gamma_1; \Delta_1 \vdash \vec{t} : A$ and $\Gamma_2; \Delta_2 \vdash \vec{r} : B$ are valid typing judgments, we have that
(1) $\mathrm{dom}(\Delta_1) \subseteq \mathrm{FV}(\vec{t}) \subseteq \mathrm{dom}(\Gamma_1, \Delta_1)$ and $\vec{t}\langle\sigma\rangle \models [A]_\tau$ for all $\sigma \in [\Gamma_1, \Delta_1]_\tau$.

(2) $\mathrm{dom}(\Delta_2) \subseteq \mathrm{FV}(\vec{r}) \subseteq \mathrm{dom}(\Gamma_2, \Delta_2)$ and $\vec{r}\langle\sigma\rangle \models [B]_\tau$ for all $\sigma \in [\Gamma_2, \Delta_2]_\tau$.
We have that $\text{dom}(\Delta_1, \Delta_2) \subseteq \text{FV}(\langle \vec{t}, \vec{r} \rangle) \subseteq \text{dom}(\Gamma_1, \Delta_1, \Gamma_2, \Delta_2)$. For any $\sigma \in [[\Gamma_1, \Delta_1, \Gamma_2, \Delta_2]]_\tau$ we have that $\sigma = \sigma_1\sigma_2$ for $\sigma_i \in [[\Gamma_i, \Delta_i]]_\tau$ and, from the disjointness of contexts, we deduce:

$$ (\vec{t}, \vec{r}) \langle \sigma \rangle = (\vec{t}, \vec{r}) \langle \sigma_1 \rangle \langle \sigma_2 \rangle \\ = (\vec{t} \langle \sigma_1 \rangle, \vec{r} \langle \sigma_2 \rangle) \Vdash [[A \times B]]_\tau, $$

derived from the definition of $[[A \times B]]_\tau$.

(×_e) Supposing that the judgments $\Gamma_1; \Delta_1 \vdash t : A \times B$ and $\Gamma_2; \Delta_2, x : A, y : B \vdash \vec{s} : C$ are valid, we obtain:

(1) $\text{dom}(\Delta_1) \subseteq \text{FV}(t) \subseteq \text{dom}(\Gamma_1, \Delta_1)$ and $t \langle \sigma \rangle \Vdash [[A \times B]]_\tau$ for all $\sigma \in [[\Gamma_1, \Delta_1]]_\tau$.

(2) $\text{dom}(\Delta_2) \cup \{x, y\} \subseteq \text{FV}(\vec{s}) \subseteq \text{dom}(\Gamma_2, \Delta_2) \cup \{x, y\}$ and $\vec{s} \langle \sigma \rangle \Vdash [[C]]_\tau$ for all $\sigma \in [[\Gamma_2, \Delta_2, \{x : A, y : B\}]]]_\tau$.

We have that $\text{dom}(\Delta_1, \Delta_2) \subseteq \text{FV}(\text{let } (x, y) = t \text{ in } \vec{s}) \subseteq \text{dom}(\Gamma_1, \Delta_1, \Gamma_2, \Delta_2)$. For any $\sigma \in [[\Gamma_1, \Delta_1, \Gamma_2, \Delta_2]]_\tau$ we have that $\sigma = \sigma_1\sigma_2$ for $\sigma_i \in [[\Gamma_i, \Delta_i]]_\tau$ and therefore

$$ \begin{aligned} (\text{let } (x, y) = t \text{ in } \vec{s}) \langle \sigma \rangle &= (\text{let } (x, y) = t \text{ in } \vec{s}) \langle \sigma_1 \rangle \langle \sigma_2 \rangle \\ &= \text{let } (x, y) = t \langle \sigma_1 \rangle \text{ in } \vec{s} \langle \sigma_2 \rangle \\ &\rightsquigarrow^* \text{let } (x, y) = \langle \vec{v}, \vec{w} \rangle \text{ in } \vec{s} \langle \sigma_2 \rangle \\ &\rightsquigarrow^* (\vec{s}[\vec{v}/x, \vec{w}/y]) \langle \sigma_2 \rangle \\ &= \vec{s} \langle \vec{v}/x, \vec{w}/y, \sigma_2 \rangle \Vdash [[C]]_\tau \end{aligned} $$

from the fact that $\langle \vec{v}/x, \vec{w}/y, \sigma_2 \rangle \in [[\Gamma_2, \Delta_2, \{x : A, y : B\}]]]_\tau$ and [Díaz-Caro et al. 2019b, Lemmas A.10 and A.3].

(×_e\#) From the validity of $\Gamma_1; \Delta_1 \vdash \vec{t} : \#(Q \times R)$ and $\Gamma_2; \Delta_2, x : \#Q, y : \#R \vdash \vec{s} : S$ we have that

(1) $\text{dom}(\Delta_1) \subseteq \text{FV}(\vec{t}) \subseteq \text{dom}(\Gamma_1, \Delta_1)$ and $\vec{t} \langle \sigma \rangle \Vdash [[\#(Q \times R)]]]_\tau$ for all $\sigma \in [[\Gamma_1, \Delta_1]]_\tau$.

(2) $\text{dom}(\Delta_2) \cup \{x, y\} \subseteq \text{FV}(\vec{s}) \subseteq \text{dom}(\Gamma_2, \Delta_2) \cup \{x, y\}$ and $\vec{s} \langle \sigma \rangle \Vdash [[S]]_\tau$ for all $\sigma \in [[\Gamma_2, \Delta_2, \{x : \#Q, y : \#R\}]]]_\tau$.

We obtain directly that $\text{dom}(\Delta_1, \Delta_2) \subseteq \text{FV}(\text{let } (x, y) = t \text{ in } \vec{s}) \subseteq \text{dom}(\Gamma_1, \Delta_1, \Gamma_2, \Delta_2)$ and, for any $\sigma \in [[\Gamma_1, \Delta_1, \Gamma_2, \Delta_2]]_\tau$ we have that $\sigma = \sigma_1\sigma_2$ for $\sigma_i \in [[\Gamma_i, \Delta_i]]_\tau$ and thus we have:

$$ \begin{aligned} (\text{let } (x, y) = t \text{ in } \vec{s}) \langle \sigma \rangle &= (\text{let } (x, y) = t \text{ in } \vec{s}) \langle \sigma_1 \rangle \langle \sigma_2 \rangle \\ &= \text{let } (x, y) = t \langle \sigma_1 \rangle \text{ in } \vec{s} \langle \sigma_2 \rangle \\ &\rightsquigarrow^* \text{let } (x, y) = \sum_{i=1}^n \alpha_i \cdot (\vec{v}_i, \vec{w}_i) \text{ in } \vec{s} \langle \sigma_2 \rangle \\ &= \sum_{i=1}^n \alpha_i \cdot \text{let } (x, y) = (\vec{v}_i, \vec{w}_i) \text{ in } \vec{s} \langle \sigma_2 \rangle \\ &\rightsquigarrow^* \sum_{i=1}^n \alpha_i \cdot \vec{s}[\vec{v}_i/x, \vec{w}_i/y] \langle \sigma_2 \rangle \\ &= \sum_{i=1}^n \alpha_i \cdot \vec{s} \langle \vec{v}_i/x, \vec{w}_i/y, \sigma_2 \rangle \rightsquigarrow^* \sum_{i=1}^n \alpha_i \cdot \vec{z}_i \in \text{span}([\vec{s}]_\tau) \end{aligned} $$
To see that this has unit norm, consider:

$$
\begin{align*}
\| \sum_{i=1}^{n} \alpha_i \cdot \vec{z}_i \|^2 &= \langle \sum_{i=1}^{n} \alpha_i \cdot \vec{z}_i | \sum_{i=1}^{n} \alpha_i \cdot \vec{z}_i \rangle = \sum_{i=1}^{n} \sum_{j=1}^{n} \alpha_i \tilde{\alpha}_j \langle \vec{z}_i | \vec{z}_j \rangle \\
&= \sum_{i=1}^{n} \sum_{j=1}^{n} \alpha_i \tilde{\alpha}_j \langle \vec{v}_i | \vec{v}_j \rangle \langle \vec{w}_i | \vec{w}_j \rangle \\
&= \sum_{i=1}^{n} \sum_{j=1}^{n} \alpha_i \tilde{\alpha}_j \langle (\vec{v}_i, \vec{w}_i) | (\vec{v}_j, \vec{w}_j) \rangle \\
&= \langle \sum_{i=1}^{n} \alpha_i (\vec{v}_i, \vec{w}_i) | \sum_{i=1}^{n} \alpha_i (\vec{v}_i, \vec{w}_i) \rangle = \| \sum_{i=1}^{n} \alpha_i \cdot (\vec{v}_i, \vec{w}_i) \|^2 = 1,
\end{align*}
$$

where we have used [Díaz-Caro et al. 2019b, Lemma A.9 and Proposition A.2].

(§i) Assuming that the premise is a valid typing judgment, we have that $FV(\vec{t}) = \text{dom}(\Gamma, \Delta)$.
Using the fact that $[[\mathbf{B}]]_{\tau} \triangleq [[\mathbf{B}]]_{\tau}$, we directly deduce that $\text{dom}(\mathbf{\Phi}\Delta) = \text{dom}(\Delta) \subseteq FV(\vec{t}) \subseteq \text{dom}(\Gamma, \Delta) = \text{dom}(\Gamma, \mathbf{\Phi}\Delta)$. Since $[[\Gamma, \Delta]]_{\tau} = [[\Gamma, \mathbf{\Phi}\Delta]]_{\tau}$ we conclude that the rule is valid.

(\#i) If the premises are valid then we have that $\text{dom}(\Delta) \subseteq FV(\vec{t}_i) \subseteq \text{dom}(\Gamma, \Delta)$, for all $i$. Furthermore, for all $\sigma \in [[\Gamma, \Delta]], \vec{t}_i \langle \sigma \rangle \models [[A]]_{\tau}$. Since $\sum_{i=1}^n |\alpha_i|^2 = 1$, we have that

$$ \left( \sum_{i=1}^{n} \alpha_i \cdot \vec{t}_i \right) \langle \sigma \rangle = \sum_{i=1}^{n} \alpha_i \cdot (\vec{t}_i \langle \sigma \rangle) \models [[\#A]]_{\tau}. $$

(§e) If the premises are valid then:

(1) $\text{dom}(\Delta_1) \subseteq FV(\vec{r}) \subseteq \text{dom}(\Gamma_1, \Delta_1)$ and for all $\sigma \in [[\Gamma_1, \Delta_1]]_\tau$, $\vec{r} \langle \sigma \rangle \models [[B]]_\tau$.

(2) $\text{dom}(\Delta_2) \cup \{x\} \subseteq FV(t) \subseteq \text{dom}(\Gamma_2, \Delta_2) \cup \{x\}$ and for all $\sigma \in [[\Gamma_2, \Delta_2, \{x : B\}]_\tau$, $t \langle \sigma \rangle \models [[A]]_\tau$.

We immediately obtain that $\text{dom}(\Delta_1, \Delta_2) \subseteq FV(t[\vec{r}/x]) \subseteq \text{dom}(\Gamma_1, \Delta_1, \Gamma_2, \Delta_2)$.

$$ t[\vec{r}/x] \langle \sigma \rangle = t[\vec{r}/x] \langle \sigma_1, \sigma_2 \rangle = t[\vec{r} \langle \sigma_1 \rangle / x] \langle \sigma_2 \rangle \models [[A]]_{\tau}, $$

since $\vec{r} \langle \sigma_1 \rangle \models B$ (from 1 and the fact that $\sigma_1 \in [[\Gamma_1, \Delta_1]]_\tau$), and so we have that $\langle \{\vec{r} \langle \sigma_1 \rangle / x \}, \sigma_2 \rangle \in [[\Gamma_2, \Delta_2, \{x : B\}]_\tau]$.

(\forall i) Suppose that $\Gamma; \Delta \vdash \vec{t} : A$ is valid and that $X \notin FV(\Gamma, \Delta)$. Then

$$ \text{dom}(\Delta) \subseteq FV(\vec{t}) \subseteq \text{dom}(\Gamma, \Delta) \text{ and } \vec{t} \langle \sigma \rangle \models [[A]]_{\tau} \text{ for all } \sigma \in [[\Gamma, \Delta]]_{\tau} $$

Let $\tau' = \tau \setminus \{X\}$. By definition, we have

$$ [[\forall X.A]]_{\tau'} = \bigcap_{B \in S_1} [[A]]_{\tau' \cup \{X \mapsto [B]_0\}} $$

Since $X \notin FV(\Gamma, \Delta)$, for all $\sigma$ such that $\sigma \in [[\Gamma, \Delta]]_\tau$, we also have $\sigma \in [[\Gamma, \Delta]]_{\tau' \cup \{X \mapsto R\}}$ for any $R \subseteq S_1$.

Therefore, $\vec{t} \langle \sigma \rangle \models [[A]]_\tau$ implies $\vec{t} \langle \sigma \rangle \models [[A]]_{\tau' \cup \{X \mapsto R\}}$ for all $R \in S_1$, thus, $\vec{t} \langle \sigma \rangle \models [[\forall X.A]]_{\tau'}$.

(\forall e) Suppose that $\Gamma; \Delta \vdash \vec{t} : \forall X.A$. Then

$$ \text{dom}(\Delta) \subseteq FV(\vec{t}) \subseteq \text{dom}(\Gamma, \Delta) \text{ and } \vec{t} \langle \sigma \rangle \models [[\forall X.A]]_{\tau} \text{ for all } \sigma \in [[\Gamma, \Delta]]_{\tau} $$

Thus, by definition, since $[[B]]_\tau \subseteq S_1$, we have $\vec{t} \langle \sigma \rangle \models [[A]]_{\tau \cup \{X \mapsto [B]_\tau\}}$.

We conclude by Lemma 5.2.

□
LEMMA 5.5. For any $\vec{t} \in \text{PUNQ}$ and any $k \ge n$ for $k, n \in \mathbb{N} - \{0\}$,

$$ \vec{t} \in [[\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)]]_0 \iff \begin{cases} \forall i = 0, \dots, 2^n - 1, \exists \vec{v}_i \in [[\#(\mathbb{B}^k)]_0 \text{ such that } \vec{t} |i\rangle \rightsquigarrow \vec{v}_i, \text{ and} \\ \vec{v}_i \perp_{\#(\mathbb{B}^k)} \vec{v}_j, \forall i \neq j. \end{cases} $$

PROOF. (The condition is necessary.) For some $\lambda x. \vec{t} \in [[\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)]]_0$, let $\vec{v}_i \in [[\#(\mathbb{B}^k)]]_0$ be the values that satisfy $\vec{t}[|i\rangle/x] \rightsquigarrow \vec{v}_i$, $\forall i = 0, \dots, 2^n - 1$. Then, for any $\alpha_i \in \overline{\mathbb{Q}}$ such that $\sum_i |\alpha_i|^2 = 1$ we have, by linearity,

$$ \vec{t}\left[\sum_i \alpha_i \cdot |i\rangle/x\right] = \sum_i \alpha_i \cdot \vec{t}[|i\rangle/x] \rightsquigarrow \sum_i \alpha_i \cdot \vec{v}_i. $$

Since $\sum_i \alpha_i \cdot |i\rangle \in [[\#(\mathbb{B}^n)]_0$, we have that $\sum_i \alpha_i \cdot \vec{v}_i \in [[\#(\mathbb{B}^k)]_0$, and therefore $\| \sum_i \alpha_i \cdot \vec{v}_i \| = 1$. From this, we can derive

$$ \begin{aligned} 1 &= \left\| \sum_i \alpha_i \cdot \vec{v}_i \right\|^2 \\ &= \left\langle \sum_i \alpha_i \cdot \vec{v}_i \middle| \sum_i \alpha_i \cdot \vec{v}_i \right\rangle \\ &= \sum_i |\alpha_i|^2 \langle \vec{v}_i \mid \vec{v}_i \rangle + \sum_{i<j} (\alpha_i \overline{\alpha_j} \langle \vec{v}_i \mid \vec{v}_j \rangle + \alpha_j \overline{\alpha_i} \langle \vec{v}_j \mid \vec{v}_i \rangle) \\ &= \sum_i |\alpha_i|^2 + \sum_{i<j} (\alpha_i \overline{\alpha_j} \langle \vec{v}_i \mid \vec{v}_j \rangle + \overline{\alpha_i \alpha_j} \langle \vec{v}_i \mid \vec{v}_j \rangle) \\ &= 1 + \sum_{i<j} 2\text{Re}(\alpha_i \overline{\alpha_j} \langle \vec{v}_i \mid \vec{v}_j \rangle). \end{aligned} $$

Picking $\alpha_0 = \alpha_1 = \frac{1}{\sqrt{2}}$, and $\alpha_i = 0$, for $i \neq 0, 1$ we deduce $\text{Re}(\langle \vec{v}_0 \mid \vec{v}_1 \rangle) = 0$ and from $\alpha_0 = \frac{1}{\sqrt{2}}$, $\alpha_1 = \frac{i}{\sqrt{2}}$ and $\alpha_i = 0, \forall i \neq 0, 1$ we obtain $\text{Im}(\langle \vec{v}_0 \mid \vec{v}_1 \rangle) = 0$ and therefore $\langle \vec{v}_0 \mid \vec{v}_1 \rangle = 0$. The same reasoning can be applied to all other pairs $\alpha_i, \alpha_j$ such that $i \neq j$ and therefore $\langle \vec{v}_i \mid \vec{v}_j \rangle = 0$.

(The condition is sufficient.) Suppose there exist $\vec{v}_i \in [[\#(\mathbb{B}^k)]_0$, $i = 0, \dots, 2^n - 1$, for which $\langle \vec{v}_i \mid \vec{v}_j \rangle = 0, \forall i \neq j$ and such that $\vec{t}[|i\rangle/x] \rightsquigarrow \vec{v}_i$. In particular, we have that, for all $i, \vec{v}_i \in \text{span}(\{|i\rangle| i = 0, \dots, 2^n - 1\})$ and $\|\vec{v}_i\| = 1$. For any given $\vec{v} \in [[\#(\mathbb{B}^n)]_0$, $\vec{v} = \sum_i \alpha_i \cdot |i\rangle$ such that $\sum_i |\alpha_i|^2 = 1$. Then,

$$ \vec{t}[\vec{v}/x] = \sum_i \alpha_i \cdot \vec{t}[|i\rangle/x] \rightsquigarrow \sum_i \alpha_i \cdot \vec{v}_i \in [[\#(\mathbb{B}^k)]_0, $$

since $\sum_i \alpha_i \cdot \vec{v}_i \in \text{span}(\{|i\rangle| i = 0, \dots, 2^n - 1\})$ and

$$ \begin{aligned} \left\| \sum_i \alpha_i \cdot \vec{v}_i \right\|^2 &= \left\langle \sum_i \alpha_i \cdot \vec{v}_i \middle| \sum_i \alpha_i \cdot \vec{v}_i \right\rangle \\ &= \sum_i |\alpha_i|^2 \langle \vec{v}_i \mid \vec{v}_i \rangle + \sum_{i<j} (\alpha_i \overline{\alpha_j} \langle \vec{v}_i \mid \vec{v}_j \rangle + \alpha_j \overline{\alpha_i} \langle \vec{v}_j \mid \vec{v}_i \rangle) \\ &= \sum_i |\alpha_i|^2 \|\vec{v}_i\|^2 + \sum_{i<j} (0 + 0) \\ &= \sum_i |\alpha_i|^2 = 1. \end{aligned} $$

Therefore, for all $\vec{v} \in [[\#(\mathbb{B}^n)]_0$, $\vec{t}[\vec{v}/x] \rightsquigarrow \#(\mathbb{B}^n)$, and finally $\lambda x. \vec{t} \in [[\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)]]_0$. $\square$

THEOREM 5.7 (COMPLETENESS). For any isometry $\mathcal{I} : \overline{\mathbb{Q}}^{2n} \to \overline{\mathbb{Q}}^{2k}$, with $k \ge n \ge 1$, there exists a closed superposition $\lambda x. \vec{t} \in S_c$ of type $\#(\mathbb{B}^n) \to \#(\mathbb{B}^k)$ that represents $\mathcal{I}$.
PROOF. We provide a constructive proof. If $\mathcal{I} : \overline{\mathbb{Q}}^{2n} \to \overline{\mathbb{Q}}^{2k}$ represents an isometry, then the columns in its matrix representation have unit norm and are mutually orthogonal. This means that $\forall i, j = 0, \dots, 2^n - 1$, $\mathcal{I}(\langle |i\rangle)\dagger \cdot \mathcal{I}(\langle |j\rangle) = 0$ if $i \neq j$. Furthermore, for any $i = 0, \dots, 2^n - 1$, $\|\mathcal{I}(\langle |i\rangle)\| = 1$ and so $\mathcal{I}(\langle |i\rangle) \triangleq (\alpha_0^i \dots \alpha_{2k-1}^i)$ can be encoded by a closed PUNQ term $\vec{v}_i = \sum_{j=0}^{2k-1} \alpha_j^i \cdot |j\rangle \in [[\#(\mathbb{B}^k)]]$. We now perform the encoding. Let $x, x_m$ and $x_{[1..m]}$ all represent different variables, for $1 \le m \le n$. We can encode the operator $\mathcal{I}$ using nested if statements, as follows:

$\vec{t} \triangleq \text{let } (x_{[1..n-1]}, x_n) = x$

in let $(x_{[1..n-2]}, x_{n-1}) = x_{[1..n-1]}$

in ...

in let $(x_1, x_2) = x_{[1..2]}$ in if $x_1$ then ... if $x_{n-1}$ then (if $x_n$ then $\vec{v}_0$ else $\vec{v}_1$)

else (if $x_n$ then $\vec{v}_2$ else $\vec{v}_3$)

...

else ... if $x_{n-1}$ then (if $x_n$ then $\vec{v}_{2n-4}$ else $\vec{v}_{2n-3}$)

else (if $x_n$ then $\vec{v}_{2n-2}$ else $\vec{v}_{2n-1}$).

Then, the term $\lambda x.\vec{t} \in S_c$ has type $\#(\mathbb{B}^n) \dashv \#(\mathbb{B}^k)$, and $\forall i = 0, \dots, 2^n - 1$, $(\lambda x.\vec{t}) |i\rangle \rightsquigarrow^* \vec{v}_i$. $\square$

THEOREM 5.8 (NON-SEPARABILITY). For any $n, k \in \mathbb{N} - \{0\}$, the type $\#(\mathbb{B}^{n+k}) \dashv (\#(\mathbb{B}^n) \times \#(\mathbb{B}^k))$ is uninhabited.

PROOF. Consider an argument by contradiction, starting with a candidate closed term $\lambda x.\vec{t} \in [[\#(\mathbb{B}^{n+k})] \dashv (\#(\mathbb{B}^n) \times \#(\mathbb{B}^k))]_0$. Define the values $(\vec{u}_i, \vec{v}_i) \in [[\#(\mathbb{B}^n) \times \#(\mathbb{B}^k)]_0$ satisfying $(\lambda x.\vec{t}) |i\rangle \rightsquigarrow^* (\vec{u}_i, \vec{v}_i)$. Notice that $\lambda x.\vec{t}$ can be subtyped as $\#(\mathbb{B}^{n+k}) \dashv \#(\mathbb{B}^{n+k})$ and therefore by Theorem 5.6 must satisfy unitarity. We conclude, therefore, that since we have $2^{n+k}$ values of $(\vec{u}_i, \vec{v}_i)$ such that they are all orthogonal and of unit norm, then they must form an orthonormal basis of $[[\#(\mathbb{B}^{n+k})]]_0$. In particular, they suffice to represent any value $\vec{s} \triangleq \sum_i \alpha_i \cdot (\vec{u}_i, \vec{v}_i)$ with $\sum_i |\alpha_i|^2 = 1$, and in particular we may choose $\vec{s}$ to be an entangled state and therefore $\vec{s} \notin [[\#(\mathbb{B}^n) \times \#(\mathbb{B}^k)]_0$. However, we have that $\sum_i \alpha_i \cdot |i\rangle \in [[\#(\mathbb{B}^{n+k})]]_0$ and that $\lambda x.\vec{t} (\sum_i \alpha_i \cdot |i\rangle) \rightsquigarrow^* \vec{s}$. $\square$

## A.3 Proofs of Section 6

Shortand notations. For two sets $S, T$, we have that

* $S \mathcal{T} \triangleq \{s \mid t \mid s \in S, t \in \mathcal{T}\}$

* $\lambda z.S \triangleq \{\lambda z.s \mid s \in S\}$

* $S[T/z] \triangleq \{s[t/z] \mid s \in S, t \in \mathcal{T}\}$

LEMMA A.2. Let $\vec{t} \in S$ and $v \in BV$, then $\langle [\vec{t}[v/x]] \mid (\vec{t}) \rangle = \langle (\vec{t}) \mid (\langle v \rangle)/x \rangle$.

PROOF. By induction on the structure of $\vec{t}$.

* $(\vec{t} = x) \quad (\langle \vec{t}[v/x] \rangle = (\langle v \rangle) = x[(\langle v \rangle)/x] = (\langle \vec{t} \rangle)[(\langle v \rangle)/x]$.

* $(\vec{t} = y) \quad (\langle \vec{t}[v/x] \rangle = (\langle y \rangle) = y = y[(\langle v \rangle)/x] = (\langle y \rangle)[(\langle v \rangle)/x] = (\langle \vec{t} \rangle)[(\langle v \rangle)/x]$.

* $(\vec{t} = |0\rangle) \quad (\langle |0\rangle[v/x] \rangle = (\langle |0\rangle) = \lambda z_1.\lambda z_2.z_1 = (\lambda z_1.\lambda z_2.z_1)[(\langle v \rangle)/x] = (\langle |0\rangle)[(\langle v \rangle)/x] = (\langle \vec{t} \rangle)[(\langle v \rangle)/x]$.

* $(\vec{t} = |1\rangle)$ Similar to case $(|0\rangle)$.
• $(\vec{t} = \text{if } r \text{ then } \vec{s}_1 \text{ else } \vec{s}_2)$

$$ \begin{aligned} (\|\vec{t}[v/x]\|) &= (\|\text{if } r[v/x] \text{ then } \vec{s}_1[v/x] \text{ else } \vec{s}_2[v/x]\|) \\ &= ((\|r[v/x]\|) \lambda x_{1...k} \cdot (\|t_1[v/x]\|) \lambda x_{1...k} \cdot (\|t_2[v/x]\|)) x_1 \dots x_k \\ &=^{\text{IH}} ((\|r\|)[(\|v\|)/x] \lambda x_{1...k} \cdot (\|t_1\|)[(\|v\|)/x] \lambda x_{1...k} \cdot (\|t_2\|)[(\|v\|)/x]) x_1 \dots x_k \\ &= ((\|r\|) \lambda x_{1...k} \cdot (\|t_1\|) \lambda x_{1...k} \cdot (\|t_2\|))[\|v\|/x] x_1 \dots x_k \\ &= (((\|r\|) \lambda x_{1...k} \cdot (\|t_1\|) \lambda x_{1...k} \cdot (\|t_2\|)) x_1 \dots x_k)[\|v\|/x] = (\|\vec{t}\|)[\|v\|/x] \end{aligned} $$

• $(\vec{t} = \lambda z.\vec{s})$

$$ \begin{aligned} (\|\vec{t}[v/x]\|) &= (\|\lambda z.\vec{s}[v/x]\|) \\ &= \lambda z.\|\vec{s}[v/x]\| \\ &=^{\text{IH}} \lambda z.\|\vec{s}\|[(\|v\|)/x] \\ &= (\|\lambda z.\vec{s}\|)[(\|v\|)/x] = (\|\vec{t}\|)[(\|v\|)/x]. \end{aligned} $$

• $(\vec{t} = s r)$

$$ \begin{aligned} (\|\vec{t}[v/x]\|) &= (\|\text{(}s r\text{)}[v/x]\|) \\ &= (\|s[v/x] r[v/x]\|) \\ &= (\|s[v/x]\|) (\|r[v/x]\|) \\ &=^{\text{IH}} (\|s\|)[(\|v\|)/x] (\|r\|)[(\|v\|)/x] \\ &= ((\|s\|) (\|r\|))[\|v\|/x] = (\|s r\|)[\|v\|/x] = (\|\vec{t}\|)[\|v\|/x]. \end{aligned} $$

• $(\vec{t} = (s, r))$

$$ \begin{aligned} (\|\vec{t}[v/x]\|) &= (\|\text{(}s, r\text{)}[v/x]\|) \\ &= (\|\text{(}s[v/x], r[v/x]\text{)}\|) \\ &= \lambda z.\text{(}z \|\text{(}s[v/x]\|) (\|r[v/x]\|) \text{)} \\ &=^{\text{IH}} \lambda z.\text{(}z \|\text{(}\|s\|)[(\|v\|)/x] (\|r\|)[(\|v\|)/x] \text{)} \\ &= (\lambda z.\text{(}z \|\text{(}\|s\|) (\|r\|) \text{)})[(\|v\|)/x] = (\|\text{(}s, r\text{)}\|)[(\|v\|)/x] = (\|\vec{t}\|)[(\|v\|)/x]. \end{aligned} $$

• $(\vec{t} = \text{let } (z_1, z_2) = s \text{ in } \vec{r})$

$$ \begin{aligned} (\|\vec{t}[v/x]\|) &= (\|\text{let } (z_1, z_2) = s[v/x] \text{ in } \vec{r}[v/x]\|) \\ &= (\|s[v/x]\|)(\lambda z_1 \cdot \lambda z_2 \cdot (\|\vec{r}[v/x]\|)) \\ &=^{\text{IH}} (\|s\|)[(\|v\|)/x](\lambda z_1 \cdot \lambda z_2 \cdot (\|\vec{r}\|)[(\|v\|)/x]) \\ &= ((\|s\|)(\lambda z_1 \cdot \lambda z_2 \cdot (\|\vec{r}\|)))[(\|v\|)/x] \\ &= (\|\text{let } (z_1, z_2) = s \text{ in } \vec{r}\|)[(\|v\|)/x] = (\|\vec{t}\|)[(\|v\|)/x]. \end{aligned} $$

• $(\vec{t} = \vec{0})$. Similar to case of $|0\rangle$.

• $(\vec{t} = \alpha \cdot \vec{s})$ $(\|\vec{t}[v/x]\|) = (\|\alpha \cdot \vec{s}[v/x]\|) = \text{if } \alpha = 0$

• $(\vec{t} = \vec{s} + \vec{r})$

LEMMA 6.6. If $\vec{t} \equiv \vec{r}$, then $\|\vec{t}\| \approx \|\vec{r}\|$.

PROOF. By inspection of the equivalence relation.

• $\vec{t}_1 + \vec{t}_2 \equiv \vec{t}_2 + \vec{t}_1$, where we have $(\|\vec{t}_1 + \vec{t}_2\|) = (\|\vec{t}_1\|) \cup (\|\vec{t}_2\|) = (\|\vec{t}_2\|) \cup (\|\vec{t}_1\|) = (\|\vec{t}_2 + \vec{t}_1\|)$.

□
• $\vec{0} + \vec{t}_1 \equiv \vec{t}_1$, in which case $\langle\vec{0} + \vec{t}_1\rangle = \{*\} \cup \langle\vec{t}_1\rangle$, therefore $\langle\vec{0} + \vec{t}_1\rangle \cong \langle\vec{t}_1\rangle$.

For all other cases, we easily find that $\langle\vec{t}\rangle = \langle\vec{r}\rangle$ and the conclusion follows. $\square$

LEMMA 6.7. $\Gamma; \Delta \vdash \vec{t} : A$ implies $\Gamma^*; \Delta^* \vdash_{\text{DLAL}} \langle\vec{t}\rangle : A^*$.

PROOF. We prove this statement by induction on the derivation tree of $\Gamma; \Delta \vdash \vec{t} : A$.

(W) By the induction hypothesis, we have that $\Gamma^*; \Delta^* \vdash_{\text{DLAL}} \langle\vec{t}\rangle : A^*$. Using rule (Weak) in DLAL we obtain $\Gamma^*, \Gamma'^*; \Delta^* \vdash_{\text{DLAL}} \langle\vec{t}\rangle : A^*$.

(C) By the IH we have $\Gamma^*, x : B^*, y : B^*; \Delta^* \vdash_{\text{DLAL}} \langle\vec{t}\rangle : A^*$. Applying rule (Cntr) in DLAL we obtain $\Gamma^*, x : B^*; \Delta^* \vdash_{\text{DLAL}} \langle\vec{t}\rangle[x/y] : A^*$ which by Lemma A.2

(≡) We can check that this is the case for all terms $\vec{t}_1, \vec{t}_2$ such that $\vec{t}_1 \equiv \vec{t}_2$. It can be shown by inspection that, for almost all cases in the equivalence relation $\equiv$, the translation is preserved, i.e. that if $\vec{t}_1 \equiv \vec{t}_2$, then $\langle\vec{t}_1\rangle = \langle\vec{t}_2\rangle$. However, this is not the case in two instances:

• $\vec{t}_1 = \vec{0} + \vec{t} \equiv \vec{t} = \vec{t}_2$. In this case, $\langle\vec{t}_1\rangle = \langle\vec{t}_2\rangle \cup \{*\}$ and therefore $\langle\vec{t}_2\rangle \subseteq \langle\vec{t}_1\rangle$ from which the conclusion follows.

• $\vec{t}_1 = 0 \cdot \vec{t} \equiv \vec{0} = \vec{t}_2$. Here, since $\langle\vec{t}_2\rangle = \{*\}$ which admits any type, the conclusion follows.

(≤) By Lemma 6.4, for all subtyping relations $A \le B$ we have that $A^* = B^*$ and therefore the result follows.

(Ax) We have that $\langle\lvert x \rvert\rangle = \{x\}$, and by rule (Id) in DLAL, we may obtain $x : A^* \vdash x : A^*$ for any $A \in \mathbb{T}$.

(0) We have that $\langle\lvert 0 \rvert\rangle = \{\lambda x.\lambda y. x\}$ and $\mathbb{B}^* = \forall X.(X \to X \to X)$, and by DLAL rules (Id), (Weak), and two uses of $(\to i)$, and finally $(\forall i)$ we obtain the desired typing derivation. Indeed, this is the standard encoding in DLAL for booleans.

(1) Analogous to (0).

(if) We have that $\langle\text{if } t \text{ then } t_1 \text{ else } t_2\rangle = (t \lambda x_{1...k} \langle t_1\rangle \lambda x_{1...k} \langle t_2\rangle) x'_1 \dots x'_k$. By the IH we have that $\Gamma'^*; \Delta'^* \vdash \langle t_1\rangle \cup \langle t_2\rangle : A^*$, and $\Gamma^*; \Delta^* \vdash t : \forall X.(X \to X \to X)$. Let $\Delta'^* = \{x_i : A_i^*\}_{i=1...k}$,

$$ \frac{\Gamma'^*; \Delta'^* \vdash \langle t_1 \rangle \cup \langle t_2 \rangle : A^*}{\Gamma'^*; \vdash \langle \lambda x_{1...k} t_1 \rangle \cup \langle \lambda x_{1...k} t_2 \rangle : A_1^* \to \dots \to A_k^* \to A^*} \quad (\neg e) \text{ times} $$

Without loss of generality, we may consider that the variables in $\Gamma'^*$ have different names in the typing of $t_1$ and $t_2$. Let us use $\overline{\Gamma'^*}$ to denote the nonlinear context of $\vec{t}_2$, where we have renamed the nonlinear variables.

Therefore, we may derive the following judgement in DLAL. Let $B \stackrel{\sim}{=} A_1^* \to \dots \to A_k^* \to A^*$.

$$ \frac{\frac{\Gamma^*; \Delta^* \vdash t : \forall X.(X \to X \to X)}{\Gamma^*; \Delta^* \vdash t : B \to B \to B} \quad (\forall e) \qquad \frac{\Gamma^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} t_1 \rangle : B \right)}{\Gamma^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} t_1 \rangle : B \to B \right)} \quad (\neg e) \qquad \overline{\Gamma'^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} \vec{t}_1 \rangle : B \right)} \quad (\neg e)}{\Gamma^*; \Gamma'^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} t_1 \rangle : B \right) \left( \langle \lambda x_{1...k} \vec{t}_2 \rangle : B \right)} \quad (\text{Cntr}) \qquad \frac{\overline{\Gamma^*; \Gamma'^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} t_1 \rangle : B \right) \left( \langle \lambda x_{1...k} \vec{t}_2 \rangle : B \right)}{\Gamma^*; \Gamma'^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} t_1 \rangle : A_1^* \to \dots \to A_k^* \to A^* \right)} \quad (\text{Cntr})}{x_i : A_i^* \vdash x_i : A_i^*} \quad (\text{Id})} \\ \frac{\Gamma^*; \Gamma'^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} t_1 \rangle : B \right) \left( \langle \lambda x_{1...k} t_2 \rangle : A_1^* \to \dots \to A_k^* \to A^* \right)}{\Gamma^*; \Gamma'^*; \Delta^* \vdash t \left( \langle \lambda x_{1...k} t_1 \rangle : B \right) \left( \langle \lambda x_{1...k} t_2 \rangle : B \right)} \quad (\neg e) $$

(if#) Since $(\#A)^* = A^*$, the proof is precisely the same as done in the case of (if).

($\to_i$) By the IH we have that $\Gamma^*; \Delta^*, x : A^* \vdash \langle\vec{t}\rangle : B^*$. By rule ($\to i$) in DLAL we obtain $\Gamma^*; \Delta^* \vdash \lambda x.\langle\vec{t}\rangle : A^* \to B^*$. Since $\langle\lambda x.\vec{t}\rangle = \lambda x.\langle\vec{t}\rangle$ and $(A \to B)^* = A^* \to B^*$ this is precisely our desired conclusion.
(-$\infty_e$) By the IH we have $\Gamma^*; \Delta^* \vdash (\|t\|) : A^* \to B^*$ and $\Gamma'^*; \Delta'^* \vdash (\|s\|) : A^*$. Applying the DLAL rule ($\to e$) we obtain $\Gamma^*, \Gamma'^*; \Delta^*, \Delta'^* \vdash (\|t\|) (\|s\|) : B^*$. Since $(\|t\|) = (\|t\|) (\|s\|)$ the proof is concluded.

(=$\Rightarrow_i$) By the IH we have $\Gamma^*, x : A^*; \Delta^* \vdash (\|\vec{t}\|) : B^*$. By rule ($\Rightarrow i$) we obtain $\Gamma^*; \Delta^* \vdash \lambda x.(\|\vec{t}\|) : A^* \Rightarrow B^*$. By Lemma 6.3 we have that $(! (A))^* = A^*$.

(=$\Rightarrow_e$) Similar to ($\to_e$). We may simply use the rule ($\Rightarrow e$) in DLAL to obtain our desired conclusion.

($\times_i$) By the IH we have that $\Gamma^*; \Delta^* \vdash (\|t\|) : A^*$ and $\Gamma'^*; \Delta'^* \vdash (\|s\|) : B^*$. We may obtain the following derivation in DLAL (i.e. the pair encoding).

$$ \frac{\frac{\frac{x : A^* \to B^* \to X \vdash x : A^* \to B^* \to X}{\Gamma^*; \Delta^* \vdash (\|t\|) : A^*} \quad (-\to e)}{\frac{\frac{\Gamma^*; \Delta^*, x : A^* \to B^* \to X \vdash x (\|t\|) : B^* \to X}{\Gamma^*; \Delta'^* \vdash (\|s\|) : B^*} \quad (-\to e)}{\frac{\frac{\Gamma^*, \Gamma'^*; \Delta^*, \Delta'^* : x : A^* \to B^* \to X \vdash x (\|t\|) (\|s\|) : X}{\Gamma^*, \Gamma'^*; \Delta^*, \Delta'^* \vdash \lambda x.(x (\|t\|) (\|s\|)) : (A^* \to B^* \to X) \to X} \quad (-\to i)}{\frac{\Gamma^*, \Gamma'^*; \Delta^*, \Delta'^* \vdash \lambda x.(x (\|t\|) (\|s\|)) : \forall X.((A^* \to B^* \to X) \to X)}{(\forall i) \quad (-\to e)} } $$

This is precisely our desired result.

($\times_e$) We have $\Gamma^*; \Delta^* \vdash (\|t\|) : \forall X.((A^* \to B^* \to X) \to X)$ and $\Gamma'^*; \Delta'^* : x : A^*, y : B^* \vdash (\|\vec{s}\|) : C^*$ by the IH. In DLAL we are able to derive

$$ \frac{\frac{\frac{\Gamma^*; \Delta^* \vdash (\|t\|) : \forall X.((A^* \to B^* \to X) \to X)}{\Gamma^*; \Delta^* \vdash (\|t\|) : (A^* \to B^* \to C^*) \to C^*} \quad (\forall e)}{\frac{\frac{\Gamma'^*; \Delta'^* : x : A^*, y : B^* \vdash (\|\vec{s}\|) : C^*}{\Gamma'^*; \Delta'^* : x : A^* \vdash \lambda y.(\|\vec{s}\|) : B^* \to C^*} \quad (-\to i)}{\frac{\Gamma'^*; \Delta'^* \vdash \lambda x.\lambda y.(\|\vec{s}\|) : A^* \to B^* \to C^*}{{(\forall e)}}} \quad (-\to i) } $$

which concludes this case.

($\times_{e\#}$) Same proof as in ($\times_e$).

($\#_i$) Trivial.

($\#_i$) ($\#_e$) ($\forall_i$) ($\forall_e$) These rules have a direct counterpart in DLAL so their proof is trivial.

□

LEMMA 6.8. For any $A \in \mathbb{T}$, there exists a polynomial $P_A$ such that, for any $\vec{t}$ where $\vdash \vec{t} : A$, the following holds $|\|\vec{t}\|| = O(P_A(|\vec{t}|))$.

PROOF. By induction on the structure of $\vec{t}$.

* If $\vec{t} = |0\rangle$, then $\|\vec{t}\| = \{\lambda x.\lambda y.x\}$ and therefore $|\vec{t}| = 1$ and $|\|\vec{t}\|| = 5$. Similar case for $t = |1\rangle$.

* If $\vec{t} = x$, then $|t| = 1$ and $\|\vec{t}\| = \{x\}$ and therefore $|\|\vec{t}\|| = 1$.

* If $\vec{t} = \lambda x.\vec{s}$, then $|\vec{t}| = 1 + |\vec{s}|$ and $|\|\vec{t}\|| = |\lambda x_{[1...k]}.(\|\vec{s}\|_{[x:1...k]})| = O(2|\vec{s}|) = O(|\vec{t}|)$.

* If $\vec{t} = t_1 t_2$, we have $|\vec{t}| = |t_1| + |t_2|$ and

$$ \begin{aligned} |(\|t_1 t_2\|)| &\triangleq |(\dots ((\|t_1\|) (\|t_2\|)) \dots (\|t_2\|))| \\ &= |(\|t_1\|)| + O(|t_1|) \cdot |(\|t_2\|)| \\ &= \text{IH} \ O(|t_1|^{d_1}) + O(|t_1|) \cdot O(|t_2|^{d_2}) \\ &= O(|\vec{t}|^{\max(d_1, d_2+1)}) . \end{aligned} $$

Notice that, if $t_1$ does not duplicate $t_2$, then the bounding degree is instead $\max(d_1, d_2)$.
* If $\vec{t} = \text{if } s \text{ then } p_1 \text{ else } p_2$, we have $|\vec{t}| = 1 + |s| + |p_1| + |p_2|$, and

$$ 
\begin{aligned}
|\langle\!\langle \vec{t} \rangle\!\rangle| &\triangleq |\langle\!\langle s \rangle\!\rangle \lambda x_{[1\dots k]} \cdot \langle\!\langle p_1 \rangle\!\rangle \lambda x_{[1\dots k]} \cdot \langle\!\langle p_2 \rangle\!\rangle) x'_1 \dots x'_k| \\
&= |\langle\!\langle s \rangle\!\rangle| + O(|p_1|) + O(|\langle\!\langle p_1 \rangle\!\rangle|) + O(|p_2|) + O(|\langle\!\langle p_2 \rangle\!\rangle|) \\
&= \text{IH} \ O(|s|^{d_1}) + O(|p_1|^{d_2}) + O(|p_2|^{d_3}) + O(|p_1|) + O(|p_2|) \\
&= O(|\vec{t}|^{\max(d_1, d_2, d_3)}).
\end{aligned}
$$

* If $\vec{t} = (t_1, t_2)$, then $|\vec{t}| = 1 + |t_1| + |t_2|$ and

$$ 
\begin{aligned}
|\langle\!\langle \vec{t} \rangle\!\rangle| &\triangleq |\lambda x.(x \langle\!\langle t_1 \rangle\!\rangle \langle\!\langle t_2 \rangle\!\rangle)| = 3 + |\langle\!\langle t_1 \rangle\!\rangle| + |\langle\!\langle t_2 \rangle\!\rangle| = \\
&\qquad \text{IH} \ O(|t_1|^{d_1}) + O(|t_2|^{d_2}) \\
&= O(|\vec{t}|^{\max(d_1, d_2)}).
\end{aligned}
$$

* If $\vec{t} = \text{let } (x, y) = t_1 \text{ in } t_2$ then $|\vec{t}| = 1 + \max(|t_1|, |t_2|)$ and

$$ 
\begin{aligned}
|\langle\!\langle \vec{t} \rangle\!\rangle| &\triangleq |\langle\!\langle t_1 \rangle\!\rangle (\lambda x.\lambda y.(\langle\!\langle t_2 \rangle\!\rangle))| = 2 + |\langle\!\langle t_1 \rangle\!\rangle| + |\langle\!\langle t_2 \rangle\!\rangle| \\
&= \text{IH} \ 2 + O(|t_1|^{d_1}) + O(|t_2|^{d_2}) \\
&= O(|\vec{t}|^{\max(d_1, d_2)}).
\end{aligned}
$$

* If $\vec{t} = \vec{t}_1 + \vec{t}_2$, then $|\vec{t}| = \max(|\vec{t}_1|, |\vec{t}_2|)$, and

$$ 
\begin{aligned}
|\langle\!\langle \vec{t} \rangle\!\rangle| &= |\langle\!\langle \vec{t}_1 \rangle\!\rangle \cup \langle\!\langle \vec{t}_2 \rangle\!\rangle| = \max(\langle\!\langle \vec{t}_1 \rangle\!\rangle, \langle\!\langle \vec{t}_2 \rangle\!\rangle) = \\
&\qquad \text{IH} \ O(\max(|\vec{t}_1|^{d_1}, |\vec{t}_2|^{d_2})) \\
&= O(|\vec{t}|^{\max(d_1, d_2)}).
\end{aligned}
$$

* If $\vec{t} = \vec{t}_1 + \vec{t}_2$, then $|\vec{t}| = \max(|\vec{t}_1|, |\vec{t}_2|)$, and

$$ 
\begin{aligned}
|\langle\!\langle \vec{t} \rangle\!\rangle| &= |\langle\!\langle \vec{t}_1 \rangle\!\rangle \cup \langle\!\langle \vec{t}_2 \rangle\!\rangle| = \max(\langle\!\langle \vec{t}_1 \rangle\!\rangle, \langle\!\langle \vec{t}_2 \rangle\!\rangle) = \\
&\qquad \text{IH} \ O(\max(|\vec{t}_1|^{d_1}, O(|\vec{t}_2|^{d_2})) \\
&= O(|\vec{t}|^{\max(d_1, d_2)}).
\end{aligned}
$$

* If $\vec{t} = \alpha \cdot \vec{s}$, then $|\vec{t}| = |\vec{s}|$, and $|\langle\!\langle \vec{t} \rangle\!\rangle| = |\langle\!\langle \vec{s} \rangle\!\rangle| = \text{IH} \ O(|\vec{s}|^d) = O(|\vec{t}|^d)$.

The degree of the polynomial bounding the size of $|\langle\!\langle \vec{t} \rangle\!\rangle$ is only increased in translating duplications (see case $\vec{t} = t_1 t_2$), so it will only depend on the number of such duplications present in the term, which is bounded by the type of the term. □

**LEMMA 6.9.** For any $\vec{v} \in V_c$, we have that $|\langle\!\langle \vec{v} \rangle\!\rangle|$ does not reduce.

**PROOF.** By induction on the structure of $\vec{v}$.

* $\vec{v} = |0\rangle$. Then $|\langle\!\langle \vec{v} \rangle\!\rangle| = \{\lambda x.\lambda y.x\}$, which does not reduce. Same for $\vec{v} = |1\rangle$.

* $\vec{v} = \lambda x.\vec{t}$. Then $|\langle\!\langle \vec{v} \rangle\!\rangle| = \lambda x.(\langle\!\langle \vec{t} \rangle\!\rangle)$ which will not reduce in DLAL in call by value.

* $\vec{v} = (v_1, v_2)$, in which case $|\langle\!\langle \vec{v} \rangle\!\rangle| = \lambda x.(x \langle\!\langle v_1 \rangle\!\rangle \langle\!\langle v_2 \rangle\!\rangle)$. By IH, we consider that no element in $\langle\!\langle v_1 \rangle\!\rangle \cup \langle\!\langle v_2 \rangle\!\rangle$ reduces in DLAL, therefore $|\langle\!\langle \vec{v} \rangle\!\rangle|$ will not reduce.

* $\vec{v} = \vec{0}$, where we have $|\langle\!\langle \vec{v} \rangle\!\rangle| = \{*\}$, which by definition does not reduce.

* $\vec{v} = \alpha \cdot \vec{w}$, where we apply the IH to $|\langle\!\langle \vec{w} \rangle\!\rangle| = |\langle\!\langle \vec{v} \rangle\!\rangle|$.

* $\vec{v} = \vec{v}_1 + \vec{v}_2$, where we apply the IH to $|\langle\!\langle \vec{v}_1 \rangle\!\rangle|$ and $|\langle\!\langle \vec{v}_2 \rangle\!\rangle|$, since $|\langle\!\langle \vec{v} \rangle\!\rangle| = |\langle\!\langle \vec{v}_1 \rangle\!\rangle \cup \langle\!\langle \vec{v}_2 \rangle\!\rangle|$. □

**LEMMA 6.10.** For any $\vec{t} \in \text{PUNQ}$, $\vec{t} \rightsquigarrow \vec{r}$ implies $|\langle\!\langle \vec{r} \rangle\!\rangle| \subseteq \bigcup_{n>0} \{S_n \mid |\langle\!\langle \vec{t} \rangle\!\rangle| \to^n S_n\}$.

**PROOF.** By induction on the reduction of $\vec{t}$.
(If₀) $\vec{t} = \text{if } |\langle 0 \rangle\text{ then } \vec{s}_0 \text{ else } \vec{s}_1 \rightsquigarrow \vec{s}_0$, therefore $\langle\vec{r}\rangle = \langle\vec{s}_0\rangle$ and we have

$$ \begin{aligned} \langle\vec{t}\rangle &= ((\lambda x.\lambda y.x) \ \lambda x_{1\dots k}.\langle\vec{s}_0\rangle \ \lambda x_{1\dots k}.\langle\vec{s}_1\rangle) \ x_1 \dots x_k \\ &\to ((\lambda y.\lambda x_{1\dots k}.\langle\vec{s}_0\rangle) \ \lambda x_{1\dots k}.\langle\vec{s}_1\rangle) \ x_1 \dots x_k \\ &\to (\lambda x_{1\dots k}.\langle\vec{s}_0\rangle) \ x_1 \dots x_k \\ &\to^k \langle\vec{s}_0\rangle \end{aligned} $$

(If₁) $\vec{t} = \text{if } |\langle 1 \rangle\text{ then } \vec{s}_0 \text{ else } \vec{s}_1 \rightsquigarrow \vec{s}_1$, therefore $\langle\vec{r}\rangle = \langle\vec{s}_1\rangle$ and we have

$$ \begin{aligned} \langle\vec{t}\rangle &= ((\lambda x.\lambda y.x) \ \lambda x_{1\dots k}.\langle\vec{s}_0\rangle \ \lambda x_{1\dots k}.\langle\vec{s}_1\rangle) \ x_1 \dots x_k \\ &\to ((\lambda y.y) \ \lambda x_{1\dots k}.\langle\vec{s}_1\rangle) \ x_1 \dots x_k \\ &\to (\lambda x_{1\dots k}.\langle\vec{s}_1\rangle) \ x_1 \dots x_k \\ &\to^k \langle\vec{s}_1\rangle \end{aligned} $$

(Abs) $\vec{t} = (\lambda x.\vec{p}) v \rightsquigarrow \vec{p}[v/x]$, and therefore

$$ \begin{aligned} \langle\vec{t}\rangle &= \langle (\lambda x.\vec{p}) v \rangle = \lambda x_1 \dots \lambda x_k. \langle\vec{p}_{[x_1 \dots k]}\rangle \quad \underbrace{\langle v \rangle \dots \langle v \rangle}_{k \text{ times}} \\ &= \{ (\lambda x_1 \dots \lambda x_k \cdot p_i) \ v_1 \dots v_k \mid p_i \in \langle\vec{p}_{[x_1 \dots k]}\rangle \}, \quad v_j \in \langle v \rangle, j = 1 \dots k \} \\ &\to \{ p_i[v_1/x_1, \dots, v_k/x_k] \mid p_i \in \langle\vec{p}\rangle \}, \quad v_j \in \langle v \rangle, j = 1 \dots k \} \\ &= \langle\vec{p}\rangle[\langle v \rangle/x] = \langle\vec{p}[v/x]\rangle = \langle\vec{r}\rangle \end{aligned} $$

(Let) $\vec{t} = (\text{let } (x, y) = (v, w) \text{ in } \vec{s})$, then $\vec{t} \rightsquigarrow \vec{s}[v/x, w/y] = \vec{s}[v/x][w/y]$, since $y \notin \text{FV}(v)$.

$$ \begin{aligned} \langle\vec{t}\rangle &= \lambda z.(z \langle v \rangle (\langle w \rangle)) \lambda x.\lambda y.\langle\vec{s}\rangle \\ &\to (\lambda x.\lambda y.\langle\vec{t}\rangle) \langle v \rangle (\langle w \rangle) \\ &\to (\lambda y.\langle\vec{s}\rangle)[\langle v \rangle/x](\langle w \rangle) \\ &\to (\langle\vec{s}\rangle)[\langle v \rangle/x][\langle w \rangle/y] \\ &= \langle\vec{s}[v/x]\rangle[\langle w \rangle/y] \quad \text{(by Lemma A.2)} \\ &= \langle\vec{s}[v/x][w/y]\rangle \quad \text{(by Lemma A.2)} \\ &= \langle\vec{r}\rangle, \quad \text{since } y \notin \text{FV}(v). \end{aligned} $$

(If⁺) If $\vec{s}_1 \rightsquigarrow \vec{s}_2$, then $\vec{t} = (\text{if } \vec{s}_1 \text{ then } \vec{p}_1 \text{ else } \vec{p}_2) \rightsquigarrow (\text{if } \vec{s}_2 \text{ then } \vec{p}_1 \text{ else } \vec{p}_2) = \vec{r}$. By the induction hypothesis, $\langle\vec{s}_2\rangle \subseteq \bigcup_{n>0}\{\mathcal{R}_n \mid (\langle s_1 \rangle \to^n \mathcal{R}_n)\}$.

$$ \begin{aligned} \langle\vec{r}\rangle &= \langle \text{if } \vec{s}_2 \text{ then } \vec{p}_1 \text{ else } \vec{p}_2 \rangle = \langle\vec{s}_2\rangle \langle\vec{p}_1\rangle \langle\vec{p}_2\rangle \\ &\subseteq \operatorname{IH} \bigcup_{n>0} \{\mathcal{R}_n \mid \langle\vec{p}_1\rangle \langle\vec{p}_2\rangle \mid (\langle s_1 \rangle \to^n \mathcal{R}_n)\} \\ &\subseteq \bigcup_{n>0} \{\mathcal{S}_n \mid (\langle s_1 \rangle \langle\vec{p}_1\rangle \langle\vec{p}_2\rangle \to^n \mathcal{S}_n)\} \\ &= \bigcup_{n>0} \{\mathcal{S}_n \mid (\langle s_1 \vec{p}_1 \vec{p}_2 \rangle \to^n \mathcal{S}_n)\} \end{aligned} $$
(App) Let $((\vec{s}_2)) \subseteq \bigcup_{n>0} \{\mathcal{R}_n \mid ((s_1)) \to^n \mathcal{R}_n\}$, then

$$((\vec{r})) = ((p \vec{s}_2)) = ((p)) ((\vec{s}_2))$$

$$\subseteq^{\text{IH}} \bigcup_{n>0} \{((p)) \mathcal{R}_n \mid ((s_1)) \to^n \mathcal{R}_n\}$$

$$\subseteq \bigcup_{n>0} \{S_n \mid ((p)) ((s_1)) \to^n S_n\}$$

$$= \bigcup_{n>0} \{S_n \mid ((p s_1)) \to^n S_n\}$$

(Appv) Similar to (App).

(Pair) Let $((\vec{s}_2)) \subseteq \bigcup_{n>0} \{\mathcal{R}_n \mid ((s_1)) \to^n \mathcal{R}_n\}$, then

$$((\vec{r})) = ((\vec{s}_2, p)) = \lambda x.(x ((\vec{s}_2)) ((p)))$$

$$\subseteq^{\text{IH}} \bigcup_{n>0} \{\lambda x.(x \mathcal{R}_n ((p))) \mid ((s_1)) \to^n \mathcal{R}_n\}$$

$$\subseteq \bigcup_{n>0} \{S_n \mid \lambda x.(x ((s_1)) ((p))) \to^n S_n\}$$

$$= \bigcup_{n>0} \{S_n \mid ((s_1, p)) \to^n S_n\}$$

(Pairv) Similar to (Pair).

(Let+) Let $\vec{t} = (\text{let } (x, y) = s_1 \text{ in } \vec{p})$ such that $s_1 \rightsquigarrow \vec{s}_2$. Then

$$((\vec{r})) = ((\vec{s}_2)) \lambda x.\lambda y.((\vec{p}))$$

$$\subseteq^{\text{IH}} \bigcup_{n>0} \{\mathcal{R}_n \lambda x.\lambda y.((\vec{p})) \mid ((s_1)) \to^n \mathcal{R}_n\}$$

$$\subseteq \bigcup_{n>0} \{S_n \mid ((s_1)) \lambda x.\lambda y.((\vec{p})) \to^n S_n\}$$

$$= \bigcup_{n>0} \{S_n \mid ((s_1) \lambda x.\lambda y.\vec{p}) \to^n S_n\}$$

(Sup) Let $\vec{t} = \sum_{i \in I} \alpha_i \cdot p_i + \sum_{j \in J} \beta_j \cdot v_j$ such that $\forall i \in I, p_i \rightsquigarrow s_i$. Then, by the induction hypothesis, we have that $\forall i \in I, ((s_i)) \subseteq \bigcup_{n>0} \{S_n \mid ((p_i)) \to^n S_n\}$. We can see that

$$((\vec{r})) = \bigcup_{i \in I} ((s_i)) \cup \bigcup_{j \in J} ((v_j))$$

$$\subseteq^{\text{IH}} \bigcup_{i \in I} \left( \bigcup_{n>0} \{S_n \mid ((p_i)) \to^n S_n\} \right) \cup \bigcup_{j \in J} ((v_j))$$

$$= \bigcup_{n>0} \{S_n \mid ((\vec{r})) \to^n S_n\}. \qquad (\text{by Lemma 6.9})$$

(Equ) Since we have that $\vec{s}_1 \equiv \vec{s}_2$ and $\vec{s}_2 \rightsquigarrow \vec{s}_3$ and $\vec{s}_3 \equiv \vec{s}_4$, by the induction hypothesis the following are true:

$$(\text{IH1}) \quad ((\vec{s}_1)) \approx ((\vec{s}_2)),$$

$$(\text{IH2}) \quad ((\vec{s}_3)) \subseteq \bigcup_{n>0} \{S_n \mid ((\vec{s}_2)) \to^n S_n\},$$

$$(\text{IH3}) \quad ((\vec{s}_3)) \approx ((\vec{s}_4)).$$
We may then see that:

$$ (\|\vec{s}_4\|) \approx^{\mathrm{IH3}} (\|\vec{s}_3\|) \sqsubseteq^{\mathrm{IH2}} \bigcup_{n>0} \{S_n \mid (\|\vec{s}_2\|) \to^n S_n\} \approx^{\mathrm{IH1}} \bigcup_{n>0} \{S_n \mid (\|\vec{s}_1\|) \to^n S_n\}. $$

This concludes the proof. □

## A.4 Proofs of Section 7

In this section of the Appendix we consider the proofs and general points addressed in Section 7.

*Restriction to the algebraic numbers.* It is important to note the role that the complex coefficients in PUNQ play in the decidability of the typing system. In PUNQ, the restriction of amplitudes to the set $\overline{\mathbb{Q}}$ of algebraic numbers ensures that, for any amplitude $\alpha$, we are capable of checking if $\alpha = 0$ and therefore, for some $\vec{t}$, if $\alpha \cdot \vec{t} = \vec{0}$. This can be done efficiently when $\alpha \in \overline{\mathbb{Q}}$, as shown in [Halava et al. 2005, Proposition 2.2]. Allowing for the full set of complex numbers, on the other hand, allows for the encoding of undecidable problems, as shown in [Adleman et al. 1997].

*Reducing ground types.* In this section, we will be interested in the time complexity of reducing terms in order to check if they are orthogonal (see Section 3.2). In the program semantics (Figure 4), we allow in rule (Sup) for one-step reductions to alter different parts of a superposition simultaneously, so as to capture a single-step evolution of a quantum machine. However, if type checking requires performing some reduction steps, it must do so in the classical model, and therefore, we must consider the number of steps required by a classical Turing machine to perform the reduction.

From the typing rules (Figure 6), we are only interested in checking the orthogonality of terms to which we have successfully attributed some ground type $Q$. This limitation ensures a bounded dimension in the set of realizers, and a maximum number of base values that can be in a superposition. For such a $Q$, we define this number the *cardinality of $Q$*.

*Definition A.3 (Ground type dimension).* For any ground type $Q$, we define the *cardinality of $Q$*, written $\mathrm{card}(Q)$, inductively as:

$$ \mathrm{card}(\mathbb{B}) \triangleq 2, \quad \mathrm{card}(\#Q) \triangleq \mathrm{card}(Q), \quad \mathrm{card}(\S Q) \triangleq \mathrm{card}(Q), \quad \mathrm{card}(Q \times R) \triangleq \mathrm{card}(Q)\mathrm{card}(R). $$

Using the unitary semantics of Section 5, we can, in an equivalent way, define $\mathrm{card}(Q)$ as the cardinality of $\mathfrak{b}[\llbracket Q \rrbracket_0]$.

**LEMMA A.4.** Let $\vdash \vec{t} : Q$ such that $\vec{t} \rightsquigarrow^* \vec{v}$ for $\vec{v} \in V$. Then $\vec{v}$ can be computed from $\vec{t}$ classically in time at most $O(\mathrm{card}(Q) \mathrm{poly}(|\vec{t}|))$.

**PROOF.** Since $\vec{t} \in [\llbracket Q \rrbracket_0$, by the unitarity semantics, we have that $\vec{t} = \sum_{i=1}^n \alpha_i \cdot t_i$, such that $\forall i, t_i \in \mathfrak{b}[\llbracket Q \rrbracket_0$ and $n \le \mathrm{dim}(Q)$. The treatment of each $t_i$ in a reduction step is at most quadratic on $|t_i|$ (e.g. checking if $t_i$ is a value, performing variable substitution, converting to normal form, ...). This is done for each term $t_i$. Since there are at most $n$ such $t_i$, where $n$ is a constant fixed by the type $Q$, the number of reduction steps in the classical model remains polynomial. □

**LEMMA 7.5.** $\mathrm{CHK}_0 \subseteq \mathrm{CHK}_\times \subseteq \mathrm{CHK}_{\mathrm{untyped}} \subseteq \mathrm{CHK}$.

**PROOF.** The fact that $\mathrm{CHK}_0 \subseteq \mathrm{CHK}_\times$ is trivial. Similarly, $\mathrm{ORTHO}_V \subseteq \mathrm{ORTHO}$ since the only difference is that we perform an orthogonality check over all values and not the subset of values that correspond to the correct type. We also have that $\mathrm{ORTHO}_\times \subseteq \mathrm{ORTHO}_V$, since any variable substitution will still lead to orthogonal terms since the closed subterm which ensures orthogonality will not be altered. □
LEMMA 7.6. ORTHO₀, ORTHOₓ ∈ PTIME, and ORTHOuntyped ∈ Π₁₀.

PROOF. We analyze each case separately.

* (ORTHO₀ ∈ PTIME) Since $\vdash \vec{t}, \vec{s} : Q$, by Theorem 6.12, there exists a polynomial $P_Q$ such that $\vec{t}$ and $\vec{s}$ reduce to values, say $\vec{t} \rightsquigarrow \vec{v}$ and $\vec{s} \rightsquigarrow \vec{w}$ in at most a number $P_Q(\max(|\vec{t}|, |\vec{s}|))$ of reduction steps. Notice that, since $\vec{t}$ and $\vec{s}$ have type $Q$, in each step of the reduction they are represented by a superposition of at most $\dim(Q)$ terms, therefore the classical complexity of calculating the reduction differs only by a constant factor from the number of reduction steps. Finally, verifying that $\langle\vec{v}|\vec{w}\rangle = 0$ is also done in polynomial time since $|\vec{v}|, |\vec{w}| \le P_Q(\max(|\vec{t}|, |\vec{s}|))$ and we only need to reduce at most a constant $\dim(Q)$ number of terms in superposition.

* (ORTHOₓ ∈ PTIME) Checking if a term contains free variables can be done in linear time on its size, i.e. in time $O(\max(|\vec{t}|, |\vec{s}|))$. If the terms are closed, computing ORTHO₀($\vec{t}, \vec{s}$) can be done in polynomial time. If the terms are open, we proceed inductively on the structure of the term until we find (or not) matching subterms that are closed and from which we can prove orthogonality. This can easily be done in polynomial time.

* (ORTHOuntyped ∈ Π₁₀) Since $V_c$ is a countable set, it suffices to show that PERP is computable. To compute PERP, we only need to reduce the terms to values $\vec{w}_1$ and $\vec{w}_2$. Notice that, since the terms which we are using in the substitution may not have the correct type, this implies that the term we are reducing might not be typable in PUNQ, which renders Theorem 6.12 inapplicable and therefore we cannot place a (in particular, finite) bound on its number of reduction steps. However, by Theorem 6.12, we know that we need only apply a polynomial $P_Q$ number of reduction steps and, if the term is not yet a value (i.e., by Theorem 3.4, it does not reduce), we know that it does not correspond to the candidate type $Q$ in PUNQ, and therefore we do not need to consider it.

If the terms do reduce to values $\vec{w}_1$ and $\vec{w}_2$, then we may check if they belong to $[[Q]]_0$, the set of realizers of $Q$. Notice that, since the grammar of ground types $Q$ does not include applications nor polymorphisms, we can check that a term belongs in $[[Q]]_0$ purely syntactically. Finally, we can check ORTHO₀ in polynomial time. □