Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Coinductive semantics
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ 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.