## Coalgebras and Infinite Data Structures ↑

### Venanzio Capretta

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.

Further course materials