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!
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 aroundx x). Since lambda-calculus is left-associative,f x xis 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.
So,
K I eis simply