4.4.2 Syntaxe et Sémantique Opérationnelle
[YING et al., 2003]
Soit Chan l'ensemble des noms de canaux quantiques,
et soit Var soit l'ensemble des variables quantiques. On suppose que
Var est un ensemble infini dénombrable. Nous allons utiliser
méta variables c, d, ... pour aller sur Chan et x,
y, z, ... pour aller sur Var. Soit ô le nom de
l'action silencieuse.
Pour chaque variable quantique x E Var,
Imaginez que nous avons un système quantique nommé par
x. Soit HX un espace de Hilbert complexe de dimension finie,
qui est l'espace d'état du système de x. Pour tout
x, y E Var, si HX = HY , alors on dit que
x et y ont le même Type. Imaginez encore qu'il existe
un système quantique grand composé de tous les x
-systèmes, x E Var, dans lequel l'ensemble de nos
processus quantiques demeurent. Nous appelons ce système composé
l'environnement de notre calcul. Supposons HX
®x?X Hx
Pour tout X c Var. Alors H = HV
ar est l'espace d'état de l'environnement. Notez que H
est un espace de Hilbert de dimension infinie dénombrable.
Nous supposons un ensemble de régimes constants du
processus, variait en charge par méta variables A, B ... Pour
chaque processus constant A, une arité non négatif
ar (A) est attribué. Soit x =
x1, x2, . . . ,
xar(A)
un triplet de variables quantiques distincts. Puis A
(x) est appelé un processus constant. Nous
écrivons P pour l'ensemble des processus quantiques, et nous
écrivons fv (P) pour l'ensemble des variables quantiques libre
en P pour chaque processus quantique p E P .
Maintenant, nous sommes prêts à présenter la syntaxe de
q-CCS.
4.4.2.1 La syntaxe
Définition 14. Les processus
quantiques sont définis inductivement par les règles de formation
suivantes :
(1) chaque processus constant A (x) est dans P et
fv (A (x)) = {x}
39
chapitre4 : Modèles de calcul quantique
(2) nil ? P et fv (nil ) = ç
(3) si p ? P, alors ô.p ? P et fv
(ô.p) = fv (p)
(4) sip ? P, X est une partie finie de Var, et
est un super-opérateur sur Hx, alors [X] .p ?
P , et fv ( [X] .p) = fv (p) ? X
(5) si p ? P, alors c?x.p ? P et fv
(c?x.p) = fv (p) - {x}
(6) si p ? P et x ?/ fv (p), alors
c!x.p ? P et fv (c!x.p) = fv (p) ? {x}
(7) si p, q ? P, alors p + q ? P et fv
(p + q) = fv (p) ? fv (q)
(8) si p,q ? P et fv (p) n fv (q) =
ç, alors p||q ? P et fv (p||q) = fv (p)
? fv (q)
(9) si p ? P et L ? Chan, alors p L
? P et fv(p L) = fv(p)
En utilisant la grammaire BNF standard la syntaxe de qCCS
peut être résumée comme suit: P := A (x)
|nil|ô.p| [X]
.p|c?x.p|c!x.p|p +
p|p||p|P L
Il est semblable à la syntaxe de CCS classiques, et les
seules différences entre eux sont :
- La clause 4 de la définition ci-dessus nous permet
d'effectuer des opérations quantiques sur certains systèmes
sous-jacent.
- La condition x ?/ fv (p) dans la clause 6
et la condition fv (p) n fv (q) = ç dans la clause
8 sont nécessaires en raison du fait bien connu que
l'information quantique inconnu ne peut être parfaitement clonée,
(à la différence des bits classiques qui peuvent être
copies et multiplies autant de fois que l'on veut, un qubit ne peut pas
être dupliqué. Ce résultat essentiel est connu sous le nom
de théorème de non-clonage. Il est à la base de la
sécurité des processus de cryptographie quantique).
Il est à noter que ces conditions nous obligent
à affecter un ensemble de variables quantiques libres pour chaque
constante à l'avance processus. Les opérations quantiques peuvent
être considérées comme des constructions pour le calcul
quantique séquentiel. Il y a également des constructions pour le
calcul séquentiel dans CCS passing value, mais ne sont pas explicitement
donnés. Ici de telles constructions sont implicitement pris en charge
dans les valeur des expressions, de sorte que l'on peut concentrer l'attention
sur l'examen des comportements de communications entre les processus.
Cependant, nous présentons explicitement les constructions pour le
calcul quantique séquentiel dans la syntaxe de q-CCS, et c'est l'un des
principaux objectifs d'observer l'interaction entre le calcul quantique
séquentiel et de la communication de l'information quantique.
L Fait la liaison de tous les noms de canal par
L, et l'entrée préfixe c?x lie la variable
x quantique. Le symbole=á sera utilisé pour
désigner á convertibilité des processus
définis en remplaçant les variables quantiques liés dans
la manière standard.
Pour chaque régime constant de procédé
A, une équation de définition de la forme :
40
chapitre4 : Modèles de calcul quantique
A (x) =def P
est supposée, où P est un processus
avec fv (P) Ç {x}. La définition
récursive dans q-CCS est différente de celle de CCS classiques
d'une certaine façon complexe. Par exemple, dans q-CCS
A (x) =def c!x.A (x)
n'est pas autorisé à être
l'équation définissant de schéma constant des processus
A. En fait, si x E fv (A (x)), alors c!x.A (x) n'est
pas un processus, et si x E/ fv (A (x)), alors fv (c!x.A (x)) fv
(A (x)). Cependant,
A (y) =def c?x.c!xA (y)
Est une équation légitime définissant
A.
| 
