Coalgebra (NWIIMC036), fall 2016
Lecturers:
Jurriaan Rot,
Aleks Kissinger,
Julian Salamanca
General information on this course can be found in the
studiegids.
Contents of this course webpage
 A solution to exercise 4 of homework assignment 2 is here.
 Homework assignment 2 is here. The deadline is Friday 13 January. You can hand it in by email, or in the exercise class.
 Both the locations for the lecture and the exercise class have changed after the break (and the location for the exercise class is different in the first week)! Please check the schedule page carefully.
 Homework assignment 1 is here. The deadline is Monday 7 November. You can hand it in by email, or in the lecture.
 The final exam has been rescheduled to Wednesday 25 January 2017, 12:3015:30.

Please register in blackboard for this course in order to receive (email)
announcements. Relevant course information will be provided here (and
not in blackboard).
 The course runs officially in weeks 3542 and 4551 of 2016, and week 2 of 2017.
 Lectures take place in HFML0220 (location for weeks 4551,2) on Mondays 15:45  17:30
(previously HG00.086, location for weeks 3542))
 Exercise classes take place in E2.12 (week 45) and HG00.086 (week 4651, 2) on Fridays 10:45  12:30
(previously HG01.058, location for weeks 3542).
 Lectures will be in taught in English.
 The final exam will be held on Wednesday 25 January 2017, 12:3015:30, in HG00.304.
We will follow Bart Jacobs' draft book, available here. We also use 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. Pointers to the relevant literature
are in the Lectures Overview section below.
We also recommend the tutorial on coalgebras and coinduction by Bart Jacobs and Jan Rutten. See here.
 Basic theory of coalgebras and coinduction (8 lectures, weeks 3542)
 streams
 categories and coalgebras
 bisimulation and coinduction
 automata
 Algebra and coalgebra (3 lectures, weeks 4547)
 algebras, monads
 distributive laws
 Bisimulation and coinduction: advanced topics (4 lectures, weeks 4851)
 relation lifting
 coinduction and lattices
 minimization, proof techniques & algorithms, applications
Details for each lecture and suggested exercises will be posted here during the course.
 Lecture 1, Monday 29 Aug, 15:4517:30, in HG00.086
 Topic: Course overview, introduction to coalgebra, first examples.
No exercise class on Friday 2 Sep
 Lecture 2, Monday 5 Sept, 15:4517:30, in HG00.086
 Topic: Streams and coinduction
 Defining streams.
 Proving equivalence with bisimulation and coinduction.
 Stream systems.
 Literature: Section 2 of [Rutten05]: Jan Rutten. A tutorial on coinductive stream calculus and signal flow graphs. Theoretical Computer Science 343, Elsevier, see here.
Exercise class, Friday 9 Sept, 10:4512:30, in HG01.058
 See here for the exercises. There are a few pointers to section 2 of [Rutten05], which also contains the background material; it will be useful to bring a copy to the exercise class.
 Lecture 3, Monday 12 Sept, 15:4517:30, in HG00.086
 Topic: Polynomial functors and their coalgebras
 Functorial constructions on sets.
 Functors (on sets), polynomial functors.
 Coalgebras for a functor.
 Literature: Section 2.2 (and a bit of 2.1) of [Jacobs].
Exercise class, Friday 16 Sept, 10:4512:30, in HG01.058
 See here for the exercises.
 Lecture 4, Monday 19 Sept, 15:4517:30, in HG00.086
 Topic: Categories, functors, coalgebras
 Categories, functors.
 Initial and final objects.
 The category of coalgebras; definition final coalgebra.
 Literature: Section 1.4 (and a bit of 2.1) of [Jacobs].
Exercise class, Friday 23 Sept, 10:4512:30, in HG01.058
 See here for the exercises.
 Lecture 5, Monday 26 Sept, 15:4517:30, in HG00.086
 Topic: Final coalgebras
 Definition, examples.
 Final coalgebra is an isomorphism.
 Coinduction for streams, revisited
 Literature: Section 2.3 (and 1.2) of [Jacobs].
Exercise class, Friday 30 Sept, 10:4512:30, in HG01.058
 See here for the exercises.
 Lecture 6, Monday 3 Oct, 15:4517:30, in HG00.086
 Topic: Bisimulations
 Definition, examples.
 Coinduction.
 Bisimulations on automata.
 Literature: material of the lecture. As reference material, you can consult J. Rutten: Universal Coalgebra, available here.
Exercise class, Friday 7 Oct, 10:4512:30, in HG01.058
 See here for the exercises.
 Lecture 7, Monday 10 Oct, 15:4517:30, in HG00.086
 Topic: Automata and coinduction
 Automata as coalgebras, language semantics.
 The final coalgebra.
 Language equality with bisimulations and coinduction.
 Literature: Section 2.3.3, Prop. 2.3.5, Section 3.4 of [Jacobs]
Exercise class, Friday 14 Oct, 10:4512:30, in HG01.058
 See here for the exercises.
 Lecture 8, Monday 17 Oct, 15:4517:30, in HG00.086
 Topics:
 Language equality with bisimulation up to congruence.
 Bisimilarity of transition systems.
 Nondeterministic automata.
 Literature: this note for the first part. For the second part: your notes of the lecture. Part of it is in Section 2.2.4 of [Jacobs];
for (coalgebraic) bisimilarity of labelled transition systems, see Example 2.1 of J. Rutten: Universal Coalgebra, available here (the example continues later in Section 2).
Exercise class, Friday 21 Oct, 10:4512:30, in HG01.058
 See here for the exercises.
 Lecture 9, Monday 7 Nov, 15:4517:30, in HFML0220
 Topics
 Algebras.
 Algebraic data types.
 Recursion.
 Literature: notes. For some froglists, see the code, which runs in Isabelle.
Exercise class, Friday 11 Nov, 10:4512:30, in E2.12
 The exercises are included in the above notes.
 Lecture 10, Monday 14 Nov, 15:4517:30, in HFML0220
 Topics
 Terms as initial algebras.
 Natural transformations.
 Monads.
 Literature: notes.
Exercise class, Friday 18 Nov, 10:4512:30, in HG00.086
 The exercises are included in the above notes.
 Lecture 11, Monday 21 Nov, 15:4517:30, in HFML0220
 Topics
 Distributive laws.
 Constructions on coalgebras.
 Determinisation.
 Literature: notes.
Exercise class, Friday 25 Nov, 10:4512:30, in HG00.086
 See here for the exercises.
 Lecture 12, Monday 28 Nov, 15:4517:30, in HFML0220
 Topics
 Lattices.
 Coinduction in a lattice.
 Upto techniques.
 Literature: notes.
Exercise class, Friday 2 Dec, 10:4512:30, in HG00.086
 See here for the exercises.
 Lecture 13, Monday 5 Dec, 15:4517:30, in HFML0220
 Topics
 Induction in a lattice.
 Latticetheoretic coinduction as coalgebraic coinduction.
 Relation lifting, HermidaJacobs bisimulations.
 Literature: notes.
Exercise class, Friday 9 Dec, 10:4512:30, in HG00.086
 See here for the exercises.
 Lecture 14, Monday 12 Dec, 15:4517:30, in HFML0220
 Topics
 Greatest bisimulation of automata.
 Kleene fixed point theorem.
 Final sequence.
 Literature: notes for the first part; for the second part (on the final sequence of a functor) see Section 4.6 of [Jacobs].
Exercise class, Friday 16 Dec, 10:4512:30, in HG00.086
 See here for the exercises.
 Lecture 15, Monday 19 Dec, 15:4517:30, in HFML0220
 Topic: Equations for Deterministic automata
 Lecturer: Julian Salamanca
 Literature: notes
No exercise class on Friday 25 Dec.
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 students will learn how to combine coinduction and induction to derive effective specification and reasoning techniques for automata. 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,
the course will be selfcontained:
only basic definitions will be needed, and these will be
introduced as part of the course.
There will a final exam, and two extended homework assignments, the first due by the end of October,
and the second in January.
The final grade will be the maximum of (H+E)/2 and E, where H is the grade given for the homework
assignments and E is the grade given for the final exam.