Dieses Kapitel präsentiert einen bahnbrechenden Ansatz zur Quantenprogrammierung, indem es Quanten- und klassische Kontrollparadigmen kombiniert. Sie führt eine Quantenlambda-Kalkulation ein, die reine Quantenkontrolle mit klassischer Kontrolle verbindet und die Darstellung sowohl reiner als auch gemischter Quantenberechnungen ermöglicht. Das Kapitel vertieft die Syntax und Semantik dieses integrierten Ansatzes und betont die Verwendung von Quantenkonfigurationen und einheitlichen Permutationen zur Steuerung von Quantenzuständen und -operationen. Es untersucht auch die operationelle Semantik des Kalküls und zeigt, wie Quantenkonfigurationen reduziert und manipuliert werden können. Die denotationale Semantik der Berechnung wird diskutiert und zeigt, wie die Integration von Quanten- und klassischer Steuerung innerhalb des Heisenberg-Bildes der Quantenmechanik interpretiert werden kann. Das Kapitel schließt mit einem detaillierten Beispiel einer Quantenbegehungssuche, das die praktischen Anwendungen des vorgeschlagenen Rahmenwerks veranschaulicht. Insgesamt bietet dieses Kapitel einen tiefen Einblick in die theoretischen und praktischen Aspekte der Kombination von Quanten- und klassischer Steuerung in Quantenprogrammiersprachen und bietet wertvolle Erkenntnisse zur Weiterentwicklung der Quantencomputertechnologie.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
The two main notions of control in quantum programming languages are often referred to as “quantum” control and “classical” control. With the latter, the control flow is based on classical information, potentially resulting from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on pure quantum computation and there the “control” is based on superposition. The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are: (1) syntactically: a modality for incorporating pure quantum types into a mixed state quantum type system; (2) operationally: an adaptation of the notion of “quantum configuration” from quantum lambda-calculi, where the quantum data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.
There are two important paradigms in the design of quantum programming languages – “classical control” and “quantum control”. In the classical control approach (e.g., [6, 13, 17, 19‐21]) the control flow of a program is conditioned on classical information that may result from quantum measurements. Type systems for quantum programming languages that are based on classical control are able to represent a variety of effects, e.g., quantum state preparation, state evolution through the application of unitary operators, and probabilistic effects induced by quantum measurements. Because of this, it is natural to conceptualise such lambda-calculi using quantum structures and models that are suited to describing mixed-state quantum computation and information (e.g., density matrices, superoperators). In the quantum control approach (e.g., [1, 10, 11, 18, 23]), one usually places an emphasis on pure state quantum computation and more specifically on superposition of terms, pure quantum states and unitary operators. In approaches that utilise classical control, one often starts with a selection of constants that represent some unitary operators (e.g., Hadamard, CNOT) and more complex unitary operations can be described in a circuit-like fashion by composing the atomic unitaries in a suitable way. Whereas in the quantum control approach, unitary operators are defined through more fundamental primitives that do not require the programmer to specify a circuit-like decomposition of the unitary operation. Because of this, a considerable economy in terms of syntax can be achieved with quantum control. For example, consider the circuit in Figure 1. It uses the well-known Toffoli gate, which would have to be decomposed as a large circuit like the one in the figure. However, the program representing this circuit can instead be written as a simple lambda term in our language given in Figure 1, where \(\textit{Tof} \triangleq \mathcal {B}(\textrm{ctrl}~\textrm{CNOT})\). To highlight this further note that the controlled Hadamard can be defined similarly to the Toffoli in our language, but a typical classically controlled quantum programming language would require two H gates, six T gates and one CNOT gate. Thus, our language offers an ease of writing programs by abstracting away quantum circuits. We aim to shift focus from drawing quantum circuits, which is a more low-level approach to writing code, to writing programs directly using syntax, which is a more high-level approach. In classical (non-quantum) programming, we can use high-level languages to write algorithms without having to specify boolean circuits or to encode integers using tuples of bits/booleans. With our paper, we are trying to advance quantum programming abstractions towards such a direction. For example, an individual qnat \(\left| n \right\rangle \) can be used instead of a tensor of qubits \(\left| q_1q_2...q_k \right\rangle \) whose binary encoding corresponds to n. We view boolean circuits and binary encodings of integers as low-level and likewise for their quantum counterparts. Our aim is to develop higher-level quantum abstractions.
Fig. 1.
A program and the corresponding circuit
Our Contributions Because of the potential presence of quantum entanglement, it is impossible (in general) to decompose a quantum state into a non-trivial tensor product of two smaller quantum states. Indeed, in the quantum lambda-calculus (QLC) [15], which is based on classical control, the type \({\textbf {qbit}}\) of qubits is an opaque type in the sense that there are no closed values of such a type. Program states may be described via quantum configurations which are triples \((\left| \psi \right\rangle , \ell , M)\), where \(\left| \psi \right\rangle \in \mathbb C^{2^n}\) is a pure quantum state (possibly entangled); M is a program possibly containing free variables of type \({\textbf {qbit}}\); \(\ell \) is a linking function that maps the free quantum variables of M to appropriate components of the state \(\left| \psi \right\rangle \). It is possible to also view \(\ell \) as a unitary permutation acting on \(\left| \psi \right\rangle \) and this view is important for our development. Such configurations, even though they are not part of the user-facing syntax, allow us to reason about entangled states and the operational semantics are described via a relation \((\left| \psi \right\rangle , \ell ,~\hbox {M)} \rightarrow _p (\left| \psi ' \right\rangle , \ell ', M')\), with p the probability of reduction.
Anzeige
The main idea that allows us to combine both quantum and classical control is to modify the quantum configurations described above by replacing the quantum state \(\left| \psi \right\rangle \) with a suitable pure quantum term\(\boldsymbol{t}\) and to replace the linking function \(\ell \) with a suitable unitary permutation\(u_\sigma \), where both \(\boldsymbol{t}\) and \(u_\sigma \) are syntactic constructs from our pure quantum language that may be assigned types.
In order to accurately model the situation with the QLC, the term \(\boldsymbol{t}\) has to correspond to a normalised vector and we replace the unitary constants from the QLC with programmable unitary constructs, so the pure subsystem also has to ensure their unitarity. Our pure subsystem is based on ideas described in [3, 18], but we further build on this by introducing an equational theory for our pure subsystem, which has unique normal forms and we describe a denotational semantics for it that is sound and complete with respect to the equational theory.
Next, we integrate the pure quantum subsystem into our main calculus, which allows us to describe both quantum and classical information and, therefore also classical control. This is a variant of the QLC with the addition of a modality \(\mathcal {B}(\boldsymbol{Q})\) which allows us to view pure quantum types \(\boldsymbol{Q}\) as types of mixed state quantum operations in the Heisenberg picture. The intuition behind this is the following: mixed states in the Schrödinger picture can be seen as CPTP maps1\((1 \mapsto \rho ) :\mathbb C \rightarrow \mathcal {T}(H)\) whereas mixed states in the Heisenberg picture are given by functionals of the form \(\textrm{tr}(\rho -) :\mathcal {B}(H) \rightarrow \mathbb C, \) both of which are determined by a choice of density operator \(\rho :H \rightarrow H\) (see [5, Section 7] for detail on this matter). This modality allows us to replace the constants for state preparation and unitaries acting on qubits in the QLC with terms and expressions from the pure subsystem acting on more general quantum types beyond qubits. The operational semantics are described via a suitable adaptation of the aforementioned quantum configurations. The denotational semantics follows previous work on quantum programming semantics based on von Neumann algebras [6, 13, 17] and we show, in addition, that the assignment \(\mathcal {B}(-)\) may be extended to a strict monoidal functor (between the relevant categories of Hilbert spaces and von Neumann algebras) that is crucial for our denotational semantics.
Overall, the two main contributions of our work are: (1) we show that quantum and classical control can be combined in a syntactic, operational and denotational sense by integrating a pure quantum control subsystem as part of the meta-theory and syntax of a quantum lambda-calculus; (2) an equational theory for a (sub)system for quantum control with unique normal forms and a sound and complete denotational semantics. Some supplementary material including extra examples, proofs, and complete figures for formation rule predicates are provided in Appendix.
Fig. 2.
A comparison of some quantum programming languages.
Anzeige
Related Work We begin by commenting on semantic approaches to classical control. In [15], the authors describe a QLC where the higher-order primitives are interpreted using techniques from the semantics of quantitative models of linear logic. In [7, 8, 24], the author(s) work with QLCs whose denotational semantics is given via game semantics. More recently, in [22], the authors have shown how to interpret a QLC with recursive types using presheaves that are enriched over a suitable base category and they also prove full abstraction. The approach that we use in this paper is based on von Neumann algebras which have been previously used for the semantics of quantum programming languages [6, 13, 17]. In particular, if we disregard the interaction between the pure subsystem and the main calculus, then our denotational model for the main calculus coincides with the one in [6]. The reason that we choose von Neumann algebras over the other approaches is because we think this gives the model which is the closest to mathematical physics out of the ones mentioned. Furthermore, our primary focus is not on developing the semantics of the classical paradigm; instead it is on the interaction between the pure quantum control subsystem and the main calculus based on classical control. Another distinguishing feature of our system, compared to the ones above, is the addition of types such as \(\mathcal {B}({{\textbf {qnat}}})\) which allow us to describe states in infinite-dimensional Hilbert spaces, such as \(\ell ^2(\mathbb N)\), and which we do not think can be easily included using the other approaches.2 For the quantum control paradigm, relevant work includes [1, 2, 9‐11]. What all these approaches have in common is that they have specific terms in their syntax for representing superposition. However, these approaches do not ensure unitarity of the relevant function spaces, in general. Our approach, instead, is based on related work first described in [18] and then later in [3]. One of the most distinctive features of this approach to quantum control is that the terms that introduce superposition are subject to strict formation conditions that ensure (linear algebraic) normalisation of the corresponding vectors. Furthermore, this approach to quantum control also imposes strict admissibility criteria on the unitary function spaces that can be formed through the type system and this ensures unitarity of the relevant expressions. Because of these considerations, we choose this approach to model quantum control in our pure subsystem. However, we have made some changes, in particular, we replace the operational semantics from these works with an equational theory instead. This works better for our approach to combining quantum and classical control within the quantum configurations (in QLCs the quantum data is considered modulo equality). We continue building on this development by describing a denotational semantics that is sound and complete with respect to the equational theory. This is the first such result for languages with quantum control.
Another paper which combines quantum and classical control is Qunity [25]. However, compared to our work, Qunity does not have an operational semantics, but instead there is a compilation procedure to quantum circuits. Furthermore, the denotational semantics of Qunity: (1) does not ensure unitarity and normalisation of the pure primitives in its language, whereas ours does; (2) does not ensure trace-preservation of the mixed primitives in the Schrödinger picture, whereas ours does indeed ensure unitality of the mixed primitives in the Heisenberg picture (which corresponds to trace-preservation under the Heisenberg-Schrödinger duality). Other differences include that Qunity is restricted to finite-dimensional quantum data and they do not have higher-order lambda abstractions for dealing with mixed-state primitives. Instead, Qunity relies on a try-catch mechanism to combine quantum and classical control, whereas our approach is based on quantum configurations. The table in Figure 2 gives a comparison of our work with other quantum programming languages. Normalised quantum terms refers to the property that terms representing pure/mixed quantum states always correspond to complex vectors with norm one/density operators with trace one. Adequacy refers to the property that two observationally distinct programs have distinct denotational interpretations.
2 Quantum Control
This part is adapted from one of the authors’ PhD thesis [14, Chapter 3], to which we refer the readers for full detail and proofs.
We write \(\textbf{Unitary}\subseteq \textbf{Isometry}\subseteq \textbf{Hilb}\) for the (sub)categories whose objects are the Hilbert spaces and whose morphisms are the unitaries (resp. isometries, bounded linear maps) between them.
2.1 Pure Quantum Syntax
We begin by describing a subsystem for quantum control. The syntax is based on symmetric pattern-matching [18]. The pure quantum types are given by the following grammar: \( \boldsymbol{Q}~::=~ \boldsymbol{I}\mid \boldsymbol{Q}_1 \boldsymbol{\otimes }\boldsymbol{Q}_2 \mid \boldsymbol{Q}_1 \boldsymbol{\oplus }\boldsymbol{Q}_2 \mid {\textbf {qnat}}. \)
We interpret every quantum type as a separable Hilbert space: the unit type is interpreted as \({\llbracket \boldsymbol{I} \rrbracket }\triangleq \mathbb C\); pair types are interpreted as tensor products; (quantum) sum types are interpreted as direct sums; finally, \({\llbracket {\textbf {qnat}} \rrbracket }\triangleq \ell ^2(\mathbb N)\). The type of qubits may be defined as \({\textbf {qbit}}\triangleq \boldsymbol{I}\boldsymbol{\oplus }\boldsymbol{I}.\) We write \({\textbf {qbit}}^{{n}}\) for the n-fold tensor product \({\textbf {qbit}}\boldsymbol{\otimes }\cdots \boldsymbol{\otimes }{\textbf {qbit}}\). The Hilbert space \(\ell ^2(\mathbb N)\) allows us to form superpositions with respect to a countable orthonormal basis (e.g., ). We may think of \(\ell ^2(\mathbb N)\) as a quantum analogue of the natural numbers, to abstract from qubit-level computation. The addition of \({\textbf {qnat}}\) allows us to reason about pure quantum computation while abstracting away from quantum circuits.
The unitary types, written as \(U(\boldsymbol{Q}_1,\boldsymbol{Q}_2)\), represent the unitary function spaces of our language. They are not interpreted as Hilbert spaces, but as sets of unitary operators: \({\llbracket U(\boldsymbol{Q}_1,\boldsymbol{Q}_2) \rrbracket } \triangleq \{~\hbox {u} :{\llbracket \boldsymbol{Q}_1 \rrbracket }\rightarrow {\llbracket \boldsymbol{Q}_2 \rrbracket }\ |\ u is a unitary operator \}\).
We now describe the language of the pure quantum subsystem whose grammar is given in Figure 3. (Pure) \({\boldsymbol{Terms}}\)\(\boldsymbol{t}\) are written in bold notation in order to distinguish with other syntactic constructs. The symbols \(\boldsymbol{x}, \boldsymbol{y}, \boldsymbol{z}\) denote pure quantum variables. We write \(\textbf{inl}_{\boldsymbol{Q}_1 \boldsymbol{\oplus }\boldsymbol{Q}_2}{\;\boldsymbol{t}}\) and \(\textbf{inr}_{\boldsymbol{Q}_1 \boldsymbol{\oplus }\boldsymbol{Q}_2}{\;\boldsymbol{t}}\) for sum type injections, and, for brevity, we often omit writing the subscripts. The term \(\boldsymbol{t}_1 \boldsymbol{\otimes }\boldsymbol{t}_2\) is used for forming pairs of terms. The terms \({\textbf {0}}\) and \({\textbf {S}}{\;\boldsymbol{t}}\) represent the qnat \(\left| 0 \right\rangle \) and the qnat \(\left| n+1 \right\rangle \), provided that \(\boldsymbol{t}\) represents the qnat \(\left| n \right\rangle \). We define \(\left| \underline{{\textbf {n}}} \right\rangle \triangleq {\textbf {S}}^{{\textbf {n}}}\ {\textbf {0}}\) and \(\left| \underline{{{\boldsymbol{t}} {\textbf {+n}}}} \right\rangle \triangleq {\textbf {S}}^{{\textbf {n}}}\ \boldsymbol{t}\), for \({\textbf {n}} \in \mathbb {N}\). The term \(u\, \boldsymbol{t}\) represents the application of a unitary \(u\) to a term \(\boldsymbol{t}\). Superpositions are represented by the term \({\sum }_{i \in \mathcal {I}} \boldsymbol{\alpha }_i \boldsymbol{\cdot }\boldsymbol{t}_i\). We impose strict conditions on these terms that ensure normalisation in §2.2.
Fig. 3.
Term grammar for the pure quantum subsystem.
In Figure 3, the \({\boldsymbol{Basis Terms}}\) (ranged over by symbols \(\boldsymbol{b},\boldsymbol{b}_i\)) are the simplest kind of pure terms. The (pure) \({\boldsymbol{Values}}\), ranged over by \(\boldsymbol{v}\) and defined in Figure 3, are the normal forms in this subsystem. They are of the form \(\sum _{i \in \mathcal {I}} \boldsymbol{\alpha }_i \boldsymbol{\cdot }\boldsymbol{b}_i\), where \(\boldsymbol{\alpha }_i \in \mathbb C,\)\(\boldsymbol{b}_i\) are basis terms, and \(\mathcal {I}\) is a finite index set. We consider \(\mathcal {I}\) as a totally ordered set so that we can work with unique normal forms. We also write \(\boldsymbol{\alpha }_1 \boldsymbol{\cdot }\boldsymbol{b}_1 + \cdots + \boldsymbol{\alpha }_n \boldsymbol{\cdot }\boldsymbol{b}_n\) for \(\sum _{i \in \{1, \ldots , n\}} \boldsymbol{\alpha }_i \boldsymbol{\cdot }\boldsymbol{b}_i.\) The formation conditions (§2.2) ensure that all terms in the sums are pairwise distinct, orthogonal, and of the same type, and thus well-formed values correspond to normalised vectors. In our equational theory, every quantum term \(\boldsymbol{t}\) can be rewritten to a normalised pure value \(\boldsymbol{v}\) (Proposition 3). The values are the canonical forms of this subsystem.
Example 1
The basis term \(\boldsymbol{*}:\boldsymbol{I}\) represents the complex scalar \(1 \in \mathbb C\). The basis terms that represent the computational basis for qubits can be defined by \(\boldsymbol{\left| 0 \right\rangle } \triangleq \textbf{inl}{\;\boldsymbol{*}} :{\textbf {qbit}}\) and \(\boldsymbol{\left| 1 \right\rangle } \triangleq \textbf{inr}{\;\boldsymbol{*}} :{\textbf {qbit}}.\) Other basis terms that can be defined include \(\boldsymbol{\left| 00 \right\rangle } \triangleq \boldsymbol{\left| 0 \right\rangle } \boldsymbol{\otimes }\boldsymbol{\left| 0 \right\rangle } :{\textbf {qbit}}^{{2}}\) and \(\boldsymbol{\left| 11 \right\rangle } \triangleq \boldsymbol{\left| 1 \right\rangle } \boldsymbol{\otimes }\boldsymbol{\left| 1 \right\rangle } :{\textbf {qbit}}^{{2}}\). If \(\boldsymbol{b}\) is a basis term, we often write it as \(\boldsymbol{\left| b \right\rangle }\) to distinguish it from other (non-basis) terms, e.g., \(\boldsymbol{\left| \underline{{\textbf {2}}} \right\rangle } :{\textbf {qnat}}\) represents the qnat \(\left| 2 \right\rangle \in \ell ^2(\mathbb N).\) Single-qubit states may be defined by . (Entangled) quantum states can be defined, e.g., . Linear combinations of qnats can also be written in the language, i.e.
Next, we describe the \({\boldsymbol{Unitaries}}\)\(u\) of Figure 3. Unitary pattern-matching\(\left\{ ~\mid \boldsymbol{b}_1 \mapsto \boldsymbol{v}_1\ \dots \mid \boldsymbol{b}_n \mapsto \boldsymbol{v}_n~ \right\} \) allows us to build unitary maps out of basis terms and values: every closed basis term \(\boldsymbol{b}_i\) is mapped to the closed value \(\boldsymbol{v}_i\); basis terms with free variables \(\boldsymbol{b}_i\) determine a mapping through the use of substitution with respect to the corresponding value \(\boldsymbol{v}_i\), wherein both \(\boldsymbol{b}_i\) and \(\boldsymbol{v}_i\) have the same free variables occurring within them, and the induced mapping is determined by performing all possible substitutions of the free variables on both sides with the same closed basis terms. The formation conditions (§2.2) ensure that the basis terms \(\boldsymbol{b}_i\) (resp. the values \(\boldsymbol{v}_i\)) determine an ONB for the type \(\boldsymbol{Q}_1\) (resp. \(\boldsymbol{Q}_2\)) and therefore \(\left\{ ~\mid \boldsymbol{b}_1 \mapsto \boldsymbol{v}_1\ \dots \mid \boldsymbol{b}_n \mapsto \boldsymbol{v}_n~ \right\} \) determines a unitary map. We introduce syntactic sugar for quantum if statements, written \({\textbf {qif}}\). If \(u_1\) is of the form \(\left\{ ~\mid \boldsymbol{b}_1 \mapsto \boldsymbol{v}_1\ \dots \mid \boldsymbol{b}_n \mapsto \boldsymbol{v}_n~ \right\} \) and \(u_2\) of the form \(\left\{ ~\mid \boldsymbol{b}'_1 \mapsto \boldsymbol{v}'_1\ \dots \mid \boldsymbol{b}'_m \mapsto \boldsymbol{v}'_m~ \right\} \) then \(\textbf{qif}~\boldsymbol{x}~\textbf{then}~\boldsymbol{x} \boldsymbol{\otimes }u_2~\textbf{else}~\boldsymbol{x} \boldsymbol{\otimes }u_1\) is short for the unitary:
Example 2
The unitaries \(\textrm{Had}\) and \(\textrm{CNOT}\) below encode the standard Hadamard and CNOT gates, respectively. \(\textrm{CNOT}\) makes use of some simple pattern-matching on its last line: it can match either with \(\left| {\boldsymbol{0}} \right\rangle \boldsymbol{\otimes }\left| {\boldsymbol{0}} \right\rangle \) or with \(\left| {\boldsymbol{0}} \right\rangle \boldsymbol{\otimes }\left| {\boldsymbol{1}} \right\rangle \). The unitary \(\textrm{Had}_{{\textbf {qnat}}} \) defines an extension of the Hadamard gate on the space \(\ell ^2(\mathbb N)\).
The remaining expressions for forming unitaries are easy to understand: \(u_2 \circ u_1\) represents composition of unitaries, \(u^*\) represents the adjoint of a unitary, \(u_1 \otimes u_2\) and \(u_1 \oplus u_2\) represent tensor products and direct sums of unitaries, and finally, \(\textrm{ctrl}\ u\) represents a qubit-controlled unitary operator. For simplicity, we sometimes write \(\{\ldots \mid \! {\boldsymbol{b}_i} \mapsto {\boldsymbol{v}_i} \ldots \}\) as a shorthand notation for the unitary \(\left\{ ~\mid \boldsymbol{b}_1 \mapsto \boldsymbol{v}_1\ \dots \mid \boldsymbol{b}_n \mapsto \boldsymbol{v}_n~ \right\} \), when n is clear from context or unimportant. We also point out that unitaries depend only on values and basis terms and that general pure terms cannot be used for the construction of unitaries.
2.2 Formation Conditions
In order to guarantee (linear-algebraic) normalisation for quantum terms and unitarity for functions, we rely on formulating: (1) a suitable orthogonality relation\(\perp \ \subseteq {\boldsymbol{Terms}}\times {\boldsymbol{Terms}}\), which is used as part of the formation condition of some terms; (2) additional predicates \(\textrm{ONB}_{\boldsymbol{Q}} \) and \(\textrm{ONB}^{val }_{\boldsymbol{Q}} \) which ensure that a set of basis terms/values of type \(\boldsymbol{Q}\) determines an ONB which is used as part of the formation conditions for the atomic introduction rule of unitaries.
The relation \(\perp \) is defined as the smallest binary relation \(\perp \ \subseteq {\boldsymbol{Terms}}\times {\boldsymbol{Terms}}\) that is closed under the rules in Figure 4. Quantum terms that are orthogonal via this relation are orthogonal in a denotational sense as well (§2.3). This relation allows us to enforce the orthogonality of terms appearing within a superposition \(\sum _{i \in \mathcal I} (\boldsymbol{\alpha }_i \boldsymbol{\cdot }\boldsymbol{t}_i).\) Under the assumption that all terms \(\boldsymbol{t}_i\) represent normalised vectors that are pairwise orthogonal, the norm of the superposition is easy to calculate (statically), and it is given by \(\sum _{i \in \mathcal I} |\boldsymbol{\alpha }_i|^2\). This justifies the formulation of the introduction rule for superposition (Figure 6) and guarantees that the vector represented by this superposition of terms is normalised.
Fig. 4.
Rules for the orthogonality relation (excerpt).
Example 3
The rules for the orthogonality relation are not restricted to closed quantum terms, e.g., \({\textbf {0}}\perp {\textbf {S}}{\;\boldsymbol{x}}\) and \(\textbf{inl}{\;\boldsymbol{x}} \perp \textbf{inr}{\;\boldsymbol{y}}\). One can also show that \(\boldsymbol{\left| + \right\rangle } \perp \boldsymbol{\left| - \right\rangle }\) (defined in Example 1). However, we cannot show that \(\textrm{Had}\ \boldsymbol{\left| 0 \right\rangle } \perp \boldsymbol{\left| - \right\rangle }\) even though \(\textrm{Had}\ \boldsymbol{\left| 0 \right\rangle }\) is equal to \(\boldsymbol{\left| + \right\rangle }\) with respect to our equational logic and also with respect to our denotational semantics (both introduced later). The reason for this is that we wish to define the orthogonality relation statically.
In order to determine whether a finite set S of (potentially open) basis terms determines an ONB for a type \(\boldsymbol{Q}\), we introduce the orthonormal basis predicates\(\textrm{ONB}_{\boldsymbol{Q}}{(S)}\) in Figure 5, originally known as orthogonal decomposition [18]. Note that there is a mistake with the rule for the tensor product in the original paper, e.g. it does not allow for the typing of a CNOT.
Fig. 5.
Orthonormal basis predicates.
Given a type \(\boldsymbol{Q}\) and a finite set of basis terms S, we say that S determines an orthonormal basis of\(\boldsymbol{Q}\), which we write as \(\textrm{ONB}_{\boldsymbol{Q}}{(S)}\), if this can be derived via the rules in Figure 5. We now explain some of the notation used therein. If S is a set of the form \(\{ \boldsymbol{b}_1 \boldsymbol{\otimes }\boldsymbol{b}_1', \ldots , \boldsymbol{b}_n \boldsymbol{\otimes }\boldsymbol{b}_m' \}\) then we define \(\pi _1(S) \triangleq \{ \boldsymbol{b}_1 , \ldots , \boldsymbol{b}_n \}\) and \(\pi _2(S) \triangleq \{ \boldsymbol{b}_1', \ldots , \boldsymbol{b}_m' \}\). In this situation, we also define \(S^1_{\boldsymbol{b}} \triangleq \{ \boldsymbol{b}' \ |\ \boldsymbol{b}\boldsymbol{\otimes }\boldsymbol{b}' \in S \} \) and \(S^2_{\boldsymbol{b}'} \triangleq \{ \boldsymbol{b}\ |\ \boldsymbol{b}\boldsymbol{\otimes }\boldsymbol{b}' \in S \} . \) Furthermore, the \(\textrm{ONB}\) predicate implies pairwise orthogonality of the associated values. Note that the predicate \(\textrm{ONB}_{\boldsymbol{Q}}{(S)}\) is defined for a finite set S consisting of basis terms. But, in order to be able to define unitaries that make use of superposition, we also work with other ONBs. Given a finite set S consisting of values, we say that S determines an ONB of type \(\boldsymbol{Q}\), and we write \(\textrm{ONB}^{val }_{\boldsymbol{Q}}{(S)}\) to indicate this, whenever this can be derived via the rules in Figure 5. We also introduce syntactic sugar: the value \(\sum ^*_{i \in \mathcal I} \boldsymbol{\alpha }_i \boldsymbol{\cdot }\boldsymbol{b}_i\) is the finite linear combination where elements with scalar 0 are omitted. In other words, the indices \(i \in \mathcal I\) such that \(\boldsymbol{\alpha }_i = 0\) are ignored, e.g., if \(\boldsymbol{\alpha }_1 = 1\) and \(\boldsymbol{\alpha }_2 = 0\), \(\sum ^*_{i \in \{1,2\}} \boldsymbol{\alpha }_i \boldsymbol{\cdot }\boldsymbol{b}_i\) is the value \(\sum _{i \in \{*\}} 1 \boldsymbol{\cdot }\boldsymbol{b}_1\).
Example 4
For \({\textbf {qbit}}\), the rules from Figure 5 show that \(\textrm{ONB}_{{\textbf {qbit}}}{(\{ \boldsymbol{\left| 0 \right\rangle }, \boldsymbol{\left| 1 \right\rangle } \})}\) and that \(\textrm{ONB}^{val }_{{\textbf {qbit}}}{(\{\boldsymbol{\left| + \right\rangle }, \boldsymbol{\left| - \right\rangle } \})}\) hold (with \(\boldsymbol{\left| \pm \right\rangle }\) defined in Example 1). We also have that \(\textrm{ONB}_{{\textbf {qbit}}}{(\{ \boldsymbol{x} \} )}\), where \(\boldsymbol{x}\) is a variable. In other words, we determine an ONB for the type \({\textbf {qbit}}\) by substituting \(\boldsymbol{x}\) with all possible closed computational basis terms of type \({\textbf {qbit}}\) (see Figure 3). For \({\textbf {qnat}}\), any set S with the property that \(\textrm{ONB}_{{\textbf {qnat}}}{(S)}\) holds, must contain a term that is not closed. We have that \(\textrm{ONB}_{{\textbf {qnat}}}{(\{ \boldsymbol{\left| \underline{{\textbf {x}}} \right\rangle }\} )}\), , and hold true and determine the same ONB for the type \({\textbf {qnat}}\) (it represents the computational basis of \(\ell ^2(\mathbb N)\)). The set used in the last predicate allows us to conclude that holds. This last set of values is used to type \(\textrm{Had}_{{\textbf {qnat}}}\) from Example 2.
Fig. 6.
Formation rules for terms and unitaries (excerpt).
Judgements for pure quantum terms have the form \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q}\) where \(\boldsymbol{\varGamma }\) stands for a linear context of the form \(\boldsymbol{\varGamma }\triangleq \boldsymbol{x}_1 :\boldsymbol{Q}_1, \ldots , \boldsymbol{x}_n :\boldsymbol{Q}_n \). The formation rules for terms are presented in Figure 6; the first two lines are standard for a linearly-typed term calculus. The rule for superposition depends on the orthogonality relation \(\perp \), and the premise ensures that the resulting superposition corresponds to a normalised vector. This is made precise later (Theorem 1). Finally, the formation rule for \(u\, \boldsymbol{t}\), i.e. the application of a unitary u to a term \(\boldsymbol{t}\), is akin to function application in lambda-calculi. However, the complexity is primarily relegated to the judgement \(\Vdash u :U(\boldsymbol{Q}_1, \boldsymbol{Q}_2)\), which ensures the unitarity of u.
The formation rules for unitaries are presented in Figure 6. In the introduction rule for atomic unitaries \(\left\{ ~\mid \boldsymbol{b}_1 \mapsto \boldsymbol{v}_1\ \dots \mid \boldsymbol{b}_n \mapsto \boldsymbol{v}_n~ \right\} \), we have that the potentially open basis terms \(\{ \boldsymbol{b}_1, \ldots , \boldsymbol{b}_n \}\) (resp. values \(\{ \boldsymbol{v}_1, \ldots , \boldsymbol{v}_n \}\)) determine an ONB for \(\boldsymbol{Q}_1\) (resp. \(\boldsymbol{Q}_2\)) in the sense explained above. Then the resulting bijective mapping that associates \(\boldsymbol{b}_i\) to \(\boldsymbol{v}_i\) uniquely determines a unitary. The formation rules for the remaining unitaries are straightforward, and they align easily with the mathematical intuition that motivates them. We also wish to note that unitaries do not depend on general terms (see Figure 3).
2.3 Denotational Semantics for Pure Quantum System
Recall (§2.1) that the interpretation of a pure quantum type \(\boldsymbol{Q}\) is a Hilbert space \({\llbracket \boldsymbol{Q} \rrbracket }\), i.e., an object of the category \(\textbf{Isometry}\), and the interpretation of a unitary type \(U(\boldsymbol{Q}_1, \boldsymbol{Q}_2)\) is the set \({\llbracket U(\boldsymbol{Q}_1,\boldsymbol{Q}_2) \rrbracket }\) of unitaries in \({\llbracket \boldsymbol{Q}_1 \rrbracket }\rightarrow {\llbracket \boldsymbol{Q}_2 \rrbracket }\).
A linear context is interpreted in the usual way \({\llbracket \boldsymbol{\varGamma } \rrbracket }\triangleq {\llbracket \boldsymbol{Q}_1 \rrbracket } \otimes \cdots \otimes {\llbracket \boldsymbol{Q}_n \rrbracket }\). The interpretation of a judgement \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q}\) is given by a morphism \({\llbracket \boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q} \rrbracket } \in \textbf{Isometry}({\llbracket \boldsymbol{\varGamma } \rrbracket }, {\llbracket \boldsymbol{Q} \rrbracket })\). We also sometimes abuse notation and write \({\llbracket \boldsymbol{t} \rrbracket }\) for brevity instead of \({\llbracket \boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q} \rrbracket }\). For closed quantum terms \(\cdot \boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q}\), we interpret the empty context as \(\mathbb C\) (the tensor unit in \(\textbf{Isometry}\)) and so we can identify \({\llbracket \cdot \boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q} \rrbracket }(1) \) with a normalised vector.
Every value \(\boldsymbol{v}\) is of the form \({\sum }_{i \in \mathcal I} \boldsymbol{\alpha }_i \boldsymbol{\cdot }\boldsymbol{b}_i\), but the sum is subject to strict admissibility conditions imposed by the orthogonality relation \(\perp \) from §2.2. The denotational significance of this relation is provided by the statement: given \(\boldsymbol{\varGamma }_1 \boldsymbol{\vdash }\boldsymbol{t}_1 :\boldsymbol{Q}\) and \(\boldsymbol{\varGamma }_2 \boldsymbol{\vdash }\boldsymbol{t}_2 :\boldsymbol{Q}\), if \(\boldsymbol{t}_1 \perp \boldsymbol{t}_2\) then \({\llbracket \boldsymbol{t}_1 \rrbracket }^*{\llbracket \boldsymbol{t}_2 \rrbracket } = 0_{{\llbracket \boldsymbol{\varGamma }_2 \rrbracket }, {\llbracket \boldsymbol{\varGamma }_1 \rrbracket }}\); which is central in proving that the interpretation of values is well-defined as isometries.
The most challenging unitaries to interpret are the unitary pattern-matchings, constructed through the use of basis terms and values (but not general terms). Another key role is played by the \(\textrm{ONB}_{\boldsymbol{Q}} \) and \(\textrm{ONB}^{val }_{\boldsymbol{Q}} \) predicates: they can be understood as determining suitable ONBs of the corresponding types. The denotational significance of these predicates is that they give us a resolution of the identity at type \(\boldsymbol{Q}\), as made precise by the following proposition.
Pattern-matching is then interpreted by \({\llbracket \Vdash \{\ldots \mid \! {\boldsymbol{b}_i} \mapsto {\boldsymbol{v}_i} \ldots \} \rrbracket } \triangleq {\sum }_{i} {\llbracket \boldsymbol{v}_i \rrbracket } \circ {\llbracket \boldsymbol{b}_i \rrbracket }^*\), and the previous proposition ensures it is unitary. Finally, we can show that the interpretation of all pure quantum terms is well-defined as isometries.
Theorem 1
If \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q}\), then \({\llbracket \boldsymbol{t} \rrbracket }\in \textbf{Isometry}({\llbracket \boldsymbol{\varGamma } \rrbracket }, {\llbracket \boldsymbol{Q} \rrbracket }).\)
Moreover, any canonical symmetric monoidal isomorphism can be represented by the unitaries of our language. The canonical symmetric monoidal isomorphisms are simply those that can be defined using the structure of a symmetric monoidal category only, i.e. isomorphisms that are given by: left and right unitors, symmetric swaps, associators, closed under composition and tensor products. We use this result later for quantum configurations.
Proposition 2
Let \(\boldsymbol{Q}_1\) and \(\boldsymbol{Q}_2\) be two pure types, and let \(f :\llbracket \boldsymbol{Q}_1 \rrbracket \rightarrow \llbracket \boldsymbol{Q}_2 \rrbracket \) be a canonical symmetric monoidal isomorphism. Then, there exists a unitary \(\Vdash u :U(\boldsymbol{Q}_1,\boldsymbol{Q}_2)\) such that \(\llbracket u \rrbracket = f\).
2.4 Equational Theory
We now describe the equational theory of the pure quantum subsystem. Given two pure quantum terms \(\boldsymbol{t}_1\) and \(\boldsymbol{t}_2\), we write \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}_1 = \boldsymbol{t}_2 :\boldsymbol{Q}\) to indicate that \(\boldsymbol{t}_1\) equals \(\boldsymbol{t}_2\) as terms of type \(\boldsymbol{Q}\) in context \(\boldsymbol{\varGamma }.\) As usual if \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}_1 = \boldsymbol{t}_2 :\boldsymbol{Q}\), the rules imply that \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}_1 :\boldsymbol{Q}\) and \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}_2 :\boldsymbol{Q}\). We now explain some of the more interesting rules in greater detail. The rules of the equational theory are divided into four groups. The first one is concerned with the usual rules for reflexivity, symmetry and transitivity. Secondly, we provide rules to handle linear algebraic identities, such as exchanging sums and the linearity of injections and unitaries; this also contains the rule \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\sum _{i=1}^1 1 \boldsymbol{\cdot }\boldsymbol{t}= \boldsymbol{t}:\boldsymbol{Q}\). A small excerpt is found below.
Congruence rules comprise the third group, e.g., \(\boldsymbol{\varGamma }\boldsymbol{\vdash }{\textbf {S}}{\;\boldsymbol{t}}_1 = {\textbf {S}}{\;\boldsymbol{t}}_2 :{\textbf {qnat}}\) given that \(\boldsymbol{\varGamma }\boldsymbol{\vdash }\boldsymbol{t}_1 = \boldsymbol{t}_2 :{\textbf {qnat}}\). Last but not least are the computational rules, which, read left to right, can be seen as providing an operational semantics. The most important rule and our version of \(\beta \)-reduction, is the rule for unitary pattern-matching applied to a basis term.
The formation conditions on unitary pattern-matching ensure that \(\textrm{ONB}_{\boldsymbol{Q}_1}{\left( \{\boldsymbol{b}_i\}_i \right) }\). With the latter, and given \(\cdot \boldsymbol{\vdash }\boldsymbol{b}' :\boldsymbol{Q}_1\), there exists a unique substitution \(\mathtt s \) and a unique \(\boldsymbol{b}_j\) such that \(\mathtt s (\boldsymbol{b}_j) = \boldsymbol{b}'\). The resulting term of the rule is then the same substitution applied to the corresponding output \(\boldsymbol{v}_j\). Such substitutions were first defined in [18], and can be deduced via an inference system.
Proposition 3
Given \(\cdot \boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q}\), there is a unique value \(\boldsymbol{v}\) s.t. \(\cdot \boldsymbol{\vdash }\boldsymbol{t}= \boldsymbol{v} :\boldsymbol{Q}\).
This proposition shows that pure terms have a unique normal form. It is crucial for the proof of the completeness theorem, and comes in handy in the rest of the paper, especially to define the reduction system for the main calculus (§3).
This section lays down the syntax and semantics of the main calculus, which combines the quantum control fragment with a classically controlled layer, a variant of a call-by-value linear lambda-calculus. The subsystem which we presented in the previous section is designed to represent pure quantum information and computation, whereas in this section, we are concerned with mixed quantum information and computation. Our denotational approach towards this uses von Neumann algebras, which provide an appropriate mathematical setting to achieve this treatment. Operationally, this is achieved by adapting the configurations (also called closures) \((\left| \psi \right\rangle , \ell , M)\) from an effectful quantum lambda-calculus, e.g., [6, 21], by replacing the quantum state \(\left| \psi \right\rangle \) with a pure term \(\boldsymbol{t}\), replacing the linking function \(\ell \) with a unitary u that can be described via our syntax and which represents a suitable permutation, and finally by defining suitable formation conditions for the configuration.
3.1 Syntax and Typing Rules
The types of the main calculus, ranged over by capital Latin letters (e.g., \(\mathrm A, \mathrm B\)) are given in Figure 7. All types except \(\textrm{Nat}\) and \(\mathcal B(\boldsymbol{Q})\) are standard in a system for a classical call-by-value linear lambda-calculus. \(\textrm{Nat}\) is a ground type representing classical natural numbers and \(\mathcal B(\boldsymbol{Q})\) is the type that represents mixed state quantum computation on the Hilbert space determined by the type \(\boldsymbol{Q}\). As we see later, this type plays an important role by introducing quantum and probabilistic effects into the system. The modality \(\mathcal B\) is inspired from the denotational model, where \(\mathcal B(H)\) represents the von Neumann algebra of bounded operators on the Hilbert space H.
Fig. 7.
Syntax of the classically controlled system.
Terms (and values) of the calculus are described in Figure 7. The term \(\textit{pure}(\boldsymbol{t})\) models the preparation of a pure quantum state represented by the quantum term \(\boldsymbol{t}\). Measurement is modelled by the term meas(M). The term \(\mathcal {B}({u})(M)\) represents the application of the unitary \(u\) to a term M. Additionally, we have two syntactic constructs to model the isomorphism between the types \(\mathcal B(\boldsymbol{Q}_1 \boldsymbol{\otimes }\boldsymbol{Q}_2)\) and \(\mathcal B(\boldsymbol{Q}_1) \otimes \mathcal B(\boldsymbol{Q}_2)\): the term \(\textit{let}\ \mathcal {B}(z) = M\textit{ in } N\) allows one to construct a term of type \(\mathcal B(\boldsymbol{Q}_1 \boldsymbol{\otimes }\boldsymbol{Q}_2)\) from a term of type \(\mathcal B(\boldsymbol{Q}_1) \otimes \mathcal B(\boldsymbol{Q}_2)\) and the term \(\textit{let}\ \mathcal {B}(x \otimes y) = M\textit{ in } N\) deals with the opposite direction. This isomorphism arises because the functor \(\mathcal B(\cdot )\) used in the denotational model is strict monoidal. Both constructs are necessary to allow the language to manipulate composed quantum systems and also terms possibly representing entangled states.
Fig. 8.
Typing rules for terms (excerpt).
Typing contexts (ranged over by symbols \(\varDelta ,\Sigma _1, \Sigma _2\)) are finite sequences \(\varDelta \triangleq x_1: \mathrm A_1, \ldots , x_n : \mathrm A_n\) mapping variables to types. We use the notation \(!\varDelta \) for contexts of the form \(x_1:\ !\mathrm A_1, \ldots , x_n:\ !\mathrm A_n.\)Typing judgements have the form \(\varDelta \vdash M : \mathrm A\) and follow a linear typing discipline to deal with quantum data. The typing rules are given in Figure 8 where, as usual, \(\Sigma _1,\Sigma _2\) denotes the disjoint union of \(\Sigma _1\) and \(\Sigma _2\). Classical bits correspond to the type \(\textit{bit} \triangleq I + I\) and mixed state qubits have type \(\textit{qbit}\triangleq \mathcal B({\textbf {qbit}})\). The rule for the term \(\textit{pure}(\boldsymbol{t})\) introduces a state \(\boldsymbol{t}\) from the quantum control fragment as a term of type \(\mathcal B(\boldsymbol{Q})\) into the main calculus. The typing rule for measurement maps a term M of quantum type \(\mathcal B(\boldsymbol{Q})\) to a term \(\textit{meas}(M)\) of classical type \(\overline{\boldsymbol{Q}}\), where the type \(\overline{\boldsymbol{Q}}\) is defined inductively on the structure of the pure quantum type \(\boldsymbol{Q}\):
This gives the classical analogue of the type \(\boldsymbol{Q},\) e.g., \(\overline{{\textbf {qbit}}} = \textit{bit}.\) For a quantum basis term \(\boldsymbol{b}\) of type \(\boldsymbol{Q}\), \(\overline{\boldsymbol{b}}\) (defined below) denotes its translation to a classical value of type \(\overline{\boldsymbol{Q}}\), which we use to represent measurement outcomes.
3.2 Operational Semantics
Quantum configurations. We lay down the operational semantics of the calculus using an adaptation of the notion of a quantum configuration.
Definition 1
(Quantum Configuration). Let \(\texttt {Conf}\) be the set of quantum configurations\(\mathcal C \triangleq (\boldsymbol{t}, u_{\sigma } , M),\) where:
\(\boldsymbol{t}\in {\boldsymbol{Terms}}\) represents a pure quantum state;
\(u_{\sigma } \in {\boldsymbol{Unitaries}}\) represents a symmetric monoidal isomorphism;
\(M \in \textsc {Terms}\) is a term from the main calculus.
In the above definition, we can think of the quantum term \(\boldsymbol{t}\) as representing a quantum state, because the quantum control fragment ensures that \(\boldsymbol{t}\) can be rewritten (in its equational theory) to a unique quantum value (Proposition 3). Next, \(u_{\sigma }\) permutes the components of \(\boldsymbol{t}\) so that they appear in the same order as variables that represent them in M. We slightly abuse terminology and refer to \(u_{\sigma }\) as a permutation, but it is meant to be understood as a canonical symmetric monoidal isomorphism (see Proposition 2). If we fix the domain and codomain of \(u_\sigma \), then the essential data is given by a choice of permutation \(\sigma \) and this makes it easier to understand how each unitary acts on the coordinates, and the contextual rules formulation becomes precise. Note that, thanks to Proposition 2, the pure quantum syntax is expressive enough to represent all the monoidal permutations that we need in the sequel.
Example 5
Consider the quantum configuration \((\boldsymbol{t} , u_{id}, x \otimes y)\), where we have and \(u_{id} \triangleq \{ \mid \boldsymbol{*\otimes w \otimes z} \mapsto \boldsymbol{w \otimes z} \}\) is a unitary with type \(\Vdash u_{id} :U(\boldsymbol{I} \boldsymbol{\otimes }{\textbf {qbit}}\boldsymbol{\otimes }{\textbf {qbit}}, {\textbf {qbit}}\boldsymbol{\otimes }{\textbf {qbit}})\). It conveys the information that the variable x in \(x \otimes y\) keeps track of the first qubit in \(\boldsymbol{t}\) and that the variable y keeps track of the second one. Whereas in the configuration \((\boldsymbol{t} , u_{swap }, x \otimes y)\) with \(u_{swap } \triangleq \{ \mid \boldsymbol{*\otimes w \otimes z} \mapsto \boldsymbol{z \otimes w} \}\), the variable x keeps track of the second qubit and y of the first one. Note that, due to quantum entanglement, the term \(\boldsymbol{t}\) cannot be decomposed into a non-trivial tensor product, and the variables x and y should be thought of as identifying qubit components of \(\boldsymbol{t}\), instead of storing quantum data themselves.
A quantum configuration \(\mathcal V = (\boldsymbol{v}, u_{\sigma } , V)\), when both the quantum term \(\boldsymbol{v}\) and term V are values, is called a value configuration. For example, \((\left| 0 \right\rangle , u_{id} , x)\) is a value configuration. A quantum configuration \(\mathcal{S}\mathcal{V}= (\boldsymbol{v}, u_{\sigma } , M)\), where \(\boldsymbol{v}\) is a quantum value, is a semi-value configuration. We write \(\texttt {VConf}\) (resp. \(\texttt {SVConf}\)) for the set of (resp. semi-)value configurations. The reason we introduce semi-value configurations, is because they allow us to define our operational semantics for the main calculus modulo equality of the pure quantum terms \(\boldsymbol{t}\) (analogous to the quantum lambda-calculus). We already proved that values \(\boldsymbol{v}\) are normal forms for the pure terms (Proposition 3), so this makes them a natural choice.
Definition 2
A quantum configuration \((\boldsymbol{t}, u_{\sigma } , M)\) is well-formed with type \(\textrm{A}\), written as \( ( \boldsymbol{t}, u_{\sigma } , M ) :\textrm{A}\) if the following judgments can be derived:
We write \(\textrm{WF}_{X}(A)\) for the set of well-formed configurations in X with type \(\textrm{A}\), where \(X \in \{ \texttt {Conf}, \texttt {VConf}, \texttt {SVConf}\}\).
\(x: \mathcal B({\textbf {qbit}}^{{2}}) , y : \textit{qbit}\vdash x \otimes y: \mathcal B({\textbf {qbit}}^{{2}}) \otimes \textit{qbit}\).
In this configuration, \(u_\textrm{id}\) is just the identity, x points to the Bell state in \(\boldsymbol{t}\) whereas y points to \(\boldsymbol{\left| 0 \right\rangle }\). We have \(n=3,m=2\), with \(\boldsymbol{Q}_1 = \boldsymbol{Q}_2 = \boldsymbol{Q}_3 = {\textbf {qbit}}\), \(\boldsymbol{Q}_1'= {\textbf {qbit}}^{{2}}\) and \( \boldsymbol{Q}_2'= {\textbf {qbit}}\). The configuration is well-formed.
The above example highlights the need for m and n (from Definition 2) to be different values. The intuition behind this difference is that the unitary \(u_{\sigma }\) partitions the n quantum types into m blocks, where each block is represented by a variable in M. Furthermore, in situations where we wish to combine two such blocks which are not next to each other in the tensor expression of the n types, we allow the possibility of permuting these blocks and merging them so that now two blocks that were initially represented by two variables are represented by one. This is formally expressed in the reduction rules we define next. The role of \(u_{\sigma }\) in a well-formed configuration is illustrated in Figure 9. The small-step reduction\(\cdot \rightarrow _{\cdot } \cdot \subseteq \texttt {Conf}\times [0,1] \times \texttt {Conf}\) is the relation defined by the rules of Figure 10: the reduction \(\mathcal C \rightarrow _p \mathcal C'\) holds when the quantum configuration \(\mathcal C\) reduces to \(\mathcal C'\) with probability \(p \in [0,1]\).
Fig. 9.
Graphical representation of a well-formed quantum configuration.
The reduction rules along with the unitaries required to state them are given in Figure 10. \(\{\boldsymbol{b}_{ij} \}_{i,j}\) stand for basis terms and s in the reduction rule for \(\textit{meas}(x)\) corresponds to the position of \(\boldsymbol{b}_i\) in the tensor product appearing in the quantum term. All sums are finite. The unitary \(u_{\sigma _{gather}}\) appearing in the reduction rule for the term \(\textit{let}\ \mathcal {B}(z) = x \otimes y\textit{ in } N\) merges two consecutive variables into one block, so that now a single variable can represent it. Similarly, in the reduction rule for the term \(\textit{let}\ \mathcal {B}(x \otimes y) = z\textit{ in } N\), the unitary \(u_{\sigma _{divide}}\) partitions a block into two, so that two variables can represent them. The two rules are symmetric as expected, since these terms only allow switching between types \(\mathcal B(\boldsymbol{Q}_1 \boldsymbol{\otimes }\boldsymbol{Q}_2)\) and \(\mathcal B(\boldsymbol{Q}_1) \otimes \mathcal B(\boldsymbol{Q}_2)\). The last rule of Figure 10 is a contextual rule which holds for any evaluation contextE. Evaluation contexts are defined by the following grammar:
One of the premises of the contextual rule states that if \(\sigma \) is a permutation which does not act on the same set of indices as \(\sigma _1,\sigma _2\), then we can form a “union” of these permutations by composing an extension of the two. For a permutation \(\sigma : S \rightarrow S\), we can define its extension \(\sigma ^{ext} : S \sqcup S' \rightarrow S \sqcup S'\) by \(\sigma ^{ext}(s) \triangleq \sigma (s)\), if \( s \in S\), \(\sigma ^{ext}(s') \triangleq s'\), if \(s' \in S'\). We now introduce the reduction relation we use to define the operational semantics.
Fig. 10.
Reduction rules and their unitary permutations.
Definition 3
The reduction relation\(\cdot \leadsto _{\cdot } \cdot \subseteq \texttt {SVConf}\times [0,1] \times \texttt {SVConf}\) is defined in the following way: we write \((\boldsymbol{v} , u_{\sigma } , M) \leadsto _p (\boldsymbol{v}' , u_{\sigma '} , M')\) whenever
The intuition behind the above definition is that it allows us to reason modulo equality of the pure terms \(\boldsymbol{t}\), as a consequence of Proposition 3.
3.3 Main properties
We show that well-formedness is preserved by the reduction relation \(\cdot \leadsto _{\cdot } \cdot \).
Theorem 3
(Subject Reduction). For a configuration \(\mathcal C_1 \in \textrm{WF}_{\texttt {SVConf}}(A) \), if \(\mathcal C_1 \leadsto _p \mathcal C_2\) for some probability \(p \in [0,1]\), then \(\mathcal C_2 \in \textrm{WF}_{\texttt {SVConf}}(A)\).
Next, we show that progress and strong normalisation hold. More specifically, a well-formed semi-value configuration \(\mathcal C\) is either a value configuration or it reduces to a finite number of semi-value configurations with total probability 1, i.e. if we have not reached a normal form then the probability to be stuck is 0.
Theorem 4
(Progress). If \(\mathcal C \in \textrm{WF}_{\texttt {SVConf}}(A)\), then either \(\mathcal C \in \texttt {VConf}\), or there exists \(\mathcal C_i \in \textrm{WF}_{\texttt {SVConf}}(A)\) such that \(\mathcal C \leadsto _{p_i} \mathcal C_i\). Moreover, if \(\{ \mathcal C_i \}_{i \in I}\) is the set of all such distinct (not \(\alpha \)-equivalent) configurations, then I is finite, and \(\sum _i p_i = 1\).
Theorem 5
(Strong Normalisation). For a configuration \(\mathcal C \in \textrm{WF}_{\texttt {SVConf}}(A)\), there is no infinite sequence of reductions \(\mathcal C \leadsto _{p_0} \mathcal C_1 \leadsto _{p_1} \mathcal C_2 \leadsto _{p_2} \cdots \).
3.4 Illustrating Example: Quantum Walk Search
Given a graph with some marked vertices, a quantum walk search is the quantum analogue of a random walk [4], which looks for these marked vertices. Each node in the graph represents the state of two quantum registers. A condition on the application of a coin operator on the first register decides the direction in which a walker should take the next step. A step in this direction is represented by the application of a unitary on the second register. After a given number of steps, measurement is performed on the second register to reveal whether the walker has arrived on a marked node. Here, we present a k-step quantum walk on a cycle with 10 nodes for simplicity in our language. Representing the second register with qubits, in this case, would require 4 qubits, whereas we represent the state of the second register with a single \({\textbf {qnat}}\). In the unitary \(\textrm{CNOT}_{{\textbf {qnat}}}\) below, we use some (hopefully obvious) syntactic sugar with the expressions involving \({\textbf {n}}\) in order to avoid writing all the cases; the letter \({\textbf {n}}\) here should not be seen as a variable.
We define the unitary S corresponding to one step of the walk as \(S \triangleq \textrm{CNOT}_{{\textbf {qnat}}} \circ (\textrm{Had}\otimes \textrm{Id})\). Finally, the k-step walk can be represented in our language as follows, where \(S^k\) represents k compositions of S with itself:
3.5 Denotational Semantics: Soundness and Adequacy
In this section we describe the denotational semantics of the main calculus. Figure 11 succinctly describes the interaction between the pure fragment and the mixed fragment. We present the functor which facilitates the main contribution of the paper, i.e combining quantum and classical control.
The\(\mathcal B\)functor. In order to model the interaction between the pure quantum subsystem and the main calculus, we define the functor \(\mathcal B : \textbf{Isometry}\rightarrow \textbf{NCPSU}\), mapping a Hilbert space H to \(\mathcal B(H).\) For an isometry \(f :H_1 \rightarrow H_2\), the map \((f^* \circ (-) \circ f)\) is an NCPSU morphism \(B(H_2) \rightarrow B(H_1),\) so by defining \(\mathcal B(f) \triangleq (f^* \circ (-) \circ f)^{op}\), we get that \(\mathcal B(f) :\mathcal B(H_1) \rightarrow \mathcal B(H_2)\) in \(\textbf{NCPSU}\). We remark that this functor restricts to a functor \(\mathcal B :\textbf{Unitary}\rightarrow \textbf{NMIU}\) and we show that the functor \(\mathcal B : \textbf{Isometry}\rightarrow \textbf{NCPSU}\) is strict monoidal.
Fig. 11.
Categorical relations.
Interpretation of Types. We interpret types as von Neumann algebras. The types corresponding to a linear call-by-value lambda-calculus are interpreted in the standard way: \({\llbracket \textrm{I} \rrbracket } \triangleq \mathbb {C}\), \({\llbracket \mathrm {A+B} \rrbracket } \triangleq {\llbracket \textrm{A} \rrbracket } \oplus {\llbracket \textrm{B} \rrbracket }\), \({\llbracket \mathrm {A \otimes B} \rrbracket } \triangleq {\llbracket \textrm{A} \rrbracket } \otimes {\llbracket \textrm{B} \rrbracket }\), \({\llbracket !\textrm{A} \rrbracket } \triangleq !{\llbracket \textrm{A} \rrbracket }\) and \({\llbracket \mathrm {A \multimap B} \rrbracket } \triangleq {\llbracket \textrm{A} \rrbracket } \multimap {\llbracket \textrm{B} \rrbracket }\). The type for natural numbers is interpreted as the commutative von Neumann algebra \(\ell ^\infty (\mathbb N)\), i.e \({\llbracket \textrm{Nat} \rrbracket } \triangleq \ell ^\infty (\mathbb {N}).\) Finally, the interpretation of the type \(\mathcal B(\boldsymbol{Q})\) uses the \(\mathcal B\) functor that allows us to incorporate pure quantum primitives into our semantics, i.e \({\llbracket \mathcal \rrbracket }{B (\boldsymbol{Q})} \triangleq \mathcal B {\llbracket \boldsymbol{Q} \rrbracket }\).
Interpretation of Typing judgements. A typing judgment of the form \(\varDelta \vdash M :\textrm{A}\) is interpreted as a morphism \({\llbracket \varDelta \vdash M :\textrm{A} \rrbracket } :{\llbracket \varDelta \rrbracket } \rightarrow {\llbracket \textrm{A} \rrbracket }\) in \(\textbf{NCPSU}\) and we often abbreviate this by writing \({\llbracket M \rrbracket }.\) An excerpt of the interpretation is defined in Figure 12.
Fig. 12.
Interpretation of typing judgements (an excerpt).
Theorem 6
For every pure quantum type \(\boldsymbol{Q}\), there exist a set X, an NMIU isomorphism \(\alpha _{\overline{\boldsymbol{Q}}} : {\llbracket \overline{\boldsymbol{Q}} \rrbracket } \cong \ell ^\infty (X)\), and an isometric isomorphism \(\beta _{\boldsymbol{Q}} : {\llbracket \boldsymbol{Q} \rrbracket } \cong \ell ^2(X)\). Moreover, \( \forall \boldsymbol{b} \in {\boldsymbol{Basis Terms}}\), \( \exists x \in X\) s.t. \(\beta _{\boldsymbol{Q}}({\llbracket \boldsymbol{b} \rrbracket }) = \alpha _{\overline{\boldsymbol{Q}}}({\llbracket \overline{\boldsymbol{b}} \rrbracket }) = \left| x \right\rangle \).
Using the above theorem, measurement is interpreted as the map \(m^{\boldsymbol{Q}} : \mathcal B({\llbracket \boldsymbol{Q} \rrbracket }) \rightarrow {\llbracket \overline{\boldsymbol{Q}} \rrbracket }\) defined as \(m^{\boldsymbol{Q}}\triangleq \alpha _{\overline{\boldsymbol{Q}}}^{op} \circ m_X^{op} \circ \mathcal B(\beta _{\boldsymbol{Q}})\).
Interpretation of Configurations. A well-formed configuration \((\boldsymbol{t}, u_\sigma , M) \) with \(\cdot \boldsymbol{\vdash }\boldsymbol{t}:\boldsymbol{Q}\), \(\Vdash u_\sigma :(\boldsymbol{Q}, \boldsymbol{Q}_1' \boldsymbol{\otimes }\cdots \boldsymbol{\otimes }\boldsymbol{Q}_m')\), and \(x_1 :\mathcal B(\boldsymbol{Q}_1'), \ldots , x_m :\mathcal B(\boldsymbol{Q}_m') \vdash M :\textrm{A}\) is interpreted as the NCPSU morphism
We can now show that our semantic interpretation is sound with respect to single-step reduction.
Theorem 7
(Soundness). For \(\mathcal C \in \textrm{WF}_{\texttt {SVConf}}(A)\), if \(\mathcal C \notin \texttt {VConf}\), then
$$ {\llbracket \mathcal C : \textrm{A} \rrbracket } = \sum _\mathcal {C \leadsto _p \mathcal C'} p {\llbracket \mathcal C' : \textrm{A} \rrbracket } , $$
where the sum ranges over all possible reducts \(\mathcal C \leadsto _p \mathcal C'\).
Next, we can show that our interpretation is sound in a big-step sense as well, which follows easily using the previous result and strong normalisation.
Theorem 8
(Strong Adequacy). For \(\mathcal C \in \textrm{WF}_{\texttt {SVConf}}(A)\),
where \(P(\mathcal C \rightarrow _{*} \mathcal V)\) indicates the overall probability that \(\mathcal C\) reduces to \(\mathcal V\).
This implies that, for any well-formed configuration \(\mathcal C\), its interpretation \({\llbracket \mathcal \rrbracket }{C}\) is an NCPU map (i.e., it is not merely subunital) and therefore it corresponds to a quantum channel in the Heisenberg picture of quantum mechanics.
4 Conclusion and Perspectives
We described a programming language which has support for both pure state quantum computation and mixed state quantum computation. We began by describing the pure quantum subsystem (§2), for which we introduced an equational theory and proved its completeness w.r.t. the denotational semantics (§2.4). Then, we described the main calculus (§3.1) which uses a new adaptation of quantum configurations (§3.2), which we used to define the operational semantics of the language. Here, the interaction between the pure quantum subsystem and the main calculus becomes apparent. We showed that our denotational semantics (§3.5) has a clear and appropriate interpretation as channels in the Heisenberg picture of quantum mechanics and we showed it is sound and adequate with respect to the operational semantics (§3.5).
Although our language has support for \(\textrm{Nat}\), an inductive type, an obvious extension would be to include more general inductive types. Additionally, support for higher-order pure quantum computation is another feature that would be interesting to add in a future work.
Another matter that could be tackled as future work is recursion. In the pure system, adding general recursion is an open and difficult problem [14, Section 5.2]. In the main calculus, our denotational model supports recursion for first-order quantum functions [13, 17]. However, our model does not support general recursion when quantum lambda abstractions are involved. There are other denotational models that support general recursion and quantum lambda abstractions, but they do not support types like qnat that correspond to \(\ell ^2(\mathbb {N})\), instead they support recursive types that intuitively correspond to infinite classical combinations of spaces involving finite-dimensional Hilbert spaces, which is not the same as \(\ell ^2(\mathbb {N})\). A model for quantum lambda abstractions, qnat and general recursion is an open problem to the best of our knowledge.
Acknowledgements
The authors would like to thank Benoît Valiron for helpful comments and discussions. Louis Lemonnier’s research was funded by the Engineering and Physical Sciences Research Council (EPSRC) under project EP/X025551/1 “Rubber DUQ: Flexible Dynamic Universal Quantum programming”. This work is also supported by the HORIZON 2020 project NEASQC, by the Inria associate team TC(Pro)\(^3\), by the PEPR integrated project EPiQ ANR-22-PETQ-0007, and by the HQI initiative ANR-22-PNCQ-0002.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
CPTP stands for ‘completely positive trace preserving’ and \(\mathcal {T}(H)\) and \(\mathcal {B}(H)\) stand for the trace-class and bounded linear operators, respectively, on a Hilbert space H.
). We may think of \(\ell ^2(\mathbb N)\) as a quantum analogue of the natural numbers, to abstract from qubit-level computation. The addition of \({\textbf {qnat}}\) allows us to reason about pure quantum computation while abstracting away from quantum circuits.
. (Entangled) quantum states can be defined, e.g., 
. Linear combinations of qnats can also be written in the language, i.e. 
, and 
hold true and determine the same ONB for the type \({\textbf {qnat}}\) (it represents the computational basis of \(\ell ^2(\mathbb N)\)). The set used in the last predicate allows us to conclude that 
holds. This last set of values is used to type \(\textrm{Had}_{{\textbf {qnat}}}\) from Example 2.
and \(u_{id} \triangleq \{ \mid \boldsymbol{*\otimes w \otimes z} \mapsto \boldsymbol{w \otimes z} \}\) is a unitary with type \(\Vdash u_{id} :U(\boldsymbol{I} \boldsymbol{\otimes }{\textbf {qbit}}\boldsymbol{\otimes }{\textbf {qbit}}, {\textbf {qbit}}\boldsymbol{\otimes }{\textbf {qbit}})\). It conveys the information that the variable x in \(x \otimes y\) keeps track of the first qubit in \(\boldsymbol{t}\) and that the variable y keeps track of the second one. Whereas in the configuration \((\boldsymbol{t} , u_{swap }, x \otimes y)\) with \(u_{swap } \triangleq \{ \mid \boldsymbol{*\otimes w \otimes z} \mapsto \boldsymbol{z \otimes w} \}\), the variable x keeps track of the second qubit and y of the first one. Note that, due to quantum entanglement, the term \(\boldsymbol{t}\) cannot be decomposed into a non-trivial tensor product, and the variables x and y should be thought of as identifying qubit components of \(\boldsymbol{t}\), instead of storing quantum data themselves.
with:
;
