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 42234BB81 for ; Wed, 11 Jan 2006 15:54:12 +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 k0BEsBVS002244 for ; Wed, 11 Jan 2006 15:54:11 +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 PAA28148 for ; Wed, 11 Jan 2006 15:54:10 +0100 (MET) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0BEs9Ld004362 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Wed, 11 Jan 2006 15:54:10 +0100 Received: from theo.dagstuhl.de ([192.76.146.31] helo=[192.168.11.178]) by haka.fmf.uni-lj.si with esmtpa (Exim 4.50) id 1EwhMR-0006gh-HQ; Wed, 11 Jan 2006 15:54:08 +0100 Message-ID: <43C51C33.2000206@andrej.com> Date: Wed, 11 Jan 2006 15:54:43 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Debian Thunderbird 1.0.7 (X11/20051017) X-Accept-Language: en-us, en MIME-Version: 1.0 To: skaller Cc: caml-list@inria.fr References: <43BD6418.4090407@barettadeit.com> <43BE6CAB.2030503@andrej.com> <43C3963D.5030601@tsc.uc3m.es> <1136981974.8962.100.camel@rosella> In-Reply-To: <1136981974.8962.100.camel@rosella> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 192.76.146.31 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com Subject: Re: [Caml-list] Coinductive semantics X-SA-Exim-Version: 4.2 (built Thu, 03 Mar 2005 10:44:12 +0100) X-SA-Exim-Scanned: Yes (on haka.fmf.uni-lj.si) X-Miltered: at concorde with ID 43C51C13.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 43C51C11.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 coinductive:01 semantics:01 wrote:01 theorem:01 theorem:01 translate:04 indicates:04 hughes:06 duality:07 duality:07 theory:07 theory:07 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 skaller wrote: > And of course, separate development of these things is fairly > silly, since as the 'co' indicates the two ideas are formally > dual. This is claim is completely false. The theory of final coalgebras is NOT just a dual of the theory of initial algebras. While it is true that final coalgebras and inital algebras are dual concepts, it is far from truth that we may translate results about one to results about others by applying simple duality. This would only be the case if we studied algebras and coalgebras in self-dual categories, which usually we do not (only very special kinds of categories are self-dual). For example, the famous Birkhoff theorem about universal algebras says something about initial algebras. It took a Ph.D. (by Jesse Hughes) to figure out what the dual of Birkhoff's theorem might be. And believe me this was not because either Jesse or his advisor failed to "apply a simple duality principle". Andrej