UNIVERSAL CO-ALGEBRA AND THEORETICAL COMPUTER SCIENCE

H. Peter Gumm

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

State based and object oriented systems may be described in the same way, but this requires that the state is explicitly modeled as a sort. From the viewpoint of the programmer, however, it is intended that the state should be "hidden" with only certain features accessible through attributes and methods. The real drawback is that this way two states may be distinguished, even if to the outside this distinction can never be observed. It has recently been discovered that state based systems such as transition systems, automata, lazy data structures and objects give rise to structures dual to universal algebra, which are called co-algebras. Equality is replaced by indistinguishability and co-induction replaces induction as proof principle. However, it turns out that one has to look at universal algebra from a more general perspective (using elementary category theoretic notions) before the dual concept of co-algebra is able to capture the relevant applications.

In our course we give an introduction to this fascinating theory which is still in an early phase of development. The (preliminary) outline of the four lectures is:

1. Data Types, Systems and Models
   • Modelling Data Types as Universal Algebras. Examples, Initial Semantics, Equality, Proofs by Induction.
   • State Based Systems and Infinite Data Objects. Examples, Final Semantics, Observational equivalence, Proofs by Co-Induction.
   • The Concept of Co-Algebra. Preliminary Definition and Examples, Homomorphisms, Substructures, Congruences.
2. Categories of Co-Algebras
   • Basic Notions of Category Theory. Category of Sets, Functors, Limits, Colimits.
   • Categories of Co-Algebras. Diagrams, Factorizations, Preservation Theorems.
   • Colimits and some Limits of Co-Algebras. Sums, Pushouts, Equalizers.
3. Structure Theory
   • Bisimulations. Motivation, Bisimilarity, Bisimulations.
   • Final Models. Examples, Adequacy, Existence.
   • Co-free Co-Algebras. Definition, Existence, Applications.
4. Special Functors and Logics for Co-Algebra
   • Co-Varieties. Closure operators, Conjunct Sums, Co-free Co-Algebras and Co-Varieties.
   • Logic for Co-Algebras. Co-Equations, Modal interpretation, Birkhoff's Theorem.
   • Special Functors. Weak pullbacks, "Non-Standard" Functors, Hypersystems.