arXiv:1711.05159v1 [cs.LO] 14 Nov 2017

CLASSICAL CONTROL, QUANTUM CIRCUITS AND LINEAR LOGIC
IN ENRICHED CATEGORY THEORY
MATHYS RENNELA AND SAM STATON
Radboud University, Nijmegen, The Netherlands
e-mail address: mathysr@cs.ru.nl
Oxford University, Oxford, The United Kingdom
e-mail address: sam.staton@cs.ox.ac.uk

Abstract. We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier
work on QWire by Paykin et al., we consider both a simple first-order linear language for
circuits, and a more powerful host language, such that the circuit language is embedded
inside the host language. Our categorical semantics for the host language is standard, and
involves cartesian closed categories and monads. We interpret the circuit language not in
an ordinary category, but in a category that is enriched in the host category. We show
that this structure is also related to linear/non-linear models. As an extended example,
we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use
this model to extend the circuit language with some recursive types.

Introduction
One of the subtle points about quantum computation is the
interaction between classical control flow and quantum opercontrol
ations. One can measure a qubit, destroying the qubit but
producing a classical bit; this classical bit can then be used to
Classical Quantum
decide whether to apply quantum rotations to other qubits.
measurements
This kind of classical control can be neatly described in quantum circuits, for example when one uses the measurement
outcome of a qubit a to conditionally perform a gate X on a qubit b:
b

X

a

•

(0.1)

This can be understood semantically in terms of mixed states, density matrices, and
completely positive maps. However, high level languages have more elaborate data structures than bits: they have higher order functions and mixed variance recursive types, and
1998 ACM Subject Classification: F.3.2 Semantics of Programming Languages.
Key words and phrases: Enriched categories, categorical semantics, linear type theory, quantum circuits,
relative monad, quantum domain theory.

LOGICAL METHODS
IN COMPUTER SCIENCE

DOI:10.2168/LMCS-???

1

c Mathys Rennela and Sam Staton
Creative Commons

2

MATHYS RENNELA AND SAM STATON

associated with these are elaborate control structures such as higher order recursive functions. These are important, paradigmatic ways of structuring programs.
How should these high level features be integrated with quantum computation? One
option is to build a semantic domain that accommodates both quantum computation and
higher order features. This is an aim of some categorical semantics of the quantum lambda
calculus [26, 31] and of prior work of the authors [35, 37]. This is a fascinating direction,
and sheds light, for example, on the structure of the quantum teleportation algorithm
(e.g. [31, Example 6]). However, the general connection between physics and higher-order
quantum functions is yet unclear. Although some recent progress has been made [22], it is
still unclear whether higher-order quantum functions of this kind are useful for quantum
algorithms.
Another approach is to understand a high level quantum programming language as
an ordinary higher-order functional language with extra features for building and running
quantum circuits. In this setting, quantum circuits form a first-order embedded domain
specific language within a conventional higher order language. This fits the current stateof-the-art in interfaces to quantum hardware, and is the basis of the languages Quipper [15]
and LiQUi|i [43]. This is the approach that we study in this paper.
Embedded languages and enriched categories. Our work revolves around a new calculus that we call ‘EWire’ (§1). It is a minor generalization of the QWire language [32, 34].
QWire idealizes some aspects of the architecture of Quipper and LiQUi|i. The idea is that
we deal with a host language separated from an embedded circuit language.
• The circuit language is a first order typed language. The types, called ‘wire types’,
include a type for qubits. The wire type system is linear to accommodate the fact
that qubits cannot be duplicated.
• The host language is a higher order language. The types of the host language do
not include the wire types, there is not a type of qubits, and it is not a linear type
system. However, there is a special host type Circ(W1 , W2 ) associated to any pair
of wire types W1 and W2 , whose inhabitants are the circuits with inputs of type W1
and outputs of type W2 .
Let us describe the circuit language in a nutshell: the very simple circuit (0.1) corresponds
to the instruction below (0.2) in the circuit language. Given two qubits a and b, it measures
the qubit a, stores the result in a bit x which is later used in the application of the classicalcontrolled-X gate and discards the bit x, then outputs the resulting qubit y.
−; a, b : qubit ⊢ C

def

= x ← gate meas a; (x, y) ← gate (bit-control X) (x, b);
() ← gate discard x; output y

: qubit

(0.2)

The interface between the host language and the circuit language is set up in terms of
boxing and unboxing. For example, the instruction
t

def

=

box (a, b) ⇒ C(a, b)

(where C is as in (0.2))

(0.3)

creates a closed term of type Circ(qubit⊗qubit,qubit) in the host language. We recover
the instruction C in the circuit language (0.2) from the boxed expression t in the host
language (0.3) by using the instruction unbox t w for some fresh wire w of type qubit.
Also, it is possible to write a program that composes two circuits C1 and C2 with the
right input/output types, for example:

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

w1

C1

w2

C2

3

w3

This is a program
comp

def

= λ(C1 , C2 ). box w1 ⇒ w2 ← unbox C1 w1 ; w3 ← unbox C2 w2 ; output w3

in the host language, associated with the type
comp : Circ(W1 , W2 ) × Circ(W2 , W3 ) → Circ(W1 , W3 )



(0.4)

where Wi is the type of the wire wi for i ∈ {1, 2, 3}.
Now, recall the idea of an enriched category, which is informally a category such that
the morphisms from A to B form an object of another category. In Section 2, once we
conceptualize types as objects and terms as morphisms, we show that the embedding of
the circuit language in the host language is an instance of enriched category
theory : the circuits (morphisms) between wire types (objects) form a type (object) of the
host language. The host composition term in (0.4) is precisely composition in the sense of
enriched categories. (See §2 for details.)
It is worth mentioning that the idea of denoting a language for circuits within a symmetric monoidal category also appears elsewhere (e.g. [13]).
For a simple version of the model, wire types are understood as finite-dimensional C*algebras, and circuits are completely positive unital maps – the accepted model of quantum
computation. Host types are interpreted as sets, and the type of all circuits is interpreted
simply as the set of all circuits. The category of sets supports higher order functions, which
shows that it is consistent for the host language to have higher order functions.
As with any higher order language, the set-theoretic model is not sufficient to fully
understand the nature of higher order functions. We envisage that other semantic models
(e.g. based on game semantics) will also fit the same framework of enriched categories, so that
our categorical framework provides a sound description of the basic program equivalences
that should hold in all models. These equivalences play the same role that the β and η
equivalences play in the pure lambda calculus. In other words, we are developing a basic
type theory for quantum computation.
Linear/non-linear models. Quantum resources cannot be duplicated or discarded, whereas
classical resources can. This suggests a connection to linear logic [14], as many others have
observed [7,16,25,26,31,38,39]. In fact, enriched category theory is closely related to linear
logic through the following observation (see also [10, 27, 28]).
Lemma 3.2 (paraphrased). The following data are equivalent:
• A symmetric monoidal closed category enriched in a cartesian closed category, with
copowers.
• A‘linear/non-linear’ (LNL) model in the sense of Benton [4]: a symmetric monoidal
adjunction between a cartesian closed category and a symmetric monoidal closed
category.
Thus, from the semantic perspective, enriched category theory is a way to study fragments and variations of linear logic. We show that every LNL model, with some minor
extra structure, induces an EWire model (see Proposition 3.4). We call these structures
LNL-EWire models.

4

MATHYS RENNELA AND SAM STATON

So LNL-EWire extends EWire with some additional connectives. However, although
these additional connectives have an established type theoretic syntax, their meaning from
the perspective of quantum physics is less clear at present. For example, LNL assumes a
first class linear function space, but categories of completely positive unital maps (or CPTP
maps) are typically not monoidal closed. Nonetheless, there is a semantic way to understand
their relevance, through the following theorem, which is proved using a variation on Day’s
construction [8], following other recent work [26, 30, 38].
Theorem 3.5 (paraphrased). Every EWire model (with a locally presentable base) embeds
in an LNL-EWire model.
Recursive types and recursive terms. Within our semantic model based on enriched
categories, we can freely accommodate various additional features in the host language,
while keeping the circuit language the same. For example, we could add recursion to the
host language, to model the idea of repeatedly trying quantum experiments, or recursive
types, to model arbitrary data types. This can be shown to be consistent by modifying the
simple model so that host types are interpreted as directed complete partial orders (dcpo’s).
Many quantum algorithms are actually parameterized in the number of qubits that they
operate on. For example, the Quantum Fourier Transform (QFT) has a uniform definition
1
and Rn is the Z rotation
for any number of qubits, where H is the Hadamard gate √12 11 −1


1
0
gate 0 e2πi/2n .
•

|x1 i

..
.
|xn i

•

···

|x2 i
|x3 i

···

···

QFT
Rn

•
R2

R3

···

H

|yn i
|yn−1 i
|yn−2 i
..
.
|y1 i

|

{z
}
rotations
We formalize this by extending the circuit language with a wire type QList of qubit-lists
for which the following equivalence of types holds:
QList ∼
= (qubit ⊗ QList) ⊕ 1
so that we can define a function
fourier : Circ(QList, QList)
We part away from the canonical intuition of circuits by considering them as first-order
and linear (in the linear logic sense of the term) instructions. In practice, it will be useful
for a circuit layout engine to know the number of qubits in the lists, suggesting a dependent
type such as
fourier : (n : Nat) → Circ(QList(n), QList(n))
but we leave these kinds of elaboration of the type system to future work.
The categorical essence of recursive data types is algebraic compactness. In short, one
says that a category C is algebraically compact (for a specific class of endofunctors) when
every endofunctor F : C → C has a canonical fixpoint, which is the initial F-algebra [3]. In

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

5

earlier work [35], the first author has shown that the category of W*-algebras is algebraically
compact and enriched in dcpo’s, and so this is a natural candidate for a semantics of the
language. In brief: circuit types are interpreted as W*-algebras, and circuits are interpreted
as completely positive sub-unital maps; host types are interpreted as dcpo’s; in particular
the collection of circuits Circ(W, W ′ ) is interpreted as the dcpo of completely positive subunital maps, with the Löwner order. In this way, we provide a basic model for a quantum
type theory with recursive types. We conclude with what is, to our knowledge, the first
categorical semantics of a language that can accommodate QFT in this parameterized way.
1. Functional programming and quantum circuits
We introduce a new calculus called EWire as a basis for analysing the basic ideas of embedding a circuit language inside a host functional programming language. EWire (for
‘embedded wire language’) is based on QWire [32] (‘quantum wire language’), and we make
the connection precise in Section 1.3. We discuss extensions of EWire in Section 4.
We assume two classes of basic wire types.
• Classical wire types, ranged over by a, b, . . . . The wire types exist in both the
circuit language and the host language. For example, the type of classical bits, or
Booleans.
• Circuit-only wire types, ranged over by α, β, . . . . These wire types only exist in the
circuit language. For example, the type of qubits.
From these basic types we build all wire types:
W, W ′ ::= I | W ⊗ W ′ | a | b | α | β . . .
We isolate the classical wire types, which are the types not using any circuit-only basic
types:
V, V ′ ::= I | V ⊗ V ′ | a | b . . .
We also assume a collection G of basic gates, each assigned an input and an output wire
type. We write G(Win , Wout ) for the collection of gates of input type Win and output type
Wout .
In addition to the embedded circuit language, we consider a host language. This is like
Moggi’s monadic metalanguage [29] but with special types for the classical wire types a, b
and a type Circ(W, W ′ ) of circuits for any wire types W and W ′ . So the host types are
A, B ::= A × B | 1 | A → B | T (A) | Circ(W, W ′ ) | a | b
The monad T is primarily to allow probabilistic computations, although one might also
add other side effects to the host language. Notice that every classical wire type V can be
understood as a first order host type |V |, according to the simple translation, called lifting:
def

V ⊗ V ′ = |V | × V ′

def

|I| = 1

def

|a| = a

6

MATHYS RENNELA AND SAM STATON

1.1. Circuit typing and host typing. A well-formed circuit judgement Γ; Ω ⊢ C : W
describes a circuit with input context
Ω = (w1 : W1 · · · wn : Wn )

(for n ∈ N)

and output wire type W under the context of host language variables
Γ = (x1 : A1 · · · xm : Am )

(for m ∈ N)

Wires are organised in patterns given by the grammar
p ::= w | () | (p, p)
associated to the following set of rules:
−
−

Ω1 =⇒ p1 : W1

Ω2 =⇒ p2 : W2

· =⇒ () : 1
Ω1 , Ω2 =⇒ (p1 , p2 ) : W1 ⊗ W2
w : W =⇒ w : W
We call concrete every circuit whose input wires are either bits or qubits, rather than
tuples, i.e. a concrete circuit is a circuit associated to a well-formed circuit judgement
⊙; ∆ ⊢ C : W for which the input context is taken in the grammar
∆ ::= · | ∆, w : bit | ∆, w : qubit
Linear type theory for circuits. The first five term formation rules are fairly standard
for a linear type theory. These are the constructions for sequencing circuits, one after
another, and ending by outputting the wires, and for splitting a tensor-product type into
its constituents. The fifth rule includes the basic gates in the circuit language.
Γ; Ω1 ⊢ C1 : W1
Ω =⇒ p : W1
Γ; Ω, Ω2 ⊢ C2 : W2
Ω =⇒ p : W
Γ; Ω ⊢ output p : W

Γ; Ω1 , Ω2 ⊢ p ← C1 ; C2 : W2
′

Ω =⇒ p : 1 Γ; Ω ⊢ C : W

Ω =⇒ p : W1 ⊗ W2

Γ; w1 : W1 , w2 : W2 , Ω′ ⊢ C : W

Γ; Ω, Ω′ ⊢ () ← p; C : W
Γ; Ω, Ω′ ⊢ (w1 , w2 ) ← p; C : W
Ω1 =⇒ p1 : W1
Ω2 =⇒ p2 : W2
Γ; Ω2 , Ω ⊢ C : W
g ∈ G(W1 , W2 )
Γ; Ω1 , Ω ⊢ p2 ← gate g p1 ; C : W
For example, coin flipping is given by the following circuit:
def

flip = a ← gate init0 (); a′ ← gate H a; b ← gate meas a′ ; output b
Interaction between the circuits and the host. A well-formed host judgement Γ ⊢ t : A
describes a host-language program of type A in the context of host language variables Γ.
The next set of typing rules describe the interaction between the host language and the
circuit language. The host can run a circuit and get the result. Since this may have side
effects, for example probabilistic behaviour, it returns a monadic type.
Γ; · ⊢ C : W
W classical
Γ ⊢ run C : T (|W |)
The next two rules concern boxing a circuit as data in the host language, and then
unboxing the data to form a circuit fragment in the circuit language. Notice that unboxing requires a pure program of type Circ(W1 , W2 ), rather than effectful program of type

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

7

T (Circ(W1 , W2 )). For example, you cannot unbox a probabilistic combination of circuits.
The monadic notation clarifies this point.
Ω =⇒ p : W1
Γ; Ω ⊢ C : W2
Γ ⊢ t : Circ(W1 , W2 ) Ω =⇒ p : W1
Γ ⊢ box (p : W1 ) ⇒ C : Circ(W1 , W2 )
Γ; Ω ⊢ unbox t p : W2
Finally we consider dynamic lifting, which, informally, allows us to send classical data to
and from the host program while the quantum circuit is running.
Γ ⊢ t : |W |
Ω =⇒ p : |W |
Γ, x : W ; Ω′ ⊢ C : W ′
W classical
W classical
Γ; − ⊢ init t : W
Γ; Ω, Ω′ ⊢ x ⇐ lift p; C : W ′
These rules are in addition to the standard typing rules for the host language, following
Moggi [29].
Additional typing rules for the host language. Recall that the types of the host language are
A, B ::= A × B | 1 | A → B | T (A) | Circ(W, W ′ ) | a | b
The standard typing rules of the monadic metalanguage are the rules of the simply-typed
λ-calculus
Γ, x : A ⊢ t : B
Γ⊢t:A→B
Γ⊢u:A
(x : A) ∈ Γ
Γ ⊢ (λxA .t) : A → B
Γ ⊢ t(u) : B
Γ⊢x:A
Terms of product types are formed following four typing rules
Γ⊢t:A×B
Γ⊢t:A×B
Γ⊢t:A Γ⊢u:B
−
Γ ⊢ (t, u) : A × B
Γ ⊢ π1 (t) : A
Γ ⊢ π2 (t) : B
Γ ⊢ unit : 1
to which we need to add the typing rules for the monad [29], associated respectively to the
unit and the strong Kleisli composition:
Γ⊢t:B

Γ ⊢ t : T (B)

Γ, x : B ⊢ u : T (C)

Γ ⊢ return(t) : T (B)
Γ ⊢ let x = t in u : T (C)
This is in addition to the typing rules for the interaction between the host language and
the circuit language.
It should be noted that since a pair of probabilistic terms Γ ⊢ t : T (A) and Γ ⊢ t′ : T (B)
isn’t usually the same thing as a term Γ ⊢ t : T (A) × T (B) (when T is a probability monad),
it is interesting from a programming language point of view to be able to reference variables
of computation type. This makes the linearity of our type system particularly relevant in
the study of probabilistic programming.
1.2. Operational semantics of EWire. Let us introduce a reduction relation on circuits,
based on [32], which reduces a circuit with no free host variables to a normal circuit. The
reduction works by rearranging patterns and resolving unboxed boxes. But first, let us start
with the (partial) destruction of patterns.
p ← output p′ ; C =⇒ C[p 7→ p′ ]
() ← (); C =⇒ C

unbox (box w ⇒ C) p =⇒ C[w 7→ p]

w1
(w1 , w2 ) ← (p1 , p2 ); C =⇒ C[ w
2

7→p1
7→p2 ]

The reduction system → on terms is defined in two parts: the host reduction rule →H is the

8

MATHYS RENNELA AND SAM STATON

operational semantics of the host language, while the reduction rule →b is the operational
semantics of boxed circuits (we refer to [32, Sec. 4] for its description), in such a way that
def

→ = →H ∪ →b
The host reduction rule →H must contain the following additional reduction rules,
which are simply the standard reduction rules of the monadic metalanguage that we’re
adding to the host language.
t →H t ′
λx.t →H λx.t′

(λx.t)t′ →H t[x 7→ t′ ]
t →H t ′

π1 (t1 , t2 ) →H t1

π2 (t1 , t2 ) →H t2

return(t) →H return(t′ )

let x = t in u →H let x = t in u[x 7→ t]

let x = (let t = y in u) in v →H let y = t in let x = u in v
with the grammar of values v given by
v ::= x | unit | (v1 , v2 ) | λxA .v | return(v)
We can now define the following reduction rules for boxing and unboxing instructions.
C =⇒ C ′

t → t′

box (w : W ) ⇒ C →b box (w : W ) ⇒ C ′

unbox t p ⇒ unbox t′ p

Then, we add the structural reduction rule

C =⇒ C ′
E[C] =⇒ E[C ′ ]

with

E ::= w ← ; C | w ← gate g p;  | () ← p;  | (w1 , w2 ) ← p; 

(1.1)

Therefore, normal circuits are given by the following grammar:
N ::= output p | w ← gate g p; N | x ⇐ lift p; N | () ← w; N | (w1 , w2 ) ← w; N
Finally, commuting conversion rules allows to reduce even more instructions to normal
forms.
w ← (p2 ← gate g p1 ; N ); C =⇒ p2 ← gate g p1 ; w ← N ; C

w ← (x ⇐ lift p; C ′ ); C =⇒ x ⇐ lift p; w ← C ′ ; C

w ← (() ← w′ ; N ); C =⇒ () ← w′ ; w ← N ; C

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

9

w ← ((w1 , w2 ) ← w′ ; N ); C =⇒ (w1 , w2 ) ← w′ ; w ← N ; C
We refer the interested reader to [32, Appendix A] for a discussion of type safety and
existence of normal forms in QWire.
1.3. QWire. The language QWire of Paykin, Rand and Zdancewic [32] is an instance of
EWire where:
• there is one classical wire type, bit, and one circuit-only wire type, qubit.
• there are basic gates meas ∈ G(qubit, bit) and new ∈ G(bit, qubit).
A subtle difference between EWire and QWire is that in QWire one can directly run a circuit
of type qubit, and it will produce a bit, automatically measuring the qubit that results
from the circuit. To run a circuit of type qubit in EWire, one must append an explicit
measurement at the end of the circuit. These explicit measurements can be appended
automatically, to give a translation from QWire proper to this instantiation of EWire. We
now summarize how this is done. We first define a translation (−) from all wire types to
classical wire types:
def

W ⊗ W′ = W ⊗ W

′

def

I =I

def

def

bit = bit qubit = bit

Then, from an arbitrary wire type W , we can extract a host type W .
From the basic gates meas and new we can define circuits
measW : Circ(W, W )

and

newW : Circ(W , W )

for all wires W . These are defined by induction on W . For example,
def

measI = id

def

measbit = id

def

measqubit = box p ⇒ p′ ← gate meas p; output p′
def

measW ⊗W ′ = box (w, w′ ) ⇒ x ← unbox measW w; x′ ← unbox measW ′ w′ ;
output (x, x′ )

and newW is defined using new ∈ G(bit, qubit) similarly. Then we define the following
derived syntax, so that run and lift can be used at all wire types, not just the classical ones:
def

qwire-run(C) = run(x ← C; unbox meas x)
def

(x ⇐ qwire-lift p ; C) = y ⇐ lift p ; x ← unbox new y ; C
2. Categorical models of EWire
We introduce the categorical semantics of EWire. Our semantic models are based around
enriched category theory [21]. The relevance of Set-enriched copowers to quantum algorithms has previously been suggested by Jacobs [17]. On the other hand, copowers and
enrichment play a key role in the non-quantum enriched effect calculus [10, 28] and other
areas [24, 27, 33, 41]. Nonetheless, our connection with the EWire syntax appears to be
novel.

10

MATHYS RENNELA AND SAM STATON

2.1. Preliminaries. Enriched categories. Let H be a cartesian closed category. Recall
that a category C enriched in H is given by a collection of objects and, for each pair
of objects c and d, an object C(c, d) in H, together with morphisms for composition
C(c, d) × C(d, e) → C(c, e) and identities 1 → C(c, c), subject to associativity and identity
laws. Much of category theory can be reformulated in the enriched setting [21].
Computational effects. Embedding the circuit language requires the use of some computational effects in the host language. When the
 circuit language involves quantum measurement, then the closed host term ⊢ run flip : T (bit) is a coin toss, and so the semantics of
the host language must accommodate probabilistic features.
Following Moggi, we model this by considering a cartesian closed category H with an
enriched monad on it. Recall that an enriched monad is given by an endofunctor T on H
together with a unit morphism η : X → T (X) for each X in H, and a bind morphism
H(X, T (Y )) → H(T (X), T (Y ))
for objects X and Y , subject to the monad laws [29].
The idea is that deterministic, pure programs in the host language are interpreted as
morphisms in H. Probabilistic, effectful programs in the host language are interpreted as
Kleisli morphisms, i.e. morphisms X → T (Y ).
Relative monads. The monads of Moggi are a slightly higher order notion. In a truly first
order language, this type arguably should not exist. In particular, there is no wire type T (A)
of all quantum computations. To resolve this mismatch, authors have proposed alternatives
such as relative monads [2] and monads with arities [5].
An ordinary relative adjunction is given by three functors J : B → D, L : B → C and
R : C → D such that there is a natural bijection
C(L(b), c) ∼
(2.1)
= D(J(b), R(c))
We write L J ⊣ R and call relative monad the functor RL : B → D.
Enriched relative adjunctions and enriched relative monads are defined in the obvious
way, by requiring J, L and R to be enriched functors and replacing the natural bijection (2.1)
with a antural isomorphism. In an enriched relative monad T = RL, the bind operation is
a morphism of type
D(J(X), T (Y )) → D(T (X), T (Y ))
Copowers and weighted limits. In enriched category theory it is appropriate to consider
weighted colimits and limits, which are a generalization of the ordinary notions. As a first
step, we consider copowers. A copower is a generalization of an n-fold coproduct. Let n be
a natural number, and let A be an object of a category C with sums, the copower n ⊙ A is
the n fold coproduct A + · · · + A. This has the universal property that to give a morphism
n ⊙ A → B is to give a family of n morphisms A → B. In general, if C is a category
enriched in a category H, and A is an object of C and h an object of H, then the copower
is an object h ⊙ A together with a family of isomorphisms
C(h ⊙ A, B) ∼
= H(h, C(A, B))
natural in B.
Weighted colimits combine the notions of copowers and of ordinary conical colimits. If
J is a H-enriched category, then we may try to take a colimit of a diagram D : J → C
weighted by a functor W : Jop → H. Here C is an H-enriched category and D and W

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

11

are H-functors. A cylinder for (W, D) is given by an object X and a H-natural family of
morphisms W (j) → C(D(j), X); the weighted limit, colimW
j Dj if it exists, is the universal
cylinder.
2.2. EWire models. Let us define a sufficient set of properties which ensure that a pair of
categories corresponds to a categorical model in which one can interpret EWire, in order to
reason about circuits and identify their denotational meaning. We assume that the circuit
language is parametrized by a fixed collection of gates, noted G.
Definition 2.1. A categorical model of EWire (C, H, H0 , T ) is given by the following data:
(1) A cartesian closed category H with a strong monad T on H. This is needed to
interpret the host language.
(2) A small full subcategory j : H0 ⊆ H. The idea is that the objects of H0 interpret
the first order host types, equivalently, the classical wire types: the types that exist
in both the host language and the circuit language.
(3) An H-enriched symmetric monoidal category (C, ⊗, I). This allows us to interpret
the circuit language, and the H-enrichment allows us to understand the host types
Circ(W, W ′ ).
(4) The category C has copowers by the objects of H0 . The copower induces a functor
J : H0 → C defined by J(h) = h ⊙ I. Then, we have a natural isomorphism
∼ H(j(h), C(I, C))
C(J(h), C) = C(h ⊙ I, C) =
and therefore a j-relative adjunction J j ⊣ C(I, −) between circuits and (host)
terms. This functor J : H0 → C interprets the translation between first order host
types and classical wire types.
(5) For each object A of C, the functor A ⊗ − : C → C preserves copowers. This makes
the functor J symmetric monoidal, and makes the relative adjunction an enriched
relative adjunction.
(6) There is an enriched relative monad morphism
runh : C(I, J(h)) → T (j(h))
where the enriched relative monad C(I, J(−)) : H0 → H is induced by the enriched
j-relative adjunction J j ⊣ C(I, −). This is the interpretation of running a quantum
circuit, producing some classical probabilistic outcome.
If the category C has a given object [[α]] for each basic quantum wire type α, and H0
has a given object [[a]] for each basic classical wire type a, then we can interpret all wire
types W as objects of C:
def

[[1]] = I

def

[[a]] = J([[a]])

def

[[W ⊗ W ′ ]] = [[W ]] ⊗ [[W ′ ]].

If the category C also has a given morphism [[g]] : [[W1 ]] → [[W2 ]] for every gate g ∈ G(W1 , W2 ),
then we can interpret the circuit langauge inside C.
In light of those axioms, and to every categorical model of EWire, we associate the
following denotational semantics.
First, we define as promised the denotation of the host type Circ(W, W ′ ) by
def

[[Circ(W, W ′ )]] = C(W, W ′ ) ∈ Obj(H)

12

MATHYS RENNELA AND SAM STATON

The semantics of the other host types is given as follows:
def

def

[[1]] = 1 [[A × A′ ]] = [[A]] × [[A′ ]]

def

def

[[A → A′ ]] = ([[A]] → [[A′ ]]) [[T (A)]] = T ([[A]]).

Ordered context of wires Ω have the following semantics:
[[h·i]] = I

[[w : W ]] = [[W ]]

[[Ω, Ω′ ]] = [[Ω]] ⊗ [[Ω′ ]]

A circuit judgement Γ; Ω ⊢ t : W is denoted by
[[Γ; Ω ⊢ t : W ]] ∈ H([[Γ]], C([[Ω]], [[W ]]))
relying on the assumption that the category H is a model of the host language. A host
type Circ(W, W ′ ) is interpreted as the hom-object C([[W ]], [[W ′ ]]), in the category H. In
this setting, denotations of boxing and unboxing instructions are trivial. Indeed, notice
that whenever Ω =⇒ p : W1 holds, we have [[Ω]] ∼
= [[W1 ]], and we put
[[Γ ⊢ box (p : W1 ) ⇒ C : Circ(W1 , W2 )]] = [[Γ; Ω ⊢ C : W2 ]]
[[Γ; Ω ⊢ unbox t p : W2 ]] = [[Γ ⊢ t : Circ(W1 , W2 )]]
The denotation of output p : W is the identity on [[W ]]. Moreover, instructions
Γ; Ω, Ω′ ⊢ () ← p; C : W and Γ; Ω′ ⊢ C : W (resp. Γ; Ω, Ω′ ⊢ (w1 , w2 ) ← p; C : W
and Γ; w1 : W1 , w2 : W2 , Ω′ ⊢ C : W ) have the same denotations whenever Ω =⇒ p : 1
holds (resp. Ω =⇒ p : W1 ⊗ W2 holds).
The lift construction is interpreted by the copower. In detail, for every object h of H,
and every object h′ of H0 , we consider the isomorphism
lifth : H(h × h′ , C(X, Y )) ∼
= H(h, C(h′ ⊙ X, Y ))
= H(h, H(h′ , C(X, Y ))) ∼
Since we’re enforcing explicit measurement here, the denotation of the operation run
for a circuit C whose output wire type is the type W is given by Def. 2.1(6).
The denotations of the remaining instructions are given as follows.
[[Γ; Ω1 , Ω ⊢ p2 ← gate g p1 ; C : W ]] = [[Γ; Ω2 , Ω ⊢ C : W ]] ◦ ([[g]] ⊗ id)
[[Γ; Ω1 , Ω2 ⊢ p ← C; C ′ : W ′ ]] = [[Γ; Ω, Ω2 ⊢ C ′ : W ′ ]] ◦ ([[Ω1 ⊢ C : W ]] ⊗ id)
Consider the operational semantics given in Section 1.2. Assuming that H is a sound
and strongly normalizing categorical model of the host language, one obtains the following
theorem by induction on typing judgements.
Theorem 2.2 (Soundness). Assume that the reduction system → of the host language is
normalizing. For every denotational semantics induced by a categorical model of EWire, if
the circuit judgement ·; Ω ⊢ C : W holds and the concrete circuit C reduces to a (concrete)
circuit C ′ , then
[[·; Ω ⊢ C : W ]] = [[·; Ω ⊢ C ′ : W ]]
Proof. In what follows, we exploit the observation that, by construction, the denotational
semantics of concrete circuits does not depend on the content of patterns [32, Lemma 10],
i.e. for every concrete circuit
[[·; Ω ⊢ C[w 7→ p] : W ]] = [[·; Ω ⊢ C : W ]]
when ·; Ω ⊢ C : W and Ω =⇒ p : W hold and w : W is an input wire.
Therefore, when C reduces to C ′ by one of the commuting conversion rules presented in
Section 1.2, which only affect patterns, the concrete circuit C ′ can be seen as a reorganization
of the patterns of the circuit C, and thus [[C ′ ]] = [[C]].
For the other reduction rules, we proceed by induction on typing judgements.

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

13

Consider the judgement ·; Ω ⊢ p ← output p′ ; C : W ′ , for which Ω =⇒ p : W holds
and the circuit p ← output p′ ; C reduces in one step to C[p 7→ p′ ]. We have by construction
[[·; Ω ⊢ p ← output p′ ; C]] = [[·; Ω ⊢ output p′ ]] ◦ ([[·; Ω ⊢ C : W ′ ]] ⊗ id) = [[·; Ω ⊢ C[p 7→ p′ ]]].
The judgements ·; Ω ⊢ () ← (); C : W and ·; Ω, · ⊢ C : W have the same denotation, i.e.
[[·; Ω ⊢ () ← (); C : W ]] = [[·; Ω, · ⊢ C : W ]]
The judgements ·; Ω ⊢ (w1 , w2 ) ← (p1 , p2 ); C : W and ·; Ω, w1 : W1 , w2 : W2 ⊢ C : W
have the same denotation, i.e.
1
[[·; Ω ⊢ (w1 , w2 ) ← (p1 , p2 ); C : W ]] = [[·; Ω, w1 : W1 , w2 : W2 ⊢ C[ w
w2

7→p1
7→p2 ]

: W ]]

Consider the judgement ·; Ω ⊢ unbox t p : W2 such that · ⊢ t : Circ(W1 , W2 ) and
Ω =⇒ p : W1 hold, where the host term t reduces in finitely many steps to a host term
t′ . Since the host reduction system is assumed to be normalizing, the host terms t and t′
both reduce in finitely many steps to a normal form box p′ ⇒ N , and therefore C and
C ′ reduce in finitely many steps to the circuit unbox (box p′ ⇒ N ) p (associated to the
input context Ω′ such that the relation Ω′ =⇒ p′ holds), which itself reduces to the circuit
N [p′ 7→ p]. Therefore, the following equality holds:
[[·; Ω ⊢ unbox t p : W2 ]] = [[·; Ω′ ⊢ N : W2 ]] = [[·; Ω ⊢ unbox t p : W2 ]]
Consider a circuit judgement ·; Ω ⊢ C : W such that C reduces to a circuit C ′ . Then,
every circuit of the form E[C] (described in the grammar 1.1) reduces in finitely many steps
to a circuit of the form E[C ′ ] through the structural reduction rule.
By induction hypothesis, from the fact that C reduces to C ′ , we have the equality
[[·; Ω ⊢ C]] = [[·; Ω ⊢ C ′ ]]. As a pair of circuits in the grammar 1.1, the pair hE[C], E[C ′ ]i is
of one of the four following forms:
hw ← C; C ′′ , w ← C ′ ; C ′′ i

hw ← gate g p; C, w ← gate g p; C ′ i

h() ← p; C, () ← p; C ′ i
h(w1 , w2 ) ← p; C, (w1 , w2 ) ← p; C ′ i
For all four different types of pair hE[C], E[C ′ ]i, the following implications establish that
[[·; Ω ⊢ E[C]]] = [[·; Ω ⊢ E[C ′ ]]], from the equality [[·; Ω ⊢ C]] = [[·; Ω ⊢ C ′ ]]:
[[·; Ω1 , Ω2 ⊢ C ′′ ]] ◦ ([[·; Ω ⊢ C]] ⊗ id) = [[·; Ω1 , Ω2 ⊢ C ′′ ]] ◦ ([[·; Ω ⊢ C ′ ]] ⊗ id)
[[·; Ω ⊢ C]] ◦ ([[g]] ⊗ id) = [[·; Ω ⊢ C ′ ]] ◦ ([[g]] ⊗ id)
[[Γ; Ω′ , Ω ⊢ () ← p; C]] = [[·; Ω ⊢ C]] = [[·; Ω ⊢ C ′ ]] = [[Γ; Ω′ , Ω ⊢ () ← p; C ′ ]]
′
[[Γ; Ω , Ω ⊢ (w1 , w2 ) ← p; C]] = [[·; Ω ⊢ C]] = [[·; Ω ⊢ C ′ ]] = [[Γ; Ω′ , Ω ⊢ (w1 , w2 ) ← p; C ′ ]]

14

MATHYS RENNELA AND SAM STATON

Our view on the semantics of quantum computing relies on the theory of C*-algebras.
The positive elements of C*-algebras correspond to observables in quantum theory, and
we understand quantum computations as linear maps that preserve positive elements, in
other words, ‘observable transformers’. Circuits (·; (x : W ) ⊢ C : W ′ ) will be interpreted
as completely positive unital maps [[W ′ ]] → [[W ]]. The reverse direction is in common with
predicate transformer semantics for conventional programming.
There are two crucial constructions of C*-algebras: matrix algebras and direct sums.
Matrix algebras provide a crucial example of C*-algebras. For example, the algebra M2 of
2 × 2 complex matrices represents the type of qubits. The direct sum of two C*-algebras,
A ⊕ B, is the set of pairs with componentwise algebra structure. For instance, C ⊕ C
represents the type of classical bits. Every finite-dimensional C*-algebra is a direct sum of
matrix algebras.
The tensor product ⊗ of finite dimensional C*-algebras is uniquely determined by two
properties: (i) that Mk ⊗ Ml ∼
= Mk×l , and (ii) that A ⊗ (−) and (−) ⊗ B preserve direct
sums. In particular Mk ⊗ A is isomorphic to the C*-algebra Mk (A) of (k × k)-matrices
valued in A.
We do not focus here on linear maps that preserve all of the C*-algebra structure, but
rather on completely positive maps. An element x ∈ A is positive if it can be written in
the form x = y ∗ y for y ∈ A. These elements correspond to quantum observables. A map
f : A → B, linear between the underlying vector spaces, is positive if it preserves positive
elements. A linear map is unital if it preserves the multiplicative unit. A linear map f is
completely positive if the map
(Mk ⊗ f ) : Mk ⊗ A → Mk ⊗ B
is positive for every k. This enables us to define a functor C ⊗(−) for every finite dimensional
C*-algebra C. Thus finite dimensional C*-algebras and completely positive unital linear
maps form a symmetric monoidal category. There are completely positive unital maps
corresponding to initializing quantum data, performing unitary rotations, and measurement,
and in fact all completely positive unital maps arise in this way (e.g. [40, 42]).
Proposition 2.3. The quadruplet (FdC∗ -Algop
CPU , Set, N, D) is a model of EWire, formed
by the opposite category of the category FdC∗ -AlgCPU of finite-dimensional C*-algebras
and completely positive unital maps, the cartesian closed category Set of sets and functions,
the skeleton N of the category of finite sets and functions (which considers natural numbers
as its objects), and the probability distribution monad D over Set. In fact it is a model of
def

def

QWire, with [[qubit]] = M2 and [[bit]] = C ⊕ C.
Proof. The category Set of sets and functions is the canonical example of cartesian closed
category, and the distribution monad D : Set → Set is a strong monad.
The category FdC∗ -Algop
CPU of the opposite category of finite-dimensional C*-algebras
and completely positive unital maps has a monoidal structure given by the tensor product
of C*-algebras, finite sums given by direct sums and the C*-algebra C of complex numbers
is the unit I.
The copower n ⊙ A of a natural number n ∈ N and a C*-algebra A is the C*-algebra
n ⊙ A, defined as the n-fold direct sum A ⊕ · · · ⊕ A like in [17]. We observe that the copower
distributes over the coproduct, i.e.
n ⊙ (A ⊕ B) = n ⊙ A ⊕ n ⊙ B

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

15

and that composition is multiplication, i.e.
n ⊙ (m ⊙ A) = nm ⊙ B
The copower n ⊙ C is the C*-algebra Cn . Copowers are preserved by endofunctors
A ⊗ −.
A ⊗ (n ⊙ B) = A ⊗ B ⊕ · · · ⊕ A ⊗ B = n ⊙ (A ⊗ B)
We still need to verify that we have a relative adjunction. Observing that
FdC∗ -Alg
(A, Cn ) ∼
(A, C) × · · · × FdC∗ -Alg
(A, C)
= FdC∗ -Alg
CPU

CPU

CPU

one deduces that
FdC∗ -AlgCPU (A, Cn ) ∼
= Set(n, FdC∗ -AlgCPU (A, C))
and therefore

op
n
∗
∼
FdC∗ -Algop
CPU (C , A) = Set(n, FdC -AlgCPU (C, A))
Then, the symmetric monoidal functor J : N → FdC∗ -Algop
CPU associates every natural
number n ∈ N to the C*-algebra Cn . The morphisms runn are given by the isomorphism
FdC∗ -Algop (C, Cn ) = FdC∗ -Alg
(Cn , C) ∼
[12, Lemma 4.1]
= D(n)

between states

CPU
on Cn and

CPU

the n-simplex

D(n) := {x ∈ [0, 1]n |

X

xi = 1}

i

The semantics of types and gates is rather standard. Probabilities are complex numbers
C and a (classical) bit is therefore an element of the C*-algebra C ⊕ C. Moreover, n-qubit
systems are modelled in the C*-algebra M2n . In other words,
1=C

bit = C ⊕ C

qubit = M2

meas : C ⊕ C → M2 : (a, b) 7→ a0 0b
and so on.

u = u† − u (for every unitary u ∈ U )

new : M2 → C ⊕ C : ac db 7→ (a, b)

Completeness. One key element to a proof of completeness is to organize terms in equivalence
classes. The syntactic category (or category of contexts) of the type theory of EWire is the
category whose objects are contexts Γ and morphisms σ : Γ → ∆ are substitutions (of
variables). A categorical model is said to be complete for a type theory if every morphism
f : [[Γ]] → [[∆]] of the categorical model is the denotation [[σ]] of a substitution σ in the
syntactic category.
From the β/η-theory, we extract the following equivalences:
(w1 , w2 ) ← (p1 , p2 ); C ≡ w1 ← output p1 ; w2 ← output p2 ; C
() ← (); C ≡ C
unbox (box p ⇒ C) p′ ≡ p ← output p′ ; C
This observation opens the door to a brand new problem, recently discussed in the literature
[32, 42] but which goes beyond the scope of the present work: finding an equational theory
for quantum circuits.

16

MATHYS RENNELA AND SAM STATON

2.3. A step towards quantum domain theory. Recall that a W*-algebra is an unital
C*-algebra A whose unit interval is a dcpo when equipped with the Löwner order (x ≤
y ⇐⇒ y − x positive), with sufficiently many normal states, i.e. normal completely
positive unital maps A → C [35, 36].
We write W∗ -AlgCPSU for the category of W*-algebras and completely positive subunital maps, which is known for being Dcpo⊥ -enriched (see [35], or [6] for a full proof of
this statement for completely positive subunital maps), where Dcpo⊥ is the category of
pointed dcpos and Scott-continuous maps which is known to be cartesian closed [1]. It is
worth noting, especially in the context of Section 5, that the category Dcpo⊥! of pointed
dcpos and strict Scott-continuous maps, is not cartesian closed but it is monoidal closed
when equipped with the smash product [1], i.e. the quotient of the cartesian product X × Y
(of two pointed dcpos X and Y ) by the relation generated by the relation ∼ such that
(x, ⊥) ∼ (⊥, y) ∼ (⊥, ⊥)
for x ∈ X and y ∈ Y .
Then, the opposite category W∗ -Algop
CPSU is part of a categorical model of QWire,
when one considers the restricted version of the monad of sub-valuations (also known as
‘sub-probabilistic powerdomain’)
def

V = dcGEMod([0, 1](−) , [0, 1])
on Dcpo⊥ (see e.g. [19, Section 5.6]), where the category dcGEMod is the category of
directed-complete generalized effect modules and Scott-continuous effect module homomorphisms, also introduced as a category of quantum predicates in [36, 37].
Proposition 2.4. The quadruplet (W∗ -Algop
CPSU , Dcpo⊥ , N, V ) is a categorical model of
QWire.
Proof. First, it has been established that the category W∗ -Algop
CPSU is symmetric monoidal
when equipped with the spatial tensor product [23] and it is a well-known fact that the
category Dcpo⊥ of pointed dcpos and Scott-continuous maps is cartesian closed [1]. The
objects of the category N, i.e. natural numbers are flat dcpos, i.e. pointed dcpos with a
bottom element ⊥ such that
x ≤ y ⇐⇒ (x = y ∨ x =⊥)
Much like in [18, Section 5.6], we introduce the restricted version of the monad of
subvaluations V = dcGEMod([0, 1](−) , [0, 1]) on Dcpo⊥ , where the category dcGEMod
is the category of directed-complete generalized effect modules and Scott-continuous effect
module homomorphisms, also introduced as a category of quantum predicates in [36, 37].
Now, recall that a strong monad over a monoidal closed category K is the same thing as
a K-enriched monad. The monad V is enriched over Dcpo⊥ and therefore a strong monad
since the category Dcpo⊥! is cartesian (monoidal) closed.
Since there is a full and faithful functor which takes every W*-algebra A to its directedcomplete generalized effect module [0, 1]A of predicates [37], there is an equivalence
V (n) = dcGEMod([0, 1]n , [0, 1]) ∼
(Cn , C) for every n ∈ N
= W∗ -Alg
CPSU

op
and therefore an equivalence V (n) ∼
= W∗ -AlgCPSU (C, Cn ) for every n ∈ N.
Building up on the constructions of Proposition 2.3, we deduce that

(W∗ -Algop
CPSU , Dcpo⊥ , N, V )

is a categorical model of QWire.

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

17

Section 4 is devoted to an investigation of the extra syntax supported by the category

W∗ -Algop
CPSU .

3. Relation to linear-non-linear models
Recent work by Selinger and collaborators [26, 38, 39] has suggested that a good setting
for quantum programming might be the linear/non-linear (LNL) models of linear logic in
the style of Benton [4]. This is, at first glance, a different approach to the QWire/EWire
approach, for the following reason. In QWire/EWire the type of circuits Circ(W, W ′ ) is a
type in the host language, and is not itself a wire type. By contrast, with LNL models, the
linear function space (W ⊸ W ′ ) is itself an object of the category containing the linear
types.
Rios and Selinger [38] gave a particular construction of an LNL model for quantum
programming. Mislove et al. [25] have also been working on some related constructions. In
this section we propose a variation on that construction that works for a broad class of
EWire models. In this way we bring the two lines of research closer together.
Definition 3.1 ( [4]). A linear/non-linear (LNL) model is given by the following data:
(1) a symmetric monoidal closed category L
(2) a cartesian closed category H
(3) a symmetric monoidal adjunction F ⊣ G formed from symmetric monoidal functors
F : H → L and G : L → H.
There is an equivalent formulation of LNL models using enriched category theory. This
plays a central role in work on the enriched effect calculus [10].
Lemma 3.2. Let H be a cartesian closed category and L be a symmetric monoidal category.
The following data are equivalent:
(1) structure making L an H-enriched symmetric monoidal closed category with copowers;
(2) a symmetric monoidal adjunction between H and L (i.e. a LNL model).
Proof. From (1) to (2), let the adjunction be the copower/hom adjunction
(−) ⊙ I ⊣ L(I, −) : (L, ⊗) → (H, ×).
which is always a symmetric monoidal adjunction.
Since L is symmetric monoidal closed, each − ⊗ Z : L → L has a right adjoint and so
preserves weighted colimits, in particular copowers:
((X ⊙ W ) ⊗ Z) ∼
= X ⊙ (W ⊗ Z)
In particular,
F (X × Y ) = (X × Y ) ⊙ I = X ⊙ (Y ⊙ I) = X ⊙ (I ⊗ (Y ⊙ I))
= (X ⊙ I) ⊗ (Y ⊙ I) = F (X) ⊗ F (Y ).
as required.
From (2) to (1), let the enrichment be given by
def

L(X, Y ) = G(X ⊸ Y ).

18

MATHYS RENNELA AND SAM STATON

def

Then L has copowers given by h ⊙ X = F (h) ⊗ X. For
H(h′ × h, G(C ⊸ D)) ∼
= C(F (h′ × h), C ⊸ D) ∼
= C(F (h′ ) ⊗ F (h), C ⊸ D)
∼
= C(F (h′ ), (F (h) ⊗ C) ⊸ D)) ∼
= H(h′ , G(F (h) ⊗ C) ⊸ D)
One must show that the symmetric monoidal closed structure is enriched. For example,
we must give a map
G(C ⊸ C ′ ) × G(D ⊸ D ′ ) → G(C ⊗ C ′ ⊸ D ⊗ D ′ )
To give such a map is to give a map
F G(C ⊸ C ′ ) ⊗ F G(D ⊸ D ′ ) → (C ⊗ C ′ ) ⊸ (D ⊗ D ′ )
and we use the one that arises from the counit of the adjunction.
Finally we show that passing from (1) to (2) and back to (1) gives the same enriched
structure up to isomorphism. But this is trivial, because
L(I, X ⊸ Y ) ∼
= L(X, Y )
And we must show that passing from (2) to (1) and back to (2) gives the same adjunction,
but this is also fairly trivial because F , being a monoidal left adjoint, must preserve copowers
and the monoidal structure:
F (X) ∼
= F (X × 1) ∼
= X ⊙ F (1) ∼
= X ⊙ I.
Definition 3.3. An LNL-EWire model (L, H, L0 , H0 , F, G) is given by a linear model
(L, H, F, G) together with a small symmetric monoidal full subcategory L0 ⊆ L and a
small full subcategory H0 ⊆ H such that F restricts to a functor H0 → L0 .
Proposition 3.4. Every LNL-EWire model (L, H, L0 , H0 , F, G) induces an EWire model,
when we put
• C = L0 ;
• The enrichment of C is given by C(X, Y ) = G(L(X, Y ));
• T = GF .
Proof. Let us verify that the axioms of Definition 2.1 are verified for the quadruplet (L0 , H0 , H, GF ).
Axiom (3) follows from Lemma 3.2. For Axiom (4) we need to show that L0 has
copowers by objects of H0 . Lemma 3.2 already gives us that L has copowers, and so we
must show that a copower h ⊙ X is in L0 when h ∈ H0 and X ∈ L0 .
LNL-EWire models are defined to be such that F restricts to a functor H0 → L0 , and
since F ∼
= ((−) ⊙ I), this requirement amounts to requiring that (h ⊙ I) ∈ L0 when h ∈ H0 .
Now a LNL-EWire model also assumes that L0 is a symmetric monoidal subcategory,
and (−) ⊗ X preserves copowers since it has a right adjoint in L, so we have the following
isomorphism in L0 :
(h ⊙ X) ∼
= (h ⊙ (I ⊗ X)) ∼
= (h ⊙ I) ⊗ X
For Axiom (5), we must show that A ⊗ − preserves copowers. This again follows from
A ⊗ − having a right adjoint, the closed structure, and hence preserving colimits.
For Axiom (6) we must give an enriched relative monad morphism, but by Lemma 3.2
this can be the identity morphism.

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

19

Theorem 3.5. For every EWire model (C, H, H0 , T ) there is an LNL-EWire model (L, H, L0 , H0 , F, G)
with a L0 = C and a relative monad morphism GF j → T .
The proof of this theorem is postponed until after the following lemma, which is kind-of
contained in [21] and is likely well known in some circles.
Lemma 3.6. Let C be a category enriched in a cartesian closed category H, and suppose
that H is also locally presentable as an enriched category. Let F be a class of weighted
def
colimits in C. Let C̄ = [Cop , H]F be the H-category of F-limit preserving H-functors.
(1) The restriction of the Yoneda embedding C → C̄ preserves F-colimits, and exhibits
the free H-colimit cocompletion of C as a category with F-colimits.
(2) If F-colimits distribute over the monoidal structure, in that the canonical maps
W
colimW
j∈J (Cj ⊗ D) −→ (colimj∈J Cj ) ⊗ D

are isomorphisms, then C̄ admits a symmetric monoidal closed structure, and the
Yoneda embedding C → C̄ strongly preserves the symmetric monoidal structure.
Proof. For (1), we first recall that it is straightforward to show that the Yoneda embedding
factors through C → C̄, this follows from the definition of limit. Moreover, it is routine
to check that this restricted Yoneda embedding preserves F-colimits: this follows from the
Yoneda lemma.
Less trivial is the fact that the C̄ of F-limit preserving functors is a reflective subcategory of the category of all functors Ĉ, i.e. that the embedding C̄ → Ĉ has a left adjoint.
This can be proved using a general method of orthogonality subcategories (e.g. [21, Ch. 6]),
since a functor is in C̄ if it is orthogonal to the canonical morphism
W
colimW
i C(−, di ) → C(−, colimi di )

for each diagram in the class F. From this reflection property we conclude that C̄ has all
colimits.
Now we consider an F-colimit preserving functor F : C → D where D is cocomplete.
We show that F extends essentially uniquely to a functor F! : C̄ → D that preserves all
colimits.
C(=,−)

C

C̄
F

F!

D
First recall that F already extends essentially uniquely to a functor F! : Ĉ → D, which has
a right adjoint, the functor D(F (=), −) : D → Ĉ. Moreover D(F (=), −) factors through
C̄ ⊆ Ĉ: this follows from the assumption that F preserves F-colimits.
So the adjunction
F! ⊣ D(F (=), −) : D → Ĉ
restricts to an adjunction
F! ⊣ D(F (=), −) : D → C̄
and so F! : C̄ → D preserves colimits, and is the required extension of F .
As for (2), recall that the presheaf category Ĉ has a symmetric monoidal closed such
that the Yoneda embedding C → Ĉ is strongly monoidal. This structure is due to Day [8],

20

MATHYS RENNELA AND SAM STATON

and, for F, G ∈ Ĉ, we have
(F ⊗Day G)(Z) =

R X,Y

C(X ⊗ Y, Z) × F (X) × G(Y )

(F ⊸ G)(X) = Ĉ(F, G(X ⊗ −))
If G preserves F-limits, then, because each (X ⊗ −) : C → C preserves F-limits too,
(F ⊸ G) preserves F-limits. In other words, if G ∈ C̄ then (F ⊸ G) ∈ C̄. This condition
is sufficient for extending (⊸) to a symmetric monoidal closed structure on C̄ ⊆ Ĉ, such
that the reflection Ĉ → C̄ is strongly monoidal [9]. (Note that this does not mean that the
embedding C̄ → Ĉ is strongly monoidal.)
Proof. (Proof of Theorem 3.5.) Let F be the class of copowers by objects of H0 . Let
def

L = [Cop , H]F be the category of H0 -copower preserving H-functors. By Lemma 3.6, the
category L has a symmetric monoidal closed structure, and the Yoneda embedding C → L
def
preserves it. Let L0 = C. By Lemma 3.2, this structure gives rise to an LNL model.
Finally, we must give a relative monad morphism GF j → T . Recall that we assume
that in an LNL-EWire model, F restricts to a functor H0 → L0 = C. By Lemma 3.2,
F = ((−) ⊙ I), and this restriction property means that L0 is closed under copowers by
objects of H0 . So GF j = L(I, j(−)⊙I) ∼
= C(I, j(−)⊙I), and the relative monad morphism
is the (run) structure of the EWire model.
From Theorem 3.5, we deduce that every EWire model (C, H, H0 , T ) induces an expodef

def

nential construction ! = J ◦ L(I, −) : L → L where L = [Cop , H]F .
4. Extensions of EWire
Let us part away from the traditional notion of circuits in order to be able to deal with
inputs and outputs of sum types and recursive types: in what follows, circuits are first-order
linear instructions. Therefore, the structures that our circuit language manipulate are not
per se circuits but generalised circuits.
4.1. Conditional branching. To extend EWire with conditional branching, one needs to
introduce sum types (that is, W ::= · · · | W ⊕ W ′ and A ::= · · · | A + A′ ), and gates
in1 ∈ G(W1 , W1 ⊕ W2 ) and in2 ∈ G(W2 , W1 ⊕ W2 ) for every pair of types W1 and W2 .
Additionally, we introduce case expressions
case p of (in1 w1 → C1 | in2 w2 → C2 ) : W
(where p : W1 ⊕ W2 , C1 : Circ(W1 , W ) and C2 : Circ(W2 , W )) and extend the grammar of
patterns:
p ::= · · · | in1 p | in2 p
Then, bit is 1 ⊕ 1. A wire type W ⊕ W ′ is classical if W and W ′ are classical, and then:
def

W ⊕ W ′ = |W | + W ′
Patterns of sums are eliminated using
Ω =⇒ p : Wi
Ω =⇒ ini p : W1 ⊕ W2

i ∈ {1, 2}

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

21

and the typing rule for branching is the following:
Γ; w1 : W1 , Ω′ ⊢ C1 : W

Ω =⇒ p : W1 ⊕ W2

Γ; w2 : W2 , Ω′ ⊢ C2 : W

Γ; Ω, Ω′ ⊢ case p of (in1 w1 → C1 | in2 w2 → C2 ) : W
4.2. Recursive types. Let us complete the grammars of wire types and host types:
W ::= · · · | X | µX.W

A ::= · · · | X | µX.A
def

A wire type µX.W is classical if W is, and |µX.W | = µX. |W |.
We assume that G contains gates
foldµX.W ∈ G(W [X 7→ µX.W ], µX.W )

unfoldµX.W ∈ G(µX.W, W [X 7→ µX.W ])

which corresponds to the folding/unfolding of a recursive type µX.W . For example, for the
type QList of quantum lists defined by QList = µX.qubit ⊗ X ⊕ 1, we have
fold ∈ G(qubit ⊗ QList ⊕ 1, QList)

unfold ∈ G(QList, qubit ⊗ QList ⊕ 1)

def

As another example, QNat = µX.X ⊕ 1 is a wire type of natural numbers and Nat =
def
µX.X +1 is the host type of natural numbers. The type QNat is classical and |QNat| = Nat.
In line with [11], we introduce the recursive typing rules as type judgements Θ ⊢ τ ,
which entail that the type τ is well-formed with respect to the context of distinct type
variables Θ. We introduce the following set of rules for typing judgements:
Θ, X ⊢ W
Θ ⊢ W1 Θ ⊢ W2
⊛
∈
{⊗,
⊕}
′
Θ, X, Θ ⊢ X
Θ⊢1
Θ ⊢ µX.W
Θ ⊢ W ⊛W
1

2

The typing judgement Θ ⊢ Γ holds whenever Γ is a context of language variables such that
Θ ⊢ τ holds for every variable (x : τ ) ∈ Γ.
At this point, one might question the interest for recursive types in a circuit-based
language. In the traditional conceptualization of circuits, lists and other infinite data types
must be instantiated at a specific length to be used as the input type of a circuit and
therefore (iso)recursive types cannot appear in the wire types of a circuit.
Let us illustrate our interest for patterns of recursive types by focusing on the pattern
p : QList. We want to implement the Quantum Fourier Transform. Taking inspiration
from [32, Sec. 6.2] and [15], we assume a host language constant
CR : Nat → Circ(qubit ⊗ qubit, qubit ⊗ qubit)
so that (CR n) corresponds to the controlled rotation by 22π
m around the z-axis. Then the
program rotations performs the rotations of a QFT circuit and the instruction (fourier)
corresponds to the QFT, as illustrated in the circuit in the introduction.

22

MATHYS RENNELA AND SAM STATON

length :
Circ ( QList , QNat⊗QList ) =
box qs = >
cas e qs o f [] = > output
(0 ,[])
| ( q : qs ’) = >
(n , qs ’) <- unbox length
qs ’;
output ( S n , q : qs ’)

rotations :
Nat -> Circ ( qubit⊗QList , qubit⊗QList ) =
lambda m . box (c , qs ) = >
cas e qs o f [] = > output (c ,[])
| ( q : qs ’) = >
(n , qs ’) <- unbox length qs ’ ;
n <= lift n ;
(c , qs ’) <- unbox ( r o t a t i o n s m ) (c , qs ’
) ;
(c , q ) <- unbox ( CR (1+m - n ) ) (c , q ) ;
output (c ,( q : qs ’) )

f o u r i e r : Circ ( QList , QList ) =
box qs = >
cas e qs o f [] = > []
| ( q : qs ’) = >
qs ’ <- unbox f o u r i e r qs ’ ;
(n , qs ’) <- unbox length qs ’ ;
n <= lift n ;
(q , qs ’) <- unbox ( r o t a t i o n s n ) (q , qs ’)
q <- gate H q ; output (q , qs ’)

Here we are using some standard syntactic sugar for recursive types and lists. For example,
length is more verbosely written
Y (lambda l . box qs = >
qs <- unfold qs ;
cas e qs o f
in2 () = > qs <- gate in1 () ; qs <- gate fold qs ;
z <- gate in1 () ; z <- gate fold z ;
output (z , qs )
| in1 (q , qs ) = >
(n , qs ) <- unbox l qs ;
qqs <- gate in1 (q , qs ) ; qqs <- gate fold qqs ;
n ’ <- gate in2 n ; n ’ <- gate fold n ;
output ( n ’ , qqs ) )

where Y is a fixed point combinator, defined using recursive types.
It is important to note that this standard QFT algorithm leaves the list in reverse
order, and so for many purposes this program must be composed with a standard list
reversal program, omitted here.
In this setting, we consider recursive types because they are a quick way of introducing
operations over lists, and these quickly fit into our categorical formalism. The drawback is
that in quantum programming, it is useful to make the lengths of lists more explicit. For
example, the type system does not tell us that (unbox fourier qs) has the same length as
qs. This is a familiar problem in a functional language such as Haskell, but it is particularly
inconvenient for a quantum circuit layout engine, especially if one want to ensure that the
terms which correspond to circuits are terminating.

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

23

A good way to deal with it would be through some kind of dependent types [32, Sec. 6.2],
for instance allowing a type QArray(n) of arrays of qubits of size n and
fourier : (n : Nat) → Circ(QArray(n), QArray(n))
In practice, introducing those dependent types indexed by natural numbers in EWire requires the existence of rules such as
q : qubit l : Π(n:N) QArray(n)
{} : Π(n:N) QArray(0)
fold(q, l) : Π
QArray(n + 1)
(n∈N)

One can see Π(n:N) QArray(n) as the family of types formed by the types for the arrays of
qubits of size n.
However, the discussion here is focused on categorical models of QWire in which one
can denote recursive types, exploiting a presheaf-theoretic semantics which we intend to use
as a foundation for a theory of quantum domains. Therefore, integrating dependent types to
EWire/QWire and associating such types to an appropriate categorical semantics is left for
future work. Ideally, one would want to use dependent types indexed by natural numbers
in order to ensure that circuits terminates, i.e. that every circuit reduces to a normal form.
5. What is a quantum domain?
In this section, we are discussing the possibility of defining quantum domains, that is,
a mathematical objects which describe quantum programs, in the same way that domains
were introduced to describe functional classical programs. We rely on the notion of algebraic
compactness which provides a way to interpret recursive types as fixpoints of endofunctors.
And in line with the technical approach that we have adopted in Section 2 and Section 3,
our quantum domain theory is formulated in the language of enriched category theory. That
is, we consider categories of order-enriched functors, which are functors enriched over some
category of domains (i.e. dcpos, in this context).
Recall that a Dcpo⊥! -enriched category C is algebraically compact [3] for locally continuous endofunctors if every locally continuous endofunctor F on C (i.e. F is such that all
FX,Y : C(X, Y ) → C(F X, F Y ) are Scott-continuous) has a canonical fixpoint written µF ,
which is the initial F -algebra (where Dcpo⊥! is the category of pointed dcpos and strict
Scott-continuous maps).
Every algebraically compact category C, as part of a categorical model (C, H, T ), is
a domain-theoretic model of FPC [11, Def. 6.7] and as such provides a computationally
adequate model for the language FPC, a functional programming language with recursive
types [11, Th. 7.14].
The algebraic compactness of the category of W*-algebras together with (completely)
positive sub-unital maps has already been established [35]. This result establishes W*algebras and completely positive unital maps as a categorical model of higher-order quantum computing. For example, the type QList is denoted by the fixpoint ⊕k≥0 M2k of the
endofunctor F : X 7→ X ⊗ M2 ⊕ 1.
Ultimately, we are interested in quantum domains, that is in finding models and convenient programming languages that mix quantum features and classical features more

24

MATHYS RENNELA AND SAM STATON

generally. Enriched category theory offers a compelling way to elevate ourselves from the
theory of W*-algebras.
Indeed, whenever a category C is enriched over a category H, one can form a category
of H-enriched presheaves [Cop , H], which inherits some of the structure of H and C. In
particular, when a category C is enriched over the category Dcpo (resp. Dcpo⊥! ), orderenriched presheaves Cop → Dcpo (resp. Cop → Dcpo⊥! ) are the objects of the free colimit
completion of the category C as a Dcpo-enriched category (resp. as a Dcpo⊥! -enriched
category). It is worth mentioning that Malherbe et al. [26] also used presheaves in their
steps towards a model of a higher-order quantum programming language.
Definition 5.1. For every category C of quantum computation enriched over the category
Dcpo (resp. Dcpo⊥! ), a quantum predomain (resp. quantum domain) is an order-enriched
contravariant presheaf F : Cop → Dcpo (resp. F : Cop → Dcpo⊥! ). Assuming by
convention that we’re considering a fixed category of quantum computation C, we write
QPredom and QDom! for the presheaf categories [Cop , Dcpo] and [Cop , Dcpo⊥! ].
In an earlier work [37], it was suggested to define a quantum domain as a quantum
predomain whose root F (C) is a pointed dcpo, i.e. a dcpo which has a least element. To
benefit from the notions of Day convolution [8] and algebraic compactness [3], we adopt here
a more restrictive notion of quantum domains as presheaves enriched over pointed dcpos.
It is worth mentioning that the literature is rich of examples of dcpo structures over
quantum systems, upon which quantum (pre)domains can be built. Normal states N S(A)
and predicates [0, 1]A of a C*-algebra A form dcpos whenever A is a W*-algebra. Projections
Proj(A) on a finite-dimensional C*-algebra A, which are elements p of A which are selfadjoint (i.e., p = p∗ ) and idempotent (i.e., p = p2 ), are continuous lattices, used in von
Neumann’s quantum logic. Furthermore, one can consider the dcpo C(A) of commutative
C*-subalgebras of a C*-algebra A (seen as classical views of a quantum system) ordered by
inclusion.
Other examples can be formed from Hilbert spaces. Every m by n complex matrix (resp.
isometry) M ∈ Cm×n induces a completely positive (resp. completely positive unital) map
M ∗ − M : Mm → Mn . Therefore, one can consider the category NMat of non-zero natural
numbers, seen as dimensions, and morphisms m → n, seen as m by n complex matrices. In
this setting, composition is given by matrix multiplication. In this context, every natural
number n ∈ N can be identified with the finite-dimensional Hilbert space Cn .
5.1. A denotational semantics for QWire with recursive types. At this stage, the
skeptical reader might argue that our quantum predomains aren’t much more than glorified
families of dcpos. We justify the adoption of a functorial approach in our quantum domain
theory by the fact that category-theoretic tools easily allow us to define new quantum domains from existing ones. In particular, we can define sums and copowers for quantum
(pre)domains, following a construction already introduced in [37].
As it is the usage in enriched presheaf categories, the coproduct of quantum predomains
(resp. quantum domains) is defined pointwise on the coproduct of Dcpo (resp. Dcpo⊥! ),
and therefore it has the universal property of the coproduct.

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

25

Moreover, for every Dcpo⊥! -enriched category of quantum computation Q with copowers in a category H0 , we can build the copower of quantum domains in H0 as a functor
⊙ : H0 × QDom → QDom
def

(h, F ) 7→ h ⊙ F = F (h ⊙ −) : Qop → Dcpo⊥!

This has the universal property of ‘copower by representables’ (see e.g. [20]). The construction takes inspiration from the fact that the equivalence Mn (A) ∼
= Mn ⊗ A holds for every
C*-algebra A and every natural number n ∈ N. In that context: for every n ∈ N, n ⊙ F is
the quantum domain defined as the mapping A 7→ F (Mn (A)) on objects and f 7→ F (Mn (f ))
on maps.
As for the monoidal product of quantum (pre)domains, it is important to recall that the
Day convolution provides a monoidal structure to any presheaf category of a small category
enriched over a complete and cocomplete closed symmetric monoidal category, such as the
categories Set, Dcpo, Dcpo⊥ [1, Theorem 3.3.3] and Dcpo⊥! [1, Theorem 3.3.4].
The following proposition will not come as a surprise to the reader familiar with enriched
categories: mostly, it follows from the fact that the Yoneda embedding is full and faithful.
Proposition 5.2. Consider a categorical model of QWire (C, Dcpo⊥ , T ) where C is a
def

small category. We write QDom! = [Cop , Dcpo⊥! ] for the category of quantum domains
over the category C, whose coproducts are defined pointwise.
Then, the quadruplet (QDom! , Dcpo⊥ , N, T ) is a categorical model of QWire, with
QDom! algebraically compact for locally continuous endofunctors.

Proof. As discussed at the beginning of this section, the coproduct of quantum domains
F, G : Cop → Dcpo⊥! is defined pointwise on the disjoint sum of pointed dcpos, with the
quantum domain which acts as q 7→ 1 on objects (where 1 = {⋆} is the singleton dcpo). And
the copower ⊙ : H0 × QDom! → QDom! of quantum domains is built upon the copower
of the category C.
Since the category C is a small category, the Day convolution [8] provides us with
a symmetric monoidal closed structure (QDom! , ⊗Day , ⊸) for quantum domains, and algebraic compactness for locally continuous endofunctors on QDom! is given by [11, Example 6.9], which states that the Dcpo⊥! -enriched category of Dcpo⊥! -enriched functors
W → Dcpo⊥! is algebraically compact for locally continuous endofunctors for every small
Dcpo⊥! -enriched category W.
Then, every endofunctor F ⊗ − on the category QDom! has a right adjoint in the
monoidal closed structure and therefore preserves colimits, and in particular copowers.
Finally, exploiting the fact that the enriched Yoneda embedding y : C → [Cop , Dcpo⊥! ]
is full and faithful, we observe that there is a one-to-one correspondance between completely
positive unital maps I → J(n) and Scott-continuous natural transformations
C(−, I) ⇒ C(−, J(n))
which leads us to the following equivalence
T (n) ∼
= C(I, J(n)) ∼
= [Cop , Dcpo⊥! ](I, J(n)) for every n ∈ N

26

MATHYS RENNELA AND SAM STATON

Consequently, the triplet ([FdC∗ -Algop
CPSU , Dcpo⊥! ], Dcpo⊥ , V ) is a categorical model
of QWire, which will be investigated in future work. It is worth noting that while Section 3
considered over a cartesian closed category, we’re providing here another construction in
terms of enriched functors but this time over the monoidal closed category Dcpo⊥! , in order
to obtain algebraic compactness. This suggests that the construction in terms of enriched
functors provided by Theorem 3.5 isn’t unique.
On another matter, it is important to note that probabilistic computations are captured
by commutative C*-algebras, offering us a model for probabilistic circuits given by the triplet
∗
([FdCC∗ -Algop
CPSU , Dcpo⊥! ], Dcpo⊥! , V ), where FdCC -AlgCPSU is the category of finitedimensional commutative C*-algebras together with completely positive sub-unital maps
between them). This is particularly interesting since the Lawvere theory L≤1 of subconvex
sets is equivalent to FdCC∗ -Algop
CPSU [12], the opposite category of the category of finitedimensional commutative C*-algebras and completely positive sub-unital maps. We expect
that this semantic connection between probabilistic and quantum programming might be
the point of start of a better understanding of the interaction between those two paradigms.
Summary. Having described a family of embedded languages for (quantum) circuits in
Section 1, we describe their denotational models in enriched category theory in Section 2.
Later in Section 3, we establish a connection with the Benton’s notion of linear-non-linear
models. Finally, after an exploration in Section 4 of some of the possible extensions of the
languages considered in this work, we initiate a discussion on quantum domain theory in
Section 5, that we describe through the study of the denotational semantics of quantum
programming languages using enriched category theory and domain theory.
Acknowledgements. The authors would like to thank Tom Hirschowitz, Bart Jacobs,
Shane Mansfield, Paul-André Melliès, Michele Pagani, and Peter Selinger for helpful discussions, but also Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev for hosting
the first author at Tulane University during the early stage of the elaboration of this work,
and Jennifer Paykin and Robert Rand for introducing us to the subtle aspects of QWire.
The research leading to these results has received funding from the ERC grant agreement
n. 320571, a Royal Society fellowship, and the EPSRC grant EP/N007387/1.
References
[1] Samson Abramsky and Achim Jung. Domain theory. In Handbook of logic in computer science. Oxford
University Press, 1994.
[2] Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. In
Proc. FOSSACS’10, pages 297–311. Springer, 2010.
[3] Michael Barr. Algebraically compact functors. Journal of Pure and Applied Algebra, 82(3):211–231,
1992.
[4] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop
on Computer Science Logic, pages 121–135. Springer, 1994.
[5] Clemens Berger, Paul-André Melliès, and Mark Weber. Monads with arities and their associated theories.
J. Pure Appl. Algebra, 216(8-9):2029–2048, 2012.
[6] Kenta Cho. Semantics for a quantum programming language by operator algebras. New Generation
Computing, 34(1-2):25–68, 2016.
[7] Ugo Dal Lago, Claudia Faggian, Benoı̂t Valiron, and Akira Yoshimizu. The geometry of parallelism:
classical, probabilistic, and quantum effects. In Proceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages, pages 833–845. ACM, 2017.

CLASSICAL CONTROL AND QUANTUM CIRCUITS IN ENRICHED CATEGORY THEORY

27

[8] Brian Day. On closed categories of functors. In Reports of the Midwest Category Seminar IV, pages
1–38. Springer, 1970.
[9] Brian Day. A reflection theorem for closed categories. Journal of Pure and Applied Algebra, 2:1–11,
1972.
[10] Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. The enriched effect calculus: syntax and
semantics. Journal of Logic and Computation, 2012.
[11] Marcelo P Fiore and Gordon D Plotkin. An axiomatisation of computationally adequate domain theoretic models of FPC. In Proc. LICS’94, 1994.
[12] Robert Furber and Bart Jacobs. From Kleisli categories to commutative C*-algebras: probabilistic
Gelfand duality. In Proc. CALCO’13, pages 141–157. Springer, 2013.
[13] Dan R Ghica and Achim Jung. Categorical semantics of digital circuits. In Proceedings of the 16th
Conference on Formal Methods in Computer-Aided Design, pages 41–48. FMCAD Inc, 2016.
[14] Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1–101, 1987.
[15] Alexander S Green, Peter LeFanu Lumsdaine, Neil J Ross, Peter Selinger, and Benoı̂t Valiron. Quipper:
a scalable quantum programming language. In Proc. PLDI’13, pages 333–342. ACM, 2013.
[16] Ichiro Hasuo and Naohiko Hoshino. Semantics of higher-order quantum computation via geometry of
interaction. Annals of Pure and Applied Logic, 168(2):404–469, 2017.
[17] Bart Jacobs. On block structures in quantum computation. In Proc. MFPS’13, volume 298 of Electron.
Notes Theor. Comput. Sci., pages 233–255. Elsevier, 2013.
[18] Bart Jacobs. A recipe for state-and-effect triangles. In Proc. CALCO’15, volume 35, 2015.
[19] Bart Jacobs. A recipe for state-and-effect triangles. Logical Methods in Computer Science, 13, 2017.
[20] George Janelidze and Gregory M Kelly. A note on actions of a monoidal category. Theory Appl. Categ,
9(61-91):02, 2001.
[21] Max Kelly. Basic concepts of enriched category theory, volume 64. CUP Archive, 1982.
[22] Aleks Kissinger and Sander Uijlen. A categorical semantics for causal structure. In Proc. LICS’17, 2017.
[23] Andre Kornell. Quantum collections. arXiv preprint arXiv:1202.2994, 2012.
[24] Paul Blain Levy. Call-by-push-value: A functional/imperative Synthesis, volume 2. Springer Science &
Business Media, 2012.
[25] Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. A dcpo-enriched linear/non-linear model.
manuscript, 2017.
[26] Octavio Malherbe, Philip Scott, and Peter Selinger. Presheaf models of quantum computation: an outline. In Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky,
pages 178–194. Springer, 2013.
[27] Paul-André Melliès. Parametric monads and enriched adjunctions. 2012.
[28] R. E. Møgelberg and Sam Staton. Linear usage of state. Logical Methods in Computer Science, 10(1),
2014.
[29] Eugenio Moggi. Computational lambda-calculus and monads. In Proc. LICS’89, 1989.
[30] Peter O’Hearn. On bunched typing. Journal of functional Programming, 13(4):747–796, 2003.
[31] Michele Pagani, Peter Selinger, and Benoı̂t Valiron. Applying quantitative semantics to higher-order
quantum computing. In Proc. POPL’14, pages 647–658. ACM, 2014.
[32] Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: a core language for quantum circuits. In
Proc. POPL’17, pages 846–858. ACM, 2017.
[33] John Power. Enriched Lawvere theories. Theory Appl. Categories, 6(7):83–93, 1999.
[34] Robert Rand, Jennifer Paykin, and Steve Zdancewic. Qwire practice: Formal verification of quantum
circuits in coq. EPTCS, 2017.
[35] Mathys Rennela. Towards a quantum domain theory: order-enrichment and fixpoints in W*-algebras.
In Proc. MFPS XXX, volume 308, pages 289–307, 2014.
[36] Mathys Rennela. Operator algebras in quantum computation. arXiv preprint arXiv:1510.06649, 2015.
[37] Mathys Rennela and Sam Staton. Complete positivity and natural representation of quantum computations. In Proc. MFPS XXXI, volume 319, pages 369–385. Electron. Notes Theoret. Comput. Sci.,
2015.
[38] Francisco Rios and Peter Selinger. A categorical model for a quantum circuit description language.
arXiv preprint arXiv:1706.02630, 2017.
[39] Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, 2015.

28

MATHYS RENNELA AND SAM STATON

[40] Peter Selinger. Towards a quantum programming language. Math. Struct. Comput. Sci., 14(04):527–586,
2004.
[41] Sam Staton. Freyd categories are enriched Lawvere theories. In Proc. WACT, Electron. Notes Theor.
Comput. Sci., pages 197–206, 2013.
[42] Sam Staton. Algebraic effects, linearity, and quantum programming languages. In Proc. POPL’15, pages
395–406. ACM, 2015.
[43] Dave Wecker and Krysta M Svore. LIQUi|>: A software design architecture and domain-specific language for quantum computing. arXiv preprint arXiv:1402.4467, 2014.

This figure "qft.png" is available in "png" format from:
http://arxiv.org/ps/1711.05159v1

