Kleene fixed-point theorem

In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following: The ascending Kleene chain of f is the chain obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that where

lfp

{\displaystyle {\textrm {lfp}}}

denotes the least fixed point.

Although Tarski's fixed point theorem does not consider how fixed points can be computed by iterating f from some seed (also, it pertains to monotone functions on complete lattices), this result is often attributed to Alfred Tarski who proves it for additive functions.

[1] Moreover, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.

[2] Source:[3] We first have to show that the ascending Kleene chain of

exists in

To show that, we prove the following: As a corollary of the Lemma we have the following directed ω-chain: From the definition of a dcpo it follows that

has a supremum, call it

What remains now is to show that

is the least fixed-point.

First, we show that

is a fixed point, i.e. that

has no influence in determining the supremum we have:

, making

The proof that

is in fact the least fixed point can be done by showing that any element in

is smaller than any fixed-point of

(because by property of supremum, if all elements of a set

are smaller than an element of

is smaller than that same element of

This is done by induction: Assume

We now prove by induction over

The base of the induction

As the induction hypothesis, we may assume that

We now do the induction step: From the induction hypothesis and the monotonicity of

(again, implied by the Scott-continuity of

), we may conclude the following:

Now, by the assumption that