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.

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, tandis qu'avec les matrices on n'a que l'algèbre linéaire standard.

$A \cong B$




teleport_big-1 (53K) Commençons doucement. Monty, téléportation !

Plusieurs fans de Star Trek, ou de science-fiction en général se sont posé une question cauchemardesque : et si ce malheureux Kirk avait été reconstitué deux fois ou plus? Après tout, dès que l'information concernant les corps des voyageurs passe dans la machine de téléportation, elle peut être stockée et transmise, disons, 47 fois, créant une formidable pagaille juridique: qui est le "vrai"?

La question d'identité d'un objet est une sérieuse question philosophique. Si on peut copier l'information "gratuitement", et si cette information équivaut à une réalisation physique de quelque chose, les paradoxes sont inévitables. Dans le monde physique classique le problème ne se pose pas, on peut par décret affirmer que tous les objets soient différents. Mais en physique quantique les objets identiques sont vraiment identiques, l'impossibilité de distinguer entre deux électrons (protons, mésons, etc.) est cardinale, et pleine de conséquences observables (cela change la statistique de Boltzmann en Fermi [ou Bose], change la thermodynamique, et tout !) Alors, comment éviter ce paradoxe sans tricher (disant que de toute façon on ne pourra jamais obtenir la totalité des informations sur Kirk ; il suffit que Kirk soit un seul atome !).

La réponse existe. En 1982 Wooters, Żurek et Dieks ont formalisé le théorème de non-clonage, l'affirmation (connue avant mais intuitivement) qu'un état quantique qui n'est pas connu a priori ne peut être copié. Le processus de copie détruit obligatoirement l'original, et la destruction accompagne la reconstitution, donc on ne peut pas reconstituer un objet deux fois, il faut toujours un "original", réduire l'information quantique à l'information classique est impossible. Le processus de téléportation implique la nécessité de transférer au préalable une forte dose d'information quantique, sous forme des sous-systèmes intriqués (entangled), qui n'ont rien à voir avec l'objet téléporté, mais qui est détruite lors du transfert, ensemble avec l'original. Le sous-système distant "devient" le clône.

Revenons aux sources du problème.

Une transformation en informatique est l'application d'une fonction, dont le type est noté comme une implication logique $A \to B$. Or, en logique on peut réutiliser la prémisse $A$ plusieurs fois dans une preuve ; en programmation (fonctionnelle ou autre) on peut en principe appliquer une fonction et garder l'original.

Mais dans la logique linéaire de Girard, il existe le connecteur $\multimap$ : l'"implication linéaire". Quand on exploite $A \multimap B$, on n'a plus le droit d'utiliser $A$...

Vous voyez l'analogie?

siala baba $zoau$ $\ket{0} \quad \braket{1}{z} \; \bra{1} mm$ dziadek wiedzial $ \opavg{U_z}{\hat{A}}{0}$ a $\dyade{pzdrum}{frouk}$ srubka

$$ A \simbot B \multimap C \parr D \otimes E^\bot + K$$

Qu'est-ce que c'est?