Equational Definability of Some Classes of Coalgebras

Robert Goldblatt

Certain kinds of coalgebra have proven useful in the modelling of features of object-oriented programming languages [3, 2]. The kind we consider has a non-empty set X of states (which may be thought of as the possible realisations of some notion of object), and a set of method operations m : X × I^{m} → X and attribute functions a : X × I^{a} → O^{a}, where I^{m} and I^{a} are sets of inputs and O^{a} a set of outputs or observable values.

A calculus of terms for these coalgebras is developed using variables and constants for members of input and output sets, symbols for methods and attributes, and a special state symbol σ which may be thought of as a parameter denoting the “current” state. An observable equation t_{1} ≈ t_{2} has terms t_{1} and t_{2} taking observable values.

The ultrafilter enlargement of a coalgebra A is defined as a new coalgebra whose states are certain “rich” ultrafilters on the state set of A. These ultrafilters are required to contain special sets of states defined by observable equations. It is shown that

a class of coalgebras is definable by Boolean combinations of observable equations if and only if it is closed under disjoint unions, ultrafilter enlargements, and domains and images of coalgebraic morphisms (or equivalently, images of bisimulation relations).

This may be viewed as a coalgebraic analogue of Birkhoff’s characterisation of equationally definable classes of algebras by closure under homomorphic images, subalgebras, and direct products.

[1] Robert Goldblatt. What is the Coalgebraic Analogue of Birkhoff’s Variety Theorem? Research Report 99–34, School of Mathematical and Computing Sciences, Victoria University of Wellington, December 1999.

[2] Bart Jacobs. Objects and Classes, Coalgebraically. In B. Freitag, C. B. Jones, C. Lengauer, and H.-J. Schek, editors, Object-Orientation with Parallelism and Persistence, pages 83–103. Kluwer Academic Publishers, 1996.

[3] Horst Reichel. An Approach to Object Semantics Based on Terminal Co-Algebras. Mathematical Structures in Computer Science, 5:129–152, 1995.

Address: School of Mathematical and Computing Sciences, Victoria University, P. O. Box 600, Wellington, New Zealand

E-mail: Rob.Goldblatt@vuw.ac.nz