A Rewriting Theory for Quantum $\lambda$-Calculus

In the last 20 years, many proposals for quantum programming languages have emerged [28, 30, 40, 39, 8, 11]. Similar to classical languages, the paradigm of higher-order, functional quantum programming languages have been shown to be a fertile playground for the development of well-founded, formal quantum languages aiming at the formal analysis of quantum programs [40, 11].

The quantum $\lambda$-calculus of Selinger&Valiron [42] lies arguably at the foundation of the development of higher-order, quantum functional programming languages [14, 13, 38, 12, 35]. Akin to other extensions of lambda-calculus with probabilistic [17, 15, 21] or non-deterministic behavior [16], the quantum lambda calculus extends the regular lambda calculus – core of functional programming languages – with a set interface to manipulate a quantum memory. Due to the properties of the quantum memory, quantum lambda-calculi should handle non-duplicable data and probabilistic behavior.

One of the critical points that a quantum programming language should address is the problem of the non-duplicability of quantum data. In the literature, non-duplicable data is usually captured with tools coming from linear logic. The first approach [42, 38, 12] consists in using types, imposing all functions to be linear by default, and with the use of a special type $!A$ to explicitly pinpoint duplicable objects of type $A$. An alternative – untyped – approach [13, 14] considers instead an untyped lambda calculus, augmented with a special term construct “$!$” and validity constraints to forbid the duplication of qubits.

A quantum $\lambda$-calculus featuring all of quantum computation should not only permit the manipulation of quantum register with unitary operations but should also give the possibility to measure them, and retrieve a classical bit of information. As the latter is a probabilistic operation, an operational semantics for a quantum $\lambda$-calculus is inherently probabilistic. As in the non-quantum case, probabilistic choice and unbounded recursion yield subtle behaviors.
Fair Coin.   Consider the following program $L$, written in a mock-up ML language with quantum features, similar to the language of [42]:

For this introduction, we only describe its behavior informally. The term $L$ above produces a qubit¹¹1The reader unfamiliar with the notation should not worry, as the formal details are not essential at this point: just retain that the state of our qubit is a superposition of two (basis) states, which play the role of head and tail. When needed, in Section 3 we provide a brief introduction to the mathematical formalism for quantum computation [37]. in state $\frac{\sqrt{2}}{2}(|0⟩+|1⟩)$ by creating a fresh qubit in state $|0⟩$ (this is the role of $\mathrm{𝚗𝚎𝚠}$), and applying the Hadamard gate $H$. Measuring this qubit amounts to flipping a fair coin with equal probability $\frac{1}{2}$. In one case, the program returns the identity function $I$; otherwise, it diverges – the term $\mathrm{\Omega }$ stands for the usual, non-terminating looping term.

The program $L$, therefore, uses the quantum memory only once (at the beginning of the run of the program), and it terminates with probability $\frac{1}{2}$.
Unbounded Use of Fair Coin.   In the context of probabilistic behavior, unbounded loops might terminate asymptotically: A program may terminate with probability $1$, but only at the limit (almost sure termination). A simple example suffices to illustrate this point.

Consider a quantum process $R$ that flips a coin by creating and measuring a fresh qubit. If the result is head, the process stops, outputting $I$. If the result is tail, it starts over. In our mock-up ML, the program $R$ is

After $n$ iterations, the program $R$ is in normal form with probability $\frac{1}{2}+\frac{1}{2^2}+\mathrm{\cdots }+\frac{1}{2^n}$. Even if the termination probability is $1$, this probability of termination is not reached in a finite number of steps but as a limit. The program in Equation 1 is our leading example: we formalize it in Example 4.3.

As it is customary when dealing with choice effects, the probabilistic behavior is dealt with by fixing an evaluation strategy. Think of tossing a (quantum) coin and duplicating the result, versus tossing the coin twice, which is indeed one key issue at the core of confluence failure in such settings (as observed in [16, 13]). Following the standard approach adopted for functional languages with side effects, the evaluation strategy in quantum $\lambda$-calculi such as [42, 38, 12] is a deterministic call-by-value strategy: an argument is reduced to a value before being passed to a function.

One aspect that has been seldom examined is however the properties of the general reduction associated to the quantum lambda-calculus: this is the purpose of this paper.

Lambda calculus has a rich, powerful notion of reduction, whose properties are studied by a vast amount of literature. Such a general rewriting theory provides a sound framework for reasoning about programs transformations, such as compiler optimizations or parallel implementations, and a base on which to reason about program equivalence. The two fundamental operational properties of lambda calculus are confluence and standardization. Confluence guarantees that normal forms are unique, standardization that if a normal form exists, there is a strategy that is guaranteed to terminate in such a form.

As pioneered by Plotkin [41], standardization allows to bridge between the general reduction (where programs transformation can be studied), and a specific evaluation strategy, which implements the execution of an idealized programming language. Summarizing the situation, for programming languages, there are two kinds of term rewriting: run-time rewriting (“evaluation”) and compile-time rewriting (program transformations).

In the context of quantum lambda-calculi, the only line of research discussing rewriting (rather than fixing a deterministic strategy) has been pursued by Dal Lago, Masini, and Zorzi [14, 13]: working with an untyped quantum lambda-calculus, they establish confluence results (and also a form of standardization, but only for the sub-language without measurement [13] – therefore, without the probabilistic behavior).

In this paper, we study not only confluence but also standardization and normalization results for a quantum $\lambda$-calculus featuring measurement, and where $\beta$ reduction (the engine of $\lambda$-calculus) is fully unrestricted. Recent advances in probabilistic and monadic rewriting theory [9, 12, 19, 33, 6, 23, 27, 32] allow us to tackle this task with a formalism and powerful techniques unavailable a decade ago. Still, quantum rewriting is more challenging than probabilistic rewriting because we need to manage the states of the quantum memory. The design of the language is, therefore, also delicate: we need to control the duplication of qubits while allowing the full power of $\beta$-reduction.

We can summarize the contributions of the paper as follows. These are described in more details in Section 5, once all the necessary materials have been set up.

• $\mathrm{■}$

  An untyped quantum lambda-calculus, closely inspired by [14] but re-designed to allow for a more general reduction, now encompassing the full strength of $\beta$-reduction; validity constraints make it quantum-compatible.

• $\mathrm{■}$

  The calculus is equipped with a rich operational semantics, which is sound with respect to quantum computation. The general reduction enables arbitrary $\beta$-reduction; surface reduction (in the spirit of [43] and other calculi based on Linear Logic) plays the role of an evaluation strategy.

• $\mathrm{■}$

  We study the rewriting theory for the system, proving confluence of the reduction, and standardization.

• $\mathrm{■}$

  We obtain a normalization result that scales to the asymptotic case, defining a normalizing strategy w.r.t. termination at the limit.

Missing proofs and some more technical details are given in the extended version [25].

Our quantum calculus is built on top of Simpson’s calculus ${\mathrm{\Lambda }}^{!}$ [43], a variant of untyped $\lambda$-calculus inspired by Girard’s Linear Logic [29]. In this choice, we follow [14, 13, 12]. Indeed, the fine control of duplication which ${\mathrm{\Lambda }}^{!}$ inherits from linear logic makes it an ideal base for quantum computation.

The Bang operator $!$ plays the role of a marker for non-linear management: duplicability and discardability of resources. Abstraction is refined into linear abstraction $\lambda x.M$ and non-linear abstraction ${\lambda }^{!}x.M$. The latter allows duplication of the argument, which is required to be suspended as thunk $!N$, behaving as the $!$-box of linear logic.

In our paper, as well as in [14, 13, 12], surface reduction (i.e., no reduction is allowed in the scope of the $!$ operator) is the key ingredient to allow for the coexistence of quantum bits with duplication and erasing. Unlike previous work however, in our setting $\beta$-reduction – the engine of $\lambda$-calculus – is unconstrained. We prove that only quantum operations needs to be surface, making ours a conservative extension of the usual $\lambda$-calculus, with its full power.

The reader may have recognized that reduction in our calculus follows the Call-by-Push-Value paradigm, with the Bang operator thunking a computation. In fact, Simpson’s calculus [43], more precisely the fragment without linear abstraction, is essentially an untyped version of Call-by-Push-Value, and it has been extensively studied in the literature of Linear Logic also with the name of Bang calculus [20, 31, 10], as a unifying framework which subsumes both Call-by-Name (CbN) and Call-by-Value(CbV) calculi.

Termination and confluence concern the existence and the uniqueness of normal forms, which are the results of a computation. Standardization and normalization are concerned with how to compute a given outcome. For example, is there a strategy which guarantees termination, if possible? The desired outcome is generally a specific kind of terms. In the classical theory of $\lambda$-calculus (à la Barendregt), the terms of interest are head normal forms. In the Call-by-Value approach, the terms of computational interest are values.
Classical $\lambda$-calculus.   The simplest form of standardization is factorization: any reduction sequence can be re-organized so as to first performing specific steps and then everything else. A paradigmatic example is the head factorization theorem of classical $\lambda$-calculus (theorem 11.4.6 in [7]): every $\beta$-reduction sequence $M{\to }_{\beta }^{\ast }N$ can be re-organized/factorized so as to first reducing head redexes and then everything else – in symbols $M{\to }_h^{\ast }\cdot {\to }_{\neg h}^{\ast }N$.

A major consequence is head normalization, relating arbitrary $\beta$ reduction with head reduction, w.r.t. head normal forms, the terms of computational interest in classical $\lambda$-calculus. A term $M$ has head normal form if and only if head reduction terminates:

Plotkin’s Call-by-Value.   This kind of results takes its full computational meaning in Plotkin’s [41] Call-by-Value $\lambda$-calculus The terms of interest are here values. Plotkin relates arbitary $\beta$ reduction (${\to }_{{\beta }_v}$) and the evaluation strategy ${\to }_l$ which only performs weak-left steps (no reduction in the scope of abstractions), by establishing

In words: the unconstrained reduction (${\to }_{{\beta }_v}$) returns a value if and only if the evaluation strategy (${\to }_l$) returns a value. The proof relies on a factorization: $M{\to }_{{\beta }_v}^{\ast }N$ iff $M{\to }_l^{\ast }\cdot {\to }_{\neg l}^{\ast }N$.
Simpson’s pure calculus.   Standardization and Normalization results have been established by Simpson also for its calculus ${\mathrm{\Lambda }}^{!}$ [43]. Here, the evaluation strategy is surface reduction, i.e. no reduction is allowed in the scope of a $!$ operator.
Summary.   The table in Table 1 summarize the factorization and normalization result for the three calculi (respectively based on $\beta ,{\beta }_v,{\beta }_{!}$) which we have discussed.

Formally, raw terms $M,N,P,\mathrm{\dots }$ are built according to the following grammar.

where $x$ ranges over a countable set of variables, $r_i$ over a disjoint set of registers where $i\in N$ is called the identifier of the register, and $U_A$ over a set of build-in n-ary gates. In this paper, we limit the arity $n$ to be $1$ or $2$. Pairs do not appear as a primitive construct, but we adopt the standard encoding, writing $⟨M,N⟩$ as sugar for $\lambda f.\left(fM\right)N$. We also use the shorthand $⟨M_1,\mathrm{\dots },M_n⟩$ for $⟨M_1⟨M_2,\mathrm{\dots }⟩⟩$. The variable $x$ is bound in both $\lambda x.P$ and ${\lambda }^{!}x.P$. As usual, we silently work modulo $\alpha$-equivalence. Given a term of shape $\mathrm{𝚖𝚎𝚊𝚜}(P,M,N)$, we call $M$ and $N$ its branches. As usual, the set of free variables of a term $M$ are denoted with $\mathrm{𝙵𝚅}(M)$. The set of registers identifiers for a term $M$ is denoted with $\mathrm{𝚁𝚎𝚐}(M)$.

To deal with the problem in Remark 3.1, we need to introduce the notions of context and surface context, to speak of occurrences and surface occurrences of subterms.

A context is a term with a hole. We define general contexts where the hole can appear anywhere, and surface contexts for contexts where holes do not occur in the scope of a $!$ operator, nor in the branches of a $\mathrm{𝚖𝚎𝚊𝚜}(-,-,-)$. They are generated by the grammars

where $⦇⦈$ denotes the hole of the corresponding context. The notation $\text{C}⦇R⦈$ (or $\text{S}⦇R⦈$) stands for the term where the only occurrence of a hole $⦇⦈$ in C (or S) is replaced with the term $R$, potentially capturing free variables of $R$.

Contexts and surface contexts allow us to formalize two notions of occurence of a subterm $T$. The pair $(\text{C},T)$ (resp. $(\text{S},T)$) is an occurence (resp. surface occurence) of $T$ in $M$ whever $M=\text{C}⦇T⦈$ (resp. $M=\text{S}⦇T⦈$). By abuse of notation, we will simply speak of occurrence of a subterm in $M$, the context being implicit.

We can now define a notion of valid terms, agreeing with the quantum principle of no-cloning.

Before diving into the definition of the notion of program, we briefly recall here the mathematical formalism for quantum computation [37].

The basic unit of information in quantum computation is a quantum bit or qubit. The state of a single qubit is a normalized vector of the 2-dimensional Hilbert space $C^2$. We denote the standard basis of $C^2$ as $\{|0⟩,|1⟩\}$, so that the general state of a single qubit can be written as $\alpha |0⟩+\beta |1⟩$, where ${|\alpha |}^2+{|\beta |}^2=1$.

The basic operations on quantum states are unitary operations and measurements. A unitary operation maps an n-qubit state to an n-qubit state, and is described by a unitary $2^n\times 2^n$-matrix. We assume that the language provides a set of built-in unitary operations, including for example the Hadamard gate $H$ and the controlled not gate $\mathrm{𝖢𝖭𝖮𝖳}$:

Measurement acts as a projection. When a qubit $\alpha |0⟩+\beta |1⟩$ is measured, the observed outcome is a classical bit: either $0$ or $1$, with probabilities ${|\alpha |}^2$ and ${|\beta |}^2$, respectively. Moreover, the state of the qubit collapses to $|0⟩$ (resp. $|1⟩$) if $0$ (resp. $1$) was observed.

In order to associate quantum states to registers in lambda-terms, we introduce the notion of program, consisting of a quantum memory and a lambda-term of ${\mathrm{\Lambda }}_q$. A program is closed under permutation of register identifiers.

The state of one qubit is a normalized vector in $ℰ=C^2$. The state of a quantum memory (also called qubits state in the remainder of the document) consisting of $n$ qubits is a normalized vector $𝚀\in {ℰ}^n={(C^2)}^{\otimes n}$, the $n$-fold Kronecker product of $ℰ$. The size of $𝚀$ is written $|𝚀|≔n$. We identify a canonical basis element of ${ℰ}^n$ with a string of bits of size $n$, denoted with $|b_0\mathrm{\dots }{b}_{n-1}⟩$. A state $𝚀\in {ℰ}^n$ is therefore in general of the form $𝚀={\sum }_{b_0,\mathrm{\dots }{b}_{n-1}\in \{0,1\}}{\alpha }_{b_0\mathrm{\dots }{b}_{n-1}}|b_0\mathrm{\dots }{b}_{n-1}⟩.$ If $\sigma$ is a permutation of $\{0,\mathrm{\dots }n-1\}$, we define $\sigma (𝚀)$ as $\sigma (𝚀)={\sum }_{b_0,\mathrm{\dots }{b}_{n-1}\in \{0,1\}}{\alpha }_{b_0\mathrm{\dots }{b}_{n-1}}|b_{\sigma (0)}\mathrm{\dots }{b}_{\sigma (n-1)}⟩.$

A raw program $𝐩$ is then a pair $\mathbf{[}𝚀;M\mathbf{]}$, where $𝚀\in {ℰ}^n$ and where $M$ is a valid term such that $\mathrm{𝚁𝚎𝚐}(M)=\{0,\mathrm{\dots },n-1\}$. We call $n$ the size of $𝚀$ and we denote it with $\left|𝚀\right|$. If $\sigma$ is a permutation over the set $\{0..n-1\}$, the re-indexing $\sigma (𝐩)$ of $𝐩$ is the pair $\mathbf{[}\sigma (𝚀);\sigma (M)\mathbf{]}$ where $\sigma (M)$ is $M$ with each occurence of $r_i$ replaced by $r_{\sigma (i)}$.

We recall that a rewriting system is a pair $(𝒜,\to )$ consisting of a set $𝒜$ and a binary relation $\to$ on $𝒜$ whose pairs are written $t\to s$ and called reduction steps. We denote ${\to }^{\ast }$ (resp. ${\to }^{=}$) the transitive-reflexive (resp. reflexive) closure of $\to$. We write $t\leftarrow u$ if $u\to t$. If ${\to }_1,{\to }_2$ are binary relations on $𝒜$ then ${\to }_1\cdot {\to }_2$ denotes their composition.

In order to define the operational semantics of the quantum lambda calculus, we need to formalize probabilistic reduction. We do so by means of a rewrite system over multidistributions, adopting the monadic approach recently developed in the literature of probabilistic rewriting (see e.g. [6, 12, 19, 23]). Reduction is here defined not simply on programs, but on (monadic) structures representing probability distributions over programs, called multidistributions.

The operational semantics of the language is defined by specifying the probabilistic behavior of programs, then lifting reduction to multidistributions of programs. Let us recall the notions.
Probability Distributions.  Given a countable set $\mathrm{\Omega }$, a function $\mu :\mathrm{\Omega }\to [0,1]$ is a probability subdistribution if $\Vert \mu \Vert :={\sum }_{\omega \in \mathrm{\Omega }}\mu (\omega )\le 1$ (a distribution if $\Vert \mu \Vert =1$). Subdistributions allow us to deal with partial results. We write $𝙳(\mathrm{\Omega })$ for the set of subdistributions on $\mathrm{\Omega }$, equipped with the pointwise order on functions: $\mu \le \rho$ if $\mu (\omega )\le \rho (\omega )$ for all $\omega \in \mathrm{\Omega }$. $𝙳(\mathrm{\Omega })$ has a bottom element (the subdistribution $\mathrm{𝟎}$) and maximal elements (all distributions).
Multidistributions.  We use multidistributions [6] to syntactically represent distributions. A multidistribution $𝚖={\{\{q_i{𝐩}_i\}\}}_{i\in I}$ on the set of programs $𝒫$ is a finite multiset of pairs of the form $q_i{𝐩}_i$, with $q_i\in ]0,1]$, ${𝐩}_i\in 𝒫$, and ${\sum }_i{q}_i\le 1$. The set of all multidistributions on $𝒫$ is $\mathrm{𝙼𝙳}(𝒫)$. The sum of two multidistributions is noted $+$, and is simply the union of the multisets. The product $q\cdot 𝚖$ of a scalar $q$ and a multidistribution $𝚖$ is defined pointwise $q\cdot {\{\{p_i{𝐩}_i\}\}}_{i\in I}:={\{\{(q\cdot p_i){𝐩}_i\}\}}_{i\in I}$. We write $\{\{𝐩\}\}$ for $\{\{\mathrm{\hspace{0.17em}1}𝐩\}\}$.

The relation $\to$ is confluent if ${\leftarrow }^{\ast }\cdot {\to }^{\ast }\subseteq {\to }^{\ast }\cdot {\leftarrow }^{\ast }.$ A stricter form is the diamond $\leftarrow \cdot \to \text{ implies }\to \cdot \leftarrow$, which is well known to imply confluence. Two relations $\underset{\circ }{\to }$ and $\underset{\bullet }{\to }$ on $A$ commute if :  ${\underset{\circ }{\leftarrow }}^{\ast }\cdot {\underset{\bullet }{\to }}^{\ast }\text{ implies }{\underset{\bullet }{\to }}^{\ast }\cdot {\underset{\circ }{\leftarrow }}^{\ast }$. Confluence and factorization are both commutation properties: a relation is confluent if it commutes with itself.

An element $u\in 𝒜$ is a $\to$-normal form if there is no $t$ such that $u\to t$ (written $u\to ̸$).
On normalization. In general, a term may or may not reduce to a normal form. And if it does, not all reduction sequences necessarily lead to normal form. How do we compute a normal form? This is the problem tackled by normalization: by repeatedly performing only specific steps, a normal form will be computed, provided that $t$ can reduce to any. Intuitively, a normalizing strategy for $\to$ is a reduction strategy which, given a term $t$, is guaranteed to reach normal form, if any exists.

The probability that the system described by the multidistribution $𝚖=\{\{p_i\mathbf{[}{𝚀}_i;M_i\mathbf{]}\mid i\in I\}\}$ is in surface normal form is expressed by a scalar $p=P(𝚖)\in [0,1]$ which is defined as follows:

Let $𝐩=\mathbf{[}𝚀;M\mathbf{]}$ and ${𝚖}_0=\{\{𝐩\}\}$. Let ${𝚖}_0\Rightarrow {𝚖}_1\Rightarrow {𝚖}_2\Rightarrow \mathrm{\cdots }$ a reduction sequence. $P({𝚖}_k)$ expresses the probability that after $k$ steps $𝐩$ is in snf. The probability that $𝐩$ reaches snf along the (possibly infinite) reduction sequence ${⟨{𝚖}_n⟩}_{n\in N}$ is easily defined as a limit: ${sup}_n\{P({𝚖}_n)\}.$ We also say that the sequence ${⟨{𝚖}_n⟩}_{n\in N}$ converges with probability ${sup}_n\{P({𝚖}_n)\}$.