Re: [Haskell-cafe] Infinite lists and lambda calculus (was: Detecting Cycles in Datastructures)

On 18/11/05, Greg Woodhouse wrote:

--- Lennart Augustsson wrote:

I guess I'm not doing a very good job of expressing myself. I see that if you define Y as you do, then the various functions you list have the property that Y f = f (Y f).

I don't want to draw out a boring discussion that is basically about my own qualms here, especially since I haven't really been able to articulate what it is that bothers me.

Perhaps the issue is that the manipulations below are purely syntactic, and though they work, it is not at all clear how to make contact with other notions of computability. Perhaps it is that

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

In a sense, the real definition of Y is Y f = f (Y f), this lambda term just happens to have that property, but such functions aren't rare. One fun one is: Y = (L L L L L L L L L L L L L L L L L L L L L L L L L L L L) where L = λabcdefghijklmnopqstuvwxyzr. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r))

is a perfect sensible definition, it's still just a recipe for a computation. Maybe I'm thinking too hard, but it reminds me of the mu operator. Primiive recursive functions are nice and constructive, but minimization is basically a "search", there's no guarantee it will work. If I write

g(x) = mu x (f(x) - x)

then I've basically said "look at every x and stop when you find a fixed point". Likewise, given a candidate for f, it's easy to verify that Y f = f (Y f), as you've shown, but can the f be found without some kind of "search"? Since there are recursive functions that aren't primitive recursive, the answer has to be "no".

Finally, you've exhibited a sequence of fixed points, and in this case it's intuitively clear how these correspond to something we might call an infinite list. But is there an interpetration that makes this precise? The notation

ones = cons 1 ones ones = cons 1 (cons 1 ones) ...

is suggestive, but only suggestive (at least as far as I can see). Is there a model in which [1, 1 ...] is a real "thing" that is somehow "approached" by the finite lists?

...

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

=== Gregory Woodhouse

"Interaction is the mind-body problem of computing."

--Philip Wadler

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe