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.

Leave a Comment