From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id D533ABB9C for ; Thu, 5 Jan 2006 20:48:09 +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 k05Jm9dx015023 for ; Thu, 5 Jan 2006 20:48:09 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA25778 for ; Thu, 5 Jan 2006 20:48:08 +0100 (MET) Received: from wproxy.gmail.com (wproxy.gmail.com [64.233.184.206]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k05Jm7wn015016 for ; Thu, 5 Jan 2006 20:48:08 +0100 Received: by wproxy.gmail.com with SMTP id i3so814504wra for ; Thu, 05 Jan 2006 11:48:07 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=FLrjovT5I88KhO0I+AOJ/WtkmJqHmkqu83XllDR8Isbu8NCjbJOD2Gqr080sMOu5IZfp0dKs/z+s/yvSKbG5eXCIa4NtMEm7bSN6imV9usxUESP1zTRaXn6mYu1J7sZBLR3YRFm0fcr4P9X3MYJFTvJUbzSSDc3kO2L9xy4K1mo= Received: by 10.65.115.10 with SMTP id s10mr1505749qbm; Thu, 05 Jan 2006 11:48:06 -0800 (PST) Received: by 10.65.204.6 with HTTP; Thu, 5 Jan 2006 11:48:06 -0800 (PST) Message-ID: <53c655920601051148r3a0501edn@mail.gmail.com> Date: Thu, 5 Jan 2006 20:48:06 +0100 From: David Baelde Reply-To: david.baelde@ens-lyon.org To: Alessandro Baretta Subject: Re: [Caml-list] Coinductive semantics Cc: Ocaml In-Reply-To: <43BD6418.4090407@barettadeit.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline References: <43BD6418.4090407@barettadeit.com> X-Miltered: at nez-perce with ID 43BD77F9.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 43BD77F7.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 coinductive:01 semantics:01 fixpoint:01 coinductive:01 fixpoint:01 lazy:01 freezes:01 terminates:01 short:01 finite:02 types:02 types:02 cons:03 elements:05 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=RCVD_BY_IP autolearn=disabled version=3.0.3 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