Lecturers:
Alexandra Silva and
Sam Staton.
General information on this course can be found in the
studiegids.
Contents of this course webpage

Please register in blackboard for this course in order to receive (email)
announcements. Relevant course information will be provided here (and
not in blackboard).
 Exercise sheet 1 is here: [pdf]. Deadline: Tues 21 Oct. (Minor clarifications added to exercises on Tues 14 Oct.)
Handwritten solutions are recommended. Please deliver to Sam Staton's pigeon hole or his office (Mercator 03.02).
 Exercise sheet 2 is here: [pdf]. Deadline: Wdnesday 14 Jan.
Handwritten solutions are recommended. Please deliver to Alexandra's pigeon hole(first floor) or by email (as a pdf).
 The course runs officially in weeks 3651 in 2014, and weeks 23 of 2015.
 Lectures take place in HG01.028 on Tuesdays 15:30  17:30.
 Lectures will be in taught in English.
 The exam will be on Friday 30 Jan 2015, 8:30  11:30 in HG00.308.
We will be follow Bart Jacobs' draft book, available here. We might give additional material, such as slides, handouts, and
research papers on coalgebra. All material will be made available electronically
via this webpage, or distributed during class.
We also recommend the tutorial on coalgebras and coinduction by Bart Jacobs and Jan Rutten. See here.
Note: The course will be taught in English.
 Lecture 1, Tuesday 2 Sep, 15:3017:30, in LIN4
 Topic: Course overview, introduction to coalgebra, examples.
 Lecture 2, Tuesday 9 Sep, 15:3017:30, in HG01.028
 Topic: Coalgebras for polynomial functors.
Section 2.2 of Jacobs' book.
 Arities and Coalgebras for arities. Homomorphisms of coalgebras for arities.
 Functors on sets and coalgebras for functors. Homomorphisms of coalgebras for functors on sets.
 Natural bijections between functors.
 Suggested exercises and preparation:
 Exercises 2.2.2, 2.2.4, 1.1.1 in Jacobs' book.
 Check that the definition of "arity functor" satisfies the conditions for functors.
 Define a bijective correspondence between coalgebras for an arity and coalgebras for the corresponding arity functor. Likewise for coalgebra homomorphisms.
 Find all the natural bijections from the functor ()^{3} to itself.
 Revise concepts: functions, disjoint union, bijections, function composition.
 Learn a proof of the 'currying' bijection.
 Lecture 3, Tuesday 16 Sep, 15:3017:30, in HG01.028
 Topic: Coalgebras for functors.
Section 1.4 of Jacobs' book.
 Categories and functors. The free category on a graph.
 Coalgebras for a functor on a category.
The category of coalgebras for a functor.
 Definition: final object in a category.
 Suggested exercises and preparation:
 Fix a finite set Sigma.
Define a functor on Sets that takes a set X to the set 2 x P(X)^{Sigma}, where P is the powerset construction. A coalgebra for this functor is a nondeterministic automaton, but what does it mean for a function to be a coalgebra homomorphism?
 Show that every polynomial functor is naturally isomorphic to an arity functor.
 Consider two functors on sets, F and G, that are in natural bijection. Show that the category of Fcoalgebras is isomorphic to the category of Gcoalgebras.
 Finish 2.2.4(ii).
 Write out an equational calculation to check that morphisms of coalgebras compose.
 For those who took the course on category theory last year:
describe translations between the definition of category in that course
(with one big collection of morphisms) and
my definition of category (with a collection
of morphisms Mor(X,Y) for all objects X and Y).
 Lecture 4, Tuesday 23 Sep, 15:3017:30, in HG01.028
 Topic: Final coalgebras.
Sections 2.3 and 1.2 of Jacobs' book.
 Final objects in categories. Isomorphisms in categories. Final objects
are unique up to unique isomorphism.
 Lambek's lemma: the structure morphism of a final coalgebra is an isomorphism.
 The final Zx() coalgebra and coinductive definitions and reasoning about streams.
 Suggested exercises and preparation:
 Again:
Define a functor on Sets that takes a set X to the set 2 x P(X)^{Sigma}, where P is the powerset construction. A coalgebra for this functor is a nondeterministic automaton, but what does it mean for a function to be a coalgebra homomorphism?
 Check that inverses to isomorphisms are always unique.
 Finish checking that the final Zx() coalgebra is indeed final.
 Exercise 1.3.5 in Jacobs' book.
 Lecture 5, Tuesday 30 Sep, 15:3017:30, in HG01.028
 Topic: Algebras.
Section 2.4 Jacobs' book.
 Algebras for an arity. Terms for an arity.
 Algebras for a functor. Algebras for an arity functor; universal property
of disjoint union (coproduct).
 Dual (opposite) categories. Algebras versus coalgebras. Initial objects versus final objects. Algebras for a functor form a category; Lambek's lemma for initial algebras.
 Terms for an arity form an initial algebra. Inductive definitions from
initiality. Informal comparison with final coalgebra for an arity.
 Suggested exercises and preparation:
 Check the details of the universal property of disjoint union.
 Describe explicitly what is meant by a homomorphism between algebras for an arity.
 Finish checking that terms form an initial algebra.
 Lecture 6, Tuesday 7 October, 15:3017:30, in HG01.028
 Topic: Automata as coalgebras; relation lifting.
Part of the paper Automata and Coinduction (pdf). Section 3.1 Jacobs' book.
 Deterministic finite automata as coalgebras.
 Bisimulation and coinduction principle for automata.
 Relation lifiting and Jacobs/Hermida bisimulation for Kripke polynomial functors.
 Suggested exercises:
 Prove the coinduction principle for automata.
 Give the definition of relation lifting for coproduct and powerset.
 Exercises 3.1.1 and 3.1.2 from the book.
 Lecture 7, Tuesday 14 October, 15:3017:30, in HG01.028
 Topic: Concrete coinduction proofs. Section 3.4 Jacobs' book.
 Regular expressions as automata.
 Bisimulation proofs for language equivalence.
 Upto techniques.
 Suggested exercises:
 Exercises 3.4.43.4.7 from the book.
 Lecture 8, Tuesday 21 October, 15:3017:30, in HG01.028
 Topic: Properties of bisimulations. Section 3.2 Jacobs' book.
 Preservation properties of relation lifting.
 Closure properties of bisimulations (Proposition 3.2.6).
 Suggested exercises:
 Show that relation lifting  Rel(F)  for a Kripke polynomial functor F, forms a functor in the category REL, with sets as objects and binary relations as arrows.
 Exercises 3.2.1(i), 3.2.5, and 3.2.7 from the book.
 Lecture 9, Tuesday 11 November, 15:3017:30, in HG01.028
 Topic: Different definitions of bisimulation. Section 3.3 Jacobs' book.
 AczelMendler bisimulation.
 Bisimulations as spans and cospans.
 Equivalence of AczelMendler and HermidaJacobs for Kripke polynomial functors.
 Suggested exercises:
 Dualize the Aczel Mendler definition from bisimulations to congruences of algebras.
 Complete the proof of Theorem 3.3.1.
 Exercises 3.3.2 and 3.3.3 from the book.
 Lecture 10, Thursday 13 November, 10:3012:30, in HG00.307
 Topic: Brzozowski minimization algorithm. See here for the research paper in which the lecture was based. The missing proof from the lecture is here.
 Brzozowski algorithm.
 Contravariant powerset construction to do reverse and determinization.
 Reachbility and Observability.
 Proof of correctness using initial and final coalgebras.
 Suggested exercises:
 Define the functor B^ (contravariant on functions).
 A Moore automaton is an automaton with outputs in a set B instead of 2, like deterministic automata. Describe reverse and determinize using B^ for a Moore automaton.
 What is the final coalgebra for the Moore automata functor?
 Draw an example of a Moore automaton and apply reverse and determinize once.
 Lecture 11, Tuesday 25 November, 15:3017:30, in HG01.028.
 Topic:Monads, natural transformations, computational effects. Section 5.1 Jacobs' book. See here for the proof of the monad laws for the distribution monad (due to Rik, thanks!).
 Natural transformations: definitions and examples.

Monad: definition and examples.
 Lift, powerset and distribution monad.
 Suggested exercises:
 Show that the mu and eta we defined for distribution are indeed natural transformations.
 Define and prove that PP (double powerset) is a monad.
 Define the list monad ()^*.
 For a fixed set A, the functor ()^A is a monad (called the input/reader monad in Haskell). Define it and prove the monad laws.
 Exercises 5.1.2 and 5.1.3 of the book.
 Lecture 12, Tuesday 2 December, 15:3017:30, in HG01.028.
 Topic: Algebras for a monad, EilenbergMoore category. Section 5.4 Jacobs' book.
 Algebras for a monad: definitions and examples.
 Pointed sets, join semilattices.
 Vector spaces.
 Suggested exercises:
 Given a vector space W over the reals show that it is an algebra for the monad V() defined on objects as V(X) = { phi : Reals^X  support of phi is finite}, on arrows and monad laws are the same as for the distribution monad (see last lecture) .
 Show that any algebra for the monad V() is indeed a vector space. (that is, it satisfy the vector space laws).
 Show that given any set B and monad T, the set T(B) carries an algebra structure.
 Exercises 5.4.5 (ii) and 5.4.9 (ii) and (iii) of the book.
 Lecture 13, Tuesday 9 December, 15:3017:30, in HG01.028.
 Topic: Generalized powerset construction, language semantics of nondeterminsitic automata. See here and here for material on this topic.
 Generalized subset construction for coalgebras: definition.
 Coalgebraic language semantics (if final coalgebra exists). Connection to bisimilarity.
 Examples: nondeterministic automata, partial and weighted automata.
 Suggested exercises:
 Recall the nondeterministic automaton example from the lecture. How can one change the algebra structure on the output set 2 in order to achieve the following language semantics: a word is accepted by a state in an NFA if and only if every path labelled by the word leads to a final state.
 Show that if X and Y both have a Talgebra structure, for a given monad T, then also the cartesian product XxY and exponential X^A have a Talgebra structure.
 Show that given a coalgebra for the functor [0,1] x D()^A, where D is the subdistribution monad, one can define the semantics of such a coalgebra in terms of languages [0,1]^{A^*}.
 Lecture 14, Tuesday 16 December, 15:3017:30, in HG01.028.
 Topic: Recap, exercises on bisimulation, algebras for a monad and determinization. See here for the list of exercises.
Course description:
Statebased systems are used widely in computer science
to model concrete systems such as digital hardware,
software programs, and distributed systems.
Coalgebra is a unifying framework for
studying the behaviour of statebased systems.
In coalgebra,
a system is viewed as a black box where knowledge of the system's
state can only be obtained by observing the external behaviour.
In particular,
two states s and t are considered equivalent
if whenever we run the system starting in state s,
the observed behaviour is the same as when we run the system in
starting in state t.
The type of observations and transitions in the
external behaviour is specified by the system type.
The theory of universal coalgebra
provides general definitions of observable behaviour and bisimilarity
that can be instantiated for concrete system types,
as well as a powerful and fascinating reasoning principle called
coinduction (a notion
that is dual to the well known induction principle).
This course is an introduction to coalgebra.
The course starts by studying how various types of systems can be modelled as
coalgebras, and how coinduction can be applied to them.
These systems include basic datatypes,
such as infinite streams and trees, and many types
of automata (deterministic, nondeterministic, probabilistic, ...).
Next, a number of fundamental notions
such as language equivalence of automata,
bisimilarity of processes, and
determinisation of nondeterministic automata,
will be treated coalgebraically.
The coalgebraic framework will then be used to obtain
generalisations of these constructions to other types of systems.
Coalgebra is a rather recent field of research, existing for
a mere two decades,
and it is attracting an enthusiastic, evergrowing community.
Being relatively young, it still has many elementary and exciting
research questions to offer.
Prerequisites:
We only assume basic knowledge of automata, formal languages
and propositional logic, for example, as covered in the courses
Talen en Automaten, Discrete Wiskunde, Beweren en Bewijzen, en
Semantiek en Correctheid.
With respect to category theory and modal logic,
the course will be selfcontained:
Only basic definitions will be needed, and these will be
introduced as part of the course.
The final grade will be the 0.3 * H1+ 0.3 * H2 + 0.4 * E,
where H1 and H2 are the grade given for the two exntended homework assignments
and E is the grade given for the final exam.