Preliminaries

Let ${\displaystyle U}$ be a set and ${\displaystyle F}$ be a monotone function ${\displaystyle 2^{U}\rightarrow 2^{U}}$, that is:

${\displaystyle X\subseteq Y\Rightarrow F(X)\subseteq F(Y)}$

Unless otherwise stated, ${\displaystyle F}$ will be assumed to be monotone.

X is F-closed if ${\displaystyle F(X)\subseteq X}$

X is F-consistent if ${\displaystyle X\subseteq F(X)}$

X is a fixed point if ${\displaystyle X=F(X)}$

These terms can be intuitively understood in the following way. Suppose that ${\displaystyle X}$ is a set of assertions, and ${\displaystyle F(X)}$ is the operation which takes the implications of ${\displaystyle X}$. Then ${\displaystyle X}$ is F-closed when you cannot conclude anymore than you've already asserted, while ${\displaystyle X}$ is F-consistent when all of your assertions are supported by other assertions (i.e. there are no "non-F-logical assumptions").

The Knaster–Tarski theorem tells us that the least fixed-point of ${\displaystyle F}$ (denoted ${\displaystyle \mu F}$) is given by the intersection of all F-closed sets, while the greatest fixed-point (denoted ${\displaystyle \nu F}$) is given by the union of all F-consistent sets. We can now state the principles of induction and coinduction.

Definition

Principle of induction: If ${\displaystyle X}$ is F-closed, then ${\displaystyle \mu F\subseteq X}$

Principle of coinduction: If ${\displaystyle X}$ is F-consistent, then ${\displaystyle X\subseteq \nu F}$

Defining a set of datatypes

Consider the following grammar of datatypes:

${\displaystyle T=\bot \;|\;\top \;|\;T\times T}$

That is, the set of types includes the "bottom type" ${\displaystyle \bot }$, the "top type" ${\displaystyle \top }$, and (non-homogenous) lists. These types can be identified with strings over the alphabet ${\displaystyle \Sigma =\{\bot ,\top ,\times \}}$. Let ${\displaystyle \Sigma ^{*}}$ denote all strings over ${\displaystyle \Sigma }$. Consider the function ${\displaystyle F:2^{\Sigma ^{*}}\rightarrow 2^{\Sigma ^{*}}}$:

${\displaystyle F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}}$

In this context, ${\displaystyle x\times y}$ means "the concatenation of string ${\displaystyle x}$, the symbol ${\displaystyle \times }$, and string ${\displaystyle y}$." We should now define our set of datatypes as a fixpoint of ${\displaystyle F}$, but it matters whether we take the least or greatest fixpoint.

Suppose we take ${\displaystyle \mu F}$ as our set of datatypes. Using the principle of induction, we can prove the following claim:

All datatypes in ${\displaystyle \mu F}$ are finite

To arrive at this conclusion, consider the set of all finite strings over ${\displaystyle \Sigma }$. Clearly ${\displaystyle F}$ cannot produce an infinite string, so it turns out this set is F-closed and the conclusion follows.

Now suppose that we take ${\displaystyle \nu F}$ as our set of datatypes. We would like to use the principle of coinduction to prove the following claim:

The type ${\displaystyle \bot \times \bot \times \cdots \in \nu F}$

Here ${\displaystyle \bot \times \bot \times \cdots }$ denotes the infinite list consisting of all ${\displaystyle \bot }$. To use the principle of coinduction, consider the set:

${\displaystyle \{\bot \times \bot \times \cdots \}}$

This set turns out to be F-consistent, and therefore ${\displaystyle \bot \times \bot \times \cdots \in \nu F}$. This depends on the suspicious statement that

${\displaystyle \bot \times \bot \times \cdots =\bot \times \bot \times \cdots \times \bot \times \bot \times \cdots }$

The formal justification of this is technical and depends on interpreting strings as sequences, i.e. functions from ${\displaystyle \mathbb {N} \rightarrow \Sigma }$. Intuitively, the argument is similar to the argument that ${\displaystyle 0.{\bar {0}}1=0}$ (see Repeating decimal).

Coinductive datatypes in programming languages

Consider the following definition of a stream:^[5]

data Stream a = S a (Stream a)

-- Stream "destructors"
head (S a astream) = a
tail (S a astream) = astream

This would seem to be a definition that is not well-founded, but it is nonetheless useful in programming and can be reasoned about. In any case, a stream is an infinite list of elements from which you may observe the first element, or place an element in front of to get another stream.

Relationship with F-coalgebras

Source:^[6]

Consider the endofunctor ${\displaystyle F}$ in the category of sets:

${\displaystyle F(x)=A\times x}$

${\displaystyle F(f)=\langle \mathrm {id} _{A},f\rangle }$

The final F-coalgebra ${\displaystyle \nu F}$ has the following morphism associated with it:

${\displaystyle \mathrm {out}$ :\nu F\rightarrow F(\nu F)=A\times \nu F}

This induces another coalgebra ${\displaystyle F(\nu F)}$ with associated morphism ${\displaystyle F(\mathrm {out} )}$. Because ${\displaystyle \nu F}$ is final, there is a unique morphism

${\displaystyle {\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F}$

such that

${\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)}$

The composition ${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }$ induces another F-coalgebra homomorphism ${\displaystyle \nu F\rightarrow \nu F}$. Since ${\displaystyle \nu F}$ is final, this homomorphism is unique and therefore ${\displaystyle \mathrm {id} _{\nu F}}$. Altogether we have:

${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}}$

${\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}}$

This witnesses the isomorphism ${\displaystyle \nu F\simeq F(\nu F)}$, which in categorical terms indicates that ${\displaystyle \nu F}$ is a fixpoint of ${\displaystyle F}$ and justifies the notation.

Stream A

out astream = (head astream, tail astream)
out' (a, astream) = S a astream

Relationship with mathematical induction

We will demonstrate how the principle of induction subsumes mathematical induction. Let ${\displaystyle P}$ be some property of natural numbers. We will take the following definition of mathematical induction:

${\displaystyle P(0)\land (P(n)\Rightarrow P(n+1))\Rightarrow P(\mathbb {N} )}$

Now consider the function ${\displaystyle F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }}$:

${\displaystyle F(X)=\{0\}\cup \{x+1:x\in X\}}$

It should not be difficult to see that ${\displaystyle \mu F=\mathbb {N} }$. Therefore, by the principle of induction, if we wish to prove some property ${\displaystyle P}$ of ${\displaystyle \mathbb {N} }$, it suffices to show that ${\displaystyle P}$ is F-closed. In detail, we require:

${\displaystyle F(P)\subseteq P}$

That is,

${\displaystyle \{0\}\cup \{x+1:x\in P\}\subseteq P}$

This is precisely mathematical induction as stated.