I'm working through Samuel Mimram's book Program = Proof. In the first chapter, he discusses recursive types in OCaml, and inductive types. An exercise he provides on the topic has me a little bit confused. In the exercise, he asks the reader to define the function induced by the inductively defined type of lists, and then show that it has a greatest fixpoint, distinct from the smallest fixpoint, and provide a concrete description of it.

I believe I'm able to define the function he mentions. If we had the type of lists of integers:

type list =
    | Nil
    | Cons of int * list

Then our induced function $F : \mathcal{P}(\mathcal{U}) \rightarrow \mathcal{P}(\mathcal{U})$ (where $\mathcal{P}(\mathcal{U})$ is the powerset of all possible values of our type list) looks like:

$$ F(X) = \{ \mathrm{Cons}(n, l) \ | \ n \in \mathbb{Z},\ l \in X \} \cup \{ \mathrm{Nil} \} $$

In the book, we learn that the least fixpoint of such a function defines the set of values inhabiting our type. That makes sense. He also goes through a proof of the Knaster-Tarski theorem to demonstrate that such a least fixpoint will exist, due to the fact that $\langle \mathcal{P}(\mathcal{U}), \subseteq\rangle$ is a semilattice and $F$ is monotonic.

I can't find any intuition for reasoning about the greatest fixpoint of this function. My naïve assumption is simply that the greatest fixpoint would be the set of all infinite lists, but I think I'm missing a really crucial idea here, and I can't tie it down in my understanding. If anybody could provide some information or input on this, I would really appreciate it!


1 Answer 1


The greatest fixed point cannot contain only the infinite lists, because it must contain all the elements of the least fixed point (and every other fixed point). Another way to see this is that just the infinite lists are not even a fixed point, since applying $F$ will add $\mathrm{Nil}$, which is not infinite.

However, adding the infinite lists is the right thing to do. I'm not familiar with the book you're reading at all, so I don't know exactly how this would be realized in its setting. For instance, I don't know what $\mathrm{Cons}$ and $\mathrm{Nil}$ are intended to be exactly as operations on $\mathcal{U}$ (or what $\mathcal U$ consists of). But the idea would likely be that $\mathcal U$ has both finite and infinite things built completely out of them, the least fixed point collects just the finite ones, and the greatest fixed point collects all of them.

  • $\begingroup$ Thanks for the great answer! This cleared up a lot of my confusion. So are we able to say the least fixed point would be the infinite set of non-infinite lists? And then the greatest fixed point would include the infinite lists along with that? Also, $\mathcal{U}$ here would be the set of all possible lists in the type. So the $\mathrm{Cons}$ is being applied to all elements of a given subset of $\mathcal{U}$. I hope that's a little clearer. $\endgroup$
    – Finley
    Commented Dec 22, 2020 at 22:53
  • 2
    $\begingroup$ The least fixed point is the finite lists, and the greatest is the finite and infinite lists, yes. I don't think it makes sense to say $\mathcal U$ is just the set of list values, because those are what you are attempting to define. More likely it is some set/domain of all possible values of any type, and the types are identifying particular sub-collections of that. $\endgroup$
    – Dan Doel
    Commented Dec 22, 2020 at 22:58
  • $\begingroup$ Great, thank you. And yes, the book refers to $\mathcal{U}$ as the "set of all possible values that a program can manipulate", so it seems you are correct. I was incorrectly interpreting that as the set of all values in the list type. $\endgroup$
    – Finley
    Commented Dec 22, 2020 at 23:03
  • $\begingroup$ I hope you don't mind me commenting here - isn't the way U is defined implying that infinite lists are not included? (is there a way for a Ocaml programm to manipulate a infinite list? The way it is defined such a list would have to represented in memory right?) - Maybe I'm nitpicking but I find this definition just a bit too imprecise to really argue about the question on hand $\endgroup$
    – Random Dev
    Commented Jun 24, 2021 at 9:19
  • $\begingroup$ It is not imprecise. However OCaml is not an ideal language for thinking about it. The data types in OCaml (and Haskell, and ...) exhibit something known as 'limit-colimit coincidence,' where least and greatest fixpoints are the same, due to partial recursive definitions. This does not happen in a language based on total functions. There, the least fixed point is more like the OCaml data type (given by the code above), and the greatest like the Haskell type. But both OCaml and Haskell can define types similar to both total fixed points. $\endgroup$
    – Dan Doel
    Commented Jun 25, 2021 at 15:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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