Cours 9: Logique linéaire

Rappel: Le bang $!: Stab ⟶ Coh$ est l’adjoint à gauche du foncteur d’oubli $𝒰: Coh ⟶ Stab$:

\[Coh(!A, B) ≃ Stab(A, B)\]

Et

  • $Coh$ est SMCC avec produits et coproduits
  • $Stab$ est CCC

⟶ magie: tout ça s’organise autour d’un calcul logique: la logique linéaire

Dual/Orthogonal

Dans les espaces cohérents, il y a un dual/orthgonal/négation linéaire :

\[\vert A^⊥ \vert ≝ \vert A \vert\]

où

  • $\sim_{A^⊥} ≝ \text{ négation de la cohérence } \sim_A \text{ de } A$ (large, dans ce cas)

Propriétés du dual

On voit clairement que:

\[(A \, \& \, B)^⊥ = A^⊥ \oplus B^⊥\]

De plus:

\[(a, b) \frown_{A \multimap B} (a', b') \text{ ssi } \underbrace{¬(a \sim_A a')}_{≝ \, a \, \frown_{A^⊥} a'} \text{ ou } b \frown_B b'\]

Ce qui a poussé Girard à introduire:

Espace $A$ “parr” $B$ : $A \,⅋\, B$

\[\vert A \,⅋\, B \vert ≝ \vert A \vert × \vert B \vert\]

avec

\[(a, b) \frown_{A \,⅋\, B} (a', b') \text{ ssi } a \, \frown_{A} a' \text{ ou } b \frown_B b'\]

Donc

\[A \multimap B = A^⊥ \,⅋\, B\]

Propriétés

\[A \,⅋\, B = (A^⊥ \otimes B^⊥)^⊥\]

Rappel:

\[\sim_{A^⊥ \otimes B^⊥} \;=\; \sim_{A^⊥} \text{ et } \sim_{B^⊥} \;\overset{¬}{⟶}\; \frown_{A} \text{ ou } \frown_{B}\]

En outre:

\[⊤ = 0\\ 1 = ⊥\\ (A \& B)^⊥ = A^⊥ \oplus B^⊥\\ (A \oplus B)^⊥ = A^⊥ \& B^⊥\\ (A \,⅋\, B)^⊥ = A^⊥ \otimes B^⊥\\ (A \otimes B)^⊥ = A^⊥ \,⅋\, B^⊥\]

L’élément neutre

  • de $\otimes$: $1$
  • de $\,⅋\,$: $⊥$ (le même que le neutre pour le dual, mais c’est le cas particulier des espaces cohérents)

NB: Peu choquer: c’est un bizarre qu’on ait $1 = ⊥$ (et $⊤ = 0$), car cela ressemble à “vrai = faux” ⟶ mais il ne s’agit pas des mêmes “valeurs de vérité” (sémantique non dégénérée)

Vision de la logique venant de la théorie des modèles: la sémantique de la logique est l’ensemble de ses valeurs de vérité.

Mais: ici, on ne définit pas les valeurs de vérité de la logique linéaire ⟶ on définit la sémantique des preuves:

\[A ⊢ B \overset{⟦\_⟧}{⟼} 𝒞(A, B)\]

Et on veut qu’elle soit non dégénérée, i.e. deux preuves très différentes soient distinguées.

La sémantique des preuves est strictement plus forte que la sémantique des valeurs de vérité ⟶

  • correction (qu’on a dans les espaces cohérents): preuves ⟹ morphismes de la catégorie

  • complétude: morphismes de la catégories ⟹ preuve

    • on ne peut pas avoir un morphisme de correspondant pas à une preuve pour faux, dans ce cas

VS: sémantique de vérité

Espaces de phases (sémantique de vérité de la logique linéaire) $\sim$ Modèles de Kripke (sémantique de vérité de la logique intuitioniste) ⟶ bien-sûr, vrai et faux y sont distingués

NB 2: découverte venant de la logique linéaire: il n’y a pas que des preuves, mais il y a aussi des “pseudo-preuves” (qui sont des cliques) qui interagissent bien avec les preuves, mais qui ne sont pas pour autant des vraies preuves.

Pseudo-preuves ⟶ intéressantes quand-même, on peut y étudier l’élimination des coupures, etc…

Logique linéaire

Idée: On va pousser les négations sous les atomes.

\[A, B ≝ X \mid X^⊥\\ \mid A \otimes B \mid 1 \mid A \,⅋\, B \mid ⊥ \qquad \text{(multiplicatifs)}\\ \mid A \& B \mid ⊤ \mid A \oplus B \mid 0 \qquad \text{(additif)}\\ \mid \, !A \mid ?A \qquad \text{(modalités/exponentiels)}\]

et

\[A \multimap B ≝ A^⊥ \,⅋\, B\]

NB: pourquoi “modalités”? Vient de la logique modale, où on a des opérateurs unaires de modalité (“est possible”, “est nécessaire”, etc…)

où

Pourquoi pas $A$: $?A$

\[?A ≝ (!A^⊥)^⊥\]
  • \[\vert ? A \vert ≝ Cl_{fin}(A^⊥)\]
  • \[d \frown_{?A} d' ⟺ ∃a∈d, a'∈d'; a \frown_A a'\]

NB: c’est bien le dual de $!A$:

\[d \frown_{!A} d' ⟺ ∀a∈d, a'∈d'; a \sim_A a'\]

Exponentiels, Distributivité et Absorbance

\[!(A \& B) ≃ !A \otimes !B \\ ?(A \oplus B) ≃ ?A \,⅋\, ?B\]

NB: ça rappelle

\[2^{A+B} = 2^A \cdot 2^B\]

De plus

\[A \otimes (B \oplus C) ≃ (A \otimes B) \oplus (A \otimes C) \\ A \,⅋\, (B \& C) ≃ (A \,⅋\, B) \& (A \,⅋\, C)\]

$0$ et $⊤$ absorbants:

\[A \otimes 0 ≃ 0\\ A \,⅋\, ⊤ ≃ ⊤\]

Attention: on ne sait pas, a priori, ce que vaut $A \otimes ⊥$

Calcul des séquents de la logique linéaire classique

On va avoir un calcul des séquents monolatère:

\[⊢ A_1, ⋯, A_n\]

⟶ on aura une seule règle pour chaque connecteur.

Identité

\[\cfrac{}{⊢ A^⊥, A}\;ax\] \[\cfrac{⊢ Γ, A \quad ⊢ Δ, A^⊥}{⊢ Γ, Δ}\;cut\]

Règles multiplicatives

\[\cfrac{⊢ Γ, A \quad ⊢ Δ, B}{⊢ Γ, Δ, A \otimes B}\;\otimes\] \[\cfrac{}{⊢ 1}\;1\] \[\cfrac{⊢ Γ, A, B}{⊢ Γ, A \,⅋\, B}\;\,⅋\,\] \[\cfrac{⊢ Γ}{⊢ Γ, ⊥}\;⊥\]

Règles additives

\[\cfrac{⊢ Γ, A \quad ⊢ Γ, B}{⊢ Γ, Δ, A \& B}\;\&\] \[\cfrac{}{⊢ Γ, ⊤}\;⊤\] \[\cfrac{⊢ Γ, A_i}{⊢ Γ, A_1 \oplus A_2}\;\oplus, i ∈ \lbrace 1, 2 \rbrace\]

(pas de règle pour $0$)

NB: en déduction naturelle, que l’élimination du $0$, pas d’introduction

Règles exponentielles

\[\cfrac{⊢ ?Γ, A}{⊢ ?Γ, !A}\;\text{promotion}\] \[\cfrac{⊢ Γ, A}{⊢ Γ, ?A}\;\text{déréliction}\]

NB: pourquoi “déréliction”? Parce qu’on oublie que $A$ est linéaire.

Règles de structure

On peut ajouter des règles structurelles et d’échange, mais il n’y a pas de règle d’affaiblissement, car on n’a pas:

\[A \multimap A \otimes A\\ A \multimap 1\]

MAIS il y a une manière canonique de faire

\[d_A: \; !A \multimap !A \otimes !A\\ e_A: \; !A \multimap 1\]

avec

\[tr_\ell(d_A) ≝ \lbrace (d, (d', d'')) \mid d' ∪ d'' = d, d ∈ Cl_{fin}(A)\rbrace\\ tr_\ell(e_A) ≝ \lbrace (∅, \star) \rbrace\]

NB: dans $!A$, attention: $∅$ est la clique vide de $A$ vue comme élément de l’espace $!A$.

DONC on a des règles de contraction et d’affaiblissement unique pour les formules de la forme $!A$

\[\cfrac{⊢ Γ, ?A, ?A}{⊢ Γ, ?A}\;\text{contraction}\] \[\cfrac{⊢ Γ}{⊢ Γ, ?A}\;\text{affaiblissement}\]

Logique linéaire intuitioniste

On restreint aux séquent avec une seule formule à droite.

\[A, B ≝ X \mid A \multimap B \mid A \otimes B\\ \mid 1 \mid A \& B \mid ⊤ \mid A \oplus B \mid 0 \mid !A\]

NB:

  • on n’a pas le parr $\,⅋\,$ (remplacé par $\multimap$) parce qu’on ne peut pas l’introduire avec une seule formule à droite.
  • le pourquoi pas $?$ est éliminé aussi

Calcul des séquents

\[\cfrac{}{A ⊢ A}\;ax\] \[\cfrac{Γ ⊢ A \quad Δ, A ⊢ C}{Γ, Δ ⊢ C}\;cut\]

échange

\[\cfrac{Γ ⊢ A \quad Δ ⊢ B}{Γ, Δ ⊢ A \otimes B}\;\otimes_R\] \[\cfrac{Γ, A, B ⊢ C}{Γ, A \otimes B ⊢ C}\;\otimes_L\] \[\cfrac{}{⊢ 1}\;1_R\] \[\cfrac{Γ ⊢ C}{Γ, 1 ⊢ C}\;1_L\] \[\cfrac{Γ, A ⊢ B}{Γ ⊢ A \multimap B}\;\multimap_R\] \[\cfrac{Γ ⊢ A \quad Δ, B ⊢ C}{Γ, Δ, A \multimap B ⊢ C}\;\multimap_L\] \[\cfrac{Γ ⊢ A \quad Δ, B ⊢ C}{Γ, Δ, A \multimap B ⊢ C}\;\multimap_L\]

etc…

NB:

  • ce fragment suffit pour faire du $λ$-calcul.

  • plus pratique pour les catégories, car dans l’autre on avait tout à droite, alors qu’en catégorie:

    \[𝒞(Γ, A) ≃ Γ ⊢ A\]

    mais avec les catégories $\star$-autonomes, avec le dual, on peut faire passer les chose à gauche ou à droite (mais le fait d’avoir tout à droite ajoute du “bruit syntaxique”).

cf. llwiki.ens-lyon.fr

Intuition

La logique linéaire (LL) n’a pas de règles structurelles, à part pour les formules avec un bang.

En LL, une formule est une ressource qu’on peut utiliser qu’une fois (sauf en cas de bang), et qu’on ne peut pas jeter (“écologique”)

  • $A \multimap B$: mécanisme qui fait perdre $A$ pour nous donner $B$

  • $A \otimes B$: présence simultanée de deux ressources

  • $1$: absence de ressource

  • $A \oplus B$: choix de ressource que je ne contrôle pas, j’ai soit $A$, soit $B$, mais je ne sais pas a priori lequel (c’est donnée par la preuve).

  • $A \& B$: il y a les 2 ressources $A$ et $B$, mais je dois choisir l’une des deux

  • $⊤$:

  • $0$: on n’a rien du tout, c’est le faux ultime (alors que $⊥$ est un faux plus léger, il ne nous permet de démontrer que des formules de la forme $?A$)

  • $!A$: la ressource $A$ autant de fois que je veux

  • $?A$: la ressource peut m’être demandée un nombre arbitraire de fois

  • $A^⊥ \,⅋\, B^⊥$: demande simultanée des ressources (dual du tenseur)

  • $A \,⅋\, B$: deux ressources disponibles, mais il y a un “vase communiquant” entre les deux: quand j’en consomme une, ça a un impact sur l’autre

  • $⊤$: absence de choix (pas de stand frites par exemple, pour reprendre l’exemple du menu de Lafont)

\[\underbrace{A \multimap B}_{A^⊥ \,⅋\, B} = B^⊥ \multimap A^⊥\] \[15 \text{ euros } \multimap (\text{ salade } \& \text{ escargots } \& \text{ foie gras }) \otimes ((\text{ dorade } \oplus \text{ bar }) \underbrace{\&}_{\text{avec}} \text{ côte de boeuf }) \otimes !\text{eau}\]

Menu de Lafont:

On a 15 euros: on a un tenseur de trois choses

  • entrée au choix

    • salade
    • escargots
    • foie gras

  • plat au choix

    • dorade OU bar, mais ne dépend pas de moi: selon l’arrivage

    • côte de boeuf

  • eau: à volonté (= bang)

Cela, c’est notre point de vue ⟶ en faisant la négation linéaire, on va avoir le point de vue du restaurant, qui va recevoir 15 euros, mais va devoir fournir les ressources.

Ex: du point de vue du restaurant: $?\text{eau}$ ⟶ demandée un nombre arbitraire dde fois

Fragment intuitionniste: traduction de Girard

Fragment de la logique linéaire intuitionniste, où ne prend que

\[A, B ≝ X \mid !A \multimap B \mid A \& B \mid ⊤ \mid !A \oplus !B \mid 0\]

Définition de la logique intuitionniste:

\[A, B ≝ X \mid A ⇒ B \mid A ∧ B \mid ⊤ \mid A ∨ B \mid ⊥\] \[\underbrace{LJ}_{\text{logique intuitionniste}} \overset{(\_)^G}{\hookrightarrow} \underbrace{ILL}_{\text{fragment linéaire intuitionniste}}\] \[Γ ⊢ A \; ⟼ \; !Γ^G ⊢ A^G\]

NB: de même, on peut traduire la logique classique en logique linéaire, mais il y a plusieurs traductions possibles.

Pourquoi le $∧$ de $LJ$ a été traduit en “avec” $\&$ ?

Car

\[A \& B \multimap A \text{ et } A \& B \multimap B\]

mais on n’a pas

\[A \otimes B \multimap A \text{ ou } A \otimes B \multimap B\]

(on ne peut pas “jeter” les ressources du produit tensoriel)

Leave a comment