[
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: | Andrej Bauer <Andrej.Bauer@a...> |
| Subject: | Re: [Caml-list] Coinductive semantics |
Your main observation seems to be this: algebras in a category C are dual to coalgebras in the opposite category C^op. Leaving further insults aside, let me explain why this observation does not help much. In order to have a category C which is a useful model of computation, the category C must have certain properties (such as being cartesian closed so that we can interpret lambda calculus in it). Also, one cannot use _two_ categories C and D and model some features in C, others in D, and hope to get a coherent picture which tells how the features interact with each other. Whenever C is useful for modelling programming languages, C^op is useless. While it is true that whatever you prove about algebras in C corresponds to something about coalgebras in C^op, this tells you absolutely nothing about coalgebras in C. Since C is what we care about, we then need to study coalgebras in C separately. The symmetries that you want are not there, provably. Believe me, what you are suggesting is trivial and researchers know precisely to what amount it works. Andrej