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:

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

\bot \;\leq \;f(\bot )\;\leq \;f\left(f(\bot )\right)\;\leq \;\dots \;\leq \;f^{n}(\bot )\;\leq \;\dots

obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that

{\textrm {lfp}}(f)=\sup \left(\left\{f^{n}(\bot )\mid n\in \mathbb {N} \right\}\right)

where ${\textrm {lfp}}$ denotes the least fixed point.

This result is often attributed to Alfred Tarski, but Tarski's fixed point theorem pertains to monotone functions on complete lattices.

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 $f^{n}(\bot )\leq f^{n+1}(\bot ),n\in \mathbb {N} _{0}$

Proof by induction:

Assume n = 0. Then $f^{0}(\bot )=\bot \leq f^{1}(\bot )$ , since ⊥ is the least element.
Assume n > 0. Then we have to show that $f^{n}(\bot )\leq f^{n+1}(\bot )$ . By rearranging we get $f(f^{n-1}(\bot ))\leq f(f^{n}(\bot ))$ . By inductive assumption, we know that $f^{n-1}(\bot )\leq f^{n}(\bot )$ 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 $\mathbb {M}$ be the set of all elements of the chain: $\mathbb {M} =\{\bot ,f(\bot ),f(f(\bot )),\ldots \}$ . This set is clearly directed due to Lemma 1. 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 least fixed-point.

First, we show that $m$ is a fixed point. That is, we have to show that $f(m)=m$ . Because $f$ is Scott-continuous, $f(\sup(\mathbb {M} ))=\sup(f(\mathbb {M} ))$ , that is $f(m)=\sup(f(\mathbb {M} ))$ . Also, $\sup(f(\mathbb {M} ))=\sup(\mathbb {M} )$ (from the property of the chain) and from 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 contradiction. Assume $k$ is a fixed-point and $k<m$ . Then there has to be an $i$ such that $k=f^{i}(\bot )=f(f^{i}(\bot ))$ . But than for all $j>i$ the result would never be greater than $k$ and so $m$ cannot be a supremum of $\mathbb {M}$ , which is a contradiction.

Proof

See also