Compilation d'oracle pour calcul quantique.
Contexte.
En calcul quantique, on utilise une mémoire d'un type particulier, où l'information est encodé sur l'état de particules quantiques. Les lois de la mécanique quantique permettent de modéliser le comportement d'un tel système, et de nombreux algorithmes dit "quantiques" ont été conçus pour capitaliser sur le comportement non-classique de ce type de mémoire et résoudre de façon efficace un grand nombre de problèmes classiques.
Lors de l'interaction avec la mémoire quantique, on doit donc encoder la structure du problème classique (l'entier à manipuler, le graph à traverser, la matrice à traiter...) en instructions élémentaires quantiques. C'est ce qu'on appelle l'oracle. Le problème que l'on rencontre est que la mémoire quantique n'accepte à priori que des opérations réversibles: il s'agit donc de traduire une description classique en une séquence d'opérations réversibles.
Ces opérations peuvent être codées par un circuit réversible. Un circuit réversible est un circuit booléen utilisant des portes logiques... réversibles. Par exemple, la porte logique "NON", qui transforme "vrai" en "faux" et "faux" en "vrai" est réversible: elle est son propre inverse.
Un résultat bien connu est qu'étant donnée une fonction booléenne
f : Bool^n -> Bool^m
il est possible de générer un circuit réversible calculant
f' : Bool^n x Bool^m ----> Bool^n x Bool^m
(x,y) |---> (x, y XOR f(x))
Un tel circuit peut être généré comme la trace partielle d'exécution d'un programme. Par exemple, le programme (écrit en syntaxe Haskell)
my_and :: [Bool] -> Bool my_and = foldl (&&) True
prenant en entrée une liste de booléens et calculant la conjonction de tous les éléments de la liste génère le circuit
pour une liste de taille 5. On a 5 fils d'entrées, et le résultat du calcul se trouve sur le dernier fil de sortie. Chaque porte dans le circuit est une porte Toffoli, qui fait l'opération
(a,b,c) |--> (a,b,c ⊕ (ab))
(avec les fils lus de haut en bas). Ce système permet de transformer automatiquement un programme fonctionnel en un circuit réversible, et ce qui est utilisé dans le langage de programmation quantique Quipper [1,2].
Travail à réaliser.
L'objectif est de proposer une chaine de compilation de fonctions booléennes décrite dans un langage fonctionnel vers des circuits réversibles, en vue de proposer une bibliothèque de circuits et d'étendre la bibliothèque RevKit [3].
Vous commencerez avec un lambda-calcul typé de style PCF, avec booléens et listes, et un modèle simple de compilation en circuit réversible sans optimization particulière [1,2]. Votre travail consistera à trouver un système de type et un ensemble d'optimization de code adapté à la génération du circuit le plus petit possible.
Par exemple, le circuit suivant est généré par une implémentation de l'addition sur des entiers encodés sur 3 bits.
Après une série d'optimisations de circuit (donc après la compilation), on peut obtenir le circuit
Pourrez-vous faire aussi bien en travaillant en amont de la génération du circuit ?
Dans un deuxieme temps, vous interfacerez votre compilateur de haut-niveau avec un outil d'optimisation de bas-niveau, par exemple [4] et étudierez le facteur de compression obtenu en fonction des contraintes choisies
Le travail comportera à la fois une partie pratique (écriture du compilateur) et une partie théorique (design du système de type et des règles d'optimisation de code).
Encadrant : Benoit Valiron <benoit.valiron@lri.fr>.
Lieu du stage : Laboratoire de Recherche en Informatique (LRI), Univ. Saclay.
References
[1] Quipper. http://www.mathstat.dal.ca/~selinger/quipper/
[2] B. Valiron. Generating reversible circuits from higher-order functional programs. Proceedings of the 8th International Conference on Reversible Computation (RC'16), LNCS vol. 9720, pp. 289-306, 2016.
[3] http://www.revkit.org/
[4] Mathias Soeken, Gerhard W. Dueck, D. Michael Miller. A fast symbolic transformation based algorithm for reversible logic synthesis. In Proceedings of RC'2016, pages 307–321.