Kleene fixed-point theorem
|This article does not cite any references or sources. (December 2011)|
- 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.
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 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 .