[Prev][Next][Index][Thread]
Paper announcement
The following technical report is now
available at ftp.cwi.nl as pub/CWIreports/AP/CS-R9652.ps.Z
(also via http://www.cwi.nl/~janr).
J.J.M.M. Rutten
Universal coalgebra: a theory of systems.
Technical Report CS-R9652, CWI, Amsterdam, 1996.
Abstract:
In the semantics of programming, finite data types such as finite
lists, have traditionally been modelled by initial algebras. Later
final coalgebras were used in order to deal with infinite data types.
Coalgebras, which are the dual of algebras, turned out to be suited,
moreover, as models for certain types of automata and more generally,
for (transition and dynamical) systems.
An important property of initial algebras is that they satisfy the
familiar principle of induction. Such a principle was missing for
coalgebras until the work of Aczel (1988) on a theory of
non-wellfounded sets, in which he introduced a proof principle
nowadays called coinduction. It was formulated in terms of
bisimulation, a notion originally stemming from the world of
concurrent programming languages (Milner, 1980; Park, 1981). Using
the notion of coalgebra homomorphism, the definition of bisimulation
on coalgebras can be shown to be formally dual to that of congruence
on algebras (Aczel and Mendler, 1989).
Thus the three basic notions of universal algebra: algebra,
homomorphism of algebras, and congruence, turn out to correspond to:
coalgebra, homomorphism of coalgebras, and bisimulation, respectively.
In this paper, the latter are taken as the basic ingredients of a
theory called universal coalgebra. Some standard results from
universal algebra are reformulated (using the afore mentioned
correspondence) and proved for a large class of coalgebras, leading to
a series of results on, e.g., the lattices of subcoalgebras and
bisimulations, simple coalgebras and coinduction, and a covariety
theorem for coalgebras similar to Birkhoff's variety theorem.
AMS Subject Classification (1991): 68Q10, 68Q55
CR Subject Classification (1991): D.3.1, F.1.2, F.3.2
Keywords and Phrases: Coalgebra, algebra, dynamical system, transition
system, bisimulation, universal coalgebra, universal algebra,
congruence, homomorphism, induction, coinduction.