为了证明 SKK 和 II 是 beta 等价的，λ 演算答案

【问题标题】：To prove SKK and II are beta equivalent, lambda calculus为了证明 SKK 和 II 是 beta 等价的，λ 演算
【发布时间】：2011-04-26 01:45:32
【问题描述】：

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

SKK 和 II 是等价的。

在哪里

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

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

【问题讨论】：

标签： functional-programming lambda-calculus proof-of-correctness k-combinator s-combinator

【解决方案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）

【讨论】：

【解决方案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

【讨论】：