Least fixed point

Partial order on ${\displaystyle \mathbb {Z} _{\bot }}$

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 ${\displaystyle \mathbb {Z} _{\bot }=\mathbb {Z} \cup \{\bot \};}$ it is made a partially ordered set by defining ${\displaystyle \bot \sqsubset n}$ for each ${\displaystyle n\in \mathbb {Z} }$ and letting any two different members ${\displaystyle n,m\in \mathbb {Z} }$ be uncomparable w.r.t. ${\displaystyle \sqsubset }$, see picture.

The semantics of a program definition int f(int n){...} is some mathematical function ${\displaystyle f:\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }.}$ If the program definition f does not terminate for some input n, this can be expressed mathematically as ${\displaystyle f(n)=\bot .}$ The set of all mathematical functions is made partially ordered by defining ${\displaystyle f\sqsubseteq g}$ if, for each ${\displaystyle n,}$ the relation ${\displaystyle f(n)\sqsubseteq g(n)}$ holds, that is, if ${\displaystyle f(n)}$ is less defined or equal to ${\displaystyle g(n).}$ For example, the semantics of the expression x+x/x is less defined than that of x+1, since the former, but not the latter, maps ${\displaystyle 0}$ to ${\displaystyle \bot ,}$ and they agree otherwise.

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

int fact(int n) { if (n == 0) return 1; else return n * fact(n-1); }

is translated to a mapping

${\displaystyle F:(\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot })\to (\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }),}$ defined as ${\displaystyle (F(f))(n)={\begin{cases}1&{\text{if }}n=0,\\n\cdot f(n-1)&{\text{if }}n\neq \bot {\text{ and }}n\neq 0,\\\bot &{\text{if }}n=\bot .\\\end{cases}}}$

The mapping ${\displaystyle F}$ is defined in a non-recursive way, although fact was defined recursively. Under certain restrictions (see Kleene fixed-point theorem), which are met in the example, ${\displaystyle F}$ necessarily has a least fixed point, ${\displaystyle \operatorname {fact} }$, that is ${\displaystyle (F(\operatorname {fact} ))(n)=\operatorname {fact} (n)}$ for all ${\displaystyle n\in \mathbb {Z} _{\bot }}$.[1] It is possible to show that

${\displaystyle \operatorname {fact} (n)={\begin{cases}n!&{\text{if }}n\geq 0,\\\bot &{\text{if }}n<0{\text{ or }}n=\bot .\end{cases}}}$

A larger fixed point of ${\displaystyle F}$ is e.g. the function ${\displaystyle \operatorname {fact} _{0},}$ defined by

${\displaystyle \operatorname {fact} _{0}(n)={\begin{cases}n!&{\text{if }}n\geq 0,\\0&{\text{if }}n<0,\\\bot &{\text{if }}n=\bot ,\end{cases}}}$

however, this function does not correctly reflect the behavior of the above program text for negative ${\displaystyle n;}$ e.g. the call fact(-1) will not terminate at all, let alone return 0. Only the least fixed point, ${\displaystyle \operatorname {fact} ,}$ can reasonably be used as a mathematical program semantic.

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).