<h2>Motivation</h2>
<p>I want to define a denotational semantics (see <a href="https://cstheory.stackexchange.com/questions/3577/what-constitutes-denotational-semantics">here</a> or <a href="https://langdev.stackexchange.com/q/2019/89">here</a>) for recursive functions in my language, by representing them as mathematical functions.</p>
<h2>Background</h2>
<p>Consider a simple language that has only natural numbers, basic arithmetic, functions and <code>if</code> expressions. No side effects, to keep things simpler. (This language is similar to <a href="https://en.wikipedia.org/wiki/Programming_Computable_Functions" rel="nofollow noreferrer">PCF</a>.)</p>
<p>Our language has the following grammar:</p>
<pre><code>n ::= 0 | 1 | 2 | ...

v ::= [any identifier]

e ::= n | v | e + e | e - e | e * e | e(e) | e == e | if e then e else e

D ::= v(v) := e
</code></pre>
<p>As an example, the factorial function can be defined like this:</p>
<pre><code>f(x) :=
  if x == 0
    then 1
    else x * f(x - 1)
</code></pre>
<p>For this particular function, the mathematical meaning is fairly clear. However, let's look at how we derive its meaning in a bit more detail. In traditional mathematical notation it can be written as a <a href="https://en.wikipedia.org/wiki/Recurrence_relation" rel="nofollow noreferrer">recurrence relation</a> like this:</p>
<p><span class="math-container">$$
F(x) = \left\{ \begin{array}{ll}
1 &amp; \mathrm{if}\ x = 0 \\
x \cdot F(x - 1) &amp; \mathrm{otherwise}
\end{array}
\right.
$$</span></p>
<p>This functional equation can be solved in a <em>relatively</em> straightforward way, to find the function <span class="math-container">$F$</span>. But this approach has problems when the stopping condition of the recursive function is less obvious, or when the recursion is unbounded.</p>
<p>It is not always straightforward to solve functional equations like this one. Consider a function that loops infinitely if its argument is a counterexample to the (currently unsolved) Collatz conjecture, or otherwise returns zero. This function can be written in our language, but we currently don't have the mathematical tools to know whether that function is identical to <span class="math-container">$F(x) = 0$</span>. The functional equation is not solvable with current mathematical knowledge.</p>
<p>Also, what about infinite loops? Consider a function <code>g</code> defined by</p>
<pre><code>g(x) := g(x)
</code></pre>
<p>The functional equation for this is tautological; every mathematical function <span class="math-container">$: \mathbb{N} \to \mathbb{N}$</span> satisfies it. However, no such mathematical function accurately describes what this function does in our language, i.e. that it loops infinitely on all inputs.</p>
<h2>The question</h2>
<p>How can we give a denotational semantics for arbitrary recursive functions written in a programming language? How can we represent functions in our language as mathematical functions, when the functional equation might be unsolvable or have multiple solutions?</p>

<functions><semantics><recursion><denotational-semantics>
How can we define a denotational semantics for recursive functions?
CC BY-SA 4.0
2023-07-12T16:11:29.423Z
**Comments have been [moved to chat](https://chat.stackexchange.com/rooms/147187/discussion-on-question-by-david-young-how-can-we-define-a-denotational-semantics); please do not continue the discussion here.** Before posting a comment below this one, please review the [purposes of comments](/help/privileges/comment). Comments that do not request clarification or suggest improvements usually belong as an [answer](/help/how-to-answer), on [meta], or in [chat]. Comments continuing discussion may be removed.
V2Blast
<p>One way to represent this kind of (computable) recursive function mathematically comes from <em>domain theory</em>. I will end up describing something called a <em>Scott domain</em> in this answer, named after Dana Scott.</p>
<p>The <strong>key idea</strong> is to define an <em>ordering</em> for the gadgets in our language (natural numbers and functions) in terms of how much information content they have. We can then use this ordering to define what a recursive function means. In particular, we will use a certain kind of <em>least upper bound</em> (aka supremum) with respect to the ordering. We will also restrict what kind of set we're allowed to take the least upper bound of (this special kind of set is called a <em>chain</em>).</p>
<h1>Representing nontermination</h1>
<blockquote>
<p>Also, what about infinite loops? It isn't immediately obvious what nontermination should mean mathematically [...]</p>
</blockquote>
<p>I'll actually start by addressing this point. This is the crucial part. Once this is resolved, the other things fall into place.</p>
<p>The language described in the question just uses natural numbers as its data type (and functions on natural numbers). We might consider thinking about this data type as the set of natural numbers <span class="math-container">$\mathbb{N}$</span>.</p>
<p>However, some computations might not terminate. If we have some expression <code>3 * someFn(7)</code>, it might turn out that <code>someFn(7)</code> does not terminate and, therefore, that entire expression does not terminate.</p>
<p>So, let's extend the set of naturals with an extra element to represent nontermination which we will write ⊥ (pronounced &quot;bottom&quot;). Let's call this new set <span class="math-container">$\mathbb{N}_\bot = \mathbb{N} \cup \{\bot\}$</span>.</p>
<h1>Ordering by information content</h1>
<p>Now, here is a key step. We can give this new set <em>an ordering</em>. This ordering will be all about <em>information content</em>. Intuitively, given two elements <span class="math-container">$x, y \in \mathbb{N}_\bot$</span>, <span class="math-container">$x$</span> is &quot;less than or equal to&quot; <span class="math-container">$y$</span> if <span class="math-container">$x$</span> has &quot;at most as much information as&quot; <span class="math-container">$y$</span>. You can also think of it as &quot;<span class="math-container">$x$</span> <em>approximates</em> <span class="math-container">$y$</span>.&quot; We will write this <span class="math-container">$x \sqsubseteq y$</span>.</p>
<p><span class="math-container">$\bot$</span>, representing nontermination, gives you the <em>least</em> amount of information.</p>
<p>Our new ordering <span class="math-container">$\sqsubseteq$</span> on <span class="math-container">$\mathbb{N}_\bot$</span> will be far simpler than the usual <span class="math-container">$\le$</span> ordering on numbers.</p>
<p>It will be defined in two parts. For any element <span class="math-container">$x \in \mathbb{N}_\bot$</span>, we have:</p>
<ul>
<li><span class="math-container">$\bot \sqsubseteq x$</span></li>
<li><span class="math-container">$x \sqsubseteq x$</span></li>
</ul>
<p>So, <span class="math-container">$x$</span> &quot;approximates&quot; <span class="math-container">$y$</span> if either <span class="math-container">$x = \bot$</span> or <span class="math-container">$x = y$</span>. In particular, notice that even though <span class="math-container">$3 \le 4$</span>, it is <em>not</em> the case that <span class="math-container">$3 \sqsubseteq 4$</span> and also not the case that <span class="math-container">$4 \sqsubseteq 3$</span>. They have <em>incompatible</em> information, so they are not comparable under the <span class="math-container">$\sqsubseteq$</span> ordering.</p>
<p>We can draw a diagram to describe this:</p>
<p><span class="math-container">$$
\begin{matrix}
  0 &amp; &amp; 1 &amp;  &amp; 2 &amp; \cdots \\
  &amp;\huge\diagdown &amp; \huge| &amp; \huge\diagup \\
  &amp;&amp; \bot
\end{matrix}
$$</span></p>
<p>(Imagine there are similar connections for all other natural numbers.)</p>
<p>If <span class="math-container">$x$</span> is connected to <span class="math-container">$y$</span> and <span class="math-container">$x$</span> is drawn lower in the diagram, this means that <span class="math-container">$x$</span> is &quot;less than&quot; <span class="math-container">$y$</span>. This kind of diagram is called a <a href="https://en.wikipedia.org/wiki/Hasse_diagram" rel="nofollow noreferrer"><em>Hasse diagram</em></a>.</p>
<h1>Ordering <em>functions</em> by information content</h1>
<p>Given this, we can already start to talk about functions with nontermination. Generally, we can think of functions in our language as being elements of the set of mathematical functions <span class="math-container">$\mathbb{N}_\bot \to \mathbb{N}_\bot$</span>.</p>
<p>(<em>A brief aside: If the programming language has a call-by-value evaluation order, then we <strong>only</strong> consider <strong>strict</strong> functions from that set. A function <span class="math-container">$f$</span> is called &quot;strict&quot; if it satisfies the equation <span class="math-container">$f(\bot) = \bot$</span>.</em>)</p>
<p>We can create an ordering for the set <span class="math-container">$\mathbb{N}_\bot \to \mathbb{N}_\bot$</span> by using the <span class="math-container">$\mathbb{N}_\bot$</span> ordering <em>pointwise</em>. In particular, given two functions <span class="math-container">$f, g : \mathbb{N}_\bot \to \mathbb{N}_\bot$</span>:</p>
<ul>
<li><span class="math-container">$f \sqsubseteq g$</span> if for every x in <span class="math-container">$\mathbb{N}_\bot$</span> we have <span class="math-container">$f(x) \sqsubseteq g(x)$</span></li>
</ul>
<p>So if <span class="math-container">$s$</span> is a function that just immediately returns 0 for every input and <span class="math-container">$t$</span> is a function that goes into an infinite loop when its input is 5 but otherwise immediately returns 0, then we have <span class="math-container">$t \sqsubseteq s$</span>.</p>
<p>Our original ordering was a bit boring, mostly coinciding with equality, but this one starts to get a bit more interesting. We can also continue this process for higher-order functions, though this is outside the scope of this answer. If you do continue this process, you end up with a fairly intricate structure.</p>
<h1>Comparable things</h1>
<p>How does this actually help us with the original question? Well, this leads us directly to the concepts we need to represent recursion. There are two related concepts we need and then we can talk about recursion.</p>
<p>The first concept lets us restrict ourselves to only <em>comparable</em> collections.</p>
<p>Now that we have these orders, we can talk &quot;chains.&quot; What is a chain? A <a href="https://en.wikipedia.org/wiki/Total_order#Chains" rel="nofollow noreferrer">chain</a> is any subset <span class="math-container">$A$</span> of some ordered set (like a subset of <span class="math-container">$\mathbb{N}_\bot$</span> or a subset of <span class="math-container">$\mathbb{N}_\bot \to \mathbb{N}_\bot$</span>) where every pair of elements <span class="math-container">$x, y \in A$</span> are comparable. That is, for every <span class="math-container">$x$</span> and <span class="math-container">$y$</span> in <span class="math-container">$A$</span>, it is either the case that <span class="math-container">$x \sqsubseteq y$</span> or that <span class="math-container">$y \sqsubseteq x$</span>.</p>
<p>In the case of <span class="math-container">$\mathbb{N}_\bot$</span>, the chains are pretty simple. The empty set is a chain (vacuously). <span class="math-container">$\{\bot\}$</span> is a chain and <span class="math-container">$\{\bot, 7\}$</span> is a chain. On the other hand, <span class="math-container">$\{\bot, 7, 8\}$</span> is <em>not</em> a chain since 7 and 8 are not comparable under the ordering <span class="math-container">$\sqsubseteq$</span>.</p>
<p>The chains for <span class="math-container">$\mathbb{N}_\bot \to \mathbb{N}_\bot$</span> are more interesting. Many functions are uncomparable, just as in the <span class="math-container">$\mathbb{N}_\bot$</span> case, however there are <em>also</em> many functions that <em>are</em> comparable.</p>
<p>Those chains of functions will be very useful for us. We will look at such a chain right now. Also, this leads into the second concept we need: the <em>least upper bound</em> of a chain.</p>
<h1>Recursion</h1>
<p>Let's return to our factorial function. If we look at some input-output pairs, we know that we will find:</p>
<p><span class="math-container">$$
\begin{array} {c|cccccc}
x &amp; \bot &amp; 0 &amp; 1 &amp; 2 &amp; 3 &amp; \cdots \\ \hline
f(x) &amp; \bot &amp; 1 &amp; 1 &amp; 2 &amp; 6 &amp; \cdots
\end{array}
$$</span></p>
<p>(<em>An aside: The set of all input-output pairs of a function is called &quot;the graph&quot; of the function</em>)</p>
<p>But what if we consider a function <span class="math-container">$g_0$</span> that gives the factorial only for 0 and then, for larger numbers, goes into an infinite loop? Specifically:</p>
<p><span class="math-container">$$
\begin{array} {c|cccccc}
x &amp; \bot &amp; 0 &amp; 1 &amp; 2 &amp; 3 &amp; \cdots \\ \hline
g_0(x) &amp; \bot &amp; 1 &amp; \bot &amp; \bot &amp; \bot &amp; \cdots
\end{array}
$$</span></p>
<p>We can also consider a function <span class="math-container">$g_1$</span> that gives the factorial for 0 and 1, but then goes into an infinite loop for larger numbers:</p>
<p><span class="math-container">\begin{array} {c|cccccc}
x &amp; \bot &amp; 0 &amp; 1 &amp; 2 &amp; 3 &amp; \cdots \\ \hline
g_1(x) &amp; \bot &amp; 1 &amp; 1 &amp; \bot &amp; \bot &amp; \cdots
\end{array}</span></p>
<p>We can continue this pattern for any natural number <span class="math-container">$n$</span> to get <span class="math-container">$g_n$</span> that gives the &quot;correct&quot; answer for every <span class="math-container">$x \le n$</span> and goes into an infinite loop for <span class="math-container">$x \gt n$</span>.</p>
<p>These <span class="math-container">$g$</span>'s form a chain, in fact an <em>infinite</em> chain: <span class="math-container">$g_0 \sqsubseteq g_1 \sqsubseteq g_2 \sqsubseteq g_3 \sqsubseteq \cdots$</span></p>
<p>Call the set of these functions <span class="math-container">$G = \{g_0, g_1, g_2, \ldots\}$</span>.</p>
<p>We also see that, for any natural number <span class="math-container">$n$</span>, we have <span class="math-container">$g_n \sqsubseteq f$</span> (where <span class="math-container">$f$</span> is our factorial function). To put it another way, <span class="math-container">$f$</span> is an <em>upper bound</em> of the set <span class="math-container">$G$</span>.</p>
<p>It just so happens that <span class="math-container">$f$</span> is the <em>unique</em> upper bound of <span class="math-container">$G$</span> but in general there could be many upper bounds. I will return to this shortly. For now, it suffices to say we always want the <a href="https://en.wikipedia.org/wiki/Infimum_and_supremum" rel="nofollow noreferrer"><em>least</em> upper bound</a>.</p>
<p>The <em>least upper bound</em> of a set <span class="math-container">$A$</span> with respect to the order <span class="math-container">$\sqsubseteq$</span> is written <span class="math-container">$\sqcup\,A$</span>. If <span class="math-container">$A$</span> is a chain, then <span class="math-container">$\sqcup\,A$</span> must exist in our ordering. (<em>An aside: This is because our ordering is <a href="https://en.wikipedia.org/wiki/Chain-complete_partial_order" rel="nofollow noreferrer"><strong>chain-complete</strong></a>, but it is not necessary to understand the details of that here.</em>)</p>
<p>We say that <span class="math-container">$z$</span> is a &quot;least upper bound&quot; of the chain <span class="math-container">$A$</span> if the following two conditions hold:</p>
<ul>
<li><span class="math-container">$z$</span> is an upper bound of <span class="math-container">$A$</span></li>
<li>If <span class="math-container">$x$</span> is any upper bound of <span class="math-container">$A$</span>, then <span class="math-container">$z \sqsubseteq x$</span></li>
</ul>
<p><span class="math-container">$G$</span> is a chain. So, <span class="math-container">$\sqcup$</span> exists and we can say that <span class="math-container">$f = \sqcup \,G$</span>.</p>
<p>Though it might look different, this has similarities to finding a limit in calculus. In fact, you can reframe the calculus concept of a limit in terms of <em>directed sets</em> (which are a generalization of chains)! <sup>[1]</sup> This is outside the scope of this answer, however.</p>
<h1>Finding a chain</h1>
<p>How <em>exactly</em> did we end up with the chain of functions G? Here is an alternate presentation. Consider the function:</p>
<p><span class="math-container">$$
h(k)(x) = \left\{ \begin{array}{ll}
1 &amp; \mathrm{if}\ x = 0 \\
x \cdot k(x - 1) &amp; \mathrm{otherwise}
\end{array}
\right.
$$</span></p>
<p>This is obtained from our original function by adding a new argument <span class="math-container">$k$</span> and replacing recursive calls with calls to <span class="math-container">$k$</span>.</p>
<p>Now we can see that <span class="math-container">$g_0 = h(\bot)$</span>. In fact, we can use <span class="math-container">$h$</span> and <span class="math-container">$\bot$</span> for all of the <span class="math-container">$g$</span>'s:</p>
<ul>
<li><span class="math-container">$g_0 = h(\bot)$</span></li>
<li><span class="math-container">$g_1 = h(h(\bot))$</span></li>
<li><span class="math-container">$g_2 = h(h(h(\bot)))$</span></li>
<li>...</li>
</ul>
<p>So, for each <span class="math-container">$g_i$</span> we have <span class="math-container">$g_i = h(h(\ldots(h(⊥))\ldots))$</span> where there are exactly <span class="math-container">$i+1$</span> applications of <span class="math-container">$h$</span>. We can also write this as <span class="math-container">$g_i = h^{i+1}(\bot)$</span>. What does this give us?</p>
<p>We can now write <span class="math-container">$G$</span> as <span class="math-container">$G = \{h^n(\bot) : n \in \mathbb{N}\}$</span>.</p>
<p>We might now write</p>
<ul>
<li><span class="math-container">$f = \sqcup\,\{h^n(\bot) : n \in \mathbb{N}\}$</span></li>
</ul>
<p>or alternatively</p>
<ul>
<li><span class="math-container">$f = \sqcup_{n \in \mathbb{N}}\,h^n(\bot)$</span></li>
</ul>
<p>Previously, I had just verbally described the chain <span class="math-container">$G$</span>. Now we have given specific mathematical definitions for everything involved.</p>
<h1>Least fixed points: the meaning of recursive functions</h1>
<p>We can in fact see that <span class="math-container">$f$</span> is the <a href="https://en.wikipedia.org/wiki/Fixed-point_combinator" rel="nofollow noreferrer"><em>least fixed point</em></a> of <span class="math-container">$h$</span>.</p>
<p>First, what is a fixed point?</p>
<ul>
<li><span class="math-container">$a$</span> is called a &quot;fixed point&quot; of <span class="math-container">$f$</span> if <span class="math-container">$f(a) = a$</span></li>
<li><span class="math-container">$z$</span> is a <em>least</em> fixed point of <span class="math-container">$f$</span> if it is a fixed point of <span class="math-container">$f$</span> and, for any other fixed point <span class="math-container">$b$</span> of <span class="math-container">$f$</span>, we have <span class="math-container">$z \sqsubseteq b$</span>.</li>
</ul>
<p>So, firstly, we can see that <span class="math-container">$h(f) = f$</span>. Therefore <span class="math-container">$f$</span> is a fixed point of <span class="math-container">$h$</span>. We are just plugging in <span class="math-container">$f$</span> for the where the original recursive call went. This recovers the original function.</p>
<p>Furthermore, <span class="math-container">$f$</span> is the <em>least</em> fixed point of <span class="math-container">$h$</span>. This is more important in the case of a function which does not terminate for some of its inputs. In that case, we would need to be careful to choose the <em>least</em> fixed point to make sure that we end up with <span class="math-container">$\bot$</span> when <span class="math-container">$f$</span> does not terminate.</p>
<p><em>This</em> is what characterizes a recursive function! You take the recursive function defined in your programming language and create a new, <em>non-recursive</em> function like this (we called this new function <span class="math-container">$h$</span>):</p>
<ul>
<li>Include an additional argument (we called this argument <span class="math-container">$k$</span> when we made <span class="math-container">$h$</span>)</li>
<li>Replace all recursive calls with applications of that argument (we replaced the <span class="math-container">$f(x-1)$</span> call with <span class="math-container">$k(x-1)$</span> when we defined <span class="math-container">$h$</span>).</li>
</ul>
<p>Then the denotation of your original function is the least fixed point of this new, non-recursive function. The least fixed point of such a function <a href="https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem" rel="nofollow noreferrer">always exists</a> and <a href="https://proofwiki.org/wiki/Supremum_is_Unique" rel="nofollow noreferrer">it's always unique</a>!</p>
<h1>Tying up a loose end: multiple upper bounds</h1>
<p>In our example, we only had one upper bound. But I also said that, in general, there could be multiple upper bounds. Furthermore, we always want the <em>least</em> upper bound.</p>
<p>What is an example of a chain of functions that has multiple upper bounds? Well, say we only have the first four <span class="math-container">$g$</span>'s: <span class="math-container">$P = \{g_0, g_1, g_2, g_3\}$</span>. This has many upper bounds. In fact, not only is <span class="math-container">$f$</span> an upper bound, but so is every <span class="math-container">$g_i$</span> where <span class="math-container">$i \ge 3$</span>. It has other upper bounds beyond those, as well.</p>
<p>Where might such a chain arise? Let's say we <em>started</em> with a function that gave the factorial for only inputs less than or equal to 3 and otherwise went into an infinite loop. In a shorthand syntax for the language, we might write:</p>
<pre><code>p(0) := 1
p(1) := 1
p(2) := 2
p(3) := 6
p(x) := p(x) if x &gt; 3
</code></pre>
<p>In this case, <span class="math-container">$p$</span> is an upper bound of <span class="math-container">$P$</span>. But, as I said, there are <em>many</em> upper bounds for <span class="math-container">$P$</span>! In fact, <span class="math-container">$p$</span> turns out to be the unique <em>least</em> upper bound of <span class="math-container">$P$</span>, since it gives <em>at most</em> as much information as the other upper bounds. Never <em>more</em> information than the other upper bounds of <span class="math-container">$P$</span>.</p>
<p>If we do that same trick from above and write</p>
<p><span class="math-container">$$
u(k)(x) = \left\{ \begin{array}{ll}
f(x) &amp; \mathrm{if}\ x \le 3 \\
k(x) &amp; \mathrm{otherwise}
\end{array}
\right.
$$</span></p>
<p>then we can see that the least fixed point of <span class="math-container">$u$</span> is <span class="math-container">$p$</span>. However, <span class="math-container">$u$</span> has more fixed points.</p>
<p>Another fixed point of <span class="math-container">$u$</span> is the function which gives <span class="math-container">$f(x)$</span> whenever <span class="math-container">$x \le 3$</span> but is then always gives 7 whenever <span class="math-container">$x \gt 3$</span>. But this is not the <em>least</em> fixed point, since that function has more information than <span class="math-container">$p$</span>. There is only one <em>least</em> fixed point of <span class="math-container">$u$</span> and that is <span class="math-container">$p$</span>.</p>
<p><sup>[1] See <em>Limits: A New Approach to Real Analysis</em> by Alan F. Beardon</sup></p>
<h1>Further reading</h1>
<p>Papers:</p>
<ul>
<li><em>Domains for Denotational Semantics</em> by Dana Scott</li>
<li><em>A type-theoretical alternative to ISWIM, CUCH, OWHY</em> by Dana Scott</li>
<li><em>Toward a mathematical semantics for computer languages</em> by Dana Scott and Christopher Strachey</li>
</ul>
<p>Book chapters:</p>
<ul>
<li><em>Formal Semantics of Programming Languages</em> (chapters 5, 8, 9, 10, 12) by Glynn Winskel</li>
<li><em>Semantics of Programming Languages: Structures and Techniques</em> (chapter 4) by Carl A. Gunter</li>
<li><em>Domain-Theoretic Foundations of Functional Programming</em> by Thomas Streicher</li>
<li><em>Introduction to Lattices and Order</em> by Brian A. Davey and Hilary Priestley. This is an introduction to order theory more broadly. They also do talk about programming language semantics specifically (for example, in Ch. 9).</li>
</ul>

CC BY-SA 4.0
2023-07-03T19:36:14.537Z
2024-06-02T14:43:15.130Z
2024-06-02T14:43:15.130Z
David Young
CC BY-SA 4.0
2023-07-05T10:03:47.210Z
It's wrong to confuse continuous functions with computable ones: for example, consider the function in N_btm - - > N_btm that maps bottom to bottom and each number n to either 0 or 1 depending on whether the n'th Turing machine halts on a blank tape. That function is continuous because it is monotonic, but it isn't computable.
Mike Spivey
CC BY-SA 4.0
2023-07-05T13:24:44.587Z
@MikeSpivey Ah, you're right. I was thinking of the continuous functions from the synthetic topology from Martin Escardo's [Synthetic topology of data types and classical spaces](https://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf). In that case, continuous functions are computable by definition (Sec 3.1). I'll remove that part of my answer.
David Young
CC BY-SA 4.0
2023-08-22T05:40:44.520Z
@MartinBerger That's a good point. I'll see about including that when I get a bit more time. Also, thank you for the pointer to the survey article by Ong. It has been very interesting.
David Young
CC BY-SA 4.0
2023-08-15T21:46:18.543Z
Domain-theoretic like this is usually not precise, see the famous full-abstract problem for PCF. Luke Ong has written a survey article *Correspondence between operational and denotational semantics: the full abstraction problem for PCF*. The core issue is that (simple) domain-theoretic semantics don't rule out parallel evaluation, but PCF is a sequential language.
Martin Berger
CC BY-SA 4.0
2023-08-16T02:24:20.197Z
@MartinBerger I'm not fully sure I understand what you mean. Are you saying that I should include info about (the lack of) full abstraction in the answer, or is there something wrong? I sort of understand the full abstraction problem for PCF. I didn't intend to suggest that this semantics is fully abstract, only that it's adequate (though I didn't actually say "adequate", looking back). Thank you for the comment. I read some of your semantics answers recently and I've found them helpful.
David Young
CC BY-SA 4.0
2023-08-16T07:43:46.320Z
@DavidYoung Your answer is fine, but I think it would be even better if the shortcomings of order-theoretic methods were mentioned. Basically order theoretic models are illuminating only for simple forms of computation.
Martin Berger
# How can we define a denotational semantics for recursive functions?
Posted by: username_0 on 2023-07-03
Motivation
I want to define a denotational semantics (see here or here) for recursive functions in my language, by representing them as mathematical functions.
Background
Consider a simple language that has only natural numbers, basic arithmetic, functions and if expressions. No side effects, to keep things simpler. (This language is similar to PCF.)
Our language has the following grammar:
n ::= 0 | 1 | 2 | ...

v ::= [any identifier]

e ::= n | v | e + e | e - e | e * e | e(e) | e == e | if e then e else e

D ::= v(v) := e

As an example, the factorial function can be defined like this:
f(x) :=
  if x == 0
    then 1
    else x * f(x - 1)

For this particular function, the mathematical meaning is fairly clear. However, let's look at how we derive its meaning in a bit more detail. In traditional mathematical notation it can be written as a recurrence relation like this:
$$
F(x) = \left\{ \begin{array}{ll}
1 & \mathrm{if}\ x = 0 \\
x \cdot F(x - 1) & \mathrm{otherwise}
\end{array}
\right.
$$
This functional equation can be solved in a relatively straightforward way, to find the function $F$. But this approach has problems when the stopping condition of the recursive function is less obvious, or when the recursion is unbounded.
It is not always straightforward to solve functional equations like this one. Consider a function that loops infinitely if its argument is a counterexample to the (currently unsolved) Collatz conjecture, or otherwise returns zero. This function can be written in our language, but we currently don't have the mathematical tools to know whether that function is identical to $F(x) = 0$. The functional equation is not solvable with current mathematical knowledge.
Also, what about infinite loops? Consider a function g defined by
g(x) := g(x)

The functional equation for this is tautological; every mathematical function $: \mathbb{N} \to \mathbb{N}$ satisfies it. However, no such mathematical function accurately describes what this function does in our language, i.e. that it loops infinitely on all inputs.
The question
How can we give a denotational semantics for arbitrary recursive functions written in a programming language? How can we represent functions in our language as mathematical functions, when the functional equation might be unsolvable or have multiple solutions?
**Tags:** functions semantics recursion denotational-semantics
> **Comments:**
> **username_1**: **Comments have been [moved to chat](https://chat.stackexchange.com/rooms/147187/discussion-on-question-by-david-young-how-can-we-define-a-denotational-semantics); please do not continue the discussion here.** Before posting a comment below this one, please review the [purposes of comments](/help/privileges/comment). Comments that do not request clarification or suggest improvements usually belong as an [answer](/help/how-to-answer), on [meta], or in [chat]. Comments continuing discussion may be removed.  
---
## 1 answers
### Answer by username_0 on 2023-07-03. Score: 16 | Accepted answer
One way to represent this kind of (computable) recursive function mathematically comes from domain theory. I will end up describing something called a Scott domain in this answer, named after Dana Scott.
The key idea is to define an ordering for the gadgets in our language (natural numbers and functions) in terms of how much information content they have. We can then use this ordering to define what a recursive function means. In particular, we will use a certain kind of least upper bound (aka supremum) with respect to the ordering. We will also restrict what kind of set we're allowed to take the least upper bound of (this special kind of set is called a chain).
Representing nontermination

Also, what about infinite loops? It isn't immediately obvious what nontermination should mean mathematically [...]

I'll actually start by addressing this point. This is the crucial part. Once this is resolved, the other things fall into place.
The language described in the question just uses natural numbers as its data type (and functions on natural numbers). We might consider thinking about this data type as the set of natural numbers $\mathbb{N}$.
However, some computations might not terminate. If we have some expression 3 * someFn(7), it might turn out that someFn(7) does not terminate and, therefore, that entire expression does not terminate.
So, let's extend the set of naturals with an extra element to represent nontermination which we will write ⊥ (pronounced "bottom"). Let's call this new set $\mathbb{N}_\bot = \mathbb{N} \cup \{\bot\}$.
Ordering by information content
Now, here is a key step. We can give this new set an ordering. This ordering will be all about information content. Intuitively, given two elements $x, y \in \mathbb{N}_\bot$, $x$ is "less than or equal to" $y$ if $x$ has "at most as much information as" $y$. You can also think of it as "$x$ approximates $y$." We will write this $x \sqsubseteq y$.
$\bot$, representing nontermination, gives you the least amount of information.
Our new ordering $\sqsubseteq$ on $\mathbb{N}_\bot$ will be far simpler than the usual $\le$ ordering on numbers.
It will be defined in two parts. For any element $x \in \mathbb{N}_\bot$, we have:

$\bot \sqsubseteq x$
$x \sqsubseteq x$

So, $x$ "approximates" $y$ if either $x = \bot$ or $x = y$. In particular, notice that even though $3 \le 4$, it is not the case that $3 \sqsubseteq 4$ and also not the case that $4 \sqsubseteq 3$. They have incompatible information, so they are not comparable under the $\sqsubseteq$ ordering.
We can draw a diagram to describe this:
$$
\begin{matrix}
  0 & & 1 &  & 2 & \cdots \\
  &\huge\diagdown & \huge| & \huge\diagup \\
  && \bot
\end{matrix}
$$
(Imagine there are similar connections for all other natural numbers.)
If $x$ is connected to $y$ and $x$ is drawn lower in the diagram, this means that $x$ is "less than" $y$. This kind of diagram is called a Hasse diagram.
Ordering functions by information content
Given this, we can already start to talk about functions with nontermination. Generally, we can think of functions in our language as being elements of the set of mathematical functions $\mathbb{N}_\bot \to \mathbb{N}_\bot$.
(A brief aside: If the programming language has a call-by-value evaluation order, then we only consider strict functions from that set. A function $f$ is called "strict" if it satisfies the equation $f(\bot) = \bot$.)
We can create an ordering for the set $\mathbb{N}_\bot \to \mathbb{N}_\bot$ by using the $\mathbb{N}_\bot$ ordering pointwise. In particular, given two functions $f, g : \mathbb{N}_\bot \to \mathbb{N}_\bot$:

$f \sqsubseteq g$ if for every x in $\mathbb{N}_\bot$ we have $f(x) \sqsubseteq g(x)$

So if $s$ is a function that just immediately returns 0 for every input and $t$ is a function that goes into an infinite loop when its input is 5 but otherwise immediately returns 0, then we have $t \sqsubseteq s$.
Our original ordering was a bit boring, mostly coinciding with equality, but this one starts to get a bit more interesting. We can also continue this process for higher-order functions, though this is outside the scope of this answer. If you do continue this process, you end up with a fairly intricate structure.
Comparable things
How does this actually help us with the original question? Well, this leads us directly to the concepts we need to represent recursion. There are two related concepts we need and then we can talk about recursion.
The first concept lets us restrict ourselves to only comparable collections.
Now that we have these orders, we can talk "chains." What is a chain? A chain is any subset $A$ of some ordered set (like a subset of $\mathbb{N}_\bot$ or a subset of $\mathbb{N}_\bot \to \mathbb{N}_\bot$) where every pair of elements $x, y \in A$ are comparable. That is, for every $x$ and $y$ in $A$, it is either the case that $x \sqsubseteq y$ or that $y \sqsubseteq x$.
In the case of $\mathbb{N}_\bot$, the chains are pretty simple. The empty set is a chain (vacuously). $\{\bot\}$ is a chain and $\{\bot, 7\}$ is a chain. On the other hand, $\{\bot, 7, 8\}$ is not a chain since 7 and 8 are not comparable under the ordering $\sqsubseteq$.
The chains for $\mathbb{N}_\bot \to \mathbb{N}_\bot$ are more interesting. Many functions are uncomparable, just as in the $\mathbb{N}_\bot$ case, however there are also many functions that are comparable.
Those chains of functions will be very useful for us. We will look at such a chain right now. Also, this leads into the second concept we need: the least upper bound of a chain.
Recursion
Let's return to our factorial function. If we look at some input-output pairs, we know that we will find:
$$
\begin{array} {c|cccccc}
x & \bot & 0 & 1 & 2 & 3 & \cdots \\ \hline
f(x) & \bot & 1 & 1 & 2 & 6 & \cdots
\end{array}
$$
(An aside: The set of all input-output pairs of a function is called "the graph" of the function)
But what if we consider a function $g_0$ that gives the factorial only for 0 and then, for larger numbers, goes into an infinite loop? Specifically:
$$
\begin{array} {c|cccccc}
x & \bot & 0 & 1 & 2 & 3 & \cdots \\ \hline
g_0(x) & \bot & 1 & \bot & \bot & \bot & \cdots
\end{array}
$$
We can also consider a function $g_1$ that gives the factorial for 0 and 1, but then goes into an infinite loop for larger numbers:
\begin{array} {c|cccccc}
x & \bot & 0 & 1 & 2 & 3 & \cdots \\ \hline
g_1(x) & \bot & 1 & 1 & \bot & \bot & \cdots
\end{array}
We can continue this pattern for any natural number $n$ to get $g_n$ that gives the "correct" answer for every $x \le n$ and goes into an infinite loop for $x \gt n$.
These $g$'s form a chain, in fact an infinite chain: $g_0 \sqsubseteq g_1 \sqsubseteq g_2 \sqsubseteq g_3 \sqsubseteq \cdots$
Call the set of these functions $G = \{g_0, g_1, g_2, \ldots\}$.
We also see that, for any natural number $n$, we have $g_n \sqsubseteq f$ (where $f$ is our factorial function). To put it another way, $f$ is an upper bound of the set $G$.
It just so happens that $f$ is the unique upper bound of $G$ but in general there could be many upper bounds. I will return to this shortly. For now, it suffices to say we always want the least upper bound.
The least upper bound of a set $A$ with respect to the order $\sqsubseteq$ is written $\sqcup\,A$. If $A$ is a chain, then $\sqcup\,A$ must exist in our ordering. (An aside: This is because our ordering is chain-complete, but it is not necessary to understand the details of that here.)
We say that $z$ is a "least upper bound" of the chain $A$ if the following two conditions hold:

$z$ is an upper bound of $A$
If $x$ is any upper bound of $A$, then $z \sqsubseteq x$

$G$ is a chain. So, $\sqcup$ exists and we can say that $f = \sqcup \,G$.
Though it might look different, this has similarities to finding a limit in calculus. In fact, you can reframe the calculus concept of a limit in terms of directed sets (which are a generalization of chains)! [1] This is outside the scope of this answer, however.
Finding a chain
How exactly did we end up with the chain of functions G? Here is an alternate presentation. Consider the function:
$$
h(k)(x) = \left\{ \begin{array}{ll}
1 & \mathrm{if}\ x = 0 \\
x \cdot k(x - 1) & \mathrm{otherwise}
\end{array}
\right.
$$
This is obtained from our original function by adding a new argument $k$ and replacing recursive calls with calls to $k$.
Now we can see that $g_0 = h(\bot)$. In fact, we can use $h$ and $\bot$ for all of the $g$'s:

$g_0 = h(\bot)$
$g_1 = h(h(\bot))$
$g_2 = h(h(h(\bot)))$
...

So, for each $g_i$ we have $g_i = h(h(\ldots(h(⊥))\ldots))$ where there are exactly $i+1$ applications of $h$. We can also write this as $g_i = h^{i+1}(\bot)$. What does this give us?
We can now write $G$ as $G = \{h^n(\bot) : n \in \mathbb{N}\}$.
We might now write

$f = \sqcup\,\{h^n(\bot) : n \in \mathbb{N}\}$

or alternatively

$f = \sqcup_{n \in \mathbb{N}}\,h^n(\bot)$

Previously, I had just verbally described the chain $G$. Now we have given specific mathematical definitions for everything involved.
Least fixed points: the meaning of recursive functions
We can in fact see that $f$ is the least fixed point of $h$.
First, what is a fixed point?

$a$ is called a "fixed point" of $f$ if $f(a) = a$
$z$ is a least fixed point of $f$ if it is a fixed point of $f$ and, for any other fixed point $b$ of $f$, we have $z \sqsubseteq b$.

So, firstly, we can see that $h(f) = f$. Therefore $f$ is a fixed point of $h$. We are just plugging in $f$ for the where the original recursive call went. This recovers the original function.
Furthermore, $f$ is the least fixed point of $h$. This is more important in the case of a function which does not terminate for some of its inputs. In that case, we would need to be careful to choose the least fixed point to make sure that we end up with $\bot$ when $f$ does not terminate.
This is what characterizes a recursive function! You take the recursive function defined in your programming language and create a new, non-recursive function like this (we called this new function $h$):

Include an additional argument (we called this argument $k$ when we made $h$)
Replace all recursive calls with applications of that argument (we replaced the $f(x-1)$ call with $k(x-1)$ when we defined $h$).

Then the denotation of your original function is the least fixed point of this new, non-recursive function. The least fixed point of such a function always exists and it's always unique!
Tying up a loose end: multiple upper bounds
In our example, we only had one upper bound. But I also said that, in general, there could be multiple upper bounds. Furthermore, we always want the least upper bound.
What is an example of a chain of functions that has multiple upper bounds? Well, say we only have the first four $g$'s: $P = \{g_0, g_1, g_2, g_3\}$. This has many upper bounds. In fact, not only is $f$ an upper bound, but so is every $g_i$ where $i \ge 3$. It has other upper bounds beyond those, as well.
Where might such a chain arise? Let's say we started with a function that gave the factorial for only inputs less than or equal to 3 and otherwise went into an infinite loop. In a shorthand syntax for the language, we might write:
p(0) := 1
p(1) := 1
p(2) := 2
p(3) := 6
p(x) := p(x) if x > 3

In this case, $p$ is an upper bound of $P$. But, as I said, there are many upper bounds for $P$! In fact, $p$ turns out to be the unique least upper bound of $P$, since it gives at most as much information as the other upper bounds. Never more information than the other upper bounds of $P$.
If we do that same trick from above and write
$$
u(k)(x) = \left\{ \begin{array}{ll}
f(x) & \mathrm{if}\ x \le 3 \\
k(x) & \mathrm{otherwise}
\end{array}
\right.
$$
then we can see that the least fixed point of $u$ is $p$. However, $u$ has more fixed points.
Another fixed point of $u$ is the function which gives $f(x)$ whenever $x \le 3$ but is then always gives 7 whenever $x \gt 3$. But this is not the least fixed point, since that function has more information than $p$. There is only one least fixed point of $u$ and that is $p$.
[1] See Limits: A New Approach to Real Analysis by Alan F. Beardon
Further reading
Papers:

Domains for Denotational Semantics by Dana Scott
A type-theoretical alternative to ISWIM, CUCH, OWHY by Dana Scott
Toward a mathematical semantics for computer languages by Dana Scott and Christopher Strachey

Book chapters:

Formal Semantics of Programming Languages (chapters 5, 8, 9, 10, 12) by Glynn Winskel
Semantics of Programming Languages: Structures and Techniques (chapter 4) by Carl A. Gunter
Domain-Theoretic Foundations of Functional Programming by Thomas Streicher
Introduction to Lattices and Order by Brian A. Davey and Hilary Priestley. This is an introduction to order theory more broadly. They also do talk about programming language semantics specifically (for example, in Ch. 9).
> **Comments:**
> **username_2** (2023-07-05): It's wrong to confuse continuous functions with computable ones: for example, consider the function in N_btm - - > N_btm that maps bottom to bottom and each number n to either 0 or 1 depending on whether the n'th Turing machine halts on a blank tape. That function is continuous because it is monotonic, but it isn't computable.  
> **username_0** (2023-07-05): @MikeSpivey Ah, you're right. I was thinking of the continuous functions from the synthetic topology from Martin Escardo's [Synthetic topology of data types and classical spaces](https://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf). In that case, continuous functions are computable by definition (Sec 3.1). I'll remove that part of my answer.  
> **username_3** (2023-08-15): Domain-theoretic like this is usually not precise, see the famous full-abstract problem for PCF. Luke Ong has written a survey article *Correspondence between operational and denotational semantics: the full abstraction problem for PCF*. The core issue is that (simple) domain-theoretic semantics don't rule out parallel evaluation, but PCF is a sequential language.  
> **username_0** (2023-08-16): @MartinBerger I'm not fully sure I understand what you mean. Are you saying that I should include info about (the lack of) full abstraction in the answer, or is there something wrong? I sort of understand the full abstraction problem for PCF. I didn't intend to suggest that this semantics is fully abstract, only that it's adequate (though I didn't actually say "adequate", looking back). Thank you for the comment. I read some of your semantics answers recently and I've found them helpful.  
> **username_3** (2023-08-16): @DavidYoung Your answer is fine, but I think it would be even better if the shortcomings of order-theoretic methods were mentioned. Basically order theoretic models are illuminating only for simple forms of computation.  
> **username_0** (2023-08-22): @MartinBerger That's a good point. I'll see about including that when I get a bit more time. Also, thank you for the pointer to the survey article by Ong. It has been very interesting.  
---
