Logique linéaire

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

La logique classique telle que nous la connaissons n'étudie pas les aspects les plus élémentaires du raisonnement. Sa structure peut être décomposée en 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 structurelle 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 logique linéaire a inventée par le logicien Jean-Yves Girard en 1986 et est un produit de la théorie de la démonstration moderne.

La vision programmatoire et la vision géométrique[modifier | modifier le code]

Plutôt qu'un système formalisant certains aspects du raisonnement, la logique linéaire doit 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). 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[modifier | modifier le code]

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[modifier | modifier le code]

Les séquents[modifier | modifier le code]

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 n'é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}

Les connecteurs[modifier | modifier le code]

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

  • la négation linéaire notée A^\bot;;
  • 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 ) ;
  • la flèche linéaire est définie au moyen de la négation linéaire et de la disjonction multiplicative: A\multimap B=A^\perp\wp B

On ajoute des modalités

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

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.

Calcul des séquents linéaire[modifier | modifier le code]

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é[modifier | modifier le code]


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

Groupe multiplicatif[modifier | modifier le code]


\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[modifier | modifier le code]


\frac{\vdash \Gamma, A\quad\vdash \Gamma, B}{\vdash \Gamma, A\ \&\ B}(\&)
\qquad\qquad\qquad
\frac{\vdash \Gamma, A_i}{\vdash \Gamma, A_1 \oplus A_2}(\oplus_i)

Groupe exponentiel[modifier | modifier le code]


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



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

Quelques formules linéaires remarquables[modifier | modifier le code]

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 :

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

Lois de De Morgan 
\begin{align}(A^\perp)^\perp&\equiv A \\ (A\otimes B)^\perp&\equiv A^\perp\,\wp\,B^\perp \\ (A\oplus B)^\perp&\equiv A^\perp\,\&\,B^\perp \\ (!A)^\perp&\equiv\,?A^\perp\end{align}
Distributivité 
A\otimes(B\oplus C)\equiv(A\otimes B)\oplus(A\otimes C)
Isomorphisme exponentiel 
\,!(A \& B)\equiv \,!A \otimes \,!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\otimes(B\,\wp\,C))\multimap((A\otimes B)\,\wp\,C)

Interprétation des formules[modifier | modifier le code]

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 \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 eternelles mais beaucoup de vérités fugaces. Comme par exemple les états du système.

Certains des connecteurs linéaires  \otimes , \wp et \multimap ont été définis 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 \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  .

Notes et références[modifier | modifier le code]

  1. Puisqu'on n'a pas la règle de contraction, on doit explicitement maîtriser la duplication des propositions.

Bibliographie[modifier | modifier le code]

  • 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