On 18/11/05, Greg Woodhouse <[EMAIL PROTECTED]> wrote: > > > --- Lennart Augustsson <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> > > > "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 >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe