Knaster–Tarski theorem

The Knaster–Tarski theorem states that every monotone self-map of a complete lattice has a nonempty complete lattice of fixed points, ordered as a sublattice of the original lattice.

Complete lattice: A partially ordered set in which every subset has both a least upper bound and a greatest lower bound. Completeness supplies the bounds used to construct the theorem’s least and greatest fixed points.
Tarski's fixed-point theorem in computer science: The use of order-theoretic fixed-point results to define and analyze recursive computations. It applies the theorem to semantic equations and recursive program behavior.
Banach fixed-point theorem: A theorem guaranteeing a unique fixed point for a contraction mapping on a complete metric space. It uses metric contraction rather than order preservation and gives uniqueness rather than a lattice of solutions.
Alfred Tarski: A Polish-American logician and mathematician whose work shaped model theory, algebra, and the foundations of mathematics. Tarski proved the central fixed-point result for complete lattices.
Monotone function: A function between ordered sets that preserves their order. Order preservation is the theorem’s key condition on the self-map.
Denotational semantics: A method of defining programming-language meaning by mapping programs to mathematical objects. Recursive program meanings are often defined as least fixed points of monotone semantic operators.
Brouwer fixed-point theorem: A theorem stating that every continuous map from a compact convex set to itself has a fixed point. It relies on topology and continuity instead of lattice order and monotonicity.
Bronisław Knaster: A Polish mathematician known for contributions to topology and set theory. Knaster co-authored the 1928 paper establishing the result with Tarski.
Least fixed point: A fixed point that is less than or equal to every other fixed point in an ordered set. The theorem guarantees this extremal solution for every monotone self-map.
Dataflow analysis: A compiler technique that computes information about values and control flow across a program. Its iterative analyses seek fixed points over lattices of program facts.

Linked from 3 pages

Caristi fixed-point theoremCompared with: Tarski obtains fixed points from order structure rather than metric completeness and a potential.