Recursion [dt-000L]
So far, our semantic domains have just been (functions of) sets. While these have the advantage of being mathematically simple and intuitive, two language features make these sets insufficient for our purposes:
- Recursively defined programs, for dealing with recursion and loops, and
- Recursively defined semantic domains, for dealing with higher-order programs.
Recursively defined programs [dt-0006]
Suppose we extended the \mathcal {C} language with a while loop construct: \mathcal {C}\; \Coloneqq \; \cdots \mid \mathsf {while}\ \mathcal {B}\ \mathsf {do}\ \mathcal {C}\ \mathsf {od} The intuitive way to assign a semantics would be to use a recursive function: \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma \; = \; \begin {cases} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} However, such an equation is not a good definition. If we consider the trivial infinite loop program L \triangleq \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od}, and compute its semantics, we end up with: \llbracket \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma \; = \; \llbracket \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma This equation is satisfied by any function \Sigma \rightarrow \Sigma , so it doesn't tell us which function corresponds to the program L.
More generally, allowing our functions to be (generally) recursive causes these issues. The loop program L gives rise to the recursive equation \ell (x) = \ell (x), which has an infinite number of solutions.
If we add recursion to our programming language, we could have programs that give rise to more complex recursive equations like f(x) = f(x) + 1. By contrast to \ell (x), f(x) has no solutions (assuming f(x) operates on integers).
Upshot.
We need an explicit notion of "non-termination" on the semantics level, to properly deal with general recursion (or iteration).
Recursively defined semantic domains [dt-0007]
Suppose we extend our notion of expressions in the \mathcal {C} language with parameterless higher-order procedures: \begin {array}{l} \mathcal {E}\; \Coloneqq \; \cdots \mid \mathsf {proc}\ \mathcal {C}\\ \mathcal {C}\; \Coloneqq \; \cdots \mid x \end {array}
ExampleUsing higher-order procedures
We can store procedures in variables, so the program: \mathit {inc} := (\mathsf {proc}\ a := a + 1); \mathit {inc}; \mathit {inc} has the same effects on the variable a as the program: a := a + 1; a := a + 1
For our denotational semantics, our domains now take this form (\textcolor {blue}{\text {blue}} parts are new vs. Example [dt-0004]), where \uplus denotes disjoint union:
\begin {array}{lcl}
\mathbf {E} & \triangleq & \Sigma \rightarrow \mathbb {Z}\textcolor {blue}{\ \uplus \ \mathbf {C}}\\
\mathbf {B} & \triangleq & \Sigma \rightarrow \mathbb {B} \\
\mathbf {C} & \triangleq & \Sigma \rightarrow \Sigma \\[0.2em]
\Sigma & \triangleq & \mathcal {V} \rightarrow \mathbb {Z}\textcolor {blue}{\ \uplus \ \mathbf {C}}
\end {array}
Give a semantics to the \mathsf {proc} construct:
Exercise [dt-000P]
Solution.
ExampleA simpler equation with no solution
Consider the recursive equation X = X \rightarrow \mathbb {B}. Cantor's theorem says that there is no set X such that X \simeq \mathcal {P}(X) (where \mathcal {P}(X) is the power set of X), and seeing as \mathcal {P}(X) \simeq (X \rightarrow \mathbb {B}) it follows that X = X \rightarrow \mathbb {B} has no solution.
Any kind of higher-order construct leads to such recursive domain equations.
Upshot.
There are no (nontrivial) set-theoretic solutions to the recursive domain equations that arise from higher-order language constructs.
We will return to this problem later on! For now, let's focus on representing non-termination.