Cours 14: Théorème de Friedman: complétude

Friedman:

\[∀ Γ ⊢ M, N: A, ∀ X \text{ infinite set},\\ M =_{βη} N ⟺ ⟦M⟧_X = ⟦N⟧_X\]

Completeness: $⟸$

Extensional applicative structure

Extensional applicative structure:
\[ℳ ≝ \lbrace \underbrace{S^A}_{\text{sets}} \rbrace_{A ∈ Types} \text{ s.t. } S^{A ⇒ B} ≃ F ⊆ Set(S^A, S^B)\]

Sémantique “concrète” dans $Set$ (on ne se place plus dans le cas général d’une CCC):

  • \[⟦\_⟧_ℳ: \overbrace{Terms_{x_1:A_1, ⋯, x_n:A_n ⊢ B}}^{\text{termes de type } B \text{ dans le contexte donné}} \leadsto S^{A_1} × ⋯ × S^{A_n} → S^B\]
  • \[⟦x_1:A_1, ⋯, x_n:A_n ⊢ x_i:A_i⟧ ≝ \vec{a} ⟼ a_i\]
  • \[⟦Γ ⊢ λx.M: A → B⟧_{ℳ} ≝ \vec{g} ⟼ (a ⟼ ⟦Γ, x:A ⊢ M:B⟧ \, \vec{g} \, a)\]
  • \[⟦Γ ⊢ MN: B⟧_{ℳ} ≝ \vec{g} ⟼ ⟦Γ ⊢ M: A → B⟧ \, \vec{g} \, (⟦N⟧ \, \vec{g})\]

Modèle syntaxique

Notations: $⟦\_⟧_λ$ pour la syntaxe, $⟦\_⟧_{Set}$ dans $Set$

  • \[S^A ≝ \lbrace M \mid ∃ Γ, Γ ⊢ M:A \rbrace / =_{βη}\]
  • \[[M] ∈ S^{A ⇒ B}, [N] ∈ S^A, \; \underbrace{[M]}_{Γ ⊢ A ⇒ B} \cdot \underbrace{[N]}_{Δ ⊢ A} ≝ \underbrace{[MN]}_{Γ \, ∪ \, Δ ⊢ B} ∈ S^B\]
    • bien défini:
      • typage à la Church ⟶ on n’a pas une même variable avec deux types différents, donc on peut prendre l’union
      • par définition de $=_{βη}$, ne dépend pas du représentant choisi
  • \[⟦x_1:A_1, ⋯, x_n:A_n ⊢ M:B⟧_λ: ([N_1], ⋯, [N_n]) ⟼ [M \lbrace N_1/x_1, ⋯, N_n/x_n \rbrace]\]
  • \[⟦Γ ⊢ λy.M: A → B⟧_λ \, ([\vec{N_i}]) = [Γ ⊢ λy. M \lbrace \vec{N_i}/\vec{x_i} \rbrace]\]
    • \[[P] ∈ S^A ⟹ [Γ ⊢ λy. M \lbrace \vec{N_i}/\vec{x_i} \rbrace] \cdot [P] = [Γ ⊢ (λy. M \lbrace \vec{N_i}/\vec{x_i} \rbrace) P]\\ = [Γ ⊢ (λy. M) P \lbrace \vec{N_i}/\vec{x_i} \rbrace] = ⟦Γ ⊢ λy. M P⟧ \, (\vec{N_i}) \\ = ⟦Γ ⊢ λy. M⟧ \, (\vec{N_i}) \cdot [P]\]

Relation logique

\[ℛ^A ⊆ ⟦A⟧_{Set} × S^A\]
  • \[ℛ^o \, = \, ?\]
  • \[f \; ℛ^{A ⇒ B} [M] \, ⟺ \, ∀ a ℛ^A [N], f(a) \, ℛ^B \, \underbrace{[M]\cdot[N]}_{ = \, [MN]}\]

NB: L’idée est très générale: on définit la relation sur les types de base (selon ce qu’on veut démontrer), puis: la relation “préserve l’application fonctionnelle”: deux fonctions sont en relation ssi pour tous les arguments en relation, les images restent en relation.

NB 2: Candidats de réductibilité ⟶ relation unaire

Lemme 1: $∀x_1:A_1, ⋯, x_n:A_n ⊢ M:B, ∀ a_i \, ℛ^{A_i} \, [N_i] (i ≤ n)$:

\[⟦M⟧_{Set}(a_1, ⋯, a_n) \, ℛ^B \, \underbrace{⟦M⟧_λ \, ([N_1], ⋯, [N_n])}_{= \, [M \lbrace N_1/x_1, ⋯, N_n/x_n \rbrace]}\]

Lemme de surjectivité:

\[∀ \, [N] ∈ S^A, ∃ a ∈ ⟦A⟧_{Set}; \quad a \, ℛ^A \, [N]\]

NB: $_ \; ℛ^A: X ⟶ ℳ$ est surjective

Lemme 2 de fonctionnalité:

\[∀ a ∈ ⟦A⟧_{Set}, ∀ [M], [M'] ∈ S^A,\\ a \, ℛ^A \, [M] \text{ et } a \, ℛ^A \, [M'] ⟹ [M] = [M']\]

NB: $_ \; ℛ^A: X ⟶ ℳ$ est une fonction partielle (on a besoin du lemme précédent pour montrer celui-là).

Comment définir $ℛ^o$?

C’est ici que l’hypothèse “$X$ infini” est cruciale:

Soit $i: S^o \hookrightarrow X$ une injection. On pose

\[ℛ^o ≝ i^{-1} ⊆ X × S^o\]

Des lemmes vers le résultat

Cas où $M$ et $N$ sont clos

Si $M, N$ sont clos et $⟦M⟧{Set} = ⟦N⟧{Set}$, alors

\[M =_{βη} N\]

Par le lemme 1 et par clôture:

  • $⟦M⟧_{Set} \, ℛ^B \, ⟦M⟧_λ$

  • $⟦N⟧_{Set} \, ℛ^B \, ⟦N⟧_λ$

Par le lemme de fonctionnalité:

\[⟦M⟧_λ = ⟦N⟧_λ\]

d’où:

\[[M] = [N] \text{ , i.e. } M =_{βη} N\]

Preuve des deux lemmes

$∀A$:

  1. \[a \; ℛ^A \; [M], [M'] ⟹ [M] = [M']\]
  2. \[∀[M], ∃ a; \quad a \; ℛ^A \; [M]\]

Proof:

By induction on $A$:

  • $A = σ$: trivial

  • $A = B ⇒ C$:

    • Let $a \; ℛ^{B ⇒ C} \; [M], [M’]$.

      Take $x^B$ a fresh variable. By 2 on $B$:

      \[∃ b \; ℛ^B \; [x]\]

      So

      \[f(b)\; ℛ^C \; [Mx], [M'x]\]

      By 1 on $C$:

      \[[Mx] = [M'x] \text{ , i.e } Mx =_{βη} M'x\]

      i.e.

      \[\underbrace{λx. Mx}_{=_η \, M} =_{βη} \underbrace{λx. M'x}_{=_η \, M'}\]

      because $x ∈ fv(M) ∪ fv(M’)$

    • Let $[M] ∈ S^{B ⇒ C}$.

      Fix $c_0 ∈ ⟦C⟧{Set}$. Let $b ∈ ⟦B⟧{Set}$.

      Define

      \[f(b) = \begin{cases} c &&\text{ if } ∃[N]; b \; ℛ^B \; [N], \text{ so that } ∃c \; ℛ^C \; [MN] \text{ by 2 on } C \\ c_0 &&\text{ else} \end{cases}\]

      Let’s show that $f \; ℛ^{B ⇒ C} \; M$.

      If $b’ \; ℛ^B \; [N’]$: by 1 on $B$, we have only $[N’]$ in relation with $b’$. Therefore: $f(b’) \; ℛ^C \; [MN’]$.

NB: these two properties are “dual” in a sense, since we use 2 in a positive position to prove 1 by induction (and vice versa).

Preuve du lemme 1

Lemme 1: $∀x_1:A_1, ⋯, x_n:A_n ⊢ M:B, ∀ a_i \, ℛ^{A_i} \, [N_i] (i ≤ n)$:

\[⟦M⟧_{Set}(a_1, ⋯, a_n) \, ℛ^B \, \underbrace{⟦M⟧_λ \, ([N_1], ⋯, [N_n])}_{= \, [M \lbrace N_1/x_1, ⋯, N_n/x_n \rbrace]}\]

Preuve:

Cas de base: $Γ, x:A ⊢ x:A$

$g_i \; ℛ^{A_i} \; [N_i], \quad a \; ℛ^A \; [N]$.

\[\underbrace{⟦x⟧_{Set} \; (\vec{g}, a)}_{ = \, a} \; ℛ^A \; \underbrace{⟦x⟧_λ \; ([\vec{N_i}], [N])}_{= \, N}\]

$Γ ⊢ λx^A. M: A ⇒ B$

$g_i \; ℛ^{A_i} \; [N_i], \quad ⟦λx. M⟧_{Set} \, \vec{g} \; ℛ^{A ⇒ B} \; [M \lbrace \vec{N_i}/x_i \rbrace]$.

Let $a \; ℛ^A \; [P]$,

\[\underbrace{(⟦λx. M⟧_{Set} \, \vec{g}) \, a}_{= ⟦M⟧_{Set} \, (\vec{g}, a)} \; ℛ^B \; \underbrace{[M \lbrace \vec{N_i}/x_i \rbrace \, P]}_{= MP \lbrace \vec{N_i}/x_i \rbrace}\]

then, as $Γ, x:A ⊢ M:B$: we conclude by IH.

$Γ ⊢ MN: B$

then $Γ ⊢ M: A ⇒ B, \; Γ ⊢ N:A$

$g_i \; ℛ^{A_i} \; [N_i]$, by IH.

\[⟦M⟧_{Set} \, \vec{g_i} \; ℛ^{A ⇒ B} \; [M \lbrace \vec{N_i}/x_i \rbrace]\\ ⟦N⟧_{Set} \, \vec{g_i} \; ℛ^{A} \; [N \lbrace \vec{N_i}/x_i \rbrace]\]

and

\[\underbrace{⟦M⟧_{Set} \, \vec{g_i} \, (⟦N⟧_{Set} \, \vec{g_i})}_{⟦MN⟧_{Set} \, \vec{g_i}} \; ℛ^B \; \underbrace{[M \lbrace \_ \rbrace N \lbrace \_ \rbrace]}_{= [MN \lbrace \_ \rbrace]}\]

Leave a comment