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

then

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

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

where lfp denotes the least fixed point, lub denotes the least upper bound, and bot_L is the bottom element of L.

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

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

where gfp denotes the greatest fixed point, glb denotes the greatest lower bound, and top_L is the top element of L.

[edit] See also

• Knaster–Tarski theorem
• Other fixed-point theorems