Yannick Delbecque — site personnel

Quantum Games as Quantum Types

Abstract

In this thesis, we present a new model for higher-order quantum programming languages. The proposed model is an adaptation of the probabilistic game semantics de- veloped by Danos and Harmer [DH02]: we expand it with quantum strategies which enable one to represent quantum states and quantum operations. Some of the basic properties of these strategies are established and then used to construct denotational semantics for three quantum programming languages. The first of these languages is a formalisation of the measurement calculus proposed by Danos et al. [DKP07]. The other two are new: they are higher-order quantum programming languages. Previous attempts to define a denotational semantics for higher-order quantum programming languages have failed. We identify some of the key reasons for this and base the design of our higher-order languages on these observations.

The game semantics proposed in this thesis is the first denotational semantics for a λ-calculus equipped with quantum types and with extra operations which allow one to program quantum algorithms. The results presented validate the two different approaches used in the design of these two new higher-order languages: a first one where quantum states are used through references and a second one where they are introduced as constants in the language. The quantum strategies presented in this thesis allow one to understand the constraints that must be imposed on quantum type systems with higher-order types. The most significant constraint is the fact that abstraction over part of the tensor product of many unknown quantum states must not be allowed.

Quantum strategies are a new mathematical model which describes the interaction between classical and quantum data using system-environment dialogues. The interactions between the different parts of a quantum system are described using the rich structure generated by composition of strategies. This approach has enough generality to be put in relation with other work in quantum computing. Quantum strategies could thus be useful for other purposes than the study of quantum programming languages.

Abrégé

Nous présentons dans cette thèse un nouveau modèle pour les langages de programmation quantique. Notre modèle est une adaptation de la sémantique de jeux probabilistes définie par Danos et Harmer [DH02]: nous y ajoutons des stratégies quantiques pour permettre la représentation des états et des opérations quantiques. Nous établissons quelques propriétés de base de ces stratégies. Ces propriétés sont ensuite utilisées pour construire des sémantiques dénotationnelles pour trois langages de programmation quantique. Le premier langage est une formalisation du calcul par mesures proposé par Danos et al. [DKP07]. Les deux autres langages sont nouveaux: ce sont des langages quantiques d’ordre supérieur dont la syntaxe a été construite à partir d’observations expliquant l’échec des tentatives précédentes pour construire une sémantique dénotationnelle pour de tels langages.

La sémantique de jeux présentée dans cette thèse est la première sémantique dénotationnelle pour de tels λ-calculs équipés de types et d’opérations supplémentaires permettant la programmation d’algorithmes quantiques. Les résultats présentés valident les deux approches différentes utilitées dans la conception de ces deux nouveaux languages d’ordre supérieur: une première où les états quantiques sont indirectement accessibles via des références et une seconde où ils sont introduit directement comme des constantes dans le langage. Les stratégies quantiques présentées permettent de comprendre les contraintes devant être imposées aux systèmes de type quantique comportant des types d’ordre supérieurs. La contrainte la plus importante est le fait que l’abstraction sur une partie d’un état quantique comportant plusieurs qbits inconnus doit être prohibée.

Les stratégies quantiques constituent un nouveau modèle mathématique qui décrit l’interaction entre les données classiques et quantiques par des dialogues entre système et environnement. L’interaction entre les differentes parties d’un système quantique y est décrite à l’aide d’une structure riche en utilisant la composition de strategies. L’approche utilisé est assez générale pour être mise en relation avec d’autres travaux en informatique quantique. Les propriétés des stratégies quantiques pourraient donc être utiles à d’autre fins que l’étude des languages de programmation quantiques.