Cours 6: Domaines de Scott

Dans une Catégorie Cartésienne Close (CCC)

Hom interne:
\[𝒞(Γ × A, B) ≃ 𝒞(Γ, \underbrace{A ⇒ B}_{= B^A \text{ : hom interne de la CCC}})\]

De plus:

\[1 × A ≃ A\]

Pourquoi “hom interne”?

Soit $A ∈ 𝒞$:

Point (élément) de $A$:

$a: 1 ⟶ A$

\[𝒞(A, B) ≃ 𝒞(1 × A, B) ≃ 𝒞(1, B^A)\]

Propriété fondamentale de la sémantique dénotationnelle

\[M ≃_β N ⟹ ⟦M⟧_ρ = ⟦N⟧_ρ\]

Donc

\[⟦M⟧_ρ = ⟦N⟧_ρ ⟹ ∀ρ', C \text{ contexte}; ⟦C[M]⟧_{ρ'} = ⟦C[N]⟧_{ρ'}\]

Théorème de Böhm en $λ$-calcul: Si $M$ et $N$ sont $βη$-normaux:

\[M \neq N ⟹ ∃ C \text{ contexte}; \begin{cases} C[M] ⟶^\ast \texttt{TRUE} ≝ λx,y.x \\ C[N] ⟶^\ast \texttt{FALSE} ≝ λx,y.y \\ \end{cases}\]

Dans le cas du $λ$-calcul pur, on cherche $λ: D^D ⟶ D, @: D ⟶ D^D$ tq

  • $β$-contraction:

    \[@ \circ λ = id_{D^D}\]

NB: Si on veut aussi la $η$-expansion:

  • $η$-expansion:

    \[λ \circ @ = id_D\]

Retour aux fonctions Scott-continues

Remarque: Comme les fonctions continues sont déterminées par leurs valeurs sur un ensemble dense, tel que $ℚ ⊆ ℝ$:

\[\underbrace{\vert 𝒞^0(ℝ) \vert}_{= \vert ℝ^ℚ \vert = \vert ℝ \vert} ≃ \vert ℝ \vert\]

Domaines de Scott

Compacité

Compacité d’un point ≃ point isolé d’une suite

Point $d ∈ (D, ≤)$ compact:

ssi \(∀ Δ \text{ filtrant}, d ≤ ∨ Δ ⟹ ∃x ∈ Δ, d ≤ x\)

NB: Les points compacts correspondent à une quantité finie d’information (rappel: $⊥$: pas d’information): puisque si l’information de $d$ est contenue dans $∨ Δ$, alors il existe un rang fini à partir duquel on a cette information.

On pose

\[𝒦(x) ≝ \lbrace d ≤ x \mid d \text{ compact} \rbrace\]

L’ensemble des compacts est filtrant (le sup de deux compacts est compact).

Ex de point non-compact:

Dans $ℕ ∪ \lbrace ω \rbrace$, la chaîne ascendante des entiers, ayant pour sup $ω$, $d = ω$ n’est pas compact:

  • $d = ω ≤ ω$
  • mais n’existe pas d’entier $n$ tel que $d = ω ≤ n$

Domaines de Scott

$x, y∈D$ sont compatibles:

ssi il existe $z$ tel que $x, y ≤ z$

Un cpo $(D, ≤)$ est un domaine de Scott:

ssi

  1. Pour tous $x, y ∈ D$ compatibles, $x ∨ y$ existe
  2. Algébricité: \(∀x ∈ D, x = \bigvee 𝒦(x)\)

Soit $f: (D, ≤) ⟶ (E, ≤)$ et soient $x ∈ D,\; e\text{ compact } ≤ f(x)$ ($e$ est un approximant fini de l’image de $x$).

On pose

\[apx_f(x, e) ≝ \lbrace d ∈ 𝒦(x) \mid e \text{ compact } ≤ f(d)\rbrace\]

NB: on se rapproche de la notion de continuité: pour toute approximation finie de $f(x)$ a pour image réciproque une approximation finie de $x$.

Caractérisation des fonctions continues sur les compacts

Prop: Soient $D, E$ des domaines de Scott, et $f: D ⟶ E$.

  1. $f$ est continue, i.e. $∀ Δ \text{ filtrant}$:

    • $f(Δ)$ filtrant
    • $∨ f(Δ) = f(∨ Δ)$
  2. \[∀x ∈ D, f(x) = \bigvee_{d ∈ 𝒦(x)} f(d)\]
  3. $f$ est monotone et \(∀ x∈D, e ∈ 𝒦(f(x)), apx_f(x, e) ≠ ∅\)

Preuve:

1) ⟹ 2)

\[f(x) = f\left(\bigvee_{d ∈ 𝒦(x)} d\right) = \bigvee_{d ∈ 𝒦(x)} f(d)\]

2) ⟹ 3)

Monotonie:

Si $x ≤ x’$, alors $𝒦(x) ⊆ 𝒦(x’)$, et

\[f(x) = \bigvee_{d ∈ 𝒦(x)} f(d) ≤ \bigvee_{d ∈ 𝒦(x')} f(d) = f(x')\]

Soit $e ∈ 𝒦(f(x))$. On cherche $d ∈ 𝒦(x)$ tel que $e ≤ f(d)$.

\[e ≤ f(x) = \bigvee_{d ∈ 𝒦(x)} f(d) \overset{\text{compacité de } e}{⟹} ∃d∈ 𝒦(x), e ≤ f(d)\]

3) ⟹ 1)

La monotonie donne le caractère fibrant de $f(Δ)$ et l’inégalité $∨ f(Δ) ≤ f(∨Δ)$.

Montrons que $f(∨Δ) ≤ ∨ f(Δ)$: par algébricité, il suffit de démontrer:

\[𝒦(f(∨Δ)) ⊆ 𝒦(∨ f(Δ))\]

Soit $e ∈ 𝒦(f(∨Δ))$. On sait qu’il existe $d ∈ apx_f(∨Δ, e) ≠ ∅$.

En particulier, $d ∈ 𝒦(∨ Δ)$, et par compacité: \(∃x ∈ Δ; d ≤ x\)

Donc

\[e ≤ f(d) \overset{\text{monot.}}{≤} f(x) ≤ \bigvee f(Δ)\]

NB:

  • donc les fonctions continues sont caractérisées par leurs valeurs sur les compacts.

Topologie de Scott

Scott-continuité ⟺ continues pour la topologie de Scott:

$O$ ouvert de Scott ssi

  • $O$ est clos par le haut:

    \[x ∈ O, x ≤ x' ⟹ x' ∈ O\]

  • $∀Δ \text{ filtrant}$:

\[∨ Δ ∈ O ⟹ O ∩ Δ ≠ ∅\]

Prop: Soient $(D, ≤), (E, ≤)$ des cpos. Alors $f: D ⟶ E$ est continue par rapport à la topologie de Scott ssi elle est Scott-continue (au sens défini précédemment).

A partir de maintenant, on va laisser tomber la topologie…. :-(

On va considérer des extensions qui ne vont prendre en compte que l’ordre des cpos.

Historiquement, on avait des modèles “trop gros”, contenant des fonctions continues n’étant l’interprétation d’aucun $λ$-terme.

Ex: considérer le cpo (fini, donc domaine de Scott)

$Bool$:

  digraph {
    rankdir=BT;
    ⊥ -> 1, 0;

  }

On pose

\[\text{ou parallèle}≝ \begin{cases} Bool × Bool &⟶ Bool \\ (⊥,⊥) &\mapsto ⊥ \\ (⊥,1) &\mapsto 1 \\ (1,⊥) &\mapsto 1 \\ (⊥,0) &\mapsto 0 \\ (0,⊥) &\mapsto 0 \\ (0,0) &\mapsto 0 \\ \end{cases}\]

(les autres cas étant définis par monotonie)

Cette fonction ne peut être l’interprétation d’aucune $λ$-terme, parce qu’en $λ$-calcul, il y a toujours une dissymétrie (un argument qui domine sur l’autre).

Par contre, le ou séquentiel est implémentable par des $λ$-termes:

\[\text{ou séquentiel}≝ \begin{cases} Bool × Bool &⟶ Bool \\ (⊥,⊥) &\mapsto ⊥ \\ (⊥,1) &\mapsto ⊥ \\ (1,⊥) &\mapsto 1 \\ (⊥,0) &\mapsto 0 \\ (0,⊥) &\mapsto 0 \\ (0,0) &\mapsto 0 \\ \end{cases}\]

(deuxième ligne change)

On a donc cherché une sémantique plus “restreinte” qui rejette des fonctions comme le ou parallèle. Cette restriction est le déterminisme ⟶ on ne peut obtenir 1 que d’une seule manière avec le ou séquentiel.

⟹ Gérard Berry: $dI$-domains:

condition supplémentaire de stabilité, l’ensemble $apx_f(x, e) ≠ ∅$, a un minimum (qui correspond à l’information minimale qui nous conduit à l’approximation $e$)

Dans $dI$-domain:

  • c’est un domaine de Scott
  • il y a les infs
  • $d$ pour distributivité
  • propriété $I$: si $d$ est compact, alors $𝒦(d)$ est fini

Espaces cohérents (espaces de cohérence)

  • Cas particulier des $dI$-domains.
  • en anglais: coherence spaces (car coherent spaces déjà pris) ⟶ en fr: “espaces de cohérence”
Un espace cohérent:

est une paire $A = (\vert A \vert, \sim_A)$ où:

  • $\vert A \vert$ est un ensemble, dit trame
  • $\sim_A ⊆ \vert A \vert × \vert A \vert$ est une relation réflexive et symétrique, dite cohérence.
Une clique de $A$:

est un ensemble $x ⊆ \vert A \vert$ tq \(∀a, a' ∈ x, a \sim_A a'\)

Ex: $Bool ≝ (\lbrace 0, 1 \rbrace, 0 \sim_A 0, 1 \sim_A 1)$

On dénote par $Cl(A)$ l’ordre partiel des cliques de $A$ ordonnées par inclusion.

NB: les éléments de la trame sont dénotés par $a ∈ \vert A \vert$, les cliques par $x ⊆ \vert A \vert$

Prop: $Cl(A)$ est un $dI$-domain

Preuve:

Plus petit élément

$⊥ = ∅$

Sup filtrants

Si $Δ ⊆ Cl(A)$ filtrante: $∀x, x’ ∈ Δ, ∃ z ∈ Δ; x, x’ ⊆ z$.

  • $\bigcup Δ$ est une clique (union des éléments de $Δ$).
  • $a, a’ ∈ \bigcup Δ ⟹ ∃Δ \ni x \ni a, x’ \ni a’$

Lemme: les points compacts de $Cl(A)$ sont exactement les cliques finies.

Preuve:

Soit $d ∈ Cl(A)$ une clique finie, et $d ⊆ \bigcup Δ$ où $Δ ⊆ Cl(A)$ est filtrante. On vérifie que $d ⊆ x$, pour une clique $x ∈ Δ$.

Soit $d ∈ Cl(A)$ telle que $∀Δ \text{ filtrant}$,

\[d ⊆ \bigcup Δ ⟹ ∃ x ∈ Δ; d ⊆ x\]

Prenons

\[Δ ≝ \lbrace e \mid e \text{ finie} ⊆ d \rbrace\]

C’est filtrant, et $\bigcup Δ = d$ (en fait, c’est l’algébricité, qu’on démontre là).

Par hypothèse,

\[∃e ∈ Δ \text{ tq } d ⊆ e\]

donc $d$ est finie.

On vérifie les autres propriétés aisément.

Catégorie des espaces cohérents

Soient $A, B$ des espaces cohérents.

Morphismes $f: A ⟶ B$ de la catégorie des espaces cohérents

Les morphismes sont les

fonctions continues $f: A ⟶ B$:

i.e. les fonctions Scott-continues de $Cl(A)$ vers $Cl(B)$

Trace d’une fonction continue

Soient $x ∈ Cl(A), \; e ⊆_{\text{finie}} f(x)$

On sait que

\[apx_f(x, e) ≠ ∅\]

i.e.

\[∃ \, d ⊆_{\text{finie}} x; e ⊆ f(d)\]

On peut appliquer cela à $e ≝ \lbrace b \rbrace$, avec $b ∈ f(x)$.

\[∃ \, d ⊆_{\text{finie}} x; b ∈ f(d)\]

NB: une clique peut être vue comme un ensemble d’informations cohérentes entre elles.

Trace de $f$:
\[tr(f) ≝ \lbrace (d, b) ∈ Cl_{finie}(A) × \vert B \vert \mid b ∈ f(d)\rbrace\]

La trace caractérise $f$, dans un domaine de Scott:

\[f(x) = \bigcup\limits_{d ⊆_{\text{finie}} x} f(d) = \lbrace b \mid ∃ \, d ⊆_{\text{finie}} x; \; (d, b) ∈ tr(f) \rbrace\]

Leave a comment