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 ("poset" for short) 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.
Examples With the usual order on the real numbers, the least fixed point of the real function f(x) = x2 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. Let G = ( V , A ) {\displaystyle G=(V,A)} be a directed graph and v {\displaystyle v} be a vertex. The set of vertices accessible from v {\displaystyle v} can be defined as the least fixed-point of the function f : ℘ ( V ) → ℘ ( V ) {\displaystyle f:\wp (V)\to \wp (V)} , defined as f ( X ) = { v } ∪ { x ∈ V : for some w ∈ X there is an edge from w to x } . {\displaystyle f(X)=\{v\}\cup \{x\in V:{\text{ for some }}w\in X{\text{ there is an edge from }}w{\text{ to }}x\}.} The set of vertices which are co-accessible from v {\displaystyle v} is defined by a similar least fix-point. The strongly connected component of v {\displaystyle v} is the intersection of those two least fixed-points. Let G = ( V , Σ , R , S 0 ) {\displaystyle G=(V,\Sigma ,R,S_{0})} be a context-free grammar. The set E {\displaystyle E} of symbols which produces the empty string ε {\displaystyle \varepsilon } can be obtained as the least fixed-point of the function f : ℘ ( V ) → ℘ ( V ) {\displaystyle f:\wp (V)\to \wp (V)} , defined as f ( X ) = { S ∈ V : S ∈ X or ( S → ε ) ∈ R or ( S → S 1 … S n ) ∈ R and S i ∈ X , for all i } {\displaystyle f(X)=\{S\in V:\;S\in X{\text{ or }}(S\to \varepsilon )\in R{\text{ or }}(S\to S^{1}\dots S^{n})\in R{\text{ and }}S^{i}\in X{\text{, for all }}i\}} , where ℘ ( V ) {\displaystyle \wp (V)} denotes the power set of V {\displaystyle V} .
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.
Denotational semantics
In computer science, the denotational semantics approach uses least fixed points to obtain from a given program text a corresponding mathematical function, called its semantics. To this end, an artificial mathematical object, ⊥ {\displaystyle \bot } , is introduced, denoting the exceptional value "undefined". Given e.g. the program datatype int, its mathematical counterpart is defined as Z ⊥ = Z ∪ { ⊥ } ; {\displaystyle \mathbb {Z} _{\bot }=\mathbb {Z} \cup \{\bot \};}
… excerpt ends here. Continue reading the full article.
