### 1. Induction

If you’re reading this, you’ve probably encountered proof by mathematical induction. It’s a ubiquitous technique at every level of study and research, and a standard tool in our arsenal whenever we approach a new problem.

A proof by induction follows quite a formulaic structure. Let’s do a simple example.

#### Proposition 1.1:

#### Proof:

First, we have to verify the base case

Then we assume

as our inductive hypothesis, and argue as follows

Thus by the principle of induction, the proposition holds for all natural numbers.

### 2. Inductive Types

Most axiomatisations of the natural numbers include the principle of induction or some statement equivalent to it. One common formulation states that if a subset of the natural numbers contains zero and is closed under the successor function, then that subset is the whole set of naturals. In this formulation, our proof above showed precisely that the set

contains 0, and that it is closed under taking successors, and therefore that it is equal to ℕ. The underlying idea here is that a natural number is either 0 or the successor of some other natural number and that there are no other possibilities. In this sense, you can build ℕ starting with only 0 and using only the successor function.

One way to bake this idea into the definition is to define the naturals in the form of an inductive type. We define the naturals as everything you can get by repeatedly applying the constructor (the successor function) to the constant 0.

We can define other inductive types like this, for example lists of integers. We start with a constant “nil”, which represents the empty list; Our constructor is then a function denoted :: which takes a natural number *n *and a list *L*, and outputs the list *n*::*L*, where *n* is appended to the start of *L*. For example 6::[1,2,3] = [6,1,2,3]. More explicitly:

The nature of this definition allows us to perform inductive proofs here too.

#### Proposition 2.1:

Every list is finite.

#### Proof:

Firstly nil is finite. Then, if *L* is finite, *n*::*L* is finite. Therefore by induction, all lists are finite.

### 3. Coinductive Types

As proposition 2.1 shows, the list type isn’t capable of handling infinite content. You can’t build infinite things from finite things in finitely many steps. If we want to express infinite data-types then we’ll need a new kind of definition.

Let’s do an example, and consider infinite lists, which from now on we’ll refer to as streams. As before, we can append something to the front of a stream such as 6::[1,4,9,16,25, … ] = [6,1,4,9,16,25, … ]. But this time this doesn’t give us a way to build all of the streams in the same way as with the lists. We don’t have anywhere to start from!

However, this time we can also consider the other direction. Given any stream *S* we can break *S* into two parts; we can extract the first element called the head of *S*, or we can discard the first element and just take the rest which we call the tail of *S* which will be a new stream. In notation this is

If you completely specify the head and tail of S, then you completely specify S. For example, if

then *S* is the stream [7,7,7,7, … ] and if

then *S₀ *= [0,1,2,3,4,5, … ].

Just as every inductive type comes with an induction principle, every coinductive type comes with a coinduction principle — which we’ll construct in the next few parts.

### 4. Fixed Points

To figure out what coinduction principles look like, we should start by describing induction principles in more generality.

An inductive type is built from a set of constants and a set of constructors. For ℕ, this was 0 and the constructor was *n* ↦ *n+1*. We formulated the principle of induction to say that if a set contained 0, and was closed under the successor function, then that set contained all of ℕ. We can express this principle in the following statement:

The idea here is that if *A* is closed under the successor function, then for every *a* in *A*, *a+1* is in *A*, which precisely means that the set of all of the *a+1*s is a subset of *A*. The same reasoning applies to 0.

For lists, if we make the identification *n*::*L* = (*n*, *L*) then we can phrase the induction principle there as

Notably, in both cases, if we replace *A* with ℕ or List(ℕ), the ⊆ relation becomes an equality. To generalise these we consider monotone set-valued functions. These map sets to sets (not values of sets!) satisfying the following relationship:

You can verify that both of the above examples are monotone. Then we say that a set *X* is “*F*-closed” if and only if

And that X is “*F*-consistent” if and only if

Then define *μF* as the intersection of all *F*-closed sets.

#### Proposition 4.1:

*μF* is a fixed point for *F*.

#### Proof:

Firstly we have:

which since *F* is monotone implies

which from the definition of *μF* as an intersection implies

which together with the first statement implies

In this sense, *μF* is the least fixed point of *F*. And we can use this fact to formulate induction in a highly general way:

#### Theorem 4.2 (Principle of Induction):

If *F* is a monotone set-valued function and *X* is a set in the domain of *F*, then

The proof is immediate from the above work.

Notably, the argument for proposition 4.2 also works to characterise a greatest fixed point of *F*. Define *νF * to be the union of *F*-consistent sets, i.e.

and then since this is the greatest fixed point of *F* we get:

#### Theorem 4.3 (Principle of Coinduction):

If *F* is a monotone set-valued function and *X* is a set in the domain of *F*, then

Let’s do a simple example to illustrate. The set of streams Stream(ℕ) satisfies

and further more, we have that

and so for any set *X*, it follows by coinduction that

### 5. Applications of Coinduction

As it may initially appear, coinduction doesn’t look that powerful. With induction, if you want to prove a property of *μF*, you can write down an *F*-closed set which has that property, and the result follows immediately for *μF*. In contrast, with *νF*, it looks like all you can do is prove that something is a subset of *νF*.

It turns out, however, that by carefully choosing* F *we can still prove very powerful results. For this, we will study the lexicographic ordering on the set of streams.

The lexicographic ordering is defined as follows: we say that *σ* ≤ *τ* if and only if

Intuitively, if the first elements are different you stop there. If they’re not, then you look at the next element of the stream and keep going until you find a difference. Since a relation between streams is a subset of Stream(ℕ)², we can identify ≤ with the subset

Then if we define the function

It is easy to show that ≤ is *νT*.

#### Proposition 5.1:

The lexicographic ordering on streams is transitive. i.e. if ≤ is the lexicographic order then

#### Proof:

Consider the set

and suppose we have streams *σ*,* ρ*, and *τ *such that* σ* ≤ *ρ* ≤ *τ*. By definition of ≤, we have

Now suppose that hd(*σ*) = hd(*τ*). We get that

by the definition of ≤. This immediately implies that (tl(*σ*), tl(*τ*)) is an element of *R*. In turn, this means that *R* is *T*-consistent which means we can apply coinduciton! We conclude:

or in other words that

which is exactly what we were trying to show.

Unless you’re doing specific kinds of functional programming, you’re not very likely to need coinductive types or to use coinduction as a proof technique — most mathematicians don’t know about it or use it, because in a lot of situations there are other ways to prove these results, even if coinduction would be simpler or quicker.

That’s not really the point, however. The point is that we described an existing technique in a new way, and used that to develop interesting generalisations and ideas that we wouldn’t have thought about otherwise. A lot of the most powerful and insightful mathematics was discovered by this kind of process.

For those who know category theory, some good further reading would be to look at the concepts of initial algebras and final co-algebras — which encode the work we’ve been doing here in a categorical concept, and make the duality at play even more explicit.

Thanks for reading :)

### References and Further reading:

https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf

This is the main paper this article is based on, though I rephrased or reformulated quite a few things, and didn’t touch on the more in depth and advanced mathematical logic.

https://ncatlab.org/nlab/show/algebra+for+an+endofunctor

This is a good place to start the further reading on the category stuff.

https://www.andrew.cmu.edu/user/avigad/Talks/qpf.pdf

More relevant further reading on inductive and coinductive types and their categorical semantics — a little experience with the lean proof language is also helpful.