Electronic Notes in Theoretical Computer Science

On a Fully Abstract Model for a Quantum Linear Functional Language

Peter Selinger, Benoît Valiron

Published Jul 1, 2008• 45 citations

Abstract

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.

DOI: 10.1016/j.entcs.2008.04.022

Related papers

Semantics for a higher-order functional programming language for quantum computation

Benoît Valiron

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.

Jan 1, 20087 citations

Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power

Ugo Dal Lago, Andrea Masini, Margherita Zorzi

We study an untyped lambda calculus with quantum data and classical control. This work stems from previous proposals by Selinger and Valiron and by Van Tonder. We focus on syntax and expressiveness, rather than (denotational) semantics. We prove subject reduction, confluence and a standardization theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

arXiv:cs/0703152Mar 30, 20070 citations

Quantum Game Semantics

Marc de Visme

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.

Sep 28, 20200 citations

On Quantum and Probabilistic Linear Lambda-calculi (Extended Abstract)

Benoît Valiron

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.

Electronic Notes in Theoretical Computer ScienceFeb 1, 20111 citation

Full abstraction for the quantum lambda-calculus

Pierre Clairambault, Marc de Visme

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.

Proceedings of the ACM on Programming LanguagesDec 20, 201925 citations

A functional programming language for quantum computation with classical control

Benoît Valiron

The objective of this thesis is to develop a functional programming language for quantum computers based on the QRAM model, following the work of P. Selinger (2004) on quantum flow-charts. We construct a lambda-calculus without side-effects to deal with quantum bits. We equip this calculus with a probabilistic call-by-value operational semantics. Since quantum information cannot be duplicated due to the no-cloning property, we need a resource-sensitive type system. We develop it based on affine intuitionistic linear logic. Unlike the quantum lambda-calculus proposed by Van Tonder (2003, 2004), the resulting lambda-calculus has only one lambda-abstraction, linear and non-linear abstractions being encoded in the type system. We also integrate classical and quantum data types within our language. The main results of this work are the subject-reduction of the language and the construction of a type inference algorithm.

Jan 1, 200417 citations