Modèles formels pour l'informatique quantique

5.3.1 QML : langage de programmation fonctionnel quantique

QML [Altenkirch et Grattage, 2005] est un langage fonctionnel pour les calculs quantiques sur des types finis. Le langage présente des données quantiques et les structures de contrôle quantique, et intègre le calcul quantique réversible et irréversible. QML est basé sur la logique linéaire stricte, pour maitre l'affaiblissement en évidence, les programmes stricts sont libre de décohérence.

La conception de QML est guidée par sa sémantique catégorique : les programmes QML sont interprétés comme des morphismes dans la catégorie FQC de Finite Quantum Computations. Ceci fournit une sémantique constructive de calculs quantiques irréversibles réalisables comme portes quantiques. Les relations entre la catégorie FQC et son homologue réversible classique, FCC (Finite Classical Computations), sont également explorées dans [Grattage, 2006a].

La sémantique opérationnelle des programmes QML est présentée en utilisant des circuits quantiques standards, tandis que la sémantique dénotationnelle est donnée en utilisant les super opérateurs.

5.3.1.1 La conception de QML

QML [Grattage, 2006b] possède à la fois des données quantique et le contrôle quantique, QML permet la contraction mais les contrôles affaiblissement et la mesure implicite. QML utilise

49

chapitre5 : Langages de programmation quantiques

une logique strictement linéaire avec un opérateur d'affaiblissement explicite, mais avec des contractions implicites. Cela se justifie par le fait que la signification d'un programme peut être affectée par le changement des affaiblissements, mais pas par les contractions déplacées. Deux opérateurs conditionnels sont également introduits : if, qui mesure un qubit, et if⁰, ce qui ne permet pas de mesurer, mais qui n'exige que les branches orthogonales. Cette exigence se traduit par l'introduction d'un jugement orthogonal à des conditions QML qui invoquent if⁰. La conception de QML est également motivée par la considération de la sémantique opérationnelle: la catégorie FQC. De la même manière que la catégorie FQC des calculs quantiques a été défini par analogie à la catégorie FCC de calculs classiques, le langage QML est conçu pour être aussi proche de formalismes classiques tant que possible. En effet, un sous-langage classique de QML pourrait être défini qui utilise FCC de sa sémantique opérationnelle, plutôt que FQC.

5.3.1.2 La syntaxe de QML

La syntaxe et les règles de typage de QML [Grattage, 2006b]sont basées sur la logique linéaire stricte : les contractions sont implicites, tandis que les affaiblissements sont une opération explicite qui correspondent à des mesures. Les types de QML sont de premier ordre et fini. Il n'y a pas de types récursifs, donc, par exemple, un type de nombres naturels quantique ne peut être définie. Le constructeur de type de QML est le produit tensoriel, ?, ce qui correspond à un type de produit. Qubits et superpositions de qubits simples sont des primitives. QML a deux constructions : if, qui mesure un qubit dans les données qu'il analyse (le classique-if), et if⁰, qui ne mesure pas, mais exige que les résultats soient toujours existés en sous-espaces orthogonaux (le quantum-if). Les preuves de l'orthogonalité peuvent être insérées automatiquement par le compilateur, et donc ne figurent pas dans la syntaxe des termes. Les symboles grecs u, r, p sont utilisés pour parcourir des types QML, qui sont donnés par la grammaire suivante :

u = ö1|ö2|u ? r

Un approvisionnement infini de noms de variables concrètes est supposé, et x, y, z sera utilisée pour parcourir sur les noms. Les contextes de typage (F, z) sont donnés par :

F =.|F,x : u

Où . représente le contexte vide, mais il sera omis si le contexte est non vide. Pour plus de simplicité, on suppose que chaque variable apparaît au plus une fois. Les contextes correspondent à des fonctions d'un ensemble fini de variables à des types.

Pour définir la syntaxe des expressions les constantes ê, é E C sont également utilisés, et variables

50

chapitre5 : Langages de programmation quantiques

de la fonction sont utilisés pour désigner les programmes QML préalablement définis. Les termes de QML consistent en celles d'un langage fonctionnel du premier ordre, à des données étendu quantique, une structure de commande quantique, et un opérateur de mesure. La grammaire des termes QML est définie comme suit :

(variables) x, y, .... E Vars

(prob,amplitudes) k, é, ... E C

? |qtrue y |0|k×t|t+u

(patterns) p, q ::= x|(x, y)

?

(termes) t, u ::= x|x^y |()|(t, u)| let p = t in u| if t then u else ^u0|if° t then uelseu'|qfalse

?

Ici, la notation vectorielle á est utilisée pour des séquences d'objets syntaxiques. Formellement,

elle correspond au méta notation suivante :

? á= å

|á ?á

Les données quantiques sont modélisées en utilisant les constructions kxt, t+u, avec la constante 0 formé des termes avec une amplitude de probabilité zéro. Le terme k x t, où k est un nombre complexe, associe l'amplitude k de probabilité avec le terme t. Le terme t + u décrit une superposition quantique de t et u. Les superpositions quantiques sont des valeurs de premier ordre, et peuvent être utilisés dans une condition pour donner un contrôle quantique. Par exemple, if⁰(qtrue + qfalse)then t else u

Evalue à la fois t et u tout en conservant les résultats dans une superposition quantique. Comme un exemple de superpositions formant, le terme ^v12 x qfalse + ^v12 x qtrue est une superposition de qfalse et qtrue. Les facteurs de Normalisation qui sont égaux sont parfois omises, et peuvent ensuite être déduites d'être égaux ; l'exemple précédent devenir simplement qfalse + qtrue.