Kleene fixed-point theorem: Difference between revisions

Revision as of 22:38, 20 October 2013

Revision as of 12:55, 28 June 2014

Line 30:

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, we show that <math>m</math> is a fixed point. That is, we have to showi.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>. (from the property of the chain) andIt fromfollows 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|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 proof by induction over <math>i</math> that <math>\forall i \in \mathbb{N}\colon f^i(\bot) \sqsubseteq k</math>. For the induction start, we take <math>i = 0</math>: <math>f^0(\bot) = \bot \sqsubseteq k</math> obviously holds, since <math>\bot</math> is the smallest 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 ==