Coinduction

Discussion

The principles, as stated, are somewhat opaque, but can be usefully thought of in the following way. Suppose you wish to prove a property of ${\displaystyle \mu F}$. By the principle of induction, it suffices to exhibit an F-closed set ${\displaystyle X}$ for which the property holds. Dually, suppose you wish to show that ${\displaystyle x\in \nu F}$. Then it suffices to exhibit an F-consistent set that ${\displaystyle x}$ is known to be a member of.

Examples

Defining a set of data types

Consider the following grammar of datatypes:

$${\displaystyle T=\mathrm{\perp }|\mathrm{\top }|T\times T}$$

That is, the set of types includes the "bottom type" ${\displaystyle \mathrm{\perp }}$, the "top type" ${\displaystyle \mathrm{\top }}$, and product types. These types can be identified with strings over the alphabet ${\displaystyle \mathrm{\Sigma }=\{\mathrm{\perp },\mathrm{\top },\times \}}$. Let ${\displaystyle {\mathrm{\Sigma }}^{\le \omega }}$ denote all (possibly infinite) strings over ${\displaystyle \mathrm{\Sigma }}$. Consider the function ${\displaystyle F:2^{{\mathrm{\Sigma }}^{\le \omega }}\to 2^{{\mathrm{\Sigma }}^{\le \omega }}}$:

$${\displaystyle F(X)=\{\mathrm{\perp },\mathrm{\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 \mathrm{\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 \mathrm{\perp }\times \mathrm{\perp }\times \cdots \in \nu F}$

Here ${\displaystyle \mathrm{\perp }\times \mathrm{\perp }\times \cdots }$ denotes the infinite string ${\displaystyle (\mathrm{\perp },\times ,\mathrm{\perp },\times ,\dots )}$. To use the principle of coinduction, consider the set:

$${\displaystyle S=\{\mathrm{\perp },\mathrm{\perp }\times \mathrm{\perp }\times \cdots \}}$$

This set is F-consistent. First, ${\displaystyle \mathrm{\perp }\in \{\mathrm{\perp },\mathrm{\top }\}\subseteq F(S)}$. Second, since ${\displaystyle \mathrm{\perp }\in S}$ and ${\displaystyle \mathrm{\perp }\times \mathrm{\perp }\times \cdots \in S}$, we have ${\displaystyle \mathrm{\perp }\times (\mathrm{\perp }\times \mathrm{\perp }\times \cdots )\in F(S)}$. Interpreting strings as sequences (functions from ${\displaystyle \mathbb{N}\to \mathrm{\Sigma }}$), prepending the finite prefix ${\displaystyle \mathrm{\perp }\times }$ to the infinite string ${\displaystyle \mathrm{\perp }\times \mathrm{\perp }\times \cdots }$ yields ${\displaystyle \mathrm{\perp }\times \mathrm{\perp }\times \cdots }$ itself, so ${\displaystyle \mathrm{\perp }\times \mathrm{\perp }\times \cdots \in F(S)}$. Therefore ${\displaystyle S\subseteq F(S)}$, and by the principle of coinduction, ${\displaystyle \mathrm{\perp }\times \mathrm{\perp }\times \cdots \in \nu F}$.

Note. The representation of types as strings over ${\displaystyle \mathrm{\Sigma }}$ is not faithful to the underlying tree structure. Finite strings such as ${\displaystyle \mathrm{\perp }\times \mathrm{\top }\times \mathrm{\perp }}$ are ambiguous without bracketing, and for any infinite string ${\displaystyle s}$ the concatenation ${\displaystyle s\times t=s}$ for all ${\displaystyle t}$, so distinct trees may be identified. This does not affect the argument above, which only illustrates the principle of coinduction via F-consistency, but it would matter in settings where constructor structure must be preserved. A standard structural treatment represents types via the isomorphism ${\displaystyle T\cong 1+1+(T\times T)}$; see F-coalgebra for details.

Coinductive datatypes in programming languages

Consider the following definition of a stream in Haskell:

<span id="mwzQ"></span><span class="kr" id="mwzg">data</span><span class="w" id="mwzw"> </span><span class="kt" id="mw0A">Stream</span><span class="w" id="mw0Q"> </span><span class="n" id="mw0g">a</span><span class="w" id="mw0w"> </span><span class="ow" id="mw1A">=</span><span class="w" id="mw1Q"> </span><span class="kt" id="mw1g">S</span><span class="w" id="mw1w"> </span><span class="n" id="mw2A">a</span><span class="w" id="mw2Q"> </span><span class="p" id="mw2g">(</span><span class="kt" id="mw2w">Stream</span><span class="w" id="mw3A"> </span><span class="n" id="mw3Q">a</span><span class="p" id="mw3g">)</span> <span class="c1" id="mw3w">-- Stream "destructors"</span> <span class="nf" id="mw4A">head</span><span class="w" id="mw4Q"> </span><span class="ow" id="mw4g">::</span><span class="w" id="mw4w"> </span><span class="kt" id="mw5A">Stream</span><span class="w" id="mw5Q"> </span><span class="n" id="mw5g">a</span><span class="w" id="mw5w"> </span><span class="ow" id="mw6A">-></span><span class="w" id="mw6Q"> </span><span class="n" id="mw6g">a</span> <span class="nf" id="mw6w">head</span><span class="w" id="mw7A"> </span><span class="p" id="mw7Q">(</span><span class="kt" id="mw7g">S</span><span class="w" id="mw7w"> </span><span class="n" id="mw8A">a</span><span class="w" id="mw8Q"> </span><span class="n" id="mw8g">astream</span><span class="p" id="mw8w">)</span><span class="w" id="mw9A"> </span><span class="ow" id="mw9Q">=</span><span class="w" id="mw9g"> </span><span class="n" id="mw9w">a</span> <span class="nf" id="mw-A">tail</span><span class="w" id="mw-Q"> </span><span class="ow" id="mw-g">::</span><span class="w" id="mw-w"> </span><span class="kt" id="mw_A">Stream</span><span class="w" id="mw_Q"> </span><span class="n" id="mw_g">a</span><span class="w" id="mw_w"> </span><span class="ow" id="mwAQA">-></span><span class="w" id="mwAQE"> </span><span class="kt" id="mwAQI">Stream</span><span class="w" id="mwAQM"> </span><span class="n" id="mwAQQ">a</span> <span class="nf" id="mwAQU">tail</span><span class="w" id="mwAQY"> </span><span class="p" id="mwAQc">(</span><span class="kt" id="mwAQg">S</span><span class="w" id="mwAQk"> </span><span class="n" id="mwAQo">a</span><span class="w" id="mwAQs"> </span><span class="n" id="mwAQw">astream</span><span class="p" id="mwAQ0">)</span><span class="w" id="mwAQ4"> </span><span class="ow" id="mwAQ8">=</span><span class="w" id="mwARA"> </span><span class="n" id="mwARE">astream</span>

The first line says that a stream is made up of an element followed by a stream (S is a constructor of elements, and a denotes for an arbitrary type for the elements). As there is no base case, 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

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

$${\displaystyle \begin{array}{cc}F(x)& =A\times x\\ F(f)& =⟨{\mathrm{i}\mathrm{d}}_A,f⟩\end{array}}$$

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

$${\displaystyle \mathrm{o}\mathrm{u}\mathrm{t}:\nu F\to F(\nu F)=A\times \nu F}$$

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

$${\displaystyle \overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}:F(\nu F)\to \nu F}$$

such that

$${\displaystyle \mathrm{o}\mathrm{u}\mathrm{t}\circ \overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}=F\left(\overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}\right)\circ F(\mathrm{o}\mathrm{u}\mathrm{t})=F\left(\overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}\circ \mathrm{o}\mathrm{u}\mathrm{t}\right)}$$

The composition ${\displaystyle \overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}\circ \mathrm{o}\mathrm{u}\mathrm{t}}$ induces another F-coalgebra homomorphism ${\displaystyle \nu F\to \nu F}$. Since ${\displaystyle \nu F}$ is final, this homomorphism is unique and therefore ${\displaystyle {\mathrm{i}\mathrm{d}}_{\nu F}}$. Altogether we have:

$${\displaystyle \begin{array}{cc}\overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}\circ \mathrm{o}\mathrm{u}\mathrm{t}& ={\mathrm{i}\mathrm{d}}_{\nu F}\\ \mathrm{o}\mathrm{u}\mathrm{t}\circ \overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}=F(\overline{F(\mathrm{o}\mathrm{u}\mathrm{t})}\circ \mathrm{o}\mathrm{u}\mathrm{t})& ={\mathrm{i}\mathrm{d}}_{F(\nu F)}\end{array}}$$

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

Stream as a final coalgebra

We will show that Stream A is the final coalgebra of the functor ${\displaystyle F(x)=A\times x}$. Consider the following implementations:

<span id="mwAUY"></span><span class="nf" id="mwAUc">out</span><span class="w" id="mwAUg"> </span><span class="n" id="mwAUk">astream</span><span class="w" id="mwAUo"> </span><span class="ow" id="mwAUs">=</span><span class="w" id="mwAUw"> </span><span class="p" id="mwAU0">(</span><span class="n" id="mwAU4">head</span><span class="w" id="mwAU8"> </span><span class="n" id="mwAVA">astream</span><span class="p" id="mwAVE">,</span><span class="w" id="mwAVI"> </span><span class="n" id="mwAVM">tail</span><span class="w" id="mwAVQ"> </span><span class="n" id="mwAVU">astream</span><span class="p" id="mwAVY">)</span> <span class="nf" id="mwAVc">out'</span><span class="w" id="mwAVg"> </span><span class="p" id="mwAVk">(</span><span class="n" id="mwAVo">a</span><span class="p" id="mwAVs">,</span><span class="w" id="mwAVw"> </span><span class="n" id="mwAV0">astream</span><span class="p" id="mwAV4">)</span><span class="w" id="mwAV8"> </span><span class="ow" id="mwAWA">=</span><span class="w" id="mwAWE"> </span><span class="kt" id="mwAWI">S</span><span class="w" id="mwAWM"> </span><span class="n" id="mwAWQ">a</span><span class="w" id="mwAWU"> </span><span class="n" id="mwAWY">astream</span>

These are easily seen to be mutually inverse, witnessing the isomorphism. See the reference for more details.

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 0\in P\wedge (n\in P\Rightarrow n+1\in P)\Rightarrow \mathbb{N}\subseteq P}$$

Now consider the function ${\displaystyle F:2^{\mathbb{N}}\to 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.