Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

This is, I'm afraid, another question that MSE couldn't answer.

It's easy to see how inductively-defined data types correspond to least fixed points. Let's take the natural numbers as an example, whose 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?

share|improve this question
    
A good starting point is: cs.ru.nl/~bart/PAPERS/JR.pdf –  Matteo Mio Apr 21 '13 at 17:13
    
The version available from here is better-looking on my computer: citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.1418 ; thanks, having a look. –  Ben Millwood Apr 21 '13 at 19:09
add comment

2 Answers

You've got the levels mixed up a bit because you are thinking too set-theoretically. While it is likely that you can get the carrier sets of inductive and coinductive datatypes as least and greatest fixed points, respectively, you will still wonder where to get constructors, destructors, recursion and corecursion.

An inductive type corresponds to an initial algebra for a functor $F : \mathsf{Set} \to \mathsf{Set}$. For example, the natural numbers are the initial algebra for the functor $F(X) = 1 + X$ where $1$ is the singleton set and $+$ is disjoint sum. Similarly, the set of binary trees is the initial algebra for the functor $F(X) = 1 + X^2$. An initial algebra consists of a set $I$ and a structure map $i : F(I) \to I$. The structure map gives us the constructors for the datatype, and the initiality of $I$ gives a recursion principle. Let's look at this for binary trees:

  • the initial algebra for $F(X) = 1 + X^2$ is the set $T$ of finite binary trees. Its structure map $t : 1 + T^2 \to T$ can be decomposed into two parts. The first part $\mathsf{nil} : 1 \to T$ is the empty tree, and the second part $\mathsf{cons} : T^2 \to T$ is the constructor which takes two trees and puts them together into a new tree.

  • the initiality of $T$ says that, given any set $A$ and a map $a : 1 + A^2 \to A$ there is a unique algebra homomorphism $h : (T,t) \to (A,a)$. We decompose $a$ into an element $x_0 \in A$ and a map $g : A^2 \to A$. Then the initiality says that there is a unique map $h : T \to A$ such that $$h(\mathsf{nil}) = x_0$$ and $$h(\mathsf{cons}(u, v)) = g(h(u), h(v)).$$ This is just definition of $h$ by recursion on the structure of the tree.

Now let us look at final coalgebras, which ought to correspond to coinductive types (codata). For example, the final coalgebra for $F(X) = 1 + X$ is the set $\mathbb{N} \cup \lbrace \infty \rbrace$, the final coalgebra for $F(X) = 1 + X^2$ contains finite and infinite binary trees, while the final coalgebra for $F(X) = 2 \times X$ is the set of infinite binary streams. Again, the structure map of such a final coalgebra gives us the destructors for codata, while finality gives a way of constructing maps into the codata.

For example, consider the final coalgebra $S$ for $F(X) = 2 \times X$. The structure map $s : S \to 2 \times S$ decomposes into two maps $\mathsf{hd} : S \to 2$ and $\mathsf{tl} : S \to S$ which I am suggestively calling "head" and "tail". Finality of $S$ means that, given any set $A$ and a map $a : A \to 2 \times A$, there is a unique coalgebra homomorphism $\phi : (A,a) \to (S,s)$. If we decompose $a$ into $h : A \to 2$ and $t : A \to A$, then $\phi$ is the unique map satisying $$\mathsf{hd}(\phi(x)) = h(x)$$ and $$\mathsf{tl}(\phi(x)) = \phi(t(x)).$$ I hope I got that right.

So it is indeed the case that inductive datatypes are "least fixed points" and the coinductive datatypes are the "greatest fixed points", but in the categories of algebras and coalgebras, respectively.

share|improve this answer
    
Thanks for the answer. I did a poor job of explaining my existing knowledge in the question – I'm already mostly familiar with initial algebras and final coalgebras, and in particular why they are fixed points. I still don't see why they are "greatest" – terminal coalgebras may well have morphisms into other coalgebras which are not terminal, so what is the ordering with respect to which they are greatest? (The reason I'm thinking set-theoretically is that it works so beautifully for data that I felt there must be something interesting going on there) –  Ben Millwood Apr 22 '13 at 7:49
    
(When I say "I did a poor job of explaining my existing knowledge", I guess I mean "I didn't do that thing at all" :) sorry about that) –  Ben Millwood Apr 22 '13 at 7:50
    
Well, if you only care abut the carrier sets, you could look at greatest fixed points, I suppose. I will write another answer. –  Andrej Bauer Apr 22 '13 at 16:11
    
It depends what you mean by only caring about the carrier sets. What the constructors and destructors are is embedded in the $F$ whose lfp/gfp I am tyring to find – but in the data case, I don't have to assume much about them at all, I could take them to be "pair with 0" and "pair with 1" for example. The recursion principle for data comes from the minimality condition, so I have that too. So it seems to me like the set-theoretic lfp for a certain simple operation is precisely an initial algebra, and the question is if the gfp can be connected to a terminal coalgebra. –  Ben Millwood Apr 22 '13 at 19:58
    
Actually, I think the cool and correct way to do codata is to use set theory with antifoundation. See Barwise's book "Vicious Circles", books.google.si/… –  Andrej Bauer Apr 23 '13 at 9:01
show 2 more comments

Following Andrej's recommendation in comments, I went and looked up Vicious Circles by Barwise and Moss. There, codata can indeed be modelled by greatest fixed points in the subset-inclusion order, but working in a set theory with an antifoundation axiom.

In particular, we have (for example) that the greatest fixed point in set-theory-with-foundation for the $F$ I gave above (with $s$ interpreted as ordinal successor) is $\omega$, which is lacking a unique fixed point for $s$, but with a suitable antifoundation axiom it is $\omega \cup \Omega$ where $\Omega$ is the unique solution to $x = \{x\}$, so also a fixed point of $s$.

The antifoundation axiom is playing a key role here: not only does it ensure the existence of the necessarily ill-founded objects that accompany codata, they also include a uniqueness condition so that coinduction and corecursion can be properly defined. If I have that every element of the "conatural numbers" is either zero or the successor of a conatural number, I can recursively unfold this into a set picture which will necessarily be some chain of successor applications that is either infinite or ends in 0 – crucially, by antifoundation, the length of the chain determines uniquely the identity of the element, just as required by the coinduction principle.

The conclusion is that greatest fixed points may or may not exist in various contexts, but it's the antifoundation axiom which ensures that they are the right thing with regards to coinduction and corecursion principles.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.