On Jun 22, 2006, at 10:16 AM, Brian Hulley wrote:
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.
Induction doesn't apply to co-inductive objects, such as infinite
lists AKA streams.
I particular, the "length" of an infinite list is undefined, much as
the "size" of an infinite set is undefined. The only think you can
discuss, a la Cantor, is cardinality. In both cases, as mentioned by
another poster, it is aleph-null.
<aside>
Every few months a discussion arises about induction and Haskell
datatypes, and I feel compelled to trot out this oft-misunderstood
fact about Haskell: 'data' declarations in Haskell introduce co-
inductive definitions, NOT inductive ones. Induction, in general,
does not apply to ADTs defined in Haskell; this is in contrast to
similar-looking definitions in, eg, ML. This is a common source of
confusion, especially for mathematically-inclined persons new to
Haskell. Does anyone know of a good reference which clearly explains
the difference and its ramifications? I've never been able to find a
paper on the topic that doesn't dive head-first into complicated
category theory (which I usually can't follow) ...
</aside>
Rob Dockins
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
-- TMBG
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
