Kleene fixed-point theorem

Computation of the least fixpoint of f(x) = 1/10x²+atan(x)+1 using Kleene's theorem in the real interval [0,7] with the usual order

In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following:

Kleene Fixed-Point Theorem. Suppose $(L,⊑)$ is a directed-complete partial order (dcpo) with a least element, and let $f:L\to 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

$\mathrm{\perp }⊑f(\mathrm{\perp })⊑f(f(\mathrm{\perp }))⊑\cdots ⊑f^n(\mathrm{\perp })⊑\cdots$

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

$\text{<mrow data-mjx-texclass="ORD">lfp</mrow>}(f)=\sup \left(\{f^n(\mathrm{\perp })\mid n\in \mathbb{\mathbb{N}}\}\right)$

where $\text{<mrow data-mjx-texclass="ORD">lfp</mrow>}$ 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

We first have to show that the ascending Kleene chain of $f$ exists in $L$. To show that, we prove the following:

Lemma. If $L$ is a dcpo with a least element, and $f:L\to L$ is Scott-continuous, then $f^n(\mathrm{\perp })⊑f^{n+1}(\mathrm{\perp }),n\in {\mathbb{\mathbb{N}}}_0$

Proof. We use induction:

• Assume n = 0. Then $f^0(\mathrm{\perp })=\mathrm{\perp }⊑f^1(\mathrm{\perp }),$ since $\mathrm{\perp }$ is the least element.
• Assume n > 0. Then we have to show that $f^n(\mathrm{\perp })⊑f^{n+1}(\mathrm{\perp })$. By rearranging we get $f(f^{n-1}(\mathrm{\perp }))⊑f(f^n(\mathrm{\perp }))$. By inductive assumption, we know that $f^{n-1}(\mathrm{\perp })⊑f^n(\mathrm{\perp })$ holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.

As a corollary of the Lemma we have the following directed ω-chain:

$\mathbb{𝕄}=\{\mathrm{\perp },f(\mathrm{\perp }),f(f(\mathrm{\perp })),\dots \}.$

From the definition of a dcpo it follows that $\mathbb{𝕄}$ 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, $f(\sup (\mathbb{𝕄}))=\sup (f(\mathbb{𝕄}))$, that is $f(m)=\sup (f(\mathbb{𝕄}))$. Also, since $\mathbb{𝕄}=f(\mathbb{𝕄})\cup \{\mathrm{\perp }\}$ and because $\mathrm{\perp }$ has no influence in determining the supremum we have: $\sup (f(\mathbb{𝕄}))=\sup (\mathbb{𝕄})$. 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{𝕄}$ is smaller than any fixed-point of $f$ (because by property of supremum, if all elements of a set $D\subseteq L$ 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 $\mathrm{\forall }i\in \mathbb{\mathbb{N}}:f^i(\mathrm{\perp })⊑k$. The base of the induction $(i=0)$ obviously holds: $f^0(\mathrm{\perp })=\mathrm{\perp }⊑k,$ since $\mathrm{\perp }$ is the least element of $L$. As the induction hypothesis, we may assume that $f^i(\mathrm{\perp })⊑k$. 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: $f^i(\mathrm{\perp })⊑k⟹f^{i+1}(\mathrm{\perp })⊑f(k).$ Now, by the assumption that $k$ is a fixed-point of $f,$ we know that $f(k)=k,$ and from that we get $f^{i+1}(\mathrm{\perp })⊑k.$

See also

• Other fixed-point theorems