# Resource-Aware Quantum Programming with General Recursion and Quantum Control

Kostia Chardonnet, Emmanuel Hainry, Romain Péchoux, Thomas Vinet

► To cite this version:

Kostia Chardonnet, Emmanuel Hainry, Romain Péchoux, Thomas Vinet. Resource-Aware Quantum Programming with General Recursion and Quantum Control. 2026. hal-05518918

HAL Id: hal-05518918

https://inria.hal.science/hal-05518918v1

Preprint submitted on 19 Feb 2026

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

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

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Resource-Aware Quantum Programming with General Recursion and Quantum Control

**Kostia Chardonnet** [✉]
Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

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

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

**Emmanuel Hainry** [✉]
Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

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

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

**Romain Péchoux** [✉]
Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

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

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

**Thomas Vinet** [✉]
Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

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

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

## Abstract

This paper introduces the hybrid quantum language with general recursion Hyrql, driven towards resource-analysis. By design, Hyrql does not require the specification of an initial set of quantum gates. Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which yield quantum circuits of distinct complexity.

Regarding resource-analysis, we show how to relate the runtime of an expressive fragment of Hyrql programs with the size of the corresponding quantum circuits. We also manage to capture the class of functions computable in quantum polynomial time, which, by Yao's Theorem, corresponds to families of circuits of polynomial size. Consequently, this result paves the way for the use of termination and runtime-analysis techniques designed for classical programs to guarantee bounds on the size of quantum circuits.

**2012 ACM Subject Classification** Theory of computation → Quantum complexity theory; Mathematics of computing → Lambda calculus

**Keywords and phrases** Hybrid Quantum Programs, Resource Analysis

## 1 Introduction

**Motivations.** Most well-known quantum algorithms, such as Shor's algorithm [48], were historically designed on the Quantum Random Access Machine (QRAM) model [33]. In this model, a program interacts with a quantum memory through basic operations complying with the laws of quantum mechanics. These operations include a fixed set of quantum gates, chosen to be universal, as well as a probabilistic measurement of qubits. Consequently, the control flow is purely classical, i.e., depends on the (classical) outcome of a measure. Based on this paradigm, several high-level quantum programming languages have been introduced, each with different purposes and applications, from assembly code [18, 19], to imperative languages [26], circuit description languages [28], and λ-calculi [47].

A relevant issue was to extend these models to programs with quantum control, also known as coherent control, enabling a “program as data” treatment for the quantum paradigm. Quantum control consists in the ability to write superposition of programs in addition to superposition of data and increases the expressive power of quantum programming languages. It allows the programmer to write algorithms such as the quantum switch, which uses fewer resources (quantum gates) than algorithms with classical control [16] and is physically implementable [1, 43]. Hence, quantum control provides a computational advantage over classical control [3, 49, 34]. In the last decades, several quantum programming languages implementing this concept have been designed, non-exhaustively [2, 44, 24, 37, 56]. To get the best of both worlds, a natural next step was the development of hybrid
2 A Resource-Aware Hybrid Language

languages, i.e., languages that allow classical and quantum flow/data to be combined. The
hybrid paradigm is conveying considerable practical interest: for example, it is used by
quantum variational algorithms, a class of quantum algorithms leveraging both classical and
quantum computing resources to find approximate solutions to optimization problems; and the
properties of hybrid languages have also been deeply studied, non-exhaustively [51, 54, 21, 9].

Since hybrid languages offer interesting prospects in terms of expressiveness and optimal
resource consumption, a relevant and open issue concerns the development of resource-aware
(static) analyses of their programs. These static analyses can be applied to predict the
low-level resources required to execute quantum algorithms, such as the depth or size of a
quantum circuit.

**Contributions.** This work solves the above issue for the first time by introducing a HYbrid Recursive Quantum Language *Hyrql* on which a resource analysis can be performed. *Hyrql* is a hybrid extension of the functional quantum language *Spm* (*Symmetrical pattern-matching*) of [44, 37]. In *Spm*, the programmer can write down directly unitary applications, combining quantum superposition of terms with pattern-matching. Unitarity is enforced by a (decidable) linear typing discipline using an orthogonality predicate. *Spm* is, however, a purely quantum language, which makes the manipulation (and, consequently, resource analysis) of classical information awkward: they can be neither discarded nor duplicated by linearity. The hybrid nature of *Hyrql* relies on a typing discipline which delineates a clear separation between quantum/linear and classical/non-linear data in the typing contexts. Similarly to *Spm*, *Hyrql* does not include measurement: the flow from quantum data to classical data is handled through the use of a *shape* construct, as introduced in [28], which returns the classic structural information on data containing quantum information, without getting any information on the value of the quantum states. For example, the *shape* of a qubit list provides classical (duplicable) information, such as the number of qubits. The decision to provide *Hyrql* with a *Spm*-architecture was motivated by two important factors. First, in contrast with most of its competitors, *Spm* does not require the inclusion of an initial set of quantum gates, making its resource analysis generic. Second, thanks to its pattern-matching design, *Spm* allows for the reuse of a wide variety of tools designed for resource analysis (e.g., termination or complexity) of term rewriting systems.

Our paper contains the following main contributions:

- The introduction of the hybrid language with general recursion *Hyrql*, as well as its operational semantics, type system, and standard properties: confluence (Theorem 11), progress (Theorem 13), and subject reduction (Theorem 14).

- A proof that the orthogonality predicate in *Hyrql* is $\Pi_2^0$-complete, hence undecidable (Theorem 16). Consequently, typing is not decidable. This is not surprising as the language encompasses general recursion. The decidability of typing can still be recovered, on expressive sub-fragments of the language, e.g., when *Hyrql* is restricted to finite types and terminating programs (Proposition 17).

- A compilation from terms (of the good type) to quantum circuits, whose size is bounded by the runtime-complexity of the initial term (Theorem 25). In particular, terms that terminate in polynomial time characterize exactly the complexity class FBQP (Theorem 27 and 28). This result is not trivial, as lambda calculi do not comply with van Emde Boas' invariant thesis [50], i.e., a polynomial time reduction on a lambda term may correspond to an exponential time reduction on a Turing machine.

- An overview on how complexity results can be obtained and automatized by translating our language into term-rewrite systems, to use existing techniques for runtime analysis (e.g.,
interpretations [38], recursive path orderings [22, 23], dependency pairs [4], size-change principle [36]).

We illustrate the expressive power of the language through several examples: implementation of basic quantum gates (Hadamard gate, Example 1), higher-order (quantum switch, Example 2), general recursion (bounded quantum walk, Example 3), and hybrid control flow (protocol *BB84* [10], Example 30).

<table><caption>Table 1 Comparison table between hybrid quantum languages</caption><thead><tr><th></th><th>Hyrql</th><th>FOQ [29]</th><th>RQC<sup>++</sup> [55]</th><th>Silq [12]</th><th>Qunity [51]</th><th>DLPZ [21]</th></tr></thead><tbody><tr><td>Resource-aware</td><td>✓</td><td>✓</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>General recursion</td><td>✓</td><td>✗</td><td>✓</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>Higher-order</td><td>✓</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td></tr></tbody></table>

**Related works.** In Table 1, we provide a non-exhaustive comparison between the main families of hybrid quantum languages which treat classical data as first-class citizen. Towards that end, we consider the three following criteria.

- *Resource-aware* highlights if the language is designed towards resource analysis, that is, allows to characterize well-known complex classes of quantum computational models. This is the case of FOQ [29, 30], which characterizes, under restrictions, quantum polynomial time and quantum polylogarithmic time [27]. However, Hyrql has a greater expressive power than FOQ as it is not restricted to unitary operators. Moreover, all standard inductive datatypes can be expressed in Hyrql, whereas FOQ is restricted to lists of qubits.

- *General recursion* specifies whether the language includes unbounded recursion on classical data. The ability to handle this type of recursion is necessary for a resource analysis to be relevant (i.e., not trivial as in the case of strong normalizing languages).

- *Higher-order* denotes the ability of the language to feature general higher-order terms, i.e., functions taking functions as input. While some languages of Table 1 have syntactic constructs to do so, most of them are restricted to first-order calls.

As we are interested in resource analysis in the general setting, Table 1 only compares Hyrql with hybrid languages, rather than with existing languages with quantum control, non-exhaustively [44, 24, 54, 56]. Other studies have already been carried out on resource analysis in quantum programming languages. They use techniques (e.g., type systems) developed in the field of Implicit Computational Complexity (ICC, see [42]) to characterize quantum complexity classes [20], to infer the expected cost or expected value of a quantum program [6], or to infer upper bounds on quantum resources (depth and size of circuits) [17]. However, these studies are restricted to classical control. For example, [20] studies the use of soft linear logic [35] on a quantum lambda calculus [46], [6] adapts expectation transformers on a language based on QPL [45], and [17] develops a dependent type system on a variant of the Quipper circuit description language [28].

## 2 The Hyrql Programming Language

We introduce the syntax, the operational semantics, and the type system of Hyrql along with illustrating examples.
$$
\begin{array}{l@{\qquad}l}
(\text{Values}) & v ::= x \mid |0\rangle \mid |1\rangle \mid c(v_1, \dots, v_n) \mid \lambda x.t \mid \text{letrec} f x = t \mid \sum_{i=1}^n \alpha_i \cdot v_i \\
(\text{Terms}) & t ::= x \mid |0\rangle \mid |1\rangle \mid \text{qcase} t \{ |0\rangle \to t_0, |1\rangle \to t_1 \} \\
& \qquad \mid c(t_1, \dots, t_n) \mid \text{match} t \{ c_1(\vec{x}_1) \to t_1, \dots, c_n(\vec{x}_n) \to t_n \} \\
& \qquad \mid \lambda x.t \mid \text{letrec} f x = t \mid t_1 t_2 \mid \sum_{i=1}^n \alpha_i \cdot t_i \mid \text{shape}(t)
\end{array}
$$

<caption>Table 2 Syntax of the Hyrql language</caption>

2.1 Syntax

The syntax of Terms and Values in Hyrql is provided in Table 2. Terms feature variables, noted x, y, f, ... and taken from an infinite countable set of variables. We denote by $\vec{e}$ a (finite and possible empty) sequence of elements $e_1, \dots, e_n$. Qubits are introduced through basis states $|0\rangle, |1\rangle$, allowing us to write quantum conditionals $\text{qcase} t \{|0\rangle \to t_0, |1\rangle \to t_1\}$, which corresponds to the superposition of $t_0$ and $t_1$ controlled by qubit $t$. Hyrql also features classical constructors $c^s$ consisting of a constructor symbol $c$, and a signature $s$ indicating the type of the constructor. This will be formalized in Section 2.3 and will be used only when required. Constructors can be used in constructor application $c(t_1, \dots, t_n)$ and through pattern-matching, sometimes abbreviated as $\text{match}_{1 \le i \le n} t \{c_i(\vec{x}_i) \to t_i\}$. Each constructor symbol $c$ comes with a fixed arity and is always fully applied. We assume the existence of standard inductive constructors for unit ($\text{e}$), tensor products $\otimes$, natural numbers 0 and $S$, and lists $[]$ and $::$. For convenience, constructors are sometimes used in an infix notation. For example, tensor products will be written as $x \otimes y$ and list constructors as $h :: t$.

Higher-order is featured via a standard $\lambda$-abstraction $\lambda x.t$, and a construct for general recursion $\text{letrec} f x = t$. Term application is denoted by $t_1 t_2$.

Given amplitudes $\alpha_i \in \mathbb{C}$, the term $\sum_{i=1}^n \alpha_i \cdot t_i$ represents a superposition of terms $t_i$. In the special case where $n=2$, we just write $\alpha_1 \cdot t_1 + \alpha_2 \cdot t_2$. In a dual manner, the **shape** construct, introduced in [28], returns the classic structural information on data containing quantum information. For example, the shape of a qubit list is a copy of the list structure without the qubits (see Example 6).

In order to avoid conflicts between free and bound variables, we will always work up to
$\alpha$-conversion and use Barendregt's convention [8, p. 26] which consists in keeping all bound
and free variable names distinct, even when this remains implicit. We also define a partial
order $\triangleleft$ on terms, where $s \triangleleft t$ if $s$ is a strict subterm of $t$. We denote $\triangleleft$ as the reflexive
closure of $\triangleleft$. The size of a term is written $|t|$ and is defined standardly in Definition 29.

As we work with amplitudes and superpositions, Terms and Values have to be considered
with respect to a vector space structure. Towards that end, we define an equivalence relation
$\equiv$ in Table 3. Such definition relies on equivalence contexts, defined by the following grammar:

$$
(\text{Equiv. contexts}) \quad C_{\equiv} ::= \diamond \quad \mathbf{qcase} \ C_{\equiv} \left\{ \begin{array}{@{}l@{}} |0\rangle \to t_0, |1\rangle \to t_1 \end{array} \right\} \quad | \ c(\vec{t}_1, C_{\equiv}, \vec{t}_2) \ | \ tC_{\equiv} \ | \ C_{\equiv} t \\
\qquad \mid \mathbf{match}_{1 \le i \le n} \ C_{\equiv} \left\{ c_i(\vec{x}_i) \to t_i \right\} \ | \ t + C_{\equiv} \ | \ \mathbf{shape}(C_{\equiv})
$$

An equivalence context $C_{\equiv}$ is thus a term with one hole $\circ$; let $C_{\equiv}[t]$ be the term obtained by
filling the hole with $t$ in $C_{\equiv}$. The first rules of Table 3 make the definition of the $\sum$ construct
unambiguous/sound, i.e., it corresponds exactly to repeated applications of the $+$ construct.
The last rules of Table 3 are commutation rules highlighting the linearity of quantum terms.
$$t_1 + t_2 \equiv t_2 + t_1 \qquad t_1 + (t_2 + t_3) \equiv (t_1 + t_2) + t_3 \qquad 1 \cdot t \equiv t \qquad t + 0 \cdot t' \equiv t$$

$$\alpha \cdot (\beta \cdot t) \equiv (\alpha\beta) \cdot t \qquad \alpha \cdot (t_1 + t_2) \equiv \alpha \cdot t_1 + \alpha \cdot t_2 \qquad \alpha \cdot t + \beta \cdot t \equiv (\alpha + \beta) \cdot t$$

$$\mathbf{qcase} (\sum_{j=1}^{m} \alpha_j \cdot s_j) \{|0\rangle \to t_0, |1\rangle \to t_1\} \equiv \sum_{j=1}^{m} \alpha_j \cdot (\mathbf{qcase} s_j \{|0\rangle \to t_0, |1\rangle \to t_1\})$$

$$c(\vec{t}_1, \sum_{j=1}^{m} \alpha_j \cdot s_j, \vec{t}_2) \equiv \sum_{j=1}^{m} \alpha_j \cdot c(\vec{t}_1, s_j, \vec{t}_2)$$

$$\mathbf{match}_{1 \le i \le n} (\sum_{j=1}^{m} \alpha_j \cdot s_j) \{c_i(\vec{x}_i) \to t_i\} \equiv \sum_{j=1}^{m} \alpha_j \cdot (\mathbf{match}_{1 \le i \le n} s_j \{c_i(\vec{x}_i) \to t_i\})$$

$$t(\sum_{i=1}^{m} \alpha_j \cdot s_j) \equiv \sum_{j=1}^{m} \alpha_j \cdot t s_j$$

$$C_{\equiv}[t] \equiv C_{\equiv}[t'] \quad \text{when } t \equiv t'$$

<caption>Table 3 Equivalence relation ≡ ⊆ Terms × Terms</caption>

**► Example 1 (Quantum State and Hadamard Gate).** We can define the orthogonal basis states as $|\pm\rangle \triangleq \frac{1}{\sqrt{2}} \cdot |0\rangle \pm \frac{1}{\sqrt{2}} \cdot |1\rangle$. The Hadamard gate can be encoded in Hyrql:

$$\text{Had} \triangleq \lambda x. \mathbf{qcase} x \{|0\rangle \to |+\rangle, |1\rangle \to |-\rangle\}$$

**► Example 2 (Quantum Switch).** The quantum switch [16] is a program which, on two unitaries $U, V$ and a two-qubit state $|\phi\rangle$, applies $UV$ and $VU$, in superposition, to the second qubit, controlled by the value of the first qubit. This can be implemented in Hyrql by $QS U V |\phi\rangle$, where $QS$ is defined as:

$$\mathbf{QS} \triangleq \lambda f. \lambda g. \lambda q. \mathbf{match} q \{c \otimes t \to \mathbf{qcase} c \{|0\rangle \to |0\rangle \otimes f(gt), |1\rangle \to |1\rangle \otimes g(ft)\}\}$$

**► Example 3 (Bounded quantum walk).** Hyrql allows one to write recursive programs that are classically and quantumly controlled. The program $bqwalk$ produces all the possible quantum walk paths of size at most $n$, starting from a quantum state $q$:

$$\text{repeat} \triangleq \text{letrec} g n = \text{match} n \{0 \to [] , S(m) \to |0\rangle :: g m\}$$

$$\text{bqwalk} \triangleq \text{letrec} f q = \lambda n. \mathbf{qcase} q \left\{ \begin{array}{l} |0\rangle \to |0\rangle :: \text{(repeat } n) \\ |1\rangle \to |1\rangle :: \text{match } n \left\{ \begin{array}{l} 0 \to [] \\ S(m) \to (f(\text{Had } |1\rangle) m) \end{array} \right\} \end{array} \right\}$$

The programs from Examples 2 and 3 are strictly more than quantum circuits, as one execution of the program does not provide a full description of the corresponding behaviour. Thus, Hyrql is more than a circuit description language [28]. We also provide the hybrid quantum protocol BB84 [10] and the Quantum Fourier Transform in Appendix A.

## 2.2 Operational Semantics

In this section, we define the call-by-value operational semantics of Hyrql. As we are interested in resource analysis, we want to avoid reducing non-meaningful terms, e.g., a reduction of $t$ in $s+0 \cdot t \equiv s$ is meaningless. Towards that end, we introduce canonical forms (Definition 4), which take care of removing ill-behaved terms before applying a reduction. It relies on pure terms, which are defined by the following grammar:

$$(\text{Pure terms}) \quad p ::= x \mid |0\rangle \mid |1\rangle \mid \mathbf{qcase} p \{|0\rangle \to t_0, |1\rangle \to t_1\} \mid c(p_1, \dots, p_n) \\ \qquad \mid \mathbf{match}_{1 \le i \le n} p \{c_i(\vec{x}_i) \to t_i\} \mid \lambda x.t \mid \text{letrec} f x = t \mid tp \mid \text{shape}(t)$$
<figure><img src="image_10.png" /><figcaption>Table 4 Reduction rules of the language</figcaption></figure>

A *pure value*, denoted $v_p$, is a pure term that is a value.

**► Definition 4 (Canonical form).** A canonical form of a term $t$ is any term $t'$ such that $t \equiv t'$ and $t' = \sum_{i=1}^{n} \alpha_i \cdot p_i$, where $p_i$ are pure terms, $\alpha_i \neq 0$ and $p_i \equiv p_j$ implies $i = j$. The set of canonical forms is denoted by **CAN**.

The canonical form always exists and is unique for well-typed terms (Lemma 12). Note that the naming *pure terms* comes from [24] and is not related to *pure states* in quantum computing, as pure terms could semantically yield a mixed quantum state.

We also define *evaluation contexts* by the following grammar:

$$ (\text{Evaluation contexts}) \quad E ::= \diamond \left| \begin{array}{@{}l@{}} \mathbf{qcase} E \{ |0\rangle \rightarrow t_0, |1\rangle \rightarrow t_1 \} \mid c(\vec{p}, E, \vec{v}_p) \\ \mathbf{match}_{1 \le i \le n} E \{ c_i(\vec{x}_i) \rightarrow t_i \} \mid tE \mid Ev_p \end{array} \right. $$

Again, let $E[t]$ be the term obtained by filling the hole $\diamond$ with $t$ in $E$.

The operational semantics of *Hyrql* is described in Table 4 as a reduction relation $\rightsquigarrow \subseteq$ Terms $\times$ Terms, where $\{t/x\}$ denotes the standard substitution of a variable $x$ by a term $t$. The reduction implements a *call-by-value* strategy.

In the rule (Can), $t \rightsquigarrow^? t'$ holds if either $t \rightsquigarrow t'$ or, $\neg(\exists t'', t \rightsquigarrow t'')$ and $t' = t$. Intuitively, it means that we apply one reduction for each element of a superposition, when possible. In the rule (Shape_c), $\mathbf{shape}(\vec{v})$ is syntactic sugar for $\mathbf{shape}(v_1), \dots, \mathbf{shape}(v_n)$, and the shape of a signature $\mathbf{shape}(s)$ is defined formally in Definition 8. In all rules of Table 4, except for the (Can) and (Equiv) rules, the left-hand-side term is a pure term (i.e., not a superposition). This implies that any summation must be expressed as a canonical form, which avoids reducing a subterm with a null amplitude, or more generally to reduce two identical terms that would sum up to 0. The goal is to avoid reductions that have no physical meaning, as this would invalidate all resource analysis results.

We define $\rightsquigarrow^*$ as the reflexive and transitive closure of $\rightsquigarrow$. For $k \in \mathbb{N}$, we also write $t \rightsquigarrow^* \leq k t'$, when $t$ reduces to $t'$ in at most $k$ steps. A term $t$ *terminates*, if any chain of reduction starting from $t$ reaches a value, meaning that $t \rightsquigarrow^* \leq k v$ holds for some $k$.
**► Example 5.** Let us consider the Had program from Example 1, we can check that it gives the desired result when applying it to $|0\rangle$:

$$ \begin{align*} \text{Had} |0\rangle \rightsquigarrow \text{qcase} |0\rangle \{ |0\rangle \rightarrow |+\rangle, |1\rangle \rightarrow |-\rangle \} &\text{ via (Lbd)} \\ \rightsquigarrow |+\rangle &\text{ via (Qcase}_0) \end{align*} $$

Since the Hadamard gate is its own inverse we can recover $|0\rangle$. Given the following term $h_v = \text{qcase } v \{|0\rangle \rightarrow |+\rangle, |1\rangle \rightarrow |-\rangle\}$, we have the following:

$$ \text{Had} |+\rangle \equiv \frac{1}{\sqrt{2}} \cdot \text{Had} |0\rangle + \frac{1}{\sqrt{2}} \cdot \text{Had} |1\rangle \rightsquigarrow \frac{1}{\sqrt{2}} \cdot h_0 + \frac{1}{\sqrt{2}} \cdot h_1 \rightsquigarrow \frac{1}{\sqrt{2}} \cdot |-\rangle + \frac{1}{\sqrt{2}} \cdot |0\rangle \equiv |0\rangle $$

Note that the reductions are performed in parallel on each term of the superpositions using rule (Can) of Table 4.

**► Example 6.** Given a qubit list $l = |0\rangle :: |1\rangle :: |+\rangle :: []$, one can verify that shape($l$) $\rightsquigarrow$* () :: () :: () :: [] (note that $::$ and $[]$ use distinct signatures in $l$ and the reduct of shape($l$)). The result is a list of same length as $l$, with no quantum data anymore, hence it can be treated non-linearly. This operation is independent of the value of each qubit in the list.

It is worth mentioning that while we can write qubit streams in Hyrql, the call-by-value strategy will require it to be evaluated before doing any operation on such data.

## 2.3 Type System

**Types and Contexts.** Types in Hyrql are provided by the following grammar:

$$ (\text{Types}) \quad T ::= \text{Qbit} \mid B \mid T \to T \mid T \Rightarrow T $$

Qbit is the type for qubits and B is a constructor type from a fixed set $\mathbb{B}$. A basic type, noted $B^l$, is either a qubit type, or a constructor type B, i.e., $B^l \in \{\text{Qbit}\} \cup \mathbb{B}$. Each constructor type is defined by its set of constructors:

$$ \text{Cons}(B) \triangleq \{c^s \mid s = B_1^l, \dots, B_n^l \rightarrow B\} $$

A constructor symbol c comes with a signature s of arity n, defining the inputs and output types of c. We may write $c^B$ when s is of arity 0. By construction, $\text{Cons}(B) \cap \text{Cons}(B') = \emptyset$ when $B \neq B'$. In what follows, we will consider the following constructor types: a unit type 1 with a unique constructor ()$^1$; tensor types $B_1^l \otimes B_2^l$ for given types $B_1^l, B_2^l$ with a unique constructor $\otimes^{B_1^l, B_2^l} B_2^l \rightarrow B_1^l \otimes^{B_2^l} B_2^l$; natural numbers nat with constructors $0^{\text{nat}}$ and $S^{\text{nat} \to \text{nat}}$; lists list($B^l$) for a given type $B^l$, with constructors $[]^{\text{list}(B^l)}$ and $:\!^B$, list($B^l$) $\rightarrow$ list($B^l$). We consider that $\mathbb{B}$ always contains the unit type 1.

The language also features two distinct higher-order types for linear and non-linear functions, denoted respectively by $\to$ and $\Rightarrow$.

In the typing discipline, it will be useful to distinguish between types based on whether or not they contain quantum data. The latter must follow the laws of quantum mechanics (no-cloning), whereas classical types are more permissive. Towards that end, we define inductively the set of quantum constructor types $\mathbb{B}_Q$ by

$$ \mathbb{B}_Q \triangleq \{B \in \mathbb{B} \mid \exists c^{B_1^l, \dots, B_n^l} \rightarrow B, \exists 1 \le i \le n, B_i^l \in \mathbb{B}_Q \cup \{\text{Qbit}\}\}. $$

A quantum constructor type $B_Q \in \mathbb{B}_Q$ has (at least) a constructor symbol with a type Qbit or (inductively) a quantum constructor type in its signature. The set $\mathbb{B}_C$ of classical constructor
8 A Resource-Aware Hybrid Language

types $B_C$ is defined by $B_C \triangleq B \setminus B_Q$. For example, $1$, nat $\in B_C$ whereas list(Qbit) $\in B_Q$. This allows us to split the types between quantum types $Q$ and classical types $C$:

$$Q ::= Qbit \mid B_Q \quad C ::= B_C \mid T \to T \mid T \Rightarrow T$$

It is now assumed that the inputs of each constructor are ordered, containing first variables of classical type, then variables of quantum type, enabling a hybrid behaviour.

Typing contexts are defined as follows:

$$\Gamma, \Delta ::= \emptyset | \{x : T\} | \{[x : T]\} | \Gamma \cup \Delta,$$

where $[x : T]$ is called a *boxed variable*, indicating that $x$ is a linear variable captured by a *shape* construct. We define the *domain* of a context $\Delta$ as the set of its variables, i.e., $\text{dom}(\Delta) \triangleq \{x \mid \exists T, x : T \in \Delta \lor [x : T] \in \Delta\}$. Whenever we write $\Gamma, \Delta$ or $\Gamma; \Delta$, it is assumed that $\Gamma$ and $\Delta$ are compatible, that is, $\text{dom}(\Gamma) \cap \text{dom}(\Delta) = \emptyset$. We use the shorthand notation $\vec{x} : \vec{T}$ for $x_1 : T_1, \dots, x_n : T_n$; and $[\Delta]$ for $[x_1 : T_1], \dots, [x_n : T_n]$.

**Typing rules.** A typing judgment is written $\Gamma; \Delta \vdash t : T$, describing that the term $t$ is *well-typed*, with type $T$, under *non-linear context* $\Gamma$ and *linear context* $\Delta$. The typing rules of the language are defined in Table 5. A well-typed term $\Gamma; \Delta \vdash t : T$ is *closed* if $\Gamma = \Delta = \emptyset$. A well-typed closed term $t$ is said to *terminate over any input*, if for any well-typed closed value $v_1, \dots, v_n$ terminating over any input such that $tv_1 \dots v_n$ is a well-typed closed term of type $B^l$, $tv_1 \dots v_n$ terminates.

Typing rules rely on an external *orthogonality* predicate on terms. This uses the notion of $\Delta$-context substitutions, which, for a given $\Delta$, denote the substitutions $\sigma$ such that for any $x : T$ with $x : T \in \Delta$ or $[x : T] \in \Delta$, $\sigma(x) = v$, where $v$ is a well-typed closed value of type $T$ that terminates over any given input. It also requires the definition of an *inner product* on values with a canonical form, defined below, where $\delta_{x,y}$ is the Kronecker symbol.

$$\langle v, w \rangle \triangleq \sum_{i=1}^{n} \sum_{j=1}^{m} \alpha_i \beta_j^* \delta_{v_i, w_j}, \quad \text{where } v \equiv \sum_{i=1}^{n} \alpha_i \cdot v_i \in \text{CAN} \text{ and } w \equiv \sum_{j=1}^{m} \beta_j \cdot w_j \in \text{CAN}$$

**► Definition 7 (Orthogonality).** Let $\Gamma; \Delta \vdash t : Q$ and $\Gamma; \Delta \vdash t' : Q$ be two well-typed terms. $t$ and $t'$ are orthogonal, written $t \perp t'$, if for any $\Gamma \cup \Delta$-context substitution $\sigma$:

- $\sigma(\text{shape}(t)) \rightsquigarrow^* v, \sigma(\text{shape}(t')) \rightsquigarrow^* v'$ and $v = v'$;

- $\sigma(t) \rightsquigarrow^* v \in \text{CAN}, \sigma(t') \rightsquigarrow^* v' \in \text{CAN}, \text{ and } \langle v, v' \rangle = 0$.

These conditions imply that the reduced values share the same classical structure, and that their quantum data is orthogonal. For example, orthogonal lists must be of the same size. This is used in the typing rules (qcase) and (sup) of Table 5 to ensure the feasibility of typed terms, similarly to existing languages [24, 37, 21]. Note that the rules requiring this predicate apply it only to well-typed terms, thus the type system is not cyclic. While an alternative condition could have been given with dependent types, this gives a uniform process that is defined for any type, including types that could be defined later by a programmer, and a simpler type system. As we will prove that values have a unique canonical form (Lemma 12), the inner-product condition is sound.

We also define the *shape of a basic type* below.

**► Definition 8.** The shape of a basic type is defined inductively as $\text{shape}(\text{Qbit}) \triangleq 1$, and $\text{shape}(B)$ is the type defined by the constructor set

$$\text{Cons}(\text{shape}(B)) \triangleq \{ c^{\text{shape}(s)} \mid c^s \in \text{Cons}(B) \}$$
$$ \overline{\Gamma; x : T \vdash x : T} \quad (\text{ax}) $$

$$ \overline{\Gamma, x : C; \emptyset \vdash x : C} \quad (\text{ax}_c) $$

$$ \overline{\Gamma; \emptyset \vdash |0\rangle : Qbit} \quad (\text{ax}_0) $$

$$ \frac{\Gamma; \Delta \vdash t : Qbit \quad \Gamma; \Delta' \vdash t_0 : Q \quad \Gamma; \Delta' \vdash t_1 : Q \quad t_0 \perp t_1}{\Gamma; \emptyset \vdash |1\rangle : Qbit} \quad (\text{ax}_1) \quad (\text{qcase}) $$

$$ \frac{s = B_1^{\|}, \dots, B_n^{\|} \rightarrow B \quad \Gamma; \Delta_i \vdash t_i : B_i^{\|}}{\Gamma; \Delta_1, \dots, \Delta_n \vdash c^s(t_1, \dots, t_n) : B} \quad (\text{cons}) $$

$$ \frac{\text{Cons}(B) = \{c_i^{s_i}\}_{i=1}^n \quad s_i = \overrightarrow{C_i}, \overrightarrow{Q_i} \rightarrow B \quad \Gamma_1; \Delta_1 \vdash t : B \quad \Gamma_2, \overrightarrow{y_i} \rightarrow \overrightarrow{C_i}; \Delta_2, \overrightarrow{z_i} \rightarrow \overrightarrow{Q_i} \vdash t_i : B^{\|}}{\Gamma_1, \Gamma_2; \Delta_1, \Delta_2 \vdash \text{match}_{1 \le i \le n} t \{c_i^{s_i}(\overrightarrow{y_i}, \overrightarrow{z_i}) \rightarrow t_i\} : B^{\|}} \quad (\text{match}) $$

$$ \frac{\Gamma; \Delta, x : T \vdash t : T' \quad (\text{abs})}{\Gamma; \Delta \vdash \lambda x.t : T \rightarrow T'} $$

$$ \frac{\Gamma, x : C; \Delta \vdash t : T \quad (\text{abs}_c)}{\Gamma; \Delta \vdash \lambda x.t : C \Rightarrow T} $$

$$ \frac{\Gamma, f : T; \emptyset \vdash \lambda x.t : T \quad (\text{rec})}{\Gamma; \emptyset \vdash \text{letrec} f x = t : T} $$

$$ \frac{\Gamma; \Delta \vdash t_1 : T \rightarrow T' \quad \Gamma; \Delta' \vdash t_2 : T}{\Gamma; \Delta, \Delta' \vdash t_1 t_2 : T'} \quad (\text{app}) $$

$$ \frac{\Gamma; \Delta \vdash t_1 : C \Rightarrow T \quad \Gamma; \emptyset \vdash t_2 : C}{\Gamma; \Delta \vdash t_1 t_2 : T} \quad (\text{app}_c) $$

$$ \frac{\Gamma; \Delta \vdash t_i : Q \quad \sum_{i=1}^n |\alpha_i|^2 = 1 \quad \forall i \neq j, t_i \perp t_j}{\Gamma; \Delta \vdash \sum_{i=1}^n \alpha_i \cdot t_i : Q} \quad (\text{sup}) \quad \frac{\Gamma; \Delta \vdash t : B^{\|}}{\Gamma, [\Delta]; \emptyset \vdash \text{shape}(t) : \text{shape}(B^{\|})} \quad (\text{shape}) $$

$$ \frac{\Gamma, [x : B^{\|}] ; \Delta, y : B^{\|} \vdash t : T}{\Gamma; \Delta, y : B^{\|} \vdash t \{y/x\} : T} \quad (\text{contr}) $$

$$ \frac{\Gamma; \Delta \vdash t : T \quad t \equiv t'}{\Gamma; \Delta \vdash t' : T} \quad (\text{equiv}) $$

<caption>Table 5 Typing rules of the language</caption>

where the shape of a signature $s = B_1^{\|}, \dots, B_n^{\|} \rightarrow B$ is defined as

$$ \mathbf{shape}(s) \triangleq \mathbf{shape}(B_1^{\|}), \dots, \mathbf{shape}(B_n^{\|}) \rightarrow \mathbf{shape}(B). $$

In particular, the shape of a list of qubits is a list of units, i.e., $\mathbf{shape}(\text{list}(Qbit)) = \text{list}(1)$, which is coherent with the reduction rules in Table 4. By construction, it always holds that $\mathbf{shape}(B^{\|}) \in \mathbb{B}_C$. This is used in the typing rule (shape) of Table 5, which extracts the classical structure of a quantum term, boxes any variable in $\Delta$, and puts it in the non-linear context. The judgment obtained has an empty linear context and thus can be used classically (i.e., duplicated or discarded). A boxed variable $x$ can be removed using rule (contr) of Table 5, by associating with a linear variable of same type $y$, allowing to read both the quantum data and the classic structural information of $y$ (see Example 9).

**Typing derivations.** We write $\pi \triangleright \Gamma; \Delta \vdash t : T$ for the tree of root $\Gamma; \Delta \vdash t : T$ derived using the rules of Table 5. We also denote by $\pi \triangleright (r)[t_1, \dots, t_n]$ the subtree of $\pi$ rooted by (r) and whose premises are $t_1, \dots, t_n$.

**► Example 9.** The length of a list can be computed by the following term:

$$ \mathbf{len} \triangleq \mathbf{letrec} f x = \mathbf{match} x \{[ ] \rightarrow 0, h :: t \rightarrow S(f t)\} $$

Notice that we discard $h$, thus the list is not used linearly. Therefore, we can only type this as a non-linear function, i.e., $\emptyset; \emptyset \vdash \mathbf{len} : \text{list}(B) \Rightarrow \mathbf{nat}$ for a given $B \in \mathbb{B}_C$. However,
**Theorem 13 (Progress).** Let $\emptyset; \emptyset \vdash t : T$ be a closed term, either $t$ is equivalent to a value, or $t$ reduces.

Contrary to standard progress lemmas, we require $t$ to be a value up to equivalence. For instance, the term $|0\rangle + 0 \cdot (\lambda y.y) |1\rangle$ does not reduce and is not a value.

Finally, typing is also preserved by reduction, provided we consider pure or terminating terms.

**Theorem 14 (Subject reduction).** Let $\Gamma; \Delta \vdash t : T$ be a well-typed term, and $t \rightsquigarrow t'$. If $t$ terminates or $t$ is pure, then $\Gamma; \Delta \vdash t' : T$.

**Remark 15.** Theorem 14 does not hold on non-terminating and non-pure terms, as we cannot type non-terminating superpositions. This is the case with the following example, with the Bell state $|\Phi^+\rangle = \frac{1}{\sqrt{2}} \cdot |0\rangle \otimes |0\rangle + \frac{1}{\sqrt{2}} \cdot |1\rangle \otimes |1\rangle$:

$$ (\lambda y.qcase((\text{letrec } f x = fx)|0\rangle)\{ |0\rangle \rightarrow |0\rangle \otimes y, |1\rangle \rightarrow |1\rangle \otimes y \}) |\Phi^+\rangle $$

While such a term is well-typed, it reduces to a superposition of non-terminating pure terms, which is impossible to type through the rule (sup) from Table 5, as the orthogonality predicate requires termination. This is a counterpart of having a general language with few restrictions; however, as resource analysis will be done on terminating terms, such ill-behaved cases will not be considered.

## 3.2 Decidability of Orthogonality

The orthogonality predicate of Definition 7 is extensionally complete. As a consequence, it is undecidable. Indeed, it is as hard as the Universal Halting Problem [25], that is $\Pi_2^0$-complete in the arithmetical hierarchy [41]. Orthogonality uses the inner product, which requires computing additions, multiplications, and nullity checks on complex numbers. Recall that algebraic numbers are complex numbers in $\mathbb{C}$ that are roots of a polynomial in $\mathbb{Q}[X]$, and write their sets as $\bar{\mathbb{C}}$. In the field of algebraic numbers, equality is decidable, and product and sum are computable in polynomial time [31]. We thus restrict ourselves to terms that only contain amplitudes $\alpha \in \bar{\mathbb{C}}$.

**Theorem 16 (Undecidability of orthogonality).** Deciding orthogonality between two well-typed terms is $\Pi_2^0$-complete.

This is not surprising as Hyrql allows for general recursion. Decidability can be recovered under some slight restrictions. Towards that end, we introduce for basic types a type depth $d$ as a partial function $d : \{\text{Qbit}\} \cup \mathbb{B} \rightarrow \mathbb{N}$, defined as follows:

$$ d(\text{Qbit}) \triangleq 1 \qquad d(B) \triangleq \max_{\substack{s=B^l, \dots, B_n^l \\ c^s \in \text{Cons}(B)}} \left( \sum_{i=1}^{n} d(B_i^l) \right) + 1 $$

Note that $d(B^l)$ is undefined on inductive types. We call finite types any basic type with a defined depth.

**Proposition 17.** Given a finite type $B^l$, and two terminating terms $\emptyset; \emptyset \vdash s : B^l$, $\emptyset; \emptyset \vdash t : B^l$, it is decidable whether they are orthogonal.

In previous works of Spm [15, 14], the syntax of the language was restrictive enough to ensure the decidability of orthogonality. As Spm is a strict sublanguage of Hyrql, orthogonality can also be decided on this fragment.
## 3.3 Complexity Properties

We finally discuss how quantum circuits and their size are related to terms of Hyrql and their runtime-complexity. Towards that end, we introduce a sublanguage of Hyrql (Hyrql(T), Definition 24) based on three restrictions: one on the runtime-complexity of the program, to ensure terminating terms (Time(T), Definition 18); one on types, to obtain terms that can be represented as circuits (CircuitTerms, Definition 19); and one on recursive calls, to have a faithful relation between the size of the circuit and the runtime-complexity (Faithful, Definition 22). This allows, for terms terminating in polynomial time, to characterize precisely the class FBQP. We first define the time termination of a term.

**Definition 18.** Given a term $\emptyset; \emptyset \vdash t : Q \to Q'$ and a function $T : \mathbb{N} \to \mathbb{N}$, we say that $t$ terminates in time $T$, if for any value $\emptyset; \emptyset \vdash v : Q$, $tv$ terminates in at most $T(|v|)$ steps. Let $\text{Time}(T)$ be the set of terms terminating in time $T$.

Note that this definition should not be confused with termination defined in Section 2.2.

To obtain terms that can be compiled to a circuit form, we introduce a typed restriction CircuitTerms, which relies on the following type grammar:

$$B_r ::= \text{Qbit} \mid \text{nat} \mid \text{list}(B_r) \mid B_r \otimes B_r \mid B_r \to B_r \mid B_r \Rightarrow B_r$$

**Definition 19 (Circuit terms).** We define CircuitTerms as the set of well-typed terms $\pi \triangleright \emptyset; \emptyset \vdash s : Q \to Q'$ satisfying the following conditions:

- Any type in $\pi$ is generated by the grammar of $B_r$;

- Any rule $\pi \triangleright (\text{sup})[t_1, \dots, t_n]$ satisfies $t_i \in \text{Value}$;

- Any rule $\pi \triangleright (\text{qcase})[t, t_0, t_1]$ satisfies either $t_0, t_1 \in \text{Value}$; or $t_0 = c(|0\rangle, s_0)$ and $t_1 = c(|1\rangle, s_1)$, for $c \in \{\otimes, \dots\}$.

While the first condition yields terms that can be represented by a circuit, the two others allow for an efficient compilation and guarantees that any superposition can be compiled effectively to circuits. Note that while these terms only take inputs of type $Q$, to represent them clearly in a quantum circuit, they can nonetheless contain multiple inputs and higher-order constructs in their body. This restriction alone is sufficient to compile $t$ to a family of circuits in Theorem 21, provided $t$ terminates for a given time $T$.

**Example 20.** The following term, which is an adaptation of the program from Example 3, belongs to CircuitTerms.

$$\pi \triangleright \emptyset; \emptyset \vdash \lambda x.\text{match} x \{q \otimes n \to \text{bqwalk} q n\} : \text{Qbit} \otimes \text{nat} \to \text{list}(\text{Qbit})$$

Any type in $\pi$ is derived from $B_r$. Term superposition happens only in Had and is between values. Furthermore, there are two qcase constructs, either between values, or between two terms $|0\rangle :: s_0$ and $|1\rangle :: s_1$, thus it satisfies all properties of CircuitTerms. Note that as $B_r$ allows for tensor products, any program taking multiple inputs can always be rewritten using the same technique so that it belongs to CircuitTerms.

In the literature, family of circuits are parameterized by the size of their input. However, in Hyrql, knowing the size might not be sufficient, e.g., on inputs of type `list(Qbit) ⊗ list(Qbit)`. To remedy this, we will parameterize the family by the shape of the input, which will give us the necessary information. Formally, we define

$$S(Q) \triangleq \{w | \emptyset; \emptyset \vdash w : \text{shape}(Q)\}$$

$$S(w) \triangleq \{v | \emptyset; \emptyset \vdash v : Q \wedge \text{shape}(v) \rightsquigarrow w\}, \forall w \in S(Q),$$
where $S(Q)$ is the set of shape of terms of type $Q$, and $S(w)$ the set of values of shape $w$.

Assuming an encoding of $t \in \text{CircuitTerms}$ to a quantum state $|t\rangle$, which can be done naturally, a circuit $C$ is said to approximate $v$ on input $v'$ with probability $p$, if $C$ evaluates to $|\phi\rangle$, on input $|v'\rangle$ (up to ancillary qubits), and $|\langle v|\phi\rangle|^2 \ge p$.

**Theorem 21 (Circuit compilation).** Let $t \in \text{CircuitTerms} \cap \text{Time}(T)$ be a term of type $Q \to Q'$ for a given $T: \mathbb{N} \to \mathbb{N}$. Then, we can generate a family of circuits $C(t) \triangleq (C_w)_{w \in S(Q)}$ such that for any $w \in S(Q)$ and any $v \in S(w)$, $C_w$ approximates $v'$ with probability $\frac{2}{3}$ on input $v$, where $tv \rightsquigarrow^* v'$.

We are now interested in the size of each circuit of the family, i.e., the total number of gates acting on the circuit; in particular, the goal is to exhibit a relation between the size and the runtime of the initial term $t$. To avoid a blowup due to recursive calls, we introduce a syntactic restriction **Faithful**. It relies on the notion of the width of a variable $f$ in a term $t$, written $w(f, t)$ and defined inductively as follows:

$$
\begin{align*}
w(f, x) &\triangleq \delta_{x,f} \qquad w(f, |i\rangle) \triangleq 0 \qquad w(f, \lambda x.t) \triangleq w(f, t) \qquad w(f, \text{letrec } g x = t) \triangleq w(f, t) \\
w(f, t_1 t_2) &\triangleq w(f, t_1) + w(f, t_2) \qquad w(f, \sum_{i=1}^n \alpha_i \cdot t_i) = \max_{1 \le i \le n} w(f, t_i) \\
w(f, c(t_1, \dots, t_n)) &\triangleq \sum_{i=1}^n w(f, t_i) \qquad w(f, \text{shape}(t)) = w(f, t) \\
w(f, \text{qcase } t \{ |0\rangle \to t_0, |1\rangle \to t_1 \}) &\triangleq w(f, t) + \max(w(f, t_0), w(f, t_1)) \\
w(f, \text{match}_{1 \le i \le n} t \{ c_i(\vec{x}_i) \to t_i \}) &\triangleq w(f, t) + \max_{1 \le i \le n} w(f, t_i)
\end{align*}
$$

**Definition 22.** A term $t$ is said to compile faithfully, if for any term $t' = (\text{letrec } f \ x = s)$ such that $t' \le t$, the following conditions hold:

- $w(f, s) \le 1$;

- $\exists! t', \forall t_1, ft_1 \le s \implies t_1 = t'$;

- $\neg \exists t', t'f \le s$.

Let **Faithful** be the set of terms that compile faithfully.

The first two conditions are derived from [30], and ensure that, for each recursive program $\text{letrec } f \ x = s$, all recursive calls are done in different branches of a **qcase** or **match**, with the same input. Furthermore, the last condition ensures that this behaviour is preserved, even in presence of higher-order constructs.

**Example 23.** The program of Example 20 belongs to **Faithful**, as both **bqwalk** and **repeat** only perform one recursive call. All the examples across the paper also satisfy this criterion.

**Definition 24.** Let $T: \mathbb{N} \to \mathbb{N}$. We define **Hyrl**($T$) as follows:

$$ \text{Hyrl}(T) \triangleq \text{CircuitTerms} \cap \text{Faithful} \cap \text{Time}(T) $$

Any term in this subset compiles to quantum circuits of size bounded polynomially by $T$.

**Theorem 25 (Bounded circuit compilation).** Let $T: \mathbb{N} \to \mathbb{N}$, and let $t \in \text{Hyrl}(T)$ be a term of type $Q \to Q'$. Then, we can generate a family of circuits $C(t) \triangleq (C_w)_{w \in S(Q)}$ and a polynomial $P$ such that, for any $w \in S(Q)$:

- $|C_w| \le P(T(|w|))$;

- $\forall v \in S(w), C_w$ approximates $v'$ with probability $\frac{2}{3}$ on input $v$, where $tv \rightsquigarrow^* v'$.
14 A Resource-Aware Hybrid Language

We now want to use Theorem 25 to obtain a characterization of FBQP (Definition 26). We recall that a family of circuits $(C_n)_{n \in \mathbb{N}}$ is said to be uniform polynomially-sized with $\alpha: \mathbb{N} \to \mathbb{N}$ if there exists $P \in \mathbb{N}[X]$ such that $|C_n| \le P(n)$ and $C_n$ has exactly $\alpha(n)$ ancillary qubits, and there is a polynomial-time Turing machine, which takes $n$ as input, and outputs a representation of $C_n$ for any $n \in \mathbb{N}$.

**Definition 26 ([11]).** A binary function $f: \{0,1\}^* \to \{0,1\}^*$ is said to be computed by a family of circuits $(C_n)_{n \in \mathbb{N}}$ if for any $x \in \{0,1\}^*$, $C_{|x|}$ approximates $f(x)$ with probability $\frac{2}{3}$ on input $x$. FBQP is defined as the set of binary functions computed by a uniform polynomially-sized family of circuits.

To characterize FBQP, we define the following set of terms, which terminate in polynomial time, and have list of qubits as input:

$$ \text{Hyrql}(\text{Poly})_{\text{qList}} \triangleq \cup_{P \in \mathbb{N}[X]} \{ t \in \text{Hyrql}(P) \mid \emptyset; \emptyset \vdash t : \text{list}(\text{Qbit}) \to Q \} $$

These generated families of circuits will be indexed by natural numbers instead of shape, as one can remark that $S(\text{list}(\text{Qbit}))$ is in bijection with $\mathbb{N}$. Altogether, $\text{Hyrql}(\text{Poly})_{\text{qList}}$ contain terms that are compiled to circuits approximating functions of FBQP.

**Theorem 27 (FBQP soundness).** Let $t \in \text{Hyrql}(\text{Poly})_{\text{qList}}$, and let $f: \{0,1\}^* \to \{0,1\}^*$. If $f$ is computed by $C(t)$, then $f \in \text{FBQP}$.

For example, the Quantum Fourier Transform program from Example 31 belongs to FBQP, and can thus be compiled to circuits of polynomial size.

We now prove FBQP completeness, meaning that every function of FBQP can be represented by a function in $\text{Hyrql}(\text{Poly})_{\text{qList}}$. This is proven by writing any function of Yamakami's algebra [53], which is known to capture FBQP, into $\text{Hyrql}(\text{Poly})_{\text{qList}}$.

**Theorem 28 (FBQP completeness).** Let $f: \{0,1\}^* \to \{0,1\}^* \in \text{FBQP}$. Then, there exists $t \in \text{Hyrql}(\text{Poly})_{\text{qList}}$ such that $C(t)$ computes $f$.

We have given a typed, syntactic and semantic restriction of Hyrql, that compiles into a bounded family of quantum circuits. Such restriction could be refined, either to accept more terms by lifting requirements in Definition 22, as done in [30]; or by adding requirements to characterize more precise complexity classes [27]. We are nonetheless able to encapsulate FBQP, which demonstrates the expressivity of the $\text{Hyrql}(\text{Poly})_{\text{qList}}$ fragment.

4 Towards Automatization

Theorem 25 establishes that, given a program that terminates with a specified complexity bound, one can extract a concrete quantum circuit exhibiting the same space complexity. This result is particularly significant, as it enables the characterization of quantum polynomial time, as shown in Theorem 27 and Theorem 28. However, the burden of proving termination of a Hyrql program currently rests entirely on the programmer. This naturally raises the following question: to what extent is the termination of Hyrql programs semi automatable?

We argue that such automatization is feasible by leveraging techniques from Term Rewrite Systems (TRS)<fnref n="1" />, as they are equipped with a rich toolbox for analyzing both termination

<footnote n="1">¹ More specifically, a higher-order version called Simply-Typed TRS [52], but we do not enter this level of details here.</footnote>
and computational complexity. Approaches to termination analysis include non-exhaustively recursive path orderings [22, 23], dependency pairs [4], and size-change termination [36]. Similarly, several methods address complexity analysis, e.g., interpretation methods [13, 38, 7], and polynomial path orders [39, 5].

Although a full formal treatment is left to future work, we present an illustrative example supporting our claim. Specifically, we illustrate how a Hyrql program can be efficiently translated into a (quantum) TRS, how the reduction behaviour of the original program is faithfully simulated by the resulting rewriting system while preserving complexity bounds, and how termination and complexity results established for the TRS can be transferred back to the corresponding Hyrql program.

For example, the standard NOT gate is represented by the quantum TRS whose set of rewrite rules is {$NOT |0\rangle \to |1\rangle, NOT |1\rangle \to |0\rangle$}. The application of the NOT function symbol to $|0\rangle$ rewrites to $|1\rangle$. Similarly, the Hadamard gate $H$ can be defined using a superposition of terms {$H |0\rangle \to \frac{1}{\sqrt{2}} \cdot |0\rangle + \frac{1}{\sqrt{2}} \cdot |1\rangle, H |1\rangle \to \frac{1}{\sqrt{2}} \cdot |0\rangle - \frac{1}{\sqrt{2}} \cdot |1\rangle$}. The evaluation of a quantum term will follow a parallel strategy, similar to Hyrql operational semantics (Table 4), which reduces in parallel the distinct branches of a superposition, when possible (otherwise, the reduction will have an exponential blowup).

We claim that we can automatize the translation of any term of Hyrql to a corresponding TRS. This translation works as follows:

- Produce a set of rules, inductively on the syntax of the term;

- Yield a function symbol $f$ for the initial term $t$;

- When encountering $qcase x \{|0\rangle \to t_0, |1\rangle \to t_1\}$ (same for match), merge the two sets of rules generated for $t_0$ and $t_1$, while keeping track of which path was taken.

Coming back on Example 3, such an algorithm would generate the following rewrite rules:

$$ \left\{ \begin{array}{l} \text{Repeat } 0 \to [] \qquad \text{BQWalk } |0\rangle m \to |0\rangle :: \text{Repeat } m \\ \text{Repeat } S(m) \to |0\rangle :: \text{Repeat } m \qquad \text{BQWalk } |1\rangle 0 \to |1\rangle :: [] \\ \qquad \qquad \qquad \qquad \text{BQWalk } |1\rangle S(m) \to |1\rangle :: \text{BQWalk } (|-)m \end{array} \right\} $$

One can remark that this set of rules captures completely the behaviour of `bqwalk`, and they both compute the same function; furthermore, one reduction step for a given rewrite rule will correspond to $1 \le k \le |bqwalk|$ reduction steps in Hyrql. Therefore, a certificate on this TRS yields directly a certificate on the original term.

Now, it is possible to apply the tools we mentioned to the obtained TRS. In particular, we can use recursive path orderings [22] to show termination, coupled with quasi-interpretations [13] to get that this TRS terminates in time $O(n)$ for any input of size $n$. While such properties are not defined for quantum TRS, i.e., with superpositions and parallel reduction, they can be adapted to fit the quantum setting; a formal adaptation is left for future work. Altogether with Theorem 25, we can conclude that `bqwalk` can be compiled to a family of quantum circuits, whose size is polynomial in the size of the input.

Using the same ideas, we claim that we can describe a semantic-preserving translation algorithm from Hyrql to TRS, with no blowup on the termination complexity in either direction. Such work, along with a proper development of TRS in the quantum setting and an adaptation of existing techniques, would give a semi-automatized way to prove the feasibility/tractability of terms in Hyrql.

While this section was focused on termination and time complexity, some of the mentioned techniques also provide results to bound the space complexity of a TRS program [13]. Given a good definition of quantum space, this would make it possible to characterize quantum space complexities, and obtain bounds on the depth or width of the circuit.
References

1 Alastair A. Abbott, Julian Wechs, Dominic Horsman, Mehdi Mhalla, and Cyril Branciard. Communication through coherent control of quantum channels. *Quantum*, 4:333, September 2020. doi:10.22331/q-2020-09-24-333.

2 Thorsten Altenkirch and Jonathan Grattage. A functional quantum programming language. In *Logic in Computer Science, LICS'05*, pages 249-258. IEEE Computer Society, 2005. doi:10.1109/lics.2005.1.

3 Mateus Araújo, Fabio Costa, and Časlav Brukner. Computational advantage from quantum-controlled ordering of gates. *Phys. Rev. Lett.*, 113:250402, dec 2014. doi:10.1103/PhysRevLett.113.250402.

4 Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. *Theoretical Computer Science*, 236(1):133-178, 2000. doi:10.1016/S0304-3975(99)00207-8.

5 Martin Avanzini and Georg Moser. Dependency pairs and polynomial path orders. In *International Conference on Rewriting Techniques and Applications, RTA'09*, pages 48-62. Springer, 2009. doi:10.1007/978-3-642-02348-4_4.

6 Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, and Vladimir Zamdzhiev. Quantum expectation transformers for cost analysis. In Christel Baier and Dana Fisman, editors, *LICS '22: Symposium on Logic in Computer Science*, pages 10:1-10:13. ACM, 2022. doi:10.1145/3531130.3533332.

7 Patrick Baillot and Ugo Dal Lago. Higher-order interpretations and program complexity. *Information and Computation*, 248:56-81, 2016. doi:10.1016/j.ic.2015.12.008.

8 Henk Barendregt. The lambda calculus: its syntax and semantics. *Studies in logic and the foundations of Mathematics*, 1984. doi:10.1016/c2009-0-14341-6.

9 Kathleen Barsse, Romain Péchoux, and Simon Perdrix. A quantum programming language for coherent control, 2025. arXiv:2507.10466.

10 Charles H. Bennett and Gilles Brassard. Quantum cryptography: Public key distribution and coin tossing. *Theoretical Computer Science*, 560:7-11, 2014. doi:10.1016/j.tcs.2014.05.025.

11 Ethan Bernstein and Umesh Vazirani. Quantum Complexity Theory. *SIAM Journal on Computing*, 26(5):1411-1473, October 1997. doi:10.1137/S0097539796300921.

12 Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In *Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation*, PLDI '20, page 286-300. ACM, June 2020. doi:10.1145/3385412.3386007.

13 Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen. Quasi-interpretations a way to control resources. *Theoretical Computer Science*, 412(25):2776-2796, June 2011. doi:10.1016/j.tcs.2011.02.007.

14 Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. In Jakob Rehof, editor, *Formal Structures for Computation and Deduction (FSCD 2024)*, volume 299 of LIPIcs, pages 19:1-19:19, 2024. doi:10.4230/LIPIcs.FSCD.2024.19.

15 Kostia Chardonnet, Alexis Saurin, and Benoît Valiron. A Curry-Howard Correspondence for Linear, Reversible Computation. LIPIcs, Volume 252, CSL 2023, 252:13:1-13:18, 2023. doi:10.4230/LIPICS.CSL.2023.13.

16 Giulio Chiribella, Giacomo Mauro D'Ariano, Paolo Perinotti, and Benoît Valiron. Quantum computations without definite causal structure. *Phys. Rev. A*, 88:022318, Aug 2013. doi:10.1103/PhysRevA.88.022318.

17 Andrea Colledan and Ugo Dal Lago. Flexible type-based resource estimation in quantum circuit description languages. *Proc. ACM Program. Lang.*, 9(POPL), January 2025. doi:10.1145/3704883.

18 Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open quantum assembly language, 2017. arXiv:1707.03429.
19 Andrew W. Cross, Ali Javadi-Abhari, Thomas Alexander, Niel De Beaudrap, Lev S. Bishop, Steven Heidel, Colm A. Ryan, Prasahnt Sivarajah, John Smolin, Jay M. Gambetta, and Blake R. Johnson. OpenQASM 3: A broader and deeper quantum assembly language. *ACM Transactions on Quantum Computing*, 3(3):1–50, September 2022. doi:10.1145/3505636.

20 Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. Quantum implicit computational complexity. *Theor. Comput. Sci.*, 411(2):377–409, 2010. doi:10.1016/J.TCS.2009.07.045.

21 Kinnari Dave, Louis Lemonnier, Romain Péchoux, and Vladimir Zamdzhiev. Combining quantum and classical control: syntax, semantics and adequacy. In *Foundations of Software Science and Computation Structures, FoSSaCS 2025*, pages 155–175, Berlin, Heidelberg, 2025. Springer-Verlag. doi:10.1007/978-3-031-90897-2_8.

22 Nachum Dershowitz. Orderings for term-rewriting systems. *Theoretical computer science*, 17(3):279–301, 1982. doi:10.1016/0304-3975(82)90026-3.

23 Nachum Dershowitz. Termination of rewriting. *J. Symb. Comput.*, 3(1-2):69–115, February 1987. doi:10.1016/S0747-7171(87)80022-6.

24 Alejandro Díaz-Caro and Octavio Malherbe. Quantum control in the unitary sphere: Lambda-s1 and its categorical model. *Log. Methods Comput. Sci.*, 18(3), 2022. doi:10.46298/LMCS-18(3:32)2022.

25 Jörg Endrullis, Herman Geuvers, and Hans Zantema. *Degrees of Undecidability in Term Rewriting*, pages 255–270. Springer Berlin Heidelberg, 2009. doi:10.1007/978-3-642-04027-6_20.

26 Yuan Feng and Mingsheng Ying. Quantum Hoare logic with classical variables. *ACM Transactions on Quantum Computing*, 2(4):1–43, 2021. doi:10.1145/3456877.

27 Florent Ferrari, Emmanuel Hainry, Romain Péchoux, and Mário Silva. Quantum programming in polylogarithmic time. In *Mathematical Foundations of Computer Science, MFCS 2025*, volume 345 of *LIPIcs*, pages 47:1–47:17, 2025. doi:10.4230/LIPICS.MFCS.2025.47.

28 Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: a scalable quantum programming language. In *ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13*, pages 333–342. ACM, June 2013. doi:10.1145/2491956.2462177.

29 Emmanuel Hainry, Romain Péchoux, and Mário Silva. A programming language characterizing quantum polynomial time. In *Foundations of Software Science and Computation Structures, Fossacs 2023*, pages 156–175. Springer, April 2023. doi:10.1007/978-3-031-30829-1_8.

30 Emmanuel Hainry, Romain Péchoux, and Mário Silva. Branch sequentialization in quantum polytime. In Maribel Fernández, editor, *Formal Structures for Computation and Deduction, FSCD 2025*, volume 337 of *LIPIcs*, pages 22:1–22:22, 2025. doi:10.4230/LIPICS.FSCD.2025.22.

31 Vesa Halava, Tero Harju, Mika Hirvensalo, and Juhani Karhumäki. Skolem's problem - on the border between decidability and undecidability. Technical Report 683, Turku Center for Computer Science, 2005. URL: https://tucs.fi/publications/view/?pub_id=tHaHaHiKa05a.

32 Alexei Y. Kitaev. Quantum computations: algorithms and error correction. *Russian Mathematical Surveys*, 52(6):1191–1249, December 1997. doi:10.1070/rm1997v052n06abeh002155.

33 Emanuel Knill. Conventions for quantum pseudocode. Technical report, Los Alamos National Lab., 1996. arXiv:2211.02559.

34 Hlér Kristjánsson, Tatsuki Odake, Satoshi Yoshida, Philip Taranto, Jessica Bavaresco, Marco Túlio Quintino, and Mio Murao. Exponential separation in quantum query complexity of the quantum switch with respect to simulations with standard quantum circuits, 2024. arXiv:2409.18420.

35 Yves Lafont. Soft linear logic and polynomial time. *Theor. Comput. Sci.*, 318(1-2):163–180, 2004. doi:10.1016/J.TCS.2003.10.018.
36 Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In *Symposium on Principles of Programming Languages, POPL 2001*, pages 81–92, New York, NY, USA, January 2001. ACM. doi:10.1145/373243.360210.

37 Louis Lemonnier. *The Semantics of Effects : Centrality, Quantum Control and Reversible Recursion*. PhD thesis, Université Paris-Saclay, June 2024.

38 Jean-Yves Marion and Romain Péchoux. Sup-interpretations, a semantic method for static analysis of program resources. *ACM Trans. Comput. Logic*, 10(4), August 2009. doi:10.1145/1555746.1555751.

39 Georg Moser. *Proof Theory at Work: Complexity Analysis of Term Rewrite Systems*. Cumulative habilitation thesis, University of Innsbruck, 2009. arXiv:0907.5527.

40 Michael A. Nielsen and Isaac L. Chuang. *Quantum Computation and Quantum Information: 10th Anniversary Edition*. Cambridge University Press, June 2012. doi:10.1017/cbo9780511976667.

41 André Nies. *Computability and Randomness*. Oxford University Press, 01 2009. doi:10.1093/acprof:oso/9780199230761.001.0001.

42 Romain Péchoux. *Complexité implicite : bilan et perspectives*. Accreditation to supervise research, Université de Lorraine, October 2020. URL: https://hal.univ-lorraine.fr/tel-02978986.

43 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. Experimental superposition of orders of quantum gates. *Nature Communications*, 6(1), August 2015. doi:10.1038/ncomms8913.

44 Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. From symmetric pattern-matching to quantum control. In Christel Baier and Ugo Dal Lago, editors, *Foundations of Software Science and Computation Structures*, pages 348–364, Cham, 2018. Springer International Publishing. doi:10.1007/978-3-319-89366-2_19.

45 Peter Selinger. Towards a quantum programming language. *Mathematical Structures in Computer Science*, 14(4):527–586, August 2004. doi:10.1017/s0960129504004256.

46 Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. In Paweł Urzyczyn, editor, *Typed Lambda Calculi and Applications*, TLCA 2005, pages 354–368. Springer Berlin Heidelberg, 2005. doi:10.1007/11417170\_26.

47 Peter Selinger and Benoît Valiron. Semantic techniques in quantum computation. In Simon Gay and Ian Mackie, editors, *Quantum lambda calculus*, pages 135–172. Cambridge University Press, 2009. doi:10.1017/cbo9781139193313.005.

48 Peter W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. *SIAM Journal on Computing*, 26(5):1484–1509, 1997. doi:10.1137/S0097539795293172.

49 Márcio M. Taddei, Jaime Cariñe, Daniel Martínez, Tania García, Nayda Guerrero, Alastair A. Abbott, Mateus Araújo, Cyril Branciard, Esteban S. Gómez, Stephen P. Walborn, Leandro Aolita, and Gustavo Lima. Computational advantage from the quantum superposition of multiple temporal orders of photonic gates. *PRX Quantum*, 2:010320, Feb 2021. doi:10.1103/PRXQuantum.2.010320.

50 Peter van EMDE BOAS. *Machine Models and Simulations*, page 1–66. Handbook of Theoretical Computer Science. Elsevier, 1990. doi:10.1016/b978-0-444-88071-0.50006-0.

51 Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. Qunity: A unified language for quantum and classical computing. *Proc. ACM Program. Lang.*, 7(POPL), January 2023. doi:10.1145/3571225.

52 Toshiyuki Yamada. Confluence and Termination of Simply Typed Term Rewriting Systems. In Aart Middeldorp, editor, *Rewriting Techniques and Applications*, pages 338–352, Berlin, Heidelberg, 2001. Springer. doi:10.1007/3-540-45127-7_25.

53 Tomoyuki Yamakami. A Schematic Definition of Quantum Polynomial Time Computability. *The Journal of Symbolic Logic*, 85(4):1546–1587, December 2020. doi:10.1017/jsl.2020.45.
54 Mingsheng Ying. *Foundations of quantum programming*. Elsevier, 2024. doi:10.1016/C2014-0-02660-3.

55 Mingsheng Ying and Zhicheng Zhang. Verification of recursively defined quantum circuits, 2024. arXiv:2404.05934.

56 Charles Yuan, Agnes Villanyi, and Michael Carbin. Quantum control machine: The limits of control flow in quantum programming. *Proceedings of the ACM on Programming Languages*, 8(OOPSLA1):1–28, April 2024. doi:10.1145/3649811.

A Additional Material

► **Definition 29 (Size of a term).** Given a term $t$, its size, written $|t| \in \mathbb{N}$, is defined inductively as follows:

$$
\begin{align*}
|x| &\triangleq 1 & |0\rangle &\triangleq 1 & |1\rangle &\triangleq 1 & |\text{qcase } t\{0\to t_0, 1\to t_1\}| &\triangleq 1 + |t| + |t_0| + |t_1| \\
|c(t_1, \dots, t_n)| &\triangleq 1 + \sum_{i=1}^n |t_i| & |\text{match}_{1\le i\le n} t\{c_i(\vec{x}_i)\to t_i\}| &\triangleq 1 + |t| + \sum_{i=1}^n |t_i| \\
|\lambda x.t| &\triangleq 1 + |t| & |\text{letrec } f x = t| &\triangleq 1 + |t| & |t_1 t_2| &\triangleq |t_1| + |t_2| \\
|\sum_{i=1}^n \alpha_i \cdot t_i| &\triangleq 1 + \sum_{i=1}^n |t_i| & |\text{shape}(t)| &\triangleq 1 + |t|
\end{align*}
$$

► **Example 30 (Hybrid function — BB84 [10]).** Hyrql is able to use quantum and classical data simultaneously. For example, the well-known protocol BB84 [10], creating a quantum key from a classical key, can be implemented as follows:

$$
\begin{align*}
\text{not} &\triangleq \lambda q. \text{qcase } q \{ |0\rangle \rightarrow |1\rangle, |1\rangle \rightarrow |0\rangle \} \\
\text{cc} &\triangleq \lambda b. \lambda f. \lambda q. \text{match } b \{ 0 \rightarrow q, 1 \rightarrow f q \} \\
\text{op} &\triangleq \lambda q. \lambda n. \text{match } n \{ (x, h) \rightarrow cc h. \text{Had}(cc x \text{ not } q) \} \\
\text{keygen} &\triangleq \text{letrec } f l = \text{match } l \{ [ ] \rightarrow [ ], h :: t \rightarrow (\text{op } |0\rangle h) :: (f t) \}
\end{align*}
$$

The term `cc` applies a gate `f` conditionally with classical control on a bit `b`. The term `op` reads a pair `(x, h)`, and applies the `NOT` gate if `x = 1`, and then applies the `Hadamard` gate if `h = 1`. Finally, `keygen` generates the qubit list key.

► **Example 31 (Quantum Fourier Transform).** We can encode the well-known Quantum Fourier Transform (QFT) in our language, with however two points to notice:

■ As our natural numbers are defined recursively, defining phase gates is not direct. We thus assume that we are given a term $\phi$ such that $\phi n |0\rangle = |0\rangle$ and $\phi n |1\rangle = e^{i\pi/2^{n-1}} |1\rangle$.

■ We will use the syntactic sugar to split 2 qubits and rename them:

$$
\begin{align*}
\text{let } x \otimes y &= s \text{ int } \triangleq \text{match } s \{x \otimes y \to t\} \\
\text{cphase} &\triangleq \lambda x. \lambda n. \text{match } x \{c \otimes t \to \text{qcase } c \{ |0\rangle \to |1\rangle \otimes t, |1\rangle \to |0\rangle \otimes \phi n t \}\} \\
\text{rot} &\triangleq \text{letrec } f q = \lambda l. \lambda n. \text{match } l \left\{ \begin{array}{@{}l@{}}
    \text{let } q'' \otimes t' = f(q')(t)(S(n)) \text{ in } q'' \otimes (h' :: t') \\
    \text{rot}(h)(t)(S(S(0))) \text{ in } h' :: (f t')
  \end{array} \right\} \\
\text{rec} &\triangleq \text{letrec } f l = \text{match } l \{ [ ] \to [ ], h :: t \to \text{let } h' \otimes t' = \text{rot}(h)(t)(S(S(0))) \text{ in } h' :: (f t') \} \\
\text{append} &\triangleq \text{letrec } f l = \lambda x. \text{match } l \{ [ ] \to x :: [ ], h :: t \to h :: f t x \} \\
\text{swap} &\triangleq \text{letrec } f l = \text{match } l \{ [ ] \to [ ], h :: t \to \text{append}(f t) h \} \\
\text{qft} &\triangleq \lambda l. \text{swap}(\text{rec}(l))
\end{align*}
$$
For the sake of simplicity in the following typing trees, we may denote $;\vdash t : T$ for $\emptyset; \emptyset \vdash t : T$.

**Example 32.** As $|0\rangle, |1\rangle$ are pure values, then we get $|0\rangle \perp |1\rangle$ directly from the definition. This allows us to type $|\pm\rangle$:

$$ \frac{\overline{;\vdash |0\rangle : \text{Qbit}} (\text{ax}_0) \quad \overline{;\vdash |1\rangle : \text{Qbit}} (\text{ax}_1) \quad \frac{|\frac{1}{\sqrt{2}}|^2 + |\pm \frac{1}{\sqrt{2}}|^2 = 1}{;\vdash |\pm\rangle : \text{Qbit}} \quad |0\rangle \perp |1\rangle}{\text{sup}} $$

It is also easy to check that $|+\rangle \perp |-\rangle$:

$$ \langle |+\rangle, |-\rangle \equiv \frac{\frac{1}{\sqrt{2}} \frac{1}{\sqrt{2}} \delta_{|0\rangle,|0\rangle} - \frac{1}{\sqrt{2}} \frac{1}{\sqrt{2}} \delta_{|0\rangle,|1\rangle} + \frac{1}{\sqrt{2}} \frac{1}{\sqrt{2}} \delta_{|1\rangle,|0\rangle} - \frac{1}{\sqrt{2}} \frac{1}{\sqrt{2}} \delta_{|1\rangle,|1\rangle}}{\frac{1}{2} - \frac{1}{2}} = 0 $$

we can also type the Hadamard gate as follows:

$$ \frac{\overline{\emptyset; x : \text{Qbit} \vdash x : \text{Qbit}} \quad ;\vdash |+\rangle : \text{Qbit} \quad ;\vdash |-\rangle : \text{Qbit} \quad |+\rangle \perp |-\rangle}{\text{(qcase)}} \quad \frac{\overline{\emptyset; x : \text{Qbit} \vdash \text{qcase } x \{ |0\rangle \to |+\rangle, |1\rangle \to |-\rangle \}} : \text{Qbit}}{;\vdash \text{Had} : \text{Qbit} \to \text{Qbit}} \quad \text{(lbd)} $$

**Example 33.** The quantum switch from Example 2 can be typed by our language. For conciseness, we write $v = |0\rangle \otimes f(gt)$, $w = |1\rangle \otimes g(ft)$, $\Gamma = f : \text{Qbit} \to \text{Qbit}, g : \text{Qbit} \to \text{Qbit}$, $s = \text{match } q \{(c \otimes t) \to \text{qcase } c\{|0\rangle \to v, |1\rangle \to w\}\}$, $\Delta = c : \text{Qbit}, t : \text{Qbit}$ and $Q_2 = \text{Qbit} \otimes \text{Qbit}$. The orthogonality predicate $v \perp w$ is verified, as for any substitution of $f,g,t$, $\sigma(v) \rightsquigarrow |0\rangle \otimes v'$ and $\sigma(w) \rightsquigarrow |1\rangle \otimes w'$. Both terms have the same shape $(\otimes) \otimes (\otimes)$ and their inner product is zero. Note that we substitute by terminating terms, thus $f,g$ terminate and we can evaluate the inner product.

$$ \frac{\Gamma; c : \text{Qbit} \vdash c : \text{Qbit} \quad \Gamma; t : \text{Qbit} \vdash v : Q_2 \quad \Gamma; t : \text{Qbit} \vdash w : Q_2 \quad v \perp w}{\Gamma; \Delta \vdash \text{qcase } c \{ |0\rangle \to v, |1\rangle \to w \} : Q_2} \quad \Gamma; q : Q_2 \vdash q : Q_2 \\ \frac{\Gamma; q : Q_2 \vdash s : Q_2}{\Gamma; \emptyset \vdash \lambda q.s : Q_2 \to Q_2} \quad \frac{f : Q_2 \to Q_2; \emptyset \vdash \lambda g.\lambda q.s : (\text{Qbit} \to \text{Qbit}) \Rightarrow (Q_2 \to Q_2)}{;\vdash \text{QS} : (\text{Qbit} \to \text{Qbit}) \Rightarrow (\text{Qbit} \to \text{Qbit}) \Rightarrow (Q_2 \to Q_2)} $$

**Example 34.** Coming back on Example 9, the following typing tree derives typing for `len`, for a given type $A \in \mathbb{B}_C$, with the following notations to shorten the tree: $\Gamma_f = f : \text{list}(A) \Rightarrow \text{nat}$, $\Gamma_x = x : \text{list}(A)$, and $\Gamma = \Gamma_f, \Gamma_x, h : A, t : \text{list}(A)$. For conciseness, we also do not type $f$ and $t$ on the right part of the tree, which can both be typed as $\Gamma; \emptyset \vdash f : \text{list}(A) \Rightarrow \text{nat}$ and $\Gamma; \emptyset \vdash t : \text{list}(A)$, using $(\text{ax}_c)$ rules. We also drop the signature on constructors once they are fully applied.
$$
\begin{array}{c}
\begin{array}{c}
\frac{}{\Gamma_f, \Gamma_x; \emptyset \vdash x : \text{list}(A)} \quad \text{(ax)} \\
\frac{}{\Gamma_f, \Gamma_x; \emptyset \vdash 0^{\text{nat}} : \text{nat}} \quad \text{(cons)} \\
\frac{}{\Gamma; \emptyset \vdash S^{\text{nat} \to \text{nat}}(ft) : \text{nat}} \quad \text{(cons)} \\
\frac{}{\text{(match)}}
\end{array} \\
\begin{array}{c}
\frac{}{\Gamma_f, \Gamma_x; \emptyset \vdash \text{match} x \{[\,] \to 0, h :: t \to S(ft)\} : \text{nat}} \quad \text{(abs<sub>c</sub>)} \\
\frac{}{\Gamma_f; \emptyset \vdash \lambda x. \text{match} x \{[\,] \to 0, h :: t \to S(ft)\} : \text{list}(A) \Rightarrow \text{nat}} \quad \text{(rec)} \\
\frac{}{; \vdash \text{letrec} f x = \text{match} x \{[\,] \to 0, h :: t \to S(ft)\} : \text{list}(A) \Rightarrow \text{nat}}
\end{array}
\end{array}
$$

In particular, as *h* is not present in the syntax of *S(f t)*, we could not type *len* if *h* must be used linearly, thus if *A* ∈ *Q*.

► **Example 35.** Assuming we have a bit type bit for both constructors 0 :: bit and 1 :: bit, the typing of Example 30 can be derived, by combining most of the techniques exhibited from the previous examples, giving us ; ⊢ keygen : list(bit) ⇒ list(Qbit). Note that when we used programs in the syntax of other terms, such as Had, it is just notation to avoid rewriting the whole term.

B Proofs for Section 3.1

B.1 Intermediate results

In this subsection, we state some intermediate results and definitions that we will use through
the main proofs. Furthermore, we may use the notation {$x \to v$} for a substitution {$v/x$},
and define the support of a substitution Supp($\sigma$) as the set of variables $x_i$ such that there
exists $t_i$ with {$t_i/x_i$} $\in$ $\sigma$. When we do not need precision on the linearity of a functional
term, we may use $\to \triangleq \to \circ \cup \Rightarrow$. We also denote the free variables of $t$ by $\text{FV}(t)$.

**Proposition 10 (Weakening).** Let $\Gamma; \Delta \vdash t : T$ be a well-typed term. Then $\Gamma, \Gamma'; \Delta \vdash t : T$ holds for any context $\Gamma'$ compatible with $\Gamma, \Delta$.

**Proof.** This can be proven by induction on *t*, as the axiom rules satisfy this weakening property. Furthermore, the only variable removed from the non-linear context are bound variables, thus $\Gamma'$ stays untouched at each point. ◀

**Lemma 36.** Let $T \in \mathcal{T}$. Then, there exists a number $n \in \mathbb{N}$, types $T_i$ for $1 \le i \le n$, and a base type $B^i$ such that $T = T_1 \to \dots \to T_n \to B^i$.

**Proof.** Direct by induction on *T*: either it is a base type itself, thus we take *n* = 0; or
*T* = *T*₁ ↦ *T'*, then we use the induction hypothesis on *T'* and right associativity to
conclude.
◀

We also introduce an operator $\theta_p(t)$, called the *quantity*, which aims to measure the
amplitude of a pure term $p$ in a term $t$, e.g., a superposition.
**Definition 37.** Let $p$ be a pure term. We define the following map $\theta_p : \Lambda \to \mathbb{C}$ as follows:

$$
\begin{align*}
\theta_p(x) &\triangleq \delta_{p,x} \qquad \theta_p(|0\rangle) \triangleq \delta_{p,|0\rangle} \qquad \theta_p(|1\rangle) \triangleq \delta_{p,|1\rangle} \\
\theta_p(\mathit{qcase} t' \{ |0\rangle \to t_0, |1\rangle \to t_1 \}) &\triangleq \delta_{p,\mathit{qcase} p'} \{ |0\rangle \to t_0, |1\rangle \to t_1 \} \theta_{p'}(t') \\
\theta_p(c(t_1, \dots, t_n)) &\triangleq \delta_{p,c(p_1, \dots, p_n)} \times_{i=1}^n \theta_{p_i}(t_i) \\
\theta_p(\mathit{match}_{1 \le i \le n} t' \{ c_i(\vec{x_i}) \to t_i \}) &\triangleq \delta_{p,\mathit{match}_{1 \le i \le n} p'} \{ c_i(\vec{x_i}) \to t_i \} \theta_{p'}(t') \\
\theta_p(\lambda x.t) &\triangleq \delta_{p,\lambda x.t} \qquad \theta_p(\mathit{letrec} f x = t) \triangleq \delta_{p,\mathit{letrec} f x=t} \qquad \theta_p(t_1 t_2) \triangleq \delta_{p,p_1 p_2} \nu_{p_1,t_1} \nu_{p_2,t_2} \\
\theta_p(\sum_{i=1}^n \alpha_i \cdot t_i) &\triangleq \sum_{i=1}^n \alpha_i \cdot \theta_p(t_i) \qquad \theta_p(\mathit{shape}(t')) \triangleq \delta_{p,\mathit{shape}(p')} \nu_{p',t'}
\end{align*}
$$

We have used the notation $\delta_{p,t}$ for the Kronecker symbol, and $\nu_{p,t}$ for the equivalence Kronecker symbol, meaning $\nu_{p,t} = 1$ iff $p \equiv t$.

**Lemma 38.** Let $p$ be a pure term. Then $\theta_p(p) = 1$.

*Proof.* Proven by induction on $p$, direct by definition of the quantity.

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

**Lemma 39.** Let $p$ be a pure term and $t, t'$ be two terms of the language. If $t \equiv t'$, then $\theta_p(t) = \theta_p(t')$.

*Proof.* By induction on each rule defining $\equiv$ in Table 3; the transitive and reflexive case can be derived from this. The first two lines of rules are verified directly as $\mathbb{C}$ is a vectorial space. The three linearity rules also work by definition of summation and the linear constructs. Finally, we can prove the $C_\equiv$ case by doing an induction on the depth of $C_\equiv$, the base case being just $t \equiv t'$ and then obtaining the result by induction.

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

**Lemma 40.** Let $s, t$ be two pure terms. Then $\theta_s(t) = \nu_{s,t}$. Furthermore, if $s, t$ are values, then $\theta_s(t) = \delta_{s,t}$.

*Proof.* Note by Lemma 38, $\theta_s(s) = 1$. If $\theta_s(t) = 0$, then $s \not\equiv t$, else Lemma 39 would fail. Now, one can check by induction on $t$ that if $\theta_s(t) = 1$, then $s \equiv t$. This is done directly, mainly proving $\equiv$ using $C_\equiv$. The second part of the lemma is also obtained directly by induction of $t$, by looking at the definition of the quantity.

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

**Lemma 41.** Let $t$ be a term of the language. Suppose $t \not\equiv 0 \cdot t'$. Then $t$ has a canonical form $\sum_{i=1}^n \alpha_i \cdot t_i$, that is unique up to reordering and equivalence on the $t_i$.

*Proof.* Let us prove existence by induction on $t$.

- If $t = x, |0\rangle, |1\rangle, \lambda x.s, \mathit{letrec} f x = s, s_1 s_2$ or $\mathit{shape}(s)$, then $t$ is directly pure and $t \equiv 1 \cdot t$, which is a canonical form.

- Suppose $t = c(t_1, \dots, t_n)$. If we have any $t_i \equiv 0 \cdot t'_i$, then $t \equiv 0 \cdot c(t_1, \dots, t'_i, \dots, t_n)$. Therefore, we can apply the induction hypothesis on each $t_i$, meaning we have $t_i \equiv \sum_{j_i=1}^{n_i} \alpha_{j_i} \cdot t_{j_i}$. By developing $t$ under $\equiv$, we have $t \equiv \sum_{j_1=1}^{n_1} \dots \sum_{j_n=1}^{n_n} \alpha_{j_1} \dots \alpha_{j_n} \cdot c(t_{j_1}, \dots, t_{j_n})$. This can be seen as one big sum $\sum_{k=1}^{n_1 \dots n_k} \alpha_k \cdot c(t_1^k, \dots, t_n^k)$, where $\alpha_k = \alpha_{j_1} \dots \alpha_{j_n}$. In particular, $\alpha_k \not\equiv 0$ as each $\alpha_{j_i} \not\equiv 0$; and if $c(t_1^k, \dots, t_n^k) \equiv c(t_1^{k'}, \dots, t_n^{k'})$, then by Lemma 39, $\theta_{c(t_1^k, \dots, t_n^k)}(c(t_1^{k'}, \dots, t_n^{k'})) = 1$ as they are both pure, but by analyzing the formula, this implies $\theta_{t_i^k}(t_i^{k'}) = 1$, thus by Lemma 39, $t_i^k \equiv t_i^{k'}$. By induction hypothesis, this is not possible for all $1 \le i \le n$, therefore terms are pairwise not equivalent, which concludes.
- The same process can be done for $t = \mathbf{qcase} t' \{|0\rangle \to t_0, |1\rangle \to t_1\}$ or $t = \mathbf{match} t \{\dots\}$, as they have an identical behaviour to a constructor with one slot.

- Finally, suppose $t = \sum_{i=1}^n \alpha_i \cdot t_i$. Any $t_i \equiv 0 \cdot t'_i$ will be removed from the sum through $t+0 \cdot t' \equiv t$, then we can apply the i.h. on the remaining $t_i$. Finally, using distributivity, we can obtain a big sum $\sum_{k=1}^n \beta_k \cdot s_k$, where $s_k$ are pure terms. We can group $s_k$ that are equivalent, then remove any potential term with a 0 phase, and the term obtained satisfies the canonical form definition. Note that as $t \not\equiv 0 \cdot t'$, the sum obtained is actually well defined, in particular there is at least one term.

Unicity comes from our quantity function defined above. Suppose $t$ has two canonical forms $t = \sum_{i=1}^n \alpha_i \cdot t_i \equiv \sum_{j=1}^m \beta_j \cdot s_j$. As all $t_i$ are pure, for any $1 \le i_0 \le n$, $\theta_{t_{i_0}}(\sum_{i=1}^n \alpha_i \cdot t_i) = \sum_{i=1}^n \alpha_i \theta_{t_{i_0}}(t_i)$. By Lemma 40, $\theta_{t_{i_0}}(t_i) = \nu_{t_{i_0}, t_i}$, however the $t_i$ are not equivalent pairwise, thus $\theta_{t_{i_0}}(\sum_{i=1}^n \alpha_i \cdot t_i) = \alpha_{i_0} \ne 0$. However, by the same argument, $\theta_{t_{i_0}}(\sum_{j=1}^m \beta_j \cdot s_j) = \sum_{j=1}^m \beta_j \theta_{t_{i_0}}(s_j)$. If there is no $s_j \equiv t_{i_0}$, then Lemma 39 fails, thus there is at least one; and there cannot be more than one, else, $s_j \equiv t_{i_0} \equiv s_{j'}$, thus by transitivity $s_j \equiv s_{j'}$, which is not possible as this is a canonical form. Therefore, there exists $j_0$ such that $\theta_{t_{i_0}}(\sum_{j=1}^m \beta_j \cdot s_j) = \beta_{j_0}$; by Lemma 39, we obtain $\alpha_{i_0} = \beta_{j_0}$. Thus, any $t_i$ has a unique and distinct (as they are not equivalent) match in $s_j$, therefore $n \le m$. The same process can be done the other way around, so $m \le n$, thus $m = n$. So each sum contains the same number of elements, such that there is a map from $1, \dots, n$ to $1, \dots, n$ that associates $i$ with $j$ such that $t_i \equiv s_j$ and $\alpha_i = \beta_j$. Therefore, both sums are equal up to an equivalence on $t_i$ and permutation of the $t_i$. ◀

**Lemma 42.** Let $t$ be a well-typed term, suppose that $t$ terminates and has a canonical form $\sum_{i=1}^n \alpha_i \cdot s_i$. Then any element has the same shape, meaning $\mathbf{shape}(s_i) \rightsquigarrow^* v_i$, $\mathbf{shape}(s_j) \rightsquigarrow^* v_j$, and $v_i = v_j$ for any $i, j$.

**Proof.** By induction on the typing, and the constructed canonical form. Few points to note:

- for (qcase), as $t_0 \perp t_1$, in particular they have the same shape, thus any $s_i$ will reduce to a superposition of $t_0, t_1$;

- for (match), even if the inside argument is the superposition, by induction hypothesis, all elements have the same shape, thus in particular reduce to the same $t_i$.

- For (sup), $t_i \equiv t_j$, thus they have the same shape. ◀

Another process that we will do in proofs is completing canonical forms. Given two terms $s, t$ with canonical forms $\sum_{i=1}^n \alpha_i \cdot s_i$ and $\sum_{j=1}^m \beta_j \cdot t_j$, one can always create the set $S$, that contains all the $s_i, t_j$ such that they are pairwise non equivalent. Then, by adding $0 \cdot t'$, we can write each canonical form as $\sum_{k=1}^l \alpha_l \cdot w_l$ and $\sum_{k=1}^l \beta_k \cdot w_k$. This is not a canonical form as some phases are zero, but it is equivalent to the first canonical form, thus to $s, t$; and such shape is actually close enough to keep most existing results on the canonical form, such as normalization.

The following lemma abuses the operational semantics, by supposing that we have a rule allowing to reduce any term $\sum_{i=1}^n 0 \cdot t_i$ to $\sum_{i=1}^n 0 \cdot t'_i$ when $t_i \rightsquigarrow^? t'_i$. Our type system can easily be expanded to satisfy the properties; in fact, all the following results, i.e., subject reduction and confluence are proven by taking this case into account. Furthermore, we will later prove that any well-typed term cannot be expressed as so, thus this rule is only necessary for the proofs, and we have thus chosen to omit it.

**Lemma 43.** Let $t = \sum_{i=1}^n \alpha_i \cdot t_i$, suppose $t_i \rightsquigarrow^* v_i$. Then $t \rightsquigarrow^* \sum_{i=1}^n \alpha_i \cdot v_i$.
**Proof.** For each $t_i$ such that $t_i \equiv 0 \cdot s$, or such that $\alpha_i = 0$, we can remove it via (equiv), thus $t \equiv \sum_{k=1}^l \alpha_k \cdot t_k$. By writing each canonical form, up to completion, as $t_k \equiv \sum_{j=1}^m \beta_{k,j} \cdot s_j$, $s_j \rightsquigarrow s'_j$ and $\sum_{k=1}^l \alpha_k \cdot \beta_{k,j} = \gamma_j$:

$$t \equiv \sum_{j=1}^{m} \gamma_j \cdot s_j \equiv \sum_{j, \gamma_j \neq 0} \gamma_j \cdot s_j \rightsquigarrow \sum_{j, \gamma_j \neq 0} \gamma_j \cdot s'_j \equiv \sum_{j=1}^{m} \gamma_j \cdot s'_j \equiv \sum_{k=1}^{n} \alpha_k \cdot t'_k,$$

as the $s_j$ are pairwise not equivalent, either all $\gamma_j = 0$, or it is a canonical form. If the obtained form is a value, then we can stop here, and the result will be correct; even if $t_i$ is not a value, the non-value parts will still be canceled via (Equiv) at the end, as the reduction is deterministic. Else, we can apply (Can), and we can replace $0 \cdot s_j$ by $0 \cdot s'_j$. Furthermore, we can add back the removed terms from the beginning, adding back $t'_i$ instead of $t_i$, to get that $\sum_{k=1}^l \alpha_k \cdot t'_k \equiv \sum_{i=1}^n \alpha_i \cdot t'_i$. We conclude by (Equiv), and chaining this multiple times; such process terminates as the $t_i$ do terminate. ◀

## B.2 Proofs of confluence

**Lemma 44 (Equivalence preservation).** Let $s_1, s_2$ be two well-typed terms. Suppose $s_i \rightsquigarrow t_i$ for $i = 1, 2$. Then $t_1 \equiv t_2$.

**Proof.** We prove this result by induction of the sum of the depth of the derivation trees of $s_i \rightsquigarrow t_i$.

Consider the base case where both derivation trees have the same root. Apart from (Can) and (Shape$_s$), having the same root implies that $s_1 = s_2$, and as reduction is deterministic, $t_1 = t_2$, thus $t_1 \equiv t_2$. In the case of (Can), by Lemma 41, if one has a canonical form, then by $\equiv$ the second also has a canonical form, which is identical up to commutation and equivalence on the terms. Thus, $s_1 = \sum_{j=1}^n \alpha_i \cdot r_i$, and $s_2 = \sum_{j=1}^n \beta_i \cdot q_i$, where both sums are identical, up to commutation and each $q_i$ is equivalent to a $r_j$. We can apply the induction hypothesis on $q_i, r_j$, to get that the reduced terms are also equivalent, and up to commuting the terms back, we obtain the equivalence at the end. If not, both terms have 0 phase, and equivalence is direct from this. The same process can be applied for (Shape$_s$), but inside the **shape** construct, by Lemma 42, as it is a value.

Now, suppose that the trees do not have the same root. First, do not consider any (Shape) rule. Again, apart from (Can) and (Equiv), all left terms are pure, and by Lemma 39, no distinct rule can yield two equivalent terms. Suppose the first tree has a (Equiv) root, meaning:

$$\frac{s_1 \equiv q_1 \qquad q_1 \rightsquigarrow r_1 \qquad r_1 \equiv t_1}{s_1 \rightsquigarrow t_1} \quad (\text{Equiv})$$

By transitivity, $q_1 \equiv s_2$, thus we can apply the induction hypothesis on $q_1 \rightsquigarrow r_1$ and $s_2 \rightsquigarrow t_2$ to get $r_1 \equiv t_2$, and by transitivity, $t_1 \equiv t_2$. Same can be done for the right term.

Now, suppose the first tree has a (Can) root. As the right tree has neither a (Can) or (Equiv) root, it has a root with a pure term. This implies that all phases are not zero, and that $s_1$ is a canonical form. By uniqueness, $s_1 = 1 \cdot q_1$, with $q_1 \equiv s_2$, and $t_1 = 1 \cdot r_1$. We can apply the induction hypothesis on $q_1 \rightsquigarrow r_1$, $s_2 \rightsquigarrow t_2$, to get $t_1 \equiv t_2$ by transitivity of (Equiv). Same can be done for the right term.

The same process can be done for the (Shape) rules, but inside the **shape** construct. ◀
**► Theorem 11 (Confluence).** Given a well-typed term $t$, if there exist $t_1$ and $t_2$ such that $t \rightsquigarrow^* t_1$ and $t \rightsquigarrow^* t_2$, then there exist $t_3$ and $t_4$ such that $t_1 \rightsquigarrow^* t_3$, $t_2 \rightsquigarrow^* t_4$ and $t_3 \equiv t_4$.

*Proof.* Let us prove semi-confluence, which implies confluence. Let $t \rightsquigarrow t_1$ and $t \rightsquigarrow^* t_2$. If $t = t_2$, then result is direct; else $t \rightsquigarrow t_3 \rightsquigarrow^* t_2$. If $t_3 = t_2$, by the above result, $t_1 \equiv t_2$, which concludes. Else $t \rightsquigarrow t_3 \rightsquigarrow t_4 \rightsquigarrow^* t_2$. By the above result, $t_3 \equiv t_1$. And as $t_3 \rightsquigarrow t_4$, then $t \rightsquigarrow t_4$ by (Equiv). Therefore, $t \rightsquigarrow t_1 \rightsquigarrow t_4 \rightsquigarrow^* t_2$, and we conclude. ◀

## B.3 Proofs for Canonical Forms

**► Lemma 45.** Let $t$ be a term and $s$ be a pure term. Suppose $\theta_s(t) \neq 0$. Then $t$ has a unique canonical form.

*Proof.* Suppose $t \equiv 0 \cdot t'$. Then $\theta_s(t) = \theta_s(0 \cdot t') = 0$ by Lemma 39 and by definition of the quantity; this contradicts the initial hypothesis. We can then conclude by Lemma 41. ◀

**► Lemma 12 (Canonical form for typed terms).** Let $\Gamma; \Delta \vdash t : T$ be a well-typed term. Then $t$ has a canonical form $\sum_{i=1}^n \alpha_i \cdot p_i$, and this canonical form is unique, up to equivalence on each $p_i$ and term reordering. Furthermore, $\forall 1 \le i \le n$, $\Gamma; \Delta \vdash p_i : T$.

*Proof.* Let us first prove that for any well-typed $t$, there exists a pure term $s$ such that $\theta_s(t) \neq 0$; we then conclude by Lemma 45. By induction on $t$:

- If $t$ is pure, then take $s = t$ and result is direct;

- If the root is (cons), meaning $t = c(t_1, \dots, t_n)$, then by induction hypothesis, as $t_i$ is typed, there is a pure term $s_i$ such that $\theta_{s_i}(t_i) \neq 0$. We can take $s = c(s_1, \dots, s_n)$ and conclude.

- Same is done for (qcase) and (match).

- If the root is (equiv), $t \equiv t'$, we obtain the result by induction hypothesis on $t'$ and conclude by Lemma 39.

- If the root is (contr), then $t = \sigma(t')$; we can apply the induction hypothesis on $t'$ and take $s = \sigma(s')$ which will preserve $\sigma$.

- Finally, if the root is (sup), $t = \sum_{i=1}^n \alpha_i \cdot t_i$. By typing, $t_i$ is well-typed, thus by induction hypothesis and Lemma 45, $t_i$ has a canonical form. Furthermore, as $t_i \perp t_j$, each $t_i$ terminates, with $t_i \rightsquigarrow^* \sum_{j=1}^{n_i} \beta_{i,j} \cdot w_j^i$, being canonical forms. One can complement each canonical form to get $t_i \rightsquigarrow^* \sum_{j=1}^m \beta_{i,j} w_j$, where the $w_j$ are pure and distinct pairwise. We can thus use Lemma 43, and get that $t \rightsquigarrow^* \sum_{j=1}^m (\sum_{i=1}^n \alpha_i \beta_{i,j}) \cdot w_j$. If we suppose that $t \equiv 0 \cdot t'$, taking $t' = v$, by Theorem 11, $0 \cdot v \equiv \sum_{j=1}^m (\sum_{i=1}^n \alpha_i \beta_{i,j}) \cdot w_j$. By Lemma 39, $\theta_{w_j}(0 \cdot v) = 0 = \sum_{i=1}^n \alpha_i \beta_{i,j}$. One can check that by definition of $t_i \perp t_j$, the rows $(\beta_{i,1}, \dots, \beta_{i,n})$ are orthogonal, thus this would imply that $\alpha_i = 0$, which contradicts the hypothesis of (sup). Therefore, $t \not\equiv 0 \cdot t'$, by Lemma 41, $t$ has a canonical form $\sum_{k=1}^l \gamma_k \cdot u_k$, and take $s = u_1$ to conclude.

Finally, one can remark that by construction of the canonical form in Lemma 41, along with an induction on typing, the pure terms obtained are well-typed; such result is possible as the canonical form is unique, thus the one that we exhibited will match. ◀

## B.4 Proofs of progress

**► Lemma 46.** Let $t$ be a well-typed pure term of type $B^l$, and $v$ be a value. We suppose that $t \equiv v$, then $t$ is a value.
**Proof.** As $t$ is pure, $\theta_t(v) = \theta_t(t) = 1$. By definition of the quantity, it is easy to check that $\theta_t(v) = 1$ implies that $t$ is a value too, thus one can conclude. ◀

► **Lemma 47.** Let $t$ be a well-typed term of type $T_1 \to T_2$. Then its canonical form is $1 \cdot t'$.

**Proof.** Direct by the way canonical forms are generated in Lemma 41, and by typing of the different constructs. ◀

► **Theorem 13 (Progress).** Let $\emptyset; \emptyset \vdash t : T$ be a closed term, either $t$ is equivalent to a value, or $t$ reduces.

**Proof.** We prove this result by induction on the typing of $t$. First, let us consider that $t$ is a pure term.

- The rules (ax), ($\alpha x_c$) do not derive a closed term.

- The rules ($\alpha x_0$), ($\alpha x_1$) yield directly a value.

- If the root is (qcase), then $t = \mathbf{qcase} s \{ |0\rangle \to t_0, |1\rangle \to t_1 \}$, with $\emptyset; \emptyset \vdash s : \mathbf{Qbit}$. Either $s \rightsquigarrow s'$ and $t \rightsquigarrow \mathbf{qcase} s' \{ |0\rangle \to t_0, |1\rangle \to t_1 \}$ through (E); or $s \equiv v$, which by Lemma 46 indicates that $s$ is a pure value, thus $s = |i\rangle$. In any case, we can reduce through (Qcase$_i$) for $i = 0, 1$.

- Suppose $t$ is typed with (cons), namely $\emptyset; \emptyset \vdash c(t_1, \dots, t_n) : B$. This implies $\emptyset; \emptyset \vdash t_i : B_i$, thus we can apply the induction hypothesis on $t_i$. If each $t_i \equiv v_i$, then $t \equiv c(v_1, \dots, v_n)$ through $C_\equiv$, which is a value. Else, we take the first $t_i$, starting from the right, such that $t_i \rightsquigarrow t'_i$, and then $t \rightsquigarrow c(t_1, \dots, t'_i, \dots, t_n)$ by (E).

- If the root is (match), then $t = \mathbf{match} s \{ c_1(\vec{x}_1) \to t_1, \dots, c_n(\vec{x}_n) \to t_n \}$, with $\emptyset; \emptyset \vdash s : B$. Either $s \rightsquigarrow s'$ and $t \rightsquigarrow \mathbf{match} s' \{ \dots \}$ through (E); or $s \equiv v$, which by Lemma 46 indicates that $s$ is a pure value, thus $s = \bar{c}(v_1, \dots, v_m)$. As $s$ is of type $B$, then $\bar{c} \in \text{Cons}(B)$, thus $\bar{c} = c_i$ and $t \rightsquigarrow t_i$ through (Match).

- The rules (abs), ($\text{abs}_c$) and (rec) yield directly a value.

- Suppose the root of the derivation is (app), meaning $t = t_1 t_2$. By typing, $t_1, t_2$ are also closed terms and the induction hypothesis can be applied. If $t_2 \rightsquigarrow t'_2$, then $t \rightsquigarrow t_1 t'_2$ by (E). Else, $t_2 \equiv v_2$. If $t_1 \rightsquigarrow t'_1$, then $t_1 v_2 \rightsquigarrow t'_1 v_2$ by (E), and as $t \equiv t_1 v_2$, then $t \rightsquigarrow t'_1 v_2$ by (Equiv). Else, $t_1 \equiv v_1$. By Lemma 47, as $t_1$ has a functional type, then its canonical form consists of one pure term; as $v_1$ has the same canonical form by unicity, this term is a value too. Thus, $t_1 \equiv 1 \cdot v \equiv v$. Now, the only closed, well-typed values of type $C \Rightarrow T$ or $T \dashv T'$ are either $\lambda x.t'$, and as $(\lambda x.t') v_2 \rightsquigarrow \sigma(t')$ via (Lbd), then $t \rightsquigarrow \sigma(t')$ via (Equiv); or $\text{letrec} f x = t'$ and as $(\text{letrec} f x = t') v_2 \rightsquigarrow \sigma(t')$ via (Rec), then $t \rightsquigarrow \sigma(t')$ via (Equiv).

- The rule (sup) does not derive a pure term.

- Suppose the root is (shape), meaning $t = \mathbf{shape}(s)$, with $\emptyset; \emptyset \vdash s : B^|$. Note that $s$ is actually closed because its linear and non-linear context are joined in the non-linear context of $t$ which is empty. Then either $s \rightsquigarrow s'$ and $t \rightsquigarrow \mathbf{shape}(s')$ via (E); or $s \equiv v$. Either $v = |i\rangle$, and $t$ reduces through (Shape$_i$) and (Equiv); or $v = c(v_1, \dots, v_n)$ and $t$ reduces through (Shape$_c$) and (Equiv); or $v$ is a summation, as it is well-typed it has a canonical form $w$, and by transitivity $t \equiv w$, thus $t$ reduces through (Shape$_s$) and (Equiv). Any other value cannot be typed with a type $B^|$.

- Suppose the root of the derivation is (equiv), namely we have $t' \equiv t$. By hypothesis, $t$ is closed and thus $t'$ is too. Therefore, either $t' \equiv v$ and by transitivity of $\equiv$, $t \equiv v$; else $t' \rightsquigarrow t''$ and then $t \rightsquigarrow t''$ by (Equiv).

- The rule (contr) does not derive a closed term.
■ Finally, the rule (contr) cannot yield a closed term.

Now, let $t$ be a well-typed closed term; let us consider its canonical form $t' = \sum_{i=1}^{n} \alpha_i \cdot t_i$. If $t'$ is a value, then $t$ is equivalent to a value, and we conclude. Else, any term $t_i$ verifies $t_i \rightsquigarrow? t'_i$ for a given $t'_i$, by definition, and thus $t' \rightsquigarrow \sum_{i=1}^{n} \alpha_i \cdot t'_i$ by (Can), and thus $t \rightsquigarrow \sum_{i=1}^{n} \alpha_i \cdot t'_i$ by (Equiv), which concludes. ◀

## B.5 Proofs for Subject Reduction

► **Lemma 48 (Substitution lemma).** *The two following properties hold:*

- If $\Gamma, x : T'; \Delta \vdash t : T, \Gamma; \emptyset \vdash t' : T'$ and $\sigma = \{x \to t'\}$, then $\Gamma; \Delta \vdash \sigma(t) : T$.

- If $\Gamma; \Delta, x : T' \vdash t : T, \Gamma; \Delta' \vdash t' : T'$ and $\sigma = \{x \to t'\}$, then $\Gamma; \Delta, \Delta' \vdash \sigma(t) : T$.

*Proof.* We prove this by induction on the typing tree of $t$. For the first property:

- Suppose the root is $(\mathrm{ax})$, meaning $\Gamma, x : T'; y : T \vdash y : T$, then one can check that we can also type directly $\Gamma; y : T \vdash y : T$, and by definition $\sigma(y) = y$ as $y \notin \mathrm{Supp}(\sigma)$, which concludes.

- Suppose the root is $(\mathrm{ax}_c)$, then either $t = y$ with $y \neq x$, and the same process can be done as above. Else, we have $\sigma(t) = \sigma(x) = t'$, which concludes by the typing of $t'$.

- If the rules are $(\mathrm{ax}_0)$ or $(\mathrm{ax}_1)$, then again $\sigma(t) = t$ and we can derive the typing of $t$ with $\Gamma$ instead of $\Gamma, x : T'$.

- Suppose the root is $(\mathrm{qcase})$, thus $t = \mathrm{qcase} t' \{ |0\rangle \to t_0, |1\rangle \to t_1 \}$. By induction hypothesis, $x$ is removed from the context of $t', t_0, t_1$, thus we conclude by typing $\sigma(t) = \mathrm{qcase} \sigma(t') \{ |0\rangle \to \sigma(t_0), |1\rangle \to \sigma(t_1) \}$.

- Suppose the rule is $(\mathrm{cons})$, meaning $\Gamma, x : T'; \Delta_i \vdash t_i : A_i$; by i.h. $\Gamma; \Delta_i \vdash \sigma(t_i) : A_i$, and thus we can type $\Gamma; \Delta \vdash c(\sigma(t_1), \dots, \sigma(t_n)) : B$, which concludes.

- Suppose the rule is $(\mathrm{match})$, the same process can be done as for $(\mathrm{qcase})$, by remarking that $x$ cannot be a bound variable of a $t_i$, else typing could not happen.

- Suppose the root is $(\mathrm{abs})$, thus we have $\Gamma, y : T''; \Delta, x : T \vdash t : T'$; by i.h. $\Gamma; \Delta, x : T \vdash \sigma(t) : T'$, thus by $(\mathrm{abs})$ we can type $\Gamma; \Delta \vdash \lambda x.\sigma(t) : T \to T'$, which concludes as $\lambda x.\sigma(t) = \sigma(\lambda x.t)$ as $x \notin \mathrm{Supp}(\sigma)$.

- The same process can be done for $(\mathrm{abs}_c)$: we have $\Gamma, y : T'; \Delta \vdash \lambda x.t : C \Rightarrow T$, thus we can apply the induction hypothesis to $\Gamma, x : C, y : T'; \Delta \vdash t : T$ as $x \neq y$, which gives $\Gamma, x : C; \Delta \vdash \sigma(t) : T$, and we can conclude.

- Suppose the root is $(\mathrm{rec})$, then the same process as for $(\mathrm{abs}_c)$ can be applied.

- Suppose the root is $(\mathrm{app})$, meaning we have $\Gamma, x : B^l''; \Delta \vdash t_1 : B^l \to B^l'$ and $\Gamma, x : B^l''; \Delta' \vdash t_2 : B^l \to B^l'$; by i.h. we have $\Gamma; \Delta \vdash \sigma(t_1) : B^l \to B^l'$ and $\Gamma; \Delta' \vdash \sigma(t_2) : B^l$, and thus by $(\mathrm{app})$ we can type $\Gamma; \Delta \vdash \sigma(t_1)\sigma(t_2) : B^l'$ which concludes.

- The same can be done for $(\mathrm{app}_c)$.

- Suppose the root is $(\mathrm{sup})$, meaning we have $\Gamma, x : T'; \Delta \vdash t_i : T$. By induction hypothesis, we get $\Gamma; \Delta \vdash \sigma(t_i) : T$, and by definition of $\perp, t_i \perp t_j$ implies $\sigma(t_i) \perp \sigma(t_j)$, and thus we can type by $(\mathrm{sup})$ $\Gamma; \Delta \vdash \sum_{i=1}^n \alpha_i \cdot \sigma(t_i) : T$, which concludes by the action of $\sigma$ on superpositions.

- Suppose the root of the derivation is $(\mathrm{shape})$, first remark that $x$ belongs to the $\Gamma$ part, because it has no marker around it; thus we have $\Gamma, x : T'; \Delta \vdash t : B^l$, thus by i.h. $\Gamma; \Delta \vdash \sigma(t) : B^l$, and we can type by $(\mathrm{shape}) \Gamma, [\Delta]; \emptyset \vdash \mathrm{shape}(\sigma(t)) : \mathrm{shape}(B^l)$, which concludes.

- Suppose the root is $(\mathrm{contr})$, meaning we have $\Gamma, z : T', [x : B^l]; \Delta, y : B^l \vdash t : T$. Again, as $z$ comes with no marker and thus $z \neq x$, which means that we can treat the case as before, with a non-linear context $\Gamma, [x : B^l]$, and conclude.
Suppose the root is (equiv), thus $\Gamma, x : T'; \Delta \vdash t : T$; by i.h. $\Gamma; \Delta \vdash \sigma(t) : T$. One can check that if $t \equiv t'$, then $\sigma(t) \equiv \sigma(t')$, which concludes.

A similar process can be done to prove the second property. It differs only by the fact that $x$ is now present in only one subterm context; for the other subterm, while some $x$ may be present by a **shape** construct, replacing it with a well-typed value of same type, one can rewrite the typing tree with the new term (possibly by remodeling the (contr) rules), and conclude. Else, we have directly $\sigma(t) = t$, thus typing is direct. ◀

**Corollary 49.** Let $\Gamma, x_1 : T_1, \dots, x_m : T_m; \Delta, x_{m+1} : T_{m+1}, \dots, x_n : T_n \vdash t : T$ be a well-typed term. Then, for any substitution $\sigma$ such that for all $1 \le i \le n$, $x_i \in \text{Supp}(\sigma)$, $\Gamma; \Delta_i \vdash \sigma(x_i) : T_i$, we have $\Gamma; \Delta, \Delta_1, \dots, \Delta_n \vdash \sigma(t) : T$.

**Proof.** Direct by induction on $n$: the case $n=1$ is simply the above lemma, and for $n=k+1$, any substitution $\sigma$ can be written as $\sigma = \sigma' \circ \tau$ with $\tau = \{x_1 \to \sigma(x_1)\}$; $\tau(t)$ is typable by the above lemma and removes $x_1 : A_1$ from the context, and then $\sigma'(\tau(t))$ concludes by induction hypothesis. ◀

**Definition 50.** Let $\Gamma; \Delta \vdash t : T$ be a well-typed term. We say that $t$ types and terminates, written t.a.t., if $t \rightsquigarrow t_1 \dots \rightsquigarrow t_k \rightsquigarrow v$, $\Gamma; \Delta \vdash t_i : T$, $\Gamma; \Delta \vdash v : T$.

**Lemma 51.** Let $(t_i)_{1 \le i \le n}$ be well-typed terms such that $\forall i \ne j, t_i \perp t_j$. Let $s = \sum_{i=1}^n \alpha_i \cdot t_i$, and $t = \sum_{i=1}^n \beta_i \cdot t_i$ such that $s, t$ are t.a.t. and $\sum_{i=1}^n \alpha_i \beta_i^* = 0$. Then $s \perp t$.

**Proof.** As $t_i \perp t_j$, each $t_i$ reduces to a canonical form. Let us write them up to completion as $t_i \rightsquigarrow^* \sum_{j=1}^m \gamma_{ij} \cdot v_j$. By Lemma 43, $s \rightsquigarrow^* \sum_{j=1}^m (\sum_{i=1}^n \alpha_i \gamma_{ij}) \cdot v_j$, and $t \rightsquigarrow^* \sum_{j=1}^m (\sum_{i=1}^n \beta_i \gamma_{ij}) \cdot v_j$. By definition, this is a quasi canonical form, as some phases may be zero, but $v_j$ are two by two distinct; proving the orthogonality condition on this will imply orthogonality for the exact canonical form. First, it is easy to see that they all have the same shape, as $t_i$ are orthogonal, thus have the same shape. Compiling the inner product gives the following:

$$ \sum_{j=1}^{m} \sum_{j'=1}^{m} (\sum_{i=1}^{n} \alpha_i \gamma_{ij})(\sum_{i=1}^{n} \beta_i \gamma_{ij'}) \delta_{v_j, v_j'} = \sum_{1 \le i, i' \le n} \alpha_i \beta_i^* \sum_{j=1}^{m} \gamma_{ij} \gamma_{ij'}^* = \sum_{1 \le i, i' \le n} \alpha_i \beta_i^* \delta_{i, i'} = 0 $$

where the second equality is obtained by developing each sum, and the third by definition of $t_i \perp t_j$, and we conclude by the condition on $\alpha_i, \beta_i$. ◀

**Lemma 52.** Let $(t_i)_{1 \le i \le n}$, $(t'_i)_{1 \le i \le n}$ such that $\forall ij, t_i \perp t'_j$. Then for any $\alpha_i, \beta_i$, $\sum_{i=1}^n \alpha_i \cdot t_i \perp \sum_{i=1}^n \beta_i \cdot t'_i$.

**Proof.** Consider $(\tilde{t}_i)_{1 \le i \le 2n}$ where $\tilde{t}_i = t_i$ for $1 \le i \le n$, and $\tilde{t}_i = t'_i$ for $n < i \le 2n$, and apply Lemma 51. ◀

**Lemma 53.** Let $\Gamma; \Delta \vdash t : T$ be a pure term. Then we have the following typing tree:

$$ \begin{array}{c} \overline{\Gamma_0; \Delta \vdash s : T} (r) \\ \frac{\Gamma_1; \Delta \vdash \sigma_1(s) : T}{\vdots} (\text{contr}) \\ \overline{\Gamma_n; \Delta \vdash \sigma_n(s) : T} (\text{contr}) \end{array} $$

where $n \ge 0$, each $\Gamma_n = \Gamma$, $\sigma_n(s) = t$, $r$ is neither (contr) nor (equiv), and each $\Gamma_i$, respectively $\sigma_i$, contains one less marked variable, contains one more mapping, as per (contr).
**Proof.** Let $s$ be a pure term, and $\Gamma; \Delta \vdash t : T$ be any term. We prove by induction on typing of $t$ that if $\theta_s(t) \neq 0$, then $s$ satisfies the property of the lemma.

■ (ax): $t = x, \theta_s(t) \neq 0 \implies s = x$, and we can type $s$ directly.

■ ($\text{ax}_c$), ($\text{ax}_0$) and ($\text{ax}_1$) are obtained similarly.

■ (qcase): $t = \mathbf{qcase} r \{|0\rangle \to t_0, |1\rangle \to t_1\}, \theta_s(t) \neq 0 \implies s = \mathbf{qcase} q \{|0\rangle \to t_0, |1\rangle \to t_1\} \wedge r \equiv q$ by Lemma 40 as $q$ is pure. We can type $q$ via (equiv) by typing $r$ first, and then type $s$ via (qcase).

■ (cons): $t = c(t_1, \dots, t_n)$, non-zero quantity implies $s = c(s_1, \dots, s_n)$ with $s_i \equiv t_i$. We can type $t_i$ by the typing of $t$, then $s_i$ via (equiv), then $s$ via (cons).

■ (match): same as for (qcase).

■ (abs), ($\text{abs}_c$), (rec): same as (ax).

■ (app): this implies $t = t_1 t_2$, $s = s_1 s_2$, with $s_i \equiv t_i$, thus we type $s_i$ through (equiv) and conclude.

■ ($\text{app}_c$): same as (app).

■ (sup): $t = \sum_{i=1}^n \alpha_i \cdot t_i, \theta_s(t) = \sum_{i=1}^n \alpha_i \theta_s(t_i)$. As $\theta_s(t) \neq 0$, then there is $1 \le i \le n$ such that $\theta_s(t_i) \neq 0$. We can apply the induction hypothesis on $t_i$, as it has the same context and type as $t$.

■ (shape): $t = \mathbf{shape}(r)$, $s = \mathbf{shape}(q)$ and $q \equiv r$, thus we type $q$ through (equiv) and conclude.

■ (equiv): $t \equiv t', \theta_s(t) = \theta_s(t)' \neq 0$ through Lemma 39, and we apply i.h. on $t'$ as it has the same context and type.

■ (contr): $t = \sigma(r)$. We can apply the induction hypothesis on $r$, then reapply (contr) on the alternative tree.

Now, we can conclude as by Lemma 38, $\theta_s(s) = 1$; and any obtained tree satisfies the hypothesis. ◀

**Lemma 54.** Let $\emptyset; x : B^| \vdash s : B^|'$, $\sigma_v = \{x \to v\}$, $\emptyset; \emptyset \vdash v : B^|$, $\emptyset; \emptyset \vdash v' : B^|$ such that $v \perp v'$ and $s$ t.a.t. . We also suppose that any term $t$ that terminates in less steps than $s$ is also t.a.t. . Then $\sigma_v(s) \perp \sigma_{v'}(s)$.

Something that we can note is that given $s \rightsquigarrow^* \alpha \cdot |0\rangle + \beta \cdot |1\rangle$, then $\mathbf{qcase} s \{|0\rangle \to t_0, |1\rangle \to t_1\}$ will not always reduce to $\alpha \cdot t_0 + \beta \cdot t_1$, as ($C_\equiv$) requires a pure term, which is not guaranteed for $s$. However, we will have $\mathbf{qcase} s \{|0\rangle \to t_0, |1\rangle \to t_1\} \rightsquigarrow^* \alpha \cdot s_0 + \beta \cdot s_1$, where $t_i \rightsquigarrow^* s_i$. In particular, proving results of orthogonality between such terms will guarantee orthogonality between the $t_i$. Same goes for match.

**Proof.** By induction on the typing of $s$:

■ (ax) gives the desired result directly;

■ ($\text{ax}_c$), ($\text{ax}_0$) and ($\text{ax}_1$) have an empty linear context;

■ (qcase): $s = \mathbf{qcase} t \{|0\rangle \to t_0, |1\rangle \to t_1\}$; as $s$ terminates, so does $t$, in less steps than $s$, thus $t$ reduces to a well-typed value by hypothesis. Therefore, either $\emptyset; x : B^| \vdash t : \mathbf{Qbit}$; the only pure closed values of type $\mathbf{Qbit}$ are $|0\rangle$ and $|1\rangle$, thus $\sigma_v(t) \rightsquigarrow^* \alpha \cdot |0\rangle + \beta \cdot |1\rangle$, $\sigma_{v'}(t) \rightsquigarrow^* \gamma \cdot |0\rangle + \delta \cdot |1\rangle$, and by orthogonality $\alpha\gamma^* + \beta\delta^* = 0$. By definition, $\sigma_v(s) \rightsquigarrow^* \alpha \cdot t_0 + \beta \cdot t_1$, $\sigma_{v'}(s) \rightsquigarrow^* \gamma \cdot t_0 + \delta \cdot t_1$, which are well-typed as $s$ is t.a.t., and we can conclude by Lemma 51. Else, $\sigma_v(t) = t$, thus $t \rightsquigarrow^* \alpha \cdot |0\rangle + \beta \cdot |1\rangle$, $\sigma_v(s) \rightsquigarrow^* \alpha \cdot \sigma_v(t_0) + \beta \cdot \sigma_v(t_1)$. In particular, $t_0 \perp t_1$, thus $\sigma_v(t_i) \perp \sigma_{v'}(t_{i-1})$, and $\sigma_v(t_i) \perp \sigma_{v'}(t_i)$ by induction hypothesis, thus we conclude by Lemma 52, as the obtained summation is t.a.t. as a reduced of $s$.

■ (cons): there is $1 \le i \le n$ with $\emptyset; x : B^| \vdash t_i : B^|_i$. As one coordinate is orthogonal and the others are identical, orthogonality is verified for the whole term.
(match): same as for (qcase). The only difference is that $\sigma(t)$ will reduce to a linear combination of same constructor, thus $\sigma_v(s) \rightsquigarrow \sum_{j=1}^m \beta_j \cdot \sigma_{w_j}(t_i)$, where $w_j \perp w'_j$, and the result is direct by induction hypothesis and by concluding with Lemma 52.

(abs), (abs_c), (rec) do not yield a term of type $B^|\rangle$.

(app): by typing, reduction of $t_1t_2$ implies that $t_1$ reduces too to a well-typed closed value, i.e., either $\lambda x.t$ or letrec. Furthermore, by typing, either $x$ is in the context of $t_1$, thus of $t$, or in the context of $t_2$, thus of $v$. In any case, by joining all substitutions, we reach a point where $s \rightsquigarrow^* \tilde{\sigma}(t)$, and we can apply the i.h. on $t$, as it is t.a.t. as a reduced from $s$. Same goes for (app_c).

(sup): all $t_i$ have the $x$ in the context, thus $\sigma_v(t_i) \perp \sigma_{v'}(t'_i)$, and $\sigma_v(t_i) \perp \sigma_{v'}(t_j)$ for $i \neq j$ as $t_i \perp t_j$, thus we conclude by Lemma 52, as we apply the lemma on $s$, which is t.a.t. itself.

(shape): no linear context.

(equiv): apply the hypothesis on $t$, then via (Equiv) we can obtain a reduction for $s$.

(contr): just an alpha-renaming of a classical variable, does not disturb the previous proofs. ◀

**Lemma 55 (Strong Subject Reduction).** Let $\Gamma; \Delta \vdash t : T$ be a well-typed term, such that $t$ terminates in $k$ steps. Then $t$ t.a.t. .

**Proof.** This is proven by induction on the depth of termination of $t$. Let us first prove that $t$ reduces to well-typed terms. If $k=0$, the result is direct; suppose $k=k'+1$, thus $t \rightsquigarrow t' \rightsquigarrow \leq_k' v$. We will prove that $t$ t.a.t. by induction on the derivation of $\rightsquigarrow$. In most cases, we obtain that $t'$ is well-typed, which implies directly that $t$ t.a.t. by induction hypothesis on $t'$.

First, note that apart from (Can) and (Equiv), left terms are pure, thus we can apply Lemma 53 to gain a term with no (equiv) rule. Now, let us first suppose that there is no (contr) rule near the end of the typing tree.

(Qcase₀): the only non (contr) and (equiv) rule typing this syntax is (qcase), thus $\Delta = \Delta_1, \Delta_2$ with $\Gamma; \Delta_1 \vdash |0\rangle : Q$ bit and $\Gamma; \Delta_2 \vdash t_0 : Q$. Again, as $|0\rangle$ is pure, the only no (contr) and (equiv) rule typing $|0\rangle$ is $(\alpha_0)$. Therefore, $\Delta_1 = \emptyset$, and we can conclude by typing of $t_0$.

(Qcase₁): same as above.

(Match): the root of typing is (match), thus $\Delta = \Delta_1, \Delta_2$, with $\Gamma; \Delta_1 \vdash c_i^{s_i}(p_v^1, \dots, p_v^{n_i}) : B$ and $\Gamma; \vec{y}_i : \vec{C}_i; \Delta_2, \vec{z}_i : \vec{Q}_i \vdash t_i : B^|\rangle$. Again, by typing as the $v_i$ are pure, this gives us $s_i = B_1^|\rangle, \dots, B_n^|\rangle \to B$, and $\Gamma; \Delta_i^c \vdash p_v^i : B_i^|\rangle$, with $\Delta_1 = \Delta_1^c, \dots, \Delta_{n_i}^c$. As $\vec{x}_i = \vec{y}_i, \vec{z}_i$, we conclude using Corollary 49.

(Lbd) : If the root is (app), then $\Delta = \Delta_1, \Delta_2, \Gamma; \Delta_1 \vdash \lambda x.s : T' \to T$ and $\Gamma; \Delta_2 \vdash v : T'$. Typing of $\lambda x.s$ implies $\Gamma; \Delta_1, x : T' \vdash s : T'$, and thus by substitution lemma on $\sigma(s)$ we conclude. The same process can be done if the root is (app_c).

(Rec) is identical to (Lbd), up to some small tweaks.

(Can) : we consider an alternative typing tree where all equivalence relations are at the end, as we make them commute with summation, qcase, match and constructors. Therefore, we have $t \equiv s$, where $s$ has no (equiv) rule near the end. If $s$ is pure, then $t = 1 \cdot s$ (by quantity), by i.h. this reduces to $1 \cdot s'$ where $s'$ is well-typed, and using (equiv) we can type $1 \cdot s'$. Else, $s$ is not pure. Let us first prove that given two well-typed closed terms $s, t$ such that $s \perp t$ and that they terminate, reducing to well-typed closed value, then developing linearly preserves the orthogonality, meaning:
- **qcase** $s\{|0\rangle \to t_0, |1\rangle \to t_1\} \perp \text{qcase } t\{|0\rangle \to t_0, |1\rangle \to t_1\}$: we have $s \rightsquigarrow^* v$ and $t \rightsquigarrow^* w$ (they terminate as we can derive orthogonality). By definition, $v, w$ are well-typed closed values, thus $v \equiv \alpha \cdot |0\rangle + \beta \cdot |1\rangle$ and $w \equiv \gamma \cdot |0\rangle + \delta \cdot |1\rangle$. As they are orthogonal, then they will verify $\alpha\gamma^* + \beta\delta^* = 0$ (even if this is not the canonical form as some coefficients can be zero, this will still hold). Now, this indicates, by $E$, that **qcase** $s\{|0\rangle \to t_0, |1\rangle \to t_1\} \rightsquigarrow^* \alpha \cdot s_0 + \beta \cdot s_1$ and **qcase** $t\{|0\rangle \to t_0, |1\rangle \to t_1\} \rightsquigarrow^* \gamma \cdot s_0 + \delta \cdot s_1$, where $t_0 \rightsquigarrow^* s_0$ and $t_1 \rightsquigarrow^* s_1$. By Lemma 51, as $t_0 \perp t_1$, then $s_0 \perp s_1$, and thus $\alpha \cdot s_0 + \beta \cdot s_1 \perp \gamma \cdot s_0 + \delta \cdot s_1$.

- $c(s, \dots, t_n) \perp c(t, \dots, t_n)$: we suppose that $s, t$ are in first slot, other cases are done equivalently. By $E$, when reducing each term to a value, the first slot will contain the reduced value of $s$ and $t$. Then, as they are orthogonal, and the other values are identical, they have the same shape by Lemma 42, and when writing the summation to test the zero equality, we can just develop through the first coordinate to obtain back the summation from the orthogonality of $s$ and $t$.

- **match** $s\{\dots\} \perp \text{match } t\{\dots\}$: by definition, $s \rightsquigarrow \sum_{i=1}^n \alpha_i \cdot w_i$ and $t \rightsquigarrow \sum_{i=1}^n \beta_i \cdot w_i$, by writing their canonical form, and then completing by some $0 \cdot w_i$ in order to have the same pure elements on each side. As they are orthogonal, then $\sum_{i=1}^n \alpha_i \beta_i^* = 0$. Furthermore, they must have the same shape, and be a value of type $B$, thus any pure value satisfies $w_i = c_k(v_i^1, \dots, v_i^n)$. As $w_i \neq w_j$ for $i \neq j$, then one coordinate is distinct. Now, **match** $s\{\dots\} \rightsquigarrow^* \sum_{i=1}^n \alpha_i \cdot s_i$ and **match** $t\{\dots\} \rightsquigarrow^* \sum_{i=1}^n \beta_i \cdot t_i$, where $\sigma(w_i) \rightsquigarrow^* s_i$, and $\sigma(w_i) \rightsquigarrow^* t_i$. For any $i \neq j$, $\sigma_i$ and $\sigma_j$ have map one variable to a distinct pure value, as explained above; and any $v \neq w$ where $v, w$ are pure values satisfy $v \perp w$. We can thus apply Lemma 54, and get $\sigma_i(w_i) \perp \sigma_j(w_j)$. Finally, we can conclude by Lemma 51, and as $s_i, t_i$ are reduced terms from $\sigma_i(w_i)$, orthogonality is preserved.

Now, as $s$ is not pure, then there is a subterm of $s$ that contains a (sup) typing rule, followed by some (maybe 0) linear rules, i.e., (cons), (match) or (qcase), as they are the only rules which need a pure term inside their construction to be pure. By definition of $C_=$, we can develop linearly this sum to obtain $s' = \sum_{i=1}^n \alpha_i \cdot t_i$; and by construction, we can use the above result by induction, as each term is a subterm of a terminating term, thus reduces in less steps than the original term, therefore we can apply the induction hypothesis. Note that some terms may obtain a phase 0 at the end, and could have reduced in more steps; but as they will be removed, not applying this process is ok, as we will not test orthogonality with them anyway. as the base case is (sup) thus requires orthogonal terms. Therefore, by syntax, $s'$ is a sum of orthogonal well-typed terms. We can reapply this process on each $t_i$ until they are pure, which terminates as $t_i$ has a smaller typing tree than $s$, as one (sup) rule has been removed. At the end, we obtain multiple summation of pure orthogonal values $\sum_{i=1}^n \alpha_i \cdot (\cdots \sum_{k=1}^l \beta_k \cdot t_k)$. Each sum can be typed through (sup), as the coefficients come from a (sup) rule and the above cases show that orthogonality is kept. We can then develop everything, group equivalent pure terms, and obtain the canonical form back. However, after reducing each term, we can do the reverse and rewrite the obtained term as multiple summations. Furthermore, each term has either reduced, or stayed the same as it was removed; by induction hypothesis on $t_i \rightsquigarrow^? t'_i$, $t'_i$ is well-typed with the same context and type as $t$; and the orthogonality conditions are still true as we reduce terms, thus we can still type (sup) for each sum, and therefore type the big sum; as this sum is equivalent to $\sum_{i=1}^n \alpha_i \cdot t'_i$, by (equiv), we can type it and conclude.
(Shape₀) : by typing, we have Γ'; Δ' ⊢ |0⟩ : T' where Γ = Γ, [Δ'], Δ = ∅ and T = **shape**(T'). Again, as |0⟩ is pure, then we need to type it with (ax₀), which gives Δ' = ∅ and T = **shape**(Qbit) = 1. We conclude as we can type Γ; ∅ ⊢ () : 1 through (cons).

(Shape₁) : same as above.

(Shape_c) : as the root is (shape), typing gives Γ = Γ', [Δ'], Δ = ∅, T = [B] and
Γ; Δ ⊢ c(v₁, ..., vₙ) : B. Again by typing, the root being (cons), we have Γ; Δᵢ ⊢ vᵢ : Bᵢ|ᵢ
and Δ = Δ₁, ..., Δₙ. Therefore, (shape) gives Γ, [Δᵢ]; ∅ ⊢ **shape**(vᵢ) : **shape**(Bᵢ|ᵢ); as
[Δ] = [Δ₁], ..., [Δₙ], the definition of ¯c concludes.

(Shape_s): by Lemma 12, each v_i is well-typed with the same type as the summation, and we conclude as above.

(Equiv): By (equiv), Γ; Δ ⊢ t₁ : T, by i.h., Γ; Δ ⊢ t'₁ : T, and by (equiv) again on t₁ ≡ t', we conclude.

(E): by i.h. on t ↛ t', Γ; Δ ⊢ t' : T, thus one can replace the typing tree of t by the typing tree of t', and any rule will still hold. This is in particular true because E is made of no superpositions, so none of these checks happen and thus typing is preserved.

Now, given a term with some (contr) rules, we may consider the following:

■ One can first remark that any (contr) rule commutes with a (qcase), (match), or any (app) rule. Therefore, for the (Qcase), (Match), (Lbd), (Rec) rules, we can consider an alternative typing tree for *t* with *k* ≥ 0 (contr) rules at the end, and thus have *t* = σ₁...σₖ(*s*), where *s* has no (contr) rule near the end, thus we can apply the hypothesis above. Also note that if *t* ↛ *t*', then *t*' = σ₁...σₖ(*s*') and *s* ↛ *s*'. We can then apply the result above on *s* ↛ *s*', and reapply the *k* (contr) rules on *s*' to obtain the well-typedness of *t*'.

■ The (Can) rule contains terms that all have the same context, thus any (contr) rule may actually be applied on each tᵢ before.

■ Any (Shape) rule contains only values, thus no marked variable is actually given by the context and no (contr) rule is needed.

Therefore, the result still holds for any term.

**Theorem 14** (Subject reduction). Let Γ; Δ ⊢ t : T be a well-typed term, and t ↛ t'. If t terminates or t is pure, then Γ; Δ ⊢ t' : T.

**Proof.** If *t* terminates, then we can apply Lemma 55. If *t* is pure, one can remark that the proof in Lemma 55 for pure terms does not require termination, as (Can) is stopped from going further and needing the termination when *t* is pure, thus one can adapt the proof to get the result.

**C Proofs for Section 3.2**

**Theorem 16** (Undecidability of orthogonality). Deciding orthogonality between two well-typed terms is Π₂₀-complete.

**Proof.** Let us first prove the Π₂₀-hardness. Let us recall the definition of Programming Computable Functions (PCF), which is defined with the following types and terms grammar:

A, B ::= nat | A → B
t, t₁, t₂ ::= x | λx.t | t₁t₂ | fix t | n | succ | pred | ifz t₁t₂
Each term has a corresponding typing rule, and thus PCF is a typed language. It is easy to see that Hyrql can encode PCF: all of PCF's constructions are already present in Hyrql, apart from the following terms:

$$
\begin{align*}
\mathbf{fix} \ t &= \mathbf{letrec} \ f \ x = t \ f \ x \\
\mathbf{pred} &= \lambda x.\mathbf{match} \ x \{0 \to 0, S \ n \to n\} \\
\mathbf{ifz} &= \lambda x.\lambda y.\lambda n.\mathbf{match} \ n \{0 \to x, S \ m \to y\}
\end{align*}
$$

Therefore, any term of PCF can be encoded into a term in Hyrql through a total computable function. The Universal Halt problem on PCF is known to be Π<sub>2</sub><sup>0</sup>-hard. We define UHalt as the set of terms of PCF, thus terms in our language, terminating over any input, meaning tt<sub>1</sub> ... t<sub>n</sub> terminates.

Given a well-typed term *t* from PCF of type *T*₁ ↦ ... ↦ *T*ₙ ↦ *B*<sup>*l*</sup> (such type can always be obtained by the Lemma 36), we define

$$
g(t) = (tx_1 \dots x_n, |0\rangle), (tx_1 \dots x_n, |1\rangle),
$$

where $x_1, \dots, x_n$ are neither free nor bound variables of $t$. If $t \in \mathbf{UHalt}$, then it terminates over any input. In particular, this implies that $tx_1 \dots x_n$ terminates for any substitution, reducing to a value $v$; and as $(v, |0\rangle) \perp (v, |1\rangle)$, $g(t) \in \mathbf{ORTHO}$. If $g(t) \in \mathbf{ORTHO}$, then $t$ must terminate for any substitution of $x_1, \dots, x_n$, thus terminates for any value. Therefore, $t \in \mathbf{UHalt}$. Thus, $t \in \mathbf{UHalt} \iff g(t) \in \mathbf{ORTHO}$, $\mathbf{UHalt} \le \mathbf{ORTHO}$, and as $\mathbf{UHalt}$ is $\Pi_2^0$-hard, it concludes.

The fact that ORTHO ∈ Π₀² is direct by definition. Given *t*, *t'* be two terms of the same type with FV(*t*) = FV(*t'* ) = {*x*₁, ..., *x*ₙ}, and let σ*<sub>*v*₁,...,*v*ₙ</sub>* = {*x*ᵢ → *v*ᵢ}₁≤i≤n, then orthogonality decision can be written up as:

$$
\begin{align*}
\forall v_1, \dots, \forall v_n, \exists k \in \mathbb{N}, \sigma_{v_1, \dots, v_n} (\mathbf{shape}(t)) &\rightsquigarrow \leq^k v_s, \sigma_{v_1, \dots, v_n} (\mathbf{shape}(t')) &\rightsquigarrow \leq^k v'_s \\
\sigma(t) &\rightsquigarrow^* \sum_{i=1}^n \alpha_i \cdot v_i \in \mathbf{CAN}, \sigma(t') &\rightsquigarrow^* \sum_{j=1}^m \beta_j \cdot w_j \in \mathbf{CAN} \\
v_s &= v'_s \wedge \sum_{i=1}^n \sum_{j=1}^m \alpha_i \beta_j^* \delta_{v_i, w_j} = 0
\end{align*}
$$

The inside property is decidable: checking if a term reducing in less than *k* steps to a variable, written *t* ↦*≤*<sup>*k*</sup> *v*, is decidable; checking the first equality is decidable as there is no superposition (computed in *O(n*) with *n* the size of *v*), and the equality to 0 of the double sum and equality is decidable as we have restricted the scalars in $\mathbb{Q}$. Thus the inside property is $\Pi_0^0$; by definition, ORTHO belongs to $\Pi_2^0$, and thus is $\Pi_2^0$-complete. ◀

► **Proposition 17.** *Given a finite type* *B*<sup>*l*</sup>, *and two terminating terms* Ø;Ø ⊢ *s* : *B*<sup>*l*</sup>, Ø;Ø ⊢ *t* : *B*<sup>*l*</sup>, *it is decidable whether they are orthogonal*.*

**Proof.** One can check that any value of type *T* is of size |*v*| ≤ |*T*|<sub>*d*</sub>, by definition of the depth, therefore we use *n* as a bound on the size of any value of such type. In order to compute and decide ORTHO, we first need to reduce *s* and *t* to values, which is done in *f*, *g* steps. Then, computing *shape*(*s*) and *shape*(*t*) is done linearly in the size of the value, same for computing equality, thus this is done in *O(n*) steps. For the computation of the equality, one needs to compute the canonical forms for the reduced values of *s* and *t*. In particular, we can complement each canonical form, so that testing $\delta_{v_i,w_j}$ is done directly by comparing
the index. This implies checking all terms of the canonical form, and comparing it with all the other terms, thus checking $O(n)$, comparing it with $O(n)$ terms, and comparison is done in the worst case in $O(n)$ steps. Then, we compute each $\alpha_i \beta_j^*$, and then we have to sum $n$ terms and checking nullity. As we have assumed to reduce the set of complex phases such that this can be done polynomially, we assume it is not the operation with the most cost. Such calculus needs to be done in the worst case $n^3$ times. ◀

**D Proofs for Section 3.3**

**▶ Theorem 25 (Bounded circuit compilation).** Let $T: \mathbb{N} \to \mathbb{N}$, and let $t \in \text{Hyrql}(T)$ be a term of type $Q \to Q'$. Then, we can generate a family of circuits $C(t) \triangleq (C_w)_{w \in S(Q)}$ and a polynomial $P$ such that, for any $w \in S(Q)$:

- $|C_w| \le P(T(|w|))$;

- $\forall v \in S(w), C_w$ approximates $v'$ with probability $\frac{2}{3}$ on input $v$, where $tv \rightsquigarrow v'$.

**Proof.** Let $w \in S(Q)$, and $k = |w|$. We produce $C_w^t$ inductively on the syntax of $t$, first with no approximation, and show that $C_w^t$ is of size $P(T(k))$, where $P \in \mathbb{N}[X]$. From that, we approximate each gate, using the chosen universal set of gates, up to a precision $1 - \epsilon$, such that the overall circuit has a precision $\frac{2}{3}$. This approximation, done on each gate, can be done using Solovay-Kitaev theorem [32], which is known to approximate the original gate to a precision $1 - \epsilon$ in time $O(\log^c(1/\epsilon))$, for a constant $c$. Choosing $\epsilon = \frac{2}{3P(T(k))}$ satisfies the overall precision [40], and thus, our approximated circuit is of size $P(T(k)) \log^c(\frac{3P(T(k))}{2}) = O(P(T(k)) \log^c(P(T(k)))$, which can be bounded by a polynomial $Q \in \mathbb{N}[X]$, evaluated in $P(T(k))$. Therefore, the circuit is of size $Q(P(T(k))) = R(T(k))$ for $R = Q \circ P \in \mathbb{N}[X]$.

Note that due to the fact that $t \in \text{CircuitTerms}$, one can always assume that there is no (contr), (equiv) or (shape) rule; by typing, any subterm is also always well-typed. We may also omit $w$ and write $C^t$.

All obtained polynomials, by induction, are only summations of polynomial, thus there is no exponential blowup on the coefficients. Furthermore, one can check that the introduced ancillary qubits that play a role must be applied onto a gate, thus we have at most $P(T(k))$ ancillary qubits.

- If $t = \text{qcase } s\{|0\rangle \to t_0, |1\rangle \to t_1\}$, we first put $C_w^s$. Then, either $t_i$ are values, and this represents an isometry, thus a unitary (up to ancillary qubits) which will be approximated later; or they are not values, thus of the shape $c(|i\rangle, s_i)$; and we put the circuits $C_w^{s_i}$, controlled (on $|i\rangle$ for $C_w^{s_i}$), one after the other, the control wire being the output of $C_w^s$. As the three circuits have a size bounded by a polynomial, the total size is bounded by a polynomial too.

- If $t = \text{match}_{1 \le i \le n} s\{c_i(\vec{x}_i) \to t_i\}$, as we know that $t$ terminates, and the input has a precise shape, the match will only reduce to a specific branch; thus, we put $C_w^s$, followed by $C_w^{t_i}$, for the corresponding branch. It also binds the wires labelled by the variables in $c(\vec{x}_i)$ to the corresponding outputs of $t$. This yields one swap, between at most $P(T(k))$ wires, thus can be implemented by at most $P(T(k))$ CNOT gates.

- Constructors: $0$ generates a classical wire, $S(t)$ adds 1 to the classical wire, $[]$ is an empty circuit, and $h :: t, h \times t$ are both circuits put one on top of the other. The bound on the size is obtained directly, as for `qcase`.
■ If $t = \lambda x.s$, this will only reroute the wire labelled with $x$ as the first wire of the circuit (i.e., a swap). If $x$ is not used, this wire is traced out. The swap can be implemented, as for match, by $P(T(k))$ CNOT gates.

■ Suppose $t = \text{letrec} f x = s$. We generate recursively $C_s$, which contains boxes for each possible call of $f$. We do any circuit simplification (e.g. if there is a controlled gate on a wire with value $|0\rangle$, remove the gate), to remove ill-paths. We have $n \le |t|$ boxes corresponding to $f$ in $C^s$. However, one can notice that the boxes are controlled on the same wire, by restriction of the syntax of the `qcase`, and are applied on the same wire, also by restriction of `letrec`. This problem is called *branch sequentialization*, and we can transform this into only one gate $f$, adding $O(1)$ gates before and after such gate [30, Theorem 9]. Then, we generate $C_{w'}^s$, replacing the box $f$ in our circuit, but for the new corresponding input shape $w'$. Such process will terminate, as $t$ terminates, thus there is only a finite number of recursive calls. In the worst case, we have added $T(k)$ circuits, thus the total size is $T(k)P(T(k)) = P'(T(k))$, for $P' = XP \in \mathbb{N}[X]$.

■ Other terms are quite direct: $x, |0\rangle, |1\rangle$ generate a wire with this value, $st$ just puts $C^t$ and then $C_{w'}^s$, where $w'$ is the shape of $t$ for the specific input $w$; due to the type restriction, we can assume there is no **shape construct**, else it would just be on natural numbers, which gives the same number back; superpositions are only on values, thus will only create ancillary wires. ◀

**Theorem 21 (Circuit compilation).** Let $t \in \text{CircuitTerms} \cap \text{Time}(T)$ be a term of type $Q \to Q'$ for a given $T: \mathbb{N} \to \mathbb{N}$. Then, we can generate a family of circuits $C(t) \triangleq (C_w)_{w \in S(Q)}$ such that for any $w \in S(Q)$ and any $v \in S(w)$, $C_w$ approximates $v'$ with probability $\frac{2}{3}$ on input $v$, where $tv \rightsquigarrow^* v'$.

**Proof.** The circuit can be generated similarly to the proof of Theorem 25, as **Faithful** only plays a role for the size of the circuit. ◀

**Theorem 27 (FBQP soundness).** Let $t \in \text{Hyrql}(\text{Poly})_{\text{QList}}$, and let $f: \{0,1\}^* \to \{0,1\}^*$. If $f$ is computed by $C(t)$, then $f \in \text{FBQP}$.

**Proof.** We need to prove that $(C_n^t)_{n \in \mathbb{N}}$ is a uniform polynomially-sized family of circuits. As $t \in \text{Hyrql}(\text{Poly})_{\text{QList}}$, there is a polynomial $Q$ such that $t$ terminates in time $Q$. Therefore, by Theorem 25, the circuit is of size $O(P(Q(n)))$, thus of polynomial size in $n$. Note that we have indexed the circuits by $n$ rather than $w$, but $|w| = n$, as discussed before. The fact that this family is uniform is obtained by building the circuit as done in the proof of Theorem 25: one can build a Turing machine, taking as input the size $n$ (thus the shape), and suppose that it contains initially the encoding of $t$, thus without the input, onto a tape of the QTM. As the circuit is build inductively on the syntax, and it differs only by the input shape, this creation is uniform, and is done in polynomial time, as the generated circuit is of polynomial size. ◀

**Theorem 28 (FBQP completeness).** Let $f: \{0,1\}^* \to \{0,1\}^* \in \text{FBQP}$. Then, there exists $t \in \text{Hyrql}(\text{Poly})_{\text{QList}}$ such that $C(t)$ computes $f$.

**Proof.** We prove this result by using Yamakami's algebra [53]. This paper defines a function algebra, and then proves that it completely characterize FBQP. Formally, it defines the function class $\square_1^{\text{QP}}$, which is the smallest class of functions including the following gates, for
$\theta \in [0, 2\pi) \cap \tilde{C}:$

$$I(|\phi\rangle) \triangleq |\phi\rangle$$

$$PHASE_{\theta}(|\phi\rangle) \triangleq |0\rangle\langle 0|\phi\rangle + e^{i\theta}|1\rangle\langle 1|\phi\rangle$$

$$ROT_{\theta}(|\phi\rangle) \triangleq \cos \theta |\phi\rangle + \sin \theta (|1\rangle\langle 0|\phi\rangle - |0\rangle\langle 1|\phi\rangle)$$

$$NOT(|\phi\rangle) \triangleq |1\rangle\langle 0|\phi\rangle + |0\rangle\langle 1|\phi\rangle$$

$$SWAP(|\phi\rangle) \triangleq \begin{cases} |\phi\rangle & \text{if } l(|\phi\rangle) \le 1 \\ \sum_{a,b \in \{0,1\}} |ab\rangle\langle ba|\phi\rangle & \text{otherwise} \end{cases}$$

and is closed under the following schemes:

$$Compo[g, h](|\phi\rangle) \triangleq g \circ h(|\phi\rangle)$$

$$Branch[g, h] \triangleq \begin{cases} |\phi\rangle & \text{if } l(|\phi\rangle) \le 1 \\ |0\rangle \otimes g(\langle 0|\phi\rangle) + |1\rangle \otimes h(\langle 1|\phi\rangle) & \text{otherwise} \end{cases}$$

$$kQRec_t[g, h, p|\mathcal{F}_k](|\phi\rangle) \triangleq \begin{cases} g(|\phi\rangle) & \text{if } l(|\phi\rangle) \le t \\ h(\sum_{w \in \{0,1\}^k} |w\rangle \otimes f_w(\langle w|p(|\phi\rangle))) & \text{otherwise} \end{cases}$$

Here, $|\phi\rangle$ is a quantum state, i.e., belongs to the Hilbert space $\mathbb{C}^{2^n}$ for a given $n$ written in Dirac notation. Its size $l(|\phi\rangle)$ is $n$. Given $w \in \{0, 1\}^n$ with $n \le l(|\phi\rangle)$, we may write $|\phi\rangle = \sum_i \alpha_i |w_i z_i\rangle$, where $w_i \in \{0, 1\}^n$ and $z_i \in \{0, 1\}^{l(|\phi\rangle)-n}$; we then abuse the notation by writing $\langle w|\phi\rangle = \sum_i \alpha_i \langle w|w_i\rangle |z_i\rangle$. $\tilde{C}$ denotes the complex numbers whose real and imaginary parts can both be approximated by a polynomial-time Turing machine. Note that this falls in the restriction that we did in Section 3.2.

This class is proven to be FBQP complete, thus any function of FBQP can be written as a function $\square_1^{QP}$. We therefore associate any function $\square_1^{QP}$ with a given term in Hyrql, $[\square_1^{QP}]$, and prove inductively that they belong in Hyrql(Poly)$_{QList}$.

Given a word $w = w_1 \dots w_n \in \{0, 1\}^n$, we denote $L(w)$ as the list $|w_1\rangle :: \dots :: |w_n\rangle :: []$. One can remark that for any function $f \in \square_1^{QP}$, and any input $w \in \{0, 1\}^*$, $f|w\rangle = v$, where $[[f]]L(w) \rightsquigarrow v$, thus they compute the same function. As $[[f]]$ is approximated by the family of circuits $\mathcal{C}([[f]])$ by Theorem 25, then $f$ is also approximated by this family, with precision $\frac{2}{3}$, thus giving us the wanted result.

$$[[I]] \triangleq \lambda x.x$$

$$[[Ph_{\theta}]] \triangleq \lambda x.\mathbf{qcase} x \{ |0\rangle \rightarrow |0\rangle, |1\rangle \rightarrow e^{i\theta} |1\rangle \}$$

$$[[Rot_{\theta}]] \triangleq \lambda x.\mathbf{qcase} x \{ |0\rangle \rightarrow \cos \theta |0\rangle + \sin \theta |1\rangle, |1\rangle \rightarrow -\sin \theta |0\rangle + \cos \theta |1\rangle \}$$

$$[[Not]] \triangleq \lambda x.\mathbf{qcase} x \{ |0\rangle \rightarrow |1\rangle, |1\rangle \rightarrow |0\rangle \}$$

$$[[SWAP]] \triangleq \lambda x.\mathbf{match} x \{ [] \rightarrow [], h :: t \rightarrow \mathbf{match} t \{ [] \rightarrow h :: [], h' :: t' \rightarrow h' :: h :: t \} \}$$

$$[[COMP[f, g]]] \triangleq \lambda x.([f]([g]x))$$

$$[[Branch[f, g]]] \triangleq \lambda x.\mathbf{match} x \left\{ \begin{array}{l} [] \rightarrow [] \\ h :: t \rightarrow \mathbf{match} t \left\{ \begin{array}{l} [] \rightarrow h :: [] \\ h' :: t' \rightarrow \mathbf{qcase} h \left\{ \begin{array}{l} |0\rangle \rightarrow |0\rangle \otimes [[f]](h' :: t') \\ |1\rangle \rightarrow |1\rangle \otimes [[g]](h' :: t') \end{array} \right\} \end{array} \right\} \end{array} \right\}$$

All terms belong in CircuitTerms $\cap$ Faithful by construction, and as functions have no recursive construct, they terminate in a fixed time, independently of the input, and thus they belong in Hyrql(Poly)$_{QList}$.
For the recursive function, we need to introduce before some constructs. $\text{proj}_t$ is of type $\text{list}(\text{Qbit}) \to \text{Qbit}^{\times t} \times \text{list}(\text{Qbit}) \times \text{bit}$; it takes a list $x$, then returns the first $t$ elements, the remaining part of the list, and a bit indicating if the length of the list is strictly greater than $t$. If there is less elements, we put $|0\rangle$ by default for the first $t$ elements of the tuple. We then create two functions $\text{check}_t$ which returns the list reconstructed and the bit, and $\text{prōj}_t$ which discards the bit. We also define $\text{qcase}_k(x_1, \dots, x_k)\{|s\rangle \to t_s\}$ as a qcase taking $k$ qubits as inputs and producing all possible $2^k$ branches, where $s \in \{0, 1\}^k$ is the path taken by each $x_i$; $\overrightarrow{|s\rangle}$ is the notation which transform the $k$ qubits as a list of $k$ elements. This constructs allow then to define the last function of the algebra, with the following set $\mathcal{F}_k = \{f_s : s \in \{0, 1\}^k\}$, where each $f_s \in \{kQ\text{Rec}_t[g, h, p | \mathcal{F}_k], I\}$, and $[[f_s]]$ is respectively $f$ or $\lambda x.x$.

$$
\begin{align*}
\text{proj}_t &\triangleq q\lambda x.\text{match } x \quad \left\{ \begin{array}{@{}l@{}} \llbracket \, \rightarrow (|0\rangle, \dots, |0\rangle, \llbracket \, \llbracket \, \rightarrow (h_1, \dots, h_t, \llbracket \, \llbracket \, \rightarrow (h_1, \dots, h_t, h_{t+1} \therefore r_{t+1}) \end{array} \right\} \\
\text{prōj}_t &\triangleq \lambda x.\text{match } \text{proj}_t \{(h_1, \dots, h_d, r, b) \rightarrow (h_1, \dots, h_d, r)\} \\
\text{check}_t &\triangleq \lambda x.\text{match } \text{proj}_t \{(h_1, \dots, h_d, r, b) \rightarrow (h_1 \therefore \dots \therefore h_t \therefore r, b)\}
\end{align*}
\[
[[kQ\text{rec}_t[g, h, p | \mathcal{F}_k]]] \triangleq \text{letrec } f x = \text{match } \text{check}_t \ x\{(y, b) \rightarrow \text{match } b\{0 \rightarrow f(y), \\
1 \rightarrow \text{match } \text{prōj}_k(h, y) \left\{ (h_1, \dots, h_k, r) \rightarrow g(\text{qcase}_k(h_1, \dots, h_k))\{|s\rangle \rightarrow \overrightarrow{|s\rangle} \therefore [[f_s]] r\} \right\} \}
\end{align*}
$$

Again, such encoding belongs to CircuitTerms ∩ Faithful. Furthermore, terminating
in polynomial time is guaranteed, as:

■ By induction, each $g, h, p$ computes in polynomial time;

- Either $f_s$ is the identity, thus stops here, or is a recursive call on an input of size that decreases by $k$;

- Therefore, the compute time is roughly, for an input of size $n$, $\frac{n}{k} \max(P_g(n), P_h(p), P_p(n))$, where $P_g, P_h, P_p$ is the compute time of respectively $g, h, p$, which is polynomial, by induction hypothesis. The obtain time is thus polynomial in $n$. ◀