View source for Isocitrate dehydrogenase

{{Unreferenced|date=December 2011}}

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 [[complete partial order]], and let f&nbsp;:&nbsp;L&nbsp;→&nbsp;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 \; \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>

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 [[monotone function]]s on [[complete lattices]].

== Proof ==

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: 
* Assume n = 0. Then <math>f^0(\bot) = \bot \leq f^1(\bot)</math>, since ⊥ is the least element.
* Assume n > 0. Then we have to show that <math>f^n(\bot) \leq f^{n+1}(\bot)</math>. By rearranging we get <math>f(f^{n-1}(\bot)) \leq f(f^n(\bot))</math>. By inductive assumption, we know that <math>f^{n-1}(\bot) \leq 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 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>.

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>. 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 ==
* [[Knaster–Tarski theorem]]
* Other [[fixed-point theorem]]s

[[Category:Order theory]]
[[Category:Fixed-point theorems]]