Least fixed point

A function f may have many fixed points (x such that f x = x).

For example, any value is a fixed point of the identity function, (\ x . x).

If f is recursive, we can represent it as

f = fix F

where F is some higher-order function and

fix F = F (fix F).

The standard denotational semantics of f is then given by the least fixed point of F.

This is the least upper bound of the infinite sequence (the ascending Kleene chain) obtained by repeatedly applying F to the totally undefined value, bottom.


fix F = LUB bottom, F bottom, F (F bottom), ....

The least fixed point is guaranteed to exist for a continuous function over a cpo.

< Previous Terms Terms Containing least fixed point Next Terms >
leapfrog attack
leap second
learning curve
leased line
continuous function
fixed point
least fixed point
least recently used
least significant bit
least upper bound