TD10 : types de données en $𝜆$-calcul

Énoncé

1. Un peu de $𝜆$-calcul pur

1.

Si $u$ se $𝜂$-réduit en $u’$, alors $u$ et $u’$ ont les mêmes variables libres.

\[u ≝ 𝜆x. u' x ⟶_𝜂 u'\]

avec $x∉fv(u’)$

\[fv(u) = fv(u' x)\backslash \lbrace x \rbrace = (fv(u') ∪ fv(x))\backslash \lbrace x \rbrace \\ = fv(u') \backslash \lbrace x \rbrace \\ = fv(u')\]

2 / 3.

Faites dans le DM.

4.

On le vérifie aisément.

\[\cfrac{}{𝛤, x: F \vdash x : F}(Ax) \\ \cfrac{𝛤, x:F \vdash u: G}{𝛤 \vdash 𝜆x. u : F⟹G}(⟹I) \\ \cfrac{𝛤 \vdash u: F ⟹ G \quad 𝛤 \vdash v : F}{𝛤 \vdash uv : G}(⟹E) \\ \cfrac{𝛤 \vdash u: F}{𝛤 \vdash u : ∀𝛼 \cdot F}(∀ I) \text{ où } 𝛼 \text{ non libre dans } 𝛤 \\ \cfrac{𝛤 \vdash u: ∀𝛼 \cdot F}{𝛤 \vdash u : F[𝛼 := G]}(∀ E)\]

5.

Montrons que

pour toute dérivation de de jugement $x_1 : F_1, ⋯ , x_n : F_n \vdash u : F$ en système $F$, pour tout contexte saturé $C$, pour tous $v_1 ∈ R_{F_1}^C, ⋯, v_n ∈ R_{F_n}^C, u[x_1 := v_1, \ldots, x_n := v_n]$ est dans $R_F^C$.

Par induction sur la dérivation du jugement, si la dernière règle est :

• \[\cfrac{}{x_1 : F_1, ⋯ , x_n : F_n \vdash u : F}(Ax)\]

  c’est immédiat puisque $u$ est l’un des $x_i$.

• \[\cfrac{x_1 : F_1, ⋯ , x_n : F_n, x:F \vdash u: G}{x_1 : F_1, ⋯ , x_n : F_n \vdash 𝜆x. u : F⟹G}(⟹I)\]

  Pour tous $v_1 ∈ R_{F_1}^C, ⋯, v_n ∈ R_{F_n}^C$ : $𝜆x. u[x_1 := v_1, \ldots, x_n := v_n]$ est dans $R_F^C$ par hypothèse d’induction (avec affaiblissement).

• \[\cfrac{x_1 : F_1, ⋯ , x_n : F_n \vdash u: F ⟹ G \quad x_1 : F_1, ⋯ , x_n : F_n \vdash v : F}{x_1 : F_1, ⋯ , x_n : F_n \vdash uv : G}(⟹E)\]

  on conclut encore immédiatement par hypothèse d’induction.

• \[\cfrac{x_1 : F_1, ⋯ , x_n : F_n \vdash u: F}{x_1 : F_1, ⋯ , x_n : F_n \vdash u : ∀𝛼 \cdot F}(∀ I) \text{ où } 𝛼 \text{ non libre dans } x_1 : F_1, ⋯ , x_n : F_n\]

  on conclut en utilisant l’hypothèse d’induction avec le contexte $C[𝛼 \mapsto R_G^C]$

• \[\cfrac{x_1 : F_1, ⋯ , x_n : F_n \vdash u: ∀𝛼 \cdot F}{x_1 : F_1, ⋯ , x_n : F_n \vdash u : F[𝛼 := G]}(∀ E)\]

  idem au point précédent, cette fois avec le type $F[𝛼 := G]$

6.

On utilise la question 1 et le point $(iii)$ de l’énoncé introductif.

7.