Kleene fixed-point theorem

File:Kleene fixpoint svg.svg

Computation of the least fixpoint of f(x) = Template:Sfracx²+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 <math>(L, \sqsubseteq)</math> is a directed-complete partial order (dcpo) with a least element, and let <math>f: L \to L</math> be a Scott-continuous (and therefore monotone) function. Then <math>f</math> has a least fixed point, which is the supremum of the ascending Kleene chain of <math>f.</math>

The ascending Kleene chain of f is the chain

<math>\bot \sqsubseteq f(\bot) \sqsubseteq f(f(\bot)) \sqsubseteq \cdots \sqsubseteq f^n(\bot) \sqsubseteq \cdots</math>

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

<math>\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>

where <math>\textrm{lfp}</math> 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.<ref>Template:Cite journal, page 305.</ref> Moreover, the Kleene fixed-point theorem can be extended to monotone functions using transfinite iterations.<ref>Template:Cite journal</ref>

Proof

Source:<ref>Template:Cite book</ref>

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

Lemma. If <math>L</math> is a dcpo with a least element, and <math>f: L \to L</math> is Scott-continuous, then <math>f^n(\bot) \sqsubseteq f^{n+1}(\bot), n \in \mathbb{N}_0</math>

Proof. We use induction:

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

<math>\mathbb{M} = \{ \bot, f(\bot), f(f(\bot)), \ldots\}.</math>

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

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

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

See also

• Other fixed-point theorems