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 ${\displaystyle (L,\sqsubseteq )}${\displaystyle (L,\sqsubseteq )} is a directed-complete partial order (dcpo) with a least element, and let ${\displaystyle f:L\to L}${\displaystyle f:L\to L} be a Scott-continuous (and therefore monotone) function. Then ${\displaystyle f}${\displaystyle f} has a least fixed point, which is the supremum of the ascending Kleene chain of ${\displaystyle f.}${\displaystyle f.}

The ascending Kleene chain of f is the chain

${\displaystyle \bot \sqsubseteq f(\bot )\sqsubseteq f(f(\bot ))\sqsubseteq \cdots \sqsubseteq f^{n}(\bot )\sqsubseteq \cdots }${\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

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

where ${\displaystyle {\textrm {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.^[1] Moreover, the Kleene fixed-point theorem can be extended to monotone functions using transfinite iterations.^[2]

Source:^[3]

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

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

Proof. We use induction:

• Assume n = 0. Then ${\displaystyle f^{0}(\bot )=\bot \sqsubseteq f^{1}(\bot ),}${\displaystyle f^{0}(\bot )=\bot \sqsubseteq f^{1}(\bot ),} since ${\displaystyle \bot }${\displaystyle \bot } is the least element.
• Assume n > 0. Then we have to show that ${\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot )}${\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot )}. By rearranging we get ${\displaystyle f(f^{n-1}(\bot ))\sqsubseteq f(f^{n}(\bot ))}${\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 )}${\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:

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

From the definition of a dcpo it follows that ${\displaystyle \mathbb {M} }${\displaystyle \mathbb {M} } has a supremum, call it ${\displaystyle m.}${\displaystyle m.} What remains now is to show that ${\displaystyle m}${\displaystyle m} is the least fixed-point.

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

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

• Other fixed-point theorems

• Order theory
• Fixed-point theorems

• Articles with short description
• Short description is different from Wikidata