1

# Semantics for Variational Quantum Programming

Xiaodong Jia  School of MathematicsHunan UniversityChangsha410082China ,
Andre Kornell  Department of Computer ScienceTulane UniversityNew
OrleansLouisianaUSA ,  Bert Lindenhovius  Department of Knowledge-Based
Mathematical SystemsJohannes Kepler UniversitätLinzAustria ,  Michael Mislove
Department of Computer ScienceTulane UniversityNew OrleansLouisianaUSA and
Vladimir Zamdzhiev  Université de Lorraine, LORIAInriaNancyF 54000France

###### Abstract.

We consider a programming language that can manipulate both classical and
quantum information. Our language is type-safe and designed for variational
quantum programming, which is a hybrid classical-quantum computational
paradigm. The classical subsystem of the language is the Probabilistic
FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance
recursive types, term recursion and probabilistic choice. The quantum
subsystem is a first-order linear type system that can manipulate quantum
information. The two subsystems are related by mixed classical/quantum terms
that specify how classical probabilistic effects are induced by quantum
measurements, and conversely, how classical (probabilistic) programs can
influence the quantum dynamics. We also describe a sound and computationally
adequate denotational semantics for the language. Classical probabilistic
effects are interpreted using a recently-described commutative probabilistic
monad on $\mathbf{DCPO}$. Quantum effects and resources are interpreted in a
category of von Neumann algebras that we show is enriched over (continuous)
domains. This strong sense of enrichment allows us to develop novel semantic
methods that we use to interpret the relationship between the quantum and
classical probabilistic effects. By doing so we provide the first denotational
analysis that relates models of classical probabilistic programming to models
of quantum programming.

Quantum Programming, Probabilistic Programming, Semantics

††journal: PACMPL††journalvolume: 1††journalnumber: POPL††article:
1††journalyear: 2022††publicationmonth: 1††copyright: none††ccs: Semantics of
programming languages

##  1\. Introduction

Variational quantum algorithms (Peruzzo et al., 2014; McClean et al., 2016)
are increasingly important in quantum computation. The main idea is to use
hybrid classical-quantum algorithms that work in tandem to solve computational
problems. The classical part of the computation is executed on a classical
processor and the quantum part on a quantum device. During the overall
computation, intermediary results produced by the quantum device occur with
certain probabilities, and then are passed to the classical processor, which
performs computations that are used to tune the parameters of the quantum
component of the algorithm, thereby influencing the quantum dynamics.

These kinds of hybrid classical-quantum algorithms pose interesting challenges
for the design of suitable programming languages. Clearly, if we wish to
understand how to program in such scenarios, we need to devise a type system
equipped with an operational semantics that correctly models the manipulation
of _quantum resources_. This includes accounting for the fact that quantum
measurements induce _probabilistic computational effects_ that are inherited
by the classical side of the system. Moreover, quantum information behaves
very differently from classical information. For instance, quantum information
cannot be copied (Wootters and Zurek, 1982). In order to avoid potential
runtime errors, a _substructural typing discipline_ (Girard, 1987; Benton,
1995; Benton and Wadler, 1996) where contraction is restricted is appropriate
for the quantum subsystem. But, when manipulating classical information, such
restrictions are unnecessary and often inconvenient. Therefore we wish to have
a classical (non-linear) subsystem together with a quantum (linear) one that
interact nicely with each other. Furthermore, separating the quantum and
classical modes of operations has the added benefit that it makes it easier to
_extend_ existing classical programming languages with the necessary features
for type-safe variational quantum programming.

The purpose of the present paper is to address this challenge by describing a
type-safe programming language that combines classical (probabilistic)
computation with quantum computation. Another one of our goals is to provide a
denotational interpretation so that we may establish useful reasoning
principles and therefore cement the design of our language.

###  1.1. Our Contributions

We describe a programming language that is suitable for hybrid classical-
quantum computation that we call $\mathtt{VQPL}$, the _Variational Quantum
Programming Language_ (§2). The language has two kinds of judgements: a
classical (non-linear) judgement that represents classical programs, and a
quantum (linear) judgement that represents quantum programs. Our type system
also contains hybrid classical-quantum formation rules that explain how
classical probabilistic and quantum computation interact with each other (see
Figure 7).

From an operational perspective, $\mathtt{VQPL}$ supports both classical
probabilistic and quantum effects. The quantum dynamics are modelled via a
probabilistic reduction relation on quantum configurations (terms with quantum
data embedded within them), where the probabilities of reduction are
determined in accordance with the laws of quantum mechanics. The classical
dynamics are modelled via a probabilistic reduction relation on terms, where
the probabilities of reduction are induced by the quantum dynamics. We show
that our system $\mathtt{VQPL}$ is type-safe (§2.3).

We also provide a denotational interpretation of our system. We use a
recently-described commutative probabilistic monad on the category
$\mathbf{DCPO}$ (Jia et al., 2021) in order to interpret the classical
probabilistic effects (we recall this construction in §3). We interpret
quantum effects and resources in the category of hereditarily atomic von
Neumann algebras (§4), which are mathematical structures used by physicists to
study quantum foundations (Takesaki, 2000). We prove that this category is
enriched over _continuous domains_ (§4.3). This is a very strong sense of
enrichment that allows us to develop novel semantic methods that we use to
interpret the relationship between the quantum and classical probabilistic
effects (§5). In particular, we show that the theory of Kegelspitzen (Keimel
and Plotkin, 2017) provides a crucial link between the two different ways that
probability arises on the classical and quantum sides, respectively. This
allows us to systematically present all the relevant mathematical structure
within a categorical model (§6) and to use our model to provide a sound and
strongly adequate interpretation of $\mathtt{VQPL}$ (§7). Our paper is the
first to present a mathematical and denotational analysis on the link between
models of classical probabilistic programming and quantum programming. We
discuss related work and provide concluding remarks in §8.

##  2\. VQPL - The Variational Quantum Programming Language

In this section we describe the syntax and operational semantics for
$\mathtt{VQPL}$ . The classical subsystem is the _Probabilistic FixPoint
Calculus_ ($\mathtt{PFPC}$), the same language as in (Jia et al., 2021).
$\mathtt{PFPC}$ is a call-by-value simply-typed lambda calculus with mixed-
variance recursive types, (induced) term recursion and discrete probabilistic
choice. The quantum fragment of the language is a first-order linear type
system with inductive types and equipped with the usual primitives for
manipulating quantum information. This fragment is most similar to (Péchoux et
al., 2020), however in the present paper we choose a Church-style syntax in
order to more easily relate it to the classical subsystem. The distinguishing
feature of our system is the mixed linear/non-linear and quantum/classical
rules that allow the programmer to switch between the classical and quantum
modes of operation. These features make our language suitable for programming
variational quantum algorithms, where both classical and quantum computation
work in synchrony in order to solve computational problems. Our mixed
quantum/classical rules have some similarities with the QWIRE/EWIRE languages
(Paykin et al., 2017; Rennela and Staton, 2020), but both of these languages
have some severe limitations that make them unsuitable for describing
variational quantum algorithms, whereas our language does not. This is
discussed in more detail in §8.

In order to make the paper easier to read, we use bold notation for the
quantum types, contexts and terms, so that we can easily distinguish them from
the classical primitives.

###  2.1. The Type Structure

We use $X,Y$ to range over _classical type variables_ and we use
$\mathbf{X},\mathbf{Y}$ to range over _quantum type variables_. We use
$\Theta$ and $\mathbf{\Theta}$ to range over classical and quantum _type
contexts_ , respectively. Type variables and type contexts are used for the
formation of recursive types, just like in FPC (Abadi and Fiore, 1996; Fiore
and Plotkin, 1994). We say that a classical type context
$\Theta=X_{1},\ldots,X_{n}$ is _well-formed_ , written $\Theta\vdash$,
whenever all type variables within it are distinct, and likewise for a quantum
type context. The _classical types_ of our language are ranged over by $P,R$,
and the _quantum types_ are ranged over by $\mathbf{A},\mathbf{B}$. The
grammars and formation rules for our types are specified in Figure 1. The
notation $\Theta\vdash P$ indicates that type $P$ is _well-formed_ in type
context $\Theta$, and likewise for the quantum types. Of course, we are only
interested in well-formed types and from now on we only deal with such types.
The _closed classical types_ are those where $\cdot\vdash P$ and the _closed
quantum types_ are those where $\cdot\vdash\mathbf{A}$. Notice that recursive
types may be formed with no restrictions on the admissible logical polarities,
just like in FPC.

Quantum Type Variables | $\mathbf{X},\mathbf{Y}$ |  |  Classical Type Variables $X,Y$
---|---|---|---
Quantum Type Contexts | $\mathbf{\Theta}$ | ::= | $\mathbf{X}_{1},\mathbf{X}_{2},\ldots,\mathbf{X}_{n}$
Classical Type Contexts | $\Theta$ | ::= | $X_{1},X_{2},\ldots,X_{n}$
Quantum Types | $\mathbf{A},\mathbf{B}$ | ::= |  $\mathbf{X}$ | $\mathbf{I}$ | qbit | $\mathbf{A\oplus B}$ | $\mathbf{A\otimes B}$ | $\mathbf{\mu\mathbf{X}.A}$
Classical Types | $P,R$ | ::= |  $X$ | $1$ | $P+R$ | $P\times R$ | $P\to R$ | $Q(\mathbf{A},\mathbf{B})$ | $\mu X.P$
Observable Quantum Types | $\mathbf{O}$ | ::= |  $\mathbf{X}$ | $\mathbf{I}$ | $\mathbf{O_{1}\oplus O_{2}}$ | $\mathbf{O_{1}\otimes O_{2}}$ | $\mathbf{\mu\mathbf{X}.O}$
Observable Classical Types | $O$ | ::= |  $X$ | $1$ | $O_{1}+O_{2}$ | $O_{1}\times O_{2}$ | $\mu X.O$

$\mathbf{\Theta}\vdash$ $\mathbf{\Theta}\vdash\mathbf{\Theta}_{i}$
$\mathbf{\Theta}\vdash$ $\mathbf{\Theta}\vdash\mathbf{I}$
$\mathbf{\Theta}\vdash$ $\mathbf{\Theta}\vdash\textnormal{{qbit}}$
$\mathbf{\Theta}\vdash\mathbf{A}$ $\mathbf{\Theta}\vdash\mathbf{B}$
$\star\in\\{\oplus,\otimes\\}$
$\mathbf{\Theta}\vdash\mathbf{A}\star\mathbf{B}$
$\mathbf{\Theta},\mathbf{X}\vdash\mathbf{A}$
$\mathbf{\Theta}\vdash\mu\mathbf{X}.\mathbf{A}$

$\Theta\vdash$ $\Theta\vdash\Theta_{i}$ $\Theta\vdash$ $\Theta\vdash 1$
$\Theta\vdash P$ $\Theta\vdash R$ $\star\in\\{+,\times,\to\\}$ $\Theta\vdash
P\star R$ $\cdot\vdash\mathbf{A}$ $\cdot\vdash\mathbf{B}$ $\Theta\vdash$
$\Theta\vdash Q(\mathbf{A},\mathbf{B})$ $\Theta,X\vdash P$ $\Theta\vdash\mu
X.P$

$|\mathbf{X}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}X\quad|\mathbf{I}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}1\quad|\mathbf{O_{1}\otimes
O_{2}}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}|\mathbf{O_{1}}|\times|\mathbf{O_{2}}|\quad|\mathbf{O_{1}\oplus
O_{2}}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}|\mathbf{O_{1}}|+|\mathbf{O_{2}}|\quad|\mathbf{\mu
X.O}|\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\mu
X.|\mathbf{O}|$

Figure 1. Grammars and formation rules for types and translation between
observable types.

We now explain how our types should be understood. On the quantum side:
$\mathbf{I}$ is the quantum unit type; qbit is the type of qubits (quantum
bits); $\mathbf{A}\oplus\mathbf{B}$ represents quantum sum types;
$\mathbf{A}\otimes\mathbf{B}$ represents quantum pair types;
$\mathbf{\mu\mathbf{X}.A}$ is used to form quantum inductive types. All terms
of quantum type obey a linear typing discipline and so these types should be
viewed as being linear. On the classical side: $1$ is the classical unit type;
$P+R$ is for classical sum types; $P\times R$ is for classical pair types;
$P\to R$ is for classical (higher-order) function types; $\mu X.P$ is used to
form classical recursive types; $Q(\mathbf{A},\mathbf{B})$ is the type of
_first-order_ quantum lambda abstractions between quantum types $\mathbf{A}$
and $\mathbf{B}$. All terms of classical type follow a non-linear typing
discipline (no restrictions on weakening and contraction), so they should be
understood as being non-linear. Notice that the type
$Q(\mathbf{A},\mathbf{B})$ is _classical_ (non-linear). This is because our
quantum lambda abstractions are first-order and therefore they may be used any
number of times (including zero). This type would correspond to
$!(\mathbf{A}\multimap\mathbf{B})$ in a call-by-value linear lambda calculus
and may be informally thought of in this way.

###### Example 2.1.1.

Some important (closed) types are defined as follows: _Booleans_ as
$\mathtt{Bool}\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}1+1$;
_Bits_ as $\mathbf{Bit}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathbf{I}\oplus\mathbf{I}$; _Natural numbers_ as
$\mathtt{Nat}\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\mu
X.1+X$; _Linear/Quantum natural numbers_ as
$\mathbf{QNat}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathbf{\mu}\mathbf{X}.\mathbf{I}\oplus\mathbf{X}$; _Lists of
type_ $A$ as $\mathtt{List}(A)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mu X.1+(A\times X)$; _Linear/Quantum lists of type_ $\mathbf{A}$
as $\mathbf{List}(\mathbf{A})\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mu\mathbf{X.I\oplus(A\otimes X)}$; _Classical Streams of type_
$A$ as $\mathtt{Stream}(A)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mu X.1\to A\times X$.

A _subset_ of our classical/quantum types are the _observable_
classical/quantum types, which are defined in Figure 1. We use $O$ and
$\mathbf{O}$ to range over the observable classical/quantum types,
respectively. These types play an important role for some of the mixed
quantum-classical rules that we explain later. The observable quantum types
may also be understood from a physical perspective because values of these
types correspond to physically observable information. An example of a non-
observable quantum type is qbit. Indeed, observing a qubit in the physical
sense is done via a quantum measurement, which destroys the qubit and produces
a bit as output (note that $\mathbf{Bit}$ is observable in our system). The
observable classical types are exactly the _ground types_ , i.e., types formed
without any use of classical/quantum function space. The observable quantum
types are in a 1-1 correspondence with the observable classical types. For
each observable quantum type $\mathbf{O}$, we write $|\mathbf{O}|$ to indicate
its observable classical counterpart. See Figure 1 for a precise definition of
$|-|$.

###  2.2. The Term Language

Quantum Variables | $\mathbf{x},\mathbf{y}$ |  Classical Variables $x,y$ Quantum Configurations $\mathcal{C}$ ::= $[\lvert\psi\rangle,\ell,\mathbf{q}]$
---|---|---
Classical Terms | $m,n$ | ::= | $x\ |\ ()\ |\ (m,n)\ |\ \pi_{1}m\ |\ \pi_{2}m\ |\ \textnormal{\text{fold}}\ m\ |\ \textnormal{\text{unfold}}\ m\ |\ \lambda x.m\ |\ mn\ |\ $
|  |  | $\emph{in}_{1}m\ |\ \emph{in}_{2}m\ |\ (\text{case}\ m\ \text{of}\ \emph{in}_{1}x\Rightarrow n_{1}\ |\ \emph{in}_{2}y\Rightarrow n_{2})\ |$
|  |  | ${\lambda}\mathbf{(x_{1},\ldots,x_{n}).q}\ |\ \text{new}\ |\ \text{meas}\ |\ U\ |\ \text{run }\mathcal{C}$
Quantum Terms | $\mathbf{q},\mathbf{r}$ | ::= | $\mathbf{x\ |\ *\ |\ q;r\ |\ q\otimes r\ |\ let\ x\otimes y=q\ in\ r\ |\ fold\ q\ |\ unfold\ q\ |\ }m\mathbf{q}\ |\ \mathbf{init}\ m\ |$
|  |  | $\mathbf{in_{1}\ q\ |in_{2}\ q\ |\ (case\ q\ of\ in_{1}x\Rightarrow r_{1}\ |\ in_{2}y\Rightarrow r_{2}})\ |\ \mathbf{let}\ x=\text{lift}\ \mathbf{q}\ \mathbf{in\ r}$
Classical Values | $v,w$ | ::= | $x\ |\ ()\ |\ (v,w)\ |\ \emph{in}_{1}v\ |\ \emph{in}_{2}v\ |\ \textnormal{\text{fold}}\ v\ |\ \lambda x.m\ |\ {\lambda}\mathbf{(x_{1},\ldots,x_{n}).q}\ |\ $
|  |  | $\text{new}\ |\ \text{meas}\ |\ U$
Quantum Values | $\mathbf{v},\mathbf{w}$ | ::= | $\mathbf{x\ |\ *\ |\ v\otimes w\ |\ in_{1}\ v\ |\ in_{2}\ v\ |\ fold\ v}$

Figure 2. Grammars for terms, values and quantum configurations.

$\Phi\vdash$ $\Phi,x:P\vdash x:P$ $\Phi\vdash$ $\Phi\vdash():1$ $\Phi\vdash
m:P$ $\Phi\vdash n:R$ $\Phi\vdash(m,n):P\times R$ $\Phi\vdash m:P_{1}\times
P_{2}$ $i\in\\{1,2\\}$ $\Phi\vdash\pi_{i}m:P_{i}$

$\Phi\vdash m:P$ $\Phi\vdash\emph{in}_{1}m:P+R$ $\Phi\vdash m:R$
$\Phi\vdash\emph{in}_{2}m:P+R$ $\Phi\vdash m:P_{1}+P_{2}$ $\Phi,x:P_{1}\vdash
n_{1}:R$ $\Phi,y:P_{2}\vdash n_{2}:R$ $\Phi\vdash(\text{case}\ m\ \text{of}\
\emph{in}_{1}x\Rightarrow n_{1}\ |\ \emph{in}_{2}y\Rightarrow n_{2}):R$

$\Phi,x:P\vdash m:R$ $\Phi\vdash\lambda x^{P}.m:P\to R$ $\Phi\vdash m:P\to R$
$\Phi\vdash n:P$ $\Phi\vdash mn:R$ $\Phi\vdash m:P[\mu X.P/X]$
$\Phi\vdash\textnormal{\text{fold}}{}\ m:\mu X.P$ $\Phi\vdash m:\mu X.P$
$\Phi\vdash\textnormal{\text{unfold}}\ m:P[\mu X.P/X]$

Figure 3. Formation rules for terms in the (classical) FPC subsystem.

$\vdash\Phi,x:\mathbf{A}$ $\Phi;\mathbf{x:A\vdash x:A}$
$\vdash\Phi,x:\mathbf{A}$ $\Phi;\cdot\vdash*:\mathbf{I}$
$\Phi;\mathbf{\Gamma_{1}\vdash q:I}$ $\Phi;\mathbf{\Gamma_{2}\vdash r:A}$
$\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash q;r:\mathbf{A}}$
$\Phi;\mathbf{\Gamma_{1}\vdash q:A}$ $\Phi;\mathbf{\Gamma_{2}\vdash r:B}$
$\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash q\otimes r:A\otimes B}$

$\Phi;\mathbf{\Gamma_{1}\vdash q:A_{1}\otimes A_{2}}$
$\Phi;\mathbf{\Gamma_{2},x:A_{1},y:A_{2}\vdash r:B}$
$\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash let\ x\otimes y=q\ in\ r:B}$
$\Phi;\mathbf{\Gamma\vdash q:A[\mu X.A/X]}$
$\Phi;\mathbf{\Gamma\vdash\textbf{fold}\ q:\mu X.A}$
$\Phi;\mathbf{\Gamma\vdash q:\mu X.A}$
$\Phi;\mathbf{\Gamma\vdash\textbf{unfold}\ q:A[\mu X.A/X]}$

$\Phi;\mathbf{\Gamma\vdash q:A}$ $\Phi;\mathbf{\Gamma\vdash in_{1}\ q:A\oplus
B}$ $\Phi;\mathbf{\Gamma\vdash q:B}$ $\Phi;\mathbf{\Gamma\vdash in_{2}\
q:A\oplus B}$

$\Phi;\mathbf{\Gamma_{1}\vdash q:A_{1}\oplus A_{2}}$
$\Phi;\mathbf{\Gamma_{2},x:A_{1}\vdash r_{1}:B}$
$\Phi;\mathbf{\Gamma_{2},y:A_{2}\vdash r_{2}:B}$
$\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash(case\ q\ of\ in_{1}x\Rightarrow
r_{1}\ |\ in_{2}y\Rightarrow r_{2}):B}$

Figure 4. Formation rules for terms in the purely linear first-order
subsystem.

$\leavevmode\hbox{ \ignorespaces \ignorespaces\leavevmode\lower
25.5pt\hbox{\vbox{\hbox{\hskip 29.68253pt\hbox{\hskip 0.5pt\hbox{
\phantom{$\Phi;\vdash$}}\hskip 0.5pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to79.36507pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
0.5pt\hbox{$\Phi\vdash\text{new}:Q(\textnormal{{bit}},\textnormal{{qbit}})$}\hskip
0.5pt}}}} \ignorespaces}\quad\leavevmode\hbox{ \ignorespaces
\ignorespaces\leavevmode\lower 25.5pt\hbox{\vbox{\hbox{\hskip
31.70753pt\hbox{\hskip 0.5pt\hbox{ \phantom{$\Phi;\vdash$}}\hskip
0.5pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to83.41507pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
0.5pt\hbox{$\Phi\vdash\text{meas}:Q(\textnormal{{qbit}},\textnormal{{bit}})$}\hskip
0.5pt}}}} \ignorespaces}\quad\leavevmode\hbox{ \ignorespaces
\ignorespaces\leavevmode\lower 25.985pt\hbox{\vbox{\hbox{\hskip 0.5pt\hbox{$U$
is a unitary of arity of $n$}\hskip 0.5pt}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to106.87852pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 6.12344pt\hbox{\hbox{\hskip
0.5pt\hbox{$\Phi\vdash U:Q(\textnormal{{qbit}}^{\otimes
n},\textnormal{{qbit}}^{\otimes n})$}\hskip 0.5pt}}}}}
\ignorespaces}\qquad\textnormal{{bit}}\equiv\mathbf{I}\oplus\mathbf{I}$

Figure 5. Formation rules for term constants that manipulate quantum
information.

$|\mathbf{*}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}()\quad|\mathbf{v\otimes
w}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}(|\mathbf{v}|,|\mathbf{w}|)\quad|\mathbf{in_{1}\
v}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\emph{in}_{1}|\mathbf{v}|\quad|\mathbf{in_{2}\
v}|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\emph{in}_{2}|\mathbf{v}|\quad|\mathbf{fold\
v}|\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\text{fold}\
|\mathbf{v}|$

Figure 6. Translation between _closed_ and observable quantum/classical
values.

$\Phi;\mathbf{x_{1}:A_{1},\ldots,x_{n}:A_{n}\vdash q:B}$
$\Phi\vdash{\lambda}\mathbf{(x_{1},\ldots,x_{n}).q}:Q(\mathbf{A_{1}\otimes\cdots\otimes
A_{n},B})$ $\Phi\vdash m:Q(\mathbf{A},\mathbf{B})$ $\Phi;\mathbf{\Gamma\vdash
q:A}$ $\Phi;\mathbf{\Gamma}\vdash m\mathbf{q}:\mathbf{B}$
$\Phi\vdash\mathcal{C}:\mathbf{O};\textnormal{{qbit}}^{k}$
$\Phi\vdash\text{run }\mathcal{C}:|\mathbf{O}|$

$\Phi\vdash m:|\mathbf{O}|$ $\Phi;\cdot\vdash\mathbf{init}\ m:\mathbf{O}$
$\Phi;\mathbf{\Gamma_{1}\vdash q:\mathbf{O}}$
$\Phi,x:|\mathbf{O}|;\mathbf{\Gamma_{2}\vdash r:\mathbf{A}}$
$\Phi;\mathbf{\Gamma_{1},\Gamma_{2}}\vdash\mathbf{let}\ x=\text{lift}\
\mathbf{q}\ \mathbf{in\ r}:\mathbf{A}$

Figure 7. Formation rules for terms that mediate between the quantum and
classical modes of operation.

For the formation of terms and term contexts, we implicitly assume that all
types within are closed and well-formed. We use $x,y$ to range over _classical
term variables_ and $\mathbf{x},\mathbf{y}$ to range over _quantum term
variables_. Classical term contexts are ranged over by $\Phi$ and quantum term
contexts by $\mathbf{\Gamma}$. The (well-formed) term contexts are simply
lists of (distinct) variables with their types.

The term grammars of $\mathtt{VQPL}$ are specified in Figure 7. We write
$\Phi\vdash m:P$ to indicate that a classical term $m$ is well-formed and has
type $P$ given classical context $\Phi$. We write
$\Phi;\mathbf{\Gamma}\vdash\mathbf{q}:\mathbf{A}$ to indicate that a quantum
term $\mathbf{q}$ is well-formed and has type $\mathbf{A}$, given classical
context $\Phi$ and quantum context $\mathbf{\Gamma}$. A classical term $m$ of
type $A$ is _closed_ when $\cdot\vdash m:A$ and in this case we also simply
write $m:A.$ Likewise we write $\mathbf{q}:\mathbf{A}$ when
$\cdot;\cdot\vdash\mathbf{q}:\mathbf{A}$, and then we also say $\mathbf{q}$ is
closed. We use $v,w$ to range over classical values and
$\mathbf{v},\mathbf{w}$ to range over quantum values (see Figure 7).

###### Example 2.2.2.

Important closed values include: the (classical) _false_ and _true_ values
given by $\mathtt{ff}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathtt{in}_{1}():\mathtt{Bool}$ and
$\mathtt{tt}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathtt{in}_{2}():\mathtt{Bool};$ the false and true bits are
defined by $\mathbf{ff}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathbf{in}_{1}*:\mathbf{Bit}$ and
$\mathbf{tt}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathbf{in}_{2}*:\mathbf{Bit};$ the _zero natural number_
$\mathtt{zero}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathtt{fold}\ \mathtt{in}_{1}():\mathtt{Nat}$ and the _successor
function_ $\mathtt{succ}\ \stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\lambda n^{\mathtt{Nat}}.\mathtt{fold}\
\mathtt{in}_{2}n:\mathtt{Nat}\to\mathtt{Nat};$ quantum versions of
$\mathtt{zero}$ and $\mathtt{succ}$ may also be defined.

Execution of (quantum) programs is described by the small-step call-by-value
operational semantics in Figures 10–10. If $m$ and $n$ are classical terms, we
write $m\xrightarrow{p}n$ to indicate that $m$ reduces to $n$ with probability
$p\in[0,1]$ in exactly one step. Note that the probabilistic behaviour of
reduction in the classical subsystem is induced by quantum measurements from
the quantum subsystem.

####  2.2.1. Quantum Configurations

Reduction for the quantum fragment is described, as usual, in terms of
_quantum configurations_ $[\lvert\psi\rangle,\ell,\mathbf{q}]$, which may be
seen as terms with embedded quantum information. We describe quantum
configurations following (Péchoux et al., 2020; Pagani et al., 2014). Given
$n\in\mathbb{N},$ we write
$\textnormal{{qbit}}^{n}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\textnormal{{qbit}}\otimes\cdots\otimes\textnormal{{qbit}}$ for
the $n$-fold tensor product of qbit.

###### Definition 2.2.3 (Quantum Configuration).

A _quantum configuration_ is a triple $[\lvert\psi\rangle,\ell,\mathbf{q}]$,
where: $\lvert\psi\rangle$ is a _pure quantum state_ , i.e., a normalised
vector in $\mathbb{C}^{2^{n}};$ $\mathbf{q}$ is a quantum term;
$\ell:\mathrm{QFV}(\mathbf{q})\to\\{1,\ldots,\dim(\lvert\psi\rangle)\\}$ is a
function from the set of free _quantum_ variables of $\mathbf{q}$ into the
indicated set, where
$\dim(\lvert\psi\rangle)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}n$ is _dimension_ of $\lvert\psi\rangle$. We refer to $\ell$ as
the _linking function_. A quantum configuration
$[\lvert\psi\rangle,\ell,\mathbf{q}]$ is _well-formed_ in classical context
$\Phi$ with type $\mathbf{A}$ and $k$ auxiliary qubits, which we write as
$\Phi\vdash[\lvert\psi\rangle,\ell,\mathbf{q}]:\mathbf{A};\textnormal{{qbit}}^{k},$
whenever the following conditions are satisfied:

  * •

$\Phi;\mathbf{x}_{1}:\textnormal{{qbit}},\ldots,\mathbf{x}_{m}:\textnormal{{qbit}}\vdash\mathbf{q}:\mathbf{A}$
is a well-formed quantum term.

  * •

$\dim(\lvert\psi\rangle)=m+k.$

  * •

The linking function
$\ell:\\{\mathbf{x}_{1},\ldots,\mathbf{x}_{m}\\}\to\\{1,\ldots,m+k\\}$ is
injective.

A configuration $[\lvert\psi\rangle,\ell,\mathbf{q}]$ is _total_ if
$\Phi\vdash[\lvert\psi\rangle,\ell,\mathbf{q}]:\mathbf{A};\textnormal{{qbit}}^{0}$,
which we abbreviate by
$\Phi\vdash[\lvert\psi\rangle,\ell,\mathbf{q}]:\mathbf{A}$. Thus, in a total
configuration $\ell$ defines a 1 - 1 correspondence between the qubits of
$\lvert\psi\rangle$ and the free quantum variables of $\mathbf{q}.$ A
configuration is _closed_ if
$\cdot\vdash[\lvert\psi\rangle,\ell,\mathbf{q}]:\mathbf{A};\textnormal{{qbit}}^{k}$,
for some $k\in\mathbb{N}.$

We are primarily interested in well-formed configurations that are both total
and closed. Nevertheless, the premises of the structural reduction rules in
the operational semantics include non-total configurations that have some
auxiliary qubits not used by the quantum term, so it is necessary also to
consider non-total configurations (see (Pagani et al., 2014; Péchoux et al.,
2020) for more details). Otherwise, the configurations in the premises would
not be typable, so it is necessary to allow auxiliary qubits as part of the
formation conditions. Likewise, the denotational semantics includes
configurations that are not closed, because the interpretation of closed terms
may be defined using non-closed terms (e.g. lambda abstractions).

The linking function $\ell$ in a configuration
$[\lvert\psi\rangle,\ell,\mathbf{q}]$ associates the free variables of
$\mathbf{q}$, each of type qbit, to specific qubits of the quantum state
$\lvert\psi\rangle$; $\ell$ is needed because some of the qubits in
$\lvert\psi\rangle$ may be entangled, in which case $\lvert\psi\rangle$ cannot
be broken down into smaller quantum states.

We use calligraphic letters $\mathcal{C},\mathcal{D}$ to range over quantum
configurations. Given quantum configurations $\mathcal{C}$ and $\mathcal{D}$
we write $\mathcal{C}\xrightarrow{p}\mathcal{D}$ to indicate that
$\mathcal{C}$ reduces to $\mathcal{D}$ with probability $p$ in exactly one
step. This is how we model the execution of quantum programs. A _value
configuration_ is a configuration
$\mathcal{V}=[\lvert\psi\rangle,\ell,\mathbf{v}]$, where $\mathbf{v}$ is a
quantum value. Reduction in the quantum subsystem terminates at value
configurations, just as reduction in the classical system terminates at
values.

####  2.2.2. The Subsystem FPC

We have organised the term formation rules and the associated reduction rules
into several subsystems, which we now describe. Figure 7 specifies the
formation rules for the classical terms that make up the subsystem FPC (which
is well-known (Fiore, 1994; Abadi and Fiore, 1996; Fiore and Plotkin, 1994)).
The notation $P[\mu X.P/X]$ represents type substitution, which is defined as
usual. The reduction rules for these terms are standard and are shown in
Figure 10.

####  2.2.3. The Subsystem QPL

Figure 7 describes the formation rules for the quantum terms that make up a
first-order linear subsystem with inductive types. These terms and their
reduction rules are all standard, but they are now described on quantum
configurations in Figure 10. For the structural reduction rules involving
quantum evaluation contexts, the notation $\ell\cap\ell_{0}=\varnothing$
indicates that the linking functions $\ell$ and $\ell_{0}$ have disjoint
domains and the notation
$\ell\mathbin{\mathchoice{\leavevmode\vtop{\halign{\hfil$\m@th\displaystyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\textstyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\scriptstyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\scriptscriptstyle#$\hfil\cr\cup\cr\cdot\crcr}}}}\ell_{0}$
indicates the disjoint union of the two linking functions. The terms from
Figure 7 do not directly modify the quantum state $\lvert\psi\rangle.$

Figure 7 lists the formation rules for the term constants that we use to
manipulate quantum information. Note that these constants are values of type
$Q(\mathbf{A},\mathbf{B})$ and therefore are classical/non-linear (and may be
used any number of times). The associated reduction rules for quantum function
application using these constants are presented in Figure 10. The term
$U(\mathbf{x_{1}\otimes\cdots\otimes x_{k})}$ applies the unitary operation
$U$ to the qubits identified by the variables $\mathbf{x_{1},\ldots,x_{k}}$
and modifies the quantum state in the configuration accordingly. The term
$\mathbf{new\ ff}$ (resp. $\mathbf{new\ tt}$) creates a new qubit in state
$\lvert 0\rangle$ (resp. $\lvert 1\rangle$), creates a fresh new qubit
variable that points to it and modifies the quantum configuration accordingly.
The term $\mathbf{meas\ \mathbf{y}}$ measures the qubit identified by variable
$\mathbf{y}$ and produces bit $\mathbf{tt}$ or $\mathbf{ff}$ with probability
given by the Born rule of quantum mechanics. This operation _irreversibly_
modifies the quantum state and causes a _probabilistic computational effect_.

The terms in Figures 7 and 7 can be thought of as jointly making up a
subsystem that we call $\mathtt{QPL}$ (it is roughly equivalent to
$\mathtt{QPL}$ in (Selinger, 2004a; Péchoux et al., 2020)), which is a first-
order language for quantum programming.

$\displaystyle\pi_{1}(v,w)\xrightarrow{1}v\qquad\pi_{2}(v,w)\xrightarrow{1}w\qquad\qquad\textnormal{\text{unfold}}\
\textnormal{\text{fold}}\ v\xrightarrow{1}v\qquad(\lambda
x.m)v\xrightarrow{1}m[v/x]$ $\displaystyle(\text{case}\ \emph{in}_{1}v\
\text{of}\ \emph{in}_{1}x\Rightarrow n_{1}\ |\ \emph{in}_{2}y\Rightarrow
n_{2})\xrightarrow{1}n_{1}[v/x]\qquad(\text{case}\ \emph{in}_{2}v\ \text{of}\
\emph{in}_{1}x\Rightarrow n_{1}\ |\ \emph{in}_{2}y\Rightarrow n_{2})$
$\displaystyle\xrightarrow{1}n_{2}[v/y]$
$\displaystyle\mathbf{[\lvert\psi\rangle,\ell,let\ x\otimes y=v\otimes w\ in\
r]}$
$\displaystyle\xrightarrow{1}\mathbf{[\lvert\psi\rangle,\ell,r[v/x,w/y]]}$
$\displaystyle\mathbf{[\lvert\psi\rangle,\ell,case\ in_{1}v\ of\
in_{1}x\Rightarrow r_{1}\ |\ in_{2}y\Rightarrow r_{2}]}$
$\displaystyle\xrightarrow{1}\mathbf{[\lvert\psi\rangle,\ell,r_{1}[v/x]]}$
$\displaystyle\mathbf{[\lvert\psi\rangle,\ell,case\ in_{2}v\ of\
in_{1}x\Rightarrow r_{1}\ |\ in_{2}y\Rightarrow r_{2}]}$
$\displaystyle\xrightarrow{1}\mathbf{[\lvert\psi\rangle,\ell,r_{2}[v/y]]}$
$\displaystyle[\lvert\psi\rangle,\ell,\mathbf{\textbf{unfold}\ \textbf{fold}\
v}]$ $\displaystyle\xrightarrow{1}[\lvert\psi\rangle,\ell,\mathbf{v}]$
$\displaystyle\mathbf{[\lvert\psi\rangle,\ell,*;r]}\xrightarrow{1}\mathbf{[\lvert\psi\rangle,\ell,r]}\qquad[\lvert\psi\rangle,\ell,\mathbf{let}\
x=\text{lift}\ \mathbf{v}\ \mathbf{in\ r}]$
$\displaystyle\xrightarrow{1}\mathbf{[\lvert\psi\rangle,\ell,r}[|\mathbf{v}|/x]]$

$E$

$\displaystyle::=\scalebox{0.98}{$[\cdot]\ |\ (E,m)\ |\ (v,E)\ |\ \pi_{i}E\ |\
\emph{in}_{i}E\ |\ (\text{case}\ E\ \text{of}\ \emph{in}_{1}x\Rightarrow
n_{1}\ |\ \emph{in}_{2}y\Rightarrow n_{2})\ |\ Em\ |\ vE\ |\ \text{(un)fold
}E\ $}$

$\mathbf{E}$

$\displaystyle::=\scalebox{0.98}{$[\cdot]\ |\ \mathbf{E}\otimes\mathbf{q}\ |\
\mathbf{v}\otimes\mathbf{E}\ |\ \mathbf{let\ x\otimes y=E\ in\ r}\ |\
\mathbf{in}_{i}\mathbf{E}\ |\ \mathbf{(case\ E\ of\ in_{1}x\Rightarrow r_{1}\
|\ in_{2}y\Rightarrow r_{2})}\ |\ \mathbf{E};\mathbf{q}\ |\ \textbf{(un)fold
}\mathbf{E}\ |\ $}$

$m\xrightarrow{p}m^{\prime}$ $E[m]\xrightarrow{p}E[m^{\prime}]$
$[\lvert\psi\rangle,\ell,\mathbf{q}]\xrightarrow{p}[\lvert\psi^{\prime}\rangle,\ell^{\prime},\mathbf{q}^{\prime}]$
$\ell\cap\ell_{0}=\varnothing=\ell^{\prime}\cap\ell_{0}$
$\left[\lvert\psi\rangle,\ell\mathbin{\mathchoice{\leavevmode\vtop{\halign{\hfil$\m@th\displaystyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\textstyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\scriptstyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\scriptscriptstyle#$\hfil\cr\cup\cr\cdot\crcr}}}}\ell_{0},\mathbf{E[q]}\right]\xrightarrow{p}\left[\lvert\psi^{\prime}\rangle,\ell^{\prime}\mathbin{\mathchoice{\leavevmode\vtop{\halign{\hfil$\m@th\displaystyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\textstyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\scriptstyle#$\hfil\cr\cup\cr\cdot\crcr}}}{\leavevmode\vtop{\halign{\hfil$\m@th\scriptscriptstyle#$\hfil\cr\cup\cr\cdot\crcr}}}}\ell_{0},\mathbf{E[q^{\prime}]}\right]$

Figure 8. Classical evaluation contexts $(E)$, quantum evaluation contexts
$(\mathbf{E})$ and associated reduction rules.

$\displaystyle[\lvert\psi\rangle,\ell,U(\mathbf{x_{1}\otimes\cdots\otimes
x_{k})}]\xrightarrow{1}[(\sigma\circ(U\otimes\mathrm{id})\circ\sigma^{-1})\lvert\psi\rangle,\ell,\mathbf{x}_{1}\otimes\cdots\otimes\mathbf{x}_{k}],$
$\displaystyle\qquad\text{ for any permutation $\sigma$, s.t.
}\sigma(i)=\ell(\mathbf{x}_{i}),1\leq i\leq k.$
$\displaystyle[\lvert\psi\rangle,\varnothing,\mathbf{new\
ff}]\xrightarrow{1}[\lvert\psi\rangle\otimes\lvert
0\rangle,\\{\mathbf{x}\mapsto\text{dim}(\lvert\psi\rangle)+1\\},\mathbf{x}]\quad[\lvert\psi\rangle,\varnothing,\mathbf{new\
tt}]\xrightarrow{1}[\lvert\psi\rangle\otimes\lvert
1\rangle,\\{\mathbf{x}\mapsto\text{dim}(\lvert\psi\rangle)+1\\},\mathbf{x}],$
where $\mathbf{x}$ is chosen fresh.
$\displaystyle\left[\alpha\left(\sum_{i}\alpha_{i}\lvert
b_{i}\rangle\otimes\lvert 0\rangle\otimes\lvert
b^{\prime}_{i}\rangle\right)+\beta\left(\sum_{i}\beta_{i}\lvert
b_{i}\rangle\otimes\lvert 1\rangle\otimes\lvert
b^{\prime}_{i}\rangle\right),\\{\mathbf{y}\mapsto j\\},\mathbf{meas\
\mathbf{y}}\right]\xrightarrow{|\alpha|^{2}}\left[\sum_{i}\alpha_{i}\lvert
b_{i}\rangle\otimes\lvert
b^{\prime}_{i}\rangle,\varnothing,\mathbf{ff}\right]$
$\displaystyle\left[\alpha\left(\sum_{i}\alpha_{i}\lvert
b_{i}\rangle\otimes\lvert 0\rangle\otimes\lvert
b^{\prime}_{i}\rangle\right)+\beta\left(\sum_{i}\beta_{i}\lvert
b_{i}\rangle\otimes\lvert 1\rangle\otimes\lvert
b^{\prime}_{i}\rangle\right),\\{\mathbf{y}\mapsto j\\},\mathbf{meas\
\mathbf{y}}\right]\xrightarrow{|\beta|^{2}}\left[\sum_{i}\beta_{i}\lvert
b_{i}\rangle\otimes\lvert
b^{\prime}_{i}\rangle,\varnothing,\mathbf{tt}\right],$ where dim$(\lvert
b_{i}\rangle)=j-1$, so that the $j$-th qubit is measured.

Figure 9. Rules for manipulating quantum information.

$\displaystyle[\lvert\psi\rangle,\ell,({\lambda}\mathbf{(x_{1},\ldots,x_{n}).q})(\mathbf{v_{1}\otimes\cdots\otimes
v_{n}})]$
$\displaystyle\xrightarrow{1}[\lvert\psi\rangle,\ell,\mathbf{q}[\mathbf{v_{1}/x_{1},\ldots,v_{n}/x_{n}}]]$
$\displaystyle\text{run
}[\lvert\psi\rangle,\varnothing,\mathbf{v}]\xrightarrow{1}|\mathbf{v}|\qquad\qquad$
$\displaystyle[\lvert\psi\rangle,\varnothing,\mathbf{init}\
|\mathbf{v}|]\xrightarrow{1}[\lvert\psi\rangle,\varnothing,\mathbf{v}]$

$m\xrightarrow{p}m^{\prime}\phantom{[}$
$\left[\lvert\psi\rangle,\ell,m\mathbf{q}\right]\xrightarrow{p}\left[\lvert\psi\rangle,\ell,m^{\prime}\mathbf{q}\right]$
$\left[\lvert\psi\rangle,\ell,\mathbf{q}\right]\xrightarrow{p}\left[\lvert\psi^{\prime}\rangle,\ell^{\prime},\mathbf{q}^{\prime}\right]$
$\left[\lvert\psi\rangle,\ell,v\mathbf{q}\right]\xrightarrow{p}\left[\lvert\psi^{\prime}\rangle,\ell^{\prime},v\mathbf{q}^{\prime}\right]$

$[\lvert\psi\rangle,\ell,\mathbf{q}]\xrightarrow{p}[\lvert\psi^{\prime}\rangle,\ell^{\prime},\mathbf{q}^{\prime}]$
$\text{run }[\lvert\psi\rangle,\ell,\mathbf{q}]\xrightarrow{p}\text{run
}[\lvert\psi^{\prime}\rangle,\ell^{\prime},\mathbf{q}^{\prime}]$
$m\xrightarrow{p}m^{\prime}$ $[\lvert\psi\rangle,\varnothing,\mathbf{init}\
m]\xrightarrow{p}[\lvert\psi\rangle,\varnothing,\mathbf{init}\ m^{\prime}]$

Figure 10. Rules for quantum function application and extracting observable
(quantum) information.

####  2.2.4. Mixed Classical/Quantum Terms

Both subsystems $\mathrm{(P)FPC}$ (Figure 7) and $\mathtt{QPL}$ have been
studied previously (for very different purposes). The main distinguishing
feature of $\mathtt{VQPL}$ is that it demonstrates how these subsystems can be
combined and used simultaneously for variational quantum programming. The
terms and formation rules that allow us to achieve this are presented in
Figure 7, and we now describe them in greater detail.

The term ${\lambda}\mathbf{(x_{1},\ldots,x_{n}).q}$ is a value which
represents a _first-order_ quantum lambda abstraction. Note that this value is
actually classical (non-linear). The term $m\mathbf{q}$ represents _quantum
function application_. In our view, this is the most interesting rule in
$\mathtt{VQPL}$. This is because its subterm $m:Q(\mathbf{A},\mathbf{B})$
represents a _probabilistic classical program_ that eventually reduces to a
quantum lambda abstraction. Because of this, the term $m\mathbf{q}$ combines
classical probabilistic computation with quantum computation (represented by
the subterm $\mathbf{q}$), and this is reflected in the associated reduction
rules in Figure 10. Providing a semantic interpretation of this term requires
considerable effort and the development of novel semantic methods, as we show
later.

The _observable_ quantum/classical values are simply quantum/classical values
of observable types with observable context. The closed observable quantum
values are in 1-1 correspondence with the closed observable classical values,
which is made precise by the assignment $|-|$ from Figure 7. Therefore $|-|$
may be seen as a translation, not only between the observable types, but also
between their closed values, and so we may think of them as carrying the same
information. In the sequel, we see that this view extends to our denotational
interpretation as well. Observable types and values are important, because
they play a special role in the terms we introduce next.

Given any configuration $\mathcal{C}$ of _observable_ type, the term
$``\text{run }\mathcal{C}"$ reduces the configuration $\mathcal{C}$ to some
value configuration $[\lvert\psi\rangle,\varnothing,\mathbf{v}]$, then
extracts the observable quantum value $\mathbf{v}$ from it and produces its
_classical counterpart_ $|\mathbf{v}|$ as the result of the overall
computation. Note that in this situation, the observable value $\mathbf{v}$
does not depend on the quantum data, because it necessarily has an empty
quantum context and thus empty linking function, and therefore the remaining
quantum state $\lvert\psi\rangle$ may be safely discarded (this is consistent
with affine approaches to quantum programming, see (Selinger, 2004a; Péchoux
et al., 2020; Clairambault et al., 2019)). The term $``\text{run
}\mathcal{C}"$ is classical, and it allows us to execute quantum algorithms on
a quantum computer and then extract the resulting _observable_ information
into our classical subsystem for further manipulation. The entire process is
probabilistic. It is convenient to introduce some syntactic sugar. Given a
closed quantum term $\cdot;\cdot\vdash\mathbf{q}:\mathbf{O}$ of observable
type, we can define $\text{run
}\mathbf{q}\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\text{run
}[1,\varnothing,\mathbf{q}]$. Users of the programming language are not
expected to write the more general terms $``\text{run }\mathcal{C}"$ (which
are useful for formalising the operational and denotational semantics), but
only the sugarised terms $``\text{run }\mathbf{q}"$. The term
$``\mathbf{init}\ m"$ performs the reverse function of that of "run", i.e.,
given a classical (probabilistic) process $m$ of observable type, the term
$``\mathbf{init}\ m"$ prepares observable quantum information as indicated by
the observable value that $m$ reduces to in the end.

Finally, the $``\mathbf{let}\ x=\text{lift}\ \mathbf{q}\ \mathbf{in\ r}"$ term
allows us to execute a quantum term $\mathbf{q}$ of observable type and then
promote the observable quantum information it produces to the classical world,
so that we may use it any number of times within the continuation $\mathbf{r}$
(see Figure 10). This term therefore implements what is often called "dynamic
lifting" in the quantum programming literature. From a structural perspective,
it is the only term that allows us to modify the non-linear context of quantum
terms and as such may be compared to the corresponding rules of the LNL
calculus (Benton, 1995; Benton and Wadler, 1996). In practice, this term is
useful for describing quantum processes where we measure a _part of_ our
quantum state and use the measurement outcome to influence the subsequent
quantum dynamics. It is necessary for protocols like quantum teleportation.

###  2.3. Type Safety

The next two propositions show $\mathtt{VQPL}$ is type-safe. The first
proposition shows type assignment is preserved by reduction, and as a
consequence, totality of quantum configurations also is preserved.

######  Proposition 2.3.4 (Type Preservation).

If $\Phi\vdash m\colon P$ and $m\xrightarrow{p}n,$ then $\Phi\vdash n\colon
P.$ Likewise, if $\Phi\vdash\mathcal{C}:\mathbf{A};\textnormal{{qbit}}^{k}$
and $\mathcal{C}\xrightarrow{p}\mathcal{D}$, then
$\Phi\vdash\mathcal{D}:\mathbf{A};\textnormal{{qbit}}^{k}.$ In both of these
situations, if $p<1$, then there exists a term $n^{\prime}$ (resp.
configuration $\mathcal{D}^{\prime}$), such that
$m\xrightarrow{1-p}n^{\prime}$ (resp.
$\mathcal{C}\xrightarrow{1-p}\mathcal{D}^{\prime}$).

######  Proposition 2.3.5 (Progress).

If $\cdot\vdash m\colon P$, then either $m$ is a value or there exists a
classical term $n,$ such that $m\xrightarrow{p}n$ for some $p\in(0,1]$.
Likewise, if $\cdot\vdash\mathcal{C}\colon\mathbf{A};\textnormal{{qbit}}^{k}$,
then either $\mathcal{C}$ is a value configuration or there exists a quantum
configuration $\mathcal{D},$ such that $\mathcal{C}\xrightarrow{p}\mathcal{D}$
for some $p\in(0,1]$.

######  Remark 2.3.6.

As usual, Progress holds for all _closed_ terms/configurations, whereas Type
Preservation holds for all well-formed terms/configurations, including the
_open_ ones. Here we note that the static semantics is independent of the
translation $|-|$ on values. This translation only matters for three rules in
our operational semantics and it is restricted to closed observable values (in
Figure 7), because otherwise Type Preservation would fail for _open_
terms/configurations.

###  2.4. Recursion and Asymptotic Behaviour of Reduction

It is well-known that type recursion induces term recursion in $\mathtt{FPC}$
(Fiore, 1994; Abadi and Fiore, 1996; Harper, 2016), and this also is true for
$\mathtt{VQPL}.$ The call-by-value fixpoint operator

$\cdot\vdash\mathtt{fix}_{P\to R}\colon\left(\left(P\to R\right)\to P\to
R\right)\to P\to R$

may be _derived_ at any function type $P\to R$ (see (Abadi and Fiore, 1996)
and (Fiore, 1994, §8) for more details). This fixpoint operator allows us to
write recursive functions.

The probability that a term $m$ reduces to a value $v$ (in any number of
steps) may be determined as in (Pagani et al., 2014). The _probability weight_
of a reduction path
$\pi=\left(m_{1}\xrightarrow{p_{1}}\cdots\xrightarrow{p_{n}}m_{n}\right)$ is
$P(\pi)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\prod_{i=1}^{n}p_{i}.$ The probability that $m$ reduces to the
value $v$ in _at most_ $n$ steps is

$P(m\xrightarrow{}_{\leq n}v)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sum_{\pi\in\mathrm{Paths}_{\leq n}(m,v)}P(\pi),$

where $\mathrm{Paths}_{\leq n}(m,v)$ is the set of all reduction paths from
$m$ to $v$ whose length is at most $n$. The probability that $m$ reduces to
the value $v$ in _any number_ of steps is
$P(m\xrightarrow{}_{*}v)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sup_{i}P(m\xrightarrow{}_{\leq i}v).$ Similarly, the probability
that a quantum configuration $\mathcal{C}$ reduces to a value configuration
$\mathcal{V}$ (in any number of steps) is denoted
$P(\mathcal{C}\xrightarrow{}_{*}\mathcal{V})$; it is determined in exactly the
same way as above by substituting the notion of term with that of
configuration. Finally, the overall probability that a term $m$ or
configuration $\mathcal{C}$ _terminates_ is given by:

(2.1) $\mathrm{Halt}(m)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sum_{v\in\mathrm{Val}(m)}P(m\xrightarrow{}_{*}v)\qquad\qquad\mathrm{Halt}(\mathcal{C})\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sum_{\mathcal{V}\in\mathrm{ValC}(\mathcal{C})}P(\mathcal{C}\xrightarrow{}_{*}\mathcal{V}),$

where $\mathrm{ValC}(\mathcal{C})\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\\{\mathcal{V}\ |\ \mathcal{V}\text{ is a value configuration and
}P(\mathcal{C}\xrightarrow{}_{*}\mathcal{V})>0\\}$ and
$\mathrm{Val}(m)\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\\{v\
|\ v$ is a value and $P(m\xrightarrow{}_{*}v)>0\\}$. Note that both sums may
be countably infinite.

###  2.5. Examples

We now illustrate $\mathtt{VQPL}$ with some example programs.

###### Example 2.5.7.

A fair coin toss can be defined by using some simple quantum resources:
$\text{coin}_{0.5}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\text{run}\ \left(\text{meas}(H(\text{new}\
\mathbf{ff}))\right):\mathtt{Bool},$ where $H$ represents the Hadamard unitary
operation. More generally, by replacing $H$ with a suitable unitary operation
$U_{p}$, a biased coin toss $\text{coin}_{p}$ may be defined for $p\in[0,1]$
with reduction behaviour $P(\text{coin}_{p}\xrightarrow{}_{*}\mathtt{ff})=p$
and $P(\text{coin}_{p}\xrightarrow{}_{*}\mathtt{tt})=1-p.$ Notice that
coin${}_{p}:\texttt{Bool}$ is a _classical term_. This shows that classical
discrete probabilistic choice is _derivable_ and therefore the language
$\mathtt{PFPC}$ (Jia et al., 2021) is a subsystem of $\mathtt{VQPL}.$

###### Example 2.5.8.

The fixpoint operator $\mathtt{fix}$ allows us to write classical recursive
functions (as usual), but it also enables us to write quantum recursive
functions. The function $\mathtt{Ts}$ below applies the unitary $T$ to each
qubit in a list. Defining, for brevity,
$\mathtt{Fqs}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}Q(\mathbf{List}(\textnormal{{qbit}}),\mathbf{List}(\textnormal{{qbit}}))$,
let:

$\mathtt{Ts^{\prime}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\left(\mathtt{fix}_{1\to\mathtt{Fqs}}\lambda
f^{1\to\mathtt{Fqs}}.\lambda x^{1}.\
{\lambda}(\mathbf{qs}).\mathbf{case}(\mathbf{qs})\ \mathbf{of}\
\mathbf{nil}\Rightarrow\mathbf{nil}\ |\ \mathbf{q::qs^{\prime}}\Rightarrow
T\mathbf{q}::(fx)\mathbf{qs^{\prime}}\right):1\to\mathtt{Fqs},$

where we used some (hopefully obvious) syntactic sugar for pattern matching of
(linear) lists. The recursive call is performed by the $fx$ expression, which
is of type $\mathtt{Fqs}.$ Setting
$\mathtt{Ts}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathtt{Ts^{\prime}}():Q(\mathbf{List}(\textnormal{{qbit}}),\mathbf{List}(\textnormal{{qbit}}))$,
we get the desired function. An example quantum execution is given by
$P\left([\lvert
111\rangle,\ell,\mathtt{Ts}(\mathbf{x}_{1}::\mathbf{x}_{2}::\mathbf{x}_{3}::\mathbf{nil})]\xrightarrow{}_{*}[(T\otimes
T\otimes T)\lvert
111\rangle,\ell,\mathbf{x}_{1}::\mathbf{x}_{2}::\mathbf{x}_{3}::\mathbf{nil}]\right)=1,$
where $\ell$ is the linking function defined by $\ell(\mathbf{x}_{i})=i$. This
shows that classical recursion _induces_ recursion on the quantum subsystem
and therefore a quantum fixpoint operator is obviously derivable.

##  3\. Probabilistic Effects and (Commutative) Valuations Monads

As we already explained, $\mathtt{PFPC}$ is a subsystem of our language. In
this section we recall the construction of the commutative monad
$\mathcal{M}:\mathbf{DCPO}\to\mathbf{DCPO}$ of (Jia et al., 2021), which we
also use in our denotational semantics. Our classical judgements are
interpreted in the Kleisli category $\mathbf{DCPO}_{\mathcal{M}}$ of
$\mathcal{M}$, which provides a sound and (strongly) adequate model of
$\mathtt{PFPC}$ (Jia et al., 2021).

###  3.1. Domain-theoretic and Topological Preliminaries

If $D$ is a partially ordered set (_poset_), a nonempty subset $A$ of $D$ is
called _directed_ if each pair of elements in $A$ has an upper bound in $A$.
Then $D$ is a _directed complete poset_ (_dcpo_ , for short) if each of its
directed subsets has a supremum. For example, the unit interval $[0,1]$ is a
dcpo in the usual ordering. A _Scott-continuous map_ $f\colon D\to E$ between
(posets) dcpo’s is a function that is monotone and preserves (existing)
suprema of directed subsets. _Pointed posets_ have least elements, usually
denoted by $\bot_{D}$ if $D$ is the ambient poset. A Scott-continuous function
$f\colon D\to E$ between pointed dcpo’s is _strict_ if $f$ preserves the least
element, that is, $f(\bot_{D})=\bot_{E}$.

The category $\mathbf{DCPO}$ of dcpo’s and Scott-continuous functions is
complete, cocomplete and Cartesian closed (Abramsky and Jung, 1994). The
categorical (co)product of the dcpo’s $A_{1}$ and $A_{2}$ is denoted
$A_{1}\times A_{2}$ ($A_{1}$ \+ $A_{2}$), with $\pi_{1},\pi_{2}$
($\emph{in}_{1},\emph{in}_{2}$) the associated (co)projections. Initial and
terminal objects of $\mathbf{DCPO}$ are denoted by $\varnothing$ and $1$,
which are the empty dcpo and the singleton dcpo, respectively. For dcpo’s $A$
and $B$, the internal hom of $A$ and $B$ in $\mathbf{DCPO}$ is $[A\to B]$, the
space of all Scott-continuous functions $f:A\to B$ ordered pointwise.

The category $\mathbf{DCPO}_{\perp!}$ of _pointed_ dcpo’s and _strict_ Scott-
continuous functions is symmetric monoidal closed when equipped with the smash
product and strict Scott-continuous function space, and it also is complete
and cocomplete (Abramsky and Jung, 1994).

The _Scott topology_ $\sigma D$ on a dcpo $D$ consists of the upper subsets
$U={\uparrow\,}U\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\\{x\in D\mid(\exists u\in U)\,u\leq x\\}$ that are _inaccessible
by directed suprema:_ i.e., if $A\subseteq D$ is directed and $\sup A\in U$,
then $A\cap U\not=\emptyset$. The topological space $(D,\sigma D)$ is also
written as $\Sigma D$. Scott-continuous functions between dcpo’s $D$ and $E$
are exactly the continuous functions between $\Sigma D$ and $\Sigma E$ (Gierz
et al., 2003, Proposition II-2.1). We always equip $[0,1]$ with the Scott
topology unless stated otherwise.

If $B\subseteq D$ and $D$ is a dcpo, then $B$ is a _sub-dcpo_ if every
directed subset $A\subseteq B$ satisfies $\sup_{D}A\in B$, where $\sup_{D}A$
denotes the supremum of $A$ in $D$. In this case, $B$ is a dcpo in the induced
order from $D$ and $\sup_{D}A=\sup_{B}A$ for each directed subset $A$ of $B$.

###  3.2. The Monad $\mathcal{M}$

If $X$ is a topological space, then the open set lattice $\mathcal{O}X$ is a
complete lattice in the inclusion order, hence a dcpo. A _subprobability
valuation_ on $X$ is a Scott-continuous function
$\nu\colon\mathcal{O}X\to[0,1]$ that is strict ($\nu(\emptyset)=0$) and
modular $(\nu(U)+\nu(V)=\nu(U\cup V)+\nu(U\cap V))$. The set $\mathcal{V}X$ of
subprobability valuations on $X$ is a dcpo in the _stochastic order_ defined
by: $\nu_{1}\leq\nu_{2}$ if and only if $\nu_{1}(U)\leq\nu_{2}(U)$ for all
$U\in\mathcal{O}X$, for $\nu_{1},\nu_{2}\in\mathcal{V}X$, and the supremum of
a directed family of valuations $\\{\nu_{i}\\}_{i\in I}$ is computed
pointwise: $(\sup_{i\in
I}\nu_{i})(U)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sup_{i\in I}\nu_{i}(U)$, for all $U\in\mathcal{O}X$. The least
element of $\mathcal{V}X$ is the constantly zero valuation ${\mathbf{0}}_{X}$.
The dcpo $\mathcal{V}X$ also enjoys a convex structure: if
$\nu_{i}\in\mathcal{V}X$ and $r_{i}\geq 0$ for $i=1,\ldots,n$ and
$\sum_{i=1}^{n}r_{i}\leq 1$, then the convex sum $\sum_{i=1}^{n}r_{i}\nu_{i}$,
defined by
$(\sum_{i=1}^{n}r_{i}\nu_{i})(U)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sum_{i=1}^{n}r_{i}\nu_{i}(U)$ for $U\in\mathcal{O}X$, also is in
$\mathcal{V}X$.

The _Dirac valuations_ $\delta_{x}$, for $x\in X$, are defined by
$\delta_{x}(U)=1$ if $x\in U$ and $\delta_{x}(U)=0$ otherwise. These are
canonical examples of subprobability valuations, as are their convex sums,
which we call _simple valuations_ : they have form
$\sum_{i=1}^{n}r_{i}\delta_{x_{i}}$, where $x_{i}\in X$, $r_{i}\geq 0$, and
$\sum_{i=1}^{n}r_{i}\leq 1$. The simple valuations are denoted $\mathcal{S}X$,
and $\mathcal{S}X\subseteq\mathcal{V}X$, but $\mathcal{S}X$ is not a dcpo in
general.

If $f\colon X\to[0,1]$ is a continuous function and $\nu\in\mathcal{V}X$, the
_integral of $f$ against $\nu$_ is given by the Choquet formula

$\int_{x\in X}f(x)d\nu\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\int_{0}^{1}\nu(f^{-1}((t,1]))dt,$

where the right side is a Riemann integral of the bounded antitone function
$t\mapsto\nu(f^{-1}((t,1]))$. Since $f$ is continuous, and
$(t,1]\subseteq[0,1]$ is Scott open for each $t\in[0,1]$, $f^{-1}((t,1])$ is
open in $X$, so $\nu(f^{-1}((t,1]))$ is well defined. Thus the integral makes
sense. If no confusion can occur, we simply write $\int_{x\in X}f(x)d\nu$ as
$\int fd\nu$. Note that if $f\colon X\to[0,1]$ is fixed, then the map
$\nu\mapsto\int fd\nu\colon\mathcal{V}X\to[0,1]$ is Scott-continuous. Other
basic properties of this integral can be found in (Jones, 1990).

If $D$ is a dcpo, then
$\mathcal{V}D\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{V}\Sigma D=\mathcal{V}(D,\sigma(D))$ is well-defined, and
(Jones, 1990) proved that $\mathcal{V}$ extends to a monad on $\mathbf{DCPO}$.

####  3.2.1. Monad Structure

The _unit_ of $\mathcal{V}$ at $D$ is $\eta^{\mathcal{V}}_{D}\colon
D\to\mathcal{V}D::x\mapsto\delta_{x}$. The _Kleisli extension_ $f^{\dagger}$
of a Scott-continuous map $f\colon D\to\mathcal{V}E$ maps $\nu\in\mathcal{V}D$
to $f^{\dagger}(\nu)\in\mathcal{V}E$, where for $U\in\sigma E$,
$f^{\dagger}(\nu)(U)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\int_{x\in D}f(x)(U)d\nu.$ The _multiplication_
$\mu^{\mathcal{V}}_{D}\colon\mathcal{V}\mathcal{V}D\to\mathcal{V}D$ is given
by $\mu\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathrm{id}_{\mathcal{V}D}^{\dagger}$. Thus, $\mathcal{V}$ defines
an endofunctor on $\mathbf{DCPO}$ that sends a dcpo $D$ to $\mathcal{V}D$, and
a Scott-continuous map $h\colon D\to E$ to
$\mathcal{V}(h)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}(\eta_{E}\circ h)^{\dagger}$, so
$\mathcal{V}(h)(\nu)(U)=\nu(h^{-1}(U))$ for $\nu\in\mathcal{V}D$ and
$U\in\sigma E$. The valuation $h_{*}(\nu)=\mathcal{V}(h)(\nu)$ is called the
_push forward of $\nu$ by $h$_.

In fact, $\mathcal{V}$ defines a strong monad on $\mathbf{DCPO}$ (Jones,
1990): the strength at $(D,E)$ is

$\tau^{\mathcal{V}}_{DE}\colon D\times\mathcal{V}E\to\mathcal{V}(D\times
E)::(x,\nu)\mapsto\lambda U.\int_{y\in E}\chi_{U}(x,y)d\nu,$

where $\chi_{U}$ is the characteristic function of $U\in\sigma(D\times E)$.
However, it is unknown whether $\mathcal{V}$ is a commutative monad on
$\mathbf{DCPO}$. This is equivalent to showing the Fubini-style equation

(3.1) $\int_{x\in D}\int_{y\in E}\chi_{U}(x,y)d\xi d\nu=\int_{y\in
E}\int_{x\in D}\chi_{U}(x,y)d\nu d\xi,$

holds for dcpo’s $D$ and $E$, where $U\in\sigma(D\times E)$ and
$\nu\in\mathcal{V}D,\xi\in\mathcal{V}E$ (Jones and Plotkin, 1989). To address
this problem, the authors of (Jia et al., 2021) define a subclass of
valuations that simultaneously validates (3.1), contains all simple
valuations, and forms a dcpo in the stochastic order. They prove their
construction defines a commutative valuations monad $\mathcal{M}$ on
$\mathbf{DCPO}$. We devote the rest of this subsection to describing their
construction; for more details, see (Jia et al., 2021).

###### Definition 3.2.1.

For a dcpo $D$, $\mathcal{M}D$ is the intersection of all sub-dcpo’s of
$\mathcal{V}D$ containing $\mathcal{S}D$.

We call the valuations in $\mathcal{M}D$ the _$\mathcal{M}$ -valuations_ on
$D$. In fact, $\mathcal{M}D$ is the smallest sub-dcpo of $\mathcal{V}D$
containing $\mathcal{S}D$. It follows that the $\mathcal{M}$-valuations on $D$
consist of the simple valuations on $D$, directed suprema of simple valuations
on $D$, directed suprema of directed suprema of simple valuations on $D$ and
so forth, transfinitely. It is straightforward to show that (3.1) holds when
$\xi$ and $\nu$ are simple valuations, and because the nested integral
operations are Scott-continuous in the valuations components, it follows (3.1)
holds for $\mathcal{M}$-valuations. This is the idea behind the proof of the
following theorem.

######  Theorem 3.2.2 ((Jia et al., 2021, Theorem 8)).

$\mathcal{M}$ has the structure of a _commutative_ monad on $\mathbf{DCPO}$
when equipped with the (co)restricted monad operations of $\mathcal{V}$.

Since the inclusions $\mathcal{M}D\subseteq\mathcal{V}D$ form a strong map of
monads, we are justified in viewing $\mathcal{M}$ as a submonad of
$\mathcal{V}$ and we use the same notation for the monad operations of
$\mathcal{M}$ and $\mathcal{V}$.

##  4\. Quantum Effects and Hereditarily Atomic von Neumann Algebras

We now turn our attention to the model for the quantum subsystem of
$\mathtt{VQPL}$. We begin with a short review of operator algebras, which can
be used to study quantum foundations. The standard references are (Blackadar,
2006), (Takesaki, 2000) and (Kadison and Ringrose, 1997). For quantum
computing, it is sufficient to consider a special class of operator algebras
that is known as the _hereditarily atomic von Neumann algebras_. This class
consists of (possibly infinite) products of finite-dimensional matrix
algebras. These algebras were studied in (Kornell, 2020), where it is shown
that the dual category has a concrete description as _quantum sets_. Our main
result in this section is to prove that the category of hereditarily atomic
von Neumann algebras is enriched over continuous domains (§4.3), which is
crucial for providing a semantic interpretation of the "$m\mathbf{q}$" term.

###  4.1. Definition of von Neumann algebras

If $H$ is a Hilbert space, any linear map $x:H\to H$ is called an _operator_ ,
and $x$ is _bounded_ if it is continuous with respect to the norm $\|\cdot\|$
induced by the inner product $\langle\cdot,\cdot\rangle$ on $H$. The space
$B(H)$ of all bounded operators on $H$ forms an algebra over $\mathbb{C}$ with
composition as multiplication. Moreover, $B(H)$ has an _involution_ $x\mapsto
x^{*}$, where $x^{*}$ is the unique bounded operator satisfying $\langle
x^{*}k,h\rangle=\langle k,xh\rangle$ for $h,k\in H$. A subalgebra $A\subseteq
B(H)$ that is closed under the involution is called a _$*$ -subalgebra_. If,
in addition, $xy=yx$ for each $x,y\in A$, we call $A$ _commutative_. The
_commutant_ of a subset $S\subseteq B(H)$ is $S^{\prime}=\\{y\in B(H)\mid
xy=yx\ (\forall x\in S)\\}$.

###### Definition 4.1.1.

Let $H$ be a Hilbert space. A _von Neumann algebra_ on $H$ is a $*$-subalgebra
$M$ of $B(H)$ such that $M^{\prime\prime}=M$. If $K$ is another Hilbert space,
and $N$ is a von Neumann algebra on $K$, a linear map $\varphi:M\to N$ that
preserves the multiplication and the involution is a _$*$ -homomorphism_. If,
in addition, $\varphi$ is bijective, it is a $*$-isomorphism.

The commutant of any non-empty set in $B(H)$ always contains $1_{H}$, so
$1_{H}\in M$ for any von Neumann algebra $M\subseteq B(H)$. We sometimes write
$1_{H}$ as $1_{M}$ to emphasize it is the unit of $M$.

###### Example 4.1.2.

$B(H)$ itself is a von Neumann algebra, and if $H$ is $n$-dimensional, then
$B(H)$ is $*$-isomorphic to $\mathrm{M}_{n}(\mathbb{C})$, the algebra of
$n\times n$-complex valued matrices. This example plays an important role in
the definition of hereditarily atomic von Neumann algebras below.

###### Example 4.1.3.

If $X$ is a set, then $\ell^{2}(X)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\\{f:X\to\mathbb{C}\mid\sum_{x\in X}|f(x)|^{2}<\infty\\}$ is a
Hilbert space with inner product $\langle
f,g\rangle\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\sum_{x\in
X}\overline{f(x)}g(x)$. The space
$\ell^{\infty}(X)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\\{f:X\to\mathbb{C}\mid\sup_{x\in X}|f(x)|<\infty\\}$ equipped
with the norm $\|f\|\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sup_{x\in X}|f(x)|$ can be embedded isometrically into
$B(\ell^{2}(X))$ via the maps $f\mapsto m_{f}$, where
$m_{f}:\ell^{2}(X)\to\ell^{2}(X)$ is the left multiplication $g\mapsto fg$
(Landsman, 2017, Proposition B.73). Thus, identifying $\ell^{\infty}(X)$ with
its image in $B(\ell^{2}(X))$ shows it is a commutative von Neumann algebra on
$\ell^{2}(X)$ (Landsman, 2017, Proposition B.108).

Given Hilbert spaces $(H_{\alpha})_{\alpha\in\mathrm{A}}$, the sum
$\bigoplus_{\alpha\in\mathrm{A}}H_{\alpha}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\\{(h_{\alpha})_{\alpha\in\mathrm{A}}\in\prod_{\alpha\in\mathrm{A}}H_{\alpha}\mid\sum_{\alpha\in\mathrm{A}}\|h_{\alpha}\|^{2}<\infty\\}$
is a Hilbert space with inner product $\langle
k,h\rangle\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sum_{\alpha\in\mathrm{A}}\langle k_{\alpha},h_{\alpha}\rangle$
for $k=(k_{\alpha})_{\alpha\in\mathrm{A}}$ and
$h=(h_{\alpha})_{\alpha\in\mathrm{A}}$.

######  Proposition 4.1.4.

(Takesaki, 2000, Proposition II.3.3) Let $M_{\alpha}$ be a von Neumann algebra
on a Hilbert space $H_{\alpha}$ for each $\alpha\in A$. Then
$\prod_{\alpha\in\mathrm{A}}M_{\alpha}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\\{(x_{\alpha})_{\alpha\in\mathrm{A}}\mid\sup_{\alpha\in\mathrm{A}}\|x_{\alpha}\|<\infty\\}$
is a von Neumann algebra on $H\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\bigoplus_{\alpha\in\mathrm{A}}H_{\alpha}$, where
$xh\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}(x_{\alpha}h_{\alpha})_{\alpha\in\mathrm{A}}\in H$ for
$x=(x_{\alpha})_{\alpha\in\mathrm{A}}\in\prod_{\alpha\in\mathrm{A}}M_{\alpha}$
and $h=(h_{\alpha})_{\alpha\in\mathrm{A}}\in H$.

###### Definition 4.1.5.

We call a von Neumann algebra $M$ _hereditarily atomic_ , or simply an _HA-
algebra_ , if $M$ is isomorphic to $\prod_{\alpha\in\mathrm{A}}M_{\alpha}$,
where each $M_{\alpha}$ is $*$-isomorphic to some matrix algebra.

In order to make the correspondence between HA-algebras and the types of our
language clearer, we overload notation and often write $\bigoplus_{\alpha\in
A}M_{\alpha}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\prod_{\alpha\in\mathrm{A}}M_{\alpha}.$

###### Example 4.1.6.

All of the following are HA-algebras and we indicate to which type they
correspond. The complex numbers $\mathbb{C}$ correspond to type $\mathbf{I}$;
the algebra $\mathrm{M}_{2}(\mathbb{C})$ corresponds to type qbit; the algebra
$\bigoplus_{n\in\mathbb{N}}\mathbb{C}$ corresponds to type
$\mathbf{QNat}\equiv\mu\mathbf{X}.\mathbf{I}\oplus\mathbf{X}$; the algebra
$\bigoplus_{n\in\mathbb{N}}\mathrm{M}_{2^{n}}(\mathbb{C})$ corresponds to type
$\mathbf{List}(\textnormal{{qbit}})\equiv\mathbf{\mu
X.I\oplus(\textnormal{{qbit}}\otimes X)}.$ Moreover, if $X$ is a set, then
$\ell^{\infty}(X)\cong\bigoplus_{x\in X}\mathbb{C}$ is an HA-algebra and we
will see it corresponds to _observable_ quantum types, in general.

###  4.2. Quantum Computation with Hereditarily Atomic von Neumann Algebras

In this subsection, we define the appropriate notion of morphism that is
computationally relevant.

If $M$ is a von Neumann algebra on a Hilbert space $H$, we say $x\in M$ is
_self adjoint_ if $x^{*}=x$, and _positive_ if $x=y^{*}y$ for some $y\in M$;
equivalently $\langle h,xh\rangle\geq 0$ for each $h\in H$ (Kadison and
Ringrose, 1997). Given self-adjoint elements $x$ and $y$ in $M$, we write
$x\leq y$ iff $y-x$ is positive. The relation $\leq$ is a partial order on the
set $M_{\mathrm{sa}}$ of self-adjoint elements in $M$ under which
$M_{\mathrm{sa}}$ is _bounded directed complete:_ if $A$ is directed and
$\alpha\mapsto x_{\alpha}\in M_{\mathrm{sa}}$ is a monotone ascending net that
is bounded (i.e., $x_{\alpha}\leq y\in
M_{\mathrm{sa}}\forall\alpha\in\mathrm{A}$), then $(x_{\alpha})_{\alpha\in A}$
has a supremum $\sup_{\alpha\in\mathrm{A}}x_{\alpha}=x\in M_{\mathrm{sa}}$.
The partial order $\leq$ is often called the _Löwner order_.

In fact, $x$ is the limit of $(x_{\alpha})$ in the _strong operator topology_
on $M$: i.e., $\lim_{\alpha\in\mathrm{A}}x_{\alpha}h=xh$ for each $h\in H$;
this also implies convergence with respect to the _weak operator topology_ on
$M$, i.e., $\lim_{\alpha\in\mathrm{A}}\langle k,x_{\alpha}h\rangle=\langle
k,xh\rangle$ for each $h,k\in H$ (Blackadar, 2006, Proposition I.3.2.5 &
Corollary I.3.2.6). As a consequence, the _unit interval of $M$_,
$[0,1]_{M}=\\{x\in M_{\mathrm{sa}}\mid 0\leq x\leq 1_{M}\\}$ is a dcpo.

A linear function $\varphi:M\to N$ between von Neumann algebras is _unital_ if
$\varphi(1_{M})=1_{N}$, _subunital_ if $\varphi(1_{M})\leq 1_{N}$; $\varphi$
is _positive_ if it preserves positive elements, equivalently, if $\varphi$ is
monotone with respect to $\leq$. A positive and subunital $\varphi\colon M\to
N$ restricts to a monotone map $[0,1]_{M}\to[0,1]_{N}$, which by linearity
completely determines $\varphi$. We call $\varphi$ _normal_ if it preserves
the suprema of bounded increasing nets, i.e., if it is Scott continuous with
respect to $\leq$.

We denote by $\mathrm{M}_{n}(M)$ the von Neumann algebra of all $n\times
n$-matrices with entries in $M$. Any linear map $\varphi:M\to N$ between von
Neumann algebras induces a linear map
$\varphi^{(n)}:\mathrm{M}_{n}(M)\to\mathrm{M}_{n}(N)$ obtained by applying
$\varphi$ entrywise. We say that $\varphi$ is _completely positive_ if
$\varphi^{(n)}$ is positive for each $n\in\mathbb{N}$. In particular, any
completely positive map is positive. Finally, we say that a linear map
$\varphi:M\to N$ is an _NCPSU_ map, if $\varphi$ is normal completely positive
and subunital. We note that every normal unital $*$-homomorphism is an NCPSU
map, but the converse is not true, in general.

###### Definition 4.2.7.

We denote the category of von Neumann algebras and NCPSU maps by
$\mathbf{vN}$. Its full-on-objects subcategory having normal unital
$*$-homomorphisms as morphisms is denoted by $\mathbf{vN}_{*}$. The category
of HA-algebras and NCPSU maps is denoted by $\mathbf{HA}$ and we denote the
full-on-objects subcategory of $\mathbf{HA}$ with normal unital
$*$-homomorphisms by $\mathbf{HA}_{*}$. The categories relevant for our
semantics are their formal duals given by
$\mathbf{Q}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}(\mathbf{HA})^{\mathrm{op}}$ and
$\mathbf{Q}_{*}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}(\mathbf{HA}_{*})^{\mathrm{op}}$.

######  Remark 4.2.8.

When working with von Neumann algebras, it is customary to adopt the
Heisenberg picture of quantum mechanics, rather than the Schrödinger one. This
corresponds to working in the category $\mathbf{Q}$ which is the formal dual
of $\mathbf{HA}.$ In fact, the program of non-commutative geometry is based on
dualities between categories of operator algebras and “formal dual”
categories. Furthermore, this approach is also established in quantum
programming semantics (Péchoux et al., 2020; Cho and Westerbaan, 2016) and
necessary for the appropriate categorical structure (§6.2).

From now on, all $*$-homomorphisms we work with are implicitly assumed to be
unital and normal. We interpret quantum values in $\mathbf{Q}_{*}$ and quantum
terms in $\mathbf{Q}$. Next, we describe maps between HA-algebras that are
crucial for quantum computation and that we use in our semantics.

$\begin{array}[]{l|l|l|l}\mathrm{tr}:\mathrm{M}_{n}(\mathbb{C})\to\mathbb{C}&\
\mathrm{state}_{\rho}:\mathbb{C}\to\mathrm{M}_{2^{n}}(\mathbb{C})&\
\mathrm{meas}:\mathrm{M}_{2}(\mathbb{C})\to\mathbb{C}\oplus\mathbb{C}&\
\mathrm{unitary}_{U}:\mathrm{M}_{2^{n}}(\mathbb{C})\to\mathrm{M}_{2^{n}}(\mathbb{C})\\\
\mathrm{tr}::x\mapsto\sum_{i}x_{i,i}&\
\mathrm{state}_{\rho}::\alpha\mapsto\alpha\rho&\
\mathrm{meas}::\begin{pmatrix}\alpha&\beta\\\
\gamma&\delta\end{pmatrix}\mapsto\begin{pmatrix}\alpha&\delta\end{pmatrix}&\
\mathrm{unitary}_{U}::x\mapsto UxU^{*}\\\
\mathrm{tr}^{*}:\mathbb{C}\to\mathrm{M}_{n}(\mathbb{C})&\
\mathrm{state}_{\rho}^{*}:\mathrm{M}_{2^{n}}(\mathbb{C})\to\mathbb{C}&\
\mathrm{meas}^{*}:\mathbb{C}\oplus\mathbb{C}\to\mathrm{M}_{2}(\mathbb{C})&\
\mathrm{unitary}^{*}_{U}:\mathrm{M}_{2^{n}}(\mathbb{C})\to\mathrm{M}_{2^{n}}(\mathbb{C})\\\
\mathrm{tr}^{*}::\alpha\mapsto\alpha 1_{\mathrm{M}_{n}(\mathbb{C})}&\
\mathrm{state}_{\rho}^{*}::x\mapsto\mathrm{tr}(x\rho)&\
\mathrm{meas}^{*}::\begin{pmatrix}\alpha&\delta\end{pmatrix}\mapsto\begin{pmatrix}\alpha&0\\\
0&\delta\end{pmatrix}&\ \mathrm{unitary}_{U}^{*}::x\mapsto U^{*}xU\end{array}$

Figure 11. Maps in the Schrödinger picture $(\varphi\colon M\to N)$ and their
Hermitian adjoints $(\varphi^{*}\colon N\to M)$.

The maps in the upper half of Figure 11 describe NCPSU maps between HA-
algebras that are well-known in the quantum computing literature. The map
"$\mathrm{tr}$" computes the trace of a matrix; the map
"$\mathrm{state}_{\rho}$" prepares a new (mixed) quantum state that is
described by the density matrix $\rho$; the map "$\mathrm{meas}$" performs a
destructive quantum measurement on a qubit and returns a bit as outcome; the
map "$\mathrm{unitary}_{U}$" applies the unitary matrix $U$ of arity $n$ to an
$n$-dimensional quantum state. These are the appropriate maps to take in the
Schrödinger picture of quantum mechanics, but as explained above, the
Heisenberg picture is more appropriate for our denotational semantics, so it
is the Hermitian adjoints of these maps (bottom half of Figure 11) that are
relevant to us. By writing
$\varphi^{\ddagger}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}(\varphi^{*})^{\mathrm{op}}$ for
$\varphi\in\\{\mathrm{tr},\mathrm{state}_{\rho},\mathrm{meas},\mathrm{unitary}_{U}\\}$,
these maps are then morphisms of $\mathbf{Q}.$ In particular,
$\mathrm{meas}^{\ddagger}:\mathrm{M}_{2}(\mathbb{C})\to\mathbb{C}\oplus\mathbb{C}$
is the morphism of $\mathbf{Q}$ which represents quantum measurement.

We also define a morphism
$\mathrm{new}^{\ddagger}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathrm{meas}^{\mathrm{op}}\in\mathbf{Q}(\mathbb{C}\oplus\mathbb{C},\mathrm{M}_{2}(\mathbb{C}))$.
The way to think of this map (in $\mathbf{Q}$) is that given a bit
$i\in\\{0,1\\}$, the map would prepare the density matrix $\lvert
i\rangle\langle i\rvert$. Indeed, notice that (in $\mathbf{Q}$) we have
$\mathrm{meas}^{\ddagger}\circ\mathrm{new}^{\ddagger}=(\mathrm{meas}\circ\mathrm{meas}^{*})^{\mathrm{op}}=\mathrm{id}_{\mathbb{C}\oplus\mathbb{C}}$,
as expected.

###  4.3. Continuous Domain Enrichment of $\mathbf{Q}$

The category $\mathbf{vN}$ is enriched over $\mathbf{DCPO}_{\perp!}$ (Cho,
2016), where $\varphi\leq\psi$ iff $\psi-\varphi$ is completely positive, for
$\varphi,\psi\in\mathbf{vN}(M,N)$. The $\mathbf{DCPO}_{\perp!}$-enrichment of
$\mathbf{vN}$ immediately implies that of $\mathbf{HA}$ and $\mathbf{Q}$.

While $\mathbf{DCPO}_{\perp!}$-enrichment is important, it is insufficient for
our purposes. In particular, the crucial connection between the semantics of
the quantum and classical probabilistic effects in our language requires
$\mathbf{Q}(A,B)$ to be an $\mathcal{M}$-algebra for $A,B$ objects of
$\mathbf{Q}$ (Theorem 5.3.10). We can show this is the case when $\mathbf{Q}$
is enriched in a much stronger sense, namely, when $\mathbf{Q}$ is enriched
over continuous dcpo’s (see Theorem 5.3.8). Explaining all this is our next
goal.

We begin with continuous dcpo’s. For $x,y$ in a dcpo $D$, $x$ is _way-below_
$y$ (in symbols, $x\ll y$) if and only if for every directed set $A$ with
$y\leq\sup A$, there is some $a\in A$ such that $x\leq a$. A dcpo $D$ is
_continuous_ , or simply a _domain_ , if every element $x\in D$ is the
supremum of a directed set of elements that are way-below $x$. We use
$\mathbf{DOM}$ to denote the category of domains and Scott-continuous maps.

It was noted in (Selinger, 2004b, Example 2.7) that the unit interval of
$\mathrm{M}({\mathbb{C}}^{n})$ is a continuous dcpo, from which it is easy to
show $[0,1]_{A}$ is a domain for every HA-algebra $A$; in fact, this is an if-
and-only-if (Furber, 2019). We conclude this section with a much stronger
result.

######  Theorem 4.3.9.

The category $\mathbf{Q}$ is enriched over $\mathbf{DOM}.$

###### Proof.

The proof (Appendix A) starts with the fact that $[0,1]_{A}$ is a domain for
each HA-algebra $A$ and then makes extensive use of the representation theory
of von Neumann algebras. ∎

##  5\. Probabilistic Effects, Quantum Effects and Kegelspitzen

Our language shows that quantum effects induce probabilistic effects on the
classical side (via the "run" term) and, vice-versa, probabilistic effects on
the classical side can also influence the quantum dynamics (via the "init" and
"$m\textbf{q}$" terms). In this section, we describe the mathematical
structure we use to interpret this correspondence.

In particular, we show there is a strong relationship between the Kleisli
category $\mathbf{DCPO}_{\mathcal{M}}$ of $\mathcal{M}$ (where we interpret
classical programs) and our category $\mathbf{Q}$ of hereditarily atomic von
Neumann algebras (where we interpret quantum programs). The link between the
two categories is provided by the theory of (continuous) Kegelspitzen (Keimel
and Plotkin, 2017). The relationship we identify is crucial for the
interpretation of the mixed classical/quantum judgements of Figure 7, and it
links the classical theory of valuations monads to the quantum theory of von
Neumann algebras.

###  5.1. (Continuous) Kegelspitzen

We begin by recalling the definition of Kegelspitzen (Keimel and Plotkin,
2017).

###### Definition 5.1.1.

A Kegelspitze is a dcpo equipped with a convex structure. More precisely:
$\bullet$ A _barycentric algebra_ is a set $A$ endowed with binary operations
$(a,b)\mapsto a+_{r}b\colon A\times A\to A$ indexed by $r\in[0,1]$ such that
for all $a,b,c\in A$ and $r,p\in[0,1]$, the following equations hold:

$a+_{1}b=a;\quad a+_{r}b=b+_{1-r}a;\quad
a+_{r}a=a;\quad(a+_{p}b)+_{r}c=a+_{pr}(b+_{\frac{r-pr}{1-pr}}c)~{}~{}\text{provided}~{}r,p<1.$

$\bullet$ A _pointed barycentric algebra_ is a barycentric algebra $A$ with a
distinguished element $\bot$. For $a\in A$ and $r\in[0,1]$, we define scalar
multiplication $r\cdot a\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}a+_{r}\bot$. A map $f\colon A\to B$ between pointed barycentric
algebras is _linear_ if $f(\bot_{A})=\bot_{B}$ and $f(a+_{r}b)=f(a)+_{r}f(b)$
for all $a,b\in A,r\in[0,1]$.
$\bullet$ A _Kegelspitze_ is a pointed barycentric algebra $K$ equipped with a
directed-complete partial order such that scalar multiplication $(r,a)\mapsto
r\cdot a\colon[0,1]\times K\to K$ and the binary operation $(a,b)\mapsto
a+_{r}b\colon K\times K\to K$, for $r\in[0,1]$, are Scott-continuous (in both
arguments). A _continuous Kegelspitze_ is a Kegelspitze that is a domain in
the equipped order.

###### Example 5.1.2.

For each dcpo $D$, $\mathcal{M}D$ is Kegelspitze: for $\nu_{i}\in\mathcal{M}D$
and $r_{i}\geq 0,i=1,\ldots,n$ with $\sum_{i=1}^{n}r_{i}\leq 1$, the convex
sum $\sum_{i=1}^{n}r_{i}\nu_{i}$ is again in $\mathcal{M}D$. Then, if
$\nu_{1},\nu_{2}\in\mathcal{M}D$ and $r\in[0,1]$, we define
$\nu_{1}+_{r}\nu_{2}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}r\nu_{1}+(1-r)\nu_{2}$. The zero valuation $\mathbf{0}_{D}$ is the
distinguished least element. If, in addition, $D$ is a domain, then
$\mathcal{M}D=\mathcal{V}D$ is a continuous Kegelspitze (Jia et al., 2021).
For each Scott-continuous map $f\colon D\to E$, the map
$\mathcal{M}(f)\colon\mathcal{M}D\to\mathcal{M}E$ is Scott-continuous and
linear.

###### Example 5.1.3.

The real unit interval $[0,1]$ is obviously a continuous Kegelspitze. More
generally, the unit interval $[0,1]_{A}$ of any von Neumann algebra $A$ is a
Kegelspitze. If $A$ also is hereditarily atomic, then $[0,1]_{A}$ is a
continuous Kegelspitze by (Selinger, 2004b, Example 2.7). Moreover, any NCPSU
map $f:A\to B$ between von Neumann algebras $A$ and $B$, is Scott-continuous
and linear when (co)restricted to the unit intervals of $A$ and $B$.

###  5.2. Correspondence between Observable Quantum/Probabilistic Effects

Our next result describes a bijective correspondence between _observable_
quantum/probabilistic effects that allows us to interpret the terms dealing
with observable primitives. A semantic observation (which we make precise
later) shows that: any quantum observable type $\mathbf{O}$ is interpreted as
a commutative HA-algebra that is $*$-isomorphic to $\ell^{\infty}(X)$ for some
set $X$; its classical observable counterpart $|\mathbf{O}|$ is interpreted as
the _discrete domain_ with underlying set $X$. Moreover, quantum values
correspond to $*$-homomorphisms and classical values to Dirac valuations.

######  Theorem 5.2.4.

Let $X$ be an arbitrary set. Then, there exists an isomorphism of (continuous)
Kegelspitzen
$r_{X}\colon\mathbf{Q}(\mathbb{C},\ell^{\infty}(X))\cong\mathcal{M}(X,\sqsubseteq)\colon
r_{X}^{-1}$, where $\sqsubseteq$ is the discrete order on $X$. Furthermore,
this isomorphism restricts to a 1-1 correspondence between the
$*$-homomorphisms of $\mathbf{Q}(\mathbb{C},\ell^{\infty}(X))$ and the Dirac
valuations of $\mathcal{M}(X,\sqsubseteq)$.

###### Proof.

See Appendix B. ∎

Combined with the above semantic observation, this theorem shows there is a
1-1 correspondence between the quantum and classical probabilistic states of
_observable_ types, and also a 1-1 correspondence between the interpretations
of quantum and classical observable values. This isomorphism is used for the
interpretations of the "run" and "init" terms.

Next, we construct an isomorphism that we use for the interpretation of
dynamic lifting (the "lift" term). This is similar to a construction first
reported in (Rennela and Staton, 2020).

######  Proposition 5.2.5.

Given a dcpo $X$, HA-algebras $A,B$, and a _discrete_ dcpo $Y$, there exists a
Scott-continuous and linear bijection
$\widehat{(-)}\colon\mathbf{DCPO}(X\times
Y,\mathbf{Q}(A,B))\cong\mathbf{DCPO}(X,\mathbf{Q}(\ell^{\infty}(Y)\otimes
A,B)),$ natural in all components.

###### Proof.

See Appendix C. ∎

###  5.3. Combining Probabilistic and Quantum Effects

In the previous subsection we considered _observable_ effects. In the present
subsection, we show how to combine _arbitrary_ quantum and probabilistic
effects _into_ quantum ones.

We begin by noting that on any Kegelspitze, the binary operations $a+_{r}b$
generalize to convex sums. We then use these convex sums in order to define
_barycentre_ maps.

###### Definition 5.3.6.

In each pointed barycentric algebra $K$, given $a_{i}\in
K,r_{i}\in[0,1],i=1,\ldots,n$ with $\sum_{i=1}^{n}r_{i}\leq 1$, we inductively
define the convex sum by

$\sum_{i=1}^{n}r_{i}a_{i}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\begin{cases}a_{1}&\text{, if }r_{1}=1,\\\
a_{1}+_{r_{1}}(\sum_{i=2}^{n}\frac{r_{i}}{1-r_{1}}a_{i})&\text{, if
}r_{1}<1.\end{cases}$

This sum is invariant under index-permutation: for $\pi$ a permutation of
$\\{1,\ldots,n\\}$,
$\sum_{i=1}^{n}r_{i}a_{i}=\sum_{i=1}^{n}r_{\pi(i)}a_{\pi(i)}$ (Jones, 1990,
Lemma 5.6). If $K$ is a Kegelspitze, then the expression
$\sum_{i=1}^{n}r_{i}a_{i}$ is Scott-continuous in each $r_{i}$ and $a_{i}$. A
_countable_ convex sum also can be defined: if $a_{i}\in K$ and
$r_{i}\in[0,1]$, for $i\in\mathbb{N}$, with $\sum_{i\in\mathbb{N}}r_{i}\leq
1$, define
$\sum_{i\in\mathbb{N}}r_{i}a_{i}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sup\\{\sum_{j\in J}r_{j}a_{j}\ |\ J\subseteq\mathbb{N}\text{ and
}J\text{ is finite}\\}.$

###### Definition 5.3.7.

Let $K$ be a Kegelspitze and $s=\sum_{i=1}^{n}r_{i}\delta_{x_{i}}$ be a simple
valuation on $K$. The _barycentre_ of $s$ is defined as
$\beta_{*}(s)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sum_{i=1}^{n}r_{i}x_{i}$. Furthermore, if $K$ is a continuous
Kegelspitze and $\nu\in\mathcal{M}K$, the _barycentre_ of $\nu$ is defined as
$\beta(\nu)\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\sup\\{\beta_{*}(s)\mid s\in\mathcal{S}K\text{ and }s\ll\nu\\}$.

When $K$ is a _continuous_ Kegelspitze, the barycentre map
$\beta\colon\mathcal{M}K\to K::\nu\mapsto\beta(\nu)$ is well-defined, unique,
Scott-continuous and linear (Jia et al., 2021). We emphasise that _continuity_
is crucial for establishing this and it is unclear if this holds otherwise.
Moreover, the following also is true.

######  Theorem 5.3.8 ((Jia et al., 2021)).

The Eilenberg-Moore category $\mathbf{DOM}^{\mathcal{M}}$ of $\mathcal{M}$
over $\mathbf{DOM}$ is isomorphic to the category of continuous Kegelspitzen
and Scott-continuous linear maps. In particular:

  1. (1)

Each _continuous_ Kegelspitze $K$ admits a linear barycentre map
$\beta\colon\mathcal{M}K\to K$ (as in Definition 5.3.7) for which the pair
$(K,\beta)$ is an Eilenberg-Moore algebra of $\mathcal{M}$ over
$\mathbf{DOM}$.

  2. (2)

Conversely, on each $\mathcal{M}$-algebra $(K,\beta)$ on $\mathbf{DOM}$,
define $a+_{r}b\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\beta(\delta_{a}+_{r}\delta_{b})$ for $a,b\in K$ and $r\in[0,1]$.
Then with the operations $+_{r}$, $K$ is a continuous Kegelspitze and
$\beta\colon\mathcal{M}K\to K$ is linear.

In §4 we saw that $\mathbf{Q}$ is enriched over $\mathbf{DOM}$. We now further
strengthen that result.

######  Theorem 5.3.9.

The category $\mathbf{Q}$ is enriched over _continuous_ Kegelspitzen in the
following sense: for all objects $A$, $B$ in $\mathbf{Q}$, the homset
$\mathbf{Q}(A,B)$ is a _continuous_ Kegelspitze, and for any morphism
$\varphi:A\to B$ in $\mathbf{Q}$ and any object $C$ in $\mathbf{Q}$, the
following maps are Scott-continuous and linear:

$\mathbf{Q}(C,\varphi):\mathbf{Q}(C,A)\to\mathbf{Q}(C,B)::\psi\mapsto\varphi\circ\psi\quad\text{and}\quad\mathbf{Q}(\varphi,C):\mathbf{Q}(B,C)\to\mathbf{Q}(A,C)::\psi\mapsto\psi\circ\varphi.$

###### Proof.

See Appendix A. ∎

Combining these two theorems gives the main result of this section.

######  Theorem 5.3.10.

For any HA-algebras $A$ and $B$, there exists a (unique) Scott-continuous and
linear barycentre map
$\beta\colon\mathcal{M}\mathbf{Q}(A,B)\to\mathbf{Q}(A,B)$ that is also an
Eilenberg-Moore algebra of $\mathcal{M}$.

The above properties of $\beta$ are exactly what is needed to interpret the
"$m\mathbf{q}$" term from Figure 7, which allows us to combine classical
probabilistic computation with quantum computation.

##  6\. Categorical Model

In this section we organise the relevant mathematical data into several
categories that we later use to describe our denotational semantics. A
diagrammatic summary is provided in Figure 12 ($\S\ref{sec:semantics}$).

###  6.1. The Kleisli Category of $\mathcal{M}$

This subsection provides a summary of the development in (Jia et al., 2021) of
the Kleisli category of the monad $\mathcal{M}:\mathbf{DCPO}\to\mathbf{DCPO}$,
which we denote $\mathbf{DCPO}_{\mathcal{M}}$. In order to distinguish between
the categorical primitives of $\mathbf{DCPO}$ and
$\mathbf{DCPO}_{\mathcal{M}}$, we adopt the notation of (Jia et al., 2021),
indicating the morphisms of $\mathbf{DCPO}_{\mathcal{M}}$ by
$f:A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}B$, and using
$f\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}g\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mu\circ\mathcal{M}(f)\circ g$ to denote the Kleisli composition
of morphisms in $\mathbf{DCPO}_{\mathcal{M}}$ (where $\mu$ is the
multiplication of $\mathcal{M}$). We write
$\textbf{id}_{A}:A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}A$ with $\textbf{id}_{A}=\eta_{A}:A\to\mathcal{M}A$ for the identity
morphisms in $\mathbf{DCPO}_{\mathcal{M}}.$ The adjunction
$\mathcal{J}\dashv\mathcal{U}:\mathbf{DCPO}_{\mathcal{M}}\to\mathbf{DCPO}$
that factorises $\mathcal{M}$ is determined by the assignments:

$\displaystyle\mathcal{J}A\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}A,\quad\mathcal{J}f\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\eta\circ
f,\quad\mathcal{U}A\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{M}A,\quad\mathcal{U}f\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mu\circ\mathcal{M}f.$

####  6.1.1. Coproducts

$\mathbf{DCPO}_{\mathcal{M}}$ inherits (small) coproducts from $\mathbf{DCPO}$
in the standard way (Jacobs, 2016, pp. 264) and we write
$A_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}A_{2}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}A_{1}+A_{2}$ for the induced (binary) coproduct. The induced
coprojections are given by $\mathcal{J}(\emph{in}_{1})\colon
A_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}A_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}A_{2}$ and $\mathcal{J}(\emph{in}_{2})\colon
A_{2}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}A_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}A_{2}.$ Then for $f\colon
A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}C$ and $g\colon
B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}D$,
$f\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}g=[\mathcal{M}(\emph{in}_{C})\circ
f,\mathcal{M}(\emph{in}_{D})\circ g]$ and the functor $\mathcal{J}$ strictly
preserves coproducts.

####  6.1.2. Symmetric monoidal structure

Because $\mathcal{M}$ is _commutative_ , it induces a canonical symmetric
monoidal structure on $\mathbf{DCPO}_{\mathcal{M}}$ making $\mathcal{J}$ a
strict monoidal functor (Power and Robinson, 1997). The induced tensor product
is
$A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}B\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}A\times B$ with
Kleisli projections
$\mathcal{J}(\pi_{A}):A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}A$ and
$\mathcal{J}(\pi_{B}):A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}B$; but these projections do _not_ satisfy the universal property of a
product. The tensor product of $f\colon
A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}C$ and $g\colon
B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}D$ is denoted by
$f\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}g$ and it is defined as usual. It follows that Kleisli products distribute
over Kleisli coproducts and we write
$d_{A,B,C}:A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}(B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr}
}}C)\cong(A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}B)\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr}
}}(A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}C)$ for this natural isomorphism.

####  6.1.3. Kleisli Exponential

The adjunction $\mathcal{J}\dashv\mathcal{U}$ also contains the structure of a
_Kleisli-exponential_. Following (Moggi, 1991), we use this to interpret
higher-order function types.

For each dcpo $B$, we use
$[B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}-]\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}[B\to\mathcal{U}(-)]:\mathbf{DCPO}_{\mathcal{M}}\to\mathbf{DCPO}$
to denote the right adjoint of the functor
$J(-)\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}B:\mathbf{DCPO}\to\mathbf{DCPO}_{\mathcal{M}}$. Therefore, on objects,
$[B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}C]=[B\to\mathcal{M}C].$ This determines a family of Scott-continuous
bijections
$\lambda:\mathbf{DCPO}_{\mathcal{M}}(\mathcal{J}A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}B,C)\cong\mathbf{DCPO}(A,[B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}C]),$ natural in $A$ and $C$, often called _currying_. We also denote the
counit of these adjunctions by
$\epsilon:\mathcal{J}[B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}-]\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}B\Rightarrow\mathrm{Id}$, which is often called _evaluation_. Since this
family of adjunctions is parameterised by objects $B$ of
$\mathbf{DCPO}_{\mathcal{M}}$, standard categorical results (Mac Lane, 1998,
§IV.7) imply the assignment
$[B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}-]:\mathbf{DCPO}_{\mathcal{M}}\to\mathbf{DCPO}$ can be extended uniquely to
a bifunctor
$[-\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}-]:\mathbf{DCPO}_{\mathcal{M}}^{\mathrm{op}}\times\mathbf{DCPO}_{\mathcal{M}}\to\mathbf{DCPO},$
such that $\lambda$ is natural in all three components.

####  6.1.4. Enrichment Structure

The Kleisli category $\mathbf{DCPO}_{\mathcal{M}}$ is enriched over
$\mathbf{DCPO}_{\perp!}:$ for dcpo’s $A,B$ and $C$, the Kleisli exponential
$[A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}B]=[A\to\mathcal{M}B]=\mathbf{DCPO}_{\mathcal{M}}(A,B)$ is a pointed dcpo
and the Kleisli composition
$\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}\colon[A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}B]\times[B\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}C]\to[A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}C]$ is strict and Scott continuous. Furthermore, the adjunction
$\mathcal{J}\dashv\mathcal{U}$ also is $\mathbf{DCPO}$-enriched, as are the
bifunctors
$(-\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}-),(-\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}-)$ and
$[-\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}-].$

The category $\mathbf{DCPO}_{\mathcal{M}}$ also has a convex structure: for
each dcpo $B$, $\mathcal{M}B$ is a Kegelspitze in the stochastic order by
Example 5.1.2, from which it follows that
$[A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}B]=\mathbf{DCPO}_{\mathcal{M}}(A,B)$ also is a Kegelspitze in the pointwise
order. This convex structure is preserved by Kleisli composition
$\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}$, Kleisli coproduct
$\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}$ and Kleisli product
$\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}$ (Jia et al., 2021, Lemma 38).

####  6.1.5. The Subcategories $\mathbf{TD}$ and $\mathbf{PD}$

We identify two important subcategories of $\mathbf{DCPO}_{\mathcal{M}}$: one
for the interpretation of classical values ($\mathbf{TD}$) and one for solving
recursive domain equations ($\mathbf{PD}$).

###### Definition 6.1.1.

The subcategory $\mathbf{TD}$ of _deterministic total maps_ is the full-on-
objects subcategory of $\mathbf{DCPO}_{\mathcal{M}}$ whose morphisms $f\colon
X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}Y$ admit a factorisation $f=\mathcal{J}(f^{\prime})=\eta_{y}\circ
f^{\prime},$ for some $f^{\prime}$.

Each map
$f:X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}Y$ in $\mathbf{TD}$ satisfies $f(x)=\delta_{y}$ for some $y\in Y$, by
definition. We call such maps _deterministic_ because they carry no
interesting convex structure, and they are _total_ in that they map all inputs
$x\in X$ to non-zero valuations. $\mathbf{TD}$ is important because all
_classical values_ of our language are interpreted in $\mathbf{TD}$. In fact,
$\mathbf{DCPO}\cong\mathbf{TD}$ (Jia et al., 2021, Proposition 40).

The canonical copy map at an object $A$ in our model is given by the map
$\mathcal{J}\langle\mathrm{id}_{A},\mathrm{id}_{A}\rangle\colon
A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}A$; likewise, the canonical discarding map at $A$ is the map
$\mathcal{J}(1_{A})\colon
A\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}1,$ where $1_{A}\colon A\to 1$ is the terminal map of $\mathbf{DCPO}$.
Because maps in $\mathbf{TD}$ are in the image of $\mathcal{J}$, they are
compatible with the copy and discard maps, and hence also with weakening and
contraction (Benton, 1995).

###### Definition 6.1.2.

The subcategory of _deterministic partial maps_ , denoted $\mathbf{PD}$, is
the full-on-objects subcategory of $\mathbf{DCPO}_{\mathcal{M}}$ each of whose
morphisms $f\colon
X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}Y$ admits a factorisation
$f=\left(X\xrightarrow{f^{\prime}}Y_{\perp}\xrightarrow{\phi_{Y}}\mathcal{M}Y\right),$
where $Y_{\perp}$ is the dcpo obtained from $Y$ by freely adding a least
element $\perp$, and where $\phi_{Y}$ is the map $\phi_{Y}\colon
Y_{\perp}\to\mathcal{M}Y::y\mapsto\begin{cases}{\mathbf{0}}_{Y}&\text{, if
}y=\perp\\\ \delta_{y}&\text{, if }y\neq\perp\end{cases}.$

These maps are _partial_ because they map some inputs to $\mathbf{0}$; they
also are deterministic, because the convex structure is trivial in both cases.
This is justified by the fact that
$\mathbf{PD}\cong\mathbf{DCPO}_{\mathcal{T}}\cong\mathbf{DCPO}_{\perp!},$
where $\mathbf{DCPO}_{\mathcal{T}}$ is the Kleisli category of the lift monad
$\mathcal{T}:\mathbf{DCPO}\to\mathbf{DCPO}$ (Jia et al., 2021).

####  6.1.6. Solving Recursive Domain Equations

The standard method for interpreting recursive types is to construct
_parameterised initial algebras_ (Fiore, 1994; Fiore and Plotkin, 1994). We
employ this approach in $\mathbf{PD}$ using the limit-colimit coincidence
theorem (Smyth and Plotkin, 1982).

###### Definition 6.1.3 (see (Fiore, 1994, §6.1)).

Given a category $\mathbf{C}$ and a functor
$\mathcal{T}\colon\mathbf{C}^{n+1}\to\mathbf{C},$ a _parameterised initial
algebra_ for $\mathcal{T}$ is a pair
$(\mathcal{T}^{\sharp},\iota^{\mathcal{T}}),$ such that:

  * •

$\mathcal{T}^{\sharp}\colon\mathbf{C}^{n}\to\mathbf{C}$ is a functor;

  * •

$\iota^{\mathcal{T}}\colon\mathcal{T}\circ\langle\mathrm{Id},\mathcal{T}^{\sharp}\rangle\Rightarrow\mathcal{T}^{\sharp}:\mathbf{C}^{n}\to\mathbf{C}$
is a natural transformation;

  * •

For every $\vec{C}\in\text{Ob}(\mathbf{C}^{n})$, the pair
$(\mathcal{T}^{\sharp}\vec{C},\iota^{\mathcal{T}}_{\vec{C}})$ is an initial
$\mathcal{T}(\vec{C},-)$-algebra.

The usual notion of an initial algebra arises in the case that $n=1$.

######  Proposition 6.1.4 (see (Lindenhovius et al., 2021, §4.3)).

Let $\mathbf{C}$ be a category with an initial object and all
$\omega$-colimits, and let $\mathcal{T}\colon\mathbf{C}^{n+1}\to\mathbf{C}$ be
an $\omega$-cocontinuous functor. Then $\mathcal{T}$ has a parameterised
initial algebra $(\mathcal{T}^{\sharp},\iota^{\mathcal{T}})$ and the functor
$\mathcal{T}^{\sharp}\colon\mathbf{C}^{n}\to\mathbf{C}$ is also
$\omega$-cocontinuous.

In fact, the subcategory $\mathbf{PD}$ has sufficient structure to solve
recursive domain equations, because it is _$\mathbf{DCPO}$ -algebraically
compact_ (Jia et al., 2021). Therefore, every $\mathbf{DCPO}$-enriched
_covariant_ functor on $\mathbf{DCPO}_{\mathcal{M}}$ that restricts to
$\mathbf{PD}$ has a parameterised initial algebra (whose inverse is a
parameterised final coalgebra). Solving equations involving _mixed-variance_
functors (induced by function types) can be done using the limit-colimit
coincidence theorem (Smyth and Plotkin, 1982). An important observation made
in (Smyth and Plotkin, 1982) is that all type expressions (including function
spaces) can be interpreted as covariant functors on _subcategories of
embeddings_. For more details on this, see (Lindenhovius et al., 2019, 2021);
here we also follow this approach.

###### Definition 6.1.5.

If $\mathbf{C}$ is a $\mathbf{DCPO}$-enriched category, a morphism $e\colon
X\to Y$ is an _embedding_ if there exists a (necessarily unique) _projection_
$e^{p}\colon Y\to X$, i.e., a morphism satisfying $e^{p}\circ
e=\mathrm{id}_{X}$ and $e\circ e^{p}\leq\mathrm{id}_{Y}.$ $\mathbf{C}_{e}$
denotes the full-on-objects subcategory of $\mathbf{C}$ whose morphisms are
the embeddings.

######  Proposition 6.1.6 ((Jia et al., 2021, Proposition 47)).

The category $\mathbf{PD}_{e}$ has an initial object and all
$\omega$-colimits, and the assignments:

$\displaystyle\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}_{e}\colon\mathbf{PD}_{e}\times\mathbf{PD}_{e}\to\mathbf{PD}_{e}\text{
defined by
}X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}_{e}Y\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}Y\ \text{and}\
e_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}_{e}e_{2}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}e_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.21529pt\cr$\times$\cr}
}}e_{2}$
$\displaystyle\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr}
}}_{e}\colon\mathbf{PD}_{e}\times\mathbf{PD}_{e}\to\mathbf{PD}_{e}\text{
defined by
}X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}_{e}Y\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}Y\ \text{and}\
e_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}_{e}e_{2}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}e_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.86108pt\cr$+$\cr} }}e_{2}$
$\displaystyle[\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}]_{e}^{\mathcal{J}}\colon\mathbf{PD}_{e}\times\mathbf{PD}_{e}\to\mathbf{PD}_{e}\text{
defined by
}[X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}Y]_{e}^{\mathcal{J}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}[X\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}Y]\ \text{and}\
[e_{1}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}e_{2}]_{e}^{\mathcal{J}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}[e_{1}^{p}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}e_{2}]$

are _covariant_ $\omega$-cocontinuous bifunctors on $\mathbf{PD}_{e}$.

Thus Propositions 6.1.4 and 6.1.6 show we can solve recursive domain equations
induced by all well-formed type expressions within $\mathbf{PD}_{e}$, notably
with no restrictions on the admissible logical polarities of the types.
However, our classical judgements support weakening and contraction, so we
have an extra proof obligation: proving each isomorphism that is a solution to
a recursive domain equation can be copied and discarded. This is true, because
every isomorphism of $\mathbf{PD}$ (and $\mathbf{PD}_{e}$) also are
isomorphisms of $\mathbf{TD}$ (Jia et al., 2021, Propoistion 48).

###  6.2. The Quantum Category $\mathbf{Q}$

We now describe the categorical structure of $\mathbf{Q}$ and its subcategory
$\mathbf{Q}_{*}$. We interpret quantum terms in $\mathbf{Q}$ and quantum
values in $\mathbf{Q}_{*}$.

####  6.2.1. Coproducts

Proposition 4.1.4 describes the categorical product on $\mathbf{vN}_{*}$,
which restricts to a categorical product on $\mathbf{HA}_{*}$ since the
product of hereditarily atomic von Neumann algebras clearly is hereditarily
atomic. Moreover, the product on $\mathbf{HA}_{*}$ extends to a product on
$\mathbf{HA}$. As a consequence, $\mathbf{Q}$ and $\mathbf{Q}_{*}$ have small
coproducts and we write $A\oplus B$ to denote the coproduct in both
categories. We write the coprojections as $\mathbf{in}_{1}\colon A\to A\oplus
B$ and $\mathbf{in}_{2}\colon B\to A\oplus B.$ Note that the initial object
$\mathbf{0}$ of $\mathbf{Q}_{*}$, given by the 1 element HA-algebra, is a zero
object in $\mathbf{Q}$ (but not in $\mathbf{Q}_{*}$).

####  6.2.2. Symmetric Monoidal Structure

Given two von Neumann algebras $M$ and $N$ on Hilbert spaces $H$ and $K$,
respectively, the algebraic tensor product $M\odot N$ acts in a natural way on
the Hilbert space tensor product $H\otimes K$. The weak operator closure of
$M\odot N$ in $B(H\otimes K)$ is a von Neumann algebra, usually denoted
$M\bar{\otimes}N$, and called the _spatial tensor product_ of $M$ and $N$. The
construction in (Blackadar, 2006, III.2.2.5) shows the spatial tensor product
of von Neumann algebras induces a symmetric monoidal product on both
$\mathbf{HA}_{*}$ and $\mathbf{HA}$, hence on $\mathbf{Q}_{*}$ and
$\mathbf{Q}$. We write $A\otimes B$ for the tensor product in both
$\mathbf{Q}$ and $\mathbf{Q}_{*}$. Moreover, $\mathbf{Q}_{*}$ is symmetric
monoidal closed (Kornell, 2020, Theorem 9.1) and therefore there exists a
natural isomorphism $\mathbf{d}_{A,B,C}:A\otimes(B\oplus C)\cong(A\otimes
B)\oplus(A\otimes C)$.

####  6.2.3. Adjunctions

The subcategory inclusion $\mathcal{I}:\mathbf{Q}_{*}\to\mathbf{Q}$
corresponds to an embedding $\mathbf{HA}_{*}\to\mathbf{HA}$ that is shown to
have a left adjoint in (Westerbaan, 2019, Section 4.3.4). Therefore
$\mathcal{I}$ has a right adjoint. Moreover, the adjunction between
$\mathbf{Q}_{*}$ and $\mathbf{Q}$ is Kleislian (Westerbaan, 2019) and the
subcategory inclusion $\mathcal{I}:\mathbf{Q}_{*}\to\mathbf{Q}$ is a strict
monoidal functor that strictly preserves coproducts.

The assignment $\ell^{\infty}(-)$ extends to a functor
$\ell^{\infty}:\mathbf{Set}\to\mathbf{HA}^{\mathrm{op}}_{*}$ whose action on
functions $f:X\to Y$ between sets is a normal $*$-homomorphism
$\ell^{\infty}(f):\ell^{\infty}(Y)\to\ell^{\infty}(X)::k\mapsto k\circ f$.
Hence we obtain a functor $\ell^{\infty}:\mathbf{Set}\to\mathbf{Q}_{*}$, which
is fully faithful; its essential image is the full subcategory of
$\mathbf{Q}_{*}$ consisting of all commutative hereditarily atomic von Neumann
algebras.

####  6.2.4. Affine Structure

The monoidal unit $\mathbb{C}$ is _initial_ in $\mathbf{HA}_{*}$ and therefore
it is _terminal_ in $\mathbf{Q}_{*}$, but the same is not true for
$\mathbf{HA}$ and $\mathbf{Q}$. The terminal map of $\mathbf{Q}_{*}$ at
$\mathrm{M}_{n}(\mathbb{C})$ is actually $\mathrm{tr}^{\ddagger}$ (see §4.2).
This allows us to define suitable discarding maps. The map
$\mathrm{drop_{k}}^{\ddagger}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}(x\mapsto x\otimes
1)^{\mathrm{op}}\in\mathbf{Q}(A\otimes\mathrm{M}_{2^{k}}(\mathbb{C}),A)$
should be thought of (in $\mathbf{Q}$) as discarding $k$ auxiliary qubits;
this map is used for the interpretation of the "run" term when we execute a
non-total quantum configuration that has $k$ auxiliary qubits (which may be
safely discarded at the end of the computation). Indeed, notice that in the
category $\mathbf{Q}$, we have
$\mathrm{drop}_{k}^{\ddagger}\circ(\mathrm{id}_{A}\otimes\mathrm{state}_{\rho}^{\ddagger})=\mathrm{id}_{A},$
for any density matrix $\rho$ in $\mathrm{M}_{2^{k}}(\mathbb{C})$, as one
would expect (for brevity, we implicitly suppress the isomorphism
$A\otimes\mathbb{C}\cong A$).

####  6.2.5. Solving Recursive Domain Equations

We now show that the category $\mathbf{Q}_{*}$ has sufficient structure to
construct parameterised initial algebras for polynomial functors. On the
quantum side, this covers all recursive domain equations that have to be
solved.

######  Proposition 6.2.7.

The category $\mathbf{Q}_{*}$ is cocomplete and the functors
$\otimes\colon\mathbf{Q}_{*}\times\mathbf{Q}_{*}\to\mathbf{Q}_{*}$ and
$\oplus\colon\mathbf{Q}_{*}\times\mathbf{Q}_{*}\to\mathbf{Q}_{*}$ are
cocontinuous.

###### Proof.

Cocompleteness of $\mathbf{Q}_{*}$ is shown in (Kornell, 2020, Proposition
8.6); the coproduct bifunctor $\oplus$ is obviously cocontinuous; the functor
$\otimes$ is cocontinuous because $\mathbf{Q}_{*}$ is monoidal closed. ∎

##  7\. Denotational Semantics

$\mathbf{Set}$$\mathbf{DCPO}$

$\dashv$

$\mathcal{L}$$\mathbf{Q}_{*}$

$\dashv$

$\ell^{\infty}$$\mathbf{DCPO}_{\mathcal{M}}$$\dashv$$\mathcal{J}$$\mathbf{Q}$$\dashv$$\mathcal{I}$Observable
ValuesClassical ValuesQuantum ValuesQuantum TermsClassical Terms

Figure 12. Overview of the categorical model.

We now give the denotational semantics of our language. In Figure 12, we
summarise the overall structure of the interpretation. The blue arrows show
where the indicated programming primitives can be interpreted. Every such
primitive may also be interpreted in a category above it by following the
corresponding left adjoint. All depicted categories are symmetric monoidal and
so are the adjunctions between them. The left adjoints $\mathcal{L}$ and
$\ell^{\infty}$ are both fully faithful and this allows us to interpret the
_observable_ values in the bottom three categories and also to coherently
relate these interpretations.

###  7.1. Interpretation of Types

We begin with the interpretation of (open) types, which is described in Figure
18. Open quantum types are interpreted as functors
$\mathbf{{\llbracket\Theta\vdash A\rrbracket}}\colon\
\mathbf{Q}_{*}^{|\mathbf{\Theta}|}\to\mathbf{Q}_{*}$ and open classical types
are interpreted as functors ${\llbracket\Theta\vdash P\rrbracket}\colon\
\mathbf{PD}_{e}^{|\Theta|}\to\mathbf{PD}_{e}$. Given closed types
$\cdot\vdash\mathbf{A}$ and $\cdot\vdash P$, we write $\mathbf{{\llbracket
A\rrbracket}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathbf{{\llbracket\cdot\vdash
A\rrbracket}}(*)\in\text{Ob}(\mathbf{Q}_{*})=\text{Ob}(\mathbf{Q})$ and
${\llbracket P\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}{\llbracket\cdot\vdash
P\rrbracket}(*)\in\text{Ob}(\mathbf{PD}_{e})=\text{Ob}(\mathbf{DCPO}).$

$\displaystyle\mathbf{{\llbracket\Theta\vdash A\rrbracket}}\colon\
\mathbf{Q}_{*}^{|\Theta|}\to\mathbf{Q}_{*}\quad{\llbracket\mathbf{\Theta}\vdash\mathbf{\Theta}_{i}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\Pi_{i}\quad\mathbf{{\llbracket\Theta\vdash
I\rrbracket}}\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\
K_{\mathbb{C}}\quad\mathbf{{\llbracket\Theta\vdash\textnormal{{qbit}}\rrbracket}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\
K_{\mathrm{M}_{2}(\mathbb{C})}\quad\mathbf{{\llbracket\Theta\vdash\mu
X.A\rrbracket}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathbf{{\llbracket\Theta,X\vdash A\rrbracket}}^{\sharp}$
$\displaystyle\mathbf{{\llbracket\Theta\vdash A\oplus
B\rrbracket}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\oplus\circ\langle\mathbf{{\llbracket\Theta\vdash
A\rrbracket}},\mathbf{{\llbracket\Theta\vdash
B\rrbracket}}\rangle\qquad\mathbf{{\llbracket\Theta\vdash A\otimes
B\rrbracket}}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\otimes\circ\langle\mathbf{{\llbracket\Theta\vdash
A\rrbracket}},\mathbf{{\llbracket\Theta\vdash B\rrbracket}}\rangle$
$\displaystyle{\llbracket\Theta\vdash P\rrbracket}\colon\
\mathbf{PD}_{e}^{|\Theta|}\to\mathbf{PD}_{e}\qquad{\llbracket\Theta\vdash\Theta_{i}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\Pi_{i}\qquad{\llbracket\Theta\vdash
1\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\
K_{1}\qquad{\llbracket\Theta\vdash\mu
X.P\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}{\llbracket\Theta,X\vdash P\rrbracket}^{\sharp}$
$\displaystyle{\llbracket\Theta\vdash
P+R\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\
\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern
0.77498pt\cr$+$\cr} }}_{e}\circ\ \langle{\llbracket\Theta\vdash
P\rrbracket},{\llbracket\Theta\vdash
R\rrbracket}\rangle\qquad{\llbracket\Theta\vdash P\times
R\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize def}}}}{{=}}\
\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.19376pt\cr$\times$\cr}
}}_{e}\circ\ \langle{\llbracket\Theta\vdash
P\rrbracket},{\llbracket\Theta\vdash R\rrbracket}\rangle$
$\displaystyle{\llbracket\Theta\vdash P\to
R\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}[\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-2.71246pt\cr$\to$\cr}
}}]_{e}^{\mathcal{J}}\circ\langle{\llbracket\Theta\vdash
P\rrbracket},{\llbracket\Theta\vdash
R\rrbracket}\rangle\qquad{\llbracket\Theta\vdash
Q(\mathbf{A},\mathbf{B})\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}K_{\mathbf{Q}(\mathbf{{\llbracket
A\rrbracket}},\mathbf{{\llbracket B\rrbracket}})}$

Figure 13. Interpretation of types. $K_{X}$ is the constant-$X$-functor.

$\begin{array}[]{l l l l l}\mathbf{{\llbracket
I\rrbracket}}=\mathbb{C}&\mathbf{{\llbracket A\otimes
B\rrbracket}}=\mathbf{{\llbracket A\rrbracket}}\otimes\mathbf{{\llbracket
B\rrbracket}}&\mathbf{{\llbracket A\oplus B\rrbracket}}=\mathbf{{\llbracket
A\rrbracket}}\oplus\mathbf{{\llbracket
B\rrbracket}}&{\llbracket\mu\mathbf{X}.\mathbf{A}\rrbracket}\cong{\llbracket\mathbf{A}[\mu\mathbf{X}.\mathbf{A}/\mathbf{X}]\rrbracket}\\\\[3.87498pt]
{\llbracket 1\rrbracket}=1&{\llbracket P\times R\rrbracket}={\llbracket
P\rrbracket}\times{\llbracket R\rrbracket}&{\llbracket
P+R\rrbracket}={\llbracket P\rrbracket}+{\llbracket
R\rrbracket}&{\llbracket\mu X.P\rrbracket}\cong{\llbracket P[\mu
X.P/X]\rrbracket}\\\\[3.87498pt]
\mathbf{{\llbracket\textnormal{{qbit}}\rrbracket}}=\mathrm{M}_{2}(\mathbb{C})&{\llbracket
P\to R\rrbracket}=\left[{\llbracket P\rrbracket}\to\mathcal{M}{\llbracket
R\rrbracket}\right]&{\llbracket
Q(\mathbf{A},\mathbf{B})\rrbracket}=\mathbf{Q}(\mathbf{{\llbracket
A\rrbracket}},\mathbf{{\llbracket B\rrbracket}})&\end{array}$

Figure 14. Derived equations for closed types.

$\begin{array}[]{l}{\llbracket\Phi\vdash
m:P\rrbracket}:{\llbracket\Phi\rrbracket}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-2.71246pt\cr$\to$\cr}
}}{\llbracket P\rrbracket}\text{ in $\mathbf{DCPO}_{\mathcal{M}}$}\\\
{\llbracket\Phi,x:P\vdash
x:P\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}\pi_{2}\\\
{\llbracket\Phi\vdash():1\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}1\\\ {\llbracket\Phi\vdash(m,n):P\times
R\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}({\llbracket
m\rrbracket}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.19376pt\cr$\times$\cr}
}}{\llbracket
n\rrbracket})\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}\mathcal{J}\langle\mathrm{id},\mathrm{id}\rangle\\\
{\llbracket\Phi\vdash\pi_{i}m:P_{i}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}\pi_{i}\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}{\llbracket
m\rrbracket},\text{ for }i\in\\{1,2\\}\\\
{\llbracket\Phi\vdash\emph{in}_{i}m:P_{1}+P_{2}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}\emph{in}_{i}\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}{\llbracket
m\rrbracket},\text{ for }i\in\\{1,2\\}\\\ {\llbracket\Phi\vdash(\text{case}\
m\ \text{of}\ \emph{in}_{1}x\Rightarrow n_{1}\ |\ \emph{in}_{2}y\Rightarrow
n_{2}):R\rrbracket}\\\ \quad\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}[{\llbracket n_{1}\rrbracket},{\llbracket
n_{2}\rrbracket}]\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}d\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}(\mathrm{id}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.19376pt\cr$\times$\cr}
}}{\llbracket
m\rrbracket})\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}\mathcal{J}\langle\mathrm{id},\mathrm{id}\rangle\\\
{\llbracket\Phi\vdash\lambda x^{P}.m:P\to
R\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}\lambda({\llbracket m\rrbracket})\\\
{\llbracket\Phi\vdash
mn:R\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\epsilon\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}({\llbracket
m\rrbracket}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.0}{.}\cr\kern-0.19376pt\cr$\times$\cr}
}}{\llbracket
n\rrbracket})\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}\mathcal{J}\langle\mathrm{id},\mathrm{id}\rangle\\\
{\llbracket\Phi\vdash{\lambda}(\mathbf{x}_{1},\ldots,\mathbf{x}_{n}).\mathbf{q}:Q(\mathbf{A}_{1}\otimes\cdots\otimes\mathbf{A}_{n},\mathbf{B})\rrbracket}\\\
\quad\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}\mathbf{{\llbracket q\rrbracket}}\\\
{\llbracket\Phi\vdash\text{new}:Q(\textnormal{{bit}},\textnormal{{qbit}})\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}(x\mapsto\text{new}^{\ddagger})\\\
{\llbracket\Phi\vdash U:Q(\textnormal{{qbit}}^{\otimes
n},\textnormal{{qbit}}^{\otimes
n})\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}(x\mapsto\text{unitary}_{U}^{\ddagger})\\\
{\llbracket\Phi\vdash\text{meas}:Q(\textnormal{{qbit}},\textnormal{{bit}})\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathcal{J}(x\mapsto\text{meas}^{\ddagger})\\\
{\llbracket\Phi\vdash\textnormal{\text{fold}}{}\ m:\mu
X.P\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathrm{fold}\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}{\llbracket
m\rrbracket}\\\ {\llbracket\Phi\vdash\textnormal{\text{unfold}}\ m:P[\mu
X.P/X]\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}\mathrm{unfold}\mathbin{\raisebox{0.9pt}{\scalebox{0.7}{$\varodot$}}}{\llbracket
m\rrbracket}\\\ {\llbracket\Phi\vdash\text{run
}\mathcal{C}:|\mathbf{O}|\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto
r(\mathrm{drop}_{k}^{\ddagger}\circ{\llbracket\mathcal{C}\rrbracket}_{x})\end{array}$
Figure 15. Interpretation of classical term judgements.

$\begin{array}[]{l}{\llbracket\Phi;\mathbf{\Gamma\vdash
q:A}\rrbracket}\colon{\llbracket\Phi\rrbracket}\to\mathbf{Q}({\llbracket\mathbf{\Gamma}\rrbracket},{\llbracket\mathbf{A}\rrbracket})\text{
in $\mathbf{DCPO}$}\\\\[1.93748pt] {\llbracket\Phi;\mathbf{y:A\vdash
y:A}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\mathrm{id}_{\mathbf{{\llbracket A\rrbracket}}}\\\
{\llbracket\Phi;\cdot\vdash*:\mathbf{I}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\mathrm{id}_{\mathbb{C}}\\\\[3.87498pt]
{\llbracket\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash
q;r:\mathbf{A}}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto(\cong\circ(\mathbf{{\llbracket
q\rrbracket}}_{x}\otimes\mathbf{{\llbracket r\rrbracket}}_{x}))\\\
{\llbracket\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash q\otimes r:A\otimes
B}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\mathbf{{\llbracket
q\rrbracket}}_{x}\otimes\mathbf{{\llbracket r\rrbracket}}_{x}\\\\[3.87498pt]
{\llbracket\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash let\ x\otimes y=q\ in\
r:B}\rrbracket}\\\ \quad\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\mathbf{{\llbracket
r\rrbracket}}_{x}\circ(\mathrm{id}_{\mathbf{{\llbracket\Gamma_{2}\rrbracket}}}\otimes\mathbf{{\llbracket
q\rrbracket}}_{x})\circ\text{swap}\\\\[1.93748pt]
{\llbracket\Phi;\mathbf{\Gamma}\vdash\mathbf{in}_{i}\
\mathbf{q}:\mathbf{A}\oplus\mathbf{B}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\mathbf{in}_{i}\circ\mathbf{{\llbracket
q\rrbracket}}_{x}\\\\[3.87498pt]
{\llbracket\Phi;\mathbf{\Gamma_{1},\Gamma_{2}\vdash(case\ q\ of\
in_{1}x\Rightarrow r_{1}\ |\ in_{2}y\Rightarrow r_{2}):B}\rrbracket}\\\
\quad\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto[\mathbf{{\llbracket
r_{1}\rrbracket}}_{x},\mathbf{{\llbracket
r_{2}\rrbracket}}_{x}]\circ\mathbf{d}\circ(\mathrm{id}\otimes\mathbf{{\llbracket
q\rrbracket}}_{x})\circ\text{swap}\\\\[1.93748pt]
{\llbracket\Phi;\mathbf{\Gamma}\vdash
m\mathbf{q}:\mathbf{B}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\beta({\llbracket
m\rrbracket}_{x})\circ\mathbf{{\llbracket q\rrbracket}}_{x}\\\
{\llbracket\Phi;\mathbf{\Gamma\vdash\textbf{fold}\ q:\mu
X.A}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\mathrm{fold}\circ\mathbf{{\llbracket q\rrbracket}}_{x}\\\
{\llbracket\Phi;\mathbf{\Gamma\vdash\textbf{unfold}\ q:A[\mu
X.A/X]}\rrbracket}\\\ \quad\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\mathrm{unfold}\circ\mathbf{{\llbracket
q\rrbracket}}_{x}\\\\[1.93748pt] {\llbracket\Phi;\cdot\vdash\mathbf{init}\
m:\mathbf{O}\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto r^{-1}({\llbracket m\rrbracket}_{x})\\\
{\llbracket\Phi;\mathbf{\Gamma_{1},\Gamma_{2}}\vdash\mathbf{let}\
x=\text{lift}\ \mathbf{q}\ \mathbf{in\ r}:\mathbf{A}\rrbracket}\\\
\quad\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}x\mapsto\widehat{\mathbf{{\llbracket
r\rrbracket}}}_{x}\circ(\mathbf{{\llbracket
q\rrbracket}}_{x}\otimes\mathrm{id}_{\mathbf{{\llbracket\Gamma_{2}\rrbracket}}})\\\
\end{array}$ Figure 16. Interpretation of quantum term judgements.

${\llbracket\Phi\vdash[\lvert\psi\rangle,\ell,\mathbf{q}]:\mathbf{A};\textnormal{{qbit}}^{k}\rrbracket}\colon{\llbracket\Phi\rrbracket}\to\mathbf{Q}(\mathbb{C},{\llbracket\mathbf{A}\rrbracket}\otimes{\llbracket\textnormal{{qbit}}^{k}\rrbracket})::x\mapsto(\mathbf{{\llbracket
q\rrbracket}}_{x}\otimes\mathrm{id}_{{\llbracket\textnormal{{qbit}}^{k}\rrbracket}})\circ\sigma_{\ell}\circ\text{state}_{\lvert\psi\rangle\langle\psi\rvert}^{\ddagger}$

Figure 17. Interpretation of quantum configurations.

$\displaystyle\mathrm{fold}_{\mathbf{\mu X.A}}$
$\displaystyle:\mathbf{{\llbracket A[\mu
X.A/X]\rrbracket}}=\mathbf{{\llbracket X\vdash
A\rrbracket}}\mathbf{{\llbracket\mu X.A\rrbracket}}\cong\mathbf{{\llbracket\mu
X.A\rrbracket}}:\mathrm{unfold}_{\mathbf{\mu X.A}}$
$\displaystyle\mathrm{fold}_{\mu X.P}$ $\displaystyle:{\llbracket P[\mu
X.P/X]\rrbracket}={\llbracket X\vdash P\rrbracket}{\llbracket\mu
X.P\rrbracket}\cong{\llbracket\mu X.P\rrbracket}:\mathrm{unfold}_{\mu X.P}$

Figure 18. Definition of the folding/unfolding isomorphisms.

######  Proposition 7.1.1.

The assignments $\mathbf{{\llbracket\Theta\vdash A\rrbracket}}\colon\
\mathbf{Q}_{*}^{|\mathbf{\Theta}|}\to\mathbf{Q}_{*}$ and
${\llbracket\Theta\vdash P\rrbracket}\colon\
\mathbf{PD}_{e}^{|\Theta|}\to\mathbf{PD}_{e}$ are well-defined
$\omega$-cocontinuous functors.

###### Proof.

By induction using Propositions 6.1.4, 6.1.6 and 6.2.7. ∎

######  Lemma 7.1.2 (Substitution).

Given quantum types $\mathbf{\Theta,X\vdash A}$ and $\mathbf{\Theta\vdash B}$
and classical types $\Theta,X\vdash P$ and $\Theta\vdash R$, then:

$\displaystyle\mathbf{{\llbracket\Theta\vdash
A[B/X]\rrbracket}}=\mathbf{{\llbracket\Theta,X\vdash
A\rrbracket}}\circ\langle\mathrm{Id},\mathbf{{\llbracket\Theta\vdash
B\rrbracket}}\rangle\quad\text{and}\quad{\llbracket\Theta\vdash
P[R/X]\rrbracket}={\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle\mathrm{Id},{\llbracket\Theta\vdash
R\rrbracket}\rangle.$

For closed recursive types, the folding/unfolding isomorphisms are defined in
Figure 18, where the equalities are from Lemma 7.1.2 and the unnamed
isomorphisms are the initial algebras. Note that $\mathrm{fold}_{\mu X.P}$ and
$\mathrm{fold}_{\mathbf{\mu X.A}}$ are isomorphisms in $\mathbf{TD}$ and
$\mathbf{Q}_{*}$, respectively. Now, the derived equations in Figure 18 follow
immediately.

####  7.1.1. Relationship Between Observable Types

Quantum/classical observable types play a special role in our language and
they also satisfy a special denotational relationship that we now describe.

######  Proposition 7.1.3.

Let $\mathbf{O}$ be a closed quantum observable type with $|\mathbf{O}|$ its
classical counterpart. Then there exists a canonical _set_
${\llparenthesis\mathbf{O}\rrparenthesis}$, defined by induction on the
derivation of $\cdot\vdash\mathbf{O}$, such that: (1)
${\llbracket\mathbf{O}\rrbracket}\cong\ell^{\infty}{\llparenthesis\mathbf{O}\rrparenthesis}$
in $\mathbf{Q}_{*}$; and (2)
${\llbracket|\mathbf{O}|\rrbracket}=\mathcal{L}{\llparenthesis\mathbf{O}\rrparenthesis},$
where $\mathcal{L}:\mathbf{Set}\to\mathbf{DCPO}$ is the obvious left adjoint
functor that equips a set $X$ with the discrete order.

###### Proof.

Both of these statements follow as special cases of the abstract categorical
semantics in (Lindenhovius et al., 2021, 2019, Section 6), where the source
category is $\mathbf{Set}$ and the target one is $\mathbf{Q}_{*}$ and
$\mathbf{TD}$, respectively (note that $\mathbf{TD}\cong\mathbf{DCPO},$ so
$\mathbf{DCPO}$ can also be taken). ∎

######  Remark 7.1.4.

The coherence conditions outlined in (Lindenhovius et al., 2021, 2019) are
very strong and the functor $\ell^{\infty}:\mathbf{Set}\to\mathbf{Q}_{*}$ is a
fully faithful strong symmetric monoidal left adjoint (just like
$\mathcal{L})$. To avoid notational overhead, we treat the $*$-isomorphism in
(1) above as an equality.

Proposition 7.1.3 shows that the interpretation of any classical observable
type is a _discrete domain_ and the set
${\llparenthesis\mathbf{O}\rrparenthesis}$ is simply its underlying set. We
may safely extend the action of the functor $\ell^{\infty}$ to discrete dcpo’s
and then by the above remark it follows that observable types are related by
the following strong relationship:

(7.1)
${\llbracket\mathbf{O}\rrbracket}=\ell^{\infty}({\llbracket|\mathbf{O}|\rrbracket}).$

This shows the interpretation ${\llbracket\mathbf{O}\rrbracket}$ of a quantum
observable type $\mathbf{O}$ is a _commutative_ HA-algebra.

###  7.2. Interpretation of Terms and Quantum Configurations

A classical context $\Phi=x_{1}\colon P_{1},\ldots,x_{n}\colon P_{n}$ is
interpreted as the dcpo
${\llbracket\Phi\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}{\llbracket P_{1}\rrbracket}\times\cdots\times{\llbracket
P_{n}\rrbracket},$ and a quantum context $\mathbf{\Gamma=x_{1}\colon
A_{1},\ldots,x_{n}\colon A_{n}}$ is interpreted as the HA algebra
$\mathbf{{\llbracket\Gamma\rrbracket}\stackrel{{\scriptstyle\textrm{{\scriptsize
def}}}}{{=}}{\llbracket A_{1}\rrbracket}\otimes\cdots\otimes{\llbracket
A_{n}\rrbracket}}$. The interpretation of classical/quantum term judgements
and quantum configurations is defined by mutual induction in Figures 18, 18
and 18. Next, we explain some of the notation used therein.

The interpretation of a classical term judgement $\Phi\vdash m\colon P$ is a
morphism ${\llbracket\Phi\vdash m\colon
P\rrbracket}\colon{\llbracket\Phi\rrbracket}\mathbin{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{2.0}{.}\cr\kern-3.01385pt\cr$\to$\cr}
}}{\llbracket P\rrbracket}$ in $\mathbf{DCPO}_{\mathcal{M}}$ that we often
abbreviate by writing ${\llbracket m\rrbracket}$. Likewise, a quantum term
judgement $\Phi;\mathbf{\Gamma\vdash q:A}$ is interpreted as a morphism
${\llbracket\Phi;\mathbf{\Gamma\vdash
q:A}\rrbracket}\colon{\llbracket\Phi\rrbracket}\to\mathbf{Q}({\llbracket\mathbf{\Gamma}\rrbracket},{\llbracket\mathbf{A}\rrbracket})$
in $\mathbf{DCPO}$ that we often abbreviate by writing $\mathbf{{\llbracket
q\rrbracket}}$. For an element $x\in{\llbracket\Phi\rrbracket}$, we also write
$\mathbf{{\llbracket q\rrbracket}}_{x}$ and ${\llbracket m\rrbracket}_{x}$ as
a shorthand for $\mathbf{{\llbracket q\rrbracket}}(x)$ and ${\llbracket