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: 2006-01-13 (10:23)
From: Hendrik Tews <tews@t...>
Subject: Re: [Caml-list] Coinductive semantics
Dear skaller,

please read some of the relevant paper, for instance the tutorial
on (Co)Algebras and (Co)Induction.

   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.
Please read the relevant definitions. Coalgebras are the duals of
algebras _but_ coalgebra morphisms are not the duals of algebra
morphisms. Otherwise the theory of coalgebras would be void.
Because most interesting properties/definitions are connected
with the morphisms you get that the theory of algebras is _not_
dual to the theory of coalgebras.

   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.
   The same clearly applies to initial and final algebras,
   and ALL other dual concepts -- that's the whole POINT of duality.
This is completely wrong. If you dualize an initial algebra you
get a final coalgebra, _but in Set^op, (ie, dualized Set)_.
Nobody is interested in final coalgebras in Set^op. People are
interested in finial coalgebras in _Set_, which are the same as
initial algebras in Set^op.

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.

   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. Go out, read the papers on
the Co-Birkhoff theorem! Then you'll see that duality was always
considered by all authors on that subject. The point is that when
you dualize the Birkhoff theorem you don't get a theorem on



PS. Sorry if I missed some of your points, I did not read all of
your prose.