# Kleene fixed-point theorem

(Redirected from Kleene fixpoint 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 \; \le \; f(\bot) \; \le \; f\left(f(\bot)\right) \; \le \; \dots \; \le \; f^n(\bot) \; \le \; \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) \le 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 showing that any Element in $\mathbb{M}$ is smaller than any fixed-point of $f$. This is done by induction: Assume $k$ is some fixed-point of $f$. We now proof by induction over $i$ that $\forall i \in \mathbb{N}\colon f^i(\bot) \sqsubseteq k$. For the induction start, we take $i = 0$: $f^0(\bot) = \bot \sqsubseteq k$ obviously holds, since $\bot$ is the smallest element of $L$. As the induction hypothesis, we may assume that $f^i(\bot) \sqsubseteq 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(\bot) \sqsubseteq k ~\implies~ f^{i+1}(\bot) \sqsubseteq 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}(\bot) \sqsubseteq k$.