Coinductive semantics
[
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: [Camllist] Coinductive semantics 
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 "coalgebra" mean, formally. I take the first to > be an algebraic structure with a single set and any number of operationswithin > 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 > coalgebras can be easily interpreted in this definition. As my advisor once explained: algebras are about putting things togethertake 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 aparttake 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 coalgebras are the same beasts, except that > when referring to algebras we implicitly declare interest in inductive > properties of initial structures, and when referring to coalgebras we imply > interest in the coinductive 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