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

2006/6/22, Brian Hulley :

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.

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