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 ABE6ABB81 for ; Fri, 13 Jan 2006 15:42:28 +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 k0DEgShr017105 for ; Fri, 13 Jan 2006 15:42:28 +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 PAA05958 for ; Fri, 13 Jan 2006 15:42:27 +0100 (MET) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0DEgPPj007054 for ; Fri, 13 Jan 2006 15:42:26 +0100 Received: from rosella (ppp33-253.lns1.syd6.internode.on.net [59.167.33.253]) by smtp3.adl2.internode.on.net (8.13.5/8.13.5) with ESMTP id k0DEgMjr062005; Sat, 14 Jan 2006 01:12:23 +1030 (CST) (envelope-from skaller@users.sourceforge.net) Subject: Re: [Caml-list] Coinductive semantics From: skaller To: Hendrik Tews Cc: caml-list@inria.fr In-Reply-To: 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> Content-Type: text/plain Date: Sat, 14 Jan 2006 01:42:22 +1100 Message-Id: <1137163342.3681.533.camel@rosella> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 43C7BC54.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 43C7BC51.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 coinductive:01 semantics:01 hendrik:01 tews:01 algebra:01 andrej:01 set-:01 functor:01 nat:01 nat:01 sequences:01 neck:98 bush:98 lambda: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 On Fri, 2006-01-13 at 11:23 +0100, Hendrik Tews wrote: > Dear skaller, > This is completely wrong. If you dualize an initial algebra you > get a final coalgebra, _but in Set^op, (ie, dualized Set)_. Indeed. > Nobody is interested in final coalgebras in Set^op. Why not? This is really the key point of misunderstanding I think. I'm not disputing your claim, I'm asking why not? Perhaps they should be? The dual of a vector space is a space of functionals, and is independently useful and interesting. Why doesn't this apply to programming languages as well? Andrej actually answered that here: "Whenever C is useful for modelling programming languages, C^op is useless" "The symmetries that you want are not there, provably." Why? Why is C^op useless for all possible C that are useful for modelling programming languages? For example an answer like "The distributive law is required in C and never holds in C^op" would be an answer (not claiming it is the case just trying to illustrate the kind of answer I would like to see). > 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. Yet somehow Charity has both and supports both symmetrically and seamlessly, more or less as I would desire. So perhaps what I need (as a programmer) isn't what I asked for (the client has genuine needs but doesn't know what they are.. the client asks for X, but really needs Y .. the expert gives them Y anyhow :) > 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. Why (are you sorry about a fault that is clearly mine)? The court jester or fool was an important contributor to social cohesion. Some fool like me who risks looking stupid .. and look at all the good information now coming out! I'm sure I'm not the only one to appreciate it. Most people wouldn't risk looking stupid .. I did. I'm willing to stick my neck out. But I do take exception to being accused of trying to 'badmouth' a group of people who I have great respect for -- mathematicians and especially category theorists. Even if I were to say research direction was on the wrong track, right or wrong I wouldn't be trying to badmouth anyone (I'll reserve that for John Howard and George Bush :) > Go out, read the papers on > the Co-Birkhoff theorem! That's a pretty big ask of someone who isn't a category theorist isn't it? Most mathematicians can't understand category theory .. and I'm just an ordinary programmer :) > Then you'll see that duality was always > considered by all authors on that subject. Hmm .. correct me if I'm wrong, but weren't initial algebras studied well before final coalgebras? Perhaps even before category theory existed? I would have thought there were quite a few term calculi around, such as formal polynomials, lambda calculus, etc .. and it seems to me the study of coalgebras is newer. -- John Skaller Felix, successor to C++: http://felix.sf.net