Coalgebra (NWIIMC036), fall 2018
Lecturers:
Jurriaan Rot,
Aleks Kissinger
General information on this course can be found in the
studiegids.
Contents of this course webpage
 Homework assignment 2 is here. The deadline is Friday 21 December. You can hand it in by email, in class, or in my mailbox.
 Homework assignment 1 is here. The deadline is Monday 5 November. You can hand it in by email, or in the lecture.

Please register for this course in order to receive (email)
announcements. Relevant course information will be provided here.
 The course runs officially in weeks 3642 and 4551 of 2018.
 Lectures take place in MERC I 00.28 on Mondays 13:30  15:15
 Exercise classes take place in MERC I 00.28 on Thursdays 13:30  15:15
 Lectures will be in taught in English.
 The final exam will be held on Friday 11 January 2019, 12:3015:30, in HG00.108.
 There will be two assignments, which also count towards the final grade and are
mandatory, one halfway during the course and one by the end. These will be announced in due time.
For general information about coalgebras see Bart Jacobs' book,
a draft of which is available here
(referred to as [Jacobs] below),
or Jan Rutten's draft book
(referred to as [Rutten] below).
We will refer to parts of both books.
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 (7 lectures, weeks 3642)
 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 3 September, 13:3015:15, in MERC I 00.28
 Topic: Course overview, introduction to coalgebra, first examples.
 Literature: slides (first part), notes
(second part). Optional, for more background: Preface and section 1.1 of [Jacobs], Chapter 6 of
[Rutten].
No exercise class on Thursday 6 Sept
 Lecture 2, Monday 10 September, 13:3015:15, in MERC I 00.28
 Topic: Streams and coinduction
 Defining streams.
 Proving equivalence with bisimulation and coinduction.
 Stream systems.
 Literature: 7.1  7.4 of [Rutten], for now excluding the parts we haven't covered, in particular the stuff on bisimulations of stream systems in 7.1. Theorem 96 in 7.4 is the same as our coinduction principle: the relation ~ is defined
by s ~ t iff there is a bisimulation containing (s,t).)
Exercise class, Thursday 13 Sept, 13:3015:15, in MERC I 00.28
 See here for the exercises (small update in 1b, 13 sept). If you can't get enough of it, there's plenty more in [Rutten]...
 Lecture 3, Monday 17 September, 13:3015:15, in MERC I 00.28
 Topic: Coalgebras for Set functors
 Functorial constructions.
 Functors on Set, polynomial functors.
 Coalgebras for a functor.
 Literature: 2.2 and a bit of 2.1 in [Jacobs]; also, for the first part, see section 1.4 of the tutorial by Jacobs and Rutten
Exercise class, Thursday 20 Sept, 13:3015:15, in MERC I 00.28
 See here for the exercises

Lecture 4, Monday 24 September, 13:3015:15, in MERC I 00.28
 Topic: Categories
 Categories, functors.
 Isomorphisms.
 Initial and final objects, (co)products.
 Literature: Section 1.4 (and most of 2.1) of [Jacobs].
Exercise class, Thursday 27 Sept, 13:3015:15, in MERC I 00.28
 See here for the exercises

Lecture 5, Monday 1 October, 13:3015:15, in MERC I 00.28
 Topic: Final coalgebras
 Definition, examples.
 Lambek's lemma.
 Automata as coalgebras.
 Literature: Section 2.3 (and 1.2) of [Jacobs].
Exercise class, Thursday 4 Oct, 13:3015:15, in MERC I 00.28
 See here for the exercises (4 Oct: small update in ex 1 and 7)

Lecture 6, Monday 8 October, 13:3015:15, in MERC I 00.28
 Topic: Bisimulations
 Definition, examples.
 Coinduction.
 Language equivalence of automata.
 Literature: notes
Exercise class, Thursday 11 Oct, 13:3015:15, in MERC I 00.28
 See here for the exercises

Lecture 7, Monday 15 October, 13:3015:15, in MERC I 00.28
 Topic: Nondeterministic systems
 Labelled transition systems, bisimilarity.
 Nondeterministic automata and determinisation, coalgebraically.
 Language equivalence.
 Literature: notes (Section 3 wasn't really covered; this
will be treated in a later lecture)
Exercise class, Thursday 18 Oct, 13:3015:15, in MERC I 00.28
 See here for the exercises

Lecture 8, Monday 5 November, 13:3015:15, in MERC I 00.28
 Topic: Algebras
 Algebras for a functor.
 Algebraic data types, recursion.
 Natural transformations.
 Literature: notes
Exercise class, Thursday 8 Nov, 13:3015:15, in MERC I 00.28
 Exercises are included in the lecture notes

Lecture 9, Monday 12 November, 13:3015:15, in MERC I 00.28
 Topic: Monads
 Terms as an initial algebra.
 Monads.
 Kleisli category of a monad.
 Literature: notes.
Also, here is the Isabelle code. (It can be read in a text editor and run in
Isabelle.
The first time Isabelle opens, it takes a really long time because its got to build the libraries, but after that its fine.)
Exercise class, Thursday 15 Nov, 13:3015:15, in MERC I 00.28
 Exercises are included in the lecture notes

Lecture 10, Monday 19 November, 13:3015:15, in MERC I 00.28
 Topic: Algebra and Coalgebra for Regular Expressions
 Brzozowski derivatives.
 Equivalence of regular expressions.
 Language equivalence with bisimulation up to congruence.
 Literature: notes
Exercise class, Wednesday 21 Nov, 8:3010:15, in HG00.068
 See here for the exercises

Lecture 11, Monday 26 November, 13:3015:15, in MERC I 00.28
 Topic: Lattices and Coinduction
 Lattices.
 Coinduction in a lattice.
 Upto techniques.
 Literature: notes
Exercise class, Wednesday 28 Nov, 8:3010:15, in HG00.068
 See here for the exercises

Lecture 12, Monday 3 December, 13:3015:15, in MERC I 00.28
 Topic: Induction; Coinduction in Lattices and Categories
 Induction.
 Latticetheoretic and categorical (co)induction.
 Relation lifting, HermidaJacobs bisimulations.
 Literature: notes
Exercise class, Thursday 6 Dec, 13:3015:15, in MERC I 00.28
 See here for the exercises; and here
for a solution to exercise 5

Lecture 13, Monday 10 December, 13:3015:15, in MERC I 00.28
 Topic: Final sequence
 Greatest bisimulation of automata.
 Kleene fixed point theorem.
 Final sequence of a functor.
 Literature: notes
for the first half; for the second half, see section 4.6 of [Jacobs].
Exercise class, Thursday 13 Dec, 13:3015:15, in MERC I 00.28
 See here for the exercises

No lecture on Monday 17 December.
Exercise class, Thursday 20 Dec, 13:3015:15, in MERC I 00.28
 We'll do a bit of recap, organised around some 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 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 (completely separate from
the weekly homework, which is not graded), the first due around the end of October,
and the second in January.
The final grade will be given by (H+E)/2, where H is the grade given for the homework
assignments and E is the grade given for the final exam.