In some recent work I’ve done on abstract interpretation I had to use the following fact about postfixpoints (i.e, a value $x$ such that $x \sleq F(x)$) of monotone functions on complete lattices:

For any set M of postfixpoints of a monotone function F, the least upper bound of M is itself a postfixpoint of F.

This result follows immediately from the fact that the set of postfixpoints of $F$ form a complete lattice which was proved in [Cousot & Cousot, 1979]. However their proof is far from straightforward, so I thought I would provide a direct proof of this property as it illustrates how to prove this style of property.

Preliminaries

We will fix some set $L$ equipped with a partial ordering ($\sleq$), least upper bound ($\sqcup$), and greatest lower bound ($\sqcap$) operators. We will consider some function $F: L \rightarrow L$ that is monotone with respect to $\sleq$, i.e. $x \sleq y \Rightarrow F(x) \sleq F(y)$. Next, fix some set $M \subseteq L$ such that

\[ x \in M \Rightarrow x \sleq F(x) \]

That is, $M$ is some set of postfixpoints of $F$. Our goal then is to show:

\[ \join M \sleq F(\join M) \]

The Proof

An important property we will exploit here is that least upper bounds are pointwise monotone. That is, for any two sets $S$ and $U$, if for every element $s$ of $S$ there is an element $u$ of $U$ such that $s \sleq u$ then $\join S \sleq \join U$.

By definition, the set $P = \{ F(x) \mid x \in M \}$ is pointwise greater or equal to the set $M$. Thus, we have that:

\[ \join M \sleq \join_{x \in M} F(x) = \join P \]

Note that in the above, the least upper bounds are defined because we assumed that $L$ is a complete lattice, which states the least upper bound is defined for any subset of $L$.

Let us now consider some element $x \in M$. By the definition of least upper bounds, we have that $x \sleq \join M$. By the monotonicity of $F$, we then have:

\[ F(x) \sleq F(\join M) \]

In other words, $F(\join M)$ is an upper bound for the set $P$. This means that $F(\join M)$ must be greater or equal to the least upper bound of $P$. Thus, by transitvity, we get:

\[ \join M \sleq \join P \sleq F(\join M) \]

This completes our proof.

The Dual Proof

It is reasonable to expect that a similar result holds for the meet of a set of prefixpoints., i.e.:

For any set N of prefixpoints of a monotone function F, the greatest lower bound of N is itself a prefixpoint of F.

Formally:

\[ \forall N \subseteq L.(\forall x \in N.F(x) \sleq x) \Rightarrow F(\meet N) \sleq \meet N \]

This proposition is true, but it turns out we don’t need to directly prove it! In fact, it follows from the application of the above result to the dual of the lattice $L$. The dual lattice $L^\natural$ is just the regular lattice $L$ with everything flipped around or on its head:

\[ \begin{align} x \sleq^\natural y \Leftrightarrow y \sleq x && \sqcup^\natural X = \meet X && \meet^\natural X = \sqcup X \end{align} \]

Before proceeding, let’s ensure that we still have a complete lattice. The partial order $\sleq^\natural$ is still anti-symmetric, reflexive, and transitive. Let’s next verify that our new least-upper bound operator $\sqcup^\natural$ in fact defines a least upper bound. So, we must show that, for every subset $X \in L^\natural$:

\[ \forall y.(\forall x \in X.x \sleq^\natural y) \Rightarrow \sqcup^\natural X \sleq^\natural y \]

Substituting definitions we simply get:

\[ \forall y.(\forall x \in X.y \sleq x) \Rightarrow y \sleq \sqcap X \]

Which must hold from the definition of $\sqcap$ as a greatest lower bound operator. A similar result holds for our definition of $\sqcap^\natural$. Finally, observe that $F$ is still monotone with respect to $\sleq^\natural$:

\[ x \sleq^\natural y \Rightarrow y \sleq x \Rightarrow F(y) \sleq F(x) \Rightarrow F(x) \sleq^\natural F(y) \]

Let us now restate our desired property of prefixpoints in this dual lattice:

\[ \forall N \subseteq L.(\forall x \in N.x \sleq^\natural F(x) \Rightarrow \join^\natural N \sleq^\natural F(\join^\natural N) \]

As $L^\natural$ is a complete lattice, this must be true from our result on prefixpoints above! You will often find this strategy in the literature, particularly in abstract interpretation paper; the authors will prove a proposition over least upper bounds and $\sleq$ in a complete lattice, and the result over greatest lower bounds and $\sleq^\natural$ (AKA $\sqsupseteq$) will follow “for free”.

Thanks to Doug Woos for his feedback on early versions of this post.