15 December 2023, Coinduction: a Categorical tour of Computation, Liam Chung

Induction is well known as both an important method of definition as well as proof, but it has some important blind spots. Inductive definitions use constructors, that is, methods to make new objects. Inductively constructed data must have an end, in the context of real programs. This makes it more difficult to use for modelling computation with (possibly) infinite data streams, or where program termination is not guaranteed.

In this talk we'll discuss coinduction, the dual notion to induction. Where induction is formulated as rules for creating new things, coinduction is formulated as rules for taking them apart. This gives it wide utility in modeling computational states without assuming we know what they look like, a so-called black box approach.

We'll also delve into the basics of the mathematical concepts underpinning this duality, namely the duality of algebras and coalgebras. While these topics take heavy inspiration from category theory and universal algebra, no prior significant knowledge of either will be assumed.