You are right in that the equation x+1 = x
has no solution when x
is a number. What's going on here is that x
is not restricted to being a number; it can be a function of functions.
About xx
: In general in lambda calculus f x
is a function application, so xx
is "x applied to x", or x(x)
. Note how x is both the function that is being applied and the value being passed to it.
So, if F(x) = x+1
, you have F(xx) = x(x)+1
, W = λx.(x(x)+1)
, and X=W(W)
would be the function:
X = W(W) = (λx.(x(x)+1)) (λy.(y(y)+1))
This may seem very abstract because if you try to expand X on any concrete value you'll find that the process never ends. But don't let that bother you; in spite of that X
is a fixed point of F
because
F(X) = F(W(W)) by definition of X = W(W)
= (λx.F(x(x))) W using the fact that (λt.f(t))x is f(x)
= W(W) by definition of W = λx.F(x(x))
= X by definition of X = W(W).