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.