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 CPO (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

${\displaystyle \bot \;\sqsubseteq \;f(\bot )\;\sqsubseteq \;f\left(f(\bot )\right)\;\sqsubseteq \;\dots \;\sqsubseteq \;f^{n}(\bot )\;\sqsubseteq \;\dots }$

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

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

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

This result is often attributed to Alfred Tarski, but 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).

Proof^[1]

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

Proof by induction:

• Assume n = 0. Then ${\displaystyle f^{0}(\bot )=\bot \sqsubseteq f^{1}(\bot )}$ , since ⊥ is the least element.
• Assume n > 0. Then we have to show that ${\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot )}$ . By rearranging we get ${\displaystyle f(f^{n-1}(\bot ))\sqsubseteq f(f^{n}(\bot ))}$ . By inductive assumption, we know that ${\displaystyle f^{n-1}(\bot )\sqsubseteq 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 ${\displaystyle \mathbb {M} }$  be the set of all elements of the chain: ${\displaystyle \mathbb {M} =\{\bot ,f(\bot ),f(f(\bot )),\ldots \}}$ . This set is clearly a directed/ω-chain, as a corollary of Lemma 1. From definition of CPO follows that this set has a supremum, we will call it ${\displaystyle m}$ . What remains now is to show that ${\displaystyle m}$  is the least fixed-point.

First, we show that ${\displaystyle m}$  is a fixed point, i.e. that ${\displaystyle f(m)=m}$ . Because ${\displaystyle f}$  is Scott-continuous, ${\displaystyle f(\sup(\mathbb {M} ))=\sup(f(\mathbb {M} ))}$ , that is ${\displaystyle f(m)=\sup(f(\mathbb {M} ))}$ . Also, since ${\displaystyle f(\mathbb {M} )=\mathbb {M} \setminus \{\bot \}}$  and because ${\displaystyle \bot }$  has no influence in determining ${\displaystyle \sup }$ , we have that ${\displaystyle \sup(f(\mathbb {M} ))=\sup(\mathbb {M} )}$ . It follows that ${\displaystyle f(m)=m}$ , making ${\displaystyle m}$  a fixed-point of ${\displaystyle f}$ .

The proof that ${\displaystyle m}$  is in fact the least fixed point can be done by showing that any Element in ${\displaystyle \mathbb {M} }$  is smaller than any fixed-point of ${\displaystyle f}$  (because by property of supremum, if all elements of a set ${\displaystyle D\subseteq L}$  are smaller than an element of ${\displaystyle L}$  then also ${\displaystyle \sup(D)}$  is smaller than that same element of ${\displaystyle L}$ ). This is done by induction: Assume ${\displaystyle k}$  is some fixed-point of ${\displaystyle f}$ . We now prove by induction over ${\displaystyle i}$  that ${\displaystyle \forall i\in \mathbb {N} \colon f^{i}(\bot )\sqsubseteq k}$ . For the induction start, we take ${\displaystyle i=0}$ : ${\displaystyle f^{0}(\bot )=\bot \sqsubseteq k}$  obviously holds, since ${\displaystyle \bot }$  is the smallest element of ${\displaystyle L}$ . As the induction hypothesis, we may assume that ${\displaystyle f^{i}(\bot )\sqsubseteq k}$ . We now do the induction step: From the induction hypothesis and the monotonicity of ${\displaystyle f}$  (again, implied by the Scott-continuity of ${\displaystyle f}$ ), we may conclude the following: ${\displaystyle f^{i}(\bot )\sqsubseteq k~\implies ~f^{i+1}(\bot )\sqsubseteq f(k)}$ . Now, by the assumption that ${\displaystyle k}$  is a fixed-point of ${\displaystyle f}$ , we know that ${\displaystyle f(k)=k}$ , and from that we get ${\displaystyle f^{i+1}(\bot )\sqsubseteq k}$ .

See also

• Knaster–Tarski theorem
• Other fixed-point theorems

References

1. Stoltenberg-Hansen, V.; Lindstrom, I.; Griffor, E. R. (1994). Mathematical Theory of Domains by V. Stoltenberg-Hansen. Cambridge University Press. p. 24. doi:10.1017/cbo9781139166386. ISBN 0521383447.