Logique linéaire

La logique linéaire (LL), inventée par le logicien Jean-Yves Girard en 1986, est un produit de la théorie de la démonstration moderne. Elle résulte d'une analyse du comportement des preuves des logiques classique et intuitionniste au travers de la procédure d'élimination des coupures introduite par Gentzen en 1936 pour prouver son Hauptsatz (un résultat fondamental en logique).

La logique linéaire promeut une vision géométrique des syntaxes formelles en cultivant l'analogie avec l'algèbre linéaire (espaces cohérents) et en introduisant de nouvelles représentations des preuves utilisant des graphes (réseaux de preuves), voire des opérateurs (géométrie de l'interaction). Elle a également permis à Girard de proposer une approche logique de la complexité algorithmique (logique linéaire légère et élémentaire). Elle a connu un grand succès, notamment en informatique théorique, sans doute à cause des nombreux outils originaux qu'elle introduit et parce qu'elle décompose les logiques intuitionniste et classique, fournissant donc un cadre unifié pour l'étude de celles-ci.

Origine de la logique linéaire

La logique linéaire est née de l'étude d'un modèle dénotationnel des termes du lambda-calcul typé, c’est-à-dire via la correspondance de Curry-Howard, des preuves de la logique intuitionniste. C'est en effet en développant le modèle des espaces cohérents que Girard a remarqué que l'on peut y définir une notion de fonction linéaire (en un sens très proche des fonctions linéaires entre espaces vectoriels), qui permet de décomposer toute fonction de $A$ dans $B$ en une fonction non linéaire générique de $A$ dans $!A$ et une fonction linéaire de $!A$ dans $B$ ($!A$ est un espace cohérent associé à $A$ dont la construction rappelle celle d'algèbre tensorielle). Cette propriété se résume par la formule fondatrice de la logique linéaire :

Fichier:LL intuitionnistic impl.png

où le membre gauche désigne l'espace des fonctions de $A$ dans $B$ alors que le membre droit désigne l'espace des fonctions linéaires de $!A$ dans $B$.

Syntaxe

Les connecteurs de la logique linéaire propositionnelle classique (CLL) sont :

• la négation linéaire notée $A^{\bot }$ ou $nil(A)$ ;
• une conjonction et une disjonction multiplicative : le tenseur ($\otimes$) et le par ($\wp$) ;
• une conjonction et une disjonction additive : le avec (&) et le plus ($\oplus$) ;
• deux modalités exponentielles : le bien sûr (!) et le pourquoi pas (?) ;
• la flèche linéaire est définie au moyen de la négation linéaire et de la disjonction multiplicative : Fichier:LL def impl.png

Il y a deux syntaxes principales pour écrire les preuves : le calcul des séquents et les réseaux de preuves. Le théorème de séquentialisation assure que l'on peut traduire toute preuve d'une syntaxe à l'autre. Les deux syntaxes satisfont le théorème d'élimination des coupures.

Les réseaux de preuves sont des hypergraphes dont les sommets sont des formules reliées au moyen d'hyperarêtes représentant les règles logiques. Ils forment une syntaxe très synthétique munie de nombreuses propriétés géométriques, mais complexe à définir, aussi il est plus simple d'aborder la logique linéaire du côté calcul des séquents.

Calcul des séquents linéaire

Le calcul des séquents linéaire s'obtient à partir du calcul des séquents classique en supprimant les principes structurels de contraction et d'affaiblissement. Cette suppression est la cause du dédoublement des connecteurs de conjonction et de disjonction.

Groupe identité

${\frac {}{\vdash \Gamma ,A,A^{\bot }}}(axiome)\qquad \qquad \qquad {\frac {\vdash \Gamma ,A\quad \vdash A^{\bot },\Delta }{\vdash \Gamma ,\Delta }}(coupure)$

Groupe multiplicatif

${\frac {\vdash \Gamma ,A\quad \vdash B,\Delta }{\vdash \Gamma ,A\otimes B,\Delta }}(\otimes )\qquad \qquad \qquad {\frac {\vdash \Gamma ,A,B}{\vdash \Gamma ,A\wp B}}(\wp )$

Groupe additif

${\frac {\vdash \Gamma ,A\quad \vdash \Gamma ,B}{\vdash \Gamma ,A\ {\mbox{avec}}\ B}}({\mbox{avec}})\qquad \qquad \qquad {\frac {\vdash \Gamma ,A_{i}}{\vdash \Gamma ,A_{1}\oplus A_{2}}}(\oplus _{i})$

Groupe exponentiel

${\frac {\vdash \Gamma ,?A,?A}{\vdash \Gamma ,?A}}(contraction)\qquad \qquad \qquad {\frac {\vdash \Gamma ,A}{\vdash \Gamma ,?A}}(dereliction)$

${\frac {\vdash \Gamma }{\vdash \Gamma ,?A}}(affaiblissement)\qquad \qquad \qquad {\frac {\vdash ?\Gamma ,A}{\vdash ?\Gamma ,!A}}(promotion)$

Quelques formules linéaires remarquables

Voici quelques unes des principales formules prouvables (par exemple en calcul des séquents) en logique linéaires. Dans ce qui suit le symbole $\equiv$ représente l'équivalence linéaire :

Fichier:LL def equiv.png

Lois de De Morgan

Distributivité

Fichier:LL iso distrib.png

Isomorphisme exponentiel

Fichier:LL iso expo.png

Remarquons que grâce aux lois de De Morgan, chacune de ces équivalences a une duale, par exemple la négation d'un pourquoi pas est le bien sûr de la négation, le par distribue sur le avec...

Pour finir voici une tautologie linéaire importante, qui n'est toutefois pas une équivalence :

Semi-distributivité

Fichier:LL semi distributivity.png

Interprétation des formules

Du point de vue traditionnel où la logique est vue comme science de la vérité ou comme analyse du langage, la logique linéaire avec ses deux conjonctions, ses deux disjonctions, ses modalités exponentielles, peut sembler un peu ésotérique. Elle se comprend beaucoup mieux au travers de la correspondance de Curry-Howard.

Une interprétation naturelle des formules de la logique linéaire est de les voir comme des types, c’est-à-dire des descriptions formelles des comportements entrée/sortie des programmes. À l'instar de la logique intuitionniste (ou plus précisément de la formalisation de la logique intuitionniste), la logique linéaire est constructive au sens de Curry-Howard, c’est-à-dire que les démonstrations (formelles) de LL peuvent être vues comme des programmes dont les entrées sont typées par les formules en hypothèse et les sorties par les formules en conclusion. La logique linéaire diffère toutefois de la logique intuitionniste sur un point essentiel : elle dispose d'une négation qui satisfait toutes les symétries que l'on trouve en logique classique sous le nom de lois de De Morgan : la négation est involutive, la négation d'une conjonction est la disjonction des négations, etc. De plus par rapport à la logique intuitionniste, LL ajoute un degré supplémentaire d'expressivité en permettant de spécifier des relations fines entre les entrées et les sorties des programmes.

Si l'on considère par exemple la formule A$-\!\circ$B, A implique linéairement B, du point de vue traditionnel elle exprime que l'on peut dériver la propriété B en utilisant l'hypothèse A une et une seule fois. Cette contrainte peut sembler arbitraire et se comprend sans doute mieux en la transposant via Curry-Howard en la phrase : un programme de type A$-\!\circ$B prend une entrée de type A et utilise celle-ci exactement une fois pour calculer son résultat de type B. Un tel programme peut donc faire l'économie d'allouer un espace mémoire spécifique dans lequel sauvegarder la valeur de son entrée, ou plus précisément un tel programme consomme son entrée au cours du calcul (typiquement un automate fini consomme entièrement une et une unique fois le mot passé en entrée).

Dans ce cadre, la négation linéaire $nil(A)$ d'une formule A n'a pas vraiment d'interprétation simple selon le point de vue traditionnel. Par contre elle se comprend bien comme type : un programme de type $A$ est un programme qui produit un résultat de type $A$ ; un programme de type $nil(A)$ est un programme qui utilise linéairement une entrée de type $A$. La négation linéaire exprime donc la dualité entre les entrées et les sorties et l'on comprend mieux qu'elle soit involutive : une sortie de type $nil(A)$ est une entrée de type $A$.

On peut donner un autre cadre d'interprétation, celui de la notion de ressources. Dans ce cadre, le caractère idempotent des connecteurs de l'algèbre de Boole pose des problèmes. Par exemple l'idempotence du $\vee$ se traduit par la formule :

$A\vee A\equiv A$

Elle signifie que toute ressource $A$ peut être dupliquée. Cette idempotence empêche de considérer simplement les aspects quantitatifs des ressources.

Cette propriété implique aussi qu'un fait est une vérité éternelle. C'est un autre des grands points faibles du paradigme logique quand il s'agit de réprésenter des systèmes dynamiques qui comportent peu de vérités eternelles mais beaucoup de vérités fugaces. Comme par exemple les états du système.

Certains des connecteurs linéaires $\otimes$, $\wp$ et $-\circ$ ont été défini par Girard en rejetant cette propriété.

Dans ce cadre les opérateurs multiplicatifs ainsi que $nil$ trouvent une signification simple et naturelle :

• le fois : $A\otimes B$ signifie la conjonction des ressources $A$ et $B$ ;
• le par : $\wp$ signifie que les ressources $A$ et $B$ sont utilisables mais pas de façon conjointe ;
• l'implication linéaire : A$-\circ$B signifie la transformation de $A$ en $B$. A est consommé et est transformé en B. Cette notion est essentielle pour la représentation des systèmes dynamiques. ;

• $nil(A)$ a une interprétation simple : il s'agit du besoin de A. C’est-à-dire $-A$ .

Références

• J.-Y. Girard, Linear Logic, Theoretical Computer Science no 50, 1987
• Advances in Linear Logic, London Mathematical Society Lecture Notes Series no 222, Cambridge University Press, 1995
• Linear Logic in Computer Science, London Mathematical Society Lecture Notes Series no 316, Cambridge University Press, 2004