Kleene Fixed-point Theorem - Proof

Proof

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 M be the set of all elements of the chain: . This set is clearly directed. From definition of CPO follows that this set has a supremum, we will call it m. What remains now is to show that m is the fixpoint. that is, we have to show that f(m) = m. Because f is continuous, f(sup(M)) = sup(f(M)), that is f(m) = sup(f(M)). But sup(f(M)) = sup(M) (from the property of the chain) and from that f(m) = m, making m a fixpoint.

The proof that m is the least fixpoint can be done by contradiction. Assume k is a fixpoint and k < m. Than there has to be i such that . But than for all j > i the result would never be greater than k and so m cannot be a supremum of M, which is a contradiction.