Cours 13: Théorème de Friedman: correction

Nouveau professeur pour cette seconde partie : Michele Pagani

Rappels

En $λ$-calcul simplement typé:

Types:
\[A, B \; ≝ \; σ \mid A → B\]
Termes:
\[M \; ≝ \; x \mid λx^A. M \mid MN\]
\[\underbrace{x_1: A_1, ⋯, x_n: A_n}_{Γ} ⊢ M: B\] \[\cfrac{x_1: A_1, ⋯, x_n: A_n}{x_i:A_i} \\ \cfrac{Γ, x:A ⊢ M:B}{Γ ⊢ λx^A.M:A → B}\\ \cfrac{Γ ⊢ M:A → B \qquad Γ ⊢ N:A}{Γ ⊢ (MN): B}\\\]

Sémantique dénotationnelle dans $Set$:

  • $⟦σ⟧_X = X ∈ Set$
  • $⟦A → B⟧_χ = ⟦B⟧_X^{⟦A⟧_X}$
  • $⟦x_1:A_1, ⋯, x_n: A_n ⊢ M:B⟧_X = ⟦x_1:A_1⟧_X × ⋯ × ⟦x_n: A_n⟧_X ⟶ ⟦B⟧_X$

Exponentielle dans une CCC:

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

Pour le $λ$-calcul simplement typé: on a besoin d’un objet réflexif dans une CCC

\[D \vartriangleright D ⇒ D\]

i.e.

tout élément de $D ⇒ D$ est aussi un élément de $D$.

NB: $Set$ n’a pas d’objet réflexif, ce qui a poussé Dana Scott à définir ses domaines de Scott.

Modèles du $λ$-calcul

  • $Set$ pour le simplement typé
  • $Scott$ (CPOs et fonction Scott-continues): pour le $λ$-calcul typé et non typé
  • $Stab$ (espaces cohérents et fonctions stables)

NB: sématnique dénotationnelle: pourquoi?

  1. Pour étudier la théorie équationnelle entre les termes:

    \[M \sim N ⟺ ⟦Γ ⊢ M⟧ = ⟦Γ ⊢ N⟧\]

    et parler “d’équivalences de programmes”, et de leurs propriétés partagées

  2. on peut introduire de nouvelles primitives dans le calcul:

    \[A ⇒ B \; = \; !A \multimap B\]

    Exemples:

    • primitives probabilistes
    • computation quantique ⟶ on a besoin de la linéarité (non duplication, etc…)

  3. Compilation dans le langage haut-niveau vers un langage bas-niveau: Ex: Categorical Abstract Machine (a donné naissance à CamL) basée sur les catégories cartésiennes closes.

    Ex:

    \[⟦(λx.x)y⟧ = ev \circ ⟨Λ(π_2^2), π_2^2⟩\]

NB: dans cette seconde partie du cours, on se concentrera surtout sur 1 et 2.

Théorème de Friedman (1973)

Chap. 4 de AMADIO-CURIEN: “Domains and $λ$-calculi” ⟶ théorème 4.5.8

Th (Friedman, 1973): Let $X$ be an infinite set and $⟦_⟧_X$ be the interpretation of the simply typed $λ$-calculus in the CCC Set associating $X$ with the ground type. For any terms $Γ ⊢ M:A$ and $Γ ⊢ N:A$, we have:

\[M =_{βη} N ⟺ ⟦M⟧_X = ⟦N⟧_X\]

NB:

  • on peut alors profiter du fait que travailler avec $⟦M⟧_X$ et $⟦N⟧_X$ est beaucoup plus agréable !

  • pas vrai pour n’importe quelle CCC

$βη$-equivalence

Congruence:
  • symetric
  • reflexive
  • transitive

  • and:

    \[\cfrac{M =_{βη} N}{λx. M =_{βη} λx. N} \\ \, \\ \cfrac{M =_{βη} N \qquad P =_{βη} Q}{MP =_{βη} NQ}\]
$=_{βη}$:

is the smallest congruence over $Λ$ s.t.

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

Definition de $⟦_⟧_X$

\[⟦x_1:A_1, ⋯, x_n: A_n ⊢ M:B⟧ ∈ ⟦x_1:A_1⟧ × ⋯ × ⟦x_n: A_n⟧ ⟶ ⟦B⟧\]

  • Variables ⟶ projections:

    \[⟦x_1: A_1, ⋯, x_n: A_n ⊢ x_i: A_i⟧ = π_i\]

  • $λ$-abstractions ⟶ use the adjonction:

    \[⟦Γ ⊢ λx^A. M: A → B⟧ = Λ(⟦Γ, x:A ⊢ M:B⟧)\\ = \vec{g} ⟼ (a ⟼ ⟦M⟧(\vec{g}, a))\]

  • Application ⟶ pairing:

    \[⟦Γ ⊢ MN: B⟧ = ev \circ ⟨⟦Γ ⊢ M: A → B⟧, ⟦Γ ⊢ N: A⟧⟩\\ = \vec{g} ⟼ ⟦M⟧(\vec{g}, ⟦N⟧(\vec{g}))\]

NB: on a fait un effacement dans le premier point, une duplication dans le dernier point.

Démonstration du théorème de Friedman

\[M =_{βη} N \overset{\text{correction}}{⟹} ⟦M⟧_X = ⟦N⟧_X\] \[M =_{βη} N \overset{\text{complétude}}{⟸} ⟦M⟧_X = ⟦N⟧_X\]

Correction

\[M =_{βη} N \overset{\text{correction}}{⟹} ⟦M⟧_X = ⟦N⟧_X\]

par induction sur la taille de la dérivation de $=_{βη}$

Trois actions possibles :

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

Le plus délicat: premier cas: $⟦(λx.M)N⟧ = ⟦M \lbrace N/x \rbrace⟧$

Substitution lemma: Let $Γ, x:A ⊢ M:B$ and $Γ ⊢ N:A$, then

\[⟦Γ ⊢ M \lbrace N/x \rbrace: B⟧ = \vec{g} ⟼ ⟦M⟧(\vec{g}, ⟦N⟧(\vec{g}))\]

Proof: By induction on $M$.

Attention: il y a une difficulté pour $⟦λx.Mx⟧ = ⟦M⟧$ (contextes et types omis): on a besoin de montrer que $(a ⟼ ⟦Γ, x:A ⊢ M:B⟧(\vec{g}, a) a) = (a ⟼ ⟦Γ ⊢ M:A→B⟧(\vec{g}, a))$, via

Weakening lemma: si $x ∉ fv(M)$:

\[⟦Γ, x:A ⊢ M:B⟧(\vec{g}, a) = ⟦Γ ⊢ M:B⟧(\vec{g})\]

Complétude

\[M =_{βη} N \overset{\text{complétude}}{⟸} ⟦M⟧_X = ⟦N⟧_X\]

Preuve de Friedman: définit

  • un modèle syntaxique $S$

  • une famille de relations $\lbrace R^A\rbrace_{A ∈ Types}$

    • $R^A ⊆ ⟦A⟧^{Set}_X × ⟦A⟧^S$
    • pour tout $M$: $⟦⊢ M:A⟧^{Set} R^A ⟦⊢M:A⟧^S$

    • $R^A$ est fonctionnelle:

      \[∀d ∈ ⟦A⟧^{Set}_X, ⟦N⟧, ⟦N'⟧ ∈ ⟦A⟧^S\\ d R^A ⟦N⟧^S \text{ et } d R^A ⟦N⟧^S ⟹ ⟦N⟧^S = ⟦N'⟧^S\]
    • \[\cfrac{⟦M⟧^S = ⟦N⟧^S}{M =_{βη} N}\]

NB: $R^A$ est un cas particulier de relation logique (logical relation) ⟶ ex: les candidats de réductibilité (on s’intéressait aux termes fortement normalisables au lieu de la relation de $βη$-équivalence) étaient des cas particuliers de relation logique unaire.

Leave a comment