15
$\begingroup$

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?

$\endgroup$
1

1 Answer 1

14
$\begingroup$

One way to represent this kind of (computable) recursive function mathematically comes from domain theory.

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).
$\endgroup$
7
  • $\begingroup$ "which I've written in kind of a strange Unicode way, since we don't have LaTeX support here" -- Even if/when we get it, it won't include Tikz. Either way, nice answer! $\endgroup$
    – Bbrk24
    Jul 3, 2023 at 19:58
  • 2
    $\begingroup$ 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. $\endgroup$ Jul 5, 2023 at 10:03
  • 1
    $\begingroup$ @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. In that case, continuous functions are computable by definition (Sec 3.1). I'll remove that part of my answer. $\endgroup$ Jul 5, 2023 at 13:24
  • $\begingroup$ 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. $\endgroup$ Aug 15, 2023 at 21:46
  • 1
    $\begingroup$ @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. $\endgroup$ Aug 16, 2023 at 7:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .