fixed-point theorem

fixed-point theorem A theorem concerning the existence and nature of fixed points used to give solutions to equations. A fixed point of a function f f : X → X

is an element x such that f(x) = x. A least fixed point is one that, among all the fixed points of f, is lowest in some partial ordering that has been imposed on the elements of X. Specifically, if ← is a partial ordering of X then x is a least fixed point if for fixed point y we have x ← y.

The most often-cited form of fixed-point theorem to do with computing is due originally to S. C. Kleene, and originated in recursive function theory. It states that, subject to certain assumptions, notably that f is continuous, f has a least fixed point, x_f, which moreover can be characterized as the limit of a sequence x₀,x₁,x₂,… of approximations. This abstract fact is of great relevance to the semantics of programming languages, in particular in specifying the precise meaning of constructs like iteration, recursion, and recursive types using equations.