Least fixed point

In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the order of the poset. A function need not have a least fixed point, but if it does then the least fixed point is unique.
For example, with the usual order on the real numbers, the least fixed point of the real function "f"("x") = "x"2 is "x" = 0 (since the only other fixed point is 1 and 0 < 1). In contrast, "f"("x") = "x" + 1 has no fixed points at all, so has no least one, and "f"("x") = "x" has infinitely many fixed points, but has no least one.
Applications.
Many fixed-point theorems yield algorithms for locating the least fixed point. Least fixed points often have desirable properties that arbitrary fixed points do not.
In mathematical logic and computer science, the least fixed point is related to making recursive definitions (see domain theory and/or denotational semantics for details).
Immerman
and Vardi
independently showed the descriptive complexity result that the polynomial-time computable properties of linearly ordered structures are definable in FO(LFP), i.e. in first-order logic with a least fixed point operator. However, FO(LFP) is too weak to express all polynomial-time properties of unordered structures (for instance that a structure has even size).
Examples.
Let "G" = ("V", "A") be a directed graph and "v" be a vertex. The set of nodes accessible from "v" can be defined as the set "S" which is the least fixed-point for the property: "v" belongs to "S" and if "w" belongs to "S" and there is an edge from "w" to "x", then "x" belongs to "S".
The set of nodes which are co-accessible from "v" is defined by a similar least fix-point. On the one hand the strongly connected component of "v" is the intersection of those two least fixed-points.
Let formula_1 be a context-free grammar. The set formula_2 of symbols which produces the empty string formula_3 can be obtained as the least fixed-point of the function formula_4, defined as formula_5, where formula_6 denotes the power set of formula_7.
Greatest fixed points.
Greatest fixed points can also be determined, but they are less commonly used than least fixed points. However, in computer science they, analogously to the least fixed point, give rise to corecursion and codata.