Greg Woodhouse wrote:
--- Paul Hudak <[EMAIL PROTECTED]> wrote:
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.
You can easily verify that
Y f = f (Y f)
LHS =
Y f =
(\f. (\x. f (x x)) (\x. f (x x))) f =
(\x. f (x x)) (\x. f (x x)) =
f ((\x. f (x x) (\x. f (x x)))
RHS =
f (Y f) =
f ((\f. (\x. f (x x)) (\x. f (x x))) f) =
f ((\x. f (x x)) (\x. f (x x)))
So (\f. (\x. f (x x)) (\x. f (x x))) is a fixpoint combinator
(one of infinitely many).
-- Lennart
-- Lennart
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
