Kleene fixed-point theorem
|This article does not cite any sources. (December 2011) (Learn how and when to remove this template message)|
- Let (L, ⊑) be a CPO (complete partial order), and let f : L → L be a Scott-continuous (and therefore monotone) function. Then f has a least fixed point, which is the supremum of the ascending Kleene chain of f.
The ascending Kleene chain of f is the chain
where denotes the least fixed point.
This result is often attributed to Alfred Tarski, but 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).
We first have to show that the ascending Kleene chain of f exists in L. To show that, we prove the following lemma:
- Lemma 1:If L is CPO, and f : L → L is a Scott-continuous function, then
Proof by 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.
Immediate corollary of Lemma 1 is the existence of the chain.
Let be the set of all elements of the chain: . This set is clearly a directed/ω-chain, as a corollary of Lemma 1. From definition of CPO follows that this set has a supremum, we will 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 , we have that . 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 . For the induction start, we take : obviously holds, since is the smallest 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 .
- Stoltenberg-Hansen, V.; Lindstrom, I.; Griffor, E. R. (1994). Mathematical Theory of Domains by V. Stoltenberg-Hansen. Cambridge University Press. p. 24. doi:10.1017/cbo9781139166386. ISBN 0521383447.