Lattices & CPOs — where fixed points live
Parent: order-theory
The completeness ladder
- lattice — a poset where every pair has a least upper bound (join
∨) and greatest lower bound (meet∧).- complete lattice — every subset has a join and a meet (so there's a top
⊤and bottom⊥).- CPO / dcpo — a poset with a least element
⊥and joins of all directed sets (or of all chains).
Why these two exact strengths: they are the homes of the constructive fixed-point theorems (no choice needed):
- complete lattice → Knaster–Tarski: a monotone map has a whole complete lattice of fixed points (a least and a greatest).
- CPO → Kleene: a Scott-continuous map has a least fixed point
⊔ₙ fⁿ(⊥), reached by climbing from⊥— the semantics of recursion.
Examples: the powerset under ⊆ (complete lattice); divisors of n under | (a lattice); partial functions ordered by extension, and "flat" data domains, are CPOs (⊥ = "undefined") — the setting for denotational semantics.