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, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.
Proof
Source:3
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 \}.}From the definition of a dcpo it follows that M {\displaystyle \mathbb {M} } has a supremum, call it m . {\displaystyle m.} What remains now is to show that m {\displaystyle m} is the least fixed-point.
First, we show that m {\displaystyle m} is a fixed point, i.e. that f ( m ) = m {\displaystyle f(m)=m} . Because f {\displaystyle f} is Scott-continuous, f ( sup ( M ) ) = sup ( f ( M ) ) {\displaystyle f(\sup(\mathbb {M} ))=\sup(f(\mathbb {M} ))} , that is f ( m ) = sup ( f ( M ) ) {\displaystyle f(m)=\sup(f(\mathbb {M} ))} . Also, since M = f ( M ) ∪ { ⊥ } {\displaystyle \mathbb {M} =f(\mathbb {M} )\cup \{\bot \}} and because ⊥ {\displaystyle \bot } has no influence in determining the supremum we have: sup ( f ( M ) ) = sup ( M ) {\displaystyle \sup(f(\mathbb {M} ))=\sup(\mathbb {M} )} . It follows that f ( m ) = m {\displaystyle f(m)=m} , making m {\displaystyle m} a fixed-point of f {\displaystyle f} .
The proof that m {\displaystyle m} is in fact the least fixed point can be done by showing that any element in M {\displaystyle \mathbb {M} } is smaller than any fixed-point of f {\displaystyle f} (because by property of supremum, if all elements of a set D ⊆ L {\displaystyle D\subseteq L} are smaller than an element of L {\displaystyle L} then also sup ( D ) {\displaystyle \sup(D)} is smaller than that same element of L {\displaystyle L} ). This is done by induction: Assume k {\displaystyle k} is some fixed-point of f {\displaystyle f} . We now prove by induction over i {\displaystyle i} that ∀ i ∈ N : f i ( ⊥ ) ⊑ k {\displaystyle \forall i\in \mathbb {N} :f^{i}(\bot )\sqsubseteq k} . The base of the induction ( i = 0 ) {\displaystyle (i=0)} obviously holds: f 0 ( ⊥ ) = ⊥ ⊑ k , {\displaystyle f^{0}(\bot )=\bot \sqsubseteq k,} since ⊥ {\displaystyle \bot } is the least element of L {\displaystyle L} . As the induction hypothesis, we may assume that f i ( ⊥ ) ⊑ k {\displaystyle f^{i}(\bot )\sqsubseteq k} . We now do the induction step: From the induction hypothesis and the monotonicity of f {\displaystyle f} (again, implied by the Scott-continuity of f {\displaystyle f} ), we may conclude the following: f i ( ⊥ ) ⊑ k ⟹ f i + 1 ( ⊥ ) ⊑ f ( k ) . {\displaystyle f^{i}(\bot )\sqsubseteq k~\implies ~f^{i+1}(\bot )\sqsubseteq f(k).} Now, by the assumption that k {\displaystyle k} is a fixed-point of f , {\displaystyle f,} we know that f ( k ) = k , {\displaystyle f(k)=k,} and from that we get f i + 1 ( ⊥ ) ⊑ k . {\displaystyle f^{i+1}(\bot )\sqsubseteq k.}
See also
- Other fixed-point theorems
References
Alfred Tarski (1955). "A lattice-theoretical fixpoint theorem and its applications". Pacific Journal of Mathematics. 5:2: 285–309., page 305. http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.pjm/1103044538 ↩
Patrick Cousot and Radhia Cousot (1979). "Constructive versions of Tarski's fixed point theorems". Pacific Journal of Mathematics. 82:1: 43–57. https://projecteuclid.org/euclid.pjm/1102785059 ↩
Stoltenberg-Hansen, V.; Lindstrom, I.; Griffor, E. R. (1994). Mathematical Theory of Domains by V. Stoltenberg-Hansen. Cambridge University Press. pp. 24. doi:10.1017/cbo9781139166386. ISBN 0521383447. 0521383447 ↩