A Tutorial on (Co)Algebras and (Co)Induction

Algebraic structures which are generated by a collection of constructors| like natural numbers (generated by a zero and a successor) or nite lists and trees| are of well-established importance in computer science. Formally, they are initial algebras. Induction is used both as a de nition principle, and as a proof principle for such structures. But there are also important dual\coalgebraic" structures, which do not come equipped with constructor operations but with what are sometimes called\destructor" operations (also called observers, accessors, transition maps, or mutators). Spaces of in nite data (including, for example, in nite lists, and non-well-founded sets) are generally of this kind. In general, dynamical systems with a hidden, black-box state space, to which a user only has limited access via speci ed (observer or mutator) operations, are coalgebras of various kinds. Such coalgebraic systems are common in computer science. And\coinduction" is the appropriate technique in this coalgebraic context, again both as a de nition principle and as a proof principle. The latter involves bisimulations. It is the aim of this tutorial to provide a brief introduction to this relatively new eld of coalgebra.

rivista o collana

 Bulletin of the European Association for Theoretical Computer Science (EATCS Bulletin)