Re: [Caml-list] Coinductive semantics

[Andrej Bauer <Andrej.Bauer@andrej.com>]

Alessandro Baretta wrote:
> I am very much ashamed of myself for discovering that I simply I have no clue as 
> to what the terms "algebra" and "co-algebra" mean, formally. I take the first to 
> be an algebraic structure with a single set and any number of operations--within 
> this definition the notion of initial algebra can be interpreted without 
> difficulty

Yes, that's what algebras are, except that you may also impose equations
that operations are supposed to satisfy (such as associativity).

> --but what in the world is the second? I can't think of anything 
> different, really: a set and some operations. Even the definition of final 
> co-algebras can be easily interpreted in this definition.

As my advisor once explained: algebras are about putting things
together--take two numbers and "put them together" with an operation,
take an element and a list and put them together to form a new list.
Coalgebras are about taking things apart--take a stream and decompose it
into the head and the tail, take a binary tree and decompose it into its
left and right subtrees, take a Markov process and "decompose" it into
its first transition and the rest of the process, etc. So, in this sense
coalgebras still are sets with operations, you are perfectly right.
Perhaps we could say that algebras have constructors and coalgebras have
"deconstructors".

What may be confusing is that a final coalgebra is also an algebra. For
example, the coalgebraic structure of (finite and infinite) binary trees
may be described by the operation

  take_apart : tree -> (unit | tree * tree)

which takes a tree and returns either (), signifying the tree cannot be
taken apart (the empty tree), or a pair (l,r) where l and r are the left
and the right subtrees, respectively. By Lambek's Lemma take_apart is an
isomorphism. Its inverse (still acting on infinite and finite trees)

  put_together : (unit | tree * tree) -> tree

is best seen as a pair of constructors: put_together () gives a tree
without any subtrees (the empty tree), whereas put_together (l,r) is the
tree whose left and right subtrees are l and r, respectively.

Exercise for skaller ;-): using basic duality, derive the fact that
every initial algebra is also a colagebra, and give an example. How does
this allow us to relate an initial algebra (finite trees) and the
corresponding final coalgebra (infinite and finite trees)?

> So, is it true that algebras and co-algebras are the same beasts, except that 
> when referring to algebras we implicitly declare interest in inductive 
> properties of initial structures, and when referring to co-algebras we imply 
> interest in the co-inductive properties of final structures?

Both algebras and coalgebras are sets with operations. The difference is
in what these operations are doing (constructors vs. deconstructors) and
what properties they have (induction vs. coinduction).

Andrej