least fixed point

Also found in: Wikipedia.

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.

The least fixed point is guaranteed to exist for a continuous function over a cpo.
References in periodicals archive ?
In the more normal case that only the least fixed point is computable, that will also be safe.
In order to discuss the least fixed point, we will rely on the flow functions being monotonic.
Our least-fixed-point definition is that we take info as the least fixed point of the system

Full browser ?