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.
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)
v
v
f:\wp(V)\to\wp(V)
f(X)=\{v\}\cup\{x\inV:forsomew\inXthereisanarcfromwtox\}.
v
v
Let
G=(V,\Sigma,R,S0)
E
\varepsilon
f:\wp(V)\to\wp(V)
f(X)=\{S\inV: S\inXor(S\to\varepsilon)\inRor(S\toS1...Sn)\inRandSi\inX,foralli\}
\wp(V)
V
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 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,
\bot
int, its mathematical counterpart is defined as Z\bot=Z\cup\{\bot\};
\bot\sqsubsetn
n\inZ
n,m\inZ
\sqsubset
The semantics of a program definition int f(int n){...} is some mathematical function
f:Z\bot\toZ\bot.
f does not terminate for some input n, this can be expressed mathematically as f(n)=\bot.
f\sqsubseteqg
n,
f(n)\sqsubseteqg(n)
f(n)
g(n).
x+x/x is less defined than that of x+1, since the former, but not the latter, maps 0
\bot,
Given some program text f, its mathematical counterpart is obtained as least fixed point of some mapping from functions to functions that can be obtained by "translating" f.For example, the C definition
F:(Z\bot\toZ\bot)\to(Z\bot\toZ\bot),
(F(f))(n)=\begin{cases}1&ifn=0,\ n ⋅ f(n-1)&ifn ≠ \botandn ≠ 0,\ \bot&ifn=\bot.\ \end{cases}
F
fact was defined recursively.Under certain restrictions (see Kleene fixed-point theorem), which are met in the example, F
\operatorname{fact}
(F(\operatorname{fact}))(n)=\operatorname{fact}(n)
n\inZ\bot
\operatorname{fact}(n)=\begin{cases}n!&ifn\geq0,\ \bot&ifn<0orn=\bot.\end{cases}
A larger fixed point of
F
\operatorname{fact}0,
\operatorname{fact}0(n)=\begin{cases}n!&ifn\geq0,\ 0&ifn<0,\ \bot&ifn=\bot,\end{cases}
n;
fact(-1) will not terminate at all, let alone return 0.Only the least fixed point, \operatorname{fact},
Immerman[2] [3] and Vardi[4] 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).
The greatest fixed point of a function can be defined analogously to the least fixed point, as the fixed point which is greater than any other fixed point, according to the order of the poset. In computer science, greatest fixed points are much less commonly used than least fixed points. Specifically, the posets found in domain theory usually do not have a greatest element, hence for a given function, there may be multiple, mutually incomparable maximal fixed points, and the greatest fixed point of that function may not exist. To address this issue, the optimal fixed point has been defined as the most-defined fixed point compatible with all other fixed points. The optimal fixed point always exists, and is the greatest fixed point if the greatest fixed point exists. The optimal fixed point allows formal study of recursive and corecursive functions that do not converge with the least fixed point.[5] Unfortunately, whereas Kleene's recursion theorem shows that the least fixed point is effectively computable, the optimal fixed point of a computable function may be a non-computable function.[6]