--- Paul Hudak
The important property of Y is this:
Y f = f (Y f)
Right. This is just a formal statement of the property thaat f fixex Y f. I'm with you so far.
In this way you can see it as "unwinding" the function, one step at a
time. If we define f as (\ones. cons 1 ones), then here is one step of unwinding:
Y f ==> f (Y f) ==> cons 1 (Y f)
I'm with you here, too, except that we are *assuming* that Y has the stated property. If it does, it's absolutely clear that the above should hold.
If you do this again you get:
cons 1 (cons 1 (Y f))
and so on. As you can see, continuing this process yields the infinite list of ones.
Right.
Now note that if we define g as (\ones. cons 1 (cons 1 ones)), we get:
Y g ==> g (Y g) ==> cons 1 (cons 1 (Y g))
Now, this is where things get a little mysterious. Where did g come from? I understand that the "x x" om formal definition of Y is what makes everything work (or, at least I think I do). When I try and think this all through, I wind up with something like this: First of all, I'm after a "list" (named ones) with the property that ones = cons 1 ones. How can I express the existence of such a thing as a fixed point? Well, if it does exist, it must be a fixed point of f = \x. cons 1 x, because f ones ==> (\x. cons 1 x) ones ==> cons 1 ones ==? ones Now, if I write Y = \y. (\x y (x x)) (\x. y x x) then, Y f ==> cons 1 (\x. cons 1 ( x x)) (\x (cons 1) x x) and I'm left to ponder what that might mean. Formally, I can see that this pulls an extra cons 1 out to the left, and so we're led to your g
which obviously also yields the infinite list of ones. Yet f is not equal to g.
To me, all this really seems to be saying is that for any n, there's a lambda expression explicitly involving [1, 1, ..., 1] (n times) that is a "solution" to the above problem, which I interpet (perhaps incorrectly) to mean that *if* there were a "real" list that wedre a solution to the above recurrence, then for any n, there would be an initial sublist consisting of just 1's. Now, I know that lambda expressions are not lists, though lists can be encoded as lambda expressions. For finite lists, this all seem simple enough, but in this case we seem to have a lambda expression that is not a (finite) list, but that can nevertheless be "approximated" in some3 sense by finte lists. But I can't really put my finger on just what that sense might be.
Does this help?
Yes, it does. Very much so.
-Paul
===
Gregory Woodhouse