Tarski's fixed point theorem
Let be a complete lattice and a monotonic function.
- the set of postfix points of (e.g. is a postfix point)
- the set of prefix points of
- the set of fixed points of . Note that .
Theorem: Let . Then is the least element of (dually, is the largest element of ).
Proof. Let range over elements of .
- applying monotonic from we get
- so is a lower bound on , but is the greatest lower bound, so
- is closed under , by monotonicity, so
- is a lower bound on , so
- from and we have , so
- is a lower bound on so it is also a lower bound on a smaller set
In fact, the set of all fixpoints is a lattice itself.
Tarski's Fixed Point theorem shows that in a complete lattice with a monotonic function on this lattice, there is at least one fixed point of , namely the least fixed point .
Iterating Sequences and Omega Continuity
Tarski's theorem guarantees fixpoints in complete lattices, but the above proof does not say how to find them.
How difficult it is to find fixpoints depends on the structure of the lattice.
Let be a monotonic function on a lattice. Let and . We obtain a sequence . Let .
Lemma: The value is a prefix point.
Observation: need not be a fixpoint (example in exercises, e.g. on lattice [0,1] of real numbers).
Definition: A function is -continuous if for every chain we have
Lemma: For an -continuous function , the value is the least fixpoint of .
By definition of -continuous we have .
But because is the least element of the lattice.
Thus and is a fixpoint.
Now let's prove it is the least.
Let be such that . We want . This is equivalent to .
We can prove this by induction : and if , then by monotonicity of and by definition of we have .
When the function is not -continuous, then we obtain as above (we jump over a discontinuity) and then continue iterating. We then take the limit of such sequence, and the limit of limits etc., ultimately we obtain the fixpoint.