From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 530A9BB81 for ; Fri, 13 Jan 2006 11:23:45 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0DANiHx018131 for ; Fri, 13 Jan 2006 11:23:45 +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 LAA01900 for ; Fri, 13 Jan 2006 11:23:44 +0100 (MET) Received: from mail.tcs.inf.tu-dresden.de (tcs01.inf.tu-dresden.de [141.76.75.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0DANiPY018124 for ; Fri, 13 Jan 2006 11:23:44 +0100 Received: from localhost (localhost [127.0.0.1]) by mail.tcs.inf.tu-dresden.de (Sun Java System Messaging Server 6.1 HotFix 0.06 (built Nov 11 2004)) with ESMTP id <0IT100L6Q0VJ3O00@mail.tcs.inf.tu-dresden.de> for caml-list@inria.fr; Fri, 13 Jan 2006 11:23:43 +0100 (MET) Received: from tcs01.inf.tu-dresden.de ([127.0.0.1]) by localhost (mail.tcs.inf.tu-dresden.de [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 06415-08 for ; Fri, 13 Jan 2006 11:23:43 +0100 (MET) Received: from ithif59.inf.tu-dresden.de (ithif59.inf.tu-dresden.de [141.76.75.59]) by mail.tcs.inf.tu-dresden.de (Sun Java System Messaging Server 6.1 HotFix 0.06 (built Nov 11 2004)) with ESMTPS id <0IT100KM70VJNM00@mail.tcs.inf.tu-dresden.de> for caml-list@inria.fr; Fri, 13 Jan 2006 11:23:43 +0100 (MET) Received: from tews by ithif59.inf.tu-dresden.de with local (Exim 4.50) id 1ExM5v-00031y-Pa for caml-list@inria.fr; Fri, 13 Jan 2006 11:23:43 +0100 Date: Fri, 13 Jan 2006 11:23:43 +0100 From: Hendrik Tews Subject: Re: [Caml-list] Coinductive semantics In-reply-to: <1137102848.3681.268.camel@rosella> To: caml-list@inria.fr Message-id: MIME-version: 1.0 Content-type: text/plain; charset=us-ascii Content-transfer-encoding: 7BIT X-Virus-Scanned: amavisd-new at tcs.inf.tu-dresden.de References: <43BD6418.4090407@barettadeit.com> <43BE6CAB.2030503@andrej.com> <43C3963D.5030601@tsc.uc3m.es> <1136981974.8962.100.camel@rosella> <43C51C33.2000206@andrej.com> <1137031853.3681.138.camel@rosella> <43C661AF.2080404@andrej.com> <1137102848.3681.268.camel@rosella> User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.4 X-Miltered: at concorde with ID 43C77FB0.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43C77FB0.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; hendrik:01 tews:01 tews:01 caml-list:01 coinductive:01 semantics:01 algebra:01 theorems:01 algebra:01 set-:01 functor:01 nat:01 nat:01 sequences:01 hendrik: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 Dear skaller, please read some of the relevant paper, for instance the tutorial on (Co)Algebras and (Co)Induction. First, you agree the ideas are dual .. and that's a formal mathematical statement that the very definitions are obtainable from each other by a mechanical application of the duality principle -- provided the definitions are stated formally enough of course. Please read the relevant definitions. Coalgebras are the duals of algebras _but_ coalgebra morphisms are not the duals of algebra morphisms. Otherwise the theory of coalgebras would be void. Because most interesting properties/definitions are connected with the morphisms you get that the theory of algebras is _not_ dual to the theory of coalgebras. To take a simpler example, I simply say in some category X with products, and perhaps some extra structure, you can dualise any set of theorems to obtain another theory. The same clearly applies to initial and final algebras, and ALL other dual concepts -- that's the whole POINT of duality. This is completely wrong. If you dualize an initial algebra you get a final coalgebra, _but in Set^op, (ie, dualized Set)_. Nobody is interested in final coalgebras in Set^op. People are interested in finial coalgebras in _Set_, which are the same as initial algebras in Set^op. Take for instance the (set-) functor F(X) = (X x nat) + 1, where x is product, + is disjoint union, 1 is a one-element set. The initial algebras for it are the finite lists over nat. The final coalgebra for it are sequences over nat, that is finite and infinite list over nat. Do you see the difference? This difference makes coalgebras interesting. dual -- they are, necessarily. The problem is that before duality was considered bodies of theories arose from different considerations that were not in fact dual i the literature, Sorry, you make yourself a fool here. Go out, read the papers on the Co-Birkhoff theorem! Then you'll see that duality was always considered by all authors on that subject. The point is that when you dualize the Birkhoff theorem you don't get a theorem on coalgebras! Bye, Hendrik PS. Sorry if I missed some of your points, I did not read all of your prose.