Kleene fixpoint theorem
From Wikipedia, the free encyclopedia
In mathematics, the Kleene fixpoint theorem of order theory states that given any complete lattice L, and any continuous (and therefore monotone) function
- <math>f: L \to L,</math>
the least fixed point (lfp) of f is the least upper bound of the ascending Kleene chain of f, that is
- <math>\textrm{bot}_L \le f(\textrm{bot}_L) \le f(f(\textrm{bot}_L)) \le ...</math>
obtained by iterating f on the bottom element of L. Expressed in a formula, the Kleene fixpoint theorem states that
- <math>\textrm{lfp}(f) = \textrm{lub}\left(\left\{f^i(\textrm{bot}_L) \mid i\in\mathbb{N}\right\}\right)</math>
where <math>\textrm{lfp}</math> denotes the least fixed point, <math>\textrm{lub}</math> denotes the least upper bound, and <math>\textrm{bot}_L</math> is the bottom element of <math>L</math>.

