Coalgebra (NWI-IMC036), 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

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

Announcements

• 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:30-15: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).

Dates, Time and Location

• The course runs officially in weeks 35-42 and 45-51 of 2016, and week 2 of 2017.
• Lectures take place in HFML0220 (location for weeks 45-51,2) on Mondays 15:45 - 17:30 (previously HG00.086, location for weeks 35-42))
• Exercise classes take place in E2.12 (week 45) and HG00.086 (week 46-51, 2) on Fridays 10:45 - 12:30 (previously HG01.058, location for weeks 35-42).
• Lectures will be in taught in English.
• The final exam will be held on Wednesday 25 January 2017, 12:30-15:30, in HG00.304.

Course Material

We will follow Bart Jacobs' draft book, available here. 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 (8 lectures, weeks 35-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 29 Aug, 15:45-17:30, in HG00.086
   • Topic: Course overview, introduction to coalgebra, first examples.
No exercise class on Friday 2 Sep
2. Lecture 2, Monday 5 Sept, 15:45-17: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:45-12: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.
3. Lecture 3, Monday 12 Sept, 15:45-17: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:45-12:30, in HG01.058
• See here for the exercises.
4. Lecture 4, Monday 19 Sept, 15:45-17: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:45-12:30, in HG01.058
• See here for the exercises.
5. Lecture 5, Monday 26 Sept, 15:45-17: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:45-12:30, in HG01.058
• See here for the exercises.
6. Lecture 6, Monday 3 Oct, 15:45-17: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:45-12:30, in HG01.058
• See here for the exercises.
7. Lecture 7, Monday 10 Oct, 15:45-17: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:45-12:30, in HG01.058
• See here for the exercises.
8. Lecture 8, Monday 17 Oct, 15:45-17:30, in HG00.086
   • Topics:
     • Language equality with bisimulation up to congruence.
     • Bisimilarity of transition systems.
     • Non-deterministic 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:45-12:30, in HG01.058
• See here for the exercises.
9. Lecture 9, Monday 7 Nov, 15:45-17: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:45-12:30, in E2.12
• The exercises are included in the above notes.
10. Lecture 10, Monday 14 Nov, 15:45-17:30, in HFML0220
    • Topics
      • Terms as initial algebras.
      • Natural transformations.
      • Monads.
    • Literature: notes.
Exercise class, Friday 18 Nov, 10:45-12:30, in HG00.086
• The exercises are included in the above notes.
11. Lecture 11, Monday 21 Nov, 15:45-17:30, in HFML0220
    • Topics
      • Distributive laws.
      • Constructions on coalgebras.
      • Determinisation.
    • Literature: notes.
Exercise class, Friday 25 Nov, 10:45-12:30, in HG00.086
• See here for the exercises.
12. Lecture 12, Monday 28 Nov, 15:45-17:30, in HFML0220
    • Topics
      • Lattices.
      • Coinduction in a lattice.
      • Up-to techniques.
    • Literature: notes.
Exercise class, Friday 2 Dec, 10:45-12:30, in HG00.086
• See here for the exercises.
13. Lecture 13, Monday 5 Dec, 15:45-17:30, in HFML0220
    • Topics
      • Induction in a lattice.
      • Lattice-theoretic coinduction as coalgebraic coinduction.
      • Relation lifting, Hermida-Jacobs bisimulations.
    • Literature: notes.
Exercise class, Friday 9 Dec, 10:45-12:30, in HG00.086
• See here for the exercises.
14. Lecture 14, Monday 12 Dec, 15:45-17: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:45-12:30, in HG00.086
• See here for the exercises.
15. Lecture 15, Monday 19 Dec, 15:45-17:30, in HFML0220
    • Topic: Equations for Deterministic automata
    • Lecturer: Julian Salamanca
    • Literature: notes
No exercise class on Friday 25 Dec.

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