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:

Kleene Fixed-Point Theorem. Suppose ( L , ⊑ ) {\displaystyle (L,\sqsubseteq )} is a directed-complete partial order (dcpo) with a least element, and let f : L → L {\displaystyle f:L\to L} be a Scott-continuous (and therefore monotone) function. Then f {\displaystyle f} has a least fixed point, which is the supremum of the ascending Kleene chain of f . {\displaystyle f.}

The ascending Kleene chain of f is the chain

⊥ ⊑ f ( ⊥ ) ⊑ f ( f ( ⊥ ) ) ⊑ ⋯ ⊑ f n ( ⊥ ) ⊑ ⋯ {\displaystyle \bot \sqsubseteq f(\bot )\sqsubseteq f(f(\bot ))\sqsubseteq \cdots \sqsubseteq f^{n}(\bot )\sqsubseteq \cdots }

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

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

where lfp {\displaystyle {\textrm {lfp}}} 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, the 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 {\displaystyle f} exists in L {\displaystyle L} . To show that, we prove the following:

Lemma. If L {\displaystyle L} is a dcpo with a least element, and f : L → L {\displaystyle f:L\to L} is Scott-continuous, then f n ( ⊥ ) ⊑ f n + 1 ( ⊥ ) , n ∈ N 0 {\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot ),n\in \mathbb {N} _{0}}

Proof. We use induction: Assume n = 0. Then f 0 ( ⊥ ) = ⊥ ⊑ f 1 ( ⊥ ) , {\displaystyle f^{0}(\bot )=\bot \sqsubseteq f^{1}(\bot ),} since ⊥ {\displaystyle \bot } is the least element. Assume n > 0. Then we have to show that f n ( ⊥ ) ⊑ f n + 1 ( ⊥ ) {\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot )} . By rearranging we get f ( f n − 1 ( ⊥ ) ) ⊑ f ( f n ( ⊥ ) ) {\displaystyle f(f^{n-1}(\bot ))\sqsubseteq f(f^{n}(\bot ))} . By inductive assumption, we know that f n − 1 ( ⊥ ) ⊑ f n ( ⊥ ) {\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. As a corollary of the Lemma we have the following directed ω-chain:

M = { ⊥ , f ( ⊥ ) , f ( f ( ⊥ ) ) , … } . {\displaystyle \mathbb {M} =\{\bot ,f(\bot ),f(f(\bot )),\ldots \}.}

… excerpt ends here. Continue reading the full article.