Lambda Calculus: fixed point theorem help

I'm studying the lambda calculus and there's something I can't understand in the fixed point theorem.

I'm reading the Barendregt book Lamba Calculi with Types, but at the moment I'm studyng the untyped one, in the first part of the book.

It says there is a fixed point combinator: ( \ = lambda )

Y = \f.(\x.f(xx))(\x.f(xx))

such that

for any F, F(YF) = YF

So, if my F is just a variable, let's say F = q, then how

q(Yq) can become Yq?

I am sure I am missing something.
Can you help me?


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


Try starting from YF and see if you can get to F(YF).

I think it is: YF = ( \f.

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?

It is right

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

What I miss, maybe, is that

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?

Depends on the context...

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

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) = .... = Fn(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.

Makes sense...

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.


Next step

Once you see why the equation is true. I want you to try a few different F's

F n = prefact R n = if n > 1 then n*R(n-1) else 1
F n = prefib S n = if 2 > n then 1 else S(n-1) + S(n-2)
F a b = preremainder T a b = if b > a then a else T(a-b,b)

Now for a moment picture if
R were factorial or S were fibonacci or T were remained life would be good.

Now consider what Y.prefact, Y.prefib, Y.preremander are