                         QPL 2006 Preliminary Version

On a fully abstract model for a quantum linear functional language (extended abstract)

Peter Selinger^{1 ,2}

Dalhousie University, Halifax, Nova Scotia, Canada

Benoît Valiron^{3}

University of Ottawa, Ottawa, Ontario, Canada

Abstract This paper studies the linear fragment of the programing language for quantum computation with classical control described in [4]. We sketch the language, and discuss equivalence of terms. We also describe a fully abstract denotational semantics based on completely positive maps. Keywords: Quantum computing, functional programming, linear lambda calculus, higher order, semantics.

1 Introduction

This work studies a linear functional programming language for quantum computation with classical control, derived from the language in [4].

The first denotational semantics of a quantum programming language was given by the first author in [3], for the quantum flowchart language QFC. The semantics given there was compositional and took place in a category of superoperators, which are special completely positive maps. However, the language lacked a crucial feature found in functional programming languages, namely, the notion of higher-order functions.

In [4], we sought to address this omission by introducing a typed lambda calculus for quantum computation. This language resembles QFC in that it combines quantum and classical data types with classical control features, but it also includes lambda abstractions and therefore function closures. The problem of deciding the

1 Research supported by NSERC.

2 Email: selinger@mathstat.dal.ca
3 Email: bvali087@uottawa.ca

This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Selinger and Valiron

duplicability of data was solved syntactically, by giving a type system that distinguishes duplicable and non-duplicable types. The quantum lambda calculus possesses a reduction semantics, but no denotational semantics has been given for it so far.

In this paper, we study the restriction of the quantum lambda calculus to the purely linear case. This means we study the fragment of the language where each value, classical and quantum, must be used exactly once. The linear quantum lambda calculus differs from its nonlinear cousin in that it is less sensitive to the evaluation order of terms. We give a denotational semantics for this language in a category of completely positive maps, and we show that it is fully abstract with respect to the operational semantics.

The question of finding a denotational semantics for the full quantum lambda calculus is still open, but we hope that this work is a step in that direction.

The plan of the paper is as follows. First we briefly describe the language and the type system. Then we develop an operational semantics for it, and we define a notion of equivalence of terms. Finally we build a denotational semantics for the language, and we show the full abstraction result.

2 A linear lambda-calculus for quantum computation

In [4], we have defined an operational semantics for a lambda calculus for quantum computation with classical control. Here, we study the purely linear fragment of this language. We begin by re-adapting the definitions and results from this earlier paper for the linear setting.

2.1 Terms and Programs

Definition 2.1 The linear quantum lambda calculus has the following terms:

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 [1]. The set of free variables of a term M is written FV (M). We also sometimes use the shorthand notation ⟨M_{1}, …, M_{n}⟩ = ⟨M_{1}, ⟨M_{2}, … ⟩⟩. In the following, we often write c for an arbitrary constant of the language, i.e., 0, 1, meas, new, U, or ∗.

The set of types is defined by

A, B ::= bit | qbit | A ⊸ B | ⊤ | A ⊗ B.

Note that, unlike the language of [4], there is no type constructor !A. We use the same shortcut for the product type as we did for the product term, to define A ⊗ … ⊗ A. To each constant term c, we associate a fixed type A_{c}, namely meas : qbit ⊸ bit, 0, 1 : bit, new : bit ⊸ qbit, ∗ : ⊤ and U : qbit^{⊗n} ⊸ qbit^{⊗n}. A typing judgement is a triple Δ ▷ M : A, where Δ is a list of distinct typed variables called a typing context, M is a term, and A is a type. We say that a typing judgement is valid if it follows from the typing rules given in Table 1.

x : A ▷ x : A (ax_{1})  ▷ c : A_{c} (ax_{2})
Γ_{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}Γ_{1} ▷ M_{1} : A_{1} & Γ_{2} ▷ M_{2} : A_{2} \\ Γ_{1}, Γ_{2} ▷ ⟨M_{1}, M_{2}⟩ : A_{1} ⊗ A_{2} \end{matrix} (⊗.I)  ▷ ∗ : ⊤ (⊤) Δ ▷ Ω : A (Ω)
Γ_{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)

Table 1 Typing rules for the linear quantum lambda calculus

Although this language is intended to manipulate quantum information, no constants of type qbit are provided in the definition of lambda-terms. Indeed, while it would be possible to allow constant qubit expressions such as α|0⟩ + β|1⟩, such a notation would not lend itself to expressing entangled states. Instead, we introduce the concept of a quantum array and a linking function to express terms with embedded quantum data.

Definition 2.2 A quantum closure is a triple [Q, L, M] where Q is a normalized vector in ⊗_{i=1}^{n}ℂ^{2}, for some n ⩾ 0, L is a bijective function from a set |L| of term variables to {0, …, n − 1}, and M is a term. Q is called a quantum array, and L is called a linking function. We write |Q| = n. If L(x_{i}) = i, we will sometimes write L as the ordered list |x_{1} ⋯ x_{n}⟩. The idea is that the variable x_{i} is bound in the term M to qubit number L(x_{i}) of the state Q. We also call the pair (Q, L) a quantum context.

We extend the notion of α-equivalence to quantum closures:

[Q, |x ⋯ y ⋯ z⟩, M] =_{α} [Q, |x ⋯ y′ ⋯ z⟩, M[y′/y]]

if y ∉ FV (M) ∪ |L|.

Definition 2.3 A quantum closure [Q, L, M] is well-typed (or valid) of type A in the typing context Γ, written Γ ⊨ [Q, L, M] : A, if |L| ∩ |Γ| = ∅ and Γ, x_{1}:qbit, …, x_{k}:qbit ▷ M : A is a valid typing judgement, where {x_{1} … x_{k}} = |L| ∩ FV (M).

A well-typed quantum closure is closed if |Γ| = ∅, and a closed well-typed quantum closure is also called a program.

A well-typed quantum closure is called a computation if |L| ⊆ FV (M), or equivalently, if FV (M) = |L| ∪ |Γ|.

3 Operational semantics

3.1 Small step semantics

The language contains a probabilistic operation: the measurement. This probabilistic operation forces us to choose a reduction strategy.

[Q, L, Ω] →_{1}^{ω} [Q, L, Ω]  [Q, L, (λx.M)V] →_{1}^{β} [Q, L, M[V/x]]

[Q, L, let ⟨x_{1}, x_{2}⟩ = ⟨V_{1}, V_{2}⟩ in N] →_{1}^{let} [Q, L, N[V_{1}/x_{1}, V_{2}/x_{2}]]

[Q, L, if 0 then M else N] →_{1}^{if_{0}} [Q, L, N]

[Q, L, if 1 then M else N] →_{1}^{if_{1}} [Q, L, M]

{[Q, L, N] →_{p}^{κ} [Q′, L′, N′] \atop [Q, L, MN] →_{p}^{κ} [Q′, L′, MN′]} ; {[Q, L, M_{1}] →_{p}^{κ} [Q′, L′, M′_{1}] \atop [Q, L, ⟨M_{1}, M_{2}⟩] →_{p}^{κ} [Q′, L′, ⟨M′_{1}, M_{2}⟩]} {[Q, L, M] →_{p}^{κ} [Q′, L′, M′] \atop [Q, L, MV] →_{p}^{κ} [Q′, L′, M′V]} ; {[Q, L, M_{2}] →_{p}^{κ} [Q′, L′, M′_{2}] \atop [Q, L, ⟨V_{1}, M_{2}⟩] →_{p}^{κ} [Q′, L′, ⟨V_{1}, M′_{2}⟩]}

[Q, L, P] →_{p}^{κ} [Q′, L′, P′] [Q, L, if P then M else N] →_{p}^{κ} [Q′, L′, if P′ then M else N]

[Q, L, M] →_{p}^{κ} [Q′, L′, M′] [Q, L, let ⟨x_{1}, x_{2}⟩ = M in N] →_{p}^{κ} [Q′, L′, let ⟨x_{1}, x_{2}⟩ = M′ in N]

Table 2 Reduction rules for the quantum lambda calculus

Definition 3.1 We define the call-by-value reduction strategy for the linear quantum lambda calculus by structural induction. For this purpose we need the notion of a value. We define a value term to be of the form V, W ::= x | c | λx.M | ⟨V, W ⟩. A value program is a program of the form [Q, L, V], where V is a value term. The rules for the reduction are an adaptation of the ones found in [4].

We set the rules to be the “classical” ones found in Table 2, plus the following “quantum” rules. In the first two rules, let Q = ∑_{j} Q_{j}^{0} ⊗ α_{j}|0⟩ ⊗ Q̃_{j}^{0} + ∑_{j} Q_{j}^{1} ⊗ β_{j}|1⟩ ⊗ Q̃_{j}^{1}, where Q_{j}^{b} ∈ ℂ^{2^{i−1}} and Q̃_{j}^{b} ∈ ℂ^{2^{n−i}}.

[Q, |x_{1} ⋯ x_{n}⟩, meas x_{i}] →_{|α|^{2}}^{m_{0}} [∑_{j} Q_{j}^{0} ⊗ Q̃_{j}^{0}, |x_{1} ⋯ x_{i−1}x_{i+1} ⋯ x_{n}⟩, 0],
[Q, |x_{1} ⋯ x_{n}⟩, meas x_{i}] →_{|α|^{2}}^{m_{1}} [∑_{j} Q_{j}^{1} ⊗ Q̃_{j}^{1}, |x_{1} ⋯ x_{i−1}x_{i+1} ⋯ x_{n}⟩, 1].

If w is a fresh term variable not yet in use:

[Q, |x_{1} ⋯ x_{n}⟩, new 0] →_{1}^{n_{0}} [Q ⊗ |0⟩, |x_{1} ⋯ x_{n}w⟩, w],
[Q, |x_{1} ⋯ x_{n}⟩, new 1] →_{1}^{n_{1}} [Q ⊗ |1⟩, |x_{1} ⋯ x_{n}w⟩, w].

If Q′ is the result of applying U to the quantum bits L(x_{1}), …, L(x_{n}) in Q:

[Q, L, U⟨x_{1}, …, x_{n}⟩] →_{1}^{U} [Q′, L, ⟨x_{1}, …, x_{n}⟩].

Note that since we want a linear language, we modified the measurement rule from [4] by deleting the quantum bit measured from the quantum array.

Lemma 3.2 (Substitution) If Δ, x : A ▷ M : B and if Γ ▷ N : A then Δ, Γ ▷ M[N/x] : B is a valid typing judgement.

Note that, in the non-linear case, the Substitution Lemma only holds when N = V is a value. However, in the linear calculus considered here, it holds for general N.

Theorem 3.3 (Safety properties) If P is a closed valid computation of type A, either it is a value or P →_{ρ} P′ , with P′ a closed valid computation of type A.

Proof. The proof is an adaptation of the proof of Theorems 1 and 2 in [4]. ⊓ ⊔

The language being linear, the reduction has a strong relation on the length of the terms.

Definition 3.4 Let l(M) be the length of a term M, defined recursively as l(x) = l(c) = l(Ω) = 1, l(λx.M) = l(M) + 1, l(let ⟨x, y⟩ = M in N) = l(M) + l(N) + 1, l(if P then M else N) = l(P) + max(l(M), l(N)), l(MN) = l(⟨M, N⟩) = l(M) + l(N) + 1.

Lemma 3.5 If x ∈ FV (M), then l(M[N/x]) = l(M) + l(N) − 1.

Lemma 3.6 If [Q, L, M] →_{ρ}^{x} [Q′, L′, M′], then either x ≠ ω and l(M′) < l(M) or x = ω and l(M′) = l(M). In the latter case, [Q, L, M] = [Q′, L′, M′].

Definition 3.7 A program [Q, L, M] that reduces with a ω-rule is called a fixed point.

Theorem 3.8 (Strong Normalization) If P = [Q, L, M] is a closed valid computation, P reduces to a value or to a fixed point in at most l(M) steps.

Proof. Follows from Lemma 3.6. ⊓ ⊔

3.2 Quantum context and reduction

When describing the reduction rules, we carefully separated the quantum context from the lambda-term. In this subsection we show that the precise order of quantum bits in the quantum array does not matter.

Definition 3.9 If σ is a permutation of {1, …, n}, we extend σ to ℕ with σ(j) = j for j > n, and we define σ̄ to be the corresponding permutation of quantum bits σ̄|x_{1} ⋯ x_{n} ⋯ x_{n+k}⟩ = |x_{σ(1)} ⋯ x_{σ(n)}x_{n+1} ⋯ x_{n+k}⟩. We say that (Q_{1}, L_{1}) is σ-equivalent to (Q_{2}, L_{2}) if Q_{1} and Q_{2} have the same size, Q_{2} = σ̄(Q_{1}) and L_{2} = σ^{−1} ∘ L_{1}. We write (Q_{1}, L_{1}) =_{α}^{σ} (Q_{2}, L_{2}). We define an equivalence relation called alpha-equivalence on quantum contexts by (Q_{1}, L_{1}) =_{α} (Q_{2}, L_{2}) if there exists a σ such that (Q_{1}, L_{1}) =_{α}^{σ} (Q_{2}, L_{2}).

The alpha-equivalence is sound with respect to the semantics:

Lemma 3.10 If [Q, L, M] →_{p} [Q′, L′, M′] then [σ̄Q, σL, M] →_{p} [σ̄Q′, σL′, M′].

3.3 Reduction to values

In the reduction process, what we are really seeking is the final result of the computation. In this section we explicate the relation of programs to values.

Definition 3.11 We informally recall a notion defined in [4]: If X is the set of closed valid programs and U the set of values, let prob_{U} : X × U → [0, 1] be the map prob_{U}(P, V) that returns the total probability for a program P to end up on the value V in zero or more steps. This function is called the big-step reduction.

We also define the small-step reduction operation prob : X × X → [0, 1]: for closed programs P, P′, we define prob(P, P′) = p if there is a single-step probabilistic reduction P →_{p} P′, prob(V, V) = 1 if V is a value program, and prob(P, P′) = 0 in all other cases. Note that for all well-typed P, ∑_{P′∈X} prob(P, P′) = 1.

Definition 3.12 If P is a closed well-typed program of type bit, and b ∈ {0, 1}, we define (P ⇓ b) = ∑_{V ∈U_{b}} prob′(P, V), where U_{b} is the set of valid programs with term the value b. We say that P evaluates to b with probability P ⇓ b.

Definition 3.13 We define a formal probability distribution of quantum closures to be Γ ⊨ ∑_{i} ρ_{i}[Q_{i}, L_{i}, M_{i}] : A, where each Γ ⊨ [Q_{i}, L_{i}, M_{i}] : A is valid and ∑ ρ_{i} ⩽ 1. The distribution is said to be closed if |Γ| = ∅.

Lemma 3.14 Given a set Z, let 𝒞Z be the set of probability distributions over it. The small-step reduction prob : X × X → [0, 1] can be curried to a map prob′ : 𝒞X → 𝒞X: prob′(∑_{i} α_{i}P_{i}) = ∑_{i} α_{i} ∑_{P′∈X} prob(P_{i}, P′)P′. Similarly, prob_{U} : X × U → [0, 1] can be curried to a map prob′_{U} : 𝒞X → 𝒞U: prob′_{U}(∑_{i} α_{i}P_{i}) = ∑_{i} α_{i}prob_{U}(P_{i}, V)V. The definition of P ⇓ b can be extended in the same way to probability distributions of programs.

Lemma 3.15 If ⊨ P : A is valid, so is ⊨ prob′P : A and ⊨ prob′_{U}P : A.

Due to the strong normalization theorem, applying the map prob′_{U} is applying the map prob′ finitely many times.

Proposition 3.16 If [Q, L, M] is a closed valid computation, then the reduction verifies

prob^{′l(M)}[Q, L, M] = ∑_{i=1}^{n} ρ_{i}[Q_{i}, L_{i}, V_{i}] + ∑_{j=1}^{m} ρ′_{j}P_{j},

with prob′_{U}[Q, L, M] = ∑_{i=1}^{n} ρ_{i}[Q_{i}, L_{i}, V_{i}], the P_{j} being fixed points, ∑_{i} ρ_{i} +∑_{j} ρ′_{j} = 1, and n + m < 2^{l(M)}.

4 Denotational semantics

In [3] the notion of completely positive map is used to model the notion of quantum computation. We aim to show that the linear subset of the quantum lambda calculus has the category CPM as a fully abstract model. Note that the interpretation will not be “onto” all completely positive maps, but will only be “onto up to scalar multiplies”. In this section we set the definition of the denotational semantics.

4.1 The category CPM

We recall the definition of the category V [3].

• The objects are signatures σ = n_{1}, …, n_{k}, i.e., finite tuples of positive integers,

\begin{aligned}[[x : A ▷ x : A]](v) & = & v & [[▷ 0 : bit]](x) & = & (x, 0) \\ [[▷ ∗ : ⊤]](x) & = & x & [[▷ 1 : bit]](x) & = & (0, x) \end{aligned}

[[Δ ▷ Ω : A]] = 0 : [[Δ]] → [[A]]
[[▷ new : bit ⊸ qbit]] = Φ(ι) : 1 → [[bit]] ⊗ [[qbit]]
[[▷ meas : qbit ⊸ bit]] = Φ(p) : 1 → [[qbit]] ⊗ [[bit]]
[[▷ U : qbit^{⊗n} ⊸ qbit^{⊗n}]] = Φ(U) : 1 → 2^{2n}

\begin{aligned}[[Δ, x : A ▷ M : B]] & = & f : [[Δ]] ⊗ [[A]] → [[B]] \\ [[Δ ▷ λx.M : A ⊸ B]] & = & Φ(f) : [[Δ]] → [[A]] ⊗ [[B]] \end{aligned}

[[Δ ▷ M : A ⊸ B]] = Φ(g) : [[Δ]] → [[A]] ⊗ [[B]]
[[Γ ▷ N : A]] = f : [[Γ]] → [[A]]
[[Δ, Γ ▷ MN : B]] : x ⊗ y ↦ g(x ⊗ (fy)) : [[Δ]] ⊗ [[Γ]] → [[B]]
[[Δ ▷ P : bit]] : x ↦ (px, qx) : [[Δ]] → [[bit]]
[[Γ ▷ M : A]] = f : [[Γ]] → [[A]]
[[Γ ▷ N : A]] = g : [[Γ]] → [[A]]
[[Δ, Γ ▷ if P then M else N : A]] : x ⊗ y ↦ (px)(fy) + (qx)(gy)
[[Δ ▷ M : A]] = f : [[Δ]] → [[A]]
[[Γ ▷ N : B]] = g : [[Γ]] → [[B]]
[[Δ, Γ ▷ ⟨M, N⟩ : A ⊗ B]] : x ⊗ y ↦ fx ⊗ gy : [[Δ]] ⊗ [[Γ]] → [[A]] ⊗ [[B]]

Table 3 Denotational semantics for typing judgments.

• the arrows σ → σ′ are linear maps V_{σ} → V_{σ′}, where V_{n_{1},...,n_{k}} = ℂ^{n_{1}×n_{1}} × … × ℂ^{n_{k}×n_{k}}.

There is a tensor product (n_{1}, …, n_{k}) ⊗ (m_{1}, …, m_{l}) = n_{1}m_{1}, …, n_{1}m_{l}, n_{2} m_{1}, …, n_{k}m_{l} and a canonical isomorphism V_{σ⊗τ} ≃ V_{σ} ⊗V_{τ}. Thus V has a structure of symmetric monoidal closed category. The unit element is the signature 1. From the vector spaces property, V(σ ⊗ τ, σ′) =_{Φ} V(σ, τ ⊗ σ′): If B(τ) is a basis for V_{τ}, then from f ∈ V(σ ⊗ τ, σ′) we construct g = Φ(f) ∈ V(σ, τ ⊗ σ′) by g(s) = ∑_{b∈B(τ)} b ⊗ f(s ⊗ b). Conversely, given such a g, if g(s) = ∑_{b∈B(τ),u∈B(σ′)} α_{b,u}b ⊗ u, one constructs f = Φ^{−1}(g) by f(s ⊗ t) = ∑_{u∈B(σ′)} α_{t,u}u. This makes V monoidal closed.

The category CPM has the same objects as V and as arrows completely positive maps (see [3]).

4.2 Modeling the quantum lambda-calculus

We set the denotation of types to be [[bit]] = (1, 1), [[A ⊗ B]] = [[A]]⊗[[B]], [[qbit]] = 2, and [[A ⊸ B]] = [[A]] ⊗ [[B]], and the denotation of contexts to be

[[x_{1} : A_{1}, …, x_{n} : A_{n}]] = [[A_{1}]] ⊗ ⋯ ⊗ [[A_{n}]], [[∅]] = 1.

The denotation for typing judgments of the form Δ ▷ M : A is a linear map [[Δ]] → [[A]], defined inductively as in Table 3. Here, Φ : hom(A ⊗ B, C) → hom(A, B ⊗ C) is the bijection from the compact closed structure and ι and p are respectively the quantum bits creation and the measurement operation:

\begin{aligned}ι : & 1, 1 & → & 2 & p : & 2 & ↦ & 1, 1 \\ & (a, b) & ↦ & ( \begin{matrix}a & 0 \\ 0 & b \end{matrix} ) & & ( \begin{matrix}a & b \\ c & d \end{matrix} ) & ↦ & (a, d) \end{aligned}

We also define the denotation for a computation. Consider the valid computation Δ ⊨ [Q, L, M] : A where L = |x_{1} ⋯ x_{n}⟩ and |Q| = n. The quantum context (Q, L) can be seen as a map g : 1 → 2^{⊗n} such that g(1) = Q. Then if

[[Δ, x_{1} : qbit, …, x_{n} : qbit ▷ M : A]] = f : [[Δ]] ⊗ 2^{⊗n} → [[A]],

one defines [[Δ ⊨ [Q, L, M] : A]] as the composition

\xymatrix{[[Δ]] \ar[r]^{id_{[[Δ]]}⊗g} & [[Δ]] ⊗ 2^{⊗n} \ar[r]^{f} & [[A]].}

One extends this definition to probabilistic distributions of computations using linearity:

[[Δ ⊨ ∑_{i} ρ_{i}P_{i}]] = ∑_{i} ρ_{i}[[Δ ⊨ P_{i}]].

Lemma 4.1 Denotations of terms and computations are completely positive maps.

Lemma 4.2 (Substitution) If |Γ| ∩ |Δ| = ∅ and [[Δ, x : A ▷ M : B]] = G : [[Δ]] ⊗ [[A]] → [[B]], [[Γ ▷ N : A]] = F : [[Γ]] → [[A]], then [[Δ, Γ ▷ M[N/x] : B]] = H : [[Δ]] ⊗ [[Γ]] → [[B]], with H(d ⊗ g) = G(d ⊗ (F g))

Lemma 4.3 Given a valid closed computation P : A with prob′P = ∑_{i} ρ_{i}P_{i} then [[P : A]] = [[prob′P : A]] = [[prob′_{U}P : A]].

4.3 Fullness of the semantics for the first order fragment

Proposition 4.4 For any types A = U_{1} ⊗ ⋯ ⊗ U_{n} and B = V_{1} ⊗ ⋯ ⊗ V_{m}, where each U_{i} and V_{j} is either bit or qbit, if F : [[A]] → [[B]] is any superoperator, then there exists a valid typing judgement x : A ▷ M : B of denotation F.

Corollary 4.5 For every type A = U_{1}⊗⋯⊗U_{n}, where each U_{i} is either bit or qbit, and for every hermitian positive element v ∈ V_{[[A]]} of trace at most 1, v = [[M : A]](1) for some closed valid term M.

5 Equivalence classes of terms

Being able to build terms, we need some tools to compare them. One can compare them through syntactic manipulations, or one can have a finer approach using the two semantics we have built: in the case of the operational semantics, the behavior of the terms is what defines the equivalence, and in the case of the denotational semantics, the equivalence is expressed by the denotation of the terms.

(β) Γ ▷ (λx.M)N  ≈_{ax} M[N/x] : A
(η) Γ ▷ λx.Mx  ≈_{ax} M : A ⊸ B
(β_{⊗}) Γ ▷ let ⟨x, y⟩ = ⟨N, P ⟩ in M  ≈_{ax} M[N/x, P/y] : A
(η_{⊗}) Γ ▷ let ⟨x, y⟩ = M in ⟨x, y⟩  ≈_{ax} M : A ⊗ B
(β_{if}^{1}) Γ ▷ if 1 then M else N  ≈_{ax} M : A
(β_{if}^{0}) Γ ▷ if 0 then M else N  ≈_{ax} N : A
(Ω) Γ ▷ M[Ω/x]  ≈_{ax} Ω : A
(η_{if}) Γ ▷ if B then M[1/x] else M[0/x] ≈_{ax} M[B/x] : A
(id) Γ ▷ meas(new M)  ≈_{ax} M : qbit

Table 4 Axiomatic equivalence

5.1 Axiomatic equivalence

A first notion of equality of terms can be defined by a set of syntactic rules. This is known as the axiomatic equivalence.

Definition 5.1 We define an equivalence relation ≈_{ax} on typing judgement. We write the relation as Γ ▷ M ≈_{ax} N : A, and we define it to be the smallest relation satisfying the rules in Table 4, the alpha-equivalence and one congruence rule (ξ) per term constructor. This means for example:

Γ ▷ M ≈_{ax} M′ : A ⊸ B Δ ▷ N ≈_{ax} N′ : A

Γ, Δ ▷ MN ≈_{ax} M′N′ : B (ξ_{app})

{Γ, x : A ▷ M ≈_{ax} M′ : B \atop Γ ▷ λx.M ≈_{ax} λx.M′ : A ⊸ B} (ξ_{λ})

We call it the axiomatic equivalence relation.

Lemma 5.2 The order of the arguments in an application does not matter. Similarly, one can apply the arguments as a pairing or sequentially. More precisely:

[Q, L, ((λxy.M)N)P] ≈_{ax} [Q, L, ((λyx.M)P)N]
[Q, L, let ⟨x, y⟩ = ⟨N, P ⟩ in M] ≈_{ax} [Q, L, ((λxy.M)N)P]

5.2 Operational context

To say that two arbitrary terms have the same behavior, we need a way to observe them. The only observable types at our disposal are the types bit and ⊤. So the fact that two terms M and M′ have the same behavior can be understood as the fact that in whichever context C[−] we “use” them, if C[−] : bit, then C[M] reduces to 0, respectively, 1, with the same probability as C[M′]. Such a term C[−] is called an operational context.

Definition 5.3 We define a formal operational context to be a formula defined by the following BNF:

C[−] ::= [−] | (C[−]M) | (MC[−]) | λx.C[−] | ⟨C[−], M⟩ | ⟨M, C[−]⟩
| let ⟨x, y⟩ = C[−] in M | let ⟨x, y⟩ = M in C[−]
| if C[−] then M else N | if M then C[−] else C′[−].

We call [−] the hole of the context.

The notions of well-typed contexts and free variables in contexts are defined the same ways as for terms. Note that there exists a new notion: the notion of captured variables, which are the variables whose scope includes the hole. We can make this more precise by speaking of typed contexts:

Definition 5.4 A typed operational context is a typing tree with root Γ′ ▷ C[−] : B, considering the additional axiom Γ ▷ [−] : A, i.e., a typing tree of the form

Γ ▷ [−] : A ; ⋮ ; Γ′ ▷ C[−] : B.

We say that this context is of type B, with free variables Γ′, a hole of type A, and captured variables Γ. We also use the notation Γ′ ▷ C[Γ ▷ − : A] : B for a typed operational context.

Lemma 5.5 If

Γ ▷ [−] : A ; ⋮ ; Γ′ ▷ C[−] : B.

is a valid typing derivation, then so is

Δ, Γ ▷ [−] : A ; ⋮ ; Δ, Γ′ ▷ C[−] : B,

provided the variables that occur in Δ are fresh.

5.3 Operational equivalence

We define a notion of operational equivalence, based on the reduction rules and observations of type bit, as in [2]. (Equivalently, it would suffice to consider observations of type ⊤).

Definition 5.6 Let ▷ C[Γ ▷ − : A] : bit be a closed typed operational context of type bit, and let P = [Q, L, M] be a well-typed computation with typing judgement Γ ⊨ [Q, L, M] : A. In this case we define the substitution C[P] by [Q, L, C[M]], where M is syntactically replacing [−] in C[−]. We linearly extend this definition to probabilistic distributions of programs of the form Γ ⊨ ∑_{i} ρ_{i}P_{i} : A by setting C[∑_{i} ρ_{i}P_{i}] = ∑_{i} ρ_{i}C[P_{i}].

Lemma 5.7 In Definition 5.6, the substitution is well typed and a valid typing judgement for it is ⊨ [Q, L, C[M]] : bit.

Proof. A direct consequence of Lemma 5.5. ⊓ ⊔

Definition 5.8 Given two well-typed computations Γ ▷ P, P′ : A, we say that P is operationally equivalent to P′ with respect to Γ if for all closed typed operational contexts ▷ C[Γ ▷ − : A] : bit, C[P] ⇓ 0 = C[P′] ⇓ 0 and C[P] ⇓ 1 = C[P′] ⇓ 1. In this case, we write Γ ▷ P ≈_{op} P′ : A. If M, M′ are terms, we say that Γ ▷ M ≈_{op} M′ : A if Γ ⊨ [|⟩, |⟩, M] ≈_{op} [|⟩, |⟩, M′] : A.

5.4 Denotational equivalence

The last equivalence we can define is the denotational equivalence. This equivalence relation is simply stated:

Definition 5.9 We say that two typing judgments Γ ▷ M, M′ : A are denotationally equivalent if [[Γ ▷ M : A]] and [[Γ ▷ M′ : A]] are the same map in CPM. In that case we write Γ ▷ M ≈_{den} M′ : A.

We extend this definition to computations: Γ ⊨ P ≈_{den} P′ : A is true if [[Γ ⊨ P : A]] = [[Γ ⊨ P′ : A]].

6 Soundness of the axiomatic equivalence and full abstraction of the denotational semantics

The three defined equivalence relations we have built have the expected behavior: The axiomatic equivalence is sound with respect to the operational equivalence and the denotational semantic is fully abstract with respect to the operational semantics:

Theorem 6.1 (Soundness) If Γ ⊨ M ≈_{ax} M′ : A then Γ ⊨ M ≈_{op} M′ : A.

An immediate corollary is that the quantum context is not a side-effect, i.e., the order of evaluation does not affect the outcome.

Corollary 6.2 Γ ▷ ((λxy.P)M)N ≈_{op} ((λyx.P)N)M.

Proof. Using Lemma 5.2 and the soundness theorem. ⊓ ⊔

Theorem 6.3 (Full abstraction) The denotational semantics is fully abstract with respect to the operational equivalence of typing judgments, i.e.

[[Γ ▷ M : A]] = [[Γ ▷ M′ : A]] if and only if Γ ▷ M ≈_{op} M′ : A.

Remark 6.4 The presence of the non-terminating term Ω is necessary for full abstraction to hold. Without it, every program terminates with probability 1, and there is only one definable map bit → ⊤. Thus, although λf.(f0) and λf.(f1) of type (bit ⊸ ⊤) ⊸ ⊤ have different denotations, no context will distinguish them.

6.1 Proof of the soundness theorem

Assume Theorem 6.3. It suffices to show that if Γ ▷ M ≈_{ax} M′ : A then Γ ▷ M ≈_{den} M′ : A. We show this by structural induction on the proof of Γ ▷ M ≈_{ax} M′ : A.

We detail the cases (β_{if}^{1}) and (η).

For the (β_{if}^{1}) case, let [[Γ ▷ M, N : A]] = f, g : [[Δ]] → [[A]] and [[▷ 1 : bit]] = (p, q) : 1 → 1, 1. Then [[Γ ▷ if 1 then M else N : A]] : 1 ⊗ y ↦ (p1)(fy) + (q1)(gy) which is y ↦ fy, namely [[Γ ▷ M : A]].

The case (η) is done as follows. Consider the proof tree

\begin{matrix}Γ ▷ M : A ⊸ B & x : A ▷ x : A \\ Γ, x : A ▷ Mx : B \end{matrix} ; Γ ▷ λx.(Mx) : A ⊸ B

and set

[[x : A ▷ x : A]] = Id_{A} : [[a]] → [[A]]
[[Γ ▷ M : A ⊸ B]] = Φ(g) : [[Δ]] → [[A]] ⊗ [[B]]. Then
[[Γ, x : A ▷ Mx : B]] = f : [[Γ]] ⊗ [[A]] → [[B]]

with f(x ⊗ y) = g(x ⊗ Id_{A}(y)) = g(x ⊗ y), and we are done.

Note that cases (β) and (let) are done using Lemma 4.2. ⊓ ⊔

6.2 Full abstraction: preliminary lemmas

Lemma 6.5 For any two valid closed computations P, P′ of type bit, they have the same denotation if and only if for all b ∈ {0, 1}, P ⇓ b = P′ ⇓ b.

Proof. Consider two valid computations P, P′ : bit. Suppose they have the same denotation f. Then from Lemma 4.3, f is also the denotation of prob′_{U}P and of prob′_{U}P′. But by definition, [[prob′_{U}P]] = (p, q), where p = (prob′_{U}P) ⇓ 0 = P ⇓ 0 and q = (prob′_{U}P) ⇓ 1 = P ⇓ 1, and similarly for P′. Thus P ⇓ b = P′ ⇓ b. The argument being reversible, we get the other implication. ⊓ ⊔

Lemma 6.6 If [[Γ ▷ M:A]] = [[Γ ▷ M′:A]] and C[Γ ▷ − : A] : bit is a valid context, then [[C[M] : bit]] = [[C[M′] : bit]].

Proof. The proof uses Lemma 4.2. ⊓ ⊔

Definition 6.7 Given a type A, we define the canonical first-order representation \overline{A} of A by the following: \overline{bit} = bit, \overline{qbit} = qbit, \overline{⊤} = ⊤, \overline{A ⊗ B} = \overline{A} ⊗ \overline{B}, \overline{A ⊸ B} = \overline{A} ⊗ \overline{B}.

Lemma 6.8 For all types A, [[A]] = [[\overline{A}]].

Lemma 6.9 For all types A, there exist two terms x : A ▷ Υ_{A} : \overline{A} and x : \overline{A} ▷ \overline{Υ}_{A} : A and constants λ, λ′ > 0, such that [[Υ_{A}]] = λid_{[[A]]} and [[\overline{Υ}_{A}]] = λ′id_{[[A′]]}.

Proof. The terms Υ_{A} and \overline{Υ}_{A} are simultaneously constructed by structural induction on A. ⊓ ⊔

Lemma 6.10 For all types A, let σ = [[A]] and let m, m′ be hermitian positive elements in V_{σ}, m ≠ m′. Then there exists a well-typed term x : A ▷ M : bit such that [[M]](m) ≠ [[M]](m′).

Proof. By Lemma 6.9, it suffices, without loss of generality, to consider the case where A = bit ⊗ … ⊗ bit ⊗ qbit ⊗ … ⊗ qbit. However, in this case, the claim follows easily from Proposition 4.4 on the fullness of the semantics in first order. ⊓ ⊔ Lemma 6.11 Given any type A and any hermitian positive v ∈ V_{[[A]]}, there exists a closed term M : A and λ > 0 such that [[M]](1) = λv.

Proof. By Corollary 4.5 and Lemma 6.9. ⊓ ⊔

6.3 Proof of the full abstraction theorem

If [[Γ ▷ M : A]] = [[Γ ▷ M′ : A]], take any valid context C[Γ ▷ − : A] : bit for those two terms. Then from Lemma 6.6, [[▷ C[M] : bit]] = [[▷ C[M′] : bit]]. From Lemma 6.5, C[M] ⇓ b = C[M′] ⇓ b, for b ∈ {0, 1}. Since this holds for arbitrary contexts, M and M′ are operationally equivalent.

The opposite implication follows from Lemma 6.10 and Lemma 6.11. Consider two typing judgments Γ ▷ M, M′:A with denotations F =[[Γ ▷ M : A]] and G = [[Γ ▷ M′ : A]], such that F ≠ G.. Since the vector space V_{[[Γ]]} is spanned by hermitian positive elements, there exists a hermitian positive v ∈ V_{[[Γ]]} such that F (v) ≠ G(v).

If Γ = x_{1}:A_{1}, …, x_{n}:A_{n}, let B = A_{1} ⊗ … ⊗ A_{n}. By Lemma 6.11, there exists a closed term R : B such that [[R : B]](1) = λv, for some λ > 0. By Lemma 6.10, there exists a term x : A ▷ S : bit such that [[x : A ▷ S : bit]](F v) ≠ [[x : A ▷ S : bit]](Gv). Now consider C[Γ ▷ − : A] : bit defined by

let ⟨x_{1}, … x_{n}⟩ = R in let x = [−] in S.

Then [[C[M]]](1) ≠ [[C[M′]]](1), hence by Lemma 6.5, C[M]⇓b ≠ C[M′]⇓b, for some b ∈ {0, 1}. It follows that M ≉_{op}M′, which completes the proof of full abstraction.

⊓ ⊔

7 Conclusion

In this paper we have restricted our study to the linear fragment of the programming language of [4]. We gave a syntactic notion of equivalence of terms and an operational one, together with a fully abstract model for the latter.

Several questions remain open. First, the exact image of the denotational semantics is still to be characterized as a subset of the completely positive maps. Then it would be interesting to explore the categorical semantics of the linear language. Finally, we may want to add weakening and duplication and find a denotational semantics for the full quantum lambda calculus.

References

[1] Barendregt, H. P., “The Lambda-Calculus, its Syntax and Semantics,” Studies in Logic and the Foundation of Mathematics 103, North Holland, 1984, second edition.

[2] Danos, V. and R. S. Harmer, Probabilistic game semantics, ACM Transactional on Computational Logic 3 (2002), pp. 359–382.

[3] Selinger, P., Towards a quantum programming language, Mathematical Structures in Computer Science 14 (2004), pp. 527–586.

[4] Selinger, P. and B. Valiron, A lambda calculus for quantum computation with classical control, in: P. Urzyczyn, editor, Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), Lecture Notes in Computer Science 3461 (2005), pp. 354–368.