Kleene fixed-point theorem: Difference between revisions

Revision as of 23:55, 23 July 2013

Latest revision as of 06:58, 10 May 2025

(29 intermediate revisions by 25 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.

This result is often attributed to [[Alfred Tarski]], butAlthough [[Tarski's fixed point theorem]] pertains to [[Monotone function|monotone functions]] on [[complete lattices]].

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:

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

:'''Proof.''' byWe use induction:

:* Assume n = 0. Then <math>f^0(\bot) = \bot \leqsqsubseteq 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) \leqsqsubseteq f^{n+1}(\bot)</math>. By rearranging we get <math>f(f^{n-1}(\bot)) \leqsqsubseteq f(f^n(\bot))</math>. By inductive assumption, we know that <math>f^{n-1}(\bot) \leqsqsubseteq f^n(\bot)</math> holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.

ImmediateAs a corollary of the Lemma 1we ishave the existencefollowing of thedirected ω-chain.:

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

Let <math>\mathbb{M}</math> be the set of all elements of the chain: <math>\mathbb{M} = \{ \bot, f(\bot), f(f(\bot)), \ldots\}</math>. This set is clearly directed due to Lemma 1. From definition of CPO follows that this set has a supremum, we will call it <math>m</math>. What remains now is to show that <math>m</math> is the least fixed-point.

First,From wethe showdefinition that <math>m</math> isof a fixeddcpo point.it That is, we have to showfollows 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> has a supremum, thatcall isit <math>f(m) = \sup(f(\mathbb{M}))</math>. Also, <math>\sup(f(\mathbb{M})) = \sup(\mathbb{M})</math> (fromWhat theremains propertynow ofis theto chain) and fromshow that <math>f(m) = m</math>, makingis <math>m</math>the aleast fixed-point of <math>f</math>.

TheFirst, proofwe show that <math>m</math> is in fact the ''least''a fixed point, can be done by showingi.e. that any Element in <math>\mathbb{M}</math>f(m) is= smaller than any fixed-point of <math>fm</math>. This is done by induction: AssumeBecause <math>kf</math> is some[[Scott fixedcontinuity|Scott-point ofcontinuous]], <math>f</math>. We now proof by induction over <math>i</math> that <math>(\forall i \in sup(\mathbb{NM}\colon)) = \sup(f^i(\botmathbb{M})) \sqsubseteq k</math>. For the induction start, wethat take <math>i = 0</math>:is <math>f^0(\botm) = \bot sup(f(\sqsubseteq kmathbb{M}))</math>. obviously holdsAlso, since <math>\bot</math>mathbb{M} is= the smallest element of <math>L</math>. As the induction hypothesis, we may assume that <math>f^i(\botmathbb{M}) \sqsubseteq kcup\{\bot\}</math>. We now do the induction step: From the induction hypothesis and the monotonicity ofbecause <math>f\bot</math> (again,has impliedno byinfluence thein Scott-continuitydetermining ofthe <math>f</math>),supremum we may conclude the followinghave: <math>\sup(f^i(\botmathbb{M})) \sqsubseteq= k ~\implies~ f^sup(\mathbb{i+1M}(\bot) \sqsubseteq f(k)</math>. Now,It by the assumptionfollows that <math>k</math>f(m) is= a fixed-point of <math>fm</math>, we know thatmaking <math>f(k) = km</math>, anda fromfixed-point that we getof <math>f^{i+1}(\bot) \sqsubseteq k</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]]

{{mathlogic-stub}}