Cours 2 : Modèles du 𝜆-calcul

Modèle du $𝜆$-calcul

Modèle du $𝜆$-calcul :
  • Un ensemble $D≠∅$ (domaine) muni

  • une fonction $⟦\bullet ⟧$ :

    • tq pour tout $𝜆$-terme $t$, environnement $𝜌 : Var ⟶ D$, $⟦t⟧𝜌 ∈ D$

tq pour tous $u, v$ :

\[u =_𝛽 v ⟹ ⟦u⟧𝜌 = ⟦v⟧𝜌\]

NB :

  • Gros problème ⟶ une seule solution avec cette définition naïve : $D$ est un singleton
  • On aimerait $D^D ≃ D$, mais si on a ça, alors $D$ est un singleton ⟶ cf. th de Cantor :
    • \[\vert D^D \vert = \vert D \vert^{\vert D \vert} ≥ 2^{\vert D \vert} > \vert D \vert \text{ si } \vert D \vert≥2\]
  • $⟦x⟧𝜌 = 𝜌(x)$
  • $⟦uv⟧𝜌 = i(⟦u⟧𝜌)(⟦v⟧𝜌)$
  • $⟦𝜆x. u⟧𝜌 = r(V \mapsto ⟦u⟧(𝜌[x \mapsto V]))$

Dana Scott ⟶ sémantique dénotationelle

⟹ invente le premier modèle non-trivial du $𝜆$-calcul : $D_∞$ (propriétés simples mais définition compliquée)

Plotkin : invente, lui, le modèle $ℙ_𝜔$ (propriétés compliquées mais définition simple)

Engeler : modèle proche de celui de Plotkin.

DCPO :

Dans $ℙ(A), ⊆$, pour tout $E⊆A$, $ℙ_{fin}(E)$ est dirigée.

Ex de fonction non Scott-continue :

la fonction $f$ “quantificateur universel pour 1”,

$f(1⋯1) = \bot$ nécessairement pour avoir la monotonie (puisque qu’on doit avoir $\bot = f(110) ≥ f(11)$), mais

\[\top = f(1⋯) ≠ \sup \underbrace{f(1⋯1)}_{=\bot} = \bot\]

Bijection de $ℕ^2 ⟶ ℕ$

\[\begin{cases} ℕ^2 ⟶ ℕ \\ ⟨i,j⟩ \mapsto \dfrac{(i+j)(i+j+1)}{2} +j \end{cases}\]

Bijection de $ℙ_{fin}(ℕ) ⟶ ℕ$

\[\begin{cases} ℙ_{fin}(ℕ) ⟶ ℕ \\ \lbrace n_1, ⋯, n_k \rbrace \mapsto \sum\limits_{ i } 2^{n_i} \end{cases}\]

On aimerait bien :

  • $i : ℙ_𝜔 ⟶ [ℙ_𝜔 ⟶ ℙ_𝜔]$
  • $r : [ℙ_𝜔 ⟶ ℙ_𝜔] ⟶ ℙ_𝜔$

Lemme : Si $f∈[ℙ_𝜔 ⟶ ℙ_𝜔]$, $f$ est déterminée de façon unique par ses valeurs sur $ℙ_{fin}𝜔$

Dém :

\[E = \bigcup_{A∈ℙ_{fin}(E)} A\]

Comme $f$ est continue :

\[f(E) = \bigcup_{A∈ℙ_{fin}(E)} f(A)\]

Donc :

\[r(f)≝ \lbrace \Big\langle ⟨A⟩, n \Big\rangle \mid A∈ℙ_{fin}𝜔, n∈f(A) \rbrace\] \[i(E) ≝ E' \mapsto \bigcup_{A∈ℙ_{fin}(E')} \lbrace n \mid \Big\langle ⟨A⟩, n \Big\rangle ∈ E \rbrace\]

Donc maintenant :

$⟦u⟧𝜌 ∈ ℙ_𝜔$

  • $⟦x⟧𝜌 = 𝜌(x)$
  • $⟦uv⟧𝜌 = i(⟦u⟧𝜌)(⟦v⟧𝜌)$
  • $⟦𝜆x. u⟧𝜌 = r(V \mapsto ⟦u⟧(𝜌[x \mapsto V]))$

Mais il y a 2 problèmes :

  1. il faut que $⟦u⟧𝜌$ est continue en $𝜌$
  2. $i$ est continue
  3. $i(⟦u⟧𝜌)$ est continue

Tout marche car dans les CPO : une fonction de deux variables est continues en chacune des variables ssi elle est continue conjointement

Rappel : Si $f: X ⟶ X$ est continue d’un DCPO pointé (avec un $\bot$), alors $f$ a un plus petit point fixe $lfp(x) ≝ \sup_{n∈ℕ} f^n(\bot)$

Ex : vérifier que la sémantique de n’importe quel combinateur de point fixes $Y$ dans $ℙ_𝜔$ : $⟦Yu⟧𝜌$ vérifie :

  • $⟦Yu⟧𝜌 = i(⟦u⟧𝜌)(⟦Yu⟧𝜌)$
  • $⟦Yu⟧𝜌 = lfp\Big(i(⟦u⟧𝜌)\Big)$

Ex : dans $ℙ_𝜔$

\[⟦𝜆x, y. xy⟧ ≠ ⟦𝜆x. x⟧\]

donc pas de compatibilité avec la $𝜂$-réduction

mais le modèle de Scott $D_∞$ lui est compatible avec la $𝜂$-réduction !

Comment on construit $D_∞$ ?

Soit $D_0$ un DCPO pointé.

\[D_0 ⟶ D_1 ≝ [D_0 ⟶ D_0] ⟶ D_2 ≝ [D_1 ⟶ D_1]\]

avec

  • $i_0 : D_0 ⟶ D_1, d_0 \mapsto (\bullet \mapsto d_0)$
  • $r_0 : D_1 ⟶ D_0, d_1 \mapsto d_1(\bot)$

Puis :

  • $i_1 ≝ d_1 \mapsto i_0 \circ d_1 \circ r_0$
  • $r_1 ≝ d_2 \mapsto r_0 \circ d_2 \circ i_0$

Arbres de Böhm

Leave a comment