TD3 : stratégies et combinateurs

Énoncé

EX 1

1.

let fact n = if n>0 then n * fact (n-1) else 1

let F f n = if n>0 then n * f (n-1) else 1
\[F f ≝ 𝜆f. n \, (𝜆x. \, n × f (Pred \, n)) \, 1 \\ Succ \, n ≝ 𝜆n f x. f(n f x) \\ Pred \, n ≝ 𝜆n. 𝜋_1 \Big( n \, \big(𝜆c. ⟨𝜋_2 c, Succ \, 𝜋_2 c⟩\big) \, ⟨0,0⟩ \Big) \\ n × m ≝ 𝜆n, m. n (m f) \\ fact ≝ Y F \\ = 𝜆f. (𝜆x. f (xx)) (𝜆x. f (xx)) \Bigg( 𝜆f. n \, \Big(𝜆x. \, n × f \Big(𝜋_1 \bigg( n \, \big(𝜆c. ⟨𝜋_2 c, Succ \, 𝜋_2 c⟩\big) \, ⟨0,0⟩ \bigg) \Big)\Big) \, 1 \Bigg)\]

2.

\[\begin{align*} fact & \vartriangleright Y F &&\text{(1)} \\ & \vartriangleright F (\underbrace{Y F}) &&\text{(1)} \\ & \vartriangleright F (\underbrace{F (Y F)}) &&\text{(3)+(1)} \\ \end{align*}\]

Et on boucle sans s’arrêter.

Solution ⟶ faire une $𝜂$-expansion pour bloquer l’évaluation de $fact$

⟹ on remplace $fact$ par $𝜆x. fact x$

3.

\[\begin{align*} fact \, 0 & \vartriangleright Y F \, 0 &&\text{(1)+(2)} \\ & \vartriangleright (F (Y F)) \, 0 &&\text{(2)+(1)} \\ & \vartriangleright (F ( F (F (Y F)))) \, 0 &&\text{(2)+(3)+(1)} \\ \end{align*}\]

Pour résoudre ce problème, on redéfinit

\[Y ≝ 𝜆f. (𝜆x f(𝜆y.x x y)) (𝜆x f(𝜆y.x x y))\]

EX 2

1.

\[I \, M ≝ SK K M \\ ⟶ (K M) (K M) \\ ⟶ K M (K M) \\ ⟶ M\]

2.

\[[K]_𝒞 = 𝜆xy.x \\ [S]_𝒞 = 𝜆x y z. (xz) (yz)\]

3.

  • $𝜆^\ast (x, y) = Ky$ si $x≠y$
  • $𝜆^\ast (x, x) = I$
  • $𝜆^\ast (x, S) = KS$
  • $𝜆^\ast (x, K) = KK$

  • $𝜆^\ast (x, MN) = S \, 𝜆^\ast (x, M) \, 𝜆^\ast (x, N)$

    • en effet : \(S \, 𝜆^\ast (x, M) \, 𝜆^\ast (x, N) P \\ ⟶ (𝜆^\ast (x, M) P) \, (𝜆^\ast (x, N) P) \\ ⟶M[x := P]N[x := P] \\ ⟶ MN[x := P]\)

4.

\[𝜆^\ast (x, 𝜆^\ast (y, x)) = 𝜆^\ast (x, Kx)$ \\ = S (KK) I ≠ K\] \[∀N, S (KK) I N = (K K N) (I N) \\ = K N\]

5.

  • $[x]_𝜆 = x$
  • $[MN]_𝜆 = [M]_𝜆 [N]_𝜆$
  • $[𝜆x.M]_𝜆 = 𝜆^\ast (x, [M]_𝜆)$
\[u \vartriangleright v\]

⟶ $u’ v’ \vartriangleright u’’ v’$

  • $[u’] ⟶ [u’’]$
  • $[u’ v’] ⟶ [u’’ v’]$

⟶ $u’ v’ \vartriangleright u’ v’’$

si $u’∈V$

⟶ $(𝜆x. u’) v’ \vartriangleright u’[x := v’]$

$(𝜆x. u’) v’ ⟶ 𝜆^\ast (x, [u’]_𝜆) [u’]_𝜆 ⟶ [u’] [x := [v’]]$

  • $[[u]_𝜆]$
  • $[[x]_𝜆] = x$

  • $[[MN]_𝜆]_𝒞 = [[M]_𝜆]_𝒞 [[N]_𝜆]_𝒞 = _𝛽 MN$

  • $[[𝜆x.M]_𝜆]_𝒞 = [𝜆^\ast (x,M)]_𝒞$

  • $M = y≠x$ :

    \[[Ky]_𝒞 = [K]_𝒞 y \\ = (𝜆x z. x)y \\ =_𝛽 𝜆 z. y\]

  • $M = x$ :

    \[[I]_𝒞 = [SKK]_𝒞 \\ =_𝛽 𝜆 z. z\]

  • $M = NP$ : on vérifie que

    \[[[𝜆x.M]_𝜆]_𝒞 =_𝛽 𝜆 z. N z\]

Leave a comment