functional-programminglambda-calculusproof-of-correctnessk-combinators-combinator

To prove SKK and II are beta equivalent, lambda calculus


I am new to lambda 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.


Solution

  •   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)