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 Thu, 20060112 at 15:03 +0100, Andrej Bauer wrote: > Dear skaller, > > with all due respect, you are being silly here. I am quite familiar with > research in initial algebras and final coalgebras. I am a researcher > myself. I know. > May I ask what experience you have with present research > directions in inital algebra and final coalgebras? Very little, apart from reading occasional papers I don't understand :) But I don't think I'm being silly, I think you just misunderstood my point. Even ordinary people are capable of reasoning, and academics often can't see the wood for the trees. In this case it seems simple  to me anyhow. The ideas are dual, the theories should be symmetrical, if they're not then its the theories that are out of whack and need to be fixed. Just as, for example, C++ is unbalanced, because it has good support for products (structs) but lacks proper sums. So again, when you said: "The theory of final coalgebras is NOT just a dual of the theory of initial algebras." I consider you wrong, because your statement is about history  and mine is an axiom. Mine isn't about the current state of the art  its about where it should be going KNOWING that the theories are necessarily symmetrical. We can speculate about why products are understood better than sums, why there's been more research into functional than stateful programming: the history of mathematics is fascinating. It's kind of like the discussion of 'void'. Your argument at that time just showed my inability to express myself ;( You said Ocaml was an expression language and so unit was the right type for a statement  and so missed the point that one could  and I WAS  arguing that Ocaml is not a functional language, and if we're arguing about changes to make it better, you cannot sensibly turn around and argue statements can't be void *because* it uses a syntactic form appropriate for a language semantics it doesn't have in the first place: given the mismatch another way to fix the problem is to change it so it some syntactic forms are considered statements, and then your argument evaporates. It's quite possible to do that, I have done it in Felix, and I have seen it done in other languages developed by world renowned experts (including many examples from Reynolds, and Jays FISh: FISh used 'command' as the type of a statement, rather than 'void', so there's an additional argument about whether void  which has a functional interpretation  can be used instead: recall I conceded it was a hack, but appeared to work in practice anyhow, at least in a language like Felix with extensional polymorphism) The problem here is communication of subtle things like intent and viewpoint. As in this case, where what YOU mean by 'the theory' seems to me to be different to what I mean  I can't believe we could disagree on the underlying mathematics  you'd be right every time on that I'm sure. But it isn't just a matter of the actual formal facts, but their context. Please read again the interchange: >> 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 initial algebras are dual >concepts, it is far from truth that we may translate results about one >to results about others by applying simple duality. 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. And then you say the theories are not  yet theories are nothing more than the bodies of theorems derived from a given set of axioms and particular inference rules: here the rules are invariant so it follows immediately the theories ARE in fact NECESSARILY dual, and indeed derivable from each other by mechanical application of the duality. I do not require a PhD to do basic logical reasoning  and it turns out I just paraphrased Maclane anyhow :) You go on to explain that the systems are not studied in selfdual categories .. which is the wood for the trees problem. It isn't relevant, except historically, and I myself made a comment (which I paraphrase having deleted the email) that this may lead to theorems in an unfamiliar setting, which could be a difficulty. In citing the case of dualising Birkhoff being hard work you have just confirmed this  but your conclusion that my claim is false is quite unjustified  and that's because you seems to have incorrectly assumed my arguments applied only within a single setting  which I did not. [I'm saying they SHOULD apply in a single setting .. and citing the fact this isn't the case as the actual problem!] 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. I didn't say about the same category!!! Obviously!! Since the dual categories have sums not products. But it is certainly a dual theory by construction. The same clearly applies to initial and final algebras, and ALL other dual concepts  that's the whole POINT of duality. So perhaps you can now see what I was really saying? That the PROBLEM isn't the mathematical theories are not 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, and that at least for the purpose of studying programming languages the lack of symmetry is ITSELF the real problem. There's no way to construct a good programming language that isn't fully symmetrical  that's my opinion. It is based on intuition, its only an opinion, and I might be convinced otherwise: as I mentioned some people  perhaps many here  believe purely functional programming is the answer. I do not. So I'm left believing you can't read my English as I intend  probably because I just can't express my ideas succinctly. You say something I said is 'completely false' when in fact the claim is a belief about where research should be heading to get what I want  a decent programming language. Therefore, it isn't a statement of the kind for which you can reasonably say it is false: it isn't an argument in the mathematical sense where mathematical reasoning could be wrong, nor is it a fact of nature to be disputed, but an opinion about what research is needed to achieve my goals. You would be free to counterclaim by saying my belief was misguided, and appreciated if you explained why  since as you say that's actually YOUR area of research. For example, having said that symmetry WOULD be obtained if studies were restricted to selfdual categories, perhaps you'd care to explain why doing that is NOT a good idea, for the purpose of eventually obtaining a decent programming language?? That's a genuine question  what I learned started off with distributive categories (ones with all finite sums and products and a distributive law), and they ARE selfdual, are they not? The whole Sydney School uses them as the basis of studying programming. (You can understand my viewpoint then, having studied at Sydney .. :) Are such categories too weak? Does this mean we must pick instead just ONE of the theories or the other? Would one be better for a programming language and why? [This may well be the case because programming languages are not independent of human psychology] Finally  I wish to show why your claim about selfdual categories is misguided: "The duality principle also applies to statements involving several categories and functors between them."  Saunders MacLane, Categories for the Working Mathematician, Page 32. Wood for trees: it doesn't make any difference whether the categories are self dual or not. The 'theories' are constructed in complex *systems* and again my point is that the systems within which initial and final algebras are studies may well have been different, perhaps for historical reasons, and perhaps by demand of some particular application  my claim is that is NOT the case for study of programming languages: if the systems aren't symmetrical, and you take as an axiom they should be, it FOLLOWS that scientists interested in programming languages should be trying to find a symmetrical system. So as far as I can see it is all very simple: everything follows from the one Platonistic belief that programming languages should be symmetrical, and they should scale to all levels of application  from systems programming to building GUIs, networks and databases. At least more symmetrical than we have now! And my own experience confirms this  Ocaml is MUCH better than C++ because it provides good support for both products and sums, C++ does not. Symmetry matters. It is a key guiding principle, and responsible for most of the major breakthroughs in theoretical physics. We surely need something similar in programming theory.  John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net