开发者

To prove SKK and II are beta equivalent, lambda calculus

I am new to lambda开发者_如何学C calculus and struggling to prove the following.

SKK and II are beta equivalent.

where

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

I tried to beta reduce SKK by opening it up, but got nowhere, it becomes to messy. Dont think SKK can be reduced further without expanding S, K.


  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

(You should be able to prove that II → I)


;another approach with fewer steps, first reduce SK to λ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
0

上一篇:

下一篇:

精彩评论

暂无评论...
验证码 换一张
取 消

最新问答

问答排行榜