Kleene fixed-point theorem: Difference between revisions

Revision as of 18:33, 8 April 2012

Latest revision as of 06:58, 10 May 2025

(42 intermediate revisions by 34 users not shown)

Line 1:

{{Short description|Theorem in order theory and lattice theory}}

{{Unreferenced|date=December 2011}}

{{otheruses4|Kleene's fixed-point theorem in lattice theory|the fixed-point theorem in computability theory|Kleene's recursion theorem}}

[[File:Kleene fixpoint svg.svg|thumb|Computation of the least fixpoint of ''f''(''x'') = {{sfrac|1|10}}''x''²+[[arctangent|atan]](''x'')+1 using Kleene's theorem in the real [[interval (mathematics)|interval]] [0,7] with the usual order]]

In the [[mathematics|mathematical]] areas of [[order theory|order]] and [[lattice theory]], the '''Kleene fixed-point theorem''', named after American mathematician [[Stephen Cole Kleene]], states the following:

:''Let'Kleene Fixed-Point Theorem.''' Suppose <math>(L, be\sqsubseteq)</math> is a [[complete partial order|directed-complete partial order]] (dcpo) with a least element, and let <math>f&nbsp;:&nbsp; L&nbsp;→&nbsp; \to L</math> be a [[Scott continuity|Scott-continuous]] (and therefore [[monotone function|monotone]]) [[function (mathematics)|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 (order theory)|chain]]

:<math>\bot \; \lesqsubseteq \; f(\bot) \; \le \;sqsubseteq f\left(f(\bot)\right) \;sqsubseteq \lecdots \; \dots \; \le \;sqsubseteq f^n(\bot) \; \le \;sqsubseteq \dotscdots</math>

obtained by [[iterated function|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>

Line 14 ⟶ 16:

where <math>\textrm{lfp}</math> denotes the least fixed point.

Although [[Tarski's fixed point theorem]]

This result is often attributed to [[Alfred Tarski]], but the original statement of [[Tarski's fixed point theorem]] is about monotone functions on complete lattices. Since all complete lattices are complete partial orders but not vice-versa, and since all monotone functions on complete lattices are Scott-continuous, Tarski's fixed point theorem is entailed by the present result. (It is not guaranteed that all non-empty subsets of a complete partial order are [[directed set|directed]]; a complete lattice C is a complete partial order with the additional properties that (i) all C's non-empty subsets are directed and (ii) for every non-empty subset of C the subset's [[upper set|upper closure]] is a [[filter (mathematics)|filter]].) Yet from a set-theoretic point of view Tarski's result seems the more fundamental of the two, in the following sense: proving Kleene's result in axiomatic set theory requires a definition of, and existence proof for, the ascending Kleene chain, and since axiomatic set theory includes no syntactic element whose semantics are comparable to those of the ellipsis "..." contained in the above informal definition, axiomatic set theory will require a different sort of definition of the ascending Kleene chain. An existence proof for that chain, defined as it must be in a rigorous axiomatic set theory, appears to requires use of Tarski's theorem.

does not consider how fixed points can be computed by iterating ''f'' from some seed (also, it pertains to [[monotone function]]s on [[complete lattices]]), this result is often attributed to [[Alfred Tarski]] who proves it for additive functions.<ref>{{cite journal | author=Alfred Tarski | url=http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.pjm/1103044538 | title=A lattice-theoretical fixpoint theorem and its applications | journal = [[Pacific Journal of Mathematics]] | volume=5 | year=1955 | issue=2 | pages=285&ndash;309| doi=10.2140/pjm.1955.5.285 }}, page 305.</ref> Moreover, the Kleene fixed-point theorem can be extended to [[monotone function]]s using transfinite iterations.<ref>{{cite journal | author=Patrick Cousot and Radhia Cousot | url=https://projecteuclid.org/euclid.pjm/1102785059 | title=Constructive versions of Tarski's fixed point theorems | journal = Pacific Journal of Mathematics | volume=82 | year=1979 | issue=1 | pages=43&ndash;57| doi=10.2140/pjm.1979.82.43 }}</ref>

== Proof ==

Source:<ref>{{Cite book|title=Mathematical Theory of Domains by V. Stoltenberg-Hansen|last1=Stoltenberg-Hansen|first1=V.|last2=Lindstrom|first2=I.|last3=Griffor|first3=E. R.|publisher=Cambridge University Press|year=1994|isbn=0521383447|pages=[https://archive.org/details/mathematicaltheo0000stol/page/24 24]|language=en|doi=10.1017/cbo9781139166386|url=https://archive.org/details/mathematicaltheo0000stol/page/24}}</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 continuity|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 ==

* [[Knaster–Tarski theorem]]

* Other [[fixed-point theorem]]s

== References ==

{{Reflist}}

[[Category:Order theory]]

[[Category:Fixed-point theorems]]

[[Category:Theorems in discrete mathematics]]

{{mathlogic-stub}}

[[fr:Théorème du point fixe de Kleene]]

[[zh:克莱尼不动点定理]]