# Fun with Lattices

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.*