Under consideration for publication in Math. Struct. in Comp. Science

A lambda calculus for quantum computation with classical control

P E T E R S E L I N G E R^{1}^{†} and B E N O I T V A L I R O N^{2}

1 Department of Mathematics and Statistics, Dalhousie University, Halifax, Nova Scotia, Canada 2 Department of Mathematics and Statistics, University of Ottawa, Ottawa, Ontario, Canada

Received 18 April 2005; Revised 15 December 2005

In this paper, we develop a functional programming language for quantum computers, by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the “quantum data, classical control” paradigm, following the first author’s work on quantum flow-charts. We define a call-by-value operational semantics, and we give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

1. Introduction

The objective of this paper is to develop a functional programming language for quantum computers. Quantum computing is a theory of computation based on the laws of quantum physics, rather than of classical physics. While no large-scale general-purpose quantum computer has yet been built, it is known that certain hard computational problems, such as integer factoring, can theoretically be solved efficiently on a quantum computer (Shor 1994). For this and other reasons, quantum computing has become a fast growing research area in recent years. For a good introduction to the subject, see Nielsen and Chuang (2002) or Preskill (1999).

The laws of quantum physics dictate that there are only two kinds of elementary operations that one can perform on a quantum state, namely unitary transformations and measurements. Many existing formalisms for quantum computation, such as the quantum circuit model, put an emphasis on the former, i.e., a computation is understood as the evolution of a quantum state by means of unitary gates. In these models, measurements are usually performed at the end of the computation, by an outside observer who is not part of the formalism proper. This means that a quantum computer is considered as a purely quantum system, without any classical parts. Examples of such models include the quantum Turing machine (Benioff 1980; Deutsch 1985), where the entire machine state, including the tape, the finite control, and the position of the head, is assumed to be a quantum state. Another example is the quantum lambda calculus of van Tonder (2004), which is a higher-order, purely quantum language without an explicit measurement operation.

On the other hand, some models for quantum computing have been proposed that combine

† Research supported by NSERC.

unitary operations and measurements into a single formalism. One such example is the QRAM model of Knill (1996), which is also described by Bettelli, Calarco and Serafini (2003). Here, a quantum computer consists of a classical computer connected to a quantum device. The operation of the machine is controlled by a classical program that emits a sequence of instructions to the quantum device for performing measurements and unitary operations. This situation is summarized by the slogan “quantum data, classical control” (Selinger 2004). In such a model, there is no explicit need for an outside “observer”, as measurements can be performed by the device itself. Several programming languages have been proposed to deal with such a model (Bettelli, Calarco, and Serafini 2003; Sanders and Zuliani 2000), and the present paper is based on the work of Selinger (2004).

The main novelty of this paper is that we propose a higher-order quantum programming language, i.e., one in which functions can be considered as data. A typical feature of higher-order programming languages is that a program can take another program as an input (a situation called a “blackbox experiment” in physical terminology), or can produce another program as an output. There is no limit to the number of nesting levels of “programs within programs”. Higher-order programming languages are often described in terms of the lambda calculus, a prototypical formalism introduced by Church and Curry in the 1930’s, and we also follow this approach.

Because our language combines classical and quantum features, it is natural to consider two distinct basic data types: a type bit of classical bits and a type qbit of quantum bits. These two types have very different properties. For instance, the value of a classical bit can be copied as many times as needed. On the other hand, a quantum bit cannot be duplicated, due to the well-known no cloning property of quantum physics (Nielsen and Chuang 2002; Preskill 1999). We therefore introduce a type system for our language that distinguishes between types whose elements are duplicable, and types whose elements are not. This distinction not only exists at basic types, but also at higher-order types: for example, some functions of type qbit → qbit can be called an unlimited number of times (such as the identity function), whereas others can only be called once (such as the function that returns a fixed qubit ϕ of unknown state). Hence, the question of whether a function is duplicable or not cannot be directly seen from the types of its arguments or of its result, but must be determined by inspecting the types of any free variables occurring in the function definition. As we will show, the appropriate type system for higherorder quantum functions in our setting is a variant of affine intuitionistic linear logic (Girard 1987).

We specify the behavior of programs in our language in terms of an operational semantics with probabilistic reduction rules. One of the main results of this paper is a set of safety properties (subject reduction and progress) of the operational semantics with respect to well-typed programs. We also give a type inference algorithm, which can be used to determine whether a given term is typable in the linear type system, and to find a type for it. Type inference is an interesting problem for this language, because the linear type system does not satisfy the principal type property. Our algorithm is based on the idea that linear types are decorations of intuitionistic ones.

This work is based on the second author’s Master’s thesis (Valiron 2004). A preliminary version of this paper appeared in TLCA 2005.

2. Quantum computing basics

We briefly recall the basic definitions of quantum computing; please see Nielsen and Chuang (2002) or Preskill (1999) for a complete introduction to the subject. The basic unit of information in quantum computation is a quantum bit or qubit. The state of a single qubit is described by a normalized vector of the 2-dimensional Hilbert space ℂ^{2}. We denote the standard basis of ℂ^{2} as {|0⟩, |1⟩}, so that the general state of a single qubit can be written as α|0⟩ + β|1⟩, where |α|^{2} + |β|^{2} = 1. It is customary to identify any states that differ only by a global phase, i.e., α|0⟩ + β|1⟩ and α′|0⟩ + β′|1⟩ denote the same physical state if there is some scalar λ such that α′ = λα and β′ = λβ.

The state of n qubits is described by a normalized vector in ⊗_{i=1}^{n}ℂ^{2} ≅ ℂ^{2^{n}}. We write |xy⟩ = |x⟩ ⊗ |y⟩, so that a standard basis vector of ℂ^{2^{n}} can be denoted |⌜i⌝^{n}⟩, where ⌜i⌝^{n} is the binary representation of i in n digits, for 0 ⩽ i < 2^{n}. As a special case, if n = 0, we denote the unique standard basis vector in ℂ^{1} by |⟩.

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 given by a unitary 2^{n} × 2^{n}-matrix. It is common to assume that the computational model provides a certain set of built-in unitary operations, including for example the Hadamard gate H and the controlled not-gate CNOT , among others:

H = \frac{1}{\sqrt{2}} ( \begin{matrix}1 & 1 \\ 1 & −1 \end{matrix} ) , CNOT = ( \begin{matrix}1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{matrix} ) .

The measurement acts as a projection. When a qubit α|0⟩ + β|1⟩ is measured, the observed outcome is a classical bit. The two possible outcomes 0 and 1 are observed with probabilities |α|^{2} and |β|^{2}, respectively. Moreover, the state of the qubit is affected by the measurement, and collapses to |0⟩ if 0 was observed, and to |1⟩ if 1 was observed. More generally, given an n-qubit state |ϕ⟩ = α_{0}|0⟩ ⊗ |ψ_{0}⟩ + α_{1}|1⟩ ⊗ |ψ_{1}⟩, where |ψ_{0}⟩ and |ψ_{1}⟩ are normalized (n − 1)-qubit states, then measuring the leftmost qubit results in the answer i with probability |α_{i}|^{2}, and the resulting state will be |i⟩ ⊗ |ψ_{i}⟩.

3. The untyped quantum lambda calculus

3.1. Terms

Our language uses the notation of the intuitionistic lambda calculus. For a detailed introduction to the lambda calculus, see e.g. Barendregt (1984). We start from a standard lambda calculus with booleans and finite products. We extend this language with three special quantum operations, which are new, meas, and built-in n-ary gates. new maps a classical bit to a quantum bit. meas maps a quantum bit to a classical bit by performing a measurement operation; this is a probabilistic operation. Finally, we assume that there is a set 𝒰^{n} of built-in n-ary n-ary gates for each n. We use the letter U to range over built-in n-ary gates. Thus, the syntax of our language is as follows:

Term M, N, P ::= x | MN | λx.M | if M then N else P | 0 | 1 | meas
| new | U | ∗ | ⟨M, N⟩ | let ⟨x, y⟩ = M in N,

We follow Barendregt’s convention for identifying terms up to α-equivalence. We also sometimes use the shorthand notations

⟨M_{1}, …, M_{n}⟩ = ⟨M_{1}, ⟨M_{2}, … ⟩⟩,
let x = M in N = (λx.N)M,
λ⟨x, y⟩.M = λz.(let ⟨x, y⟩ = z in N).

3.2. Programs

The reader will have noticed that we have not provided a syntax for constant quantum states such as α|0⟩ + β|1⟩ in our language. One may ask why we did not allow the insertion of quantum states into a lambda term, such as λx.(α|0⟩ + β|1⟩). The reason is that, in the general case, such a syntax would be insufficient. Consider for instance the lambda term (λy.λf.fpy)(q), where p and q are entangled quantum bits in the state |pq⟩ = α|00⟩ + β|11⟩. Such a state cannot be represented locally by replacing p and q with some constant qubit expressions. The non-local nature of quantum states thus forces us to introduce a level of indirection into the representation of a state of a quantum program.

Definition 1. A program state is represented by a triple [Q, L, M], where

— Q is a normalized vector of ⊗_{i=0}^{n−1}ℂ^{2}, for some n ⩾ 0

— M is a lambda term,

— L is a function from W to {0, …, n − 1}, where FV (M) ⊆ W ⊆ 𝒱_{term}. L is also called the linking function or the qubit environment.

The purpose of the linking function is to assign specific free variables of M to specific quantum bits in Q. The notion of α-equivalence extends naturally to programs, for instance, the states [|1⟩, {x ↦ 0}, λy.x] and [|1⟩, {z ↦ 0}, λy.z] are equivalent. The set of program states, up to α-equivalence, is denoted by 𝕊.

Convention 2. In order to simplify the notation, we will often use the following convention: we use p_{i} to denote the free variable x such that L(x) = i. A program [Q, L, M] is abbreviated to [Q, M′] with M′ = M[p_{i_{1}}/x_{1}] … [p_{i_{n}}/x_{n}], where i_{k} = L(x_{k}).

3.3. Linearity

An important well-formedness property of quantum programs is that quantum bits should always be uniquely referenced: roughly, this means that no two variable occurrences should refer to the same physical quantum bit. The reason for this restriction is the well-known no-cloning property of quantum physics, which states that a quantum bit cannot be duplicated: there exists no physically meaningful operation which maps an arbitrary quantum bit |ϕ⟩ to |ϕ⟩ ⊗ |ϕ⟩.

Syntactically, the requirement of unique referencing translates into a linearity condition: A lambda abstraction λx.M is called linear if the variable x is used at most once during the evaluation of M. A well-formed program should be such that quantum data is only used linearly; however, classical data, such as ordinary bits, can of course be used non-linearly. Since the decision of which subterms must be used linearly depends on type information, we will not formally enforce any linearity constraints until we discuss a type system in Section 4; nevertheless, we will assume that all our untyped examples are well-formed in the above sense.

3.4. Evaluation strategy

As is usual in defining a programming language, we need to settle on a reduction strategy. The obvious candidates are call-by-name and call-by-value. Because of the probabilistic nature of measurement, the choice of reduction strategy affects the behavior of programs, not just in terms of efficiency, but in terms of the actual answer computed. We demonstrate this in an example. Let plus be the boolean addition function, which is definable as plus = λxy. if x then (if y then 0 else 1) else (if y then 1 else 0). Consider the term M = (λx.plus x x)(meas(H(new 0))).

Call-by-value. Reducing this in the empty environment, using the call-by-value reduction strategy, we obtain the following reductions:

⟶_{CBV} [|0⟩, (λx.plus x x)(meas(H p_{0}))]
⟶_{CBV} [\frac{1}{\sqrt{2}}(|0⟩ + |1⟩), (λx.plus x x)(meas p_{0})]

⟶_{CBV} \{ \begin{matrix}[ |0⟩, (λx.plus x x)(0)] \\ [ |1⟩, (λx.plus x x)(1)] \end{matrix}

⟶_{CBV} \{ \begin{matrix}[ |0⟩, plus 0 0] \\ [ |1⟩, plus 1 1] \end{matrix}

⟶_{CBV} \{ \begin{matrix}[ |0⟩, 0] \\ [ |1⟩, 0] \end{matrix}

where the two branches are taken with probability 1/2 each. Thus, under call-by-value reduction, this program produces the boolean value 0 with probability 1. Note that we have used Convention 2 for writing these program states.

Call-by-name. Reducing the same term under the call-by-name strategy, we obtain in one step [ |⟩, plus (meas(H(new 0))) (meas(H(new 0)))], and then with probability 1/4, [ |01⟩, 1 ], [ |10⟩, 1 ], [ |00⟩, 0 ] or [ |11⟩, 0 ]. Therefore, the boolean output of this function is 0 or 1 with equal probability.

Mixed strategy. Moreover, if we mix the two reduction strategies, the program can even reduce to an ill-formed term. Namely, reducing by call-by-value until we reach the term [\frac{1}{\sqrt{2}}(|0⟩ + |1⟩), (λx.plus x x)(meas p_{0})], and then changing to call-by-name, we obtain in one step the term [\frac{1}{\sqrt{2}}(|0⟩ + |1⟩), plus (meas p_{0}) (meas p_{0})], which is not a valid program since there are two occurrences of p_{0}.

In the remainder of this paper, we will only consider the call-by-value reduction strategy, which seems to us to be the most natural.

3.5. Probabilistic reduction systems

In order to formalize the operational semantics of the quantum lambda calculus, we need to introduce the notion of a probabilistic reduction system.

Definition 3. A probabilistic reduction system is a tuple (X, U, R, prob) where X is a set of states, U ⊆ X is a subset of value states, R ⊆ (X \ U) × X is a set of reductions, and prob : R → [0, 1] is a probability function, where [0, 1] is the real unit interval. Moreover, we impose the following conditions:

— For any x ∈ X, R_{x} = { x′ | (x, x′) ∈ R } is finite.

— ∑_{x′∈R_{x}} prob(x, x′) ⩽ 1

We call prob the one-step reduction, and denote x →_{p} y to be prob(x, y) = p. Let us extend prob to the n-step reduction

prob^{0}(x, y) = \{ \begin{matrix}0 & if x ≠ y \\ 1 & if x = y \end{matrix}
prob^{1}(x, y) = \{ \begin{matrix}prob(x, y) & if (x, y) ∈ R \\ 0 & else \end{matrix}
prob^{n+1}(x, y) = ∑_{z∈R_{x}} prob(x, z)prob^{n}(z, y),

and the notation is extended to x →_{p}^{n} y to mean prob^{n}(x, y) = p.

We say that y is reachable in one step with non-zero probability from x, denoted x →_{>0} y when x →_{p} y with p > 0. We say that y is reachable with non-zero probability from x, denoted x →_{>0}^{∗} y when there exists n ⩾ 0 such that x →_{p}^{n} y with p > 0.

We can then compute the probability to reach u ∈ U from x: It is a function from X × U to ℝ defined by prob_{U}(x, u) = ∑_{n=0}^{∞} prob^{n}(x, u). The total probability for reaching U from x is prob_{U}(x) = ∑_{n=0}^{∞} ∑_{u∈U} prob^{n}(x, u).

On the other hand, there is also the probability to diverge from x, or never reaching anything. This value is prob_{∞}(x) = lim_{n→∞} ∑_{y∈X} prob^{n}(x, y).

Lemma 4. For all x ∈ X, prob_{U}(x) + prob_{∞}(x) ⩽ 1.

We define the error probability of x to be the number prob_{err}(x) = 1−prob_{U}(x)−prob_{∞}(x).

Definition 5. We can define a notion of equivalence in X:

x ≈ y iff ∀u ∈ U \{ \begin{matrix}prob_{U}(x, u) = prob_{U}(y, u) \\ prob_{∞}(x) = prob_{∞}(y) \end{matrix}

Definition 6. In addition to the notion of reachability with non-zero probability, there is also a weaker notion of reachability, given by R: We will say that y is reachable in one step from x, written x ⇝ y, if xRy. By the properties of prob, x →_{>0} y implies x ⇝ y. As usual, ⇝^{∗} denotes the transitive reflexive closure of ⇝, and we say that y is reachable from x if x ⇝^{∗} y.

Definition 7. In a probabilistic reduction system, a state x is called an error-state if x ∉ U and ∑_{x′∈X} prob(x, x′) < 1. An element x ∈ X is consistent if there is no error-state e such that x ⇝^{∗} e.

Lemma 8. If x is consistent, then prob_{err}(x) = 0.

Remark 9. We need the weaker notion of reachability x ⇝^{∗} y, in addition to reachability with non-zero probability x →_{>0}^{∗} y, because a null probability of getting a certain result is not an absolute warranty of its impossibility. In the QRAM, suppose we have a qubit in state |0⟩. Measuring it cannot theoretically yield the value 1, but in practice, this might happen with small probability, due to imprecision of the physical operations and decoherence. Therefore, when we prove type safety (see Theorem 27), we will use the stronger notion. In short: a type-safe program should not crash, even in the event of random QRAM errors.

Remark 10. The converse of Lemma 8 is false. For instance, if X = {a, b}, U = ∅, a →_{1} a, and a →_{0} b, then b is an error state, and b is reachable from a, but only with probability zero. Hence prob_{err}(a) = 0, although a is inconsistent.

3.6. Operational semantics

We define a probabilistic call-by-value reduction procedure for the quantum lambda calculus. Note that, although the reduction itself is probabilistic, the choice of which redex to reduce at each step is deterministic.

Definition 11. A value is a term of the following form:

Value  V, W  ::=  x | λx.M | 0 | 1 | meas | new | U | ∗ | ⟨V, W ⟩.

The set of value states is 𝕍 = {[Q, L, V] ∈ 𝕊 | V ∈ Value}.

The reduction rules are shown in Table 1, where we have used Convention 2 to shorten the description of states. We write [Q, L, M] →_{p} [Q′, L′, M′] for a single-step reduction of states which takes place with probability p. In the rule for reducing the term U⟨p_{j_{1}}, …, p_{j_{n}}⟩, U is an n-ary built-in unitary gate, j_{1}, …, j_{n} are pairwise distinct, and Q′ is the quantum state obtained from Q by applying this gate to qubits j_{1}, …, j_{n}. In the rule for measurement, |Q_{0}⟩ and |Q_{1}⟩ are normalized states of the form |Q_{0}⟩ = ∑_{j} α_{j}|ϕ_{j}^{0}⟩⊗|0⟩⊗|ψ_{j}^{0}⟩ and |Q_{1}⟩ = ∑_{j} β_{j}|ϕ_{j}^{1}⟩⊗|1⟩⊗|ψ_{j}^{1}⟩, where ϕ_{j}^{0} and ϕ_{j}^{1} is an i-qubit state (so that the measured qubit is the one pointed to by p_{i}). In the rule for new, Q is an n-qubit state, so that Q ⊗ |i⟩ is an (n + 1)-qubit state, and p_{n} refers to its rightmost qubit.

We define a weaker relation ⇝. This relation models the transformations that can happen in the presence of decoherence and imprecision of physical operations. We define [Q, M] ⇝ [Q′, M′] to be [Q, M] →_{p} [Q′, M′], even when p = 0, plus the additional rule, if Q and Q′ are vectors of equal dimensions: [Q, M] ⇝ [Q′, M].

Lemma 12. Let prob be the function such that for x, y ∈ 𝕊, prob(x, y) = p if x →_{p} y and 0 else. Then (𝕊, 𝕍, ⇝, prob) is a probabilistic reduction system.

[Q, (λx.M)V] →_{1} [Q, M[V/x]] {[Q, N] →_{p} [Q′, N′] \atop [Q, MN] →_{p} [Q′, MN′]} {[Q, M] →_{p} [Q′, M′] \atop [Q, MV] →_{p} [Q′, M′V]} {[Q, M_{1}] →_{p} [Q′, M′_{1}] \atop [Q, ⟨M_{1}, M_{2}⟩] →_{p} [Q′, ⟨M′_{1}, M_{2}⟩]} {[Q, M_{2}] →_{p} [Q′, M′_{2}] \atop [Q, ⟨V_{1}, M_{2}⟩] →_{p} [Q′, ⟨V_{1}, M′_{2}⟩]}

[Q, if 0 then M else N] →_{1} [Q, N]
[Q, if 1 then M else N] →_{1} [Q, M]
[Q, U⟨p_{j_{1}}, …, p_{j_{n}}⟩] →_{1} [Q′, ⟨p_{j_{1}}, …, p_{j_{n}}⟩]
[α|Q_{0}⟩ + β|Q_{1}⟩, meas p_{i}] →_{|α|^{2}} [|Q_{0}⟩, 0]
[α|Q_{0}⟩ + β|Q_{1}⟩, meas p_{i}] →_{|β|^{2}} [|Q_{1}⟩, 1]
[Q, new 0] →_{1} [Q ⊗ |0⟩, p_{n}]
[Q, new 1] →_{1} [Q ⊗ |1⟩, p_{n}]
[Q, P] →_{p} [Q′, P′]
[Q, if P then M else N] →_{p} [Q′, if P′ then M else N]
[Q, M] →_{p} [Q′, M′]
[Q, let ⟨x_{1}, x_{2}⟩ = M in N] →_{p} [Q′, let ⟨x_{1}, x_{2}⟩ = M′ in N]
[Q, let ⟨x_{1}, x_{2}⟩ = ⟨V_{1}, V_{2}⟩ in N] →_{1} [Q, N[V_{1}/x_{1}, V_{2}/x_{2}]]

Table 1. Reductions rules of the quantum lambda calculus

This probabilistic reduction system has error states, for example, the states [Q, H(λx.x)] or [Q, U⟨p_{0}, p_{0}⟩]. Such error states correspond to run-time errors. In the next section, we introduce a type system designed to rule out such error states.

4. The typed quantum lambda calculus

We will now define a type system designed to eliminate all run-time errors arising from the reduction system of the previous section. We need base types (such as bit and qbit), function types, and product types. In addition, we need the type system to capture a notion of duplicability, as discussed in Section 3.3. We follow the notation of linear logic (Girard 1987). By default, a term of type A is assumed to be non-duplicable, and duplicable terms are given the type !A instead. Formally, the set of types is defined as follows, where α ranges over a set of type constants and X ranges over a countable set of type variables:

qType  A, B  ::= α | X | !A | (A ⊸ B) | ⊤ | (A ⊗ B)

Note that, because all terms are assumed to be non-duplicable by default, the language has a linear function type A ⊸ B and a linear product type A ⊗ B. This reflects the fact that there is in general no canonical diagonal function A → A ⊗ A. Also, ⊤ is the linear unit type. This will be made more formal in the typing rules below. We write !^{n}A for !!! …!!A, with n repetitions of !. We also write A^{n} for the n-fold tensor product A ⊗ … ⊗ A.

4.1. Subtyping

The typing rules will ensure that any value of type !A is duplicable. However, there is no harm in using it only once; thus, such a value should also have type A. For this reason, we define a subtyping relation <: as follows:

\begin{matrix}α <: α (α) & X <: X (X) & ⊤ <: ⊤ (⊤) & {A <: B \atop !A <: B} (D) & \begin{matrix}!A <: B \\ !A & <: & !B \end{matrix} (!) \\ \begin{matrix}A_{1} <: B_{1} & A_{2} <: B_{2} \\ A_{1} ⊗ A_{2} <: B_{1} ⊗ B_{2} \end{matrix} (⊗) & \begin{matrix}A <: A′ & B <: B′ \\ A′ ⊸ B <: A ⊸ B′ \end{matrix} (⊸) \end{matrix}

Lemma 13. For types A and B, if A <: B and (m = 0) ∨ (n ⩾ 1), then !^{n}A <: !^{m}B. Proof. Repeated application of (D) and (!). Notice that one can rewrite types using the notation:

qType A, B ::= !^{n}α | !^{n}X | !^{n}(A ⊸ B) | !^{n}⊤ | !^{n}(A ⊗ B)

with n ∈ ℕ. Using the overall condition on n and m that (m = 0) ∨ (n ⩾ 1), the rules can be re-written as:

\begin{matrix}!^{n}α <: !^{m}α (α_{2}) & !^{n}X <: !^{m}X (X_{2}) & !^{n}⊤ <: !^{m}⊤ (⊤_{2}) \\ \begin{matrix}A_{1} <: B_{1} & A_{2} <: B_{2} \\ !^{n}(A_{1} ⊗ A_{2}) & <: & !^{m}(B_{1} ⊗ B_{2}) \end{matrix} (⊗_{2}) & \begin{matrix}A <: A′ & & B <: B′ \\ !^{n}(A′ ⊸ B) & <: & !^{m}(A ⊸ B′) \end{matrix} (⊸_{2}) \end{matrix}

The two sets of rules are equivalent. Lemma 14. The rules of the second set are reversible.

Proof. Note that for each possible type only one rule can be used. Lemma 15. (qType, <:) is reflexive and transitive. If we define an equivalence relation ≑ by A ≑ B iff A <: B and B <: A, (qType/≑, <:) is a poset.

Proof. Both properties are shown by induction on the second set of rules. For transitivity, note that the condition (m = 0) ∨ (n ⩾ 1) can be re-written as (n = 0) ⇒ (m = 0), which is transitive. Lemma 16. If A <: !B, then there exists C such that A = !C.

Proof. A direct application of the second set of rules. Remark 17. The subtyping rules are a syntactic device, and are not intended to catch all plausible type isomorphisms. For instance, the types !A ⊗!B and !(A ⊗ B) are not subtypes of each other, although an isomorphism between these types is easily definable in the language.

4.2. Typing rules We need to define what it means for a quantum state [Q, L, M] to be well-typed. It turns out that the typing does not depend on Q and L, but only on M. We introduce typing judgments of the form Δ ▷ M : B. Here M is a term, B is a qType, and Δ is a typing context, i.e., a function from a set of variables to qType. As usual, we write |Δ| for the domain of Δ, and we denote typing

{A <: B \atop Δ, x:A ▷ x : B} (var)  {A_{c} <: B \atop Δ ▷ c : B} (const)
Γ_{1},!Δ ▷ P : bit Γ_{2},!Δ ▷ M : A Γ_{2},!Δ ▷ N : A
Γ_{1}, Γ_{2},!Δ ▷ if P then M else N : A

(if )

\begin{matrix}Γ_{1},!Δ ▷ M : A ⊸ B & Γ_{2},!Δ ▷ N : A \\ Γ_{1}, Γ_{2},!Δ ▷ MN : B \end{matrix} (app)

{x:A, Δ ▷ M : B \atop Δ ▷ λx.M : A ⊸ B} (λ_{1})  \begin{matrix}If F V (M) ∩ |Γ| = ∅: \\ Γ,!Δ, x:A ▷ M : B \end{matrix} ; Γ,!Δ ▷ λx.M : !^{n+1}(A ⊸ B) (λ_{2})
\begin{matrix}!Δ, Γ_{1} ▷ M_{1} : !^{n}A_{1} & !Δ, Γ_{2} ▷ M_{2} : !^{n}A_{2} \\ !Δ, Γ_{1}, Γ_{2} ▷ ⟨M_{1}, M_{2}⟩ : !^{n}(A_{1} ⊗ A_{2}) \end{matrix} (⊗.I)  Δ ▷ ∗ : !^{n}⊤ (⊤)
!Δ, Γ_{1} ▷ M : !^{n}(A_{1} ⊗ A_{2}) !Δ, Γ_{2}, x_{1}:!^{n}A_{1}, x_{2}:!^{n}A_{2} ▷ N : A

!Δ, Γ_{1}, Γ_{2} ▷ let ⟨x_{1}, x_{2}⟩ = M in N : A (⊗.E)

Table 2. Typing rules

contexts as x_{1}:A_{1}, …, x_{n}:A_{n}. As usual, we write Δ, x:A for Δ ∪ {x:A} if x ∉ |Δ|. Also, if Δ = x_{1}:A_{1}, …, x_{n}:A_{n}, we write !Δ = x_{1}:!A_{1}, …, x_{n}:!A_{n}. A typing judgment is called valid if it can be derived from the rules in Table 2.

The typing rule (ax) assumes that to every constant c of the language, we have associated a fixed type A_{c}. The types A_{c} are defined as follows:

A_{0} = !bit  A_{new} = !(bit ⊸ qbit)
A_{1} = !bit  A_{meas} = !(qbit ⊸!bit)  A_{U} = !(qbit^{n} ⊸ qbit^{n})

Note that we have given the type !(bit ⊸ qbit) to the term new. Another possible choice would have been !(!bit ⊸ qbit), which makes sense because all classical bits are duplicable. However, since !(bit ⊸ qbit) <: !(!bit ⊸ qbit), the second type is less general, and can be inferred by the typing rules.

The shorthand notations have the required behavior:

!Δ, Γ_{1}, x:A ▷ N:B !Δ, Γ_{2} ▷ M:A !Δ, Γ_{1}, Δ_{2} ▷ let x = M in N:B, {!Δ, Γ, x:A, y:B ▷ M:C \atop !Δ, Γ ▷ λ⟨x, y⟩.M:(A ⊗ B) ⊸ C},

and if FV (M) ∩ |Γ| = ∅, {!Δ, Γ, x:!^{n}A, y:!^{n}B ▷ M:C \atop !Δ, Γ ▷ λ⟨x, y⟩.M:!^{m+1}(!^{n}(A ⊗ B) ⊸ C)} are provable.

Note that, if [Q, L, M] is a program state, the term M need not be closed; however, all of its free variables must be in the domain of L, and thus must be of type qbit. We therefore define:

Definition 18. A program state [Q, L, M] is well-typed of type B if Δ ▷ M : B is derivable, where Δ = {x: qbit | x ∈ FV (M)}. In this case, we write [Q, L, M] : B.

Note that the type system enforces that variables holding quantum data cannot be duplicated; thus, λx.⟨x, x⟩ is not a valid term of type qbit⊸qbit⊗qbit. On the other hand, we allow variables to be discarded freely. Other approaches are also possible, for instance, Altenkirch and Grattage (2004) propose a syntax that allows duplication but restricts discarding of quantum values.

[figure: qubit 1:; |ϕ⟩; •; H; (1); (2); M; (3); x,y; qubit 2:; |0⟩; H; •; ⊕; qubit 3:; |0⟩; ⊕; location B; location A; U_{xy}; (4); |ϕ⟩]

Table 3. Quantum teleportation protocol

4.3. Example: quantum teleportation

Let us illustrate the quantum lambda calculus and the typing rules with an example. The following is an implementation of the well-known quantum teleportation protocol (see e.g. Nielsen and Chuang (2002)). The purpose of the teleportation protocol is to send a qubit from location A to location B, using only classical communication and a pre-existing shared entangled quantum state. In fact, this can be achieved by communicating only the content of two classical bits. In the usual quantum circuit formalism, the teleportation protocol is described in Table 3.

The state |ϕ⟩ of the first qubit is “teleported” from location A to location B. The important point of the protocol is that the only quantum interaction between locations A and B (shown as (1) in the illustration) can be done ahead of time, i.e., before the state |ϕ⟩ is prepared.

The dashed box M (shown as (3)) represents a measurement of two qubits. The gate U_{xy} (shown as (4)) depends on two classical bits x and y, which are the result of this measurement. It is defined as:

U_{00} = ( \begin{matrix}1 & 0 \\ 0 & 1 \end{matrix} ) , U_{01} = ( \begin{matrix}0 & 1 \\ 1 & 0 \end{matrix} ) , U_{10} = ( \begin{matrix}1 & 0 \\ 0 & −1 \end{matrix} ) , U_{11} = ( \begin{matrix}0 & 1 \\ −1 & 0 \end{matrix} ) .

The teleportation protocol consists of four steps:

(1) Create an entangled state \frac{1}{\sqrt{2}}(|00⟩ + |11⟩) between qubits 2 and 3.

(2) At location A, rotate qubits 1 and 2.

(3) At location A, measure qubits 1 and 2, obtaining two classical bits x and y.

(4) At location B, apply the correct transformation U_{xy} to qubit 3.

Proof of the correctness of the teleportation protocol. The rotation (2) has the following effect:

CNOT  H ⊗ id
|00⟩  ↦  |00⟩  ↦  \frac{1}{\sqrt{2}}(|00⟩ + |10⟩),
|01⟩  ↦  |01⟩  ↦  \frac{1}{\sqrt{2}}(|01⟩ + |11⟩),
|10⟩  ↦  |11⟩  ↦  \frac{1}{\sqrt{2}}(|01⟩ − |11⟩),
|11⟩  ↦  |10⟩  ↦  \frac{1}{\sqrt{2}}(|00⟩ − |10⟩).

If we apply it to the two first qubits of

(α|0⟩ + β|1⟩) ⊗ \frac{1}{\sqrt{2}}(|00⟩ + |11⟩) = \frac{1}{\sqrt{2}}(α|000⟩ + α|011⟩ + β|100⟩ + β|111⟩)

we get

\frac{1}{2}(α(|000⟩ + |100⟩) + α(|011⟩ + |111⟩) + β(|010⟩ − |110⟩) + β(|001⟩ − |101⟩))
= \frac{1}{2}(|00⟩ ⊗ (α|0⟩ + β|1⟩) + |01⟩ ⊗ (α|1⟩ + β|0⟩)
+|10⟩ ⊗ (α|0⟩ − β|1⟩) + |11⟩ ⊗ (α|1⟩ − β|0⟩))

If we measure the two first qubits, the third qubit becomes

α|0⟩ + β|1⟩ if 00 was measured,
α|1⟩ + β|0⟩ if 01 was measured,
α|0⟩ − β|1⟩ if 10 was measured,
α|1⟩ − β|0⟩ if 11 was measured.

Finally, note that if U_{xy} is applied in the case where x, y was measured, then the state of the last qubit is α|0⟩ + β|1⟩ = |ϕ⟩.

To express the quantum teleportation protocol in our quantum lambda calculus, we implement each part of the protocol as a function. We define three functions

EPR :  !(⊤ ⊸ (qbit ⊗ qbit))
BellMeasure : !(qbit ⊸(qbit ⊸ bit ⊗ bit))
U :  !(qbit ⊸(bit ⊗ bit ⊸ qbit))

The function EPR corresponds to step (1) of the protocol, and creates an entangled 2-qubit state. The function BellMeasure corresponds to steps (2) and (3), and takes two qubits, rotates and measures them. The function U corresponds to step (4). It takes a qubit q and two bits x, y and returns U_{xy}q. These functions are defined as follows:

EPR  = λx.CNOT ⟨H(new 0), new 0⟩,

BellMeasure = λq_{2}.λq_{1}.(let ⟨p, p′⟩ = CNOT ⟨q_{1}, q_{2}⟩

in ⟨ meas(Hp), meas p′⟩),

U = λq.λ⟨x, y⟩. if x then (if y then U_{11}q else U_{10}q)

else (if y then U_{01}q else U_{00}q),

where U_{xy} are defined as above when the measured qubits were x and y.

The teleportation procedure can be seen as the creation of two non-duplicable functions f and g

f : qbit ⊸ bit ⊗ bit, g : bit ⊗ bit ⊸ qbit,

such that g ∘ f(q) = q for an arbitrary qubit q. We can construct such a pair of functions by the following code:

let ⟨p, p′⟩ = EPR ∗ in let f = BellMeasure p in let g = U p′ in ⟨f, g⟩.

Note that, since f and g depend on the state of the qubits p and p′, respectively, these functions cannot be duplicated, which is reflected in the fact that the types of f and g do not contain a top-level “!”. The detailed typing derivation of these terms, and a proof that g(f(q)) → q, using the reduction rules of Table 1, are given in the Appendix.

Superdense coding. The two functions f and g generated for the quantum teleportation protocol also satisfy a dual property, namely (f ∘ g)⟨x, y⟩ = ⟨x, y⟩, for an arbitrary pair of classical bits ⟨x, y⟩. This property can be used to send two classical bits along a channel that can hold a single quantum bit, in the presence of a pre-existing shared entangled quantum state. This procedure is known as superdense coding (see Nielsen and Chuang (2002)), and it is dual to quantum teleportation. A detailed proof of (f ∘ g)⟨x, y⟩ → ⟨x, y⟩ from the reduction rules is given in the Appendix.

Remark 19. Note that the types qbit and bit ⊗bit are clearly not isomorphic. However, we have f : qbit ⊸ bit ⊗ bit and g : bit ⊗ bit ⊸ qbit such that f ∘ g = id and g ∘ f = id. This is not a contradiction, of course, because each of f and g can only be used once, and therefore they are not isomorphisms in the usual sense. We might describe such a pair of functions as a pair of “single-use isomorphisms”.

While this behavior of the functions f and g, and the corresponding properties of teleportation and superdense coding, are well-understood in quantum mechanics, this is still something of a mystery to us in the context of programming language semantics. We are not aware of any other situation in programming languages that produces such single-use isomorphisms.

4.4. Properties of the type system

We derive some basic properties of the type system.

Definition 20. We extend the subtyping relation to contexts by writing Δ <: Δ′ if |Δ′| = |Δ| and for all x in |Δ′|, Δ_{f}(x) <: Δ′_{f}(x).

Lemma 21.

(1) If x ∉ FV (M) and Δ, x:A ▷ M:B, then Δ ▷ M:B.

(2) If Δ ▷ M:A, then Γ, Δ ▷ M:A.

(3) If Γ <: Δ and Δ ▷ M : A and A <: B, then Γ ▷ M : B.

Proof. By structural induction on the type derivation of M.

The next lemma is crucial in the proof of the substitution lemma. Note that it is only true for a value V, and in general fails for an arbitrary term M.

Lemma 22. If V is a value and Δ ▷ V : !A, then for all x ∈ FV (V), there exists some U ∈ qType such that Δ(x) = !U.

Proof. By induction on V.

— If V is a variable x, then the last rule in the derivation was {B <: !A \atop Δ′, x : B ▷ x : !A} . Since

B <: !A, B must be exponential by Lemma 16.

— If V is a constant c, then FV (V) = ∅, hence the result holds vacuously.

— If V = λx.M, the only typing rule that applies is (λ_{2}), and Δ = Γ,!Δ′ with F V (M) ∩ |Δ′| = ∅. So every y ∈ FV (M) except maybe x is exponential. Since FV (λx.M) = (FV (M) \ {x}), this suffices.

— The remaining cases are similar.

Lemma 23 (Substitution). If V is a value such that Γ_{1},!Δ, x:A ▷ M : B and Γ_{2},!Δ ▷ V : A, then Γ_{1}, Γ_{2},!Δ ▷ M[V/x] : B.

Proof. By structural induction on the derivation of Γ_{1},!Δ, x:A ▷ M : B.

Corollary 24. If Γ_{1},!Δ, x:A ▷ M : B and Γ_{2},!Δ ▷ V : !^{n}A, then Γ_{1}, Γ_{2},!Δ ▷ M[V/x] : B.

Proof. From Lemma 23 and Lemma 21(3).

Remark 25. We note that all the usual rules of affine intuitionistic linear logic are derived rules of our type system, except for the general promotion rule. Indeed, ▷ new 0 : qbit is valid, but ▷ new 0 : !qbit is not. However, the promotion rule is derivable when V is a value:

{!Γ ▷ V : A \atop !Γ ▷ V :!A}.

4.5. Subject reduction and progress

Theorem 26 (Subject Reduction). Given a well-typed program [Q, L, M]:B such that [Q, L, M]⇝^{∗} [Q′, L′, M′], then [Q′, L′, M′] : B.

Proof. It suffices to show this for [Q, L, M] →_{p} [Q′, L′, M′], and we proceed by induction on the rules in Table 1. The rule [Q, (λx.M)V] →_{1} [Q, M[V/x]] and the rule for “let” use the substitution lemma. The remaining cases are direct applications of the induction hypothesis.

Theorem 27 (Progress). Let [Q, L, M] : B be a well typed program. Then [Q, L, M] is not an error state in the sense of Definition 7. In particular, either [Q, L, M] is a value, or else there exist some state [Q′, L′, M′] such that [Q, L, M]→_{p} [Q′, L′, M′]. Moreover, the total probability of all possible single-step reductions from [Q, L, M] is 1.

Corollary 28. Every sequence of reductions of a well-typed program either converges to a value, or diverges.

The proof of the Progress Theorem is similar to the usual proof, with two small differences. The first is the presence of probabilities, and the second is the fact that M is not necessarily closed. However, all the free variables of M are of type qbit, and this property suffices to prove the following lemma, which generalizes the usual lemma on the shape of closed well-typed values:

Lemma 29. Suppose Δ = x_{1}:qbit, …, x_{n}:qbit, and V is a value. If Δ ▷ V:A ⊸ B, then V is new, meas, U, or a lambda abstraction. If Δ ▷ V:A ⊗ B, then V = ⟨V_{1}, V_{2}⟩. If Δ ▷ V:bit, then V = 0 or V = 1.

Proof. By inspection of the typing rules.

Proof of the Progress Theorem. By induction on M. The claim follows immediately in the cases when M is a value, or when M is a left-hand-side of one of the rules in Table 1 that have no hypotheses. Otherwise, using Lemma 29, M is one of the following: P N, NV, ⟨N, P ⟩, ⟨V, N⟩, if N then P else Q, let ⟨x, y⟩ = N in P, where N is not a value. In this case, the free variables of N are still all of type qbit, and by induction hypothesis, the term [Q, L, N] has reductions with total probability 1, and the rules in Table 1 ensure that the same is true for [Q, L, M].

5. Type inference algorithm

It is well-known that the simply-typed lambda calculus, as well as many programming languages, satisfies the principal type property: every untyped expression has a most general type, provided that it has any type at all. Since most principal types can usually be determined automatically, the programmer can be relieved from the need to write any types at all.

In the context of our quantum lambda calculus, it would be nice to have a type inference algorithm; however, the principal type property fails due to the presence of exponentials !A. Not only can an expression have several different types, but in general none of the types is “most general”. For example, the term M = λxy.xy has possible types T_{1} = (A ⊸ B) ⊸ (A ⊸ B) and T_{2} = !(A ⊸ B) ⊸!(A ⊸ B), among others. Neither of T_{1} and T_{2} is a substitution instance of the other, and in fact the most general type subsuming T_{1} and T_{2} is X ⊸ X, which is not a valid type for M. Also, neither of T_{1} and T_{2} is a subtype of the other, and the most general type of which they are both subtypes is (A ⊸ B) ⊸!(A ⊸ B), which is not a valid type for M.

In the absence of the principal type property, we need to design a type inference algorithm based on a different idea. The approach we follow is the one suggested by Danos, Joinet, and Schellinx (1995). The basic idea is to view a linear type as a “decoration” of an intuitionistic type. Our type inference algorithm is based on the following technical fact, given below: if a given term has an intuitionistic type derivation π of a certain kind, then it is linearly typable if and only if there exists a linear type derivation which is a decoration of π. Typability can therefore be decided by first doing intuitionistic type inference, and then checking finitely many possible linear decorations.

5.1. Skeletons and decorations

The class of intuitionistic types is

iType  U, V  ::=  α | X | (U ⇒ V) | (U × V) | ⊤

where α ranges over the type constants and X over the type variables.

To each A ∈ qType, we associate its type skeleton^{†}A ∈ iType, which is obtained by removing all occurrences of “!”. Conversely, every U ∈ iType can be lifted to some^{♣}U ∈ qType with no occurrences of “!”. Formally:

Definition 30. Define functions † : qType → iType and ♣ : iType → qType by:

\begin{matrix}^{†}!^{n}α = α, ^{†}!^{n}X = X, ^{†}!^{n}⊤ = ⊤, \\ ^{†}!^{n}(A ⊸ B) = ^{†}A ⇒^{†}B, \\ ^{†}!^{n}(A ⊗ B) = ^{†}A ×^{†}B, \end{matrix}  \begin{matrix}^{♣}α = α, ^{♣}X = X, ^{♣}⊤ = ⊤, \\ ^{♣}(U ⇒ V) = ^{♣}U ⊸^{♣}V , \\ ^{♣}(U × V) = ^{♣}U ⊗^{♣}V . \end{matrix}

If U = ^{†}A, then we also say that A is a decoration of U.

Lemma 31. If A <: B, then^{†}A = ^{†}B. If U ∈ iType, then U = ^{†}^{♣}U.

Writing Δ ▶ M : U for a typing judgment of the simply-typed lambda calculus, we can extend the notion of skeleton to contexts, typing judgments, and derivations as follows:

\begin{aligned}^{†}\{x_{1}:A_{1}, …, x_{n}:A_{n}\} & = & \{x_{1}:^{†}A_{1}, …, x_{n}:^{†}A_{n}\} \\ ^{†}(Δ ▷ M : A) & = & (^{†}Δ ▶ M : ^{†}A). \end{aligned}

From the rules in Table 2, it is immediate that if Δ ▷ M : A is a valid typing judgment in the quantum lambda calculus, then ^{†}(Δ ▷ M : A) = (^{†}Δ ▶ M : ^{†}A) is a valid typing judgment in the simply-typed lambda calculus.

5.2. Decorating intuitionistic type derivations

The basic idea of our quantum type inference algorithm is the following: given a term M, first find an intuitionistic typing judgment Δ ▶ M : U, say with type derivation π, if such a typing exists. Then look for a quantum type derivation which is a decoration of π. Clearly, if the term M is not quantum typable, this procedure will fail to yield a quantum typing of M. For the algorithm to be correct, we also need the converse property to be true: if M has any quantum type derivation, then it has a quantum type derivation which is a decoration of the given intuitionistic derivation π. We therefore would ideally like to prove the following property:

Property 32 (desired). Let M be a term with an intuitionistic type derivation π. Then M is quantum typable if and only if there exists a quantum type derivation π′ of M such that^{†}π′ = π.

Unfortunately, this property is false, as the following example shows.

Example 33. Consider the term M = (λx. meas x)(new 0). Clearly this term is quantum typable, for instance, it has type bit (also !bit, !!bit etc.). Consider the following intuitionistic type derivation π for M:

x : qbit ▶ meas : qbit ⇒ bit x : qbit ▶ x : qbit

x : qbit ▶ meas x : bit ▶ λx. meas x : qbit ⇒ bit

▶ new : bit ⇒ qbit ▶ 0 : bit
▶ new 0 : qbit

▶ (λx. meas x)(new 0) : bit

This particular intuitionistic type derivation is not the skeleton of any valid quantum type derivation of M. To see this, note that the variable x has been duplicated in the typing rule for meas x. Therefore, any valid decoration of π has to give the type !qbit to x. On the other hand, the only valid quantum type for new 0 is qbit, which is not a subtype of !qbit. Hence, there is no quantum type derivation for M whose skeleton is π, demonstrating that Property 32 fails.

5.3. Normal derivations

The reason Property 32 fails is because an intuitionistic derivation can duplicate variables unnecessarily, as shown in Example 33. The duplication of a variable in a typing rule is unnecessary if the variable does not actually occur in one of the premises. We can avoid this problem by slightly changing the typing rules to disallow such unnecessary duplications. This is done by eliminating all “dummy” variables from typing contexts.

Definition 34. A typing judgment Δ ▷ M : A of the quantum lambda calculus is called normal if |Δ| = FV (M). If Δ ▷ M : A is any typing judgment, then its normal form is Δ|_{FV (M)} ▷ M : A. We also write Δ|_{M} for Δ|_{FV (M)}. If π is a type derivation, then its normal form is the derivation 𝒩(π) obtained by taking the normal form of each of its nodes.

Note that the normal form of a type derivation is not necessarily a type derivation in the strict sense, because the rules of Table 2 are not invariant under taking normal forms. However, we can define a new set of typing rules, called the normal typing rules, which are obtained by normalizing the rules from Table 2. For example, the new rule for application is:

{Γ_{1},!Δ}|_{FV (M)} ▷ M : A ⊸ B {Γ_{2},!Δ}|_{FV (N)} ▷ N : A
{Γ_{1}, Γ_{2},!Δ}|_{FV (MN)} ▷ MN : B

(app_{norm})

We treat all the other typing rules analogously.

Lemma 35. Let Δ ▷ M : A be any typing judgment. Then Δ ▷ M : A is derivable from the rules in Table 2 if and only if Δ|_{FV (M)} ▷ M : A is derivable from the normal typing rules.

Proof. The left-to-right implication follows by normalizing the type derivation of Δ ▷ M : A. The opposite implication follows because the normal typing rules are admissible by Lemma 21.

The normal form of intuitionistic typing judgments, rules, and derivations is defined analogously. The counterpart of Lemma 35 also holds in the intuitionistic case.

Relative to the normal typing rules, the analog of Property 32 holds.

Theorem 36. Let M be a term with a normal intuitionistic type derivation π. Then M is quantum typable if and only if there exists a normal quantum type derivation π′ of M such that^{†}π′ = π.

5.4. Proof of Theorem 36

The proof of Theorem 36 requires us to find a suitable decoration π′ of π. For this purpose we are going to introduce the concept of the decoration of an intuitionistic type along a quantum type. Intuitively, U ↬ A takes the skeleton from U and the exponentials from A.

Definition 37. Given A ∈ qType and U ∈ iType, we define the decoration U ↬ A ∈ qType of U along A by

U ↬ !^{n}A = !^{n}(U ↬ A),
(U ⇒ V) ↬ (A ⊸ B) = (U ↬ A) ⊸ (V ↬ B),
(U × V) ↬ (A ⊗ B) = (U ↬ A) ⊗ (V ↬ B),
in all other cases: U ↬ A = ^{♣}U.

Lemma 38. If U, V ∈ iType and A, B ∈ qType, then the following are true:

(a) ^{†}(U ↬ A) = U,

(b) If ^{†}A = U then U ↬ A = A,

(c) If A <: B then (U ↬ A) <: (U ↬ B).

Definition 39. Let Γ be an intuitionistic typing context, and Δ a quantum typing context, such that |Γ| ⊆ |Δ|. Then we define Γ ↬ Δ := Γ′, where |Γ′| = |Γ|, and for all x in |Γ|, Γ′(x) = Γ(x) ↬ Δ(x). This notation is extended to typing judgments in the following way, provided that |Γ| ⊆ |Δ|:

(Γ ▶ M : U) ↬ (Δ ▷ M : A) := Γ ↬ Δ ▷ M : U ↬ A,

and to type derivations by structural induction, provided that the intuitionistic derivation is normal.

Lemma 40. If π is a normal intuitionistic type derivation and if ρ is any quantum type derivation, then π′ := (π ↬ ρ) is a normal quantum type derivation.

Proof. By structural induction on ρ, and by case distinction on the last typing rule used. For instance, suppose the last rule used was the (app) rule. Then M = NP and the type derivation ρ ends in

\begin{matrix}{⋮ . ρ_{1} \atop Δ_{1},!Δ_{3} ▷ N : A ⊸ B} & {⋮ . ρ_{2} \atop Δ_{2},!Δ_{3} ▷ P : A} \\ Δ_{1}, Δ_{2},!Δ_{3} ▷ NP : B \end{matrix}

In normal intuitionistic lambda calculus the type derivation π is of the form:

{⋮ . π_{1} \atop Γ|_{FV (N)} ▶ N : U ⇒ V} {⋮ . π_{2} \atop Γ|_{FV (P)} ▶ P : U}
Γ|_{FV (NP)} ▶ NP : V

Writing Γ|_{X} for Γ|_{FV (X)}, the type derivation π ↬ ρ is

{⋮ . π_{1} ↬ ρ_{1} \atop Γ|_{N} ↬ (Δ_{1},!Δ_{3}) ▷ N : (U ⇒ V) ↬ (A ⊸ B)} {⋮ . π_{2} ↬ ρ_{2} \atop Γ|_{P} ↬ (Δ_{2},!Δ_{3}) ▷ P : U ↬ A}
Γ|_{NP} ↬ (Δ_{1}, Δ_{2},!Δ_{3}) ▷ NP : V ↬ B.

By induction hypothesis, π_{1} ↬ ρ_{1} and π_{2} ↬ ρ_{2} are quantum normal type derivations. If we write Γ_{i} for Γ|_{domΔ_{i}} ↬ Δ_{i}, using Lemma 38 and the definition of ↬, the last rule of the derivation above becomes:

\begin{matrix}\{Γ_{1},!Γ_{3}\}|_{N} ▷ N : (U ↬ A) ⊸ (V ↬ B) & \{Γ_{2},!Γ_{3}\}|_{P} ▷ P : U ↬ A \\ \{Γ_{1}, Γ_{2},!Γ_{3}\}|_{NP} ▷ NP : V ↬ B, \end{matrix}

which is an instance of the normal quantum (app) rule. Thus π′ := (π ↬ ρ) is a normal quantum type derivation. The other typing rules are treated similarly.

Proof of Theorem 36. For the left-to-right implication, if ρ is some quantum type derivation of M, we can define π′ = (π ↬ ρ) as in Lemma 40. Then ^{†}π′ = π follows from Lemma 38. The right-to-left implication follows trivially from Lemma 35.

5.5. Elimination of repeated exponentials

The type system in Section 4 allows types with repeated exponentials such as !!A. While this is useful for compositionality, it is not very convenient for type inference. We therefore consider a reformulation of the typing rules which only requires single exponentials.

Definition 41. For A ∈ qType, we define ^{#}A ∈ qType to be the result of erasing multiple exponentials in A. Formally, if σ(0) = 0 and σ(n + 1) = 1,

\begin{matrix}^{#}!^{n}α = !^{σ(n)}α, ^{#}!^{n}X = !^{σ(n)}X, ^{#}!^{n}⊤ = !^{σ(n)}⊤, \\ ^{#}!^{n}(A ⊸ B) = !^{σ(n)}(^{#}A ⊸^{#}B), ^{#}!^{n}(A ⊗ B) = !^{σ(n)}(^{#}A ⊗^{#}B), \end{matrix}

We also extend this operation to typing contexts and judgments in the obvious way.

Lemma 42. The following are derived rules of the type system in Table 2, for all τ, σ ∈ {0, 1}.

\begin{matrix}!Δ, Γ_{1} ▷ M_{1} : !A_{1} & !Δ, Γ_{2} ▷ M_{2} : !A_{2} \\ !Δ, Γ_{1}, Γ_{2} ▷ ⟨M_{1}, M_{2}⟩ : !(!^{τ} A_{1} ⊗!^{σ}A_{2}) \end{matrix} (⊗.I′)
!Δ, Γ_{1} ▷ M : !(!^{τ} A_{1} ⊗!^{σ}A_{2}) !Δ, Γ_{2}, x_{1}:!A_{1}, x_{2}:!A_{2} ▷ N : A

!Δ, Γ_{1}, Γ_{2} ▷ let ⟨x_{1}, x_{2}⟩ = M in N : A (⊗.E′)

Further, the normal forms of (⊗.I′) and (⊗.E′) are derivable in the normal type system.

Proof. Suppose !Δ, Γ_{1} ▷ M_{1} : !A_{1} and !Δ, Γ_{2} ▷ M_{2} : !A_{2} are derivable. Since !A_{1} <: !!^{τ} A_{1} and !A_{2} <: !!^{σ}A_{2}, therefore !Δ, Γ_{1} ▷ M_{1} : !!^{τ} A_{1} and !Δ, Γ_{2} ▷ M_{2} : !!^{σ}A_{2} are also derivable by Lemma 21(3). But then !Δ, Γ_{1}, Γ_{2} ▷ ⟨M_{1}, M_{2}⟩ : !(!^{τ} A_{1} ⊗!^{σ}A_{2}) follows from rule (⊗.I). The proof of the second rule is similar. Finally, the last claim follows from Lemma 35.

Lemma 43. If π is a derivation of a typing judgment Δ ▷ M : A from the normal quantum typing rules, then ^{#}π is a valid normal derivation of ^{#}Δ ▷ M : ^{#}A, possibly using the normal forms of (⊗.I′) and (⊗.E′) as additional rules. Moreover,^{†}π = ^{†}^{#}π.

Proof. By inspection of the rules. For each normal typing rule r, ^{#}r is either an instance of the same rule, or of the normal form of (⊗.I′) or (⊗.E′).

5.6. Description of the type inference algorithm

Theorem 36 yields a simple type inference algorithm. Given a term M, we can perform type inference in the quantum lambda calculus in three steps:

(1) Find an intuitionistic type derivation π of M, if any.

(2) Eliminate “dummy” variables to obtain its normal form 𝒩π.

(3) Find a decoration of 𝒩π which is a valid normal quantum type derivation, if any. Step (1) is known to be decidable, and step (2) is computationally trivial. By Theorem 36, step (3) will succeed if and only if M is quantum typable. Note that by Lemma 43, it suffices to consider decorations of 𝒩π without repeated exponentials. Since there are only finitely many such decorations, step (3) is clearly decidable. Also note that if the algorithm succeeds, then it returns a possible type for M. However, it does not return a description of all possible types.

Remark 44 (Efficiency of the algorithm). In principle, the search space of all possible decorations of 𝒩π is exponential in size. However, this space can be searched efficiently by solving a system of constraints. More precisely, if we create a boolean variable for each place in the type derivation which potentially can hold a “!”, then the constraints imposed by the linear type system can all be written in the form of implications x_{1} ∧ … ∧ x_{n} ⇒ y, where n ⩾ 0, and negations ¬z. It is well-known that such a system can be solved in polynomial time in the number of variables and clauses. Therefore, the type inference problem can be solved in time polynomial in the size of the type derivation π.

Note, however, that the size of an intuitionistic type derivation π need not be polynomial in the size of the term M, because in the worst case, π can contain types that are exponentially larger than M. We do not presently know whether quantum typability can be decided in time polynomial in M.

6. Conclusion and further work

In this paper, we have defined a higher-order quantum programming language based on a linear typed lambda calculus. Compared to the quantum lambda calculus of van Tonder (2004), our language is characterized by the fact that it contains classical as well as quantum features; for instance, we provide classical datatypes and measurements as a primitive feature of our language. Moreover, we provide a subject reduction result and a type inference algorithm. As the language shows, linearity constraints do not just exist at base types, but also at higher types, due to the fact that higher-order functions are represented as closures, which may in turns contain embedded quantum data. We have shown that a version of affine intuitionistic linear logic provides the right type system to deal with this situation.

There are many open problems left for further work. Several interesting variations of the language presented here need to be explored in more detail. For instance, we have not included a syntax for recursive function definitions in this paper. We believe that this can be done, but the details are more subtle than we first expected. Another obvious extension is to add the additive types of linear logic to the system. One may also study alternative reduction strategies. In this paper, we have considered the call-by-value strategy, because it conforms with our intuition of quantum computation as being essentially value-driven. However, a call-by-name strategy is also conceivable and would lead to a very different semantics and type system. Finally, an important problem that we have not addressed here is how to give a denotational semantics for higher order quantum programming languages. This appears to be a difficult problem and is the subject of ongoing research.

Appendix A. Examples

A.1. Example: Type derivation of the teleportation protocol

To illustrate the linear type system from Section 4.2, we give a complete derivation of the type of the quantum teleportation term from Section 4.3. The notation (L.x.y) means that Lemma.x.y is used.

A lambda calculus for quantum computation with classical control 21 Computing some subtypes:

1 α_{2}  !^{n}α <: α
2 α_{2}  !^{m}β <: β
3 ⊸_{2}, 1, 2  !^{k}(α ⊸!^{m}β) <: (!^{n}α ⊸ β)
4 (L.15)  A <: A
5 D, 4  !A <: A

Computing the type of EPR:

6 const, 3  ▷ new : bit ⊸ qbit
7 const, 5  ▷ 0: bit
8 app, 6, 7  ▷ new 0: qbit
9 const, 3  ▷ H: qbit ⊸ qbit
10 app, 9, 8  ▷ H(new 0): qbit
11 ⊗.I, 10, 9 ▷ ⟨H(new 0), new 0⟩ : qbit ⊗ qbit
12 const, 3  x:⊤ ▷ CNOT :(qbit ⊗ qbit) ⊸ (qbit ⊗ qbit)
13 app, 12, 11 x:⊤ ▷ CNOT ⟨H(new 0), new 0⟩: qbit ⊗ qbit
14 λ_{2}, 13  ▷ λx.CNOT ⟨H(new 0), new 0⟩:!(⊤ ⊸ (qbit ⊗ qbit))

Computing the type of BellMeasure:

15 var, 1  y:qbit ▷ y:qbit
16 const, 3  ▷ meas :qbit ⊸ bit
17 app, 16, 15 y: qbit ▷ meas y:bit
18 var, 1  x: qbit ▷ x:qbit
19 app, 9, 18 x:qbit ▷ Hx:qbit
20 app, 16, 19 x: qbit ▷ meas(Hx):bit
21 var, 1  q_{1}: qbit ▷ q_{1}: qbit
22 var, 1  q_{2}: qbit ▷ q_{2}: qbit
23 ⊗.I, 21, 22 q_{2}: qbit, q_{1}: qbit ▷ ⟨q_{1}, q_{2}⟩: qbit ⊗ qbit
24 const, 3  ▷ CNOT :(qbit ⊗ qbit) ⊸ (qbit ⊗ qbit)
25 app, 24, 23 q_{2}: qbit, q_{1}: qbit ▷ CNOT ⟨q_{1}, q_{2}⟩: qbit ⊗ qbit
26 ⊗.I, 20, 17 x: qbit, y: qbit ▷ ⟨ meas(Hx), meas y⟩: bit ⊗ bit
27 ⊗.E, 25, 26 q_{2}: qbit, q_{1}: qbit ▷ let ⟨x, y⟩ = CNOT ⟨q_{1}, q_{2}⟩

in⟨ meas(Hx), meas y⟩: bit ⊗ bit

28 λ_{1}, 27  q_{2}: qbit ▷ λq_{1}.(let ⟨x, y⟩ = CNOT ⟨q_{1}, q_{2}⟩

in ⟨ meas(Hx), meas y⟩):qbit ⊸ bit ⊗ bit

29 λ_{2}, 28  ▷ λq_{2}.λq_{1}.(let ⟨x, y⟩ = CNOT ⟨q_{1}, q_{2}⟩

in ⟨ meas(Hx), meas y⟩):!(qbit ⊸(qbit ⊸ bit ⊗ bit))

Computing the type of U:

30 var, 1  q:qbit ▷ q:qbit
31 const, 3  ▷ U_{ij}:qbit ⊸ qbit
32 app, 30, 31 q:qbit ▷ U_{ij}q:qbit
33 var, 1  y:bit ▷ y:!bit
34 var, 1  x:bit ▷ x:!bit
35 if , 33, 32, 32 q:qbit, y:bit ▷ if y then U_{i1}q else U_{i0}q:qbit
36 if , 34, 35, 35 q:qbit, x:bit, y:bit ▷ if x then (if y then U_{11}q else U_{10}q)
else (if y then U_{01}q else U_{00}q): qbit
37 ⊸′_{1}, 36  q:qbit ▷ λ⟨x, y⟩.if x then (if y then U_{11}q else U_{10}q)
else (if y then U_{01}q else U_{00}q): bit ⊗ bit ⊸ qbit
38 ⊸_{2}, 37  ▷ λq.λ⟨x, y⟩.if x then (if y then U_{11}q else U_{10}q)
else (if y then U_{01}q else U_{00}q):!(qbit ⊸(bit ⊗ bit ⊸ qbit))

Finally, computing the type of the pair ⟨f, g⟩:

39 ⊤  ▷ ∗:⊤
40 (L.21), 14, 5 ▷ EPR:⊤ ⊸ (qbit ⊗ qbit)
41 app, 40, 39 ▷ EPR ∗:qbit ⊗ qbit
42 (L.21), 29, 5 ▷ BellMeasure:qbit ⊸ (qbit ⊸ bit ⊗ bit)
43 var, 1  x:qbit ▷ x:qbit
44 app, 42, 43 x:qbit ▷ BellMeasure x: qbit ⊸ bit ⊗ bit
45 var, 1  y:qbit ▷ y:qbit
46 (L.21), 38, 5 ▷ U: qbit ⊸(bit ⊗ bit ⊸ qbit)
47 app, 46, 45 y:qbit ▷ U y: bit ⊗ bit ⊸ qbit
48 var, 1  f:qbit ⊸ bit ⊗ bit ▷ f:qbit ⊸ bit ⊗ bit
49 var, 1  g: bit ⊗ bit ⊸ qbit ▷ g: bit ⊗ bit ⊸ qbit
50 ⊗, 48, 49  g: bit ⊗ bit ⊸ qbit, f: qbit ⊸ bit ⊗ bit ▷ ⟨f, g⟩:

(qbit ⊸ bit ⊗ bit) ⊗ (bit ⊗ bit ⊸ qbit)

51 let, 47, 50  f: qbit ⊸ bit ⊗ bit, y:qbit ▷ let g = U y in ⟨f, g⟩:

(qbit ⊸ bit ⊗ bit) ⊗ (bit ⊗ bit ⊸ qbit)

52 let, 44, 51  x:qbit, y:qbit ▷ let f = BellMeasure x in let g = U y

in⟨f, g⟩):(qbit ⊸ bit ⊗ bit) ⊗ (bit ⊗ bit ⊸ qbit)

53 let, 41, 52  ▷ let ⟨x, y⟩ = EPR ∗ in let f = BellMeasure x

in let g = U y in ⟨f, g⟩)):

(qbit ⊸ bit ⊗ bit) ⊗ (bit ⊗ bit ⊸ qbit)

A.2. Example: Reduction of the teleportation term

As an illustration of the reduction rules of the quantum lambda calculus we show the detailed reduction of the term from the teleportation example from Section 4.3. The reduction of the A lambda calculus for quantum computation with classical control 23 teleportation term corresponds to the equality g ∘ f = id. We use the following abbreviations:

M_{p,p′} := let f = BellMeasure p in let g = U p′ in g(f p_{0})
B_{p_{1}} := λq_{1}.(let ⟨p, p′⟩ = CNOT ⟨q_{1}, p_{1}⟩ in ⟨ meas(Hp), meas p′⟩)
U_{p_{2}} := λ⟨x, y⟩. (if xthen (if y then U_{11}p_{2} else U_{10}p_{2}) else (if y then U_{01}p_{2} else U_{00}p_{2}))

The reduction of the term is then as follows:

[α|0⟩ + β|1⟩, \begin{matrix}let ⟨p, p′⟩ = EPR ∗ \\ in let f = BellMeasure p \\ in let g = U p′ \\ in g(f p_{0}) \end{matrix} ]
→_{1} [α|0⟩ + β|1⟩, let ⟨p, p′⟩ = CNOT ⟨H(new 0), new 0⟩ in M_{p,p′}]
→_{1} [(α|0⟩ + β|1⟩) ⊗ |0⟩, let ⟨p, p′⟩ = CNOT ⟨Hp_{1}, new 0⟩ in M_{p,p′}]
→_{1} [(α|0⟩ + β|1⟩) ⊗ \frac{1}{\sqrt{2}}(|0⟩ + |1⟩), let ⟨p, p′⟩ = CNOT ⟨p_{1}, new 0⟩ in M_{p,p′}]
→_{1} [(α|0⟩ + β|1⟩) ⊗ \frac{1}{\sqrt{2}}(|0⟩ + |1⟩) ⊗ |0⟩, let ⟨p, p′⟩ = CNOT ⟨p_{1}, p_{2}⟩ in M_{p,p′}]
→_{1} [(α|0⟩ + β|1⟩) ⊗ \frac{1}{\sqrt{2}}(|00⟩ + |11⟩), let ⟨p, p′⟩ = ⟨p_{1}, p_{2}⟩ in M_{p,p′}]
→_{1} [(α|0⟩ + β|1⟩) ⊗ \frac{1}{\sqrt{2}}(|00⟩ + |11⟩), \begin{matrix}let f = BellMeasure p_{1} \\ in let g = U p_{2} \\ in g(f p_{0}) \end{matrix} ]
→_{1}^{∗} [(α|0⟩ + β|1⟩) ⊗ \frac{1}{\sqrt{2}}(|00⟩ + |11⟩), U_{p_{2}}(B_{p_{1}}p_{0})]
→_{1} [(α|0⟩ + β|1⟩) ⊗ \frac{1}{\sqrt{2}}(|00⟩ + |11⟩), U_{p_{2}} ( \begin{matrix}let ⟨p, p′⟩ = CNOT ⟨p_{0}, p_{1}⟩ \\ in ⟨ meas(Hp), meas p′⟩ \end{matrix} )]
→_{1} [\frac{1}{\sqrt{2}} ( \begin{matrix}α|000⟩ + α|011⟩ \\ +β|110⟩ + β|101⟩ \end{matrix} ) , U_{p_{2}} ( \begin{matrix}let ⟨p, p′⟩ = ⟨p_{0}, p_{1}⟩ \\ in ⟨ meas(Hp), meas p′⟩ \end{matrix} )]
→_{1} [\frac{1}{\sqrt{2}} ( \begin{matrix}α|000⟩ + α|011⟩ \\ +β|110⟩ + β|101⟩ \end{matrix} ) , U_{p_{2}}⟨ meas(Hp_{0}), meas p_{1}⟩]
→_{1} [\frac{1}{2} ( \begin{matrix}α|000⟩ + α|011⟩ \\ +α|100⟩ + α|111⟩ \\ +β|010⟩ + β|001⟩ \\ −β|110⟩ − β|101⟩ \end{matrix} ) , U_{p_{2}}⟨ meas p_{0}, meas p_{1}⟩]

{

[figure: \frac{1}{2}; \frac{1}{2}] [\frac{1}{\sqrt{2}} ( \begin{matrix}α|000⟩ + α|011⟩ \\ +β|010⟩ + β|001⟩ \end{matrix} ) , U_{p_{2}}⟨0, meas p_{1}⟩]

[\frac{1}{\sqrt{2}} ( \begin{matrix}α|100⟩ + α|111⟩ \\ −β|110⟩ − β|101⟩ \end{matrix} ) , U_{p_{2}}⟨1, meas p_{1}⟩]

\begin{matrix}\{ & [figure: 1/2; 1/2; 1/2; 1/2] & \begin{matrix}[(α|000⟩ + β|001⟩) , U_{p_{2}}⟨0, 0⟩] \\ [(α|011⟩ + β|010⟩) , U_{p_{2}}⟨0, 1⟩] \\ [(α|100⟩ − β|101⟩) , U_{p_{2}}⟨1, 0⟩] \\ [(α|111⟩ − β|110⟩) , U_{p_{2}}⟨1, 1⟩] \end{matrix} \begin{matrix}→_{1} & ∗ & [(α|000⟩ + β|001⟩) , U_{00}p_{2}] \\ →_{1} & ∗ & [(α|011⟩ + β|010⟩) , U_{01}p_{2}] \\ →_{1} & ∗ & [(α|100⟩ − β|101⟩) , U_{10}p_{2}] \\ →_{1} & ∗ & [(α|111⟩ − β|110⟩) , U_{11}p_{2}] \end{matrix} \\ \{ & \begin{matrix}→_{1} \\ →_{1} \\ →_{1} \\ →_{1} \end{matrix} & \begin{matrix}[ (α|000⟩ + β|001⟩), p_{2} ] \\ [ (α|010⟩ + β|011⟩), p_{2} ] \\ [ (α|100⟩ + β|101⟩), p_{2} ] \\ [ (α|110⟩ + β|111⟩), p_{2} ] \end{matrix}\begin{matrix}= [ |00⟩ ⊗ (α|0⟩ + β|1⟩), p_{2} ] \\ = [ |01⟩ ⊗ (α|0⟩ + β|1⟩), p_{2} ] \\ = [ |10⟩ ⊗ (α|0⟩ + β|1⟩), p_{2} ] \\ = [ |11⟩ ⊗ (α|0⟩ + β|1⟩), p_{2} ] \end{matrix} \end{matrix}

A.3. Example: Reduction of the superdense coding term

As another example of the reduction rules, we give the reduction of the superdense coding example from Section 4.3. This reduction shows the equality f ∘ g = id. Of the four possible cases, we only give one case, namely (f ∘ g)⟨0, 1⟩ = ⟨0, 1⟩; the remaining cases are similar. We use the same abbreviations as above.

[|⟩, \begin{matrix}let ⟨p, p′⟩ = EPR ∗ \\ in let f = BellMeasure p \\ in let g = U p′ \\ in f(g⟨0, 1⟩) \end{matrix} ]

→_{1}^{∗} [\frac{1}{\sqrt{2}}(|00⟩ + |11⟩), \begin{matrix}let f = BellMeasure p_{0} \\ in let g = U p_{1} \\ in f(g⟨0, 1⟩) \end{matrix} ]

→_{1}^{∗} [\frac{1}{\sqrt{2}}(|00⟩ + |11⟩), B_{p_{0}}(U_{p_{1}}⟨0, 1⟩)]
→_{1}^{∗} [\frac{1}{\sqrt{2}}(|00⟩ + |11⟩), B_{p_{0}}(U_{01}p_{1})]
→_{1} [\frac{1}{\sqrt{2}}(|01⟩ + |10⟩), B_{p_{0}}p_{1}]
→_{1} [\frac{1}{\sqrt{2}}(|01⟩ + |10⟩), let ⟨p, p′⟩ = CNOT ⟨p_{1}, p_{0}⟩ in ⟨ meas(Hp), meas p′⟩]
→_{1} [\frac{1}{\sqrt{2}}(|11⟩ + |10⟩), let ⟨p, p′⟩ = ⟨p_{1}, p_{0}⟩ in ⟨ meas(Hp), meas p′⟩]
→_{1} [\frac{1}{\sqrt{2}}(|11⟩ + |10⟩), ⟨ meas(Hp_{1}), meas p_{0}⟩]
→_{1} [|10⟩, ⟨ meas p_{1}, meas p_{0}⟩]
→_{1}^{∗} [|10⟩, ⟨0, 1⟩]

References

T. Altenkirch and J. Grattage. A functional quantum programming language. Available from arXiv:quant-

ph/0409065, 2004. H. P. Barendregt. The Lambda-Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the

Foundation of Mathematics. North Holland, second edition, 1984.

A lambda calculus for quantum computation with classical control 25

P. Benioff. The computer as a physical system: A microscopic quantum mechanical Hamiltonian model of

computers as represented by Turing machines. Journal of Statistical Physics, 22:563–591, 1980. S. Bettelli, T. Calarco, and L. Serafini. Toward an architecture for quantum programming. The European

Physical Journal D, 25(2):181–200, August 2003. V. Danos, J.-B. Joinet, and H. Schellinx. On the linear decoration of intuitionistic derivations. Archive for

Mathematical Logic, 33:387–412, 1995. D. Deutsch. Quantum theory, the Church-Turing principle and the universal quantum computer. Proceed-

ings of the Royal Society of London. Series A, Mathematical and Physical Sciences, 400(1818):97–117, July 1985.

J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–101, 1987. E. Knill. Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National

Laboratory, 1996. M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information. Cambridge University

Press, 2002. J. Preskill. Lecture notes for Physics 229, Quantum Computation. Available from http://www.theory.

caltech.edu/people/preskill/ph229/#lecture, 1999. J. W. Sanders and P. Zuliani. Quantum programming. In R. Backhouse and J. N. Oliveira, editors, Mathe-

matics of Program Construction: 5th International Conference, volume 1837 of Lecture Notes in Computer Science, pages 80–99, Ponte de Lima, Portugal, July 2000. Springer-Verlag.

P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science,

14(4):527–586, 2004. P. W. Shor. Algorithms for quantum computation: Discrete log and factoring. In Proceedings of the 35th

Annual Symposium on Foundations of Computer Science, pages 124–134. Institute of Electrical and Electronic Engineers Computer Society Press, November 1994.

B. Valiron. A functional programming language for quantum computation with classical control. Master’s

thesis, University of Ottawa, September 2004. A. van Tonder. A lambda calculus for quantum computation. SIAM Journal of Computing, 33(5):1109–

1135, 2004. Available from arXiv:quant-ph/0307150.