Kleene fixed-point theorem: Difference between revisions

Revision as of 06:43, 9 March 2017

Revision as of 23:35, 28 March 2017

Line 3:

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:

:'''Kleene Fixed-Point Theorem.''' Suppose <math>(L, \sqsubseteq)</math> is a [[complete partial order|directed-complete partial order]], or(dcpo) with CPOa forleast shortelement, and let <math>f: L \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]]

Line 22:

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.''' If <math>L</math> is a CPOdcpo with a least element, and <math>f: L \to L</math> is Scott-continuous, then <math>f^n(\bot) \sqsubseteq f^{n+1}(\bot), n \in \mathbb{N}_0</math>

:'''Proof.''' We use induction:

Line 32:

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

From the definition of CPOa dcpo it follows that <math>\mathbb{M}</math> has a supremum, 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 the supremum we have: <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>.