$\newcommand{\bigsqcap}{\mathop ⨅}$

There is an ever growing need to establish properties of a software by means of program analysis techniques. In order to get into the topic, we first need to talk about lattices.

In order to talk about lattices, let's recap partial orders.

Partial Orders

A pair $\left(D, \sqsubseteq\right)$ with $D\not=\emptyset$ and a reflexive, transitive, and antisymmetric relation $\sqsubseteq$ is a partial order. For example, the powerset of any set with $\subseteq$ is such a partial order. Note that it can happen that some elements are not comparable to each other, as in $\left(\{0,1\}, \subseteq\right)$: $\{0\}\subsetneq\{1\}$!


Say we have a partial order $\left(D,\sqsubseteq\right)$ and some subset $X\subseteq D$.

The upper bound $u\in X$ then simply fulfills $\forall x\in X. x\sqsubseteq u$.

Now, the least upper bound aka “join” of $X$ is an upper bound of $X$ and is smaller than any other upper bound of $X$, i.e. $u\subseteq u'$ for all upper bounds $u’\in X$.

We will write the join as $\bigsqcup X$. However, if $X=\{a,b\}$, then we will write $a\sqcup b$, just because it is more visual pleasing than $\bigsqcup\{a,b\}$. :)

One last thing about join. Notice that $D$ is not restricted in any way, so it might as well be infinitely large. This, in turn, means that the join does not have to exist, e.g. $\left(\mathbb{N}, \le\right)$.


In a super-similar fashion we define lower bounds and the least lower bound.

$u\in X$ is a lower bound if $\forall x\in X. u\sqsubseteq x$.

Take a lower bound $u\in X$. It is the greatest lower bound aka “meet” of $X$ if it is greater than any other lower bound in $X$: $u’\sqsubseteq u$ for any $u’\in X$.

We also use similar notation: $\bigsqcap X$ is the meet of $X$. Similarily, $\bigsqcap\{a,b\}$ will be written as $a\sqcap b$. (Unfortunately, MathJax does not support \bigsqcap, which is why I'm using literally ⨅, the unicode character. I'm sorry. It feels dirty. :( tell me if you know a better way)


Finally, we can define a lattice as a partial order $\left(D, \sqsubseteq\right)$ such that every pair $a,b\in D$ has a join and a meet.

The lattice is complete if all subsets of it have a join and meet.

Usually, one would refer to $\bigsqcup X=\bigsqcap \emptyset$ as $\perp$ (bottom). Likewise, $\bigsqcap X=\bigsqcup \emptyset$ as $\top$ (top).

Finite Lattices

A finite lattice $(D, \sqsubseteq)$ trivially satisfies the completeness requirement:

Take any $X\subseteq D$. Since both $a\sqcap b$ and $a\sqcup b$ for any $a,b\in X\subseteq D$ exist by definition of a lattice, we can further conclude by transitivity that this holds for all of elements in $X$. So, if a finite thing is a lattice, it is also complete.