RE: [Caml-list] Coinductive semantics

["Don Syme" <Don.Syme@microsoft.com>]

I find it helpful to think of induction as simply a process of
"repeatedly adding new members to a set according to a set of rules",
and co-induction as a process of "repeatedly taking away members from a
set according to what's excluded by a set of rules, and seeing what's
left".  

For example, divergence is defined by repeatedly taking away the
convergent programs from the set of all programs.

To take a very non-serious example, think of the rules that parents lay
down for their children (which are often recursively referential, let
alone contradictory :-)).  Induction corresponds to "you may only do
what follows from the rules", whereas co-induction corresponds to "you
may do anything that is not excluded by the rules".  For an empty set of
rules an inductive child can do nothing, a co-inductive child can do
anything.  

This all shows my unfashionable set-theoretic biases :-)

Don


-----Original Message-----
From: caml-list-bounces@yquem.inria.fr
[mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of David Baelde
Sent: 05 January 2006 20:48
To: Alessandro Baretta
Cc: Ocaml
Subject: Re: [Caml-list] Coinductive semantics

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

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs