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.
I.e.
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 > |
| LEAP leapfrog attack leap second learning curve leased line | continuous function fixed point least fixed point Mu | least recently used least significant bit least upper bound leaves LEC |
