Kleene fixed-point theorem: Difference between revisions

Revision as of 17:12, 9 December 2012

Revision as of 19:42, 14 December 2012

Line 28:

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

Let '''M''' 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. From definition of CPO follows that this set has a supremum, we will call it ''m''. What remains now is to show that ''m'' is the fixpoint. that is, we have to show that ''f''(''m'') = ''m''. Because ''f'' is [[Scott continuity|Scott-continuous]], ''f''(sup(''M'')) = sup(''f''(''M))'')), that is ''f''(''m'') = sup(''f''(''M))'')). But ''sup(''f''(''M'')) = sup(''M)'') (from the property of the chain) and from that ''f''(''m'') = ''m'', making ''m'' a fixpoint.

The proof that ''m'' is the least fixpoint can be done by contradiction. Assume ''k'' is a fixpoint and ''k'' < ''m''. Than there has to be ''i'' such that <math>k = f^i(\bot) = f(f^i(\bot))</math>. But than for all ''j > i'' the result would never be greater than ''k'' and so ''m'' cannot be a supremum of '''M''', which is a contradiction.

== See also ==