Coinductive semantics
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  skaller <skaller@u...> 
Subject:  Re: [Camllist] Coinductive semantics 
On Fri, 20060113 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 oneelement 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 CoBirkhoff 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 <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net