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))$