Modèles formels pour l'informatique quantique

4.3 Sémantiques dénotationnelles

PERDRIX dans [Perdrix, 2006] présente trois sémantique dénotationnelle qui sont Sémantique observable, Sémantique admissible et une Sémantique pure. On va voire la sémantique pure.

37

chapitre4 : Modèles de calcul quantique

4.3.1 Sémantique pure :[|.|]

Associée a chaque q-terme une fonction agissant sur des distributions probabiliste.

V (x) : L'ensemble des évolutions discrètes V sur l'ensemble X V =¹(x) : L'ensemble des évolutions vérifiant V (x) = 1.

Soit P un q-terme P = (K, I, F, R) et R :

?q de H dans H^', [|a|] : H ? V =1(H')

est [|M|] = ë|ö)(ö|M†M|ö).ç M|öi

vhö|M M|öi

[|M|] Est définie même pour |ö) tant que (ö|M†M|ö) = 0 par [|M|](|ö)) = 0 ?q E F, [|q|] : H1 q ? V =¹(SF) Est [|q|] = ë|öi.ç(q,|öi)

?q E F, [|q|] Fonction continue.

4.4 qCCS

4.4.1 Introduction

Une algèbre q-CCS [YING et al., 2003] des processus quantiques purs dans laquelle les communications en déplaçant physiquement états quantiques sont autorisées et les calculs sont modélisés par des super-opérateurs, mais aucune donnée classique est explicitement concernée. Une sémantique opérationnelle de q-CCS est présentée en termes de systèmes de transitions étiquetées (non probabiliste). La bisimulation forte entre les processus modélisés dans q-CCS est définie, et de ses propriétés fondamentales algébriques sont établis, y compris unicité des solutions d'équa-tions récursives. Pour modéliser calcul séquentiel dans q-CCS, un rapport de réduction entre les processus est défini. En combinant ce qui concerne la réduction et la bisimulation forte, nous introduisons la notion de réduction-bisimulation forte, qui est un dispositif d'observation de l'interaction de calcul et de communication dans les systèmes quantiques. Enfin, la notion de bisimulation forte approximative et son homologue de réduction sont introduits. Il est prouvé que les deux similarité approximatives et la réduction-bisimilarité approximative sont conservées par les divers constructeurs du calcul quantiques. Cela nous donne un outil formel pour observer la robustesse des processus quantiques contre inexactitude dans la mise en oeuvre de ses portes élémentaires.

Préliminaires

On a vu déjà les espaces de Hilbert et les opérateurs unitaires, le produit tensoriel et la mesure quantique mais que ce qu'un super-opérateur

Super-opérateurs :

La dynamique des systèmes quantiques ne peut pas être décrite par des opérateurs unitaires, et

38

chapitre4 : Modèles de calcul quantique

l'un de ses formalismes mathématiques est la notion de super-opérateur. Un super-opérateur sur un espace de Hilbert H est un opérateur linéaire à partir de l'espace d'opérateurs linéaires sur H dans lui-même qui satisfait aux deux conditions suivantes:

- tr [ (p)] tr (p) pour chaque p E D (H).

- Positivité complète : pour tout espace de Hilbert supplémentaire HR , ('R ® ) (A) est positif fourni.

A est un opérateur positif sur HR ® H, où 'R est l'opération d'identité sur les HR.

Si la première condition est renforcée à tr [ (p)] = tr (p) pour chaque p E D (H), alors est dit être tracepreserving.