Kleene fixpoint theorem

In mathematics, the Kleene fixpoint theorem of order theory states that given any complete lattice L, and any continuous (and therefore monotone) function

Failed to parse (Missing texvc executable; please see math/README to configure.): f: L \to L,

then

1. The least fixed point (lfp) of f is the least upper bound of the ascending Kleene chain of f, that is

Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{bot}_L \le f(\textrm{bot}_L) \le f(f(\textrm{bot}_L)) \le ...

obtained by iterating f on the bottom element of L. Expressed in a formula, the Kleene fixpoint theorem states that

Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{lfp}(f) = \textrm{lub}\left(\left\{f^i(\textrm{bot}_L) \mid i\in\mathbb{N}\right\}\right)

where Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{lfp}

denotes the least fixed point, Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{lub}
denotes the least upper bound, and  Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{bot}_L
is the bottom element of Failed to parse (Missing texvc executable; please see math/README to configure.): L

.

2. The greatest fixed point (gfp) of f is the greatest lower bound of the descending Kleene chain of f, that is

Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{top}_L \ge f(\textrm{top}_L) \ge f(f(\textrm{top}_L)) \ge ...

obtained by iterating f on the top element of L. I.e. it is stated that

Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{gfp}(f) = \textrm{glb}\left(\left\{f^i(\textrm{top}_L) \mid i\in\mathbb{N}\right\}\right)

where Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{gfp}

denotes the greatest fixed point, Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{glb}
denotes the greatest lower bound, and Failed to parse (Missing texvc executable; please see math/README to configure.): \textrm{top}_L
is the top element of Failed to parse (Missing texvc executable; please see math/README to configure.): L

.

See also

• Other fixed-point theorems