Re: [Haskell-cafe] Infinite lists and lambda calculus
Greg Woodhouse wrote: Perhaps the issue is that the manipulations below are purely syntactic, But all the computation rules of the lambda calculus are syntactic in that sense. When you can prove things by symbol pushing it's the easiest way. But as Paul Hudak mentioned, there definitions that are equal, but you need something stronger to prove it, like fix point induction. 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))) 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? There is no search with this defintion (as you can see), it's very constructive. It computes the fix point which you can also define as oo fix f = lub f^i(_|_) i=0 where f^i is f iterated i times. Is that a definition of fixpoint that makes you happier? Since there are recursive functions that aren't primitive recursive, the answer has to be no. Where did primitive recursion come from? Y is used to express general recursion. 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) ... The list ones is the least upper bound in the domain of lazy (integer) lists of the following chain _|_, cons 1 _|_, cons 1 (cons 1 _|_), ... How much domain theory have you studied? Maybe that's where you can find the connection you're missing? -- Lennart ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Infinite lists and lambda calculus
--- Lennart Augustsson [EMAIL PROTECTED] wrote: It computes the fix point which you can also define as oo fix f = lub f^i(_|_) i=0 where f^i is f iterated i times. Is that a definition of fixpoint that makes you happier? Believe it or not, yes. My background is in mathematics, so something looking more like a fixed point of a continuous map seems a lot more intuitive. How much domain theory have you studied? Maybe that's where you can find the connection you're missing? None. But it seems clear that this is a deficit in my education I need to address. -- 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
Re: [Haskell-cafe] Infinite lists and lambda calculus (was: Detecting Cycles in Datastructures)
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
Re: [Haskell-cafe] Infinite lists and lambda calculus
Cale Gibbard wrote: 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. Actually no, the real definition is the top one, because the other one isn't even a valid lambda term, since it's recursive! There is no such thing as recursion in the pure lambda calculus. Of course, there are many valid definitions of Y, as you point out, both recursive and non-recursive. But I do believe that the first one above is the most concise non-recursive definition. -Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Infinite lists and lambda calculus
On 18/11/05, Paul Hudak [EMAIL PROTECTED] wrote: Cale Gibbard wrote: 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. Actually no, the real definition is the top one, because the other one isn't even a valid lambda term, since it's recursive! There is no such thing as recursion in the pure lambda calculus. I meant in the sense that Y f = f (Y f) is an axiomatic definition of Y. We're satisfied with any concrete definition of Y which meets that criterion. Of course it's not actually a lambda term, but it is an equation which a lambda term Y can satisfy. Similarly in, say, set theory, we don't say what sets *are* so much as we say what it is that they satisfy, and there are many models of set theory which meet those axioms. Y f = f (Y f) is really the only important property of Y, and any model of it will do as a concrete definition. - Cale Of course, there are many valid definitions of Y, as you point out, both recursive and non-recursive. But I do believe that the first one above is the most concise non-recursive definition. -Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
