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.