Memoire Online - Modèles formels pour l'informatique quantique

La sémantique opérationnelle de q-CCS sera donnée par transitions entre les configurations, étiquetés par actions. Une configuration est définie comme une paire (P, p) où p E P est un processus et p E D(H) indique l'état actuel de l'environnement.

Intuitivement, p est une instanciation (ou valorisation) des variables quantiques. Instanciations de variables classiques peuvent être effectuées indépendamment les unes des autres, mais les systèmes quantiques représentées par des variables différentes peuvent être mises en corrélation, car p est admis à être un état intriqué. L'ensemble des configurations est écrit Con. Soit

Actop = { [X]} où :X est une partie finie de Var et est un super-operateur dans HX est l'ensemble des opérations quantiques, et Actcom = {c?x, c!x : c E Chan et x E Var est l'en-semble des actions de communication, y compris les entrées et sorties. L'ensemble Act sera varié au cours de méta variables á, â, .... Nous avons besoin des notations suivantes pour les actions :

bv (á) est définis d'être la variable liée à á, c'est- à-dire bv (c?x) = X , et bv (ô), bv (î [X]) et bv (c!x) sont indéfinis.

Pour présenter la sémantique opérationnelle de q-CCS, nous avons besoin d'une notation plus auxiliaire. Pour tout X ? Var et super-opérateur î sur HX, l'extension cylindrique de î sur H est défini :

où _IHvar-X est l'opérateur identité sur HV _ar-X. Dans ce qui suit, nous supposons toujours que X est un ensemble fini de Var et î est un super-opérateur sur HX quand îX est rencontré. Ensuite, la sémantique opérationnelle de q-CCS est donnée comme un système de transition (Con, Act, ?), où la relation de transition ? est définie par les règles suivantes :

1. Tau : hô.P,pi4hP,pi

2. Oper : e[X]

hî[X].P,pi? hP,îX(p)i

3. Input : y ?/ fv (c?x.P)

hc?x.P,pi^c ?hPy/x,Pi

4. Output :
hc!x.P,pi^c!x?hP,pi

5. Choise : hP,Qi4hP',Q'i hP+Q,pi4hP',Q'i

hP,pi^c?x ?hP ',p'i

6. Intl1 :

(PkQ,pi^c?x?hP'kQ,p'ix(Q)

7. Intl2 : hP,piá?hP',p'i n'est pas une entrée
hPkQ,pi$hP'kQ,p'iá

hP,P)^c? hP^',pihQ,pi^c!x?hQ^',pi

8. Comm : hPkQ,pi4hPkQ',pi

9. Res : hP,pi4hP',p'i cn (á)?/L
hP/L,pi4hP'/L,p'i

10. Def : hP{y/ X},pi?hP ',p'i

A (x) =^def P

hA(x),pi4hP',p'i

L'operateur îX (.) dans la règle Oper a été défini par îX (.) =def IH(V ar_X).

Lors de passage de

sortie hc!x.P, pi ?^c!x hP, pi, le x-système est envoyé par le canal c. Notez que l'état actuel du x-système est spécifié dans p. Mais p n'est pas nécessaire d'être un état séparé, et il est possible que le x-système est empêtré avec le y-système depuis un certain y ? Var - {x}.

Par ailleurs, l'intrication entre le x-système et des y-systèmes (y ?/ Var - {x}) est conservée après l'action c!x. La transition d'entrée hc?x.P, pi ?^c?y hPy/x, Pi signifie que le y-système est reçu par le canal c, puis il est mis dans les occurrences (gratuit) de x dans P (Il peut y avoir plus d'un occurrences libres d'une seule variable x dans P, car il n'est pas nécessaire que fv (P) n fv (Q) = ö en somme P + Q). Il convient de noter que dans c?x.P la variable x est

lié et elle ne représente pas concrètement le x-système. Au contraire, il s'agit simplement d'une référence à l'endroit où le système reçu.

Ainsi, c?x.P peut exécuté l'action c?yavec y =6 x. La condition de côté y ?/ fv (c?x.p) pour le passage d'entrée est évidemment afin d'éviter les conflits nom de variable, et elle rend également que P {y/x} est bien définie. Au cours de l'exécution à la fois l'entrée et mesures de sortie, l'état de l'environnement n'est pas modifié. Passant systèmes quantiques qui se passe dans une communication décrit par la règle Comm, mais il est réalisé dans un système de «call-by-name" et ne modifie pas l'état de l'environnement.

Modèles formels pour l'informatique quantique

4.4.2.2 Sémantique Opérationnelle