TD1 : 𝛽-réduction et 𝛼-renommage

Énoncé

EX 1

1.

  1. $(𝜆x.𝜆y.x)x$
  2. $𝜆x.x$
  3. $(𝜆x.𝜆x.x)x$
  4. $(𝜆x.𝜆y.y)x$
  5. $(𝜆x.𝜆y.y)(𝜆x.x)$
3 ⟶^𝛼 4 \\ 3 ⟶^𝛽 2 \\ 4 ⟶^𝛽 𝜆y.y ⟶^𝛼 2 \\ 5 ⟶^𝛽 𝜆y.y ⟶^𝛼 2
  digraph {
    rankdir=TB;
    A[label="(𝜆x.𝜆y.y)(𝜆x.x)"];
    B[label="(𝜆y.y)"];
    C[label="(𝜆x.x)"];
    D[label="(𝜆x.𝜆y.y)x"];
    A -> B;
    C -> B;
    D -> B;
  }
  digraph {
    rankdir=TB;
    A[label="(𝜆x.𝜆y.x)x"];
    B[label="(𝜆z.𝜆y.z)x"];
    C[label="(𝜆y.x)"];
    A -> B;
    B -> C;
  }

EX 2

1.

(𝜆x.𝜆y M x) = (𝜆x.𝜆y N y)

Montrons que :

  • $M = 𝜆z.u$
  • $N = 𝜆z.v$ où $u$ et $v$ sont des termes clos.

Ces termes $M$ et $N$ conviennent clairement, et réciproquement, la seule variable qu’il peut y avoir dans $u$ est $z$.

Si $u$ contenait $z$ :

(𝜆x.𝜆y.u[z:=x]) = (𝜆x.𝜆y.v[z:=y])

Donc, comme $u$ et $v$ sont $𝛽$-normaux, l’égalité précédente est une égalité syntaxique (modulo $𝛼$-renommage), d’où :

u[z:=x] = v[z:=y]

Or : $fv(u[z:=x]) = fv(v[z:=y])$

Or : $x$ appartient au premier ensemble, $y$ au deuxième, et comme ces ensembles sont de cardinal 1 ($z$ était la seule variable libre de $u$), $x=y$, ce qui n’est pas.

2.

(𝜆z.𝜆s. s (M s z)) = (𝜆z.𝜆s M s (s z))
M_0 ≝ 𝜆x.𝜆y.y \\ M_1 ≝ 𝜆x.𝜆y.(x y) \\ M_2 ≝ 𝜆x.𝜆y.x (x y)

etc…

EX 3

T ≝ 𝜆x.𝜆y.x \\ F = 𝜆x.𝜆y.y
AND = 𝜆b_1 𝜆b_2 b_2 b_1 F \\ OR = 𝜆b_1 𝜆b_2 b_2 T b_1 \\ NOT = 𝜆b 𝜆x 𝜆y b y x

EX 4

$⟶ ⊊ ⟹$ :

Par récurrence (le cas de base étant la réflexivité).

Inclusion stricte :

((𝜆x.x)y)((𝜆x.x)y) ⟹ yy

mais

((𝜆x.x)y)((𝜆x.x)y) \not ⟶ yy

$⟹ ⊊ ⟶^\ast$ :

Par récurrence sur la structure des $𝜆$-termes : on $𝛽$-réduit les $𝜆$-termes l’un après l’autre.

Inclusion stricte :

((𝜆x.x)(𝜆x.x))y ⟶^\ast y

mais :

((𝜆x.x)(𝜆x.x))y \not ⟹ y

2.

Leave a comment