Knaster–Tarski theorem
In the mathematical areas of order and lattice theory, the Knaster–Tarski theorem, named after Bronisław Knaster and Alfred Tarski, states the following:
It was Tarski who stated the result in its most general form, and so the theorem is often known as Tarski's fixed point theorem. Some time earlier, Knaster and Tarski established the result for the special case where L is the lattice of subsets of a set, the power set lattice.
The theorem has important applications in formal semantics of programming languages and abstract interpretation.
A kind of converse of this theorem was proved by Anne C. Davis: If every order preserving function f : L → L on a lattice L has a fixed point, then L is a complete lattice.
Since complete lattices cannot be empty (they must contain supremum of empty set), the theorem in particular guarantees the existence of at least one fixed point of f, and even the existence of a least (or greatest) fixed point. In many practical cases, this is the most important implication of the theorem.
The least fixpoint of f is the least element x such that f(x) = x, or, equivalently, such that f(x) ≤ x; the dual holds for the greatest fixpoint, the greatest element x such that f(x) = x.
If f(lim xn)=lim f(xn) for all ascending sequences xn, then the least fixpoint of f is lim fn(0) where 0 is the least element of L, thus giving a more "constructive" version of the theorem. (See: Kleene fixed-point theorem.) More generally, if f is monotonic, then the least fixpoint of f is the stationary limit of fα(0), taking α over the ordinals, where fα is defined by transfinite induction: fα+1 = f ( fα) and fγ for a limit ordinal γ is the least upper bound of the fβ for all β ordinals less than γ. The dual theorem holds for the greatest fixpoint.
...
Wikipedia