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 8866BBBBB for ; Sat, 14 Jan 2006 17:52:52 +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 k0EGqpxh005495 for ; Sat, 14 Jan 2006 17:52:51 +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 RAA24203 for ; Sat, 14 Jan 2006 17:52:50 +0100 (MET) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0EGqme7005487 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Sat, 14 Jan 2006 17:52:50 +0100 Received: from bsn-77-186-71.dsl.siol.net ([193.77.186.71] helo=[192.168.1.101]) by haka.fmf.uni-lj.si with esmtpa (Exim 4.50) id 1Exodt-0003wd-6n; Sat, 14 Jan 2006 17:52:47 +0100 Message-ID: <43C92C8F.6000805@andrej.com> Date: Sat, 14 Jan 2006 17:53:35 +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: Alessandro Baretta , Caml list 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> <43C7838F.1090306@andrej.com> <43C7B17A.1070503@barettadeit.com> In-Reply-To: <43C7B17A.1070503@barettadeit.com> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 193.77.186.71 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 43C92C63.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43C92C60.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 baretta:01 algebra:01 algebra:01 binary:01 subtrees:01 constructors:01 coalgebraic:01 binary:01 subtrees:01 isomorphism: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 Alessandro Baretta wrote: > I am very much ashamed of myself for discovering that I simply I have no clue as > to what the terms "algebra" and "co-algebra" mean, formally. I take the first to > be an algebraic structure with a single set and any number of operations--within > this definition the notion of initial algebra can be interpreted without > difficulty Yes, that's what algebras are, except that you may also impose equations that operations are supposed to satisfy (such as associativity). > --but what in the world is the second? I can't think of anything > different, really: a set and some operations. Even the definition of final > co-algebras can be easily interpreted in this definition. As my advisor once explained: algebras are about putting things together--take two numbers and "put them together" with an operation, take an element and a list and put them together to form a new list. Coalgebras are about taking things apart--take a stream and decompose it into the head and the tail, take a binary tree and decompose it into its left and right subtrees, take a Markov process and "decompose" it into its first transition and the rest of the process, etc. So, in this sense coalgebras still are sets with operations, you are perfectly right. Perhaps we could say that algebras have constructors and coalgebras have "deconstructors". What may be confusing is that a final coalgebra is also an algebra. For example, the coalgebraic structure of (finite and infinite) binary trees may be described by the operation take_apart : tree -> (unit | tree * tree) which takes a tree and returns either (), signifying the tree cannot be taken apart (the empty tree), or a pair (l,r) where l and r are the left and the right subtrees, respectively. By Lambek's Lemma take_apart is an isomorphism. Its inverse (still acting on infinite and finite trees) put_together : (unit | tree * tree) -> tree is best seen as a pair of constructors: put_together () gives a tree without any subtrees (the empty tree), whereas put_together (l,r) is the tree whose left and right subtrees are l and r, respectively. Exercise for skaller ;-): using basic duality, derive the fact that every initial algebra is also a colagebra, and give an example. How does this allow us to relate an initial algebra (finite trees) and the corresponding final coalgebra (infinite and finite trees)? > So, is it true that algebras and co-algebras are the same beasts, except that > when referring to algebras we implicitly declare interest in inductive > properties of initial structures, and when referring to co-algebras we imply > interest in the co-inductive properties of final structures? Both algebras and coalgebras are sets with operations. The difference is in what these operations are doing (constructors vs. deconstructors) and what properties they have (induction vs. coinduction). Andrej