证明SKK和II是β等价的,lambda演算

Question

我是lambda演算的新手,并努力证明以下内容.

SKK和II是等效的.

哪里

S = lambda xyz.xz(yz)K = lambda xy.x I = lambda 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)