lattice

See also

Semilattices

A lot of different program analysis techniques rely on the concept of a lattice. What the hell is a lattice?

Partial ordering

Let’s say we have a set . A partial ordering is a relation that has three properties:

• Reflexivity:
• Transitivity:
• Anti-symmetry:

We call a poset.

See also: Partial orders in the abstract

Lattices: meet and join

Lets say we have a subset . A lattice is defined by two operations: meet and join.

• Join returns the least upper bound between items in the lattice.
  • is an upper bound of items in , such that any other upper bound is even larger.
  • or is the upper bound between and .
  • The element is the greatest element. .
  • We’re moving through the lattice in the direction of the gap: up!
  • In domain theory, we use least upper bounds (lubs) to order recursive function invocations and provide a concrete upper bound on their denotations.
    • If an imperative statement is a function from state to state, in the limit, what does a while loop’s function behavior loop like? That limit is the least upper bound of infinitely many recursive invocations of the loop.
• Meet returns the greatest lower bound between items in the lattice.
  • is an upper bound on items in , such that any other upper bound is even larger.
  • or is the upper bound between and .
  • The element is the least element. .
  • We’re moving through the lattice in the direction of the gap: down!
  • In dataflow analysis, we use a meet semilattice—a lattice but with only the meet operation—to combine dataflow information at CFG intersection points.
    • In this context, larger values denote more precise analyses.
    • For instance, in constant propagation, , indicating no precision on what constants the value could be, and , indicating a variable with the possibility of “the most precision”: being unanalyzed so far!

Notation

Sometimes, we use for join and for meet. Interchangeable, mostly

To make sure that join and meet have agreeing behavior, we enforce a rule called absorption:

Note that the meaning of is kind of arbitrary! For instance, in dataflow analysis, we assign to mean that provides a more precise analysis. However, in abstract interpretation, the convention is to flip this meaning: is now the more precise analysis! Additionally, in denotational semantics and domain theory, we use join to compare function specificity: greater functions are defined on more inputs.

In general, what you can rely on is that in , goes down the lattice, and goes up.

Also note that (the smallest upper bound of nothing is the smallest item), and similarly (the largest lower bound of nothing is the largest item).

In a complete lattice, every subset of has a least upper bound and greatest lower bound. In domain theory, a poset where every subset has a least upper bound is called a complete partial order.

Semi-lattices

With semilattices, you only have one of these operations, either join or meet.