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

[Cale Gibbard]

On 18/11/05, Greg Woodhouse <gregory.woodhouse at sbcglobal.net> wrote:
>
>
> --- Lennart Augustsson <lennart at augustsson.net> 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  <gregory.woodhouse at sbcglobal.net>
>
>
> "Interaction is the mind-body problem of computing."
>
> --Philip Wadler
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>