Re: [Caml-list] Coinductive semantics

[David Baelde <david.baelde@gmail.com>]

In short,

An inductive type is the least fixpoint of some equations. The
coinductive type is the greatest fixpoint. For "t = nil | cons of
e*t", the elements of the inductive type are the lists, but the
coinductive type also contains the infinite lists.

Now for induction and coinduction, not so easy to tell... The
induction is the process building inductive types, the coinduction
builds coinductive types. In theory, the induction always terminates
and build a finite object. The coinduction should be seen as a lazy
process, since it potentially builds an infinite object: running it
builds the beginning of the object, then the process freezes and waits
for you to inspect the object deep enough.

Hope this helps... at least that's a try.
--
David