In this paper we give a fully complete model for a linear probabilistic lambda-calculus. The model is a Kripke semantics based on the category of stochastic relations. We sketch how this relates to quantum computation.
This paper studies the linear fragment of the programing language for quantum computation with classical control described in [Selinger, P. and B. Valiron, A lambda calculus for quantum computation with classical control, in: P. Urzyczyn, editor, Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), Lecture Notes in Computer Science 3461 (2005), pp. 354–368]. We sketch the language, and discuss equivalence of terms. We also describe a fully abstract denotational semantics based on completely positive maps.
Quantum programming languages permit a hardware independent, high-level description of quantum algorithms. In particular, the quantum λ-calculus is a higher-order language with quantum primitives, mixing quantum data and classical control. Giving satisfactory denotational semantics to the quantum λ-calculus is a challenging problem that has attracted significant interest. In the past few years, both static (the quantum relational model) and dynamic (quantum game semantics) denotational models were given, with matching computational adequacy results. However, no model was known to be fully abstract. Our first contribution is a full abstraction result for the games model of the quantum λ-calculus. Full abstraction holds with respect to an observational quotient of strategies, obtained by summing valuations of all states matching a given observable. Our proof method for full abstraction extends a technique recently introduced to prove full abstraction for probabilistic coherence spaces with respect to probabilistic PCF. Our second contribution is an interpretation-preserving functor from quantum games to the quantum relational model, extending a long line of work on connecting static and dynamic denotational models. From this, it follows that the quantum relational model is fully abstract as well. Altogether, this gives a complete denotational landscape for the semantics of the quantum λ-calculus, with static and dynamic models related by a clean functorial correspondence, and both fully abstract.
The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the benefits of both the quantum Turing machine and the quantum circuit models. The calculus turns out to be closely related to the linear lambda calculi used in the study of linear logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.
With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite system. The linear-algebraic lambda-calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear lambda-calculus. These various notions of linearity are discussed in the context of quantum programming languages. KEYWORDS: quantum lambda-calculus, linear lambda-calculus, λ-calculus, quantum logics.
The aim of this paper is to introduce a general model of quantum computation, the quantum calculus: both unitary transformations and projective measurements are allowed; furthermore a complete classical control, including conditional structures and loops, is available. Complementary to its operational semantics, we introduce a pure denotational semantics for the quantum calculus. Based on probabilistic power domains [Jones, C. and G. D. Plotkin, A probabilistic powerdomain of evaluations, in: LICS, 1989, pp. 186–195. URL http://homepages.inf.ed.ac.uk/gdp/publications/Prob_Powerdomain.pdf], this pure denotational semantics associates with any description of a computation in the quantum calculus its action in a mathematical setting. Adequacy between operational and pure denotational semantics is established. Additionally to this pure denotational semantics, an observable denotational semantics is introduced. Following the work by Selinger, this observable denotational semantics is based on density matrices and super-operators. Finally, we establish an exact abstraction connection between these two semantics.
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.