Editing Denotational semantics (section)

===Meanings of recursive programs===
Denotational semantics is ascribed to a program phrase as a function from an environment (holding current values of its free variables) to its denotation. For example, the phrase {{code|n*m}} produces a denotation when provided with an environment that has binding for its two free variables: {{code|n}} and {{code|m}}.  If in the environment {{code|n}} has the value 3 and {{code|m}} has the value 5, then the denotation is 15.<ref name="Research Group Technical Monograph 1971"/>

A function can be represented as a set of [[ordered pair]]s of argument and corresponding result values. For example, the set {(0,1), (4,3)} denotes a function with result 1 for argument 0, result 3 for the argument 4, and undefined otherwise.

Consider for example the [[factorial]] function, which might be defined recursively as:
<syntaxhighlight lang="c">int factorial(int n) { if (n == 0) then return 1; else return n * factorial(n-1); }</syntaxhighlight>

To provide a meaning for this recursive definition, the denotation is built up as the limit of approximations, where each approximation limits the number of calls to factorial. At the beginning, we start with no calls - hence nothing is defined. In the next approximation, we can add the ordered pair (0,1), because this doesn't require calling factorial again. Similarly we can add (1,1), (2,2), etc., adding one pair each successive approximation because computing ''factorial(n)'' requires ''n+1'' calls. In the limit we get a [[total function]] from <math>\mathbb{N}</math> to <math>\mathbb{N}</math> defined everywhere in its domain.

Formally we model each approximation as a [[partial function]]  <math>\N \rightharpoonup \N</math>. Our approximation is then repeatedly applying a function implementing "make a more defined partial factorial function", i.e. <math>F : (\N \rightharpoonup \N) \to (\N \rightharpoonup \N) </math>, starting with the [[empty function]] (empty set). ''F'' could be defined in code as follows (using <code>Map<int,int></code> for  <math>\N \rightharpoonup \N</math>):
<syntaxhighlight lang="cpp">
int factorial_nonrecursive(Map<int,int> factorial_less_defined, int n)
{
  if (n == 0) then return 1;
  else if (fprev = lookup(factorial_less_defined, n-1)) then
    return n * fprev;
  else
    return NOT_DEFINED;
}

Map<int,int> F(Map<int,int> factorial_less_defined)
{ 
  Map<int,int> new_factorial = Map.empty();
  for (int n in all<int>()) {
    if (f = factorial_nonrecursive(factorial_less_defined, n) != NOT_DEFINED)
      new_factorial.put(n, f);
  }
  return new_factorial;
}
</syntaxhighlight>

Then we can introduce the notation ''F<sup>n</sup>'' to indicate [[iterated function|''F'' applied ''n'' times]].
* ''F''<sup>0</sup>({}) is the totally undefined partial function, represented as the set {};
* ''F''<sup>1</sup>({}) is the partial function represented as the set {(0,1)}: it is defined at 0, to be 1, and undefined elsewhere;
* ''F''<sup>5</sup>({}) is the partial function represented as the set {(0,1), (1,1), (2,2), (3,6), (4,24)}: it is defined for arguments 0,1,2,3,4.

This iterative process builds a sequence of partial functions from <math>\mathbb{N}</math> to <math>\mathbb{N}</math>. Partial functions form a [[chain-complete partial order]] using ⊆ as the ordering. Furthermore, this iterative process of better approximations of the factorial function forms an expansive (also called progressive) mapping because each <math>F^i\le F^{i+1}</math> using ⊆ as the ordering. So by a [[fixed-point theorem]] (specifically [[Bourbaki–Witt theorem]]), there exists a fixed point for this iterative process.

In this case, the fixed point is the least upper bound of this chain, which is the full {{code|factorial}} function, which can be expressed as the [[Union (set theory)|union]]
:<math>\bigcup_{i \in \mathbb N} F^i(\{\}). </math>

The fixed point we found is the [[least fixed point]] of ''F'', because our iteration started with the smallest element in the domain (the empty set). To prove this we need a more complex fixed point theorem such as the [[Knaster–Tarski theorem]].