Editing Least fixed point (section)

===Denotational semantics===
{{main|Denotational semantics#Meanings of recursive programs}}
[[File:ScottDomain svg.svg|thumb|Partial order on <math>\mathbb{Z}_\bot</math>]]
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, <math>\bot</math>, is introduced, denoting the exceptional value "undefined".
Given e.g. the program datatype <code>int</code>, its mathematical counterpart is defined as <math>\mathbb{Z}_\bot = \mathbb{Z} \cup \{ \bot \} ;</math>
it is made a partially ordered set by defining <math>\bot \sqsubset n</math> for each <math>n \in \mathbb{Z}</math> and letting any two different members <math>n,m \in \mathbb{Z}</math> be uncomparable w.r.t. <math>\sqsubset</math>, see picture. 

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

Given some program text <code>f</code>, its mathematical counterpart is obtained as least fixed point of some mapping from functions to functions that can be obtained by "translating" <code>f</code>.
For example, the [[C (programming language)|C]] definition 
<syntaxhighlight lang=c>int fact(int n) { if (n == 0) return 1; else return n * fact(n-1); }</syntaxhighlight><!---keep on a single line, to emphasize analogy to F--->
is translated to a mapping 
:<math>F: (\mathbb{Z}_\bot \to \mathbb{Z}_\bot) \to (\mathbb{Z}_\bot \to \mathbb{Z}_\bot) ,</math> defined as <math>(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}</math> 
The mapping <math>F</math> is defined in a non-recursive way, although <code>fact</code> was defined recursively.
Under certain restrictions (see [[Kleene fixed-point theorem]]), which are met in the example, <math>F</math> necessarily has a least fixed point, <math>\operatorname{fact}</math>, that is <math>(F(\operatorname{fact}))(n) = \operatorname{fact}(n)</math> for all <math>n \in \mathbb{Z}_\bot</math>.<ref>{{cite book |url= |author1=C.A. Gunter |author2=D.S. Scott |contribution=Semantic Domains |pages=633&ndash;674 |isbn=0-444-88074-7 |editor=Jan van Leeuwen |title=Formal Models and Semantics |publisher=Elsevier |series=Handbook of Theoretical Computer Science |volume=B |year=1990}} Here: pp.&nbsp;636–638</ref> 
It is possible to show that 
:<math>\operatorname{fact}(n) = \begin{cases} n! & \text{if } n \geq 0, \\ \bot & \text{if } n < 0 \text{ or } n = \bot. \end{cases}</math> 

A larger fixed point of <math>F</math> is e.g. the function <math>\operatorname{fact}_0 ,</math> defined by 
:<math>\operatorname{fact}_0(n) = \begin{cases} n! & \text{if } n \geq 0, \\ 0 & \text{if } n < 0, \\ \bot & \text{if } n = \bot, \end{cases}</math> 
however, this function does not correctly reflect the behavior of the above program text for negative <math>n ;</math> e.g. the call <code>fact(-1)</code> will not terminate at all, let alone return <code>0</code>.
Only the ''least'' fixed point, <math>\operatorname{fact} ,</math> can reasonably be used as a mathematical program semantic.