Kleene fixed-point theorem
In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following:
The ascending Kleene chain of f is the chain
obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that
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, this result is often attributed to Alfred Tarski who proves it for additive functions. Moreover, the Kleene fixed-point theorem can be extended to monotone functions using transfinite iterations.
Proof
Source:We first have to show that the ascending Kleene chain of exists in. To show that, we prove the following:
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 . 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, we may conclude the following: Now, by the assumption that is a fixed-point of we know that and from that we get