TD2 : graphes de réduction

Énoncé

EX 1

1.

  digraph {
    𝛺 -> 𝛺;
  }

\[𝛺 = 𝛿𝛿 = (𝜆x.xx)(𝜆x.xx)\]

2.

  digraph {
    A -> B;
    B -> B;
  }

\[((𝜆x.x)𝛿)𝛿\]

3.

  digraph {
    A -> A;
    A -> B;
  }

\[(𝜆x.y)𝛺\]

4.

  digraph {
    B -> A;
    B -> C;
    C -> B;
    C -> D;
  }

Impossible, par confluence du $𝜆$-calcul.

5.

\[(𝜆y.y)(((𝜆x.x)𝛿)𝛿)\] \[(𝜆x.x(xx))𝛿\]

6.

\[(𝜆x.xxx)(𝜆x.xxx)\]

7.

\[𝜁 ≝ 𝜆x,y.yxx \\ (𝜁𝜁)𝜁\] \[𝜔_3 ≝ 𝜆x.xxx \\ 𝜔_3 (𝜆y.𝜔_3)\]

8.

\[𝜁 = 𝜆x,y.(𝛺)yxx\]

EX 2

2.

Mq

  digraph {
    rankdir=TB;
    t -> {u,v};
    u -> w[style="dashed"];
    v -> w[style="dashed"];
  }

On fait une induction.

Quelle est la dernière règle $t ⟹ u$ :

• Si c’est refl : fini

• Si c’est abs

---

EX 3

1.

\[𝜋_1 ≝ 𝜆f. f T \\ 𝜋_2 ≝ 𝜆f. f F\] \[pair = 𝜆x,y,f. fxy\]

---

L’égalité n’est pas vraie pour tout $M$ :

avec $M ≝ 𝛿 = 𝜆x.xx$ :

\[pair (𝜋_1 𝛿) (𝜋_2 𝛿) = pair (𝛿 T) (𝛿 F) = pair (T T) (F F) = 𝜆f.f(TT)(FF)\]

2.

\[0 = 𝜆f, x. x \\ + = 𝜆m, n, f, x.m f (n f x) \\ × = 𝜆m, n, f. m (n f) \\ succ = 𝜆n, f, x. n f (f x)\]

3.

\[𝜆n. n (𝜆x. F) T\]

4.

À chaque entier $n$, on fait correspondre la paire

\[(n-1, n)\]

---

\[pred = 𝜆n. 𝜋_1 \Bigg(n \Big(𝜆p. pair (𝜋_2 p) (s(𝜋_2 p))\Big) (pair 0 0)\Bigg)\]

5.

x_0 :: x_1 :: x_2 :: []

correspond à

\[𝜆 f a. f(f(f(a x_2) x_1) x_0)\]

⟶ foldright

\[nil = 𝜆f, a. a \\ cons = 𝜆e,l,f,a. f(l a f) e \\ if nil = 𝜆l. l (𝜆a, b. F) T \\ app = 𝜆n,s,f,a. n f (s f a) \\ rev = 𝜆l. l (𝜆a,e. app \, a \, (cons \, e \, nil)) \, nil\]