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

Viewed 1561

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?

2 Answers
Related