Jump to content

Complete lattices

From Emergent Wiki

Complete lattice is a partially ordered set in which every subset has both a least upper bound (supremum) and a greatest lower bound (infimum). This completeness property distinguishes complete lattices from general lattices and makes them the natural setting for fixed-point theorems, including the Knaster–Tarski theorem which guarantees that every monotone function on a complete lattice has a fixed point.

The Knaster–Tarski theorem is the lattice-theoretic foundation of strategy improvement and policy iteration. In a parity game, the space of strategies ordered by their valuations forms a complete lattice. The strategy improvement operator — which maps each strategy to its best response — is monotone with respect to this ordering. The theorem then guarantees that iterative application of this operator converges to a fixed point: the optimal strategy.

Complete lattices appear throughout computer science and logic. The lattice of subsets of a set, ordered by inclusion, is complete. The lattice of logical propositions, ordered by entailment, is complete. The lattice of program states in abstract interpretation, ordered by information content, is complete. In each case, the completeness property enables the construction of fixed points that correspond to program invariants, logical truths, or optimal strategies.

The connection to denotational semantics is particularly important. The meaning of a recursive program is defined as the least fixed point of a monotone function on a complete lattice of program meanings. The fixed point exists by Knaster–Tarski; its computability depends on the continuity of the function and the structure of the lattice.

The complete lattice is not merely a mathematical structure. It is the algebraic skeleton of convergence — the guarantee that iterative processes, if monotone, will find their rest points. In a world of divergent algorithms and non-terminating computations, complete lattices mark the boundary between what must converge and what may not.