for fixed point combinator Y, what is \x.f(xx)

Question

For the Y combinator theorem,

 For every function F there exists an X such that FX=X

what's the F mean here? what's the fixed point for F(x) = x +1? My understanding is that x+1=x does not have a solution?

For the Proof below:

For any function F, let W be the function λx.F(xx) and let X = WW.
    We claim that X is a fixed point of F. Demonstrated as follows

    X = WW
    X = λx.F(xx) W
    X = F(WW)
    X = FX 

How's λx.F(xx) defined? again using F(x) = x + 1 as example, what's F(xx) mean?

Answer 1

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

Answer 2

There seems to be a bit confusion what fixed point for functions is and also about the lambda calculus notation.

First λx.F(xx) is a function taking an argument x and "applying" x to x and "then" "applying" F to the result, so more like function (x) { return F(x(x)); }, but do not take it literally, because in lambda calculus it is about substitutions of parameters and there is no order in which you need to do substitutions (what I used for simplification is applicative order).

So the proof rewritten to C-like syntax (actually JavaScript, as it has 1st class functions) with simple text-rewrite semantics would look like:

var W = function (x) { return F(x(x)); }
var X = W(W);

W(W) => (function (x) { return F(x(x)); }(W))
     => return F(W(W))
     => return F(X)
     => F(X)

Now back to fixed point. You give an algebraic example where fixed point does not exists... for functions it would be more like "find a fixed point of ADD1(x) = x + 1"

var F = function (x) { return x + 1; }
var W = function (x) { return F(x(x)); }
      = function (x) { return function (x) { return x + 1; }(x(x)); }
var X = W(W);

W(W) => function (x) { return function (x) { return x + 1; }(x(x)); }(W)
     => return function (x) { return x + 1; }(W(W))
     => return W(W) + 1
     => W(W) + 1
     => X + 1
     => F(X)

I hope that the familiar syntax made it less confusing rather than more :)