Lambda the Ultimate

I think it is:

YF = ( \f. (\x.f(xx)) (\x.f(xx)) ) F =

here I replace "f" with "F"

= (\x.F(xx))(\x.F(xx)) =

now I replace "x" with "(\x.F(xx))"

= F(\x.F(xx))(\x.F(xx))

now, we know that "(\x.F(xx))(\x.F(xx))" is equal to YF, so "F(\x.F(xx))(\x.F(xx))" is equal to F(YF)

Is it right?

Now can you explain the significance of this observation? :)

What I miss, maybe, is that "=" is symmetric.

So, when I apply Y to F, Y "duplicates" F, so I get F(YF).

From YF I go to F(YF).
If I procede backward (may I?), I obtain from F(YF), YF.

I'm really not sure about this. If that's right, that would means that I can write something like:

y = (\x.x)y

Am I wrong?

It depends on what you're looking at. There's one sense in which = is symmetric, and in this case, we call that relationship β-equivalence. When you're talking about "equivalence", you can go either direction. But when we're looking at lambda calculus as a programming system, we're usually interested in going only one direction. Then we call it β-reduction, and we don't usually write =. We might write, instead, something like: Y f => f (Y f). (It's important to note that in this case, one β-reduction actually increases the size of the term.)

When we're looking at it asymmetrically, the other direction is called β-expansion, and yes, you can indeed expand y to (\x.x) y. Of course, this doesn't make much sense when using lambda calculus to write programs, but in fact some compiler optimizations might perform this kind of expansion in certain cases.

Of course, this doesn't really get at the why of Y... Can you see what is special about the Y f = f (Y f) equivalence?

[edit: I should be a bit more clear. In the case of Y f = f (Y f), it isn't a simple reduction. In order to get from the left to the right side, we need to do a little bit of re-arranging (as in your post above, β-reduce twice and then η-expand). This is why it probably makes more sense to talk about equivalence than reduction in this case, and why we write = rather than =>.]

Well, I read the fixed point theorem a lot of time, and also about its consequences. So I know it's useful to simulate recursion in lambda calculus where, actually, we can't give a name to functions. So we use it for the factorial etc.

And I think I understand that applying Y to any terms, it just duplicates the term.
So YF = F(YF) = F(F(YF) = .... = Fⁿ(YF)

This seems clear to me, at least, I think.

It's just that in every book or article, on every site I see, before of what I wrote, this: any F, F(YF) = YF

I wanted to convince myself that was right, but I couldn't explain why.

I suppose the reason most people write f (Y f) = Y f is that this gives more intuition about why we want Y. That is, it makes more sense from a derivation point of view: we are looking for some Y that satisfies this equation (folds up infinite self-application into a neat little closed package). From the more operational point of view, the other direction is probably more useful.

I hope it makes more sense now...

Thanks a lot. Sadly I am just at the beginning.

Bye,
Carlo