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 (also, it pertains to monotone functions on complete lattices), this result is often attributed to Alfred Tarski who proves it for additive functions. Moreover, 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 f exists in L. 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 \mathbb{M} has a supremum, call it m. What remains now is to show that m is the least fixed-point. First, we show that m is a fixed point, i.e. that f(m) = m. Because f is Scott-continuous,, that is. Also, since and because \bot has no influence in determining the supremum we have:. It follows that f(m) = m, making m a fixed-point of f. The proof that m is in fact the least fixed point can be done by showing that any element in \mathbb{M} is smaller than any fixed-point of f (because by property of supremum, if all elements of a set are smaller than an element of L then also \sup(D) is smaller than that same element of L). This is done by induction: Assume k is some fixed-point of f. We now prove by induction over i that. The base of the induction (i = 0) obviously holds: since \bot is the least element of L. As the induction hypothesis, we may assume that. We now do the induction step: From the induction hypothesis and the monotonicity of f (again, implied by the Scott-continuity of f), we may conclude the following: Now, by the assumption that k is a fixed-point of f, we know that f(k) = k, and from that we get