2
$\begingroup$

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!

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
3
  • $\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 Dec 22 '20 at 22:53
  • 1
    $\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 Dec 22 '20 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 Dec 22 '20 at 23:03

Your Answer

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

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