Logique linéaire

Le rapport entre la logique et le monde des calculs typés (et la programmation fonctionnelle en particulier) est assez vénérable. Concrètement, tous se rappellent la correspondance de Curry-Howard entre : types et propositions ; et : termes (ou programmes) et preuves.
Ainsi, puisque dans la logique la proposition $a \to b \to a$ est vraie, un tel type existe, le programme qui définit la fonction dont le type serait a -> b -> a passera par le type-checker. Par contre, il n'existe aucune fonction polymorphe de type a -> b, ceci n'est pas une tautologie (toutes les variables ici sont quantifiées universellement). Bien sûr, pour des types concrets (surtout b), de telles fonctions existent, car $\forall a, a \to T$.

On peut formuler tout ceci d'une autre façon : un programme qui transforme le type a en b constitue une "preuve", dont les prémisses sont $a$ et la conclusion : $b$.

En 1986/1987 Jean-Yves Girard a proposé - en analysant des modèles du lambda-calcul typé et ses relations avec la logique, un schéma un peu différent du traditionnel, similaire à l'algèbre/géométrie linéaire. Le modèle contenait une "implication linéaire" dénotée : $A \multimap B$, où $A$ peut être utilisé une et une seule fois. L'idée est que l'antécédent d'une proposition constitue une ressource, consommée par la preuve.


Les principes structurels dans le calcul des séquents connus comme la contraction et l'affaiblissement sont supprimés. Pas de : $$ \frac{A, A,\Gamma \vdash \Delta}{A, \Gamma \vdash \Delta}\,, \qquad \text{ni} \qquad \frac{\Gamma \vdash \Delta}{A, \Gamma \vdash \Delta}\,. $$ Par contre, des nouveaux connecteurs ont vu le jour, la conjonction et la disjonction classiques : $\wedge, \vee$ ont été scindés, la logique contient

De plus, la négation : $A^\bot$ devient une vraie involution, $(A^\bot)^\bot = A$. On considère que ceci est l'opération de dualité. On peut écrire : $A^\bot \equiv A \multimap \bot$.

Plusieurs identités méritent d'être connus, par ex. $A \multimap B \equiv A^\bot \parr B$. La logique contient encore des opérateurs connus comme "exponentielles", par ex. $!A$ signifie : "prends un nombre quelconque de $A$". On le lit : "bien sûr !". L'opérateur $?$ est lu "pourquoi pas?" et figure dans quelques preuves. Quelques "lois de De Morgan" prennent les formes :


$$ (A\otimes B)^\bot \equiv A^\bot \parr B^\bot ; \qquad (A\oplus B)^\bot \equiv A^\bot \& B^\bot ; \qquad (!A)^\bot = ?A^\bot\,. $$

Comme la "science de la vérité", un élément de l'analyse du langage, la LL semble un peu exotique, et Girard était parfaitement conscient que ceci commence à vivre dans le contexte de la dynamique des preuves, et de la correspondance de Curry-Howard en particulier.

Et c'est ici où nous pouvons voir un peu plus de sens logique dans la description fonctionnelle des objets quantiques. Avec les types fonctionnels et les applications linéaires, on peut réellement profiter de la correspondance de Curry-Howard. Les matrices restent des objets algébriques linéaires, sans aucune logique naturelle.

Chez nous, la dualité est ... la dualité. Le produit tensoriel est ... le produit tensoriel, et nous n'avons pas besoin d'un système composite pour l'apprécier. Un opérateur agissant sur un simple vecteur est constitué de produits, projecteurs $\dyade{\alpha}{\beta}$.

La logique linéaire dispose d'une équivalence : $A \multimap A \cong A^\bot \otimes A$. (Selon Barr, ceci est valide dans les catégories dites compactes, ce qui implique la dimension finie de l'espace de Hilbert sous-jacent, mais pour les informaticiens ceci n'est pas grave. Les physiciens sont moins heureux). Si $A$ est le type de nos axes, dans $\dyade{\alpha}{\beta}$ : $\ket{\alpha}$ est un ket, and $\bra{\beta}$ - un axe, alors 

ax_proj = \ax -> (alpha ax) *> beta


et le dual : kt_proj = \kt -> (ket beta kt) *> alpha, toujours un produit.

Mais ceci est compatible avec nos définitions récursives du produit tensoriel (j'aurais dû les mentionner dans la section précédente...). Pour les scalaires c'est un produit dans un Module algébrique (ou dans VSpace) 

s <*> v = s *> v
et récursivement, si u est un vecteur ou tenseur d'ordre supérieur : 
u <*> v = \x -> u x <*> v


Notre approche aux "codes quantiques" a l'avantage - par rapport à toute sorte de "langages quantiques" (Selinger, Van Tonder, Sabry ...) de s'approcher le plus au formalisme de la logique. On ne triche pas (comme quelques uns, pour qui la transmission de l'information quantique par l'intrication est un "effet de bord", "sous la moquette"...

Ils ne comprendront pas que l'Univers boude les effets de bord. Tout est explicit, renforcé par l'unitarité des transformations (conservation des normes). Mais pour mes amis l'Univers est dans leur têtes...


Continuation-passing style dans la sauce quantique

Un rappel sommaire du CPS, le paradigme fondamental de sérialisation et de dé-hiérarchisation des applications dans la programmation fonctionnelle. Au lieu de prendre une donnée x et lui appliquer une fonction, (f x), et ainsi de suite : g (f x)). . . , on demande à ce que toute fonction f prenne un paramètre supplémentaire - le "futur", une fonction appelée continuation, qui fait quelque chose avec le résultat de f. Si la fonction "normale" f est définie : f x = ..., La fonction "continuée" f' aura la définition f' x = \k -> .... La factorielle écrite en CPS aura la forme 

fact n = fcc n id where
 fcc n = \knt -> if n==0  then knt 1 
                 else fcc (n-1) (\z -> knt (n*z))
Ceci permet de coder toute fonction récursive comme récursive terminale (mais en économisant la pile système on encombre le tas avec la création des fermetures locales...) Or, constatons, que nos états quantiques primitifs ont une telle forme. Un ket $\ket{\alpha}$ c'est \ax -> ax alpha. Un phénomène similaire se produit quand on essaie de "quantiser" une manipulation classique opclas, par exemple faire tourner un spin. Omettons les détails ; nous aurons quelque chose comme 


opquant psi = \ax -> psi (\alpha -> ax (opclas alpha))
threelin (2K) Alors, les axes "jouent le rôle de continuations" pour les kets, et ce sont des continuations linéaires, exploitables une fois.

La forme du transfert de contrôle donne une réponse à la question : comment un opérateur tensoriel ("multi-ligne") peut produire un résultat qui - justement - s'exprime par plusieurs lignes? Nous voulons UN objet. On peut faire un "multi-ket", mais son dual est une Hydre à plusieurs têtes... Ici des multiples continuations entrent en scène...

Terminons donc par une observation méthodologique. Un état quantique n'est pas un "objet", une donnée. C'est un calcul (computation) toujours en attente d'une "finalisation", la réduction par un observateur, le calcul des probabilités, etc., ce qui sort de notre cadre. Pour l'instant nous constatons que nous n'avons nullement besoin d'un "langage quantique" spécifique. Le monde fonctionnel semble être très bien adapté à la description du monde quantique. Sommes-nous tous des fonctions?...