It's easy to see how inductively-defined data types correspond to least fixed points. Let's take the natural numbers as an example, with constructors are $0 : \mathbb N$ and $s : \mathbb N \to \mathbb N$. Define the operation $F(X) = \{0\} \cup \{ s(n) : n \in X \}$, which applies the constructors to all elements of $X$. The Knaster–Tarski fixed point theorem says that the least fixed point of $F$ is $\bigcap\{ X : F(X) \subseteq X \}$.

What does that set mean? Well, it's the intersection of all sets such that applying the constructors doesn't give you anything new. So, since applying the constructors throws in $0$, $0$ must be in there. Since applying the constructors throws in every successor, every successor must be in there. The minimality property ensures that there are no more elements in there, so induction holds for this set. So it's the natural numbers.

Okay, great. Something similar is going to work for other inductive datatypes too. This indicates we can consider inductively defined datatypes as $\subseteq$-least fixed points for the set operation that applies all the constructors.

But what about coinductive data types? I've heard it said, though I'm not sure anywhere reliable, that codata corresponds to greatest fixed points. Let's go look at Knaster-Tarski again: the greatest fixed point is $\bigcup \{ X : X \subseteq F(X) \}$. What does this tell us? Well, promisingly, it says that every element is either $0$ or a successor. Certainly all of the natural numbers are in this greatest fixed-point. From what I know about coinduction, I'm expecting to get the natural numbers plus a unique fixed point of the successor.

But why should the successor have a unique fixed point? Why can't we have two, violating coinduction? Certainly this depends on what $s$ is, precisely, but all we asked of $s$ when we were doing the inductive definition was that it was injective ("free" in some sense), which feels like a much lighter condition.

How do I ensure the right number of fixed points for the constructors? How do I recover the coinduction principle? Or is it just that the order for which these constructions are LFPs and GFPs respectively isn't subset inclusion?

  • 1
    $\begingroup$ Since it wasn't getting much attention here, I've asked this question on MathOverflow too. $\endgroup$ – Ben Millwood Apr 21 '13 at 17:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.