A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract)

Peter Selinger^{1} and Benoît Valiron^{2}

              1 Dalhousie University, selinger@mathstat.dal.ca

2 University of Ottawa, bvali087@uottawa.ca

Abstract. We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is its linear type system, which includes a duplicability operator “!” as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements. The “!” operator gives rise to a comonad, as in the linear logic models of Seely, Bierman, and Benton. The side-effects give rise to a monad, as in Moggi’s computational lambda calculus. It is this combination of a monad and a comonad that makes the present paper interesting. We show that our categorical semantics is sound and complete.

1 Introduction

In the last few years, there has been some interest in the semantics of quantum programming languages. [18] gave a denotational semantics for a flow-chart language, but this language did not include higher-order types. Several authors defined quantum lambda calculi [21, 19] as well as quantum process algebras [11, 12], which had higher-order features and a well-defined operational semantics, but lacked denotational semantics. [20] gave a categorical model for a higherorder quantum lambda calculus, but omitted all the non-linear features (i.e., classical data). Meanwhile, Abramsky and Coecke [2, 9] developed categorical axiomatics for Hilbert spaces, but there is no particular language associated with these models.

In this paper, we give the first categorical semantics of an unabridged quantum lambda calculus, which is a version of the language studied in [19].

For the purposes of the present paper, an understanding of the precise mechanics of quantum computation is not required. We will focus primarily on the type system and language, and not on the structure of the actual “builtin” quantum operations (such as unitary operators and measurements). In this sense, this paper is about the semantics of a generic call-by-value linear lambda calculus, which is parametric on some primitive operations that are not further explained. It should be understood, however, that the need to support primitive quantum operations motivates particular features of the type system, which we briefly explain now.

The first important language feature is linearity. This arises from the wellknown no-cloning property of quantum computation, which asserts that quantum data cannot be duplicated [23]. So if x : qbit is a variable representing a quantum bit, and y : bit is a variable representing a classical bit, then it is legal to write f(y, y), but not g(x, x). In order to keep track of duplicability at higherorder types we use a type system based on linear logic. We use the duplicability operator “!” to mark classical types. In the categorical semantics, this operator gives rise to a comonad as in the work of [16] and [6]. Another account of mixing copyable and non-copyable data is [10], where the copyability is internal to objects.

A second feature of quantum computation is its probabilistic nature. Quantum physics has an operation called measurement, which converts quantum data to classical data, and whose outcome is inherently probabilistic. Given a quantum state α|0⟩ + β|1⟩, a measurement will yield output 0 with probability |α|^{2} and 1 with probability |β|^{2}. To model this probabilistic effect in our call-by-value setting, our semantics requires a computational monad in the sense of [14]. The coexistence of the computational monad T and the duplicability comonad ! in the same category is what makes our semantics interesting and novel. It differs from the work of [7], who considered a monad and a comonad one two different categories, arising from a single adjunction.

The computational aspects of linear logic have been extensively explored by many authors, including [8, 6, 5, 1, 22]. However, these works contain explicit lambda terms to witness the structural rules of linear logic, for example, x : !A ▷ derelict(x) : A. By contrast, in our language, structural rules are implicit at the term level, so that !A is regarded as a subtype of A and one writes x : !A ▷ x : A. As we have shown in [19], linearity information can automatically be inferred by the type checker. This allows the programmer to program as in a non-linear language.

This use of subtyping is the main technical complication in our proof of welldefinedness of the semantics. This is because one has to show that the denotation is independent of the choice of a potentially large number of possible derivations of a given typing judgment. We are forced to introduce a Church-style typing system, and to prove that the semantics finally does not depend on the additional type annotations.

Another technical choice we made in our language concerns the relation between the exponential ! and the pairing operation. Linear logic only requires !A ⊗ !B ▷ !(A ⊗ B) and not the opposite implication. However, in our programming language setting, we find it natural to identify a classical pair of values with a pair of classical values, and therefore we will have an isomorphism !A ⊗!B ≅ !(A ⊗ B).

The plan of the paper is the following. First, we describe the lambda calculus and equational axioms we wish to consider. Then, we develop a categorical model, called linear category for duplication, which is inspired by [8] and [14].

We then show that the language is an internal language for the category, thus obtaining soundness and completeness.

2 The language

We will describe a linear typed lambda calculus with higher-order functions and pairs. The language is designed to manipulate both classical data, which is duplicable, and quantum data, which is non-duplicable. For simplicity, we assume the language is strictly linear, and not affine linear as in [19]. This means duplicable values are both copyable and discardable, whereas non-duplicable values must be used once, and only once.

2.1 The type system

The set of types is given as follows: Type A, B ::= α | (A⊸B) | (A⊗B) | ⊤ | !A.

Here α ranges over type constants. While the remainder of this paper does not depend on the choice of type constants, in our main application [19] this is intended to include a type qbit of quantum bits, and a type bit of classical bits. A ⊸ B stands for functions from A to B, A ⊗ B for pairs, ⊤ for the unit type, and !A for duplicable objects of types A. We denote !!⋯!A with n !’s by !^{n}A.

The intuitive definition of !A is the key to the spirit in which we want the language to be understood: The ! on !A is understood as specifying a property, rather than additional structure, on the elements of A. Therefore, we will have !A ≅ !!A. Whether or not a given value of type A is also of type !A should be something that is inferred, rather than specified in the code.

Since a term of type !A can always be seen as a term of type A, we equip the type system with a subtyping relation as follows: Provided that (m = 0)∨(n ⩾ 1),

\begin{matrix}!^{n}α <: !^{m}α (ax), & !^{n}⊤ <: !^{m}⊤ (⊤), \\ \begin{matrix}A <: A′ & & B <: B′ \\ !^{n}(A′ ⊸ B) & <: & !^{m}(A ⊸ B′) \end{matrix} (⊸), & \begin{matrix}A <: A′ & B <: B′ \\ !^{n}(A ⊗ B) <: !^{m}(A′ ⊗ B′). \end{matrix} (⊗). \end{matrix}

This relation encapsulates the main properties terms should satisfy with respect to duplicability.

2.2 Terms

The language consists of the following typed terms, divided into values on the one hand, and general terms, or computations, on the other. Both share a subset of the values, the core values.

CoreValue U ::= x^{A} | c^{A} | ∗^{n} | λ^{n}x^{A}.M,
Value V, W ::= U | ⟨V, W ⟩ | let x^{A} = V in W | let ⟨x^{A}, y^{B}⟩^{n} = V in W |
let ∗ = V in W ,
Term M, N ::= U | ⟨M, N⟩ | (MN) | let ⟨x^{A}, y^{B}⟩^{n} = M in N | let ∗ = M in N,

where n is an integer, c ranges over a set of constant terms, x over a set of term variables and α over a set of constant types. We abbreviate (λ^{0}x^{A}.M)N by let x^{A} = N in M, λ^{n}x^{!^{m}⊤}. let ∗ = x^{⊤} in M by λ^{n}∗^{m}.M and we omit numerical indexes when they are null.

Note that the above terms carry Church-style type annotations, as well as integer superscripts; we call these terms indexed terms. We also define a notion of untyped terms as terms with no index:

PureTerm M, N ::= x | c | ∗ | λx.M | (MN) | ⟨M, N⟩ |
let⟨x, y⟩ = M in N | let ∗ = M in N .

The erasure operation Erase : Term → PureTerm is defined as the operation of removing the types and integers attached to a given indexed term. If M = Erase(M̄), we say that M̄ is an indexation of M

Finally, we define an α-equivalence on terms, denoted by =_{α}, in the usual way (see for example [3]).

2.3 Duplicable pairs and pairs of duplicable elements

Before we formally present the type system, let us informally motivate our choice of typing rules. One non-obvious choice we had to make is for the interaction of pairs and duplicability. Unlike previous works with comonads [8, 5], we want to think of the type !(A ⊗ B) as a type of pairs of elements of type A and B: we want to use the same operation to access the components as one would use for a pair of type A ⊗ B, without having to use a dereliction operation.

This immediately raises a concern: consider a pair of elements ⟨x, y⟩ of type !(A ⊗ B). Are x and y duplicable? In the usual linear logic interpretation, they are not. Having a infinite supply of pair of shoes does not mean one has an infinite supply of right shoes: we cannot discard the left shoes. On the other hand, in our interpretation of “classical” data as residing in “classical” memory and therefore being duplicable, if the string ⟨x, y⟩ is duplicable, then so should be the elements x and y. In other words, we want the duplication to “permeate” the pairing.

The choice of such a “permeable” pairing is more or less forced on us by our desire to have no explicit term syntax for structural rules. Consider the following untyped terms, which can be typed if t is of type !(A ⊗!(B ⊗ C)):

let⟨x, u⟩ = t in let⟨y, z⟩ = u in ⟨⟨z, y⟩, x⟩,  (1)
let⟨x, u⟩ = t in ⟨let⟨y, z⟩ = u in ⟨z, y⟩, x⟩.  (2)

First, we expect these two terms to be axiomatically equal. Term (2) should be of type !(!(C ⊗ B) ⊗ A), regardless of the permeability of the pairing: if ⟨y, z⟩ is duplicable, so should be ⟨z, y⟩. Now, consider the term (1) with a non-permeable pairing. In the naive type system, u ends up being of type B⊗C, and the variables y and z in the final recombination end up being respectively of type B and C. It is not possible to make ⟨z, y⟩ of the duplicable type !(C ⊗ B).

We therefore choose a permeable pairing, which will be reflected, albeit subtly, in the typing rule (⊗.I) and (⊗.E) in the following section.

{A <: B \atop !Δ, x : A ▷ x^{B} : B} (ax_{1}) {!A_{c} <: B \atop !Δ ▷ c^{B} : B} (ax_{2}) \begin{matrix}Γ_{1},!Δ ▷ M : A ⊸ B & Γ_{2},!Δ ▷ N : A \\ Γ_{1}, Γ_{2},!Δ ▷ MN : B \end{matrix} (app)

{Δ, x : A ▷ M : B \atop Δ ▷ λ^{0}x^{A}.M : A ⊸ B} (λ_{1}) {!Δ, x : A ▷ M : B \atop !Δ ▷ λ^{n+1}x^{A}.M : !^{n+1}(A ⊸ B)} (λ_{2}) !Δ ▷ ∗^{n} : !^{n}⊤ (⊤.I)
\begin{matrix}!Δ, Γ_{1} ▷ M_{1} : !^{n}A_{1} & !Δ, Γ_{2} ▷ M_{2} : !^{n}A_{2} \\ !Δ, Γ_{1}, Γ_{2} ▷ ⟨M_{1}, M_{2}⟩^{n} : !^{n}(A_{1} ⊗ A_{2}) \end{matrix} (⊗.I) \begin{matrix}!Δ, Γ_{1} ▷ M : ⊤ & !Δ, Γ_{2} ▷ N : A \\ !Δ, Γ_{1}, Γ_{2} ▷ let ∗ = M in N : A \end{matrix} (⊤.E)

\begin{matrix}!Δ, Γ_{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}^{A_{1}}, x_{2}^{A_{2}}⟩^{n} = M in N : A \end{matrix} (⊗.E)

Table 1. Typing rules

2.4 Typing judgments

A typing judgment is a tuple Δ ▷ M : A, where M is an indexed term, A is a type, and Δ is a typing context. To each constant term c we assign a type !A_{c}. A valid typing judgment is a typing judgment that can be derived from the typing rules in Table 1. We use the notation !Δ for a context where all variables have a type of the form !A. Finally, when we write a context Γ, Δ, we assume the contexts Γ and Δ to be disjoint.

The following lemmas are proved by structural induction on terms or type derivations as appropriate.

Lemma 1. If V is a value such that Δ ▷ V : !A is a valid typing judgment, then Δ = !Δ′ for some context Δ′. ⊓ ⊔

Lemma 2. Consider the following valid typing judgment: Δ, x : A ▷ M : B. Then for every free instance x^{A′} in M, A <: A′. ⊓ ⊔

Definition 1. In a typing judgment Δ ▷ M : A, a term variable x ∈ |Δ| is called dummy if x ∉ FV (M).

Lemma 3. Any dummy variable x in Δ ▷ M : B satisfies Δ(x) = !A, for some A. Conversely, if Δ ▷ M : B is valid and if x ∉ FV (M), then for all types A the typing judgment Δ, x : !A ▷ M : B is valid. ⊓ ⊔

Typing derivations are not unique per se. However for a given valid typing judgement Δ ▷ M : A two typing derivations will only differ with respect to the placement of dummy variables, namely the unused variables in context.

2.5 Type casting and substitution Lemma

Lemma 4. Suppose Δ ▷ M : A is a valid typing judgment, and suppose Δ′ <:Δ and A <: A′. Then there exists a canonical valid typing judgment Δ′ ▷ M′ : A′ such that Erase(M) = Erase(M′). Moreover, if M is a value, so is M′.

Proof. By induction on M. ⊓ ⊔

We will denote this M′ with {Δ′ <: Δ ▷ M : A <: A′}. If Δ′ = Δ or A′ = A, we omit them for clarity.

(β_{λ}) Δ ▷ let x = V in M  ≈_{ax}M[V/x]  : A
(β_{⊗}) Δ ▷ let⟨x, y⟩^{n} = ⟨V, W ⟩^{n} in M  ≈_{ax}M[V/x, W/y] : A
(β_{∗}) Δ ▷ let ∗ = ∗ in M ≈_{ax}M : A
(η_{λ}) Δ ▷ λ^{n}x^{A}.{V : !^{n}(A ⊸ B) <: A ⊸ B}x^{A} ≈_{ax}V  : !^{n}(A ⊸ B).
(β_{λ}^{2}) Δ ▷ let x^{A} = N in x^{A} ≈_{ax}N : A.
(η_{⊗}) Δ ▷ let⟨x^{A}, y^{B}⟩^{n} = N in ⟨x^{!^{n}A}, y^{!^{n}B}⟩^{n} ≈_{ax}N  : !^{n}(A ⊗ B).
(η_{∗}) Δ ▷ let ∗ = N in ∗^{n}  ≈_{ax}N  : !^{n}⊤.
(let_{1}) Δ ▷ let −_{1} = (let −_{2} = M in N) in P  ≈_{ax} let −_{2} = M in let −_{1} = N in P : A
(let_{2}) Δ ▷ let −_{1} = V in let −_{2} = W in M  ≈_{ax} let −_{2} = W in let −_{1} = V in M : A
(let^{app}) Δ ▷ let x^{A⊸B} = M in let y^{A} = N in xy  ≈_{ax}MN  : B
(let^{λ}) Δ ▷ let x^{D} = V in λ^{n}y^{A}.M  ≈_{ax}λ^{n}y^{A}. let x^{D} = V in M  : !^{n}(A ⊸ B)
(let^{⊗}) Δ ▷ let x^{A} = M in let y^{B} = N in ⟨x^{A}, y^{B}⟩^{n} ≈_{ax}⟨M, N⟩^{n}  : !^{n}(A ⊗ B)
(app_{<:}) {M : !^{n}(A ⊸ D) <: B ⊸ D′}{N : C <: B}

≈_{ax}{{M : !^{n}(A ⊸ D) <: A ⊸ D}{N : C <: A} : D <: D′}

(let_{<:}^{⊗}) let⟨x^{A′}, y^{B′}⟩^{n′} = {M : !^{n}(A ⊗ B) <: !^{n′}(A′ ⊗ B′)} in N

≈_{ax} let ⟨x^{A}, y^{B}⟩^{n} = M in {Δ, x : !^{n}A, y : !^{n}B <: Δ, x : !^{n′}A′, y : !^{n′}B′ ▷ N}

(let_{<:}^{x}) let x^{A′} = {M : A <: A′} in N ≈_{ax} let x^{A} = M in {Δ, x : A <: Δ, x : A′ ▷ N}
(let_{<:}^{∗}) let ∗ = {M : !^{m}⊤ <: !^{n}⊤} in N ≈_{ax} let ∗ = M in N

Table 2. Axiomatic equivalence axioms

(α_{let}) Δ, x : A ▷ let y^{A} = x^{A} in M : B ≈_{ax} Δ, y : A ▷ M  : B
(let^{!λ}) !Δ ▷ let x^{!C} = V in λy.M  ≈_{ax} λ^{n+1}y. let x^{!C} = V in M : !^{n+1}(A ⊸ B)
(let_{1}^{⊗}) Δ ▷ ⟨V, let − = M in N⟩  ≈_{ax} let − = M in ⟨V, N⟩  : !^{n}(A ⊗ B)
(let_{2}^{⊗}) Δ ▷ ⟨let − = M in N, V ⟩  ≈_{ax} let − = M in ⟨N, V ⟩  : !^{n}(A ⊗ B)
(let_{1}^{app}) Δ ▷ V (let − = M in N)  ≈_{ax} let − = M in V N  : B
(let_{2}^{app}) Δ ▷ (let − = M in N)V  ≈_{ax} let − = M in NV  : B

Table 3. Axiomatic equivalence: derived rules

Definition 2. Given two valid typing judgments !Δ, Γ_{1} ▷ V : A and !Δ, Γ_{2}, x : A ▷ M : B where V is a value, we define the substitution (with capture avoiding) !Δ, Γ_{1}, Γ_{2} ▷ M[V/x] : B as follows: we replace each free instance x^{A′} (where A <: A′ from Lemma 2) in M by {Δ ▷ V : A <: A′}.

Lemma 5 (Substitution Lemma). In Definition 2, !Δ, Γ_{1}, Γ_{2} ▷ M[V/x] : B is well-typed. Also, if M is a value, so is M[V/x].

Proof. Proof by structural induction on M, using Lemmas 2 and 4. ⊓ ⊔

2.6 Axiomatic equivalence

We define an equivalence relation on (indexed) typing judgments. We write Δ ▷ M ≈_{ax} M′ : A, or simply M ≈_{ax} M′, to indicate that Δ ▷ M : A and Δ ▷ M′ : A are equivalent. Axiomatic equivalent is defined as the reflexive, symmetric, transitive, and congruence closure of the rules from Tables 2, so long as both sides of the equivalences are well-typed. The symbol “−” is a place holder for x, ∗, or ⟨x, y⟩.

Lemma 6. The equivalences of Table 3 are derivable. ⊓ ⊔

The following result stipulates that all the indexations of a given erasure live in the same axiomatic class. In other words, the axiomatic equivalence class of a term is independent of its indexation.

Theorem 1. If Erase(M) = Erase(M′) and if Δ ▷ M, M′ : A are valid typing judgments, then M ≈_{ax} M′.

Proof (Sketch). The actual proof is long and technical, and is omitted here for space reasons. We proceed by first defining a special subset of terms, called neutral terms, for which the Theorem is obvious. We then prove that every term is axiomatically equivalent to a neutral term via a series of rewrite systems. ⊓ ⊔

3 Linear category for duplication

As it was advertised, the structure of the categorical semantics will closely follow the one proposed by Bierman [8], but with the added twist of a computational monad à la Moggi [14]. Indeed, since one has tensor products and a tensor unit, one can expect the categorical model to be symmetric monoidal. Since one can construct candidate maps for building a comonad, a comonoid structure for each !A and coherence maps for the comonad, we have a linear category. Finally, the computational aspect will be taken care by Moggi’s computational monad.

3.1 Linear exponential comonads

In his Ph.D. thesis, Bierman [8] gives the definition of a linear category. We prefer here the terminology given in [15], and use the concept of linear exponential comonad.

Definition 3. Let (𝒞, ⊗, ⊤) be a symmetric monoidal category [13], where α_{A,B,C} : A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C, λ_{A} : ⊤ ⊗ A → A, ρ_{A} : A ⊗ ⊤ → A and σ_{A,B} : A ⊗ B → B ⊗ A are the usual associativity, left unit, right unit and symmetry morphisms. Let (L, δ, ϵ, d^{L}, d^{L}) be a monoidal comonad [8], where ϵ_{A} : LA → A, δ_{A} : LA → LLA, d_{A,B}^{L} : LA ⊗ LB → L(A ⊗ B) and d_{⊤}^{L} : ⊤ → L⊤. We say that L is a linear exponential comonad [15] provided that

1. each object in 𝒞 of the form LA is equipped with a commutative comonoid (LA, △_{A}, ♢_{A}), where △_{A} : LA → LA ⊗ LA and ♢_{A} : LA → ⊤;

2. △_{A} and ♢_{A} are monoidal natural transformations;

3. △_{A} : (LA, δ_{A}) → (LA ⊗ LA, (δ_{A} ⊗ δ_{A}); d_{A}) and ♢_{A} : (LA, δ_{A}) → (⊤, d_{⊤}^{L}) are L-coalgebra morphisms;

4. Every map δ_{A} is a comonoid morphism (LA, ♢_{A}, △_{A}) → (L^{2}A, ♢_{LA}, △_{LA}).

The equations for 2–4 are to be found in Table 4.

3.2 Strong monad and T -exponentials.

To capture the computational effect of the probabilistic measurement, we use the notion of strong monad, as in [14]. Recall that a monad over a category 𝒞 is a triple (T, η, μ) where T : 𝒞 → 𝒞 is a functor, η : id ˙→ T and μ : T^{2} ˙→ T are natural transformations and such that T μ_{A}; μ_{A} = μ_{T A}; μ_{A} and η_{T A}; μ_{A} = id_{T A} = T η_{A}; μ_{A}. Given a map f : A → T B, we define the map f^{∗} : T A → T B by T f; μ_{B}.

[figure: LA ⊗ LB; d_{A,B}^{L}; △_{A}⊗△_{B}; (LA ⊗ LA) ⊗ (LB ⊗ LB); sw; (LA ⊗ LB) ⊗ (LA ⊗ LB); d_{A,B}^{L}⊗d_{A,B}^{L}; L(A ⊗ B); △_{(A⊗B)}; L(A ⊗ B) ⊗ L(A ⊗ B); ⊤; λ_{⊤}^{−1}; d_{⊤}^{L}; ⊤ ⊗ ⊤; d_{⊤}^{L}⊗d_{⊤}^{L}; L⊤; △_{⊤}; L⊤ ⊗ L⊤; LA ⊗ LB; ♢_{A}⊗♢_{B}; d_{A,B}^{L}; ⊤ ⊗ ⊤; λ_{⊤}; L(A ⊗ B); ♢_{A⊗B}; ⊤; ⊤; id; d_{⊤}^{L}; ⊤;; L⊤; ♢_{⊤}]

△_{A} and ♢_{A} are monoidal natural transformations.

[figure: LA; △_{A}; δ_{A}; LA ⊗ LA; δ_{A}⊗δ_{A}; L^{2}A ⊗ L^{2}A; d_{LA,LA}^{L}; L^{2}A; L△_{A}; L(LA ⊗ LA),; LA; ♢_{A}; δ_{A}; ⊤; d_{⊤}^{L}; L^{2}A; L♢_{A}; L⊤;; LA; δ_{A}; △_{A}; L^{2}A,; △_{LA}; LA ⊗ LA; δ_{A}⊗δ_{A}; L^{2}A ⊗ L^{2}A; LA; δ_{A}; ♢_{A}; L^{2}A.; ♢_{LA}; ⊤]

△_{A} and ♢_{A} are L-coalgebra maps.  δ_{A} is a comonoid morphism.

Table 4. Equations for a linear exponential comonad

Definition 4. A strong monad over a monoidal category 𝒞 is a monad (T, η, μ) together with a natural transformation t_{A,B} : A ⊗ T B → T (A ⊗ B), called the tensorial strength, subject to a number of coherence conditions.

Remark 1. If the category 𝒞 is symmetric, the tensorial strength t induces two natural transformations T A ⊗ T B → T (A ⊗ B), namely

\begin{matrix}Ψ_{1} : T A ⊗ T B ⟶^{σ_{T A,T B}} T B ⊗ T A ⟶^{t_{T B,A}} T (T B ⊗ A) ⟶^{(σ_{T B,A};t_{A,B})^{∗}} T (A ⊗ B), \\ Ψ_{2} : T A ⊗ T B ⟶^{t_{T A,B}} T (T A ⊗ B) ⟶^{(σ_{T A,B};t_{B,A})^{∗}} T (B ⊗ A) ⟶^{T σ_{B,A}} T (A ⊗ B). \end{matrix}

Note that Ψ_{1} and Ψ_{2} might not be equal: the map Ψ_{1} “evaluates” the first variable and then the second one. The map Ψ_{2} does the opposite. The strength is called commutative if Ψ_{1} = Ψ_{2}.

Lemma 7. If (T, η, μ, t) is a commutative strong monad on a symmetric monoidal category 𝒞, then (T, η, μ, Ψ_{1}) and (T, η, μ, Ψ_{2}) are monoidal monads. ⊓ ⊔

Definition 5. A symmetric monoidal category (𝒞, ⊗, ⊤) together with a strong monad (T, η, μ) is said to have T -exponentials [14], or Kleisli exponentials, if it is equipped with a bifunctor ⊸ : 𝒞^{op} × 𝒞 → 𝒞, and a natural isomorphism

Φ : 𝒞(A, B ⊸ C) ⟶^{≅} 𝒞(A ⊗ B, T C).

Lemma 8. The map Φ induces a natural transformation ε_{A,B} : (A⊸B)⊗A → T B defined by Φ(id_{A⊸B}). ⊓ ⊔

3.3 Idempotent, strong monoidal comonad

A comonad (L, ϵ, δ) on some category is said to be idempotent if δ : L ˙→ LL is an isomorphism. A monoidal comonad (L, δ, ϵ, d^{L}, d^{L}) is strong monoidal if d_{⊤}^{L} and d_{A,B}^{L} are isomorphisms.

Definition 6. Given a monoidal category (𝒞, ⊗, ⊤) with an idempotent, strong monoidal comonad (L, ϵ, δ), a bifunctor ⊸ : 𝒞^{op} × 𝒞 → 𝒞, we define a canonical arrow for 𝒞 with respect to duplication by induction: For all objects A, the arrows id_{A}, ϵ_{A}, δ_{A}, d_{⊤}^{L} and d_{A,B}^{L} are canonical. All expansions of canonical arrows with respect to duplication are also canonical. An expansion of an arrow f : A → B is defined to be either f or any of Lg,X ⊗ g, g ⊗ X, X ⊸ g, g ⊸ X, where g is an expansion of f and X ranges over the objects of the category. Finally, compositions of canonical arrows are also canonical.

Theorem 2 (Coherence for idempotent comonads). Given a category 𝒞 with the structure in Definition 6, if f, g : A → B are two canonical arrows with respect to duplication, then they are equal. ⊓ ⊔

3.4 Linear category for duplication

We now have enough background to define a candidate for the categorical model of the language we describe in Section 2.

Definition 7. A linear category for duplication is a category 𝒞 with the following structure:

– a symmetric monoidal structure (⊗, ⊤, α, λ, ρ, σ);

– an idempotent, strongly monoidal, linear exponential comonad (L, δ, ϵ, d^{L}, d^{L}, ♢, △);

– a strong monad (T, μ, η, t);

– a Kleisli exponential ⊸.

The computational linear category is defined to be the Kleisli category 𝒞_{T}, as defined in [14].

Remark 2. A linear category for duplication gives rise to a double adjunction

\xymatrix{𝒞_{L} \ar[rr]^{U^{L}} & ⊥ & 𝒞 \ar[ll]^{F^{L}} \ar[rr]^{U^{T}} & ⊥ & 𝒞_{T} , . \ar[ll]^{F^{T}}} Here the left adjunction arises from the co-

Kleisli category 𝒞_{L} of the comonad L. It is as in the linear-non-linear models of [4], and 𝒞_{L} is a category of classical (non-quantum) values. The right adjunction arises from the Kleisli category 𝒞_{T} of the computational monad T, as in [14]. Here 𝒞_{T} is a category of (effectful) quantum computations.

3.5 The category 𝒞_{λ}

Definition 8. We can define a category 𝒞_{λ} as follows: Objects are types, and arrows A → B are axiomatic classes of valid typing judgments of the form x : A ▷ V : B, where V is a value. We define the composition of arrows x : A ▷ V : B and y : B ▷ W : C to be x : A ▷ let y = V in W : C. The identity on A is set to be the arrow x : A ▷ x : A.

Lemma 9. The category 𝒞_{λ} is well-defined.

α_{A,B,C} = x : A⊗(B⊗C) ▷ let⟨y, z⟩ = x in let⟨t, u⟩ = z in ⟨⟨y, t⟩, u⟩ : (A⊗B)⊗C
λ_{A}  =  x : ⊤ ⊗ A ▷ let⟨y, z⟩ = x in let ∗ = y in z  : A
ρ_{A}  =  x : A ⊗ ⊤ ▷ let⟨y, z⟩ = x in let ∗ = z in y  : A
σ_{A,B} =  x : A ⊗ B ▷ let⟨y, z⟩ = x in ⟨z, y⟩  : B ⊗ A
η_{A}  =  x : A ▷ λ∗.x  : ⊤⊸ A
μ_{A}  = x : ⊤⊸(⊤⊸ A) ▷ λ∗.(x∗)∗  : ⊤⊸ A
t_{A,B} = z : A ⊗ (⊤⊸ B) ▷ let⟨x, y⟩ = z in λ∗.⟨x, y∗⟩  : ⊤⊸(A ⊗ B)
ϵ_{A}  =  x : !A ▷ x^{A}  : A
δ_{A}  =  x : !A ▷ x^{!^{2}A}  : !^{2}A
d_{A,B}^{!} =  z : !A ⊗!B ▷ let⟨x, y⟩ = z in ⟨x, y⟩  : !(A ⊗ B)
d_{⊤}^{!}  =  z : ⊤ ▷ let ∗ = z in ∗  : !⊤
△_{A} =  x : !A ▷ ⟨x, x⟩  : !A ⊗!A
♢_{A}  =  x : !A ▷ ∗  : ⊤
(x : A ▷ V : B) ⊗ (y : C ▷ W : D) = z : A ⊗ B ▷ let⟨x, y⟩ = z in ⟨V, W ⟩ : C ⊗ D
(x : A ▷ V : B) ⊸ (y : C ▷ W : D) = z : B ⊸ C ▷ λx.(let y = zV in W) : A ⊸ D
(x : A ▷ V : ⊤⊸ B)^{∗}  = y : ⊤⊸ A ▷ λ∗. let x = (y∗) in (V ∗) : ⊤⊸ B
Φ_{A,B,C} (x : A ▷ V : B ⊸ C)  = t : A ⊗ B ▷ λ∗. let ⟨x, y⟩ = t in V y : ⊤ ⊸ C

Table 5. Definitions of maps and operations on maps in 𝒞_{λ}

Proof. The composition of two arrows yields an arrow axiomatically equivalent to a value due to Axiom (β_{λ}) and Lemma 5. Composition is associative due to Axiom (let_{1}). The arrow x : A ▷ x : A is indeed the identity on A due to axioms (α_{let}) and (β_{λ}^{2}). ⊓ ⊔

Lemma 10. Given a valid typing judgment Δ ▷ V : A where V is a value, there exists a canonical value V′ such that Erase(V′) = Erase(V) and such that !Δ ▷ V′ : !A. We denote this V′ by {!Δ <: Δ ▷ V : A:> A′}.

Proof. By induction on V. ⊓ ⊔

Lemma 11. If Δ ▷ V ≈_{ax} W : A, and if V′ = {!Δ <: Δ ▷ V : A :> A′} and W′ = {!Δ <: Δ ▷ W : A:> A′}, then V′ ≈_{ax} W′.

Proof. By induction on V ≈_{ax} W. ⊓ ⊔

Theorem 3. If we define T (A) := ⊤ ⊸ A and L(A) =!A, together with the maps and the operations on maps defined in Table 5, 𝒞_{λ} is a linear category for duplication.

Proof. The proof is mainly a long list of verifications. It uses Theorem 1, Lemmas 9, 10 and 11. ⊓ ⊔

4 Denotational semantics

4.1 Interpretation of the language

The lambda-calculus defined in Section 2 is thought as a computational lambdacalculus. Using Moggi’s technique, we split the interpretation of the language into the interpretation of the values in a linear category for duplication 𝒞 and the interpretation of the computations, i.e. general terms, in its Kleisli category 𝒞_{T}. Without loss of generality, for notation purposes, we assume the category to be strictly monoidal.

We define an interpretation of the type system to be a map Θ that assigns to each constant type α an object Θ(α). Each type A is interpreted as an object of 𝒞: [[α]]_{Θ} = Θ(α), [[⊤]]_{Θ} = ⊤, [[!A]]_{Θ} = L[[A]]_{Θ}, [[A ⊗ B]]_{Θ} = [[A]]_{Θ} ⊗ [[B]]_{Θ} and [[A ⊸ B]]_{Θ} = [[A]]_{Θ} ⊸ [[B]]_{Θ}.

Given a valid subtyping A <: B, there exists a canonical arrow [[A]]_{Θ} → [[B]]_{Θ} in 𝒞 with respect to duplication, as defined in Definition 6. Moreover, this arrow is unique by Theorem 2. We extend the map Θ to interpret A<:B as this unique arrow and we denote it by I_{A,B}.

We use the following straightforward shortcut definitions, where A, A′, B, B′ are types and Δ, Γ and Γ′ are typing contexts:

– Split_{!Δ,Γ,Γ′} : [[!Δ]] ⊗ [[Γ]] ⊗ [[Γ′]] → [[!Δ]] ⊗ [[Γ]] ⊗ [[!Δ]] ⊗ [[Γ′]].

– Given f : [[!Δ]] ⊗ [[Γ]] → [[A]] and g : [[!Δ]] ⊗ [[Γ′]] → [[B]], we define the map f ⊗_{!Δ} g : [[!Δ]] ⊗ [[Γ]] ⊗ [[Γ′]] → A ⊗ B.

– Given a natural transformation n_{A} : F A → GA, if Δ = {x_{1} : A_{1} … x_{n} : A_{n}} we define n_{Δ} = n_{[[A_{1}]]} ⊗ … ⊗ n_{[[A_{n}]]}.

Definition 9. The map Θ is said to be an interpretation of the language if moreover it assigns to each constant term c : A_{c} an arrow Θ(c) : ⊤ → [[A_{c}]] in 𝒞.

Given a linear category for duplication 𝒞, it is possible to interpret the typing derivation of a well-typed value as a map in 𝒞 and the typing derivation of a valid computation as a map in the Kleisli category 𝒞_{T}. We define them inductively.

– If x_{1} : A_{1}, … x_{n} : A_{n} ▷ V : B is a value with typing derivation π, its value interpretation [[π]]_{Θ}^{v} is an arrow [[A_{1}]] ⊗ … ⊗ [[A_{n}]] →_{𝒞} [[B]];

– if x_{1} : A_{1}, … x_{n} : A_{n} ▷ M : A is a term with typing derivation π, its computational interpretation [[π]]_{Θ}^{c} is an arrow [[A_{1}]] ⊗ … ⊗ [[A_{n}]] →_{𝒞} T ([[B]]).

Table 6 formulates the definition in the simple case where the contexts Δ, Γ_{1} and Γ_{2} contain only one variable. One can easily extend this to the general setting.

As we already noted in Section 2.4, a valid typing judgment does not have a unique typing tree per se. However the following result holds:

Theorem 4. Given a valid typing judgment with two typing derivations π and π′, for any interpretation Θ we have [[π]]_{Θ}^{c} = [[π′]]_{Θ}^{c} (and [[π]]_{Θ}^{v} = [[π′]]_{Θ}^{v} if the typing judgment is a value).

Proof. The proof is done by showing that given any typing judgment Δ ▷ M : A with denotation f one can factor f as ♢_{!Γ} ⊗ f̄, where f̄ is the denotation of Δ′ ▷ M : A, where Δ′,!Γ = Δ and |Γ | is the set of dummy variables. ⊓ ⊔

Definition 10. Given a interpretation Θ of the language in a category 𝒞, we define the denotation of a valid typing judgment Δ ▷ M : A with typing derivation π to be [[Δ ▷ M : A]]_{Θ}^{c} = [[π]]_{Θ}^{c} and [[Δ ▷ M : A]]_{Θ}^{v} = [[π]]_{Θ}^{v} if M is a value.

Interpretation of core values:

\begin{aligned}[[!Δ, x : A ▷ x : B]]_{Θ}^{v} & = [[!Δ]] ⊗ [[A]] ⟶^{♢_{Δ}⊗I_{A,B}} [[B]] \\ [[!Δ ▷ c : B]]_{Θ}^{v} & = [[!Δ]] ⟶^{♢_{Δ}} ⊤ ⟶^{Θ(c)} [[A_{c}]] ⟶^{I_{Ac,B}} [[B]] \\ [[!Δ ▷ ∗ : !^{n}⊤]]_{Θ}^{v} & = [[!Δ]] ⟶^{♢_{Δ}} ⊤ ⟶^{d_{⊤}^{L}} L⊤ ⟶^{I_{!⊤,!^{n}⊤}} L^{n}⊤ \end{aligned} \begin{aligned}[[Δ, x : A ▷ M : B]]_{Θ}^{c} & = [[Δ]] ⊗ [[A]] ⟶^{f} T ([[B]]) \\ [[Δ ▷ λx.M : A ⊸ B]]_{Θ}^{v} & = [[Δ]] ⟶^{Φ^{−1}(f)} [[A]] ⊸ [[B]] \end{aligned} ; \frac{[[!Δ, x : A ▷ M : B]]_{Θ}^{c} = [[!Δ]] ⊗ [[A]] ⟶^{f} T ([[B]])}{[[!Δ ▷ λx.M : !^{n+1}(A ⊸ B)]]_{Θ}^{v} = [[!Δ]] ⟶^{L(Φ^{−1}f);I_{!(A⊸B),!^{n+1}(A⊸B)}} L^{n+1}([[A]] ⊸ [[B]])}

Interpretation of extended values:

\frac{[[!Δ, Γ_{1} ▷ V : A]]_{Θ}^{v} = [[!Δ]]⊗[[Γ_{1}]] ⟶^{f} [[A]] [[!Δ, Γ_{2}, x : A ▷ W : B]]_{Θ}^{v} = [[!Δ]]⊗[[Γ_{2}]]⊗[[A]] ⟶^{g} [[B]]}{[[!Δ, Γ_{2}, Γ_{1} ▷ let x = V in W : B]]_{Θ}^{v} = [[!Δ]]⊗[[Γ_{2}]]⊗[[Γ_{1}]] ⟶^{id⊗_{!Δ}f} [[!Δ]]⊗[[Γ_{2}]]⊗[[A]] ⟶^{g} [[B]]}

\begin{aligned}[[!Δ, Γ_{1}, ▷ V : !^{n}(A_{1} ⊗ A_{2})]]_{Θ}^{v} & = [[!Δ]]⊗[[Γ_{1}]] ⟶^{f} L^{n}([[A_{1}]] ⊗ [[A_{2}]]) \\ [[!Δ, Γ_{2}, x : !^{n}A_{1}, y : !^{n}A_{2} ▷ W : C]]_{Θ}^{v} & = [[!Δ]]⊗[[Γ_{2}]]⊗L^{n}[[A_{1}]] ⊗ L^{n}[[A_{2}]] ⟶^{g} [[C]] \end{aligned}

[[!Δ, Γ_{2}, Γ_{1} ▷ let⟨x, y⟩^{n} = V in W : C]]_{Θ}^{v} = [[!Δ]]⊗[[Γ_{2}]]⊗[[Γ_{1}]] ⟶^{id⊗_{!Δ}f} [[!Δ]]⊗[[Γ_{2}]]⊗L^{n}([[A_{1}]]⊗[[A_{2}]])

⟶^{id⊗(d_{[[A_{1}]],[[A_{2}]]}^{L^{n}})^{−1}} [[!Δ]]⊗[[Γ_{2}]]⊗L^{n}[[A_{1}]]⊗L^{n}[[A_{2}]] ⟶^{g} [[C]]

\frac{[[!Δ, Γ_{2} ▷ V : ⊤]]_{Θ}^{v} = [[!Δ]] ⊗ [[Γ_{2}]] ⟶^{f} ⊤ [[!Δ, Γ_{1} ▷ W : C]]_{Θ}^{v} = [[!Δ]] ⊗ [[Γ_{1}]] ⟶^{g} [[C]]}{[[!Δ, Γ_{1}, Γ_{2} ▷ let ∗ = V in W : C]]_{Θ}^{v} = [[!Δ]]⊗[[Γ_{1}]]⊗[[Γ_{2}]] ⟶^{id⊗_{!Δ}f} [[!Δ]] ⊗ [[Γ_{1}]] ⟶^{g} [[C]]}

\frac{[[!Δ, Γ_{1} ▷ V : !^{n}A]]_{Θ}^{v} = [[!Δ]] ⊗ [[Γ_{1}]] ⟶^{f} L^{n}[[A]] [[!Δ, Γ_{2} ▷ W : !^{n}B]]_{Θ}^{v} = [[!Δ]] ⊗ [[Γ_{2}]] ⟶^{g} L^{n}[[B]]}{[[!Δ, Γ_{1}, Γ_{2} ▷ ⟨V, W ⟩^{n} : !^{n}(A ⊗ B)]]_{Θ}^{v} = [[!Δ]] ⊗ [[Γ_{1}]] ⊗ [[Γ_{2}]] ⟶^{f⊗_{!Δ}g} L^{n}[[A]] ⊗ L^{n}[[B]] ⟶^{d_{A,B}^{L^{n}}} L^{n}([[A]] ⊗ [[B]])}

Interpretation of computations: First, if U is a core value, [[Δ ▷ U : A]]_{Θ}^{c} = [[Δ ▷ U : A]]_{Θ}^{v}; η_{A}.

\frac{[[!Δ, Γ_{1} ▷ M : A ⊸ B]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{1}]] ⟶^{f} T ([[A]] ⊸ [[B]]) [[!Δ, Γ_{2} ▷ N : A]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{2}]] ⟶^{g} T ([[A]])}{[[!Δ, Γ_{1}, Γ_{2} ▷ MN : B]]_{Θ}^{c} = [[!Δ]]⊗[[Γ_{1}]]⊗[[Γ_{2}]] ⟶^{f⊗_{!Δ}g} T ([[A]]⊸[[B]])⊗T ([[A]]) ⟶^{Ψ_{1}} T (([[A]]⊸[[B]])⊗[[A]]) ⟶^{ε_{A,B}^{∗}} T ([[B]])}

\begin{aligned}[[!Δ, Γ_{1} ▷ M : !^{n}(A_{1} ⊗ A_{2})]]_{Θ}^{c} & = [[!Δ]] ⊗ [[Γ_{1}]] ⟶^{f} T L^{n}([[A_{1}]] ⊗ [[A_{2}]]) \\ [[!Δ, Γ_{2}, x : !^{n}A_{1}, y : !^{n}A_{2} ▷ N : C]]_{Θ}^{v} & = [[!Δ]] ⊗ [[Γ_{2}]] ⊗ L^{n}[[A_{1}]] ⊗ L^{n}[[A_{2}]] ⟶^{g} T ([[C]]) \end{aligned}

[[!Δ, Γ_{2}, Γ_{1} ▷ let⟨x, y⟩^{n} = M in N : !^{n}C]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{2}]] ⊗ [[Γ_{1}]] ⟶^{id⊗_{!Δ}f} [[!Δ]] ⊗ [[Γ_{1}]] ⊗ T L^{n}([[A_{1}]] ⊗ [[A_{2}]])

⟶^{t;T (id⊗(d^{L^{n}} )^{−1})} T ([[!Δ]] ⊗ [[Γ_{1}]] ⊗ L^{n}[[A_{1}]] ⊗ L^{n}[[A_{2}]]) ⟶^{g^{∗}} T [[C]]

\frac{[[!Δ, Γ_{2} ▷ M : ⊤]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{2}]] ⟶^{f} T (⊤) [[!Δ, Γ_{1} ▷ N : C]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{1}]] ⟶^{g} T ([[C]])}{[[!Δ, Γ_{1}, Γ_{2} ▷ let ∗ = M in N : C]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{1}]] ⊗ [[Γ_{2}]] ⟶^{id⊗_{!Δ}f} [[!Δ]] ⊗ [[Γ_{1}]] ⊗ T (⊤) ⟶^{t;g^{∗}} T ([[C]])}

\frac{[[!Δ, Γ_{1} ▷ M : !^{n}A]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{1}]] ⟶^{f} T L^{n}[[A]] [[!Δ, Γ_{2} ▷ N : !^{n}B]]_{Θ}^{c} = [[!Δ]] ⊗ [[Γ_{2}]] ⟶^{g} T L^{n}[[B]]}{[[!Δ, Γ_{1}, Γ_{2}▷⟨M, N⟩^{n} : !^{n}(A⊗B)]]_{Θ}^{c} = [[!Δ]]⊗[[Γ_{1}]]⊗[[Γ_{2}]] ⟶^{f⊗_{!Δ}g} T L^{n}[[A]]⊗T L^{n}[[B]] ⟶^{Ψ_{1};T d_{A,B}^{L^{n}}} T L^{n}([[A]]⊗[[B]])}

Table 6. Interpretation of values and computations.

Lemma 12. Suppose that Δ ▷ V : A is a valid typing judgment where V is a

value. Then [[Δ ▷ V : A]]^{c} = [[Δ]] ⟶^{[[Δ▷V:A]]^{v}} [[A]] ⟶^{η_{[[A]]}} T ([[A]]).

Proof. Proof by induction on V, using the bifunctoriality of ⊗_{LA} and the equations for strong monadicity in Definition 4. ⊓ ⊔

4.2 Soundness of the denotation

The axiomatic equivalence and the categorical semantics are two faces of the same coin. Indeed, as we will prove in this section, two terms in the same axiomatic equivalence class have the same denotation. A corollary is that the indexation of terms does not influence the denotation. This proves semantically the fact that it is safe to work with untyped terms. An alternate justification of this fact is of course the operational semantics, which was given in [19].

Lemma 13. Suppose M′ = {Δ′ <: Δ ▷ M : A <: A′}. Then [[Δ′ ▷ M′ : A′]]^{c} = I_{Δ′,Δ}; [[Δ ▷ M : A]]^{c}; T (I_{A,A′}). If M = V is a value, from Lemma 4, M′ = V′ is a value. Then [[Δ′ ▷ V′ : A′]]^{v} = I_{Δ′,Δ}; [[Δ ▷ V : A]]^{v}; I_{A,A′}.

Proof. Proof by structural induction on M. ⊓ ⊔

Lemma 14 (Substitution). Given two valid typing judgments !Δ, Γ_{1}, x : A ▷ M : B and !Δ, Γ_{2} ▷ V : A, the typing judgment !Δ, Γ_{1}, Γ_{2} ▷ M[V/x] : B is valid. Let h be [[!Δ, Γ_{1}, Γ_{2} ▷ M[V/x] : B]]^{c} and h′ be [[!Δ, Γ_{1}, Γ_{2} ▷ W [V/x] : B]]^{v}, in the case where M = W is a value. Then they are defined by

\xymatrix{[[!Δ]] ⊗ [[Γ_{1}]] ⊗ [[Γ_{2}]] \ar[d]^{_{Split_{!Δ,Γ_{1},Γ_{2}}}} \ar@{.>}[r]^{h} & T ([[B]]) & [[!Δ]] ⊗ [[Γ_{1}]] ⊗ [[Γ_{2}]] \ar[d]^{_{Split_{!Δ,Γ_{1},Γ_{2}}}} \ar@{.>}[r]^{h′} & [[B]] \\ _{[[!Δ]]⊗[[Γ_{1}]]⊗[[!Δ]]⊗[[Γ_{2}]]} \ar[r]^{_{id⊗[[!Δ,Γ_{2}▷V:A]]_{v}}} & [[!Δ]]⊗[[Γ_{1}]]⊗[[A]], \ar[u]^{_{[[!Δ,Γ_{1},x:A▷M:B]]_{c}}} & _{[[!Δ]]⊗[[Γ_{1}]]⊗[[!Δ]]⊗[[Γ_{2}]]} \ar[r]^{_{id⊗[[!Δ,Γ_{2}▷V:A]]_{v}}} & [[!Δ]]⊗[[Γ_{1}]]⊗[[A]]. \ar[u]^{_{[[!Δ,Γ_{1},x:A▷W:B]]_{v}}}}

Proof. Proof by induction on M, using Lemma 1, Lemma 12 and the naturality of Φ. ⊓ ⊔

Theorem 5. If Δ ▷ M ≈_{ax} M′ : A then [[Δ ▷ M : A]]_{Θ}^{c} = [[Δ ▷ M′ : A]]_{Θ}^{c} (and [[Δ ▷ M : A]]_{Θ}^{v} = [[Δ ▷ M′ : A]]_{Θ}^{v} if M is a value) for every interpretation Θ.

Proof. Proof by induction on M ≈_{ax} M′, using Lemmas 13 and 14. ⊓ ⊔

Corollary 1. If Erase(M) = Erase(M′) and if Δ ▷ M, M′ : A are valid typing judgments, then [[M]]^{c} = [[M′]]^{c} (and [[M]]^{v} = [[M′]]^{v} if M is a value).

Proof. Corollary of Theorems 1 and 5. ⊓ ⊔

4.3 Completeness

The category 𝒞_{λ} being a linear category for duplication, one can interpret the language in it. This section states that the defined lambda-calculus is an internal language of linear categories for duplication.

Since the category 𝒞_{λ} is a monoidal category, one can w.l.o.g. generalize the notion of pairing to finite tensor products of terms. Then the following results are true:

Lemma 15. In 𝒞_{λ}, a valid typing judgment x_{1} : A_{1}, … x_{n} : A_{n} ▷ M : B has for computational denotation (t : A_{1} ⊗ ⋯ ⊗ A_{n} ▷ let⟨x_{1}, … x_{n}⟩ = t in λ∗.M : ⊤⊸ B). If M = V is a value, the value interpretation is (t : A_{1} ⊗ ⋯ ⊗ A_{n} ▷ let⟨x_{1}, … x_{n}⟩ = t in V : B).

Proof. Proof by structural induction on M and V. ⊓ ⊔

Theorem 6. In 𝒞_{λ}, Θ being the identity, one has [[x : A ▷ M : B]]_{Θ}^{c} ≈_{ax} (x : A ▷ λ∗.M : ⊤ ⊸ B) and [[x : A ▷ V : B]]_{Θ}^{v} ≈_{ax} (x : A ▷ V : B).

Proof. Corollary of Lemma 15 ⊓ ⊔

5 Towards a denotational model of quantum lambda calculus

As noted in the introduction, this paper is mostly concerned with the categorical requirements for modeling a generic call-by-value linear lambda calculus, i.e., its type system (which includes subtyping) and equational laws. We have not yet specialized the language to a particular set of built-in operators, for example, those that are required for quantum computation.

However, since the quantum lambda calculus [19] is the main motivation behind our work, we will comment very briefly on what additional properties would be required to interpret its primitives. The quantum lambda calculus is obtained by instantiating and extending the call-by-value language of this paper with the following primitive types, constants, and operations:

Types:  bit, qbit
Constants: 0 : !bit, 1 : !bit

new : !(bit ⊸ qbit), U : !(qbit^{n} ⊸ qbit^{n}), meas : !(qbit ⊸!bit)

Operations: Γ_{1},!Δ ▷ P : bit Γ_{2},!Δ ▷ M : A Γ_{2},!Δ ▷ N : A Γ_{1}, Γ_{2},!Δ ▷ if P then M else N : A (if )

Here, U ranges over a set of built-in unitary operations. In the intended semantics, !bit ≅ bit, while !qbit is empty. new creates a new qubit, and meas measures a qubit.

The denotational semantics of these operations is already well-understood in the absence of higher-order types. They can all be interpreted in the category Q of superoperators from [18]. The part that is not yet well-understood is how these features interact with higher-order types.

In light of our present work, we can conclude that a model of the quantum lambda calculus consists of a linear category for duplication (𝒞, L, T, ⊸), such that the associated category of computations 𝒞_{T} contains the category Q of [18] as a full monoidal subcategory. To construct an actual instance of such a model is still an open problem.

6 Conclusion

We have developed a call-by-value, computational lambda-calculus for manipulating duplicable and non-duplicable data, together with an axiomatic equivalence relation on typed terms. We use a subtyping relation in order to have implicit promotion, dereliction, copying and discarding. Then we developed categorical model for the language, inspired by the work of [8] and [14]. We finally showed that the model is sound and complete with respect to the axiomatic equivalence.

References

1. Abramsky, S.: Computational interpretations of linear logic. Theoretical Computer Science 111 (1993) 3–57 2. Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In:

Proceedings of LICS’04. (2004) 415–425

3. Barendregt, H.P.: The Lambda-Calculus, its Syntax and Semantics. North Holland (1984)

4. Benton, N.: A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In: Proceedings of CSL’94, Selected Papers. Volume 933 of Lecture Notes in Computer Science. (1994) 121–135

5. Benton, N., Bierman, G., de Paiva, V.C.V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Proceedings of TLCA’93. Volume 664 of Lecture Notes in Computer Science. (1993) 75–90

6. Benton, N., Bierman, G., Hyland, M., de Paiva, V.C.V.: Linear lambda-calculus and categorical models revisited. In: Proceedings of CSL’92, Selected Papers. Volume 702 of Lecture Notes in Computer Science. (1992)

7. Benton, N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Proceedings of LICS’96. (1996) 420–431

8. Bierman, G.: On Intuitionistic Linear Logic. PhD thesis, Computer Science Department, Cambridge University (1993)

9. Coecke, B.: Quantum information-flow, concretely, abstractly. [17] 57–73

10. Coecke, B., Pavlovic, D.: Quantum measurements without sums. In Chen, G., Kauffman, L., Lomonaco, S.J., eds.: Mathematics of Quantum Computation and Technology. Chapman & Hall (2007) 559–596

11. Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings of POPL’05, ACM Press (2005)

12. Lalire, M., Jorrand, P.: A process algebraic approach to concurrent and distributed computation: operational semantics. [17] 109–126

13. Mac Lane, S.: Categories for the Working Mathematician. Springer Verlag (1998)

14. Moggi, E.: Notions of computation and monads. Information and Computation 93 (1991) 55–92

15. Schalk, A.: What is a model for linear logic. Manuscript (2004)

16. Seely, R.A.G.: *-autonomous categories and cofree coalgebras. Contemporary Mathematics 92 (1989)

17. Selinger, P., ed.: Proceedings of QPL’04. TUCS General Publication No 33, Turku Centre for Computer Science (2004)

18. Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14 (2004) 527–586

19. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science 16 (2006) 527–552

20. Selinger, P., Valiron, B.: On a fully abstract model for a quantum linear functional language. In: Preliminary proceedings of QPL’06. (2006) 103–115

21. van Tonder, A.: A lambda calculus for quantum computation. SIAM Journal of Computing 33 (2004) 1109–1135

22. Wadler, P.: There’s no substitute for linear logic. Manuscript, presented at MFPS’92 (1992)

23. Wootters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299 (1982) 802–803