Abstract

Dexter Kozen: Coinduction

Abstract

Mathematical induction is firmly entrenched as a fundamental and ubiquitous proof principle for proving properties of inductively defined objects. Mathematics and computer science abound with such objects, and mathematical induction is certainly one of the most important tools at our disposal.

Somewhat less well entrenched is the notion of coinduction. Despite recent interest, coinduction is still not fully established in our collective mathematical consciousness. A contributing factor is that coinduction is often presented in a relatively restricted form. It is often considered synonymous with bisimulation and is used to establish equality or other relations on infinite data objects such as streams or recursive types.

In this talk I will introduce the notion of coinduction as a general proof principle and illustrate its use in some nonstandard application areas, including streams, Markov chains, and non-well-founded sets.