Francais | English | Espanõl

Kleene fixpoint theorem

From Wikipedia, the free encyclopedia

Jump to: navigation, search

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>.


[edit] See also

Personal tools