Least fixed point

In order theory, a branch of mathematics, the least fixed point (lfp or LFP) of a function is the fixed point which is less than or equal to all other fixed points, according to some partial order.

For example, the least fixed point of the real function

:"f"("x") = "x"²

is "x" = 0 with the usual order on the real numbers (since the only other fixpoint is 1 and 0 < 1). 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 somehow related to making recursive definitions (see domain theory and/or denotational semantics for details).

Immerman [N. Immerman, Relational queries computable in polynomial time, Information and Control 68 (1–3) (1986) 86–104.] and Vardi [M. Y. Vardi, The complexity of relational query languages, in: Proc. 14th ACM Symp. on Theory of Computing, 1982, pp. 137–146.] independently showed the descriptive complexity result that the polynomial-time computable properties of linearly ordered structures are definable in LFP. However, LFP is too weak to express all polynomial-time properties of unordered structures (for instance that a structure has even size).

Notes

See also

*Greatest fixed point (less commonly used)
*Kleene fixpoint theorem
*Knaster–Tarski theorem

References

* Immerman, Neil. "Descriptive Complexity", 1999, Springer-Verlag.
* Libkin, Leonid. "Elements of Finite Model Theory", 2004, Springer.