Cours 18: Catégorie des Espaces Cohérents: Modèle de PCF

cf. Linear Logic, Girard (1987)

Cette séance :

  1. Le “ou parallèle” n’existe pas dans les espaces cohérents
  2. Les espaces cohérents sont un modèle de PCF
$Coh_!$:

Catégorie de Kleisli induit par la comonade exponentielle de la catégorie sous-jacente

  • objets: Espaces cohérents $(\vert A \vert, \sim_A)$, où $\sim_A$ est réflexive et symétrique et la trame $\vert A \vert$ est dénombrable

  • $Coh(A, B)$: $f: Cl(A) ⟶ Cl(B)$ stable, i.e.

    • Monotone: $x ⊆ y ∈ Cl(A), f(x) ⊆ f(y)$

    • Préserve les sup: \(∀ \lbrace x_i \rbrace \Uparrow ⊆ Cl(A), \quad f\Big( \bigcup_i x_i \Big) = \bigcup_i f(x_i)\)

      • ces deux points sont la Scott-continuité

    • Préserve l’inf: \(∀x ∪ y ∈ Cl(A), \; f(x ∩ y) = f(x) ∩ f(y)\)

Modèle de PCF

Montrons que c’est un modèle de PCF: il faut

  • les produits cartésiens
  • l’objet exponentiel

pout interpréter la $β$-réduction

i.e. on doit montrer que

$Coh_!$ est une CCC.

NB: historiquement, Girard cherchait un modèle du système F, puis il découvre la logique linéaire

Kleisli et CCC

Modèle de la logique linéaire:

catégorie $\star$-autonome (SMCC pour la logique intuitionniste) avec une comonade $!$ exponentielle linéaire (i.e. est compatible avec la structure de SMC, par ex: $!(A \& B) ≃ !A \otimes !B$)

Kleisli d’une comonade:
\[𝒞_!(A, B) ≝ 𝒞(!A, B)\]

Si une catégorie $𝒞$ est un modèle de la logique linéaire, alors la catégorie de Kleisli $𝒞_!$ est une CCC

NB: il y a d’autres axiomatisations de la LL : entres autres :

  • linear-non linear adjunction
  • Seely categories

$Coh_!$ est une CCC

$Coh_!$ est Cartésienne

On notera $\&$ le produit cartésien, à partir de maintenant (comme on fait de la LL).

Soient $A, B$ deux espaces cohérents (esp coh).

Produit cartésien de $A \& B$:
  • \[\vert A \& B \vert ≝ \vert A \vert \sqcup \vert B \vert = \vert A \vert × \lbrace 0 \rbrace ∪ \vert B \vert × \lbrace 1 \rbrace\]
  • \[(a, b) \sim (a', b') ⟺ a \sim_A a' ∧ b \sim_B b'\]

On a

\[Cl(A \& B) = Cl(A) × Cl(B)\] \[π_i(x_0, x_1) ≝ x_i\]

Soit $z ∈ Cl(C)$.

\[⟨f_0, f_1⟩ (z) ≝ (f_0 (z), f_1(z))\]

NB: on ne peut pas poser \(\vert A \& B \vert ≝ \vert A \vert × \vert B \vert\) car sinon on définit le tenseur des deux espaces, et:

  • \[Cl(A \& B) = \lbrace z ⊆ \vert A \vert × \vert B \vert \mid ∃x ∈ Cl(A), y ∈ Cl(B); z ⊆ x × y \rbrace\]
  • \[π_i ≝ \begin{cases} Cl(A_0 \& A_1) &⟶ Cl(A_i) \\ x &\mapsto \lbrace a_i \mid ∃ a_{1-i}; (a_0, a_1) ∈ x \rbrace \end{cases}\]
  • On n’a pas la propriété universelle du produit: en prenant $A_0 ≝ ∅$: $A_0 × A_1 = ∅$, donc la composition $A_1 \overset{⟨∅, id_{A_1}⟩}{⟶} A_0 × A_1 \overset{π_1}{⟶} A_1$ ne peut pas valoir $id_{A_1}$

NB: similairement aux espaces vectoriels : la trame est une base, et $Cl(A)$ est l’espace engendré par la base

$Coh_!$ est Close

\[\begin{xy} \xymatrix{ A × B^A \ar[r]^{ev} & B \\ A × C \ar@{.>}[u]^{id × Λ(f)} \ar[ur]_f & } \end{xy}\]

Si $f: A ⟶ B$ est stable, alors pour tout $x ∈ Cl(A)$, pour tout $b ∈ f(x)$ (“bout d’information”), il existe une unique clique minimale $x_0 ⊆ x$ telle que $b ∈ f(x_0)$

NB: $x_0$ peut-être vue comme l’information minimale pour générer $b$ (on n’a pas ça pour les fonctions Scott-continues).

Preuve: La preuve utilise la définition des fonctions Scott-continues comme étant les fonctions monotones qui préserve les sups de familles dirigées.

Soit

\[D ≝ 𝒫_{fin}(x)\]

de telle sorte que

\[x = \bigcup_{d ∈ D} d\]

Alors

\[b ∈ f(x) = bigcup_{d ∈ D} f(d)\]

par Scott-continuité. Donc il existe un $x_0 ∈ D$ minimal tel que

\[b ∈ f(x_0)\]

Unicité: supposons qu’il existe un autre $x’_0$ minimal tel que $b ∈ f(x’_0)$.

Comme $x_0 ∪ x’_0 ⊆ x ∈ Cl(A)$, alors

\[f(\underbrace{x_0 ∩ x'_0}_{⊆ x_0}) = f(x_0) ∩ f(x'_0) \ni b\]

Le graphe d’une fonction stable peut donc être donné par les paires de “bouts de sortie” $b$, et les informations minimales $x_0$ associées à ces bouts $b$ ⟶ ça nous donne la trace ($x_0$ fini: continuité, unicité de $x_0$: stabilité).

\[Tr_{stab}(f) ≝ \lbrace (x_0, b) ∈ Cl_{fin}(A) × \vert B \vert \mid b ∈ f(x_0) \text{ et } ∀ x'_0 ⊊ x_0, b ∉ f(x_0) \rbrace\]

NB: on peut définir, pour tout fonction continue, la trace de manière générale :

\[Tr(f) ≝ \lbrace (x_0, b) ∈ Cl_{fin}(A) × \vert B \vert \mid b ∈ f(x_0) \rbrace\]

Mais la stabilité est essentielle pour donner des modèles (interpréter le 2e ordre) du système F, par exemple.

Notations: on notera $Tr$ la trace stable pour une fonction stable, par abus de notation.

Hom-interne $A ⇒ B$:
  • \[\vert A ⇒ B \vert = Cl_{fin}(A) × \vert B \vert\]
  • \[(x, b) \frown_{A ⇒ B} (x', b') ⟺ \text{ si } x ∪ x' ∈ Cl(A), \text{ alors } b \frown_B b'\]

NB:

  • comme $f$ doit envoyer une clique sur une clique, si $x$ et $x’$ sont cohérents dans le domaine, alors nécessairement $b$ et $b’$ appartiennent à la même clique dans le codomaine

  • Si $b = b’$, alors par minimalité, on ne peut pas avoir deux informations minimales distinctes qui le génèrent

Prop: $f: Cl(A) ⟶ Cl(B)$ est stable ssi $Tr_{stab}(f) ∈ Cl(A ⇒ B)$

Des cliques vers les fonctions stables

Soit $T ⊆ \vert A ⇒ B \vert$.

\[\hat{T}: \begin{cases} Cl(A) &⟶ Cl(B) \\ x &\mapsto \lbrace b \mid ∃ x_0 ⊆ x; (x_0, b) ∈ T \rbrace \end{cases}\]

NB: c’est plus compliqué que dans $Set$ et $CPO$: dans ces catégories, le Hom-interne étaient les fonctions elles-mêmes. Ici: on utilise des représentants de ces fonctions (les traces).

On a la même chose pour les fonctions holomorphes ! La trace est alors le développement en série entière !

Pour les fonctions $𝒞^∞$, la trace est l’expansion de Taylor !

Morphisme d’évaluation

\[ev: \begin{cases} A × A ⇒ B &⟶ B \\ (x, T) &\mapsto \hat{T} \end{cases}\]

Montrer que $ev$ est Scott-continue : similaire à $Set$.

Mais montrer qu’elle est stable est beaucoup plus délicat !

Astuce: utiliser la trace $Tr(ev)$ dans $\vert (A × A ⇒ B) ⇒ B \vert$:

\[Tr(ev) ≝ \Big\lbrace \Big((x, \lbrace (x, b) \rbrace), b\Big) \mid x ∈ Cl_{fin}(A), b ∈ \vert B \vert\Big\rbrace\]

Détails dans Proofs and Types.

Parallel or

$⟦\underbrace{\omicron}_{= 1 \oplus 1}⟧ =$

  digraph {
    rankdir=TB;
    tt; ff;
  }

$Cl(⟦\omicron⟧) =$

  digraph {
    rankdir=BT;
    ∅ -> "{tt}", "{ff}";
  }
\[por: \omicron × \omicron ⟶ \omicron\] \[Cl(\omicron \& \omicron) = Cl(\omicron) × Cl(\omicron)\] \[por ≝ \begin{cases} \omicron × \omicron ⟶ \omicron\\ ∅, \lbrace tt \rbrace &⟼ \lbrace tt \rbrace\\ \lbrace tt \rbrace, ∅ &⟼ \lbrace tt \rbrace \\ ∅, ∅ &⟼ ∅\\ \end{cases}\]

Prop: $por$ n’est pas stable

Preuve:

$(∅, \lbrace tt \rbrace), (\lbrace tt \rbrace, ∅) ⊆ (\lbrace tt \rbrace, \lbrace tt \rbrace)$

Mais

\[∅ = por(\underbrace{(∅, \lbrace tt \rbrace) ∩ (\lbrace tt \rbrace, ∅)}_{= (∅, ∅)}) ≠ por((∅, \lbrace tt \rbrace)) ∩ por((\lbrace tt \rbrace, ∅)) = \lbrace tt \rbrace ∩ \lbrace tt \rbrace = \lbrace tt \rbrace\]

Autrement:

\[((\lbrace tt \rbrace, ∅), tt), ((∅, \lbrace tt \rbrace), tt) ∈ Tr(por)\]

Mais

\[(\lbrace tt \rbrace, ∅) \text{ et } (∅, \lbrace tt \rbrace) \text{ sont cohérents (leur union est une clique)}\]

sans que

\[b ≝ tt \frown_\omicron b' ≝ tt\]

Leave a comment