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.