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

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 Subject: Re: [Caml-list] Coinductive semantics
```Dear skaller,

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.

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
coalgebras!

Bye,

Hendrik

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