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

[Brian Hulley]

minh thu wrote:
> 2006/6/22, Brian Hulley <brianh at metamilk.com>:
>> 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