[SOLVED] Fixed point of K combinator

Fixed point of K combinator

The K combinator is K := (λxy.x) and the fixed point combinator is Y := λf.(λx.f x x) (λx.f x x). I tried to calculate YK:

YK = (λx.Kxx)(λx.Kxx) = (λx.x)(λx.x) = (λx.x) = I

So because YK is the fixed point of K:

K(YK) = YK
KI = I
KIe = Ie = e

for any e. But KIe should be equal to I!

Solution

You're not starting with the correct definition of the Y-combinator. It should be Y := λf.(λx.f (x x)) (λx.f (x x)) (note the parentheses around x x). Since lambda-calculus is left-associative, f x x is equal to (f x) x, which obviously doesn't work.

Using the correct definition, we get

Y K := (λf.(λx.f (x x)) (λx.f (x x))) K
       (λx.K (x x)) (λx.K (x x))
       K ((λx.K (x x)) (λx.K (x x)))
       K (Y K)

Since Y K doesn't reduce to I, the following substitution is not allowed.

K (Y K) = Y K
K I = I

So, K I e is simply

K I e := (K I) e
         ((λx.λy.x) I) e
         (λy.I) e
         I