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

Leave a comment