Kleene fixed-point theorem: Difference between revisions

Revision as of 23:55, 23 July 2013

Revision as of 22:38, 20 October 2013

Line 8:

:<math>\bot \; \le \; f(\bot) \; \le \; f\left(f(\bot)\right) \; \le \; \dots \; \le \; f^n(\bot) \; \le \; \dots</math>

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

:<math>\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>

Line 14:

where <math>\textrm{lfp}</math> denotes the least fixed point.

This result is often attributed to [[Alfred Tarski]], but [[Tarski's fixed point theorem]] pertains to [[Monotonemonotone function|monotone functions]]s on [[complete lattices]].

== Proof ==

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) \le f^{n+1}(\bot), n \in \mathbb{N}_0</math>

Proof by induction:

Line 28:

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 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 show 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, <math>\sup(f(\mathbb{M})) = \sup(\mathbb{M})</math> (from the property of the chain) and from that <math>f(m) = m</math>, making <math>m</math> a fixed-point of <math>f</math>.

Line 40:

[[Category:Order theory]]

[[Category:Fixed-point theorems]]

{{mathlogic-stub}}