Kleene fixed-point theorem

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

The ascending Kleene chain of f is the chain

[math]\displaystyle{ \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]\displaystyle{ \textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right) }[/math]

where [math]\displaystyle{ \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 Moreover, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.

Proof

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

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

Proof. We use induction:

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

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

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

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

See also

• Other fixed-point theorems