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 x
is equal to(f x) x
, which obviously doesn't work.Using the correct definition, we get
Since Y K doesn't reduce to I, the following substitution is not allowed.
So,
K I e
is simply