Re: [Haskell-cafe] Functional progr., images, laziness and all therest

minh thu wrote:

2006/6/22, Brian Hulley :

...

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