Towards a semantics for higher-order quantum computation^{∗}

Peter Selinger^{†}

Abstract

The search for a semantics for higher-order quantum computation leads naturally to the study of categories of normed cones. In the first part of this paper, we develop the theory of continuous normed cones, and prove some of their basic properties, including a Hahn-Banach style theorem. We then describe two different concrete ∗-autonomous categories of normed cones. The first of these categories is built from completely positive maps as in the author’s semantics of first-order quantum computation. The second category is a reformulation of Girard’s quantum coherent spaces. We also point out why ultimately, neither of these categories is a satisfactory model of higher-order quantum computation.

1 Introduction

In quantum computation, one often considers programs which depend parametrically on a so-called black box, which is typically a quantum circuit that computes some unknown function. The black box is considered to be part of the input of the program, but it differs from ordinary data, such as qubits, in that it can only be tested via observing its input/output behavior. In the terminology of functional programming, programming with black boxes is a special case of what is known as higher-order functional programming, which means, programming with functions whose input and/or output may consist of other functions.

Recently, there have been some proposals for higher-order quantum programming languages, based on linear versions of the lambda calculus [11, 12, 10]. These languages have been given meaning syntactically, in terms of their operational behavior; however, there is currently no satisfactory denotational semantics of such higher-order quantum programming languages. This is in contrast to the first-order case, where a complete denotational description of the quantum computable functions on finite data types, based on superoperators, has been given [8].

∗This is a corrected version of an article which appeared in Proceedings of the 2nd International Workshop on Quantum Programming Languages, Turku Centre for Computer Science General Publication No 33, pp. 127-143, June 2004. Example 2.11 has been corrected. An expanded version with full proofs is also available.

†Department of Mathematics and Statistics, University of Ottawa, Ottawa, Ontario K1N 6N5, Canada. Email:

selinger@mathstat.uottawa.ca. Research supported by NSERC.

In trying to extend this work to the higher-order case, one is led to search for a symmetric monoidal closed category which contains the category of superoperators from [8] as a full, symmetric monoidal subcategory. This leads naturally to the study of categories of normed cones, as pioneered by Girard in his study of quantum coherent spaces [5].

In the first part of the present paper, we attempt to develop a systematic account of normed cones and their basic properties. The study of normed cones is similar, in many respects, to the study of normed vector spaces, but there are some important differences, notably the presence of a partial order, the so-called cone order. This order allows us to use techniques from domain theory [2], and to work with order-theoretic notions of convergence and continuity which are rather stronger than the corresponding notions that are usually available in normed vector spaces such as Banach spaces.

In the second part of this paper, we report on two instructive (but ultimately failed) attempts at constructing a model of higher-order quantum computation based on normed cone techniques. We describe two concrete categories of normed cones. The first such category is a direct generalizations of the category of superoperators from the author’s work on first-order quantum computation [8]. The second category is based on a reformulation of Girard’s quantum coherent spaces. Both categories turn out to be ∗-autonomous, and thus possess all the structure required to model higher-order linear language features (and more). However, neither of these categories yields the correct answer at base types, and thus they are not correct models of quantum computation. The author believes that the techniques used here are nevertheless interesting and might turn out to be building blocks in the construction of a model of higher-order quantum computation in the future.

Acknowledgments and Errata. I am grateful to Andrea Schalk for many useful discussions on the topics of this paper, and to Vincent Danos for corrections. The current version of this paper differs from the published version. I have corrected errors in Lemma 2.10 and Example 2.11, as well as some minor typos.

2 Cones

In this section, we develop the basic theory of continuous normed cones. The techniques used are similar to those employed in the study of normed vector spaces, except that we also make extensive use of domain-theoretic methods to exploit the partial order which naturally exists on cones. Another domain-theoretic treatment of cones was given by Tix [9], but the present work differs in many key details, such as the presence of a norm, and the consequently modified notion of completeness.

2.1 Abstract cones

Let ℝ_{+} be the set of non-negative real numbers. An abstract cone is analogous to a real vector space, except that we take ℝ_{+} as the set of scalars. Since ℝ_{+} is not a field, we have to replace the vector space law v + (−v) = 0 by a cancellation law v + u = w + u ⇒ v = w. We also require strictness, which means, no non-zero element has a negative.

Definition (Abstract cone). An abstract cone is a set V, together with two operations + : V × V → V and · : ℝ_{+} × V → V and a distinguished element 0 ∈ V, satisfying the following laws for all v, w, u ∈ V and λ, μ ∈ ℝ_{+}:

0 + v = v  1v = v
v + (w + u) = (v + w) + u (λμ)v = λ(μv)
v + w = w + v  (λ + μ)v = λv + μv
λ(v + w) = λv + λw,
v + u = w + u ⇒ v = w (cancellation)
v + w = 0 ⇒ v = w = 0 (strictness)

Example 2.1. ℝ_{+} is an abstract cone. The set

ℝ_{+}^{n} = {(x_{1}, …, x_{n}) | x_{1}, …, x_{n} ∈ ℝ_{+}}

is an abstract cone, with the coordinate-wise operations. More generally, if V_{1}, …, V_{n} are abstract cones, then so is V_{1} × … × V_{n}. The set of all complex hermitian positive n × n-matrices,

P_{n} = {A ∈ ℂ^{n×n} | A = A^{∗} and ∀v ∈ ℂ^{n}.v^{∗}Av ⩾ 0}

is an abstract cone.

Definition (Linear function). A linear function of abstract cones is a function f : V → W such that f(v + w) = f(v) + f(w) and f(λv) = λf(v), for all v, w ∈ V and λ ∈ ℝ_{+}.

Remark. Every abstract cone V can be completed to a real vector space env(V), which we call the enveloping space of V. The elements of env(V) are pairs (v, w), where v, w ∈ V, modulo the equivalence relation (v, w) ∼ (v′, w′) if v + w′ = v′ + w. Addition and multiplication by non-negative scalars are defined pointwise, and we define −(v, w) = (w, v). We say that an abstract cone is finite dimensional if its enveloping space is a finite dimensional vector space.

Definition (Convexity). A subset D of an abstract cone V is said to be convex if for all u, v ∈ D and λ ∈ [0, 1], λu + (1 − λ)v ∈ D. The convex closure of a set D is defined to be the smallest convex set containing D.

2.2 The cone order

Definition (Cone order). Let V be an abstract cone. The cone order is defined by v ⊑ w if there exists u ∈ V such that v + u = w. Note that the cone order is a partial order. If v ⊑ w, then we sometimes also write w − v for the unique element u such that v + u = w.

Remark. Note that every linear function of abstract cones f : V → W is also monotone, i.e., v ⊑ v′ implies f(v) ⊑ f(v′). Also, addition and scalar multiplication are monotone operations. Example 2.2. On ℝ_{+}, the cone order is just the usual order ⩽ of the reals. On ℝ_{+}^{n}, it is the pointwise order. On P_{n}, it is the so-called Löwner partial order [7].

Definition (Down-closure). Let D ⊆ V be a subset of an abstract cone. Its down-closure ↓D is the set {u ∈ V |∃v ∈ D.u ⊑ v}. We say that D is down-closed if D = ↓D. The concept of up-closure is defined dually. Note that the down-closure of a convex set is convex.

2.3 Normed cones

Definition (Norm). Let V be an abstract cone. A norm on V is a function ∥−∥ : V → ℝ_{+} satisfying the following conditions for all v, w ∈ V and λ ∈ ℝ_{+}:

∥v + w∥ ⩽ ∥v∥ + ∥w∥
∥λv∥ = λ∥v∥
∥v∥ = 0 ⇒ v = 0
v ⊑ w ⇒ ∥v∥ ⩽ ∥w∥

A normed cone V = ⟨V, ∥−∥⟩ is an abstract cone equipped with a norm.

Remark. The first three conditions of a norm are just the usual conditions for a norm on a vector space, except of course that the scalar property is restricted to non-negative scalars. The last condition ensures that the norm is monotone.

Definition (Unit ideal). The unit ideal of a normed cone V is the set

D_{V} = {v ∈ V | ∥v∥ ⩽ 1}

It is akin to the unit ball in a normed vector space.

2.4 Complete normed cones

We recall the definition of a directed complete partial order from domain theory [2].

Definition (Directed complete partial order (dcpo)). A partially ordered set A is called directed if for all a, b ∈ A, there exists c ∈ A with a, b ⊑ c. A partially ordered set (D, ⊑) is called a directed complete partial order (dcpo) if every directed subset A of D has a least upper bound in D. The least upper bound of a directed subset A is denoted by [figure]A, and it is also called the directed supremum, or sometimes the limit, of A.

If I is a directed poset and D is a dcpo, then a monotone map a : I → D is called an directed net (or simply net). As usual, we write a net as (a_{i})_{i∈I}. The image of a net is a directed subset of D, and its directed supremum is written as [figure]_{i∈I}a_{i}. Note that an increasing sequence is a particular kind of directed net.

Definition (Complete normed cone). A normed cone V is called complete if its unit ideal is a directed complete partial order.

Remark. A normed cone V is complete if and only if the following two conditions hold, for all directed nets (a_{i})_{i∈I} in V:

• if [figure]_{i}a_{i} exists, then ∥[figure]_{i}a_{i}∥ = [figure]_{i}∥a_{i}∥, and

• if {∥a_{i}∥ | i ∈ I} is bounded, then [figure]_{i}a_{i} exists.

The first of these condition states that the norm is Scott-continuous, i.e., it preserves directed suprema. The second condition is a completeness condition; it is akin to the requirement, in complete normed vector spaces, that every Cauchy sequence has a limit. However, unlike in normed vector spaces, we require convergence with respect to the order, not with respect to the norm. The norm merely serves to rule out unbounded sequences.

2.5 Examples

We write x ⊔ y for the maximum of two numbers x, y ∈ ℝ_{+}. Note that this operation is commutative and associative, has unit 0, and is distributive with respect to addition: (x ⊔ y) + z = (x + z) ⊔ (y + z).

Example 2.3. ℝ_{+} is a complete normed cone with ∥x∥ = x. The set ℝ_{+}^{n} is a complete normed cone with the 1-norm

∥(x_{1}, …, x_{n})∥_{1} := x_{1} + … + x_{n}.

The set ℝ_{+}^{n} is also a complete normed cone with the ∞-norm

∥(x_{1}, …, x_{n})∥_{∞} := x_{1} ⊔ … ⊔ x_{n}.

More generally, if V_{1}, …, V_{n} are complete normed cones, then each of the following formulas make V_{1} × … × V_{n} into a complete normed cone:

\begin{matrix}∥(v_{1}, …, v_{n})∥_{1} := ∥v_{1}∥_{V_{1}} + … + ∥v_{n}∥_{V_{n}}, \\ ∥(v_{1}, …, v_{n})∥_{∞} := ∥v_{1}∥_{V_{1}} ⊔ … ⊔ ∥v_{n}∥_{V_{n}}. \end{matrix}

We write V_{1} ⊕ … ⊕ V_{n} for the normed cone ⟨V_{1} × … × V_{n}, ∥−∥_{1}⟩, and we write V_{1} & … & V_{n} for the normed cone ⟨V_{1} × … × V_{n}, ∥−∥_{∞}⟩.

The set P_{n} of complex hermitian positive n × n-matrices is a complete normed cone with the 1-norm (or trace norm)

∥A∥_{1} = ∥A∥_{tr} = trA = ∑_{i} a_{ii}.

It is also a complete normed cone with the ∞-norm (or operator norm)

∥A∥_{∞} = sup{|Av| | v ∈ ℂ^{n}, |v| ⩽ 1},

where |v| = \sqrt{v^{∗}v} denotes the usual norm of a complex vector. Note that ∥A∥_{1} is the sum of the eigenvalues of A (counted according to multiplicity), and ∥A∥_{∞} is the maximum of the eigenvalues.

Example 2.4. Consider the set V = {(x, y) | x = y = 0 or x, y > 0} ⊆ ℝ^{2} with the norm ∥(x, y)∥ = x + y. Clearly, V is a normed cone. However, it is not complete: the increasing sequence v_{i} = (2 − 1/i, 2 − 1/i) has many upper bounds, none of which is least. For example, (2, 2) and (2, 3) are two incomparable minimal upper bounds.

Example 2.5. Let ℓ_{1} be the set of sequences in ℝ_{+} of bounded sum, together with the sum norm ∥(x_{i})_{i}∥_{1} = ∑_{i} x_{i}. Let ℓ_{∞} be the set of bounded sequences in ℝ_{+}, together with the supremum norm ∥(x_{i})_{i}∥_{∞} = sup_{i} x_{i}. Then both ℓ_{1} and ℓ_{∞} are complete normed cones. Least upper bounds are given pointwise.

Example 2.6. Let P be any partially ordered set, and let ℝ_{+}^{P} be the set of bounded monotone maps f : P → ℝ_{+}. Let ℝ_{+}^{P} be equipped with the pointwise operations of addition and scalar multiplication, and with the supremum norm ∥f∥_{∞} = sup{f(i) | i ∈ P }. Then ℝ_{+}^{P} is a complete normed cone. Least upper bounds of directed nets are given pointwise. However, note that the cone order ⊑ on ℝ_{+}^{P} does not in general coincide with the pointwise order, because for f ⊑ g, we must have that g − f is not only non-negative, but also monotone.

2.6 Continuous normed cones

We recall some additional concepts from domain theory [2].

Definition (Continuous dcpo). If w, v are elements of a dcpo D, we say that w is way below v, or in symbols, w << v, if for any directed set A with v ⊑ [figure]A, there exists some a ∈ A such that w ⊑ a. We write ↓ ↓v = {w | w << v} and ↑ ↑v = {w | v << w}. A dcpo D is called continuous if for every v ∈ D, the set ↓ ↓v is directed and v = [figure]↓ ↓v.

Definition (Continuous normed cone). A continuous normed cone is a complete normed cone whose unit ideal is a continuous dcpo.

Remark. If V is a complete normed cone, then V is continuous iff for every v ∈ V, the set ↓ ↓v is directed and v = [figure]↓ ↓v in V. In particular, continuity, as a property of complete normed cones, is independent of the norm; it only depends on the order.

2.7 Examples

Example 2.7. The complete cones ℝ_{+}, ℝ_{+}^{n}, P_{n}, ℓ_{∞}, and ℓ_{1} from Examples 2.3 and 2.5 are all continuous. In ℝ_{+}, we have x << y iff x = 0 or x < y. In ℝ_{+}^{n}, we have (x_{1}, …, x_{n}) << (y_{1}, …, y_{n}) iff for all i, x_{i} = 0 or x_{i} < y_{i}. In P_{n}, we have A << B iff for all v ∈ ℂ^{n}, v^{∗}Av = 0 or v^{∗}Av < v^{∗}Bv. In ℓ_{∞} and ℓ_{1}, we have x⃗ << y⃗ iff x⃗ is finitely supported and for all i, x_{i} = 0 or x_{i} < y_{i}. Moreover, if V_{1}, …, V_{n} are continuous normed cones, then so are V_{1} ⊕ … ⊕ V_{n} and V_{1} & … & V_{n}, and the way-below relation is given pointwise in this case.

Example 2.8. Let I = [0, 1] be the unit interval with the natural order. Consider the complete cone ℝ_{+}^{I} of monotone functions f : I → ℝ_{+} (see Example 2.6). We claim that ℝ_{+}^{I} is not a continuous cone. Indeed, consider the map g(x) = x, and suppose that f << g. We will show that f = 0. We first show that for any x ∈ I, there exists a neighborhood of x on which f is constant. Fix x ∈ I. For any ϵ > 0, define g_{ϵ} by

g_{ϵ}(y) = \{ \begin{matrix}y & if y ⩽ x − ϵ \\ x − ϵ & if x − ϵ < y ⩽ x + ϵ \\ y − 2ϵ & if x + ϵ < y. \end{matrix}

Then the net (g_{ϵ})_{ϵ>0} converges to g. Hence f ⊑ g_{ϵ} for some ϵ > 0. Since g_{ϵ} is constant on a neighborhood of x, and both f and g_{ϵ} − f are monotone, it follows that f is also constant on a neighborhood of x. As x was arbitrary, and I is connected, it follows that f is a constant function, hence necessarily f = 0. As there is only one element way below g, it follows that ℝ_{+}^{I} is not a continuous cone.

Open Problem. Characterize the partially ordered sets P for which ℝ_{+}^{P} is a continuous normed cone.

2.8 Order convergence and norm convergence

We have already remarked that, in the theory of normed cones, we normally consider convergence with respect to the order, and not with respect to the norm. However, it is sometimes useful to know more about the relationship between the two concepts.

Remark. Order-convergence does not in general imply norm-convergence; for instance, in ℓ_{∞}, the increasing sequence v_{j} = (1, 1, …, 1, 0, 0, …) has least upper bound (1, 1, …), but it does not converge in norm.

On the other hand, norm-convergence of increasing sequences implies order-conver-gence, as shown in the following lemma:

Lemma 2.9. Let V be a complete normed cone, (v_{i})_{i} an increasing sequence (or a directed net), and let v be an upper bound such that ∥v − v_{i}∥ → 0. Then v = [figure]_{i}v_{i}.

Proof. By completeness, a least upper bound exists, so let w = [figure]_{i}v_{i}. Since v is an upper bound, we have w ⊑ v. Now for all i, we have v_{i} ⊑ w, hence v − w ⊑ v − v_{i}, hence ∥v − w∥ ⩽ ∥v − v_{i}∥. As the latter quantity converges to 0, we must have ∥v − w∥ = 0, hence v = w. □

2.9 Bounded and non-expanding functions

Definition (Bounded and non-expanding linear function). Let V and W be complete normed cones. A linear function of cones f : V → W is bounded if there exists a constant c ∈ ℝ_{+} such that for all v ∈ V, ∥f(v)∥ ⩽ c∥v∥. It is non-expanding if for all v ∈ V, ∥f(v)∥ ⩽ ∥v∥.

Perhaps surprisingly, the definition of boundedness is redundant, as the following lemma shows:

Lemma 2.10. Any monotone function satisfying f(λv) = λf(v) (and therefore any linear function) between complete normed cones is bounded.

Proof. Suppose f : V → W is monotone but unbounded. For each i, choose an element v_{i} ∈ V such that ∥v_{i}∥ = 1 but ∥f(v_{i})∥ ⩾ i · 2^{i}. Now consider the sequence whose ith element is

u_{i} = v_{0} + \frac{1}{2}v_{1} + \frac{1}{4}v_{2} + … + \frac{1}{2^{i}} v_{i}.

Then (u_{i})_{i} is an increasing sequence in V, with ∥u_{i}∥ ⩽ 2 for all i. By completeness, this sequence has a least upper bound u = [figure]_{i}u_{i} with ∥u∥ ⩽ 2. On the other hand, by construction, we have ∥f(u_{i})∥ ⩾ ∥f(v_{i})∥/2^{i} ⩾ i. Now for all i, we have u_{i} ⊑ u, thus f(u_{i}) ⊑ f(u), thus i ⩽ ∥f(u_{i})∥ ⩽ ∥f(u)∥. This contradicts the fact that f(u) has finite norm. □

2.10 Continuous linear functions

Definition (Continous linear function). Let V and W be complete normed cones. A function of cones f : V → W is called Scott-continuous (or simply continuous) if it preserves directed suprema, i.e., if f([figure]_{i}a_{i}) = [figure]_{i}f(a_{i}) for all bounded directed nets (a_{i})_{i}.

Example 2.11. Consider ℓ_{∞} as in Example 2.5, and let U be an ultrafilter on ℕ. For any sequence x̄ = (x_{i})_{i} ∈ ℓ_{∞}, define lim_{U} x̄ to be the supremum of all a ∈ ℝ_{+} such that {i | x_{i} ⩾ a} ∈ U. Then the function f(x̄) = lim_{U} x̄ is linear (and thus bounded by Lemma 2.10), but not continuous: it maps each member of the increasing sequence v_{j} = (1, 1, …, 1, 0, 0, …) to 0, but maps its least upper bound to 1.

Lemma 2.12. In a complete normed cone, addition and scalar multiplication are continuous.

Proof. Note that for any fixed a, the function f(v) = a + v is an order isomorphism from V to {u ∈ V | a ⊑ u}; hence, it preserves least upper bounds of non-empty sets. Since Scott continuity is pointwise, addition as a function of two arguments is also continuous. Similarly, for any non-zero scalar λ, the function g(v) = λv is an order isomorphism from V to itself, thus preserving least upper bounds. In case λ = 0, there is nothing to show. Thus, λv is continuous as a function of v. Finally, the fact that λv is continuous as a function of λ follows from Lemma 2.9, because λ = [figure]_{i}λ_{i} implies ∥λv − λ_{i}v∥ = |λ − λ_{i}|∥v∥ → 0. □

2.11 A separation theorem

Definition (Generating set). Let V be an abstract cone, and let B ⊆ V be a down-closed, convex subset. We say that B generates V if for all v ∈ V, there exists some λ > 0 such that λv ∈ B.

Recall that a subset U of a dcpo D is called Scott-open, or simply open, if it is upclosed and for any directed set A with [figure]A ∈ U, there exists some a ∈ A ∩ U. A set is Scott-closed or closed if its complement is open.

Theorem 2.13 (Separation). Let V be a continuous normed cone, and let B and U be convex sets such that B is down-closed, U is up-closed and open, and B ∩U = ∅. Further, assume that B generates V. Then there exists a continuous linear function f : V → ℝ_{+} such that f(v) ⩽ 1 for all v ∈ B and f(u) > 1 for all u ∈ U. □

2.12 A Hahn-Banach style theorem

An important application of the separation theorem is the following Hahn-Banach style theorem for continuous normed cones:

Theorem 2.14. Let V be a continuous normed cone, and let a ∈ V with ∥a∥ > 1. Then there exists a continuous linear function f : V → ℝ_{+} with f(v) ⩽ ∥v∥, for all v ∈ V, such that f(a) > 1.

Proof. Since the norm is continuous, we can find some a′ << a such that ∥a′∥ > 1. Now apply the separation theorem to the sets B = {v ∈ V | ∥v∥ ⩽ 1} and U = ↑ ↑a′. □

Remark. One might ask whether the function f in Theorem 2.14 can be chosen so that f(a) = ∥a∥. Contrary to basic intuitions, this is not in general possible, unless one gives up the continuity of f. Consider the following counterexample. Let V = ℓ_{∞}, the set of bounded sequences in ℝ_{+} with the supremum norm (see Examples 2.5 and 2.7). Note that every sequence (x_{i})_{i} ∈ V is a directed supremum of finitely supported sequences; therefore, every continuous linear function is uniquely determined by its action on the standard basis vectors e_{j} = (δ_{ij})_{i} ∈ V. Now let a = (a_{i})_{i} where a_{i} = 2 − \frac{1}{i+1}. Then ∥a∥ = sup_{i} a_{i} = 2. However, we claim that there exists no continuous function f : V → ℝ_{+} with f(v) ⩽ ∥v∥, for all v ∈ V, such that f(a) = 2. For assume that there was such a function f. For every i, let v_{i} = a + \frac{1}{i+1}e_{i} ∈ V. Then f(v_{i}) ⩾ f(a) = 2, but also f(v_{i}) ⩽ ∥(∥v_{i}) = 2, hence f(v_{i}) = f(a) + \frac{1}{i+1}f(e_{i}) = 2. But also f(a) = 2, which implies that f(e_{i}) = 0 for all i. Since f is uniquely determined by all the f(e_{i}), it follows that f = 0, a contradiction.

3 Completely positive maps and superoperators

Categories of completely positive maps and superoperators occur naturally in the semantics of quantum programming languages, see [8]. In this section, we briefly recall the definition of these concepts. The category of superoperators is symmetric monoidal, but it lacks closed structure. Thus, it forms a useful semantics of first-order, but not higherorder quantum programming languages. In Sections 4 and 5, we will discuss two different ∗-autonomous categories derived from the category of superoperators.

3.1 Signatures, linear maps, and the category V

Definition (Signature, matrix tuple). A signature is a finite sequence σ = n_{1}, …, n_{s} of positive natural numbers, where s ⩾ 0. If n is a positive natural number, let V_{n} = ℂ^{n×n} be the set of complex n × n-matrices, regarded as a complex vector space. More generally, if σ = n_{1}, …, n_{s} is a signature, let V_{σ} = V_{n_{1}} × … × V_{n_{s}} be the set of matrix tuples ⟨A_{1}, …, A_{s}⟩, where A_{i} ∈ ℂ^{n_{i}×n_{i}}.

Definition (The category V). The category V has signatures as objects, and a morphism from σ to τ is a complex linear function f : V_{σ} → V_{τ}.

Note that the category V is equivalent to the category of finite dimensional complex vector spaces; we have defined the objects in a special way because we will equip them with additional structure later.

Let σ ⊕ σ′ denote concatenation of signatures. Then σ ⊕ σ′ is a biproduct in the category V, with the obvious projection and injection maps. The neutral object for this biproduct is the empty signature, which we denote as 0.

The tensor product of two signatures σ = n_{1}, …, n_{s} and τ = m_{1}, …, m_{t} is defined as

σ ⊗ τ = n_{1}m_{1}, …, n_{1}m_{t}, …, n_{s}m_{1}, …, n_{s}m_{t}.

Note that there is a canonical isomorphism V_{σ⊗τ} ≅ V_{σ} ⊗ V_{τ}, where V_{σ} ⊗ V_{τ} denotes the usual tensor product of vector spaces. With this identification, the operation ⊗ is seen to give rise to a symmetric monoidal structure on V. The unit for this tensor product is the signature I = 1.

Moreover, there is a canonical natural isomorphism † : V(σ ⊗ τ, ρ) ≅ V(σ, τ ⊗ ρ) [8]. Therefore, the category V, just like the category of finite dimensional vector spaces, is compact closed with σ −∘ τ = σ ⊗ τ and ⊥ = I = 1. As a matter of fact, the category V is even strongly compact closed in the sense of Abramsky and Coecke [1].

3.2 Completely positive maps and the category CPM

For a positive natural number n, let P_{n} ⊆ V_{n} be the set of hermitian positive n × nmatrices as in Example 2.1. More generally, for any signature σ = n_{1}, …, n_{s}, let P_{σ} = P_{n_{1}} × … × P_{n_{s}} ⊆ V_{σ} be the set of hermitian positive matrix tuples.

Definition (Completely positive map). Let σ, σ′ be signatures. A linear function f : V_{σ} → V_{σ′} is positive if for all A ∈ P_{σ}, one has f(A) ∈ P_{σ′}. Further, we say that f is completely positive if id_{τ} ⊗ F : V_{τ⊗σ} → V_{τ⊗σ′} is positive for all signatures τ.

Example 3.1. The linear function f : V_{2} → V_{2} defined by f( \begin{matrix}a & b \\ c & d \end{matrix} ) = ( \begin{matrix}a & c \\ b & d \end{matrix} ) is

positive, but not completely positive. To see this, note that f maps hermitian positive matrices to hermitian positive matrices, but id_{2} ⊗ f does not; for instance,

id_{2} ⊗ f( \begin{matrix}1 & 0 & 0 & 1 \\ 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & 1 \end{matrix} ) = ( \begin{matrix}1 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \end{matrix} ).

On the other hand, the function g( \begin{matrix}a & b \\ c & d \end{matrix} ) = ( \begin{matrix}a & 0 \\ 0 & d \end{matrix} ) is completely positive.

Definition (The category CPM). The category CPM of completely positive maps has the same objects as V, and has the completely positive maps as morphisms.

Lemma 3.2. CPM is a subcategory of V, and it inherits the biproducts and (strongly) compact closed structure from V. □

Remark. The category CPM was called W in [8].

3.3 Superoperators and the category Q

Let σ = n_{1}, …, n_{s} be a signature, and let A = ⟨A_{1}, …, A_{s}⟩ ∈ V_{σ} be a tuple of matrices. We define the trace of A to the sum of the traces of A_{1}, …, A_{s}:

trA = ∑_{i} trA_{i}.

Definition (Superoperator). Let σ, σ′ be signatures. A linear function f : V_{σ} → V_{σ′} is called a superoperator if f is completely positive and for all A ∈ P_{σ}, trf(A) ⩽ trA.

Definition (The category Q). The category Q of superoperators has the same objects as V and CPM, and has the superoperators as morphisms.

Lemma 3.3. Q is a subcategory of CPM. It inherits coproducts and the symmetric monoidal structure from CPM, but it fails to have products and it is not monoidal closed.

□

The reason the category Q fails to inherit the products from CPM is that the diagonal map f : σ → σ ⊕ σ with f(A) = (A, A) is trace increasing, and thus not a superoperator. The fact that Q is not monoidal closed follows from the characterization of superoperators in [8, Thm. 6.7]; it is easily seen that the hom-set Q(σ, τ) is not in one-to-one correspondence with Q(I, ρ) for any ρ.

However, the category Q also has some additional structure which is not present in CPM: it is dcpo-enriched, and consequently, it possesses a traced monoidal structure for the coproducts ⊕ (see [6, Ch. 7]). This structure can be used to interpret loops and recursion in first-order functional quantum programming languages; for details, see [8, Thm. 6.7].

4 Normed matrix spaces

Our goal is to find a monoidal closed category which contains the category Q, preferably as a full subcategory. In this section, we will describe one approach to defining such a category, which we call Q′. The idea is very simple: in the definition of a superoperator, replace the “trace” on each object by an arbitrary norm.

4.1 The category Q′

Definition (Normed matrix space). A normed matrix space is a pair V = ⟨σ, ∥−∥_{V} ⟩, where σ is a signature and ∥−∥_{σ} is a norm on the cone P_{σ}. We sometimes also call a normed matrix space a concrete cone, and we often identify it with the “underlying” normed cone ⟨P_{σ}, ∥−∥_{V} ⟩. We also often write P_{V} for P_{σ}, and similarly D_{V} for the unit ideal.

Definition (The category Q′). The category Q′ has as its objects normed matrix spaces V = ⟨σ, ∥−∥_{V} ⟩. A morphism from V = ⟨σ, ∥−∥_{V} ⟩ to W = ⟨τ, ∥−∥_{W} ⟩ is a completely positive map f : V_{σ} → V_{τ} which is norm-non-increasing, i.e., which satisfies ∥f(A)∥_{W} ⩽ ∥A∥_{V} for all A ∈ P_{σ}.

Remark. Since P_{σ} is a finite dimensional cone (i.e., embeddable in a finite dimensional vector space) and satisfies certain other regularity conditions, one can show that any norm ∥−∥ in the sense of Section 2.3 is automatically Scott-continuous and makes P_{σ} into a continuous normed cone. Similarly, any linear map of cones f : P_{σ} → P_{τ} is automatically continuous. Thus, the results of Section 2, and in particular the Hahn-Banach theorem, apply in this setting, even though continuity need not be stated explicitly as an axiom. These observations tend to simplify proofs in the finite dimensional case.

4.2 Properties of the category Q′

The category Q′ contains Q as a full subcategory. Indeed, to each object σ of Q, we can associate an object ⟨σ, ∥−∥_{tr}⟩ of Q′, where ∥A∥_{tr} = trA is the trace norm. It is then clear that the morphisms between these objects are precisely those of Q.

The category Q′ also inherits products, coproducts, and a symmetric monoidal closed structure from the category CPM, as we will now show. The structure is preserved by the forgetful functor Q′ → CPM.

4.2.1 Coproducts and products.

Given two normed matrix spaces V = ⟨σ, ∥−∥_{V} ⟩ and W = ⟨τ, ∥−∥_{W} ⟩, we define

\begin{aligned}V ⊕ W & = & ⟨σ ⊕ τ, ∥−∥_{V ⊕W} ⟩, \\ V & W & = & ⟨σ ⊕ τ, ∥−∥_{V & W} ⟩, \end{aligned}

where ∥(A, B)∥_{V ⊕W} = ∥A∥_{V} + ∥B∥_{W} and ∥(A, B)∥_{V & W} = ∥A∥_{V} ⊔ ∥B∥_{W} as in Example 2.3. Recall that “⊔” denotes the binary “maximum” operation on real numbers. It is easy to verify that with these norms, V ⊕ W is a coproduct and V & W is a product in the category Q′. Further, the object 0, with the empty signature and the unique norm, serves as the neutral object for the coproducts and products.

Remark. Just like the category Q, the category Q′ is also dcpo-enriched, and hence the coproduct operation ⊕ possesses a traced structure.

4.2.2 Symmetric monoidal structure.

Given normed matrix spaces V = ⟨σ, ∥−∥_{V} ⟩ and W = ⟨τ, ∥−∥_{W} ⟩, we would like to define their tensor product

V ⊗ W = ⟨σ ⊗ τ, ∥−∥_{V ⊗W} ⟩.

The question is how to define the norm ∥−∥_{V ⊗W}. By analogy with normed vector spaces, it would seem that the following definition is an obvious candidate, for C ∈ P_{V ⊗W}:

∥C∥_{V ⊗W} = inf{∑_{i} ∥A_{i}∥_{V} ∥B_{i}∥_{W} | C = ∑_{i} A_{i} ⊗ B_{i}, where A_{i} ∈ P_{V}, B_{i} ∈ P_{W}}.

(1)

However, there is a problem with this definition: the set over which the infimum is taken may in general be empty. In other words, not every element of P_{V ⊗W} can be written of the form ∑_{i} A_{i} ⊗ B_{i}, where A_{i} ∈ P_{V} and B_{i} ∈ P_{W}. This is best illustrated in an example, where σ = τ = 2.

Example 4.1. The matrix

C = ( \begin{matrix}1 & 0 & 0 & 1 \\ 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & 1 \end{matrix} )

cannot be written in the form ∑_{i} A_{i} ⊗ B_{i}, for positive 2 × 2-matrices A_{i}, B_{i}. To see why this is not possible, suppose it could be written in this way. Then the blockwise transpose

∑_{i} A_{i} ⊗ B_{i}^{T} = ( \begin{matrix}1 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \end{matrix} )

would also have to be positive, which it is not. □

Remark. The phenomenon described in the previous example is well-known in physics. A density matrix C ∈ P_{V ⊗W} of a bipartite quantum system can be written in the form ∑_{i} A_{i} ⊗B_{i} if and only if it is entanglement free, which means that there are only classical probabilistic correlations between the two parts. Such a state can be prepared using only classical communication.

In order to arrive at a useful definition of the tensor norm, equation (1) must be modified in some suitable way. One natural modification, which leads to a ∗-autonomous structure, is to replace “=” by “⊑” in the right-hand-side of the equation. We obtain the following:

Definition (Tensor product, tensor norm). Given normed matrix spaces V = ⟨σ, ∥−∥_{V} ⟩ and W = ⟨τ, ∥−∥_{W} ⟩, their tensor product is defined as V ⊗ W = ⟨σ ⊗ τ, ∥−∥_{V ⊗W} ⟩, where for all C ∈ P_{σ⊗τ},

∥C∥_{V ⊗W} = inf{∑_{i} ∥A_{i}∥_{V} ∥B_{i}∥_{W} | C ⊑ ∑_{i} A_{i} ⊗ B_{i}, where A_{i} ∈ P_{V}, B_{i} ∈ P_{W}}.

(2)

The definition of the tensor norm in terms of equation (2) is often impractical to work with. The following is a more practical characterization of the tensor norm in terms of its unit ideal.

Lemma 4.2. The unit ideal D_{V ⊗W} of V ⊗ W is the smallest Scott-closed, down-closed, convex set containing D_{V} ⊗ D_{W} = {A ⊗ B | A ∈ D_{V} , B ∈ D_{W} }. □

With this characterization, it is easy to prove that ⊗ defines a symmetric monoidal structure on the category Q′.

4.2.3 Monoidal closed structure

Recall from Section 3.2 that the category CPM is compact closed with σ−∘τ = σ⊗τ. We can lift this to a monoidal closed structure on Q′. In the following definition, we identify a completely positive map f : V_{σ} → V_{τ} with an element of V_{σ⊗τ} in the standard way, see [8, Sec. 6.7].

Definition (Monoidal closure). Given normed matrix spaces V = ⟨σ, ∥−∥_{V} ⟩ and W = ⟨τ, ∥−∥_{W} ⟩, their function space is defined as V −∘ W = ⟨σ ⊗ τ, ∥−∥_{V −∘W} ⟩, where for all f ∈ P_{σ⊗τ},

∥f∥_{V −∘W} = sup{∥f(A)∥_{W} | ∥A∥_{V} ⩽ 1}.  (3)

This is the usual definition of an operator norm; note that boundedness (Lemma 2.10) guarantees that the supremum in equation (3) always exists. The properties of a norm are easily verified, so that V −∘ W is a well-defined space. To prove that this indeed yields the correct monoidal closed structure corresponding to the tensor product ⊗, it suffices to prove the following, which is a consequence of Lemma 4.2:

Lemma 4.3. For normed matrix spaces V, W, and U, a completely positive map f : V ⊗ W → U is norm-non-increasing if and only if its adjoint f^{†} : V → W −∘ U is norm-non-increasing. □

4.2.4 The ∗-autonomous structure

A ∗-autonomous category is a symmetric monoidal closed category with an object ⊥, such that the canonical natural morphism V → (V −∘ ⊥) −∘ ⊥ is an isomorphism [3, 4]. The object ⊥ is called a dualizing object. It is common to write V^{⊥} = V −∘ ⊥.

Lemma 4.4. In the category Q′, the object ⊥ := I is a dualizing object.

Proof. Let V = ⟨σ, ∥−∥_{V} ⟩ be a normed matrix space. We already know that the canonical morphism δ : V → (V −∘⊥)−∘⊥ is an isomorphism in the category of completely positive maps. It remains to be shown that its inverse is norm-non-increasing, or equivalently, that δ is norm-non-decreasing. So let A ∈ P_{σ} with ∥A∥_{V} > 1. It suffices to show that ∥δ(A)∥ > 1. By the Hahn-Banach theorem (Theorem 2.14) there exists a linear function f : V → ℝ_{+} with f(B) ⩽ ∥B∥_{V} for all B, and such that f(A) > 1. Then f ∈ V −∘ ⊥ and ∥f∥_{V −∘⊥} ⩽ 1, hence ∥δ(A)∥ ⩾ ∥δ(A)(f)∥_{⊥} = ∥f(A)∥_{⊥} = f(A) > 1. □

Thus, we have:

Proposition 4.5. The category Q′ of normed matrix spaces is ∗-autonomous with finite products and coproducts and a zero object.

4.3 Why Q′ is not a model of higher-order quantum computation

The construction of the category Q′ was motivated by the search for a semantics of higherorder quantum computation, extending the semantics of first-order quantum computation given in [8]. It almost seems like this goal has been accomplished: we have obtained a category Q′ which is ∗-autonomous and which also contains the category Q of first-order quantum computations as a full subcategory. However, there is a fatal problem: The full embedding of Q in Q′ does not preserve the tensor product. We illustrate the problem in an example: Example 4.6. Consider the normed matrix space V = W = ⟨2, ∥−∥_{tr}⟩ of 2 × 2-matrices with the trace norm. This space lies within the image of the embedding of Q in Q′. Consider the space V ⊗ W with the norm ∥−∥_{V ⊗W}, as defined by equation (2). We claim that the norm on V ⊗ W is not the trace norm, and thus V ⊗ W does not lie within the image of Q in Q′. Let

C = ( \begin{matrix}1 & 0 & 0 & 1 \\ 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & 1 \end{matrix} )

as in Example 4.1. We claim that ∥C∥_{V ⊗W} = 4. Indeed, it is easy to see that

C ⊑ ( \begin{matrix}2 & 0 \\ 0 & 0 \end{matrix} ) ⊗ ( \begin{matrix}1 & 0 \\ 0 & 0 \end{matrix} ) + ( \begin{matrix}0 & 0 \\ 0 & 2 \end{matrix} ) ⊗ ( \begin{matrix}0 & 0 \\ 0 & 1 \end{matrix} ),

hence ∥C∥_{V ⊗W} ⩽ 4 by definition. To see that ∥C∥_{V ⊗W} ⩾ 4, consider the dual space V^{⊥}; for a 2 × 2-matrix B, ∥B∥_{V^{⊥}} is the maximal eigenvalue of B. Since this is bounded by the trace of B, the “identity” function f : V → V^{⊥} is norm-non-increasing. Therefore, by Lemma 4.3, its adjoint g : V ⊗ V → ⊥ is also norm-non-increasing; it maps a 4 ⊗ 4matrix (a_{ij}) to a_{00} + a_{03} + a_{30} + a_{33}. It follows that ∥C∥_{V ⊗W} ⩾ ∥g(C)∥_{⊥} = g(C) = 4, as claimed. On the other hand, the trace norm of C would be 2, and therefore ∥C∥_{tr⊗ tr} and ∥C∥_{tr} do not coincide.

5 Quantum coherent spaces

Girard introduced quantum coherent spaces as a new model of linear logic, inspired by quantum theory [5]. Quantum coherent spaces are closely related to spaces of density matrices, and they also form a ∗-autonomous category. Thus, one might ask whether they are suitable as a model for higher-order quantum computation. We will briefly sketch the definition of a version of quantum coherent spaces, adapted to the terminology of the present paper. We will also point out why they do not form a model for higher-order quantum computation.

The definitions given here differ from those of [5] in several details. For instance, we view quantum coherent spaces as certain normed cones, whereas Girard axiomatizes them directly in terms of their unit ideals. Also, we work with strict cones, whereas Girard allows non-strict cones, where the cone order is only a preorder and its induced equivalence relation must be factored out. Finally, we work with spaces of matrix tuples, whereas Girard works with spaces of matrices only (expressing matrix tuples, in effect, as block diagonal matrices). A formal proof of the equivalence of our definitions with Girard’s is not within the scope of this paper, and will be given elsewhere.

5.1 Tensor product, revisited

To motivate the definition of quantum coherent spaces, reconsider the problem from Section 4.3: if V, W are spaces in Q, then the norm on V ⊗ W in the categories Q and Q′ does not coincide. Just like the problem with equation (1), this problem can be attributed to the presence of elements in V ⊗ W which are not of the form ∑_{i} A_{i} ⊗ B_{i}; indeed, it is easy to check that for elements of the latter form, the two norms do indeed coincide.

It therefore seems natural to change the definition of the tensor product by simply removing the troublesome elements. This is precisely what quantum coherent spaces achieve. Informally, the tensor product of P_{σ} and P_{τ} is not taken to be P_{σ⊗τ}, but only a certain subset R ⊆ P_{σ⊗τ}, namely, the subset consisting precisely of the elements of the form ∑_{i} A_{i} ⊗ B_{i}. The sets R propagate to higher types. Thus, a quantum coherent space is a triple ⟨σ, R, ∥−∥⟩ of a signature, a cone R ⊆ V_{σ}, and a norm which makes R into a continuous normed cone. The formal definition follows in the next subsection.

One important feature of the category of quantum coherent spaces is that, unlike the category Q′ of the previous section, it is not based on completely positive maps, but on all positive maps. Informally speaking, this is because one has “reduced” the size of the tensor product, and thus one has to “increase” the size of the function spaces to keep the symmetric monoidal closed structure.

5.2 The category QCS

Definition (Quantum coherent space (adapted from [5])). A quantum coherent space is a triple V = ⟨σ, R_{V} , ∥−∥_{V} ⟩, where σ is a signature, R_{V} ⊆ V_{σ} is a cone, and ∥−∥_{V} is a norm making R_{V} into a continuous normed cone.

Definition (The category QCS). The category QCS has quantum coherent spaces as objects. A morphism from V = ⟨σ, R_{V} , ∥−∥_{V} ⟩ to W = ⟨τ, R_{W} , ∥−∥_{W} ⟩ is any linear, norm-non-increasing map of cones f : R_{V} → R_{W}.

The category of quantum coherent spaces possesses a ∗-autonomous structure with finite coproducts and products, given as follows: For V = ⟨σ, R_{V} , ∥−∥_{V} ⟩ and W = ⟨τ, R_{W} , ∥−∥_{W} ⟩,

\begin{aligned}V ⊕ W & = & ⟨σ ⊕ τ, R_{V} × R_{W} , ∥−∥_{V ⊕W} ⟩, \\ V & W & = & ⟨σ ⊕ τ, R_{V} × R_{W} , ∥−∥_{V & W} ⟩, \\ V ⊗ W & = & ⟨σ ⊗ τ, R_{V} ⊗ R_{W} , ∥−∥_{V ⊗W} ⟩, \\ V −∘ W & = & ⟨σ ⊗ τ, R_{V} −∘ R_{W} , ∥−∥_{V −∘W} ⟩. \end{aligned}

Here, ∥−∥_{V ⊕W} and ∥−∥_{V & W} are defined as in Section 4.2.1. The tensor cone is defined as R_{v} ⊗ R_{W} = {∑_{i∈I} A_{i} ⊗ B_{i} | A_{i} ∈ R_{V} , B_{i} ∈ R_{W} }, where I ranges over possibly infinite index sets such that the given sum converges. The tensor norm ∥−∥_{V ⊗W} is defined as in equation (2), except of course that we use R_{V} and R_{W} in place of P_{V} and P_{W}. The function space cone R_{V} −∘ R_{W} is the set of all continuous linear functions from R_{V} to R_{W}, and ∥−∥_{V −∘W} is the operator norm. The dualizing object is again I = ℝ_{+}. Remark. Note that a morphism between quantum coherent spaces is precisely a morphism between normed cones ⟨R_{V} , ∥−∥_{V} ⟩ and ⟨R_{W} , ∥−∥_{W} ⟩; thus, the forgetful functor from QCS to the category of normed cones is full and faithful. On the other hand, every finite dimensional cone can be embedded in some V_{σ}; thus, the category of quantum coherent spaces is equivalent to a suitable category of finite dimensional continuous normed cones.

5.3 Why QCS is not a model of higher-order quantum computation

Like the category Q′, the category QCS of quantum coherent spaces is ∗-autonomous, and therefore it has the required structure for modeling higher-order linear functions. There is also a canonical embedding of Q inside QCS, mapping each signature σ to ⟨σ, P_{σ}, ∥−∥_{tr}⟩. However, this embedding is not full, because of the presence of positive, non-completely positive maps in QCS. Since it was shown in [8] that the category Q captures precisely the feasible quantum functions at first-order types, it therefore follows that QCS contains some ground type morphisms, such as the morphism f from Example 3.1, which do not correspond to physically computable functions. On the other hand, there are physically feasible density matrices, such as the matrix C from Example 4.1, which do not have a valid denotation in the category QCS due to the restricted nature of its tensor cone.

References

[1] S. Abramsky and B. Coecke. A categorical semantics of quantum protocols. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004. IEEE Computer Society Press, 2004. To appear.

[2] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, 1994.

[3] M. Barr. *-Autonomous Categories. Lecture Notes in Mathematics 752. Springer Verlag, 1979.

[4] M. Barr. *-Autonomous categories and linear logic. Mathematical Structures in Computer Science, 1:159–178, 1991.

[5] J.-Y. Girard. Between logic and quantic: a tract. Manuscript, Oct 2003.

[6] M. Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec. PhD thesis, Department of Computer Science, University of Edinburgh, July 1997.

[7] K. Löwner. Über monotone Matrixfunktionen. Mathematische Zeitschrift, 38:177– 216, 1934.

[8] P. Selinger. Towards a quantum programming language. To appear in Mathematical Structures in Computer Science.

[9] R. Tix. Some results on Hahn-Banach-type theorems for continuous D-cones. Theoretical Computer Science, 264:205–218, 2001.

[10] B. Valiron. Quantum typing. In Proceedings of the 2nd International Workshop on Quantum Programming Languages, pages 163–178. Turku Centre for Computer Science General Publication No 33, June 2004.

[11] A. van Tonder. A lambda calculus for quantum computation. To appear in SIAM Journal on Computing. Available from arXiv:quant-ph/0307150, July 2003.

[12] A. van Tonder. Quantum computation, categorical semantics and linear logic. Available from arXiv:quant-ph/0312174, Dec. 2003.