Des cocycles de Feller stochastiques quantiques
∗-homomorphes sont construits pour certains générateurs non bornés, et ainsi nous obtenons des dilatations pour des semigroupes dynamiques quantiques fortement continus sur des
C∗ algèbres. Ceci généralise la construction d’un processus de Feller classique et de son semigroupe à partir d’un générateur donné. Notre construction est possible à condition que le générateur satisfasse une propriété d’invariance pour une sous-algèbre dense
A0 de la
C∗ algèbre
A et obéisse aux relations de structure nécessaires; les itérations du générateur, lorsqu’elles sont appliquées à une famille génératrice de
A0, doivent satisfaire à une condition de croissance. De plus, il est supposé que soit la sous-algèbre
A0 est engendrée par les isométries et
A est universelle, ou bien
A0 contient ses racines carrées. Ces conditions sont vérifiées dans quatre cas: marches aléatoires classiques sur les groupes discrets, le processus d’exclusion quantique symétrique introduit par Rebolledo et des flux sur le tore non commutatif et l’algèbre de rotation universelle.
Dynamiques quantiques sur réseaux Le domaine de l’informatique quantique a connu ces dernières années un fort développement. Un nouveau phénomène a récemment été découvert sur atomes de Rydberg, le scarring, qui s’est révélé être un nouveau mécanisme de brisure d’ergodicité: certains états initiaux n’explorent pas l’entièreté de l’espace de Hilbert mais restent localisés. Ce type de mécanisme a un potentiel intérêt pour encoder de l’information dans des systèmes quantiques.Dans cette thèse, on étudie des dynamiques discrètes en espace temps, qui sont des modèles quantiques simples à plusieurs corps. Des exemples de ces dynamiques discrètes sont les marches quantiques et les automates cellulaires quantiques. Elles sont écrites en termes de portes quantiques, ce qui les rend adaptées aux plateformes expérimentales.Dans la première partie de la thèse, on s’est intéressé à ces dynamiques discrètes dans le but de simuler un système physique. Plus précisément, nous proposons un automate cellulaire quantique et montrons sa convergence vers une théorie quantique des champs, le modèle de Schwinger en 1+1 dimensions.Dans la seconde partie de la thèse, nous investiguons ces dynamiques quantiques hors équilibre et étudions leurs propriétés de thermalisation sous le point de vue de l’information quantique.Nous proposons une généralisation de la marche quantique telle qu’elle interagit avec des spins situés sur les liens d’un réseau, et nous étudions les propriétés de propagation de l’aimantation et de l’intrication.Nous étudions ensuite un automate cellulaire quantique et découvrons que parmi les états chaotiques générés par la dynamique une hiérarchie peut émerger.
Méthodes Formelles pour les Langages de Programmation Quantiques Le modèle Qram est un modèle de calcul quantique pratique composé d’un ordinateur classique et un processus quantique qui communiquent entre eux. Le programme est exécuté sur l’ordinateur classique. Il envoie les instructions correspondant aux opérateurs quantiques sur le co-processeur, et reçoit le résultat de l’observation de l’état quantique. Ce modèle est considéré comme un modèle standard et plusieurs langages de programmation ont été conçus en basant sur ce modèle. Alors que les programmes dans ce modèle sont capables de réaliser tout calcul quantique grâce à l’usage de la mémoire quantique, il est difficile de les analyser sans l’aide d’un autre ordinateur quantique. Ce problème suscite le besoin pour des méthodes formelles pour les langages programmations quantiques : les outils formels pour raisonner sur l’optimisation du code, pour l’analyser des ressources, et pour spécifier et prouver les propriétés des programmes quantiques. La sémantique catégorique fait partie de ces méthodes qui fait le lien entre les opérateurs quantiques et les programmes et introduit le système logique qui peut décrire les propriétés sur l’état quantique dans le système de types. Bien que plusieurs travaux proposent des sémantiques catégoriques pour les langages de description de circuits quantiques, aucun ne supporte l’usage du résultat d’une mesure au sein du processeur classique (le ”levage dynamique”). Dans cette thèse, nous formalisons le levage dynamique qui transfère le résultat d’observations sur l’état quantique à l’information classique dans un langage de programmation de description de circuit quantique. En suivant l’approche du langage Proto-Quipper, nous définissons un langage typé de description de circuit quantique où l’information quantique levée est incorporée dans la structure ramifiée. Ensuite, le levage dynamique est formalisé dans le cadre de la sémantique opérationnelle et la sémantique catégorique. Notre sémantique catégorique est basée sur le modèle de Francisco Rios et Peter Selinger pour le langage programmation Proto-Quipper- M. Pourtant, pour formaliser le levage dynamique, nous construisons une catégorie de Kleisli en capturant la mesure quantique comme un effet de bord sur une catégorie concrète pour le circuit avec la mesure quantique. Nous prouvons le théorème de correction de la sémantique catégorique par rapport à la sémantique opérationnelle.