Coalgebra (NWI-IMC036), fall 2018

Lecturers: Jurriaan Rot, Aleks Kissinger

General information on this course can be found in the studiegids.


Contents of this course webpage


Announcements


Dates, Time and Location


Course Material

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, hand-outs, 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.


Structure


Lectures Overview

Details for each lecture and suggested exercises will be posted here during the course.
  1. Lecture 1, Monday 3 September, 13:30-15:15, in MERC I 00.28 No exercise class on Thursday 6 Sept
  2. Lecture 2, Monday 10 September, 13:30-15:15, in MERC I 00.28 Exercise class, Thursday 13 Sept, 13:30-15:15, in MERC I 00.28
  3. Lecture 3, Monday 17 September, 13:30-15:15, in MERC I 00.28 Exercise class, Thursday 20 Sept, 13:30-15:15, in MERC I 00.28
  4. Lecture 4, Monday 24 September, 13:30-15:15, in MERC I 00.28
  5. Exercise class, Thursday 27 Sept, 13:30-15:15, in MERC I 00.28
  6. Lecture 5, Monday 1 October, 13:30-15:15, in MERC I 00.28
  7. Exercise class, Thursday 4 Oct, 13:30-15:15, in MERC I 00.28
  8. Lecture 6, Monday 8 October, 13:30-15:15, in MERC I 00.28
  9. Exercise class, Thursday 11 Oct, 13:30-15:15, in MERC I 00.28
  10. Lecture 7, Monday 15 October, 13:30-15:15, in MERC I 00.28
  11. Exercise class, Thursday 18 Oct, 13:30-15:15, in MERC I 00.28

Course Description and Prerequisites

Course description:

State-based 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 state-based 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, ever-growing 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 self-contained: only basic definitions will be needed, and these will be introduced as part of the course.


Grading

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.