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
