Kleene fixed-point theorem: Difference between revisions

Revision as of 16:39, 1 February 2017

Revision as of 06:43, 9 March 2017

Line 2:

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, ⊑\sqsubseteq)</math> beis a CPO ([[complete partial order]]), or CPO for short, 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 \; \sqsubseteq \; f(\bot) \; \sqsubseteq \; f\left(f(\bot)\right) \; \sqsubseteq \; \dots \;cdots \sqsubseteq \; f^n(\bot) \; \sqsubseteq \; \dotscdots</math>

obtained by [[iterated function|iterating]] ''f'' on the [[least element]] ⊥ of ''L''. Expressed in a formula, the theorem states that

Line 17 ⟶ 18:

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]]).

== Proof<ref>{{Cite book|url=https://doi.org/10.1017/CBO9781139166386|title=Mathematical Theory of Domains by V. Stoltenberg-Hansen|last=Stoltenberg-Hansen |first=V.| last2=Lindstrom |first2=I.|last3=Griffor|first3=E. R.|publisher=Cambridge University Press |year=1994 |isbn=0521383447|___location=|pages=24|language=en|doi=10.1017/cbo9781139166386|quote=|via=}}</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 a CPO, and <math>f&nbsp;:&nbsp; L&nbsp;→&nbsp; \to L</math> is a Scott-continuous function, then <math>f^n(\bot) \sqsubseteq f^{n+1}(\bot), n \in \mathbb{N}_0</math>

We first have to show that the ascending Kleene chain of ''f'' exists in L. To show that, we prove the following lemma:

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

:Lemma 1:''If L is CPO, and f&nbsp;:&nbsp;L&nbsp;→&nbsp;L is a Scott-continuous function, then <math>f^n(\bot) \sqsubseteq f^{n+1}(\bot), n \in \mathbb{N}_0</math>

:* 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.

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

Proof by induction:

* Assume n = 0. Then <math>f^0(\bot) = \bot \sqsubseteq f^1(\bot)</math>, since ⊥ 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.

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

Immediate corollary of Lemma 1 is the existence of the chain.

Let <math>\mathbb{M}</math> beFrom the setdefinition of allCPO elementsit offollows the chain:that <math>\mathbb{M} = \{ \bot, f(\bot), f(f(\bot)), \ldots\}</math>. This set is clearly a directed/ω-chain, as a corollary of 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, 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>f(\mathbb{M}) = \mathbb{M}\setminus\{\bot\}</math> and because <math>\bot</math> has no influence in determining <math>\sup</math>,the supremum we have that: <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 Elementelement 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}\colon: f^i(\bot) \sqsubseteq k</math>. ForThe base of the induction start, we take <math>(i = 0)</math> obviously holds: <math>f^0(\bot) = \bot \sqsubseteq k,</math> obviously holds, since <math>\bot</math> is the smallestleast 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 ==