Lecturers: Alexandra Silva and Sam Staton.

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

Contents of this course webpage

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

Announcements

• Please register in blackboard for this course in order to receive (email) announcements. Relevant course information will be provided here (and not in blackboard).

• Exercise sheet 1 is here: [pdf]. Deadline: Tues 21 Oct. (Minor clarifications added to exercises on Tues 14 Oct.)

  Handwritten solutions are recommended. Please deliver to Sam Staton's pigeon hole or his office (Mercator 03.02).

• Exercise sheet 2 is here: [pdf]. Deadline: Wdnesday 14 Jan.

  Handwritten solutions are recommended. Please deliver to Alexandra's pigeon hole(first floor) or by email (as a pdf).

Dates, Time and Location

• The course runs officially in weeks 36-51 in 2014, and weeks 2-3 of 2015.
• Lectures take place in HG01.028 on Tuesdays 15:30 - 17:30.
• Lectures will be in taught in English.
• The exam will be on Friday 30 Jan 2015, 8:30 - 11:30 in HG00.308.

Course Material

Lectures Overview

1. Lecture 1, Tuesday 2 Sep, 15:30-17:30, in LIN4
   • Topic: Course overview, introduction to coalgebra, examples.
2. Lecture 2, Tuesday 9 Sep, 15:30-17:30, in HG01.028
   • Topic: Coalgebras for polynomial functors. Section 2.2 of Jacobs' book.
   • Arities and Coalgebras for arities. Homomorphisms of coalgebras for arities.
   • Functors on sets and coalgebras for functors. Homomorphisms of coalgebras for functors on sets.
   • Natural bijections between functors.
   • Suggested exercises and preparation:
   • Exercises 2.2.2, 2.2.4, 1.1.1 in Jacobs' book.
   • Check that the definition of "arity functor" satisfies the conditions for functors.
   • Define a bijective correspondence between coalgebras for an arity and coalgebras for the corresponding arity functor. Likewise for coalgebra homomorphisms.
   • Find all the natural bijections from the functor (-)³ to itself.
   • Revise concepts: functions, disjoint union, bijections, function composition.
   • Learn a proof of the 'currying' bijection.
3. Lecture 3, Tuesday 16 Sep, 15:30-17:30, in HG01.028
   • Topic: Coalgebras for functors. Section 1.4 of Jacobs' book.
   • Categories and functors. The free category on a graph.
   • Coalgebras for a functor on a category. The category of coalgebras for a functor.
   • Definition: final object in a category.
   • Suggested exercises and preparation:
   • Fix a finite set Sigma. Define a functor on Sets that takes a set X to the set 2 x P(X)^Sigma, where P is the powerset construction. A coalgebra for this functor is a non-deterministic automaton, but what does it mean for a function to be a coalgebra homomorphism?
   • Show that every polynomial functor is naturally isomorphic to an arity functor.
   • Consider two functors on sets, F and G, that are in natural bijection. Show that the category of F-coalgebras is isomorphic to the category of G-coalgebras.
   • Finish 2.2.4(ii).
   • Write out an equational calculation to check that morphisms of coalgebras compose.
   • For those who took the course on category theory last year: describe translations between the definition of category in that course (with one big collection of morphisms) and my definition of category (with a collection of morphisms Mor(X,Y) for all objects X and Y).
4. Lecture 4, Tuesday 23 Sep, 15:30-17:30, in HG01.028
   • Topic: Final coalgebras. Sections 2.3 and 1.2 of Jacobs' book.
   • Final objects in categories. Isomorphisms in categories. Final objects are unique up to unique isomorphism.
   • Lambek's lemma: the structure morphism of a final coalgebra is an isomorphism.
   • The final Zx(-) coalgebra and coinductive definitions and reasoning about streams.
   • Suggested exercises and preparation:
   • Again: Define a functor on Sets that takes a set X to the set 2 x P(X)^Sigma, where P is the powerset construction. A coalgebra for this functor is a non-deterministic automaton, but what does it mean for a function to be a coalgebra homomorphism?
   • Check that inverses to isomorphisms are always unique.
   • Finish checking that the final Zx(-) coalgebra is indeed final.
   • Exercise 1.3.5 in Jacobs' book.
5. Lecture 5, Tuesday 30 Sep, 15:30-17:30, in HG01.028
   • Topic: Algebras. Section 2.4 Jacobs' book.
   • Algebras for an arity. Terms for an arity.
   • Algebras for a functor. Algebras for an arity functor; universal property of disjoint union (coproduct).
   • Dual (opposite) categories. Algebras versus coalgebras. Initial objects versus final objects. Algebras for a functor form a category; Lambek's lemma for initial algebras.
   • Terms for an arity form an initial algebra. Inductive definitions from initiality. Informal comparison with final coalgebra for an arity.
   • Suggested exercises and preparation:
   • Check the details of the universal property of disjoint union.
   • Describe explicitly what is meant by a homomorphism between algebras for an arity.
   • Finish checking that terms form an initial algebra.
6. Lecture 6, Tuesday 7 October, 15:30-17:30, in HG01.028
   • Topic: Automata as coalgebras; relation lifting. Part of the paper Automata and Coinduction (pdf). Section 3.1 Jacobs' book.
   • Deterministic finite automata as coalgebras.
   • Bisimulation and coinduction principle for automata.
   • Relation lifiting and Jacobs/Hermida bisimulation for Kripke polynomial functors.
   • Suggested exercises:
   • Prove the coinduction principle for automata.
   • Give the definition of relation lifting for coproduct and powerset.
   • Exercises 3.1.1 and 3.1.2 from the book.
7. Lecture 7, Tuesday 14 October, 15:30-17:30, in HG01.028
   • Topic: Concrete coinduction proofs. Section 3.4 Jacobs' book.
   • Regular expressions as automata.
   • Bisimulation proofs for language equivalence.
   • Up-to techniques.
   • Suggested exercises:
   • Exercises 3.4.4-3.4.7 from the book.
8. Lecture 8, Tuesday 21 October, 15:30-17:30, in HG01.028
   • Topic: Properties of bisimulations. Section 3.2 Jacobs' book.
   • Preservation properties of relation lifting.
   • Closure properties of bisimulations (Proposition 3.2.6).
   • Suggested exercises:
   • Show that relation lifting - Rel(F) - for a Kripke polynomial functor F, forms a functor in the category REL, with sets as objects and binary relations as arrows.
   • Exercises 3.2.1(i), 3.2.5, and 3.2.7 from the book.
9. Lecture 9, Tuesday 11 November, 15:30-17:30, in HG01.028
   • Topic: Different definitions of bisimulation. Section 3.3 Jacobs' book.
   • Aczel-Mendler bisimulation.
   • Bisimulations as spans and co-spans.
   • Equivalence of Aczel-Mendler and Hermida-Jacobs for Kripke polynomial functors.
   • Suggested exercises:
   • Dualize the Aczel Mendler definition from bisimulations to congruences of algebras.
   • Complete the proof of Theorem 3.3.1.
   • Exercises 3.3.2 and 3.3.3 from the book.
10. Lecture 10, Thursday 13 November, 10:30-12:30, in HG00.307
    • Topic: Brzozowski minimization algorithm. See here for the research paper in which the lecture was based. The missing proof from the lecture is here.
    • Brzozowski algorithm.
    • Contravariant powerset construction to do reverse and determinization.
    • Reachbility and Observability.
    • Proof of correctness using initial and final coalgebras.
    • Suggested exercises:
    • Define the functor B^- (contravariant on functions).
    • A Moore automaton is an automaton with outputs in a set B instead of 2, like deterministic automata. Describe reverse and determinize using B^- for a Moore automaton.
    • What is the final coalgebra for the Moore automata functor?
    • Draw an example of a Moore automaton and apply reverse and determinize once.
11. Lecture 11, Tuesday 25 November, 15:30-17:30, in HG01.028.
• Topic:Monads, natural transformations, computational effects. Section 5.1 Jacobs' book. See here for the proof of the monad laws for the distribution monad (due to Rik, thanks!).
• Natural transformations: definitions and examples.
• Monad: definition and examples.
• Lift, powerset and distribution monad.
• Suggested exercises:
• Show that the mu and eta we defined for distribution are indeed natural transformations.
• Define and prove that PP (double powerset) is a monad.
• Define the list monad (-)^*.
• For a fixed set A, the functor (-)^A is a monad (called the input/reader monad in Haskell). Define it and prove the monad laws.
• Exercises 5.1.2 and 5.1.3 of the book.
12. Lecture 12, Tuesday 2 December, 15:30-17:30, in HG01.028.
• Topic: Algebras for a monad, Eilenberg-Moore category. Section 5.4 Jacobs' book.
• Algebras for a monad: definitions and examples.
• Pointed sets, join semi-lattices.
• Vector spaces.
• Suggested exercises:
• Given a vector space W over the reals show that it is an algebra for the monad V(-) defined on objects as V(X) = { phi : Reals^X | support of phi is finite}, on arrows and monad laws are the same as for the distribution monad (see last lecture) .
• Show that any algebra for the monad V(-) is indeed a vector space. (that is, it satisfy the vector space laws).
• Show that given any set B and monad T, the set T(B) carries an algebra structure.
• Exercises 5.4.5 (ii) and 5.4.9 (ii) and (iii) of the book.
13. Lecture 13, Tuesday 9 December, 15:30-17:30, in HG01.028.
• Topic: Generalized powerset construction, language semantics of non-determinsitic automata. See here and here for material on this topic.
• Generalized subset construction for coalgebras: definition.
• Coalgebraic language semantics (if final coalgebra exists). Connection to bisimilarity.
• Examples: non-deterministic automata, partial and weighted automata.
• Suggested exercises:
• Recall the non-deterministic automaton example from the lecture. How can one change the algebra structure on the output set 2 in order to achieve the following language semantics: a word is accepted by a state in an NFA if and only if every path labelled by the word leads to a final state.
• Show that if X and Y both have a T-algebra structure, for a given monad T, then also the cartesian product XxY and exponential X^A have a T-algebra structure.
• Show that given a coalgebra for the functor [0,1] x D(-)^A, where D is the subdistribution monad, one can define the semantics of such a coalgebra in terms of languages [0,1]^{A^*}.
14. Lecture 14, Tuesday 16 December, 15:30-17:30, in HG01.028.
• Topic: Recap, exercises on bisimulation, algebras for a monad and determinization. See here for the list of 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 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 and modal logic, the course will be self-contained: Only basic definitions will be needed, and these will be introduced as part of the course.

Grading