Langage, mathématiques, et observables

Pius Servien

Théo Kahan, P. Cavailles

Kinnari Vijay Dave

Combining classical and quantum control : A logical, syntactic and semantic perspective Cette thèse vise principalement à établir les fondements théoriques nécessaires à la conception d'un langage de programmation complet pour l'informatique quantique. L'idée qui a inspiré toutes les contributions de cette thèse est de produire dans le cadre quantique un développement similaire à celui utilisé pour les langages de programmation et la logique dans le paradigme classique. En nous appuyant sur les travaux préparatoires de la correspondance Curry-Howard-Lambek, nous essayons d'approfondir les trois pierres angulaires de cette correspondance : les langages de programmation, la logique et la théorie des catégories, en nous concentrant sur la combinaison de deux paradigmes et en considérant des programmes avec des flots de contrôle quantique et classique. Nous avons essayé d'aller plus loin. Nous avons également abordé les deux visions complémentaires de la mécanique quantique, celles de Heisenberg et de Schrödinger, et adopté l'une d'elles pour définir une sémantique physiquement intuitive pour les langages dont nous discutons. Cette thèse apporte deux contributions principales à la littérature existante sur les langages de programmation quantiques. Nous introduisons tout d'abord un lambda calcul quantique qui combine le contrôle quantique et classique, dont la conception s'appuie sur la structure mathématique de sa sémantique dénotationnelle physiquement intuitive. La sémantique opérationnelle de ce langage est basée sur une adaptation des configurations quantiques que nous introduisons, et est liée au modèle dénotationnel par un résultat d'adéquation. Le langage fournit également un prototype de types inductifs quantiques à travers le type qnat, un type pour les entiers naturels quantiques. Le modèle dénotationnel de ce calcul est basé sur les algèbres de von Neumann, qui sont au cœur de la formulation mathématique de la vision de Heisenberg de la mécanique quantique. La deuxième contribution est un langage de preuve pour le fragment IMALL de la logique linéaire qui s'appuie sur certaines observations clés du calcul présenté ci-dessus. Ce langage estl'un des premiers à pouvoir prendre en charge des programmes combinant des constructions telles que le quantum switch et la mesure. À cet égard, ce travail constitue une amélioration significative par rapport au calcul précédent, car il prend en charge une version plus fine du contrôle quantique, permettant ainsi l'écriture d'algorithmes tels que le quantum switch. La syntaxe du langage est par nature algébrique et linéaire, permettant d'écrire des combinaisons linéaires de termes. Une conséquence majeure, avec la sémantique de la modalité B qu'il introduit, est que la mesure n'est plus une construction de base du langage. Elle peut désormais être écrite comme un programme parmi d'autres dans le langage. Enfin, la sémantique dénotationnelle de ce travail est basée sur les algèbres C* - une généralisation des algèbres de von Neumann. Le modèle dénotationnel s'avère adéquat pour la sémantique opérationnelle, dont la linéarité en est une conséquence naturelle. Enfin, nous concluons cette thèse en présentant les limites de ces travaux et les orientations possibles pour des travaux futurs.

Véronique Rauline

Federico Zalamea

A la poursuite de l’individuation : description mathématique des systèmes physiques Résumé: Ce travail se veut une analyse conceptuelle de certains développements récents dans les fondements mathématiques de la Mécanique Classique et de la Mécanique Quantique qui ont permis de formuler ces deux théories dans un même langage. Du point de vue algébrique, l’ensemble des observables d’un système physique, soit-il classique ou quantique, est décrit par une algèbre de Jordan-Lie. Du point de vue géométrique, l’espace des états de tout système est décrit par un espace uniforme de Poisson avec transition de probabilité. Ces deux structures mathématiques sont ici interprétées comme une manifestation du double rôle constitutif des propriétés en physique : elles sont à la fois des quantités et des transformations. Il s’agit alors de comprendre l’articulation précise entre ces deux rôles. Au cours de l’analyse, il apparaîtra que la Mécanique Quantique peut être vue comme se distinguant de la Mécanique Classique par une condition de compatibilité entres les quantités et les transformations.D’autre part, cette thèse met en évidence l’existence d’une tension fondamentale entre une certaine façon abstraite de concevoir les structures mathématiques, présente dans la pratique de la physique mathématique, et la nécessité de spécifier des états ou des observables particulières. Il devient alors important de comprendre comment, dans le formalisme, se construit un schéma d’indexation. La “poursuite de l’individuation” est l’analyse de différentes techniques mathématiques vues comme tentatives de résolution ce problème. En particulier,nous discuterons comment la théorie des groupes permet d’y apporter une solution partielle.