Universal coalgebra - a theory of state based systems
by
H. Peter Gumm
Philipps Universität Marburg

Data Structures arising in programming have for a long time been modeled by universal algebras. If specifications are presented as equations or implications, a natural candidate for the intended semantics is the initial (free 0-generated) algebra. This adds to the specifying axioms convenient rules for recursive definitions and inductive proofs.

If state based and object oriented systems are to be described algebraically, the state must be explicitly modeled as a special sort X. From the user's viewpoint, however, the state ought to be ``hidden'' with only certain features accessible through attributes and methods. Thus, the algebraic modelling distinguishes states even though their difference may be never observable. Other drawbacks of the universal algebraic approach is that it cannot deal with nondeterministic operations of distributed programming, nor with infinite objects such as streams in functional programming.

It has recently been discovered that state based systems such as transition systems, automata, lazy data structures and objects (in the sense of object oriented programming) give rise to structures dual to universal algebras, so called co-algebras. Equality is replaced by indistinguishability and induction is replaced by by co-induction as a proof principle. In order to discover the co-algebraic nature, one first needs to look at universal algebra from a slightly more general perspective, using elementary category theoretic notions: A type is just a functor F : Set --> Set, and a universal algebra of type F is a map f^A: F(A) --> A. Dually, a coalgebra of type F is simply any map g_A : A --> F(A).

As a benefit of this more general approach, a whole new range of applications open up, reaching from state based, nondeterministic, and partial systems to dynamical systems and topological spaces. Still, most of the relevant structure theory (analogous to that of universal algebra) can be obtained. With a very mild condition on the type functor (F should be ``accessible'') we even get the Birkhoff variety theorem. But the theory is not just a simple minded dual to universal algebra. Structures such as e.g. bisimulations, that don't have a classical counterpart in universal algebra, but that are well known from computer science, figure prominently in the new theory. Substructures are not only closed under arbitrary unions - as might be expected in a dual theory - but also under finite intersections.

In our lecture we shall give some motivations and glimpses at the general theory of coalgebras, and we discuss its applicability in computer science.

http://www.mathematik.uni-marburg.de/~gumm

Date received: June 7, 2000

Copyright © 2000 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # caee-92.