An Introduction to the Theory of Coalgebras
Abstract:
This course gives an introduction to the theory of coalgebras. In the recent
years, coalgebras, the formal dual of algebras, have been recognised as
foundational models in a wide range of areas. Applications include infinite
(i.e. possibly non well-founded) data types, state based systems, operational
semantics, automata theory, modal logics, and abstract models of infinite
computations.
The goal of the lecture is to familiarise the audience with the basic concepts
of the field and to provide a solid basis for further research. Apart from the
basic concepts, we cover definitions and proofs by coinduction and logics for
reasoning about coalgebras in detail.
We begin with examining concrete examples of coalgebras, such as transition
systems, in order to motivate the general definitions. Using basic
category theory (which we keep to a minimum), we introduce coalgebras,
homomorphisms and behavioural equivalence. Using categorical duality, we
make the algebra / coalgebra duality explicit, which allows to transfer many
ideas and techniques from universal algebra.
We use this transfer principle to obtain two important techniques:
definitions and proofs by coinduction. In order to obtain coinductive
definition principles, we formulate induction in terms of algebras and then
apply duality. This way, we obtain coiteration, primitive corecursion and
course-of-value corecursion as definition principles, each of which we
illustrate by examples. Concerning proofs by coinduction, we discuss two
different methods: The bisimulation proof method and proofs by terminal
sequence induction, an inductive method for establishing behavioural
equalities.
Viewing coalgebras as state based systems, we then present logics, which can
be used to reason about coalgebras. We identify semantical structures, which
allow us to interpret multimodal logics over coalgebras. We concentrate on two
main aspects of logics for coalgebras: expressivity (aka Hennessy-Milner
property) and complete axiomatisations. We show, how coinductive
techniques enable us to prove corresponding theorems.