Kleene fixed-point theorem
|This article does not cite any references or sources. (December 2011)|
- Let L be a 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.
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, 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 directed due to 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. That is, we have to show that . Because is Scott-continuous, , that is . Also, (from the property of the chain) and from 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 . This is done by induction: Assume is some fixed-point of . We now proof 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 .