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}

et

\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

et

μ \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
  1. le premier iso vient du fait que l’adjoint à droite $G$ préserve les limites

  2. 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)$

avec

  • $𝒰 \dashv !$
  • $(ℳ, \otimes, 1)$ est la cat des objets isomorphes à $!A$ pour un $A$
!A \otimes !B ≃ !(A \& B) ⟶ !A

Leave a comment