Greg Woodhouse wrote:
--- Paul Hudak <[EMAIL PROTECTED]> wrote:
Y (\ones. cons 1 ones)
where Y (aka the "paradoxical combinator" or "fixed point
combinator") is defined as:
\f. (\x. f (x x)) (\x. f (x x))
Now, this is I have seen, but it frankly strikes me as a "formal
trick". I've never felt that this definition of Y gave me much insight
into the computation you describe below.
To see this, try unfolding the above term a few iterations using
normal-order reduction. Note that the term has no recursion in it
whatsoever.
Now, my earlier point above is that:
Y (\ones. cons 1 ones)
unwinds to the same term as:
Y (\ones. cons 1 (cons 1 ones))
yet the two terms (\ones. cons 1 ones) and
(\ones. cons 1 (cons 1 ones)) are not the same (in fact they're not
lambda convertible, either).
-Paul
And this is what leaves me scatching my head. If you leave off the
"ones", then you get a sequence of finite lists [1], [1, 1], ... that
seems to approximate the infinite list, but I find it difficult to
imagine how you might pluck a formula like \i. 1 (the ith term) out of
the air.
The important property of Y is this:
Y f = f (Y f)
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)
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.
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))
which obviously also yields the infinite list of ones. Yet f is not
equal to g.
Does this help?
-Paul
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
