Kleene fixed-point theorem
- Kleene Fixed-Point Theorem. Suppose is a directed-complete partial order (dcpo) with a least element, and let be a Scott-continuous (and therefore monotone) function. Then has a least fixed point, which is the supremum of the ascending Kleene chain of
The ascending Kleene chain of f is the chain
where denotes the least fixed point.
Although Tarski's fixed point theorem does not consider how fixed points can be computed by iterating f from some seed (also, it pertains to monotone functions on complete lattices), this result is often attributed to Alfred Tarski who proves it for additive functions  Moreover, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.
We first have to show that the ascending Kleene chain of exists in . To show that, we prove the following:
- Lemma. If is a dcpo with a least element, and is Scott-continuous, then
- Proof. We use induction:
- Assume n = 0. Then since is the least element.
- Assume n > 0. Then we have to show that . By rearranging we get . By inductive assumption, we know that holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.
As a corollary of the Lemma we have the following directed ω-chain:
From the definition of a dcpo it follows that has a supremum, call it What remains now is to show that is the least fixed-point.
First, we show that is a fixed point, i.e. that . Because is Scott-continuous, , that is . Also, since and because has no influence in determining the supremum we have: . It follows that , making a fixed-point of .
The proof that is in fact the least fixed point can be done by showing that any element in is smaller than any fixed-point of (because by property of supremum, if all elements of a set are smaller than an element of then also is smaller than that same element of ). This is done by induction: Assume is some fixed-point of . We now prove by induction over that . The base of the induction obviously holds: since is the least element of . As the induction hypothesis, we may assume that . We now do the induction step: From the induction hypothesis and the monotonicity of (again, implied by the Scott-continuity of ), we may conclude the following: Now, by the assumption that is a fixed-point of we know that and from that we get
- Other fixed-point theorems
- Alfred Tarski (1955). "A lattice-theoretical fixpoint theorem and its applications". Pacific Journal of Mathematics. 5:2: 285–309., page 305.
- Patrick Cousot and Radhia Cousot (1979). "Constructive versions of Tarski's fixed point theorems". Pacific Journal of Mathematics. 82:1: 43–57.
- Stoltenberg-Hansen, V.; Lindstrom, I.; Griffor, E. R. (1994). Mathematical Theory of Domains by V. Stoltenberg-Hansen. Cambridge University Press. pp. 24. doi:10.1017/cbo9781139166386. ISBN 0521383447.