É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]$

𝜆^\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

Tags:

Updated: