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