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 C51A6BB81 for ; Tue, 10 Jan 2006 12:07:47 +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 k0AB7kEI012301 for ; Tue, 10 Jan 2006 12:07:46 +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 MAA05901 for ; Tue, 10 Jan 2006 12:07:46 +0100 (MET) Received: from smtp03.uc3m.es (smtp03.uc3m.es [163.117.136.123]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0AB7jc2007162 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=FAIL) for ; Tue, 10 Jan 2006 12:07:45 +0100 Received: from smtp03.uc3m.es (localhost [127.0.0.1]) by localhost.uc3m.es (Postfix) with ESMTP id 20346834F5 for ; Tue, 10 Jan 2006 12:07:45 +0100 (CET) Received: from ariel.tsc.uc3m.es (ariel.tsc.uc3m.es [163.117.145.25]) (using TLSv1 with cipher EDH-RSA-DES-CBC3-SHA (168/168 bits)) (No client certificate requested) by smtp03.uc3m.es (Postfix) with ESMTP id EB5DA83440 for ; Tue, 10 Jan 2006 12:07:44 +0100 (CET) Received: from umbriel.tsc.uc3m.es (umbriel.tsc.uc3m.es [163.117.145.225]) by ariel.tsc.uc3m.es (8.13.4/8.13.4) with ESMTP id k0AB7Wcv014688 for ; Tue, 10 Jan 2006 12:07:32 +0100 DomainKey-Signature: a=rsa-sha1; s=dtsc-uc3m; d=tsc.uc3m.es; c=simple; q=dns; h=received:date:from:subject:in-reply-to:to:cc:message-id: mime-version:content-type:content-transfer-encoding: x-accept-language:references:user-agent:received-spf; b=qRMNmuxHlDrgWGVaAhDRbXre7xFCNFvq8RDSHUh5nxpg8NXLg5/921mzWP6SWHDsN 2l9uI4bQgahO8VCjwdhSg== Received: from [163.117.145.58] by umbriel.tsc.uc3m.es (Sun Java System Messaging Server 6.2-2.05 (built Apr 28 2005)) with ESMTPS id <0ISV000XEIWVBJ50@umbriel.tsc.uc3m.es> for caml-list@inria.fr; Tue, 10 Jan 2006 12:07:43 +0100 (CET) Date: Tue, 10 Jan 2006 12:10:53 +0100 From: "Francisco J. Valverde Albacete" Subject: Re: [Caml-list] Coinductive semantics In-reply-to: <43BE6CAB.2030503@andrej.com> To: Andrej Bauer Cc: Alessandro Baretta , caml-list@inria.fr Message-id: <43C3963D.5030601@tsc.uc3m.es> MIME-version: 1.0 Content-type: text/plain; charset=ISO-8859-2; format=flowed Content-transfer-encoding: 7BIT X-Accept-Language: en-us, en References: <43BD6418.4090407@barettadeit.com> <43BE6CAB.2030503@andrej.com> User-Agent: Mozilla Thunderbird 1.0.7-1.1.fc3 (X11/20050929) Received-SPF: pass (ariel.tsc.uc3m.es: 163.117.145.225 is whitelisted) receiver=ariel.tsc.uc3m.es; client-ip=163.117.145.225; helo=umbriel.tsc.uc3m.es; envelope-from=fva@tsc.uc3m.es; x-software=spfmilter 0.95 http://www.acme.com/software/spfmilter/ with libspf2; X-TSC-MailScanner-Information: e-mail scanned by MailSystem in DTSC-UC3M X-TSC-MailScanner: Found to be clean X-TSC-MailScanner-From: fva@tsc.uc3m.es X-Miltered: at nez-perce with ID 43C39582.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43C39581.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; valverde:01 caml-list:01 coinductive:01 semantics:01 algebra:01 constructors:01 datatypes:01 descriptors:01 datatypes:01 valverde:01 andrej:01 baretta:01 algebra:01 non-trivial:01 subset: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 Hi although I may be out on a limb here, I recall reading *somewhere* :( that while initial algebras where good models for stateless abstract data types (and (structural) induction the way to work over terms in the free algebra defined by constructors modulo the laws of the ADT), final algebras where good models for *stateful* datatypes (and coinduction the way to work over the finer "state descriptors" modulo the laws of state equivalence), hence they *might* be better models for *objects* (as stateful datatypes) than initial algebras. Has anybody read anything proving or disproving this? Regards, Francisco Valverde - DTSC Univ. Carlos III de Madrid Andrej Bauer wrote: >Alessandro Baretta wrote: > > >>Is there anyone around who can help? >> >> > >Induction is about initial algebras. It says that an initial algebra >does not have any non-trivial SUB-algebras. General induction principle >for the initial algebra A with operations f_1, ..., f_n (some of which >may be 0-ary operations, i.e., constants) goes as follows: > >INDUCTION PRINCIPLE: >Suppose S is a subset of A which is closed under operations f_i, meaning >that if x_1, ..., x_{k_i} are in S then also f_i(x_1, ..., x_{k_i}) is >in S (here k is the arity of operation f_i). Then S = A. > >If we apply this to the case when we have one constant f_0=Empty and one >binary operation f_1=Tree, we get as A all finite binary trees and the >induction principle: > >INDUCTION PRINCIPLE FOR FINITE BINARY TREES: >Suppose S is a set of finite binary trees such that the empty tree is in >S, and whenever x and y are in S then also tree Tree(x,y) is in S. Then >S is the set of all finite binary trees. > >Now coinduction is about final coalgebras. It says that a final >coalgebra does not have any non-trivial QUOTIENT coaglebras. This is >usually expressed as follows: if F is the final coalgebra for operations >f_1, ..., f_n, and E is an equivalence relation on F which respects the >operations, then E is the identity relation (because if it were not, we >could form a nontrivial quotient coaglebra F/E). The actual coinduction >principle may be stated for an arbitrary relation R (think of E as the >equivalence relation generated by R): > >COINDUCTION PRINCIPLE: >Suppose R is a relation on the final coalgebra F which respects the >operations, i.e., if x_1 R y_1, ...., x_{k_i} R y_{k_i} then >f_i(x_1, ..., x_{k_i}) R f_i(y_1, ..., y_{k_i}) for all x's, y's and >f_i's. Then R(x,y) implies x = y. > >An R satisfying the above condition generates the trivial equivalence >relation (equality) and so the quotient F/R is just F. > >We take again as example the final coalgebra F with one constant >f_0=Empty and one binary operation f_1=Tree. This is the set of finite >and infinite binary trees. > >COINDUCTION FOR (FINITE AND INFINITE) BINARY TREES: >Suppose R is a relation on trees such that: >(1) Empty R Empty >(2) if x R y and x' R y' then Tree(x,y) R Tree(x',y'). >Then x R y implies x = y. > >It takes some practice to get used to coinduction and to figure out how >to prove properties of final coalgebras with it. If this was too terse, >let me know (and tell me which bits to expand upon). > >Andrej > >_______________________________________________ >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 > >