Kleene fixed-point theorem: Difference between revisions

Content deleted Content added
LDL128 (talk | contribs)
LDL128 (talk | contribs)
No edit summary
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 (L, ⊑) be a CPO ([[complete partial order]]), and let f : L → L be a [[Scott continuity|Scott-continuous]] (and therefore [[monotone function|monotone]]) [[function (mathematics)|function]]. Then f has a [[least fixed point]], which is the [[supremum]] of the ascending Kleene chain of f.
 
The '''ascending Kleene chain''' of ''f'' is the [[chain (order theory)|chain]]
 
:<math>\bot \; \lesqsubseteq \; f(\bot) \; \lesqsubseteq \; f\left(f(\bot)\right) \; \lesqsubseteq \; \dots \; \lesqsubseteq \; f^n(\bot) \; \lesqsubseteq \; \dots</math>
 
obtained by [[iterated function|iterating]] ''f'' on the [[least element]] ⊥ of ''L''. Expressed in a formula, the theorem states that
Line 20:
We first have to show that the ascending Kleene chain of ''f'' exists in L. To show that, we prove the following lemma:
 
:Lemma 1:''If L is CPO, and f&nbsp;:&nbsp;L&nbsp;→&nbsp;L is a Scott-continuous, then <math>f^n(\bot) \lesqsubseteq f^{n+1}(\bot), n \in \mathbb{N}_0</math>
 
Proof by induction:
* Assume n = 0. Then <math>f^0(\bot) = \bot \leqsqsubseteq f^1(\bot)</math>, since ⊥ 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.
 
Immediate corollary of Lemma 1 is the existence of the chain.
 
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 a directed/ω-chain, as a duecorollary toof 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>, 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>.