Re: [Haskell-cafe] Functional progr., images, laziness and all therest
Brian Hulley [EMAIL PROTECTED] writes: But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. infinity+1 = infinity Surely this is just a mathematical convention, not reality! :-) Not even that. Infinity isn't a number, and it doesn't really make sense to add one to it. Couldn't an infinite list just be regarded as the maximum element of the (infinite) set of all finite lists? The point of infinity is that there is no maximum :-) -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
On Thu, Jun 22, 2006 at 05:44:58PM +0100, I wrote: It works because Haskell 'data' definitions yield both an initial fixed point (with respect to strict functions) and a terminal fixed point (with respect to arbitrary functions), and moreover these are usually the same. The former is inductive, the latter co-inductive. They differ only when the definition is strict in the recursive type, as in data Nat = Zero | Succ !Nat On second thoughts, I think the fixed points coincide in these cases too. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
Jerzy Karczmarczuk wrote: Brian Hulley wrote: [EMAIL PROTECTED] wrote: you may transform a recurrential equation yielding Y out of X: Y[n+1] = a*X[n+1] + b*Y[n] usually (imperatively) implemented as a loop, into a stream definition: ... Can you explain how this transformation was accomplished? y = (a*x0:yq) -- Here I was in error, a missing yq = a*xq + b*y with, of course, a*xq meaning map(a*) xq; x+y meaning zipWith(*) x y y0 = a*x0 Look yourself: y1 = a*x1 + b*y0 y2 = a*x2 + b*y1, etc. So, first, this is correct, element by element. Don't tell me you have never seen the assembly of all non-negative integers as an infinite list thereof: integs = 0 : (integs + ones) where ones = 1:ones it is quite similar (conceptually). Thanks for the explanation. y IS NOT a longer list than yq, since co-recursive equations without limiting cases, apply only to *infinite* streams. Obviously, the consumer of such a stream will generate a finite segment only, but it is his/her/its problem, not that of the producer. I still don't understand this point, since y = (a*x0 : yq) so surely by induction on the length of yq, y has 1 more element? 2. Are we speaking about assembly-style, imperative programming, or about functional style? Please write your loop in Haskell or any other fun. language, and share with us its elegance. Starting with: Y[n+1] = a*X[n+1] + b*Y[n] filtr a b (x0:xs) = y0 : filtr' xs y0 where y0 = a * x0 filtr' (x_n1 : xs) y_n = y_n1 : filtr' xs y_n1 where y_n1 = a * x_n1 + b * y_n In a sense I'm still using a lazy stream, but the difference is that I'm not making any use of the evaluate once then store for next time aspect of lazyness, so the above code could be translated directly to use the force/delay streams I mentioned before. Also, the original formula now appears directly in the definition of filtr' so it can be understood without an initiation into stream processing. (Piotr - I see my original wording imperative loop was misleading - in the context of functional programming I tend to just use this to mean a simple recursive function) 3. Full disagreement. There is NOTHING obfuscated here, on the contrary, the full semantics is in front of your eyes, it requires only some reasoning in terms of infinite lists. See point (1). The same could be said for all obfuscated code: it's always fully visible but just requires reasoning to understand it! :-) Still I suppose perhaps the word obfuscated was a bit strong and certainly with your explanation, which you mentioned as a prerequisite in answer to my point 1), I now understand your original code also, but not without making some effort. Best regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
2006/6/22, Brian Hulley [EMAIL PROTECTED]: Jerzy Karczmarczuk wrote: Brian Hulley wrote: [snip] y IS NOT a longer list than yq, since co-recursive equations without limiting cases, apply only to *infinite* streams. Obviously, the consumer of such a stream will generate a finite segment only, but it is his/her/its problem, not that of the producer. I still don't understand this point, since y = (a*x0 : yq) so surely by induction on the length of yq, y has 1 more element? y and yq are infinite... mt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
minh thu wrote: 2006/6/22, Brian Hulley [EMAIL PROTECTED]: Jerzy Karczmarczuk wrote: Brian Hulley wrote: [snip] y IS NOT a longer list than yq, since co-recursive equations without limiting cases, apply only to *infinite* streams. Obviously, the consumer of such a stream will generate a finite segment only, but it is his/her/its problem, not that of the producer. I still don't understand this point, since y = (a*x0 : yq) so surely by induction on the length of yq, y has 1 more element? y and yq are infinite... But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. I don't see why induction can't just be applied infinitely to prove this. Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
On 2006-06-22 at 15:16BST Brian Hulley wrote: minh thu wrote: y and yq are infinite... But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. infinity+1 = infinity I don't see why induction can't just be applied infinitely to prove this. because (ordinary) induction won't go that far. -- Jón Fairbairn Jon.Fairbairn at cl.cam.ac.uk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
On Thu, 2006-06-22 at 15:16 +0100, Brian Hulley wrote: . . . But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. I don't see why induction can't just be applied infinitely to prove this. The set of all non-negative integers has one more element than the set of all positive integers, however they have the same cardinality, aleph-null. This phenomenon is the hallmark of infinite sets. -- Bill Wood ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
2006/6/22, Brian Hulley [EMAIL PROTECTED]: minh thu wrote: 2006/6/22, Brian Hulley [EMAIL PROTECTED]: Jerzy Karczmarczuk wrote: Brian Hulley wrote: [snip] y IS NOT a longer list than yq, since co-recursive equations without limiting cases, apply only to *infinite* streams. Obviously, the consumer of such a stream will generate a finite segment only, but it is his/her/its problem, not that of the producer. I still don't understand this point, since y = (a*x0 : yq) so surely by induction on the length of yq, y has 1 more element? y and yq are infinite... But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. I don't see why induction can't just be applied infinitely to prove this. maybe i wrong, anyway : induction can be used to prove a property. we claim that the property is true for any finite i. so what's the property that you want to prove by induction ? you say 'by induction on the lenght of yq'.. but yq is just y (modulo the a*xq + b*). it's exactly the same in ones = 1:ones does the left ones longer than the right one ? mt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
Jon Fairbairn wrote: On 2006-06-22 at 15:16BST Brian Hulley wrote: minh thu wrote: y and yq are infinite... But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. infinity+1 = infinity Surely this is just a mathematical convention, not reality! :-) I don't see why induction can't just be applied infinitely to prove this. because (ordinary) induction won't go that far. I wonder why? For any finite list yq, |y| == |yq| + 1 So considering any member yq (and corresponding y) of the set of all finite lists, |y| == |yq| + 1 Couldn't an infinite list just be regarded as the maximum element of the (infinite) set of all finite lists? Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
On 2006-06-22 at 15:45BST Brian Hulley wrote: Jon Fairbairn wrote: infinity+1 = infinity Surely this is just a mathematical convention, not reality! :-) I'm not sure how to answer that. The only equality worth talking about on numbers (and lists) is the mathematical one, and it's a mathematical truth, not a convention. I don't see why induction can't just be applied infinitely to prove this. because (ordinary) induction won't go that far. I wonder why? For any finite list yq, |y| == |yq| + 1 So considering any member yq (and corresponding y) of the set of all finite lists, |y| == |yq| + 1 But the infinite lists /aren't/ members of that set. For infinite lists the arithmetic is different. |y| == |yq| +1 == |yq| If you don't use the appropriate arithmetic, your logic will eventually blow up. Couldn't an infinite list just be regarded as the maximum element of the (infinite) set of all finite lists? It can be, but that doesn't get it into the set. -- Jón Fairbairn Jon.Fairbairn at cl.cam.ac.uk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
On Jun 22, 2006, at 10:16 AM, Brian Hulley wrote: minh thu wrote: 2006/6/22, Brian Hulley [EMAIL PROTECTED]: Jerzy Karczmarczuk wrote: Brian Hulley wrote: [snip] y IS NOT a longer list than yq, since co-recursive equations without limiting cases, apply only to *infinite* streams. Obviously, the consumer of such a stream will generate a finite segment only, but it is his/her/its problem, not that of the producer. I still don't understand this point, since y = (a*x0 : yq) so surely by induction on the length of yq, y has 1 more element? y and yq are infinite... But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. I don't see why induction can't just be applied infinitely to prove this. Induction doesn't apply to co-inductive objects, such as infinite lists AKA streams. I particular, the length of an infinite list is undefined, much as the size of an infinite set is undefined. The only think you can discuss, a la Cantor, is cardinality. In both cases, as mentioned by another poster, it is aleph-null. aside Every few months a discussion arises about induction and Haskell datatypes, and I feel compelled to trot out this oft-misunderstood fact about Haskell: 'data' declarations in Haskell introduce co- inductive definitions, NOT inductive ones. Induction, in general, does not apply to ADTs defined in Haskell; this is in contrast to similar-looking definitions in, eg, ML. This is a common source of confusion, especially for mathematically-inclined persons new to Haskell. Does anyone know of a good reference which clearly explains the difference and its ramifications? I've never been able to find a paper on the topic that doesn't dive head-first into complicated category theory (which I usually can't follow) ... /aside Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
On Thu, Jun 22, 2006 at 11:06:38AM -0400, Robert Dockins wrote: aside Every few months a discussion arises about induction and Haskell datatypes, and I feel compelled to trot out this oft-misunderstood fact about Haskell: 'data' declarations in Haskell introduce co- inductive definitions, NOT inductive ones. Induction, in general, does not apply to ADTs defined in Haskell; this is in contrast to similar-looking definitions in, eg, ML. This is a common source of confusion, especially for mathematically-inclined persons new to Haskell. Does anyone know of a good reference which clearly explains the difference and its ramifications? I've never been able to find a paper on the topic that doesn't dive head-first into complicated category theory (which I usually can't follow) ... /aside I think that's untrue, from a certain point of view. A convenient semantics for Haskell data types includes values for non-termination (_|_, or bottom), partial values (containing _|_) and infinite values, with a termination ordering -- a complete partial order (cpo for short). The infinite values are needed for the complete part: they arise as the limits of ascending chains of partial values. (The semantics of ML types has extra values too, but in a different place: the partial functions in the - type.) You can do induction over Haskell data types, as long as your predicate is well-behaved on limits (which conjunctions of equations are), and also satisfied by _|_. There's a good introduction to this sort of reasoning in Introduction to Functional Programming using Haskell by Bird (or the first edition by Bird and Wadler). It works because Haskell 'data' definitions yield both an initial fixed point (with respect to strict functions) and a terminal fixed point (with respect to arbitrary functions), and moreover these are usually the same. The former is inductive, the latter co-inductive. They differ only when the definition is strict in the recursive type, as in data Nat = Zero | Succ !Nat The initial fixed point is the natural numbers plus _|_. The terminal fixed point has those elements plus an infinity. The former corresponds to what Haskell provides. So actually Haskell data types are always inductive, and usually also co-inductive. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional progr., images, laziness and all therest
minh thu wrote: maybe i wrong, anyway : induction can be used to prove a property. we claim that the property is true for any finite i. so what's the property that you want to prove by induction ? you say 'by induction on the lenght of yq'.. but yq is just y (modulo the a*xq + b*). it's exactly the same in ones = 1:ones does the left ones longer than the right one ? Thanks for pointing this out - I'd somehow missed the fact that yq was also defined in terms of y, so of course the idea of length becomes meaningless in this context (at least as far as trying to compare the length of yq with that of y) Best regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
