This paper presents a novel semantics for a quantum programming language by operator algebras, which are known to give a formulation for quantum theory that is alternative to the one by Hilbert spaces. We show that the opposite category of the category of W*-algebras and normal completely positive subunital maps is an elementary quantum flow chart category in the sense of Selinger. As a consequence, it gives a denotational semantics for Selinger's first-order functional quantum programming language QPL. The use of operator algebras allows us to accommodate infinite structures and to handle classical and quantum computations in a unified way.
This paper presents a novel semantics for a quantum programming language by operator algebras, which are known to give a formulation for quantum theory that is alternative to the one by Hilbert spaces. We show that the opposite category of the category of W*-algebras and normal completely positive subunital maps is an elementary quantum flow chart category in the sense of Selinger. As a consequence, it gives a denotational semantics for Selinger's first-order functional quantum programming language QPL. The use of operator algebras allows us to accommodate infinite structures and to handle classical and quantum computations in a unified way.
We propose a notion of quantum control in a quantum programming language which permits the superposition of finitely many quantum operations without performing a measurement. This notion takes the form of a conditional construct similar to the "if" statement in classical programming languages. We show that adding such a quantum "if" statement to the QPLprogramming language simplifies the presentation of several quantum algorithms. This motivates the possibility of extending the denotational semantics of QPL to include this form of quantum alternation. We give a denotational semantics for this extension of QPL based on Kraus decompositions rather than on superoperators. Finally, we clarify the relation between quantum alternation and recursion, and discuss the possibility of lifting the semantics defined by Kraus operators to the superoperator semantics defined by Selinger.
We propose a notion of quantum control in a quantum programming language which permits the superposition of finitely many quantum operations without performing a measurement. This notion takes the form of a conditional construct similar to the IF statement in classical programming languages. We show that adding such a quantum IF statement to the QPL programming language simplifies the presentation of several quantum algorithms. This motivates the possibility of extending the denotational semantics of QPL to include this form of quantum alternation. We give a denotational semantics for this extension of QPL based on Kraus decompositions rather than on superoperators. Finally, we clarify the relation between quantum alternation and recursion, and discuss the possibility of lifting the semantics defined by Kraus operators to the superoperator semantics defined by Selinger.
While much of the current study on quantum computation employs low-level formalisms such as quantum circuits, several high-level languages/calculi have been recently proposed aiming at structured quantum programming. The current work contributes to the semantical study of such languages by providing interaction-based semantics of a functional quantum programming language; the latter is, much like Selinger and Valiron's, based on linear lambda calculus and equipped with features like the ! modality and recursion. The proposed denotational model is the first one that supports the full features of a quantum functional programming language; we prove adequacy of our semantics. The construction of our model is by a series of existing techniques taken from the semantics of classical computation as well as from process theory. The most notable among them is Girard's Geometry of Interaction (GoI), categorically formulated by Abramsky, Haghverdi and Scott. The mathematical genericity of these techniques---largely due to their categorical formulation---is exploited for our move from classical to quantum.
In this thesis, we study quantum programming languages, and focus on the quantum lambda-calculus, a paradigmatic language defined by Selinger and Valiron, which mixes a rich classical control flow (higher order functions, etc.) and quantum data (qubit creation, measure, and unitary operations). In this thesis, we search for a denotational semantics of this language, in other words, we extract the meaning and behaviour of programs by interpreting them in an adequately chosen mathematical universe. In order to model the quantum lambda-calculus, one must adapt the traditional denotational models to the mathematics of quantum computation (Hilbert spaces, density matrices, etc.). We have three main contributions:Firstly, we extend game semantics to the quantum case. Game semantics is a dynamic approach to denotational semantics, which focuses on the sequence of interactions between a program and its environment. We obtain the first denotational model of the full quantum lambda-calculus which is both compositional and interactive, meaning that it represents the dynamic of the execution. Our model generalise the recently developed model for the probabilistic case.Secondly, we formally link our model to the only pre-existing denotational model of the full lambda-calculus, the quantum relational model of Pagani, Selinger and Valiron.Lastly, we prove that our game model is fully abstract, the gold standard of denotational semantics, which ensures a total correspondence between the programming language and the model. We deduce that the quantum relational model was also fully abstract, which was an open problem.This thesis is constituted of three parts. The first part details some preliminaries on category theory, used for defining a formal framework including both the quantum game model and the quantum relational model, some preliminaries on the mathematics of quantum computation, and then some preliminaries on quantum programming and its models. The second part starts with some preliminaries on game semantics and defines our quantum game model in the simplified case of the linear quantum lambda-calculus. The third part builds on the second part to define the full quantum game model, prove its full abstraction, and deduce that the quantum relational model is fully abstract too.
The focus of this thesis is on laying the theoretical foundation for designing an all-encompassing programming language for quantum computing. The idea inspiring all the contributions of this thesis was to mirror the development of programming languages and logic done for classical computing for its quantum counterpart. Following the groundwork of the Curry-Howard-Lambek correspondence, we try to delve into the three cornerstones of this correspondence - programming languages, logic and category theory with a focus on combining two paradigms of control flow in programs - quantum and classical into one framework. We have tried to achieve more. We have also touched upon the two complementary view of quantum mechanics- Heisenberg and Schrödinger, and adopted one view to define a physically intuitive semantics for the languages we discuss. There are two main contributions that this thesis makes to the existing literature on quantum programming languages. We first introduce a quantum lambda calculus which combines quantum and classical control, whose design is guided by the mathematical structure of its physically intuitive denotational semantics. The operational semantics for this language, is based on an adaptation of quantum configurations which we introduce, and is tied to the denotational model through an adequacy result. The language also provides a prototype of quantum inductive types through the type qnat- a type for quantum natural numbers. The denotational model for this calculus is based on von Neumann algebras- which are at the heart of the mathematical formulation of the Heisenberg view of quantum mechanics. The second contribution is a proof language for the IMALL fragment of Linear logic which builds on some key observations from the calculus introduced above. This language is one of the first such works to be able to support programs which combine constructs such as the quantum switch with measurement. In this aspect, this work is a strict improvement on the previous calculus, since it supports a more fine grained version of quantum control, thus enabling expression of algorithms such as the well-known quantum switch. The syntax is also linear algebraic in nature, supporting linear combinations of terms. A key consequence of this, along with the semantics of the B modality that it introduces is that measurement is no longer a ground construct of the language. In fact, it can now be written as just another program in the language. Finally, the denotational semantics for this work is based on C*-algebras - a generalization of von Neumann algebras. The denotational model is shown to be adequate for the operational semantics, whose linearity turns out to be a natural consequence of this. Finally, we conclude this thesis with limitations of these works and possible directions for future work.
Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics.