Cours 12: Axiomatisation catégorique de la logique linéaire

Rappels

On peut voir le $λ$-calcul comme une théorie équationnelle engendrée par cette équation (propagée à tous les contextes):

\[(λx. M)N =_β M \lbrace N/x \rbrace \\ M =_η λx. Mx \text{ si } x ∉ fv(M)\]

Vision venant de la théorie des modèles: on cherche des modèles de la théorie équationnelle du $λ$-calcul

NB: dans $Set$, il n’y en a pas, à cause du fait qu’on n’a pas de $D$ tel que

\[D^D \hookrightarrow D\]

Modèle $D$ du $λ$-calcul:: $D$ est un objet d’une CCC tel que $D^D \hookrightarrow D$

En théorie des modèles: on n’a qu’une seule sorte normalement (tous les éléments appartiennent au même domaine), mais avec le $λ$-calcul simplement typé ⟶ il y a une infinité de sortes données par ses types

\[A ≝ α \mid A → B\]

Et un modèle de cela est une CCC.

Logique linéaire

Mais maintenant, on a un calcul plus riche, avec la logique linéaire:

Types:: \[A, B \; ≝ \; X \mid X^⊥ \mid A \multimap B \mid 1 \mid A \& B \mid ⊤ \mid A \oplus B \mid 0\]
Termes:: \[M, N \; ≝ \; a \mid λa. M \mid MN \mid M \otimes N \mid M[a \otimes b := N] \mid \star \mid M[\star := N] \qquad \text{(fragment multiplicatif)}\\ \mid ⟨M, N⟩ \mod π_i \, M \mid ⟨⟩ \mid ι_i \, M \mid \texttt{case } M \texttt{ of } 1a.N /2a. P \mid \underbrace{ε.M}_{\text{destructeur } \cfrac{⊥}{A}} \qquad \text{(fragment additif)} \\ \mid x \mid !M \mid M[!x := N] \qquad \text{(fragment exponentiel)}\]

Règles de réécriture: une pour chaque connecteur, sauf $⊤, ⊥$ et $0$

Réécriture pour les multiplicatifs

\[(λa. M)[\_]N ⟶ M \lbrace N/a \rbrace [\_] \\ M[a \otimes b := (N \otimes P)[\_]] ⟶ M \lbrace N/a, P/b \rbrace [\_]\\ M[\star := \star[\_]] ⟶ M[\_]\]

Réécriture pour les additifs

\[π_i(⟨M_1, M_2⟩[\_]) ⟶ M_i [\_] \\ \texttt{case } (ι_i \, M)[\_] \texttt{ of } 1a.N_1 / 2a. N_2 ⟶ N_1 \lbrace M/a \rbrace [\_]\\ M[!x := (!N)[\_]] ⟶ M \lbrace N/x \rbrace [\_]\]

NB: les contextes jouent le même rôle que pour les réseaux, ça nous évite d’écrire des dizaines de règles de commutativité

Y a-t-il une sémantique pour cette syntaxe, qui a maintenant “une vie en elle-même”? (on est partis des espaces cohérents pour arriver à la syntaxe, puis maintenant on fait le retour syntaxe → sémantique).

Modèles de la logique linéaire: Catégories de Lafont-Seely

Catégorie $𝒞$ $\star$-autonome:

c’est une SMCC $(𝒞, \otimes, 1)$ telle que

\[(\_)^\star: 𝒞^{op} ⟶ 𝒞\]
\[{(\_)^\star}^{\star} ≃ Id\]
Pour tout $A$: $(A \otimes (\_)^\star)^{\star}$ est adjoint à droite de $A \otimes \_$ (c’est la flèche)

NB: dans le cas des e.v., le $\star$ est le dual (c’est un cas particlier de $\star$-autonome, puisqu’elle est compacte close).

Monoïde dans une catégorie monoïdale $(𝒞, \otimes, 1)$:

est un triplet $(A, μ, ν)$ où:

$A ∈ 𝒞$
$μ: A \otimes A ⟶ A$
$η: 1 ⟶ A$

tel que les diagrammes entre $λ_{A}, η$ et $μ$ et le diagramme suivant commutent:

\[\begin{xy} \xymatrix{ A \otimes (A \otimes A) \ar[rr]^{α_{A, A, A}} \ar[d]_{id_A \otimes μ} && (A \otimes A) \otimes A \ar[d]^{μ \otimes id_A} \\ A \otimes A \ar[rd]_{μ_A} && A \otimes A \ar[ld]^{μ_A} \\ &A } \end{xy}\]

Si $𝒞$ est symétrique, on que $A$ est commutatif si le diagramme entre $σ_{A, A}$ et $μ$ commute.

NB:

dans $(Set, ×, 1)$: un monoïde nous donne la définition classique
dans la cat des e.v.: c’est une algèbre
dans la cat des espaces topologique: c’est un monoïde topologique
dans la cat des monoïdes: c’est un monoïde commutatif

Un comonoïde:: est un monoïde dans la catégorie opposée

NB: intuitivement:

un monoïde correspond à une façon de d’assembler des éléments
un comonöide correspond à une façon de diviser des éléments
- l’élément neutre donne une manière de détruire un élément
- ça va nous être très utile en logique linéaire ⟶ on va avoir l’affaiblissement (duplication) et la contraction

Soient $(A, μ_A, η_A)$ et $(B, μ_B, η_B)$ deux monoïdes dans $(𝒞, \otimes, 1)$.

Un morphisme $f: A ⟶ B$ est de monoïdes si les diagrammes suivants commutent:

\[\begin{xy} \xymatrix{ A \otimes A \ar[r]^{f \otimes f} \ar[d]_{μ_A} & B \otimes B \ar[d]^{μ_B} \\ A \ar[r]_f & B } \end{xy}\]

\[\begin{xy} \xymatrix{ 1 \ar[r]^{η_A} \ar[rd]^{η_B} & A \ar[d]^{f} \\ & B } \end{xy}\]

Un modèle de la logique linéaire (= Catégorie de Lafont-Seely) est donné par:

une SMCC $ℒ(\otimes, 1, \multimap)$ (tout seul: donne un modèle de I(intuitionnistic)M(ultiplicative)LL)
- si on veut être classique (M(ultiplicative)LL): alors on demande une catégorie $\star$-autonome
avec produits et coproduits finis (IMA(dditive)LL)
une structure exponentielle (à détailler):
- pour tout $A ∈ ℒ$, un comonoïde symétrique $(!A, δ_A, ε_A)$ par rapport à $\otimes$
- une flèche $e_A: !A ⟶ A$ telle que pour toute flèche $f: !A ⟶ B$, il existe un unique morphisme de comonoïdes $f^{\dagger}: !A ⟶ !B$ tel que le diagramme suivant commute
  \[\begin{xy} \xymatrix{ !A \ar[r]^{f^\dagger} \ar[rd]_{f} & !B \ar[d]^{e_B} \\ & B } \end{xy}\]
- des isomorphismes de comonoïdes:
  \[!A \otimes !B \; ≃ \; !(A \& B)\\ 1 \; ≃ \; !⊤\]
  où $⊤$ est l’objet terminal et $\&$ le produit binaire, et
  \[δ: \; !A \otimes !B \overset{δ_A \otimes δ_B}{⟶} (!A \otimes !A) \otimes (!B \otimes !B) \overset{\text{sym}}{⟶} (!A \otimes !B) \otimes (!A \otimes !B) \\ ε: \; !A \otimes !B \overset{ε_A \otimes ε_B}{⟶} 1 \otimes 1 \overset{λ_1 = e_1}{⟶} 1 \\ δ_1: \; 1 \overset{λ_1^{-1} = e_1^{-1}}{⟶} 1 \otimes 1 \\ ε_1: \; 1 \overset{id}{=} 1\]

NB 1: celle-ci est l’axiomatique la plus synthétique/élémentaire.

NB 2: les parties multiplicatives et additives de la LL sont totalement standard en catégories: elles ne sont pas adhoc pour la LL. C’est la partie exponentielle qui n’a pas d’équivalent catégorique trivial ⟶ partie exponentielle: a mis une dizaine d’années à être définie (fin: dans les années 90).

NB 3: Vient de la définition orginelle de Lafont:

Catégorie avec tenseur, flèche, etc… tel que tout object $A$ a le comonoïde commutatif libre $!A$ sur lui: i.e pour tout commonoïde commutatif $C$, $f^{\dagger}: C ⟶ !A$ est unique et

\[\begin{xy} \xymatrix{ C \ar[r]^{f^\dagger} \ar[rd]_{f} & !A \ar[d]^{e_A} \\ & A } \end{xy}\]

commute

(ex: $!B \otimes !C$ n’est pas de la forme $! \_$, mais est quand même un comonoïde commutatif).

Mais cette notion est trop forte: car dans $Coh$, $!A$ n’est pas le comonoïde libre sur $A$ (alors qu’on a bien un modèle de la logique linéaire !): le comonoïde libre sur $A$ est

\[\vert !_m \, A \vert ≝ \lbrace μ \mid μ \text{ multi- ensemble fini sur } \vert A \vert \text{ tq } supp(μ) ∈ Cl(A) \rbrace\]

\[μ \sim_{!A} ν ⟺ supp(μ) ∪ supp(ν) ∈ Cl(A)\]

On n’a pas d’isomorphisme entre les deux foncteurs $!_e$ et $!_m$:

\[card \, \vert !_e \, 1 \vert = 2 \\ card \, \vert !_m \, 1\vert = ω\]

Mais $!_m$ donne bien un modèle pour Lafont, alors que $!_e$ non.

Puis Seely est arrivé, et a donné une nouvelle notion plus faible, malheureusement fausse ⟶ Melliès a unit les deux en corrigeant celle de Seely

Pourquoi est-ce un modèle, intuitivement ?

Dans un premier temps, ignorons les additifs.

Règles multiplicatives

\[\cfrac{}{A ⊢ A}\] \[\cfrac{Γ ⊢ A \qquad Δ, A ⊢ C}{Γ, Δ ⊢ C}\] \[\cfrac{Γ, A ⊢ B}{Γ ⊢ A \multimap B}\] \[\cfrac{Γ ⊢ A \qquad Δ, B ⊢ C}{Γ, Δ, A \multimap B ⊢ C}\] \[\cfrac{Γ, A, B ⊢ C}{Γ, A \otimes B ⊢ C}\]

Car si on a une preuve $\cfrac{δ}{C_1, ⋯, C_n ⊢ A}$, alors on a

\[⟦δ⟧ \bigotimes ⟦C_i⟧ ⟶ ⟦A⟧\] \[\cfrac{Γ ⊢ A \qquad Δ ⊢ B}{Γ, Δ \otimes A \otimes B}\]

Par propriété de bifonctorialité:

$f: Γ ⟶ A$
$g: Δ ⟶ B$

alors

\[f \otimes g: Γ \otimes Δ ⟶ A \otimes B\] \[\cfrac{}{⊢ 1}\] \[\cfrac{Γ ⊢ 1 \qquad Δ, 1 ⊢ C}{Γ, Δ ⊢ C}\]

Règles de structure

L’affaiblissement et la contraction correspondent à la structure de comonoïde (duplication et effacement).

Promotion et Déréliction

Le $\dagger$ interprète la promotion:

On a besoin du fait que le produit des bangs est (isomorphe à) le bang du produit ⟶ on a besoin des additifs.

\[\cfrac{!Γ ⊢ A}{!Γ ⊢ !A}\]

marche sans problème si $Γ$ est une formule, mais on a besoin des additifs sinon:

\[!C_1 \otimes !C_2 ≃ !(C_1 \& C_2)\]

(on se ramène à une seule formule, puis: iso dans le sens inverse)

Déréliction:

\[\cfrac{Γ, A ⊢ C}{Γ, !A ⊢ C}\]

Nouvelle Axiomatisation: Adjonction Linéaire-Non linéaire

Très élégant:

On a deux foncteurs monoïdaux:

$F: (ℳ, ×, t) ⟶ (ℒ, \otimes, 1, \multimap)$
$G: (ℒ, \otimes, 1, \multimap) ⟶ (ℳ, ×, t)$

avec

$F \dashv G$ est une adjonction monoïdale
$(ℳ, ×, t)$ cartésienne
$(ℒ, \otimes, 1, \multimap)$ avec produits et coproduits finis

$! ≝ F \circ G$ est une comonade monoïdale !!!! $e_A$ est la counité de cette comonade !

On a bien:

\[!(A \& B) = FG (A \& B) ≃ F(GA × GB) \qquad \\ ≃ FG A \otimes FG B = !A \otimes !B\]

le premier iso vient du fait que l’adjoint à droite $G$ préserve les limites
pour le deuxième iso: adjonction monoïdale (= adjonction dans la 2-cat des cat monoïdales) ⟺ adjonction + l’adjoint à gauche est monoïdal fort (préserve la structure monoïdale)

cf. Melliès: Categorical Semantics of Linear Logic / Panoramas et Synthèses

NB 1: quand on écrivait

\[Γ; Δ ⊢ A\]

à gauche: ça vit dans la catégorie cartésienne
à droite: ça vit dans la catégorie monoïdale

NB 2: avant, on était dans un cas particulier, avec

$!: Stab ⟶ Coh$
$𝒰: Coh ⟶ Stab$

et $! \dashv 𝒰$

(le foncteur d’oubli ne fait rien, c’est pour ça que la composition donne bien le bang)

$𝒰: (ℳ, \otimes, 1) ⟶ (ℒ, \otimes, 1, \multimap)$
$!: (ℒ, \otimes, 1, \multimap) ⟶ (ℳ, \otimes, 1)$