Logique linéaire

Arbre de résolution linéaire^[Quoi ?]

En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire est un système formel inventé par le logicien Jean-Yves Girard en 1987. Du point de vue logique, la logique linéaire décompose et analyse les logiques classique et intuitionniste. Du point de vue calculatoire, elle est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources.

La logique classique n'étudie pas les aspects les plus élémentaires du raisonnement. Sa structure peut être décomposée dans des systèmes formels plus élémentaires qui décrivent des étapes plus fines de la déduction ; en particulier, il est possible de s'intéresser à des logiques où certaines règles de la logique classique n'existent pas. De telles logiques sont appelées des logiques sous-structurelles. L'une de ces logiques sous-structurelles est la logique linéaire ; il lui manque en particulier la règle de contraction de la logique classique qui dit en gros que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle d'affaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement.

La vision programmatoire et la vision géométrique

La logique linéaire peut se comprendre au travers de la correspondance de Curry-Howard comme un système de typage des programmes d'ordre supérieur (lambda-calcul typé) permettant d'exprimer la manière dont ceux-ci gèrent leurs ressources, et notamment le fait qu'une ressource soit consommée linéairement, c'est-à-dire une et une seule fois pendant l'exécution du programme.

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/programmes utilisant des graphes (réseaux de preuves), voire des opérateurs (géométrie de l'interaction (en)). 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.

Les origines 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 :

$A\rightarrow B=\,!A\multimap B$

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

Le langage de la logique linéaire propositionnelle classique (CLL) est donné par la grammaire en notation BNF suivante :

A	::=	p ∣ p⊥
	∣	A ⊗ A ∣ A ⊕ A
	∣	A & A ∣ A ⅋ A
	∣	1 ∣ 0 ∣ ⊤ ∣ ⊥
	∣	!A ∣ ?A

Dans ce langage, il y a plusieurs connecteurs :

• la négation linéaire notée $A^{\bot }$ ;
• une conjonction et une disjonction multiplicative : le tenseur ($\otimes$) et le par (⅋) ;
• une conjonction et une disjonction additive : le avec (&) et le plus ($\oplus$) ;
• la flèche linéaire est définie au moyen de la négation linéaire et de la disjonction multiplicative : A ⊸ B = A^⊥ ⅋ B.

On ajoute des modalités

• ! qui signifie autant de fois que l'on veut, que l'on prononce aussi bien sûr ;
• ? qui est en quelque sorte le dual de ! et que l'on prononce pourquoi pas.

Système de preuve

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 démonstration 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.

Les séquents

Grâce à la négation qui est partie intégrante du système on peut (et on ne s'en prive pas) représenter les séquents en mettant toutes les propositions à droite du signe $\vdash$. Ainsi, par exemple au lieu d'une règle avec un antécédent et un succédent comme $A\vdash B$, on écrira une règle avec seulement un succédent comme $\vdash A^{\bot },B$. Parmi les règles de déduction dyadiques (celles qui ont deux prémisses) on distingue deux types de règles:

• les règles multiplicatives, dans de telles règles les deux séquents prémisses ont des succèdents différents que l'on accole dans la conclusion de la règle. Par exemple

${\frac {\vdash \Gamma ,A\quad \vdash B,\Delta }{\vdash \Gamma ,A\odot B,\Delta }}$

• les règles additives, dans de telles règles les deux séquents prémisses ont le même succédent en dehors des propositions qui nous intéressent, que l'on retrouve dans la conclusion. Par exemple

${\frac {\vdash \Gamma ,A\quad \vdash \Gamma ,B}{\vdash \Gamma ,A\odot B}}$

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 conduit au dédoublement des connecteurs de conjonction et de disjonction.

Groupe identité

⊢ A, A⊥ (axiome)

⊢ Γ, A ⊢ A⊥, Δ ⊢ Γ, Δ (coupure)

Groupe multiplicatif

⊢ Γ, A ⊢ B, Δ ⊢ Γ, A ⊗ B, Δ (⊗)

⊢ Γ, A, B ⊢ Γ, A ⅋ B (⅋)

Groupe additif

⊢ Γ, A ⊢ Γ, B ⊢ Γ, A & B (&)

⊢ Γ, Ai ⊢ Γ, A1 ⊕ A2 (⊕i)

Groupe exponentiel

⊢ Γ, ?A, ?A ⊢ Γ, ?A (contraction)

⊢ Γ, A ⊢ Γ, ?A (déréliction)

⊢ Γ ⊢ Γ, ?A (affaiblis­sement)

⊢ ?Γ, A ⊢ ?Γ, !A (pro­motion)

Quelques formules linéaires remarquables

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

$A\equiv B\quad =\quad (A\multimap B)\&(B\multimap A)$

Lois de De Morgan

(A⊥)⊥ ≡ A

(A ⊗ B)⊥ ≡ A⊥ ⅋ B⊥

(A ⊕ B)⊥ ≡ A⊥ & B⊥

(!A)⊥ ≡ ?A⊥

Distributivité

A ⊗ (B ⊕ C) ≡ (A ⊗ B) ⊕ (A ⊗ C)

Isomorphisme exponentiel

!(A & B) ≡ !A ⊗ !B

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é

(A ⊗ (B ⅋ C)) ⊸ ((A ⊗ B) ⅋ C)

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^{[Selon qui ?][réf. nécessaire]}. 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\multimap 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\multimap 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 représenter des systèmes dynamiques qui comportent peu de vérités éternelles mais beaucoup de vérités fugaces, comme les états du système.

Certains des connecteurs linéaires $\otimes$, ⅋ et $\multimap$ ont été définis par Girard en rejetant cette propriété^{[Laquelle ?]}.

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

• le cercle barré d'une croix (parfois appelé produit tensoriel) : $A\otimes B$ signifie la conjonction des ressources $A$ et $B$ ;
• le par : ⅋ signifie que les ressources $A$ et $B$ sont utilisables mais pas de façon conjointe ;
• l'implication linéaire : $A\multimap 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$.

Bibliographie

• 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