David Madore's WebLog: Et maintenant, un peu de logique linéaire

Index of all entries / Index de toutes les entréesXML (RSS 1.0) • Recent comments / Commentaires récents

↓Entry #2578 [older| permalink|newer] / ↓Entrée #2578 [précédente| permalien|suivante] ↓

(dimanche)

Et maintenant, un peu de logique linéaire

Je traîne depuis longtemps l'idée de vulgariser quelques notions de logique linéaire. Du point de vue de la vulgarisation, la logique linéaire a ceci de sympathique que c'est quelque chose mathématiquement à tellement « bas niveau » que je n'ai besoin de présupposer aucune sorte de connaissance mathématique préalable pour en parler : en principe, on peut la considérer comme un pur petit jeu syntactique dont les règles ne sont pas très compliquées — même si, présenté sous cette forme, il risque de ne pas apparaître comme très intéressant, et même s'il est bon d'avoir du recul pour avoir une idée de quelles règles appliquer à quel moment, la compréhension des règles elles-mêmes ne nécessite pas de savoir particulier. Du point de vue personnel, la logique linéaire est quelque chose qui me frustre beaucoup parce que, d'un côté, je la trouve extrêmement élégante et joliment symétrique, de l'autre, à chaque fois qu'elle semble avoir une application ou une interprétation quelque part, on se rend compte qu'il y a une note en bas de page qui fait que ce n'est pas vraiment la logique linéaire (il y a par exemple un axiome en plus, ou un connecteur en moins, ou seulement un fragment du système, ou quelque autre variation), et l'élégance est rompue ; et aussi, pour cette raison, l'intuition qu'on peut se former est brouillée.

De quoi s'agit-il ? D'un système formel inventé par le logicien français Jean-Yves Girard en 1987. J'avoue ne guère avoir d'idée de ce qu'il voulait faire avec, parce que les textes de Girard sont… un peu inhabituels… bourrés de mots qu'il ne définit pas, de références cryptiques, et de blagues dont on se demande si ce sont des blagues (comme l'intervention insistante du broccoli dans beaucoup de ses papiers). Mais depuis, elle a trouvé diverses applications et connexions : en logique, en informatique théorique ou plus appliquée, en algèbre et théorie des catégories, en théorie des jeux et même en physique quantique (sauf qu'à chaque fois, comme je le dis ci-dessus, il y a quelque chose en plus ou en moins) ; mais je ne compte pas essayer de décrire ces applications et connexions, qui sont pourtant sans doute ce qu'il y a de plus intéressant dans l'histoire, parce que je n'ai pas l'espace ni le temps pour ça.

Bref. Avant d'expliquer quelles sont les règles du jeu, il faut que j'essaye de donner une idée de ce dont il s'agit (en agitant les mains). On parle de logique linéaire, et il s'agit effectivement d'une généralisation de la logique classique, mais ce terme risque de donner une impression tout à fait fausse, et on devrait peut-être plutôt s'imaginer que ça s'appelle formalisme d'échanges ou synallagologie universelle ou quelque chose de ce genre (le seul problème du mot synallagologie est que personne ne sait ce qu'il veut dire puisque je viens de l'inventer… mais à part ça, il est parfait). La différence essentielle est la suivante : en logique usuelle, si on fait un raisonnement tendant à démontrer une conclusion X à partir d'hypothèses A, B et C, disons, on peut utiliser librement A, B et C dans le cours du raisonnement, chacune aussi souvent qu'on veut (on peut aussi, d'ailleurs, ne pas du tout utiliser une hypothèse) ; la logique linéaire, pour sa part, exige que chacune des « hypothèses » (qu'il vaut mieux, du coup, ne pas considérer comme des hypothèses) soit utilisée une et une seule fois : on ne peut ni les multiplier ni les faire disparaître (évidemment, il y aura des moyens de marquer des hypothèses spéciales qu'on peut multiplier et/ou faire disparaître, mais ce n'est pas le cas par défaut) ; dans ces conditions, il vaut mieux, donc, considérer qu'on n'a pas du tout à faire à une logique, à des raisonnements et à des hypothèses et conclusions, mais à des échanges (gestion de ressources abstraites, transactions économiques, réactions chimiques, que sais-je encore) qui ont des entrées (réactifs) et des sorties (produits), ou quelque chose comme ça. Par exemple, la logique linéaire pourrait concevablement servir à formaliser des contrats financiers (j'avais déjà évoqué quelque chose de ce genre), mais il ne faut pas s'imaginer que la logique linéaire elle-même dira grand-chose d'intéressant : de même que la logique classique ne fournit que le langage le plus basique au-dessus duquel on peut bâtir des raisonnements (il faut ajouter des axiomes intéressants pour obtenir quelque chose d'intéressant), la logique linéaire n'est qu'un cadre, en lui-même extrêmement primitif pour possiblement décrire des échanges.

Je digresse un peu (en agitant toujours beaucoup les mains) pour ceux qui savent ce que ces mots veulent dire : la logique linéaire peut surtout servir en informatique, par exemple pour sous-tendre un système de typage d'un langage informatique dans lequel la mémoire, ou une quelconque autre ressource, n'est pas allouée ou libérée automatiquement — le fait que le typage soit linéaire signifie précisément que les données ou ressources ne seront ni dupliquées ni perdues sans un appel explicite à des fonctions d'allocation ou de libération de la mémoire/ressource. (L'utilisation de la logique pour sous-tendre un typage fait appel à la correspondance de Curry-Howard en vertu de laquelle les types d'un langage de programmation et programmes instanciant ces types se comportent de la même manière que, respectivement, les propositions d'un système logique et preuves de ces propositions : les hypothèses et conclusions d'un raisonnement correspondent, côté informatique, aux entrées et sorties d'un programme, et la logique linéaire assure précisément que les entrées ne sont ni reproduites ni jetées.) Mais la logique linéaire peut aussi servir à modéliser le parallélisme en informatique, ou des échanges client-serveur, ou des jeux à deux joueurs, ou encore toutes sortes de choses.

Insistons sur le point suivant : il n'est pas clair (en tout cas pas clair pour moi, sans doute que Girard me dirait de retourner faire pousser des broccolis) que les formules de la logique linéaire aient un « sens » inné (alors que c'est nettement plus clair pour la logique classique) ; selon le genre de choses auxquelles on va appliquer cette logique (formalisation d'échanges, typage informatique, théorie des jeux, algèbre, mécanique quantique), il apparaîtra une sémantique pour la logique linéaire ou peut-être un fragment de la logique linéaire (et peut-être avec des axiomes en plus), mais il n'est pas possible de dire exactement ce que AB signifie de façon générale, juste quelles règles il doit vérifier. Je vais quand même essayer d'en donner une petite idée, mais cette idée sera forcément très grossière, très approximative, très informelle, et ne sert à la limite qu'à permettre de mémoriser un peu quel quantificateur fait quoi.

Tout ceci étant dit de façon extrêmement vague, à quoi ressemblent les formules de la logique linéaire et quels sont ses symboles ? Il y en a tout un paquet : ‘&’, ‘⊕’, ‘⊗’, ‘⅋’ (les quatre connecteurs binaires), ‘⊸’ (l'implication linéaire), ‘⊤’, ‘0’, ‘1’, ‘⊥’ (les quatre neutres), ‘•’ (la dualité, notée par un symbole ‘⊥’ en exposant), ‘!’ et ‘?’ (les exponentielles) ; symboles auxquels on peut encore ajouter ‘⊢’ même s'il n'est pas tant un symbole de la logique qu'un symbole qui sert à en définir les règles. Je vais discuter informellement ces différentes machins avant de définir précisément les règles de la logique : comme je viens de le dire, je vais tenter de proposer un sens intuitif (extrêmement grossier) aux symboles, mais il ne faut pas le prendre trop au sérieux, plutôt l'utiliser comme un vague guide ou moyen mnémotechnique pour retenir ce qui est quoi — ces explications informelles ne sont pas du tout nécessaires, on pourrait les sauter complètement, et on peut les ignorer si on trouve qu'elles rendent les choses plutôt plus confuses. (Néanmoins, comme je vais y mélanger des explications d'ordre syntaxique, par exemple pour dire que ‘&’ est un connecteur prenant deux arguments, qu'on note A&B le résultat de ce connecteur appliqué à ces deux arguments, ou encore que la convention de parenthésage est que A&BC se lit comme A&(BC), il vaut mieux ne pas sauter directement jusqu'aux règles.)

Il faut que j'introduise d'abord les quatre connecteurs, à savoir & (prononcer avec), ⊕ (prononcer plus), ⊗ (prononcer fois) et ⅋ (prononcer par ; si ce dernier symbole ne s'affiche pas correctement, sachez que c'est un ‘&’ retourné de 180° : certains, faute de disposer de ce symbole, écrivent ‘℘’ à la place, symbole qui a d'ailleurs lui-même une histoire assez compliquée). Du point de vue de la syntaxe, il s'agit de connecteurs binaires, c'est-à-dire que si A et B sont des formules (=expressions) de la logique linéaire, alors A&B, AB, AB et AB sont quatre nouvelles formules. On dira que :

  • & est conjonctif, additif, négatif ;
  • ⊕ est disjonctif, additif, positif ;
  • ⊗ est conjonctif, multiplicatif, positif ;
  • ⅋ est disjonctif, multiplicatif, négatif.

Ou si on préfère ranger ça en tableau :

ConjonctionDisjonction
Additif& (avec)⊕ (plus)
Multiplicatif⊗ (fois)⅋ (par)
ou bien
PositifNégatif
Additif⊕ (plus)& (avec)
Multiplicatif⊗ (fois)⅋ (par)

(Je ne prétends pas avoir expliqué ce que ces termes signifient, ni les connecteurs eux-mêmes. Il s'agit de pure terminologie.) Voici une description intuitive et sommaire de ce que ces connecteurs (je répète encore une fois qu'il ne s'agit pas d'une définition ni même d'une explication, mais juste de donner une idée préalable à laquelle se référer) :

  • Le connecteur & (avec) marque (intuitivement) le choix entre deux ressources : c'est-à-dire qu'avoir un A&B signifie (intuitivement) qu'on a un A ou un B, mais pas les deux à la fois, et qu'on dispose du choix entre les deux. (Je sais que cette description semble contradictoire à la fois avec la lecture du connecteur comme avec et avec sa classification comme conjonctif, mais ce n'est pas une erreur de ma part.) Par exemple, si un restaurateur vous propose fromage & dessert-du-jour, cela signifie qu'il vous propose de choisir entre le fromage et le dessert (mais vous ne pouvez pas avoir les deux, ni deux fois l'un, ni d'ailleurs ne rien avoir du tout).
  • Le connecteur ⊕ (plus) marque (intuitivement) l'absence de choix (ou le choix par l'adversaire, ou par le monde extérieur) entre deux ressources : c'est-à-dire qu'avoir un AB signifie (intuitivement) qu'on a un A ou un B, mais pas les deux à la fois, et qu'on ne dispose pas du choix entre les deux. Par exemple, si le dessert-du-jour est profiterole ⊕ tarte-tatin, cela signifie que ce n'est pas vous qui choisissez entre les deux.
  • Le connecteur ⊗ (fois) marque (intuitivement) la présence simultanée de deux ressources : c'est-à-dire qu'avoir un AB signifie (intuitivement) qu'on a un A et un B en même temps (qu'on le veuille ou non). Par exemple, si le plat-du-jour est saumon ⊗ oseille, vous aurez les deux (et vous ne pouvez pas avoir moins).
  • Le connecteur ⅋ (par)… ah, c'est là le problème : comme je le disais plus haut, c'est frustrant à quel point chaque interprétation de la logique linéaire semble avoir quelque chose en plus ou en moins, et l'interprétation comme des ressources ne donne pas de sens évident à ce quatrième connecteur. Le mieux que je puisse proposer est que AB signifierait très vaguement quelque chose comme : il y a deux mondes parallèles, l'un dans lequel vous auriez un A et l'autre dans lequel vous auriez un B ; même si c'est très loin d'être satisfaisant, c'est peut-être quelque chose qu'on peut garder à l'esprit.

Ces quatre connecteurs sont tous commutatifs et associatifs, c'est-à-dire que A&B est complètement interchangeable avec B&A, et que A&(B&C) l'est avec (A&B)&C (ce qui permet légitimement d'écrire simplement A&B&C pour l'un quelconque des deux), et de même pour les trois autres connecteurs. (Il y a des définitions de logiques linéaires non-commutatives, dans lesquelles les connecteurs multiplicatifs ⊗ et ⅋ ne sont plus commutatifs, mais je ne vais pas en parler ; et même là, les additifs restent commutatifs.)

À côté de ces quatre connecteurs, il faut mentionner l'opération notée par le symbole ‘⊸’ (que certains prononcent sucette, lollipop en anglais, à cause de sa forme ; mais d'autres disent simplement implique ou parlent d'implication linéaire). On peut soit considérer que ⊸ est un connecteur supplémentaire, soit le définir au moyen de la dualité (dont je vais parler ci-dessous) en décrétant que AB est un raccourci de langage pour (A)⅋B (de la même façon que, si on connaît la logique classique AB peut être un racourci de langage pour (¬A)∨B). Quoi qu'il en soit, le sens intuitif de AB est quelque chose comme une machine qui transforme un A en un B (mais ne peut servir qu'une seule fois), ou encore un contrat par lequel on [= celui qui a AB] s'engage à fournir un A et obtenir un B en échange (ceci peut éventuellement servir à donner une intuition du ⅋, puisque je viens de dire que AB est essentiellement synonyme de (A)⅋B, même si je n'ai pas encore parlé de A). À la différence des quatre connecteurs &, ⊕, ⊗ et ⅋, l'implication ⊸ n'est certainement pas commutative ni associative.

Quand on lit les expressions de logique linéaire, on fait la convention que les connecteurs dits multiplicatifs (c'est-à-dire ⊗ et ⅋) ainsi que l'implication linéaire (⊸) ont la priorité sur les connecteurs dits additifs (& et ⊕) : par exemple, ABC doit se comprendre comme (AB)⊕C ; mais pour le reste, le parenthésage doit être explicitement marqué.

Chacun des quatre connecteurs &, ⊕, ⊗ et ⅋ a un neutre correspondante (appelé aussi l'unité du connecteur, ou la constante associée). Ce sont respectivement : ⊤, 0, 1 et ⊥ (on peut les lire comme vrai, zéro, un et faux respectivement, mais je crois avoir entendu rien utilisé pour l'un d'entre eux, et pas de façon très cohérente). En tableau :

VraiFaux
Additif⊤ (neutre de &)0 (neutre de ⊕)
Multiplicatif1 (neutre de ⊗)⊥ (neutre de ⅋)
ou bien
PositifNégatif
Additif0 (neutre de ⊕)⊤ (neutre de &)
Multiplicatif1 (neutre de ⊗)⊥ (neutre de ⅋)

Quand on dit neutre, pour un connecteur, cela signifie que connecter avec ce neutre ne change rien : autrement dit, dire que ⊤ est le neutre du connecteur & signifie que A&⊤ est complètement interchangeable avec A, et de même pour A⊕0 ou bien A⊗1 ou encore A⅋⊥. On peut essayer d'en déduire un sens intuitif à ces neutres en se basant sur le sens intuitif que j'ai proposé aux connecteurs : ainsi, ⊤ serait quelque chose d'épouvantablement mauvais que personne ne veut avoir à aucun prix (si bien que quand vous avez le choix A&⊤ entre A et ⊤, vous choisirez toujours A puisque ⊤ est pire que tout), tandis que 0 serait, au contraire, quelque chose d'infiniment désirable que vous n'aurez jamais ; quant à 1, c'est « rien du tout » (si bien qu'avoir A⊗1, un A en même temps que 1, c'est juste avoir un A), et ⊥, comme d'habitude, n'est pas très intuitif (mais une interprétation très grossière possible est la mort ou l'inexistence — la terminaison d'un programme, par exemple — puisque A⅋⊥ signifie que dans un monde parallèle vous n'existez pas, ce qui vous fait une belle jambe, tandis que dans celui-ci vous avez un A).

Une autre opération de la logique linéaire est la dualité (appelée aussi négation linéaire) : on la note par un ⊥ en exposant : le dual de A est noté A (parfois prononcé nil-A). En fait, l'implication linéaire ⊸ et la dualité sont interdéfinissables : on peut soit considérer que AB est un raccourci de langage pour (A)⅋B, soit que A est un raccourci de langage pour A⊸⊥ (ce qui justifie plus ou moins l'utilisation du même symbole ‘⊥’ pour les deux, même si la notation est quand même un peu malheureuse). Le sens intuitif de A est quelque chose comme disparition d'un A, ou consommation d'un A.

Peut-être que je peux glisser ici une explication informatique informelle du fait que AB (que j'ai expliqué comme représentant un appareil pour consommer un A et à produire un B) est équivalent à (A)⅋B (que j'ai vaguement décrit comme deux mondes parallèles, l'un dans lequel on a un B et l'autre dans lequel on a un truc-qui-consomme-un-A-et-fait-disparaître-le-monde) : pour que les choses soient moins floues, disons que ce sont des ressources dans un langage de programmation ; or une façon pour un programme d'accepter un A en entrée et de renvoyer un B est de faire la chose suivante : le programme forke, c'est-à-dire, crée un nouveau fil d'exécution, l'un de ces fils attend/demande qu'on lui fournisse un A, et quand c'est le cas, transmet cette ressource à l'autre programme et termine son exécution, tandis que l'autre fil attend le message de son frère, et produit alors un B ; c'est plus ou moins ça que doit décrire l'équivalence entre AB et (A)⅋B (les deux arguments du ⅋ étant les deux fils dont je viens de parler).

La dualité fournit une symétrie de la logique linéaire : en effet,

  • (A) est (interchangeable avec) A.
  • (A&B) est (interchangeable avec) (A)⊕(B) ; et (AB) est (interchangeable avec) (A)&(B).
  • (AB) est (interchangeable avec) (A)⅋(B) ; et (AB) est (interchangeable avec) (A)⊗(B).
  • est (interchangeable avec) 0 ; et 0 est (interchangeable avec) ⊤.
  • 1 est (interchangeable avec) ⊥ ; et ⊥ est (interchangeable avec) 1.

(On comparera avec les lois de De Morgan de la logique classique : en logique classique, la négation échange la conjonction avec la disjonction, et en logique linéaire, la dualité échange les deux connecteurs additifs d'une part, et les deux multiplicatifs d'autre part.)

Quant à (AB), on peut le réécrire comme A⊗(B).

Enfin, la logique linéaire comporte des exponentielles, notées !A (qui peut être lu bien sûr, ou of course en anglais) et ?A (qui peut être lu pourquoi pas, ou why not en anglais), qui servent à permettre à la logique linéaire de traduire la situation normale en logique classique, c'est-à-dire le fait qu'une hypothèse est jetable ou multipliable à volonté. Je n'en parlerai guère plus pour le moment (la logique linéaire sans exponentielles est déjà assez intéressante et complexe), mais signalons que :

  • Le sens de !A ressemble à : (1&A)⊗(1&A)⊗(1&A)⊗⋯ ; c'est-à-dire intuitivement : autant de A que vous voulez (y compris aucun).
  • Le sens de ?A ressemble à : (⊥⊕A)⅋(⊥⊕A)⅋(⊥⊕A)⅋⋯ ; c'est-à-dire très grossièrement : autant de A que vous ne voulez pas (mais dans des univers parallèles (?)).
  • Les deux exponentielles sont duales l'une de l'autre, c'est-à-dire que (!A) est (interchangeable avec) ?(A) ; et (?A) est (interchangeable avec) !(A).

Pour mieux donner une idée du fonctionnement de toutes ces opérations, je tente une liste d'identités linéaires : cette liste n'est pas exhaustive (il n'est pas possible de dresser une liste exhaustive de telles identités), mais devrait donner au moins les plus fréquemment rencontrées, quitte à répéter certaines que j'ai déjà données ; dans ce qui suit, PQ signifie que P et Q sont interchangeables en logique linéaire (et ce, quelles que soient les valeurs des variables A, B, C, etc.) :

  • AB ≡ (A)⅋B ; et AA⊸⊥
  • (A)A
  • (A&B) ≡ (A)⊕(B) ; et (AB) ≡ (A)&(B) ; et ⊤ ≡ 0 ; et 0 ≡ ⊤
  • (AB) ≡ (A)⅋(B) ; et (AB) ≡ (A)⊗(B) ; et 1 ≡ ⊥ ; et ⊥ ≡ 1
  • A&(B&C) ≡ (A&B)&C ; et A&BB&A ; et A&⊤ ≡ A ; et A&AA
  • A⊕(BC) ≡ (AB)⊕C ; et ABBA ; et A⊕0 ≡ A ; et AAA
  • A⊗(BC) ≡ (AB)⊗C ; et ABBA ; et A⊗1 ≡ A ; et A⊗0 ≡ 0
  • A⅋(BC) ≡ (AB)⅋C ; et ABBA ; et A⅋⊥ ≡ A ; et A⅋⊤ ≡ ⊤
  • A⊗(BC) ≡ (AB)⊕(AC)
  • A⅋(B&C) ≡ (AB)&(AC)
  • 1⊸AA ; et A⊸(BC) ≡ (AB)⊸C ; et A⊸(B&C) ≡ (AB)&(AC) ; et (AB)⊸C ≡ (AC)&(BC)
  • (!A) ≡ ?(A) ; et (?A) ≡ !(A)
  • !!A ≡ !A ; et !A ≡ (!A)⊗(!A) ; et !A ≡ 1&(!A) ; et !AA&(!A)
  • ??A ≡ ?A ; et ?A ≡ (?A)⅋(?A) ; et ?A ≡ ⊤⊕(?A) ; et ?AA⊕(?A)
  • !(A&B) ≡ (!A)⊗(!B) ; et !⊤ ≡ 1
  • ?(AB) ≡ (?A)⅋(?B) ; et ?0 ≡ ⊥

(Certains râleurs râleront que mes identités ne sont pas toutes de la même nature, vu que certaines reflètent, en fait, des isomorphismes de structures de preuves alors que certaines sont seulement des implications bidirectionnelles.)

Idéalement, on devrait chercher à se faire une représentation intuitive des opérations de la logique linéaire qui rende évidentes ces identités, mais j'avoue que ça semble vraiment délicat (ou plutôt, ça semble vraiment délicat si elle ne doit pas, par ailleurs, introduire de fausses identités comme laisser penser que AA serait équivalent à ⊥ ou bien que A⊗(B&C) serait équivalent à (AB)&(AC), choses qu'il est peut-être tentant de penser mais qui ne découlent pas des règles de la logique linéaire).

Tout ce que j'ai raconté jusqu'à présent était censé donner une simple idée préliminaire de la logique linéaire, mais sans rien définir correctemnet. J'en viens maintenant aux explications plus précises.

Pour définir les règles précisément, je vais utiliser un symbole supplémentaire, qui ne fait pas partie de la logique elle-même mais sert à la définir : il s'agit du symbole ‘⊢’ (prononcé thèse ou taquet). Il s'utilise avec une suite de formules de la logique linéaire à gauche et à droite, chacune séparée par des virgules (c'est-à-dire que ça ressemble à ceci : U,V,WX,Y,Z), et le tout s'appelle un séquent. Intuitivement, il faut comprendre un séquent U,V,WX,Y,Z comme signifiant à partir de U,V,W, je peux obtenir X,Y,Z (attention, la virgule n'a pas le même sens à gauche et à droite, comme je vais le dire ci-dessous) : on dit que les formules à gauche du symbole ‘⊢’ (U,V,W) sont les antécédents (ou parfois hypothèses) du séquent, et que celles à droite (X,Y,Z) en sont les conséquents (ou parfois conclusions). La logique linéaire se définit par un certain nombre de règles qui définissent les séquents valables (et ces règles ont la forme : si ceci et ceci sont des séquents valables alors cela en est un aussi). Par exemple, A&BAB est un séquent valable (dont le contenu intuitif très grossier est quelque chose comme si j'ai le choix entre A et B, je peux y renoncer). Si on écrit simplement A&BAB dans une phrase en français, on convient que cela signifie A&BAB est un séquent valable. Un autre exemple de séquent valable (je le démontrerai plus bas) est : A⊗(BC)⊢(AB)⅋C (en revanche, sa « réciproque », c'est-à-dire si on échange l'antécédent avec le conséquent, n'est pas valable).

Notons qu'un séquent peut très bien avoir zéro formule à gauche du taquet, ou zéro à droite (ou même les deux, mais il se trouve que ⊢ n'est pas un séquent valable de la logique linéaire). Et de fait, au bout du compte, on s'intéresse surtout aux formules P telles que ⊢P [soit un séquent valable] : ce sont elles qu'on appelle les tautologies ou les théorèmes de la logique linéaire. Par exemple, on a ⊢(A&B)⊸(AB), c'est-à-dire que (A&B)⊸(AB) est une tautologie de la logique linéaire. Mais même si on veut, au final, s'intéresser à des séquents valables de la forme ⊢P, il est utile, comme étapes intermédiaires, de passer par des sortes plus générales de séquents.

En fait, dans un séquent comme U,V,WX,Y,Z, les formules séparées par des virgules à gauche du symbole ‘⊢’ (i.e., les antécédents) sont implicitement connectées par ⊗, tandis que celles à droite du symbole ‘⊢’ (i.e., les conséquents) sont implicitement connectées par ⅋ ; c'est-à-dire qu'écrire U,V,WX,Y,Z va être équivalent (même si on n'a pas besoin de le savoir) à écrire UVWXYZ. Et fort logiquement, l'absence de formule à gauche est implicitement un 1 (écrire ⊢P revient à écrire 1⊢P) et à droite c'est un ⊥. Ce ne sont pas là des choses qu'on doit savoir (ce sont des effets des règles), mais ça explique un petit peu comment les choses fonctionnent.

Voici enfin les règles elles-mêmes : dans tout ce qui suit, les lettres latines majuscules (A,B,C…) sont à remplacer par des formules quelconques de la logique linéaire, et les lettres grecques majuscules (Γ,Δ,Σ,Π) par des suites (finies) quelconques de formules séparées par des virgules (ces formules-là ne seront pas modifiées et portent le nom collectif de contexte d'application de la règle) :

  • Coupure : si ΓΔ,A [est un séquent valable] et A,ΣΠ [en est un], alors Γ,ΣΔ,Π [en est encore un].
  • Identité : on a AA [c'est un séquent valable].
  • Échange : si ΓΔ alors Γ′⊢Δ′ où Γ′ et Δ′ s'obtiennent en permutant de façon arbitraire les formules de Γ et Δ respectivement. (Remarque : on peut passer complètement sous silence l'utilisation de la règle d'échange en considérant que les listes à gauche et à droite du symbole taquet, dans un séquent, sont des multiensembles, c'est-à-dire que leur ordre n'est tout simplement pas défini.)
  • Introduction du & : si ΓA,Δ et ΓB,Δ, alors ΓA&B,Δ ; élimination du & : si Γ,AΔ ou bien Γ,BΔ alors Γ,A&BΔ.
  • Introduction du ⊕ : si ΓA,Δ ou bien ΓB,Δ alors ΓAB,Δ ; élimination du ⊕ : si Γ,AΔ et Γ,BΔ, alors Γ,ABΔ.
  • Introduction du ⊗ : si ΓA,Δ et ΣB,Π, alors Γ,ΣAB,Δ,Π ; élimination du ⊗ : si Γ,A,BΔ alors Γ,ABΔ.
  • Introduction du ⅋ : si ΓA,B,Δ alors ΓAB,Δ ; élimination du ⅋ : si Γ,AΔ et Σ,BΠ, alors Γ,Σ,ABΔ,Π.
  • Introduction du ⊤ : [quels que soient Γ et Δ,] on a Γ⊢⊤,Δ. (Il n'y a pas de règle d'élimination du ⊤.)
  • Élimination du 0 : [quels que soient Γ et Δ,] on a Γ,0⊢Δ. (Il n'y a pas de règle d'introduction du 0.)
  • Introduction du 1 : on a ⊢1 ; élimination du 1 : si ΓΔ alors Γ,1⊢Δ.
  • Introduction du ⊥ : si ΓΔ alors Γ⊢⊥,Δ ; élimination du ⊥ : on a ⊥⊢.
  • Introduction du ⊸ (=abstraction) : si Γ,AB,Δ alors ΓAB,Δ ; élimination du ⊸ (=application) : si ΓA,Δ et Σ,BΠ, alors Γ,Σ,ABΔ,Π.
  • Introduction de dualité : si Γ,AΔ alors ΓA,Δ ; élimination de dualité : si ΓA,Δ alors Γ,AΔ.
  • Promotion du ! : si !ΓA,?Δ alors !Γ⊢!A,?Δ, où !Γ signifie que chaque formule de la liste est précédée de !, et ?Δ désigne l'hypothèse analogue sur Δ ; élimination du ! : si Γ,AΔ alors Γ,!AΔ ; affaiblissement du ! : si ΓΔ alors Γ,!AΔ ; contraction du ! : si Γ,!A,!AΔ alors Γ,!AΔ.
  • Promotion du ? : si !Γ,A⊢?Δ alors !Γ,?A⊢?Δ, où !Γ signifie que chaque formule de la liste est précédée de !, et ?Δ désigne l'hypothèse analogue sur Δ ; introduction du ? : si ΓA,Δ alors Γ⊢?A,Δ ; affaiblissement du ? : si ΓΔ alors Γ⊢?A,Δ ; contraction du ? : si Γ⊢?A,?A,Δ alors Γ⊢?A,Δ.

À titre d'exemple, je vais démontrer le séquent A&BAC (je veux dire, démontrer qu'il est valable). Pour commencer, on a AA par la règle d'identité. On peut ensuite appliquer la règle d'élimination du & (avec pour contexte Γ vide et Δ=A), pour obtenir A&BA. Puis en appliquant la règle d'introduction du ⊕, on en déduit A&BAC, comme annoncé. On pourrait appliquer encore une étape d'introduction du ⊸ pour en réécrire ce séquent en : ⊢ (A&B)⊸(AC), c'est-à-dire que (A&B)⊸(AC) est une tautologie de la logique linéaire. (Par promotion du ! avec un contexte vide, on peut aussi affirmer que !((A&B)⊸(AC)) est une tautologie : toute tautologie P peut toujours être promue en !P, mais on préfère écrire simplement P.)

Comme deuxième exemple, voici un une démonstration du séquent A⊗(BC)⊢(AB)⅋C : pour commencer, on a AA et BB (par la règle d'identité, deux fois), et en appliquant la règle d'introduction du ⊗ (avec Γ=A, Δ vide, Σ=B et Π vide) on en déduit A,BAB ; mais par ailleurs, on a CC (par la règle identité), et en appliquant la règle d'élimination du ⅋ à ces deux derniers séquents on en déduit A,BCAB,C ; la règle d'élimination du ⊗ donne alors A⊗(BC)⊢AB,C, et la règle d'introduction du ⅋ donne enfin A⊗(BC)⊢(AB)⅋C, comme annoncé. Encore une fois, on pourrait appliquer encore une étape d'introduction du ⊸ pour en réécrire ce séquent en : ⊢ (A⊗(BC))⊸((AB)⅋C), c'est-à-dire que (A⊗(BC))⊸((AB)⅋C) est une tautologie de la logique linéaire.

Il faudrait bien sûr motiver l'origine de ces règles. Au niveau purement descriptif et/ou intuitif où je me place, ce n'est pas vraiment possible : je peux évidemment faire remarquer leur grande symétrie, mais la motivation essentielle vient surtout de l'observation des règles analogues pour la logique classique (dont je vais dire un mot plus bas) en retirant les règles dites « structurales » d'affaiblissement et de contraction (qui permettent essentiellement d'abandonner ou de dupliquer les hypothèses d'un raisonnement) et en regardant ce qui surnage.

Quelques remarques néanmoins. En principe, la règle de coupure n'est pas nécessaire : toute démonstration qui l'utilise peut se réécrire sans elle (cela revient, essentiellement, à refaire la démonstration utilisée dans la coupure à chaque fois qu'on veut couper). En pratique, elle est bigrement utile : c'est bien elle qui vous dit que si vous savez démontrer machin à partir de truc, et bidule à partir de machin, alors vous savez démontrer bidule à partir de truc (et donc de garder des lemmes sous le coude !). Mais l'intérêt de savoir qu'on peut éliminer les coupures, c'est que comme toutes les autres règles ne peuvent qu'ajouter des nouveaux symboles aux formules, ça simplifie énormément la démonstration du fait que certains séquents ne sont pas valables : par exemple, on se convainc facilement que 1⅋1 n'est pas une tautologie linéaire, parce que la seule façon d'arriver à ⊢1⅋1 serait par ⊢1,1 et la règle d'introduction du 1 donne juste ⊢1 et pas autre chose. ⁂ Par ailleurs, si on veut, on peut ne manipuler que des séquents sans rien à gauche (i.e., sans antécédents, avec seulement des conséquents), quitte à réécrire la règle de coupure sous la forme si ⊢Δ,A et ⊢A,Π, alors ⊢Δ,Π, et la règle d'identité sous la forme A,A ; on se passe alors des règles de dualité et de toutes les règles d'élimination.

On peut s'entraîner à appliquer ces règles en reprenant la liste des identités PQ que j'ai données plus haut et, pour chacune d'elles, en montrant PQ et QP (ce qui permet bien, via la règle de coupure, à remplacer des P par des Q ou vice versa dans un séquent). Par exemple, voici comment on démontre que !⊤⊢1 : on a ⊢1 par introduction du 1 et on en déduit !⊤⊢1 par affaiblissement du ! ; et voici comment on démontre que (réciproquement) 1⊢!⊤ : on a ⊢⊤ par introduction du ⊤, on en déduit ⊢!⊤ par promotion du !, et donc 1⊢!⊤ par élimination du 1.

La logique linéaire est difficile : même si on se limite uniquement aux formules construites avec les connecteurs multiplicatifs (⊗ et ⅋) à partir des neutres multiplicatifs (1 et ⊥), le problème de décider ce qui est une tautologie linéaire (par exemple : (⊥⊗⊥)⅋1⅋1) est algorithmiquement très difficile en général (il a été montré que rien que ce bout-là est NP-complet ; cela passe à PSPACE-complet pour la logique linéaire sans les exponentielles, et c'et tout simplement indécidable si on prend la logique linéaire complète).

La logique linéaire généralise la logique classique. Pour cela, on ajoute les règles (« structurales ») d'affaiblissement et de contraction, la première affirmant que si ΓΔ alors ΓA,Δ (affaiblissement droit, c'est-à-dire affaiblissement des conséquents) et Γ,AΔ (affaiblissement gauche, c'est-à-dire renforcement des antécédents), et la seconde que si ΓA,A,Δ alors ΓA,Δ (contraction droite) et si Γ,A,AΔ alors Γ,AΔ (contraction gauche) ; avec ces règles supplémentaires, les exponentielles deviennent inutiles, et les connecteurs & et ⊗ fusionnent en un seul qu'on peut noter ‘∧’ tandis que ⊕ et ⅋ fusionnent en un seul qu'on peut noter ‘∨’, et on obtient la logique classique. (Si on introduit l'affaiblissement structural mais pas la contraction, on obtient quelque chose qui s'appelle la logique affine, intermédiaire entre la logique classique et la logique linéaire.)

Il y a toutes sortes d'autres choses que la logique linéaire permet de retrouver : notamment, la logique intuitionniste et la structure algébrique de semi-anneau (« anneau sans soustraction »). Je pourrais aussi évoquer la logique MIX, qui ajoute à la logique linéaire la règle « de mélange », laquelle affirme que si ΓΔ et ΣΠ alors Γ,ΣΔ,Π et aussi que le séquent trivial ⊢ est valable (ce dernier permet de voir ⊥ comme tautologie, et la règle de mélange permet par exemple de voir 1⅋1 comme tautologie de la logique MIX puique ⊢1 et ⊢1 donnent ⊢1,1 par mélange donc ⊢1⅋1 par introduction du ⅋).

Je n'ai pas vraiment de conclusion à proposer à cette entrée (disons que je m'arrête là parce que je ne sais pas quoi dire sans risquer que ça devienne interminablement long), mais je reviens à ce que je disais plus haut : il n'est pas évident de se faire une intuition de ce que signifient les formules ou les opérations de la logique linéaire, parce qu'on a l'impression qu'à chaque fois qu'elle sert (à chaque fois qu'on en définit une sémantique), il y a des règles en plus ou des bouts en moins. Par exemple, Andreas Blass a défini une sémantique de la logique linéaire en termes de jeux à deux joueurs (en partant principalement de l'idée que A&B est un choix que j'ai entre A et B tandis que AB est un choix qu'a mon adversaire ; et A représente l'échange des deux joueurs), mais cette sémantique apporte des règles supplémentaires à la logique linéaire (elle n'est pas complète), donc elle ne peut pas complètement fonder l'intuition de cette dernière. Il y a quelque chose de frustrant, et que je ne comprends pas bien, au fait que la logique linéaire, qui est pourtant d'apparence si « naturelle », ne semble jamais se manifester telle quelle, il y a toujours une variation ou une autre.

↑Entry #2578 [older| permalink|newer] / ↑Entrée #2578 [précédente| permalien|suivante] ↑

Recent entries / Entrées récentesIndex of all entries / Index de toutes les entrées