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

[minh thu]

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

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