Lattices: Fixed Points and Iteration

DEV Community

Here is the payoff. Tarski's theorem: any monotone function on a complete lattice has a least fixed point, computable by iterating from bottom.

Start at (\bot). Apply (f). Join the result with the current value. Repeat until nothing changes. This is Kleene iteration:

$$x_0 = \bot, \quad x_{n+1} = x_n \vee f(x_n)$$

The sequence (x_0 \leq x_1 \leq x_2 \leq \cdots) is ascending. In a finite lattice, it must terminate.

template<BoundedLattice L, typename F>
L least_fixed_point(F f, std::size_t max_iter = 1000) {
 L x = bottom(L{});
 for (std::size_t i = 0; i < max_iter; ++i) {
 L next = join(x, f(x));
 if (next == x) return x;
 x = next;
 }
 return x;
}

This is the lattice analog of power() from the peasant post. There, monoid structure gave us repeated squaring. Here, lattice structure gives us fixed-point iteration. Different algebra, different algorithm, same principle: the structure determines the computation.

Application: Abstract Interpretation

The sign lattice is not just a mathematical curiosity. It is the simplest example of abstract interpretation, a technique for reasoning about programs without running them.

Consider a program variable x. Instead of tracking its concrete value, track its abstract sign. An assignment x = 3 gives x = positive. An operation x = a * b where a is negative and b is positive gives x = negative.

For loops, we need a fixed point. If a loop body adds a positive number to a variable starting at zero, what sign does the variable have after the loop? We compute the least fixed point of the transfer function:

Start: x = bot (unreachable)
Join with initial condition: join(bot, zero) = zero
Apply transfer: zero + positive = positive
Join: join(zero, positive) = top
Apply transfer: top + positive = top
Join: join(top, top) = top. Fixed point reached.

The result is top: the variable could be zero or positive (or, conservatively, anything). The sign lattice is too coarse to distinguish "non-negative" from "unknown". A richer lattice (like intervals) would give a tighter answer.

The point is that the algorithm is the same regardless of the lattice. Swap sign_lattice for interval<int> or powerset<N>, and least_fixed_point still works. The lattice structure determines the iteration.

The Connection

In the peasant post, the observation was: any monoid supports efficient exponentiation. In the accumulator post: any monoid supports composable streaming computation. Here: any bounded lattice supports fixed-point iteration.

Each algebraic structure comes with its own generic algorithm. Monoid structure gives power(). Lattice structure gives least_fixed_point(). The pattern repeats: define the algebra, get the algorithm.

Algorithms arise from algebraic structure.