Non-harmonious logical connectives have recently been shown to provide a natural proof-theoretic account of quantum measurement. In particular, the connective \(\mathbin{\mathsf{sup}}\) introduced by Díaz-Caro and Dowek endows intuitionistic natural deduction with both harmonious and excessive rules, and its proof language forms the core of a quantum programming language. However, the resulting calculus is still permissive enough to express non-linear or genuinely non-physical operations: nothing in the type system enforces linearity or prevents the cloning of quantum data. In this paper we introduce a linear version of the \(\mathbin{\mathsf{sup}}\)-calculus. We separate classical and quantum data by means of a two-zone context discipline, and we restrict the use of the \(\mathbin{\mathsf{sup}}\)-connective and scalar combinations to ensure that well-typed quantum programs denote linear maps between finite-dimensional Hilbert spaces. We give a natural deduction style type system, an operational semantics with both deterministic and measurement steps, and we prove subject reduction and type soundness. We then show that no term in the purely quantum fragment can implement a duplicator \(\mathsf{qbit} \multimap \mathsf{qbit} \otimes \mathsf{qbit}\), while classical outcomes of measurements can still be duplicated freely. Finally, we sketch a denotational semantics in which closed quantum terms denote completely positive maps, and we relate our system to existing quantum \(\lambda\)-calculi.
Non-harmonious logical connectives have recently been shown to provide a natural proof-theoretic account of quantum measurement. In particular, the connective (\mathbin{\mathsf{sup}}) introduced by Díaz-Caro and Dowek endows intuitionistic natural deduction with both harmonious and excessive rules, and its proof language forms the core of a quantum programming language. However, the resulting calculus is still permissive enough to express non-linear or genuinely non-physical operations: nothing in the type system enforces linearity or prevents the cloning of quantum data. In this paper we introduce a linear version of the (\mathbin{\mathsf{sup}})-calculus. We separate classical and quantum data by means of a two-zone context discipline, and we restrict the use of the (\mathbin{\mathsf{sup}})-connective and scalar combinations to ensure that well-typed quantum programs denote linear maps between finite-dimensional Hilbert spaces. We give a natural deduction style type system, an operational semantics with both deterministic and measurement steps, and we prove subject reduction and type soundness. We then show that no term in the purely quantum fragment can implement a duplicator (\mathsf{qbit} \multimap \mathsf{qbit} \otimes \mathsf{qbit}), while classical outcomes of measurements can still be duplicated freely. Finally, we sketch a denotational semantics in which closed quantum terms denote completely positive maps, and we relate our system to existing quantum (\lambda)-calculi.
The objective of this thesis is to develop a semantics for higher-order quantum information. Following the work done in the author's M.Sc. thesis, we study a lambda calculus for quantum computation with classical control. The language features two important properties. The first one, arising from the so-called no-cloning theorem of quantum computation, is the need for a distinction between duplicable and non-duplicable elements. For keeping track of duplicability at higher order, we use a type system inspired by the resource-sensitive linear logic. The second important aspect is the probability inherent to measurement, the only operation for retrieving classical data from quantum data. This forces us into choosing a reduction strategy for being able to define an operational semantics. We address the question of a denotational semantics in two respects. First, we restrict the study to the strictly linear aspect of the language. Doing so, we suppress the need for distinguishing between duplicable and non-duplicable elements and we can focus on the description of quantum features at higher order. Using the category of completely positive maps as a framework, we build a fully abstract denotational model of the strictly linear fragment of the language. The study of the full language is more demanding. For dealing with the probabilistic aspect of the language, we use a method inspired by Moggi and build a computational model with a distinction between values and computations. For the distinction between duplicability and non-duplicability in the calculus, we adapt Bierman's linear category, where the duplication is considered as a comonad with specific properties. The resulting model is what we call a linear category for duplication. Finally, we only focus on the fragment of the language that contains the aforementioned elements, and remove the classical Boolean and quantum Boolean features to get a generic computational linear lambda-calculus. In this idealized setting, we show that such a language have a full and complete interpretation in a linear category for duplication.
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.
Abstract We introduce the L!S-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic. These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the L!S-calculus as an extension of the LS-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalization and an introduction property—as well as preserve the expressiveness of the original LS-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.
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.
This paper demonstrates how to add a measurement operator to quantum λ-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML [Grattage, J. and T. Altenkirch, A functional quantum programming language, in: LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (2005), pp. 249–258] or Lineal [Arrighi, P. and G. Dowek, A computational definition of the notion of vectorial space, Electronic Notes in Theoretical Computer Science 117 (2005), pp. 249–261; Arrighi, P. and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings and confluence, in: B. Buchberger, editor, Term Rewriting and Applications, 19th International Conference, RTA-08, To appear in LNCS (2008), eprint available at arXiv:quant-ph/0612199], which is the subject of further research.
Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this problem fell short in one way or another, either limiting the language to an unusably small finitary fragment, or giving up important features of quantum physics such as entanglement. In this paper, we propose a denotational semantics for a quantum lambda calculus with recursion and an infinite data type, using constructions from quantitative semantics of linear logic.