functional-programming - 为了证明 SKK 和 II 是 beta 等价的，λ 演算

Question

我是 lambda 演算的新手，正在努力证明以下内容。

SKK 和 II 是 beta 等效的。

在哪里

S = λ xyz.xz(yz) K = λ xy.x I = λ xx

我试图通过打开它来测试减少SKK，但无济于事，它变得一团糟。不要以为SKK可以在不扩大S、K的情况下进一步缩小。

Answer 1

  SKK
= (λxyz.xz(yz))KK
→ λz.Kz(Kz)        (in two steps actually, for the two parameters)

  Kz
= (λxy.x)z
→ λy.z

  λz.Kz(Kz)
→ λz.(λy.z)(λy.z)  (again, several steps)
→ λz.z
= I

（你应该能够证明II → I）

Answer 2

;另一种步骤更少的方法，首先将SK减少到λyz.z;

SKK
= (λxyz.xz(yz))KK
→ λyz.Kz(yz) K
→ λyz.(λxy.x)z(yz) K
→ λyz.(λy.z)(yz) K
→ λyz.z K
→ λz.z
= I