least fixed point

You are here: irt.org | FOLDOC | 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

FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL