Coalgebra (NWI-IMC036), fall 2018

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

Contents of this course webpage

• Announcements
• Dates, Time and Location
• Course Material
• Structure
• Lectures Overview
• Course Description and Prerequisites
• Grading

Announcements

• 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.

Dates, Time and Location

• The course runs officially in weeks 36-42 and 45-51 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:30-15: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.

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

• Basic theory of coalgebras and coinduction (7 lectures, weeks 36-42)
  • streams
  • categories and coalgebras
  • bisimulation and coinduction
  • automata
• Algebra and coalgebra (3 lectures, weeks 45-47)
  • algebras, monads
  • distributive laws
• Bisimulation and coinduction: advanced topics (4 lectures, weeks 48-51)
  • relation lifting
  • coinduction and lattices
  • minimization, proof techniques & algorithms, applications

Lectures Overview

1. Lecture 1, Monday 3 September, 13:30-15: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
2. Lecture 2, Monday 10 September, 13:30-15: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:30-15: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]...
3. Lecture 3, Monday 17 September, 13:30-15: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:30-15:15, in MERC I 00.28
   • See here for the exercises
4. Lecture 4, Monday 24 September, 13:30-15: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:30-15:15, in MERC I 00.28
• See here for the exercises
5. Lecture 5, Monday 1 October, 13:30-15: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:30-15:15, in MERC I 00.28
• See here for the exercises (4 Oct: small update in ex 1 and 7)
6. Lecture 6, Monday 8 October, 13:30-15:15, in MERC I 00.28
   • Topic: Bisimulations
     • Definition, examples.
     • Coinduction.
     • Language equivalence of automata.
   • Literature: notes
Exercise class, Thursday 11 Oct, 13:30-15:15, in MERC I 00.28
• See here for the exercises
7. Lecture 7, Monday 15 October, 13:30-15:15, in MERC I 00.28
   • Topic: Non-deterministic systems
     • Labelled transition systems, bisimilarity.
     • Non-deterministic 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:30-15:15, in MERC I 00.28
• See here for the exercises
8. Lecture 8, Monday 5 November, 13:30-15: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:30-15:15, in MERC I 00.28
• Exercises are included in the lecture notes
9. Lecture 9, Monday 12 November, 13:30-15: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:30-15:15, in MERC I 00.28
• Exercises are included in the lecture notes
10. Lecture 10, Monday 19 November, 13:30-15: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:30-10:15, in HG00.068
• See here for the exercises
11. Lecture 11, Monday 26 November, 13:30-15:15, in MERC I 00.28
    • Topic: Lattices and Coinduction
      • Lattices.
      • Coinduction in a lattice.
      • Up-to techniques.
    • Literature: notes
Exercise class, Wednesday 28 Nov, 8:30-10:15, in HG00.068
• See here for the exercises
12. Lecture 12, Monday 3 December, 13:30-15:15, in MERC I 00.28
    • Topic: Induction; Coinduction in Lattices and Categories
      • Induction.
      • Lattice-theoretic and categorical (co)induction.
      • Relation lifting, Hermida-Jacobs bisimulations.
    • Literature: notes
Exercise class, Thursday 6 Dec, 13:30-15:15, in MERC I 00.28
• See here for the exercises; and here for a solution to exercise 5
13. Lecture 13, Monday 10 December, 13:30-15: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:30-15:15, in MERC I 00.28
• See here for the exercises
14. No lecture on Monday 17 December.
Exercise class, Thursday 20 Dec, 13:30-15:15, in MERC I 00.28
• We'll do a bit of recap, organised around some exercises.

Course Description and Prerequisites

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