Nested induction and coinduction

Nested induction and coinduction
Docent lecture, 2014-06-13. (Slightly edited.) [pdf]

Abstract

Inductive definitions are very common in computer science. The most famous example of an inductively defined set is perhaps the natural numbers. Data types, such as finite lists, and relations, for instance the semantics (meaning) of certain programming languages, can also be defined inductively.

Coinductive definitions may be less well-known, but are also common. They can for instance be used to define data types with infinite values, and the semantics of non-terminating programs.

Some concepts are partly finite, and partly infinite. One example is provided by liveness properties: "it is always (infinite) the case that eventually (finite) something will happen". Such concepts can sometimes be defined using a combination of induction and coinduction.

In the lecture I will discuss inductive and coinductive definitions, building up towards an expressive—but arguably complicated—combination of them with "nested" induction and coinduction.