Although computers have a finite memory and cannot store an infinite amount of information, Functional Programming and Type Theory allow us to represent infinite mathematical objects. These are represented as processes that generate part of the structure at every step. The mathematical/categorical formulation for these processes is the notion of coalgebra.
The first part of the course is an introduction to coalgebras with important examples like streams (infinite sequences) and non-well-founded trees. The most powerful proof method for infinite data structures is the Coinduction Principle, which allows us to prove the equality of two objects by a bisimulation, itself an infinite process that generates the equality by successive stages.
We will study methods to construct sound infinite objects, to solve recursive equations on them and to prove their properties. Examples will be given using functional programming in Haskell and formal reasoning in Coq. In Type Theory we can define coinductively not just single types, but families of types, predicates and relations. This leads to a proof technique in which the statement to be proved can be used recursively as long as it satisfies a guardedness conditions. It amounts to constructing a proof with an infinite number of logical steps.
We can combine coinduction with induction in several ways to define types with a complex internal structure. One example is the definition of all continuous functions between streams. A further generalization consists in defining a coinductive type simultaneously with a recursive function on it, in the style of induction-recursion. This leads to a very general notion of Wander types, that can be instantiated to many of the most common type-theoretic constructions.
In this section you will find, after each lecture, a list of topics that were taught and references to the chapters of the textbook.
|1. Sun 9 Apr 2017||Introduction to Infinite Types
Streams and Non-well-founded Trees
Productivity and Guardedness
|Outline of Lecture 1|
of The Construction of Infinity
|1E. Mon 10 Apr 2017||Exercise Class 1||Haskell Code|
|2. Mon 10 Apr 2017||(Final) Coalgebras
Bisimulation and CoInduction
|Outline of Lecture 2
Coalgebras in functional programming
and type theory
|2E. Tue 11 Apr 2017||Exercise Class 2||Coq Code|
|3. Tue 11 Apr 2017||Monadic Stream Functions
The Continuity Principle
|Outline of Lecture 3|
The Continuity of
Monadic Stream Functions
with Jon Fowler
|3E. Wed 13 Apr 2017||Exercise Class 3||Haskell Code|
|4. Wed 12 Apr 2017||CoInductive Reasoning
|The Coinductive Formulation
of Common Knowledge
with Colm Baston
|4E. Thu 13 Apr 2017||Exercise Class 4||Coq Code|
|A. from MGS 2013||Strategy Trees
|B. from MGS 2013||Simultaneous (Co)Induction / Recursion