From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id AEDF1BB9C for ; Thu, 5 Jan 2006 21:40:03 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k05Ke3m6019576 for ; Thu, 5 Jan 2006 21:40:03 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA26859 for ; Thu, 5 Jan 2006 21:40:02 +0100 (MET) Received: from mail-eur1.microsoft.com (mail-eur1.microsoft.com [213.199.128.139]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k05Ke1VX008342 for ; Thu, 5 Jan 2006 21:40:01 +0100 Received: from EUR-MSG-10.europe.corp.microsoft.com ([65.53.193.196]) by mail-eur1.microsoft.com with Microsoft SMTPSVC(6.0.3790.1830); Thu, 5 Jan 2006 20:39:59 +0000 X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] Coinductive semantics Date: Thu, 5 Jan 2006 20:38:50 -0000 Message-ID: <6C6555DF5D075A4EA6D27706F4EC5975044A93F8@EUR-MSG-10.europe.corp.microsoft.com> Thread-Topic: [Caml-list] Coinductive semantics Thread-Index: AcYSMixdJrk5k0ULTU+lEVnhiLj8zwAA43eQ From: "Don Syme" To: , "Alessandro Baretta" Cc: "Ocaml" X-OriginalArrivalTime: 05 Jan 2006 20:39:59.0601 (UTC) FILETIME=[322E6E10:01C61238] X-Miltered: at nez-perce with ID 43BD8423.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43BD8421.003 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 coinductive:01 semantics:01 syme:01 syme:01 corresponds:01 corresponds:01 baretta:01 ocaml:01 caml-list:01 coinductive:01 semantics:01 fixpoint:01 fixpoint:01 lazy:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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". =20 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. =20 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 =3D 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