least fixed point
<mathematics> 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.
(2005-04-12)
Nearby terms:
leap second « learning curve « leased line «
least fixed point » least recently used » least
significant bit » least upper bound
|
