TD11 : $HA_2$ et Ackermann

Énoncé

EX 1

\cfrac{𝛤 \vdash u : P[i:=t]}{𝛤 \vdash ⟨t, u⟩ : ∃i. \, P}
\cfrac{𝛤 \vdash u : ∃i. P \qquad }{𝛤 \vdash ⟨t, u⟩ : ∃i. \, P}

1.

a).

v_0 ≝ 𝜆^1 j. ⟨s(j), 𝜆^2A. 𝜆 x,y,z. xj ⟩

b).

u_0 = \textsf{ let } ⟨k, a⟩ = h_i s(0) \textsf{ in } ⟨k, 𝜆^2 A. 𝜆x, y, z. y i k (a A x y z)⟩

c).

u_s ≝ 𝜆^1 j, p. \textsf{ let } ⟨k, a⟩ = p \textsf{ in let } ⟨k', a'⟩_{ack(i, k, k')} = h_i k
⟨k', 𝜆^2 A. 𝜆 x, y, z. z i j k k' (a A x y z ) (a' A x y z)⟩

d).

v_s ≝ 𝜆 i. 𝜆 h_i. 𝜆 j. R u_0 u_s j

e).

𝜆 i. R v_0 v_s i

2.

nat ≝ N ⟹ (N⟹N) ⟹ N

a).

E(𝜆i. u) = 𝜆x_i. E(u)

On veut $u⟶v$ donc $E(u)⟶ E(v)$

EX 2. $𝜆𝜎$ simule $𝜆$

1.

\uparrow \circ \Uparrow (S) = \, \uparrow \circ (1 \cdot (S \circ \uparrow)) ⟶ (S \circ \uparrow)

2.

Par réc sur $i$ :

  • Pour $i=1$ : Par réc sur $q≥0$ :

    • $1[\Uparrow^0 (S)] =_𝜎 1[S]$
    • (q+1) [\Uparrow^q (S)] =_𝜎 ((q-1)+1) [1 \cdot (\Uparrow^{q-1} (S) \circ \uparrow)] \\ =_𝜎 (q-1) [\uparrow] [1 \cdot (\Uparrow^{q-1} (S) \circ \uparrow)] =_𝜎 (q-1) [\Uparrow^{q-1} (S) \circ \uparrow] \\ \overset{HR}{=_𝜎} [S \circ \uparrow^q]
  • Pour $i≥2$ : Par réc sur $q≥0$ :

    • $i[\Uparrow^0 (S)] =_𝜎 1[S]$
    • (q+i) [\Uparrow^q (S)] =_𝜎 ((q-1)+i+1) [1 \cdot (\Uparrow^{q-1} (S) \circ \uparrow)] \\ =_𝜎 (q-1 + i) [\uparrow] [1 \cdot (\Uparrow^{q-1} (S) \circ \uparrow)] =_𝜎 (q-1+i) [\Uparrow^{q-1} (S) \circ \uparrow] \\ \overset{HR}{=_𝜎} i[S \circ \uparrow^q]

3.

Par réc sur $1≤i≤q$ :

  • Pour $i=1$ :

    1[\Uparrow^q (S)] =_𝜎 1[1\cdot (\Uparrow^{q-1} (S) \circ \uparrow)] \\ =_𝜎 1
  • Pour $1≤i<q$ :

    i[\Uparrow^q (S)] = (i-1)[\uparrow][1\cdot (\Uparrow^q (S) \circ \uparrow)] = (i-1)[\Uparrow^q (S) \circ \uparrow][\uparrow] \\ = (i-1)[\uparrow] = i

4.

Par induction sur $v$ :

  • $x^\ast (l) = i$ où $i = \min \lbrace j \mid l(j) = x \rbrace$

  • $(uv)^\ast (l) = u^\ast (l) v^\ast (l)$

  • $(𝜆x.u)^\ast (l) = 𝜆(u^\ast (x::l))$

Leave a comment