Lambda Calculs Resource-Aware avec Contrôle Cohérent

Mots clés

langages quantiques, complexité, lambda-calcul, types

Détail de l'offre

Les langages de programmation avec contrôle quantique permettent au flot d'exécution des programmes de dépendre de données quantiques, rendant possible des superpositions de programmes, comme l'illustre le Quantum Switch [1]. Bien que ce paradigme offre une manière naturelle et expressive de modéliser le calcul quantique, il soulève des défis fondamentaux concernant la réalisabilité physique et la complexité computationnelle. En particulier, les programmes avec contrôle quantique doivent respecter à la fois les lois de la mécanique quantique et des contraintes strictes sur les ressources afin d'admettre des réalisations physiques efficaces.

Des travaux récents [2, 3] ont montré que des systèmes de types inspirés de la logique linéaire et des techniques de réalisabilité peuvent être utilisés pour garantir des propriétés physiques essentielles des programmes quantiques, telles que l'unitarité et la faisabilité. Cependant, l'interaction entre le contrôle quantique, les caractéristiques d'ordre supérieur et les garanties de ressources reste encore partiellement comprise. En particulier, il n'existe actuellement aucun cadre typé pleinement satisfaisant qui prenne simultanément en charge le contrôle quantique, les lambda-calculs quantiques d'ordre supérieur et des certifications précises de la complexité en temps et en espace.

L'objectif de cette thèse est de développer un langage de programmation quantique typé avec contrôle quantique, dans lequel la consommation de ressources est certifiée. L'approche reposera sur la logique linéaire légère et des techniques de réalisabilité afin de contrôler la duplication et l'itération, garantissant que les programmes se normalisent dans des bornes de complexité prescrites tout en restant physiquement pertinents.

Un objectif central est de concevoir un système de types qui caractérise de manière correcte et complète des classes de complexité quantique telles que BQP et FBQP. Cela inclut l'établissement d'une correspondance entre les programmes typables et des familles de circuits quantiques bornées en temps polynomial (et potentiellement en espace polynomial), fournissant ainsi une caractérisation des classes de complexité quantique dans l'esprit de la complexité implicite, et ce dans un cadre d'ordre supérieur.

Plus précisément, la thèse abordera les axes de recherche suivants :

• la conception d'un lambda-calcul quantique typé avec contrôle quantique, combinant des modalités de logique linéaire et de logique linéaire légère avec une sémantique fondée sur la réalisabilité, afin de certifier la normalisation en temps polynomial des programmes quantiques ;

• le développement de caractérisations correctes et complètes de classes de complexité quantique telles que BQP et FBQP au moyen de disciplines de typage, en étendant des résultats existants de premier ordre ou à contrôle classique à des langages d'ordre supérieur et à contrôle quantique ;

• l'identification d'un fragment bien comporté du langage dans lequel les programmes peuvent être compilés en circuits quantiques (ou en modèles de bas niveau alternatifs) de taille polynomiale, tout en préservant la sémantique et les garanties de complexité ;

• l'extension de l'analyse à la complexité en espace, dans le but de contrôler et de certifier le nombre de qubits utilisés lors de l'exécution des programmes.