In this article, we will discuss how to represent iterations in PCF using recursions. Then we are going to compare the natural-number functions definable in PCF with the classes of total and partial recursive functions. We will use lambda calculus to prove that all recursive total and partial functions on the natural numbers are definable in PCF. If you want, you can also use Turing machines to construct a similar proof!
But first, let’s take a look at how to use PCF semantics to express records and $n$-tuples, the data types that will be very helpful to simplify our discussion about the properties of functions with multiple arguments.
Records and $n$-tuples
Records
Records are a useful data type in many languages. Record is also called “struct” in C language. We will see that record expressions may be translated into PCF using pairing and projection introduced in Easy Foundations for Programming Languages III — The Language PCF.
Borrow the “struct” syntax from C language may help us understand records. Following shows an example struct in C, which is a data strucure consisting of values of different types.
1
2
3
4
5
struct person { // Personal Information Structure
char *name;
int age;
bool married;
};
Essentially, like the struct, a record is an aggregate of one or more components, each with a different label. We can combine any expressions $M_1:\sigma_1,…,M_k:\sigma_k$ and form a record \(\{ l_1 = M_1, ..., l_k = M_k \}\) whose $l_i$ component has the value of $M_i$. The type of this record may be written \(\{ l_1:\sigma_1, ..., l_k:\sigma_k \}\).
We select the $l_i$ component of any record $r$ or this type $(0 \leq i \leq k)$ using the “dot” notation $r\centerdot l_i$.
For example, the record \(\{ A=3, B=true \}\) with components labeled $A$ and $B$ has type \(\{A:nat,B:bool\}\). The $A$ component is selected by writing \(\{ A=3, B=true \} \centerdot A\).
In general, we have the equational axiom
\[\{ l_1:\sigma_1, ..., l_k:\sigma_k \} \centerdot l_i = M_i \tag*{$(record \: selection)$}\]for component selection, which can also be used as a reduction rule from left to right.
One convenient aspect of records is that component order does not matter. We can access the $A$ component of a record $r$ without having to remember which component we listed first in defining $r$. In addition, we can choose mnemonic names for labels, as in
\[\text{let } person = \{ name:string, age:nat, married:bool \}\]However, if we want to translate records into pairs and product types of PCF, we must choose an order of components. For records with two components, we can translate directly by choosing one component to be first; while for records with more than two components, we must translate into “nested” pairs.
Translation Details
To simplify the translation of $n$-component records into PCF, we will define $\boldsymbol{n}$-tuples as syntactic sugar. For any sequence of types $\sigma_1,…,\sigma_n$, we introduce the $n$-ary product notation as follows.
\[\sigma_1 \times ... \times \sigma_n \:\stackrel{\text{def}}{=}\: \sigma_1 \times (\sigma_2 \times ... (\sigma_{n-1} \times \sigma_n)...)\]To define elements of an $n$-ary product, we use the tupling notation
\[\langle M_1 ,... , M_n \rangle \:\stackrel{\text{def}}{=}\: \langle M_1 , \langle M_2 , ... \langle M_{n-1} , M_n \rangle...\rangle \rangle\]as syntactic sugar for a nested pair. It is easy to cheack that if $M_i:\sigma_i$, then
\[\langle M_1 ,... , M_n \rangle : \sigma_1 \times ... \times \sigma_n\]To retrieve the components of an $n$-tuple, we use the following notation for combinatations of binary projection functions.
\[\begin{split} \mathbf{Proj}_i^{\sigma_1 \times ... \times \sigma_n} \:&\stackrel{\text{def}}{=}\: \lambda x:\sigma_1 \times ... \times \sigma_n.\:\mathbf{Proj}_1(\mathbf{Proj}_2^{i-1}x) \quad \quad \quad \quad(i < n) \\ \mathbf{Proj}_n^{\sigma_1 \times ... \times \sigma_n} \:&\stackrel{\text{def}}{=}\: \lambda x:\sigma_1 \times ... \times \sigma_n.\:(\mathbf{Proj}_2^{n-1}x) \\ \end{split}\]The projection operator $\mathbf{Proj}_2^k$ means applying $\mathbf{Proj}_2$ for $k$ times.
And we can deduce that
\[\mathbf{Proj}_i^{\sigma_1 \times ... \times \sigma_n} \langle M_1 ,... , M_n \rangle \twoheadrightarrow M_i.\]Translation Conclusion
Using $n$-tuples, we can now translate records with more than two components into PCF quite easily. If we want to eliminate records of some type \(\{ l_1:\sigma_1, ..., l_k:\sigma_k \}\), we choose some ordering of the labels $l_1, …, l_k$ and write each type expression and record expression using this order. We then translate expressions with records into PCF as follows.
\[\begin{split} \{ l_1:\sigma_1, ..., l_k:\sigma_k \} \:&\stackrel{\text{def}}{=}\: \sigma_1 \times ... \times \sigma_k \\ \{ l_1 = M_1, ..., l_k = M_k \} \:&\stackrel{\text{def}}{=}\: \langle M_1 ,... , M_k \rangle \\ M \centerdot l_i \:&\stackrel{\text{def}}{=}\: \mathbf{Proj}_i^{\sigma_1 \times ... \times \sigma_n} M \end{split}\]If an expression contains more than one type of records, we apply the same process to each type independently.
Iteration and Tail Recursion
Many algorithms, when written in an imperative language like C, use the following pattern of iteration.
1
2
3
4
Initialize;
while (! Done) {
Stmt; // Statements
}
In the “Initialize” part before the while loop, we may need to declare and initialize the value of some variables that will be used in the loop.
If the “Initialize” and “Stmt” parts only change the values of a fixed, finite set of variables, and “Done” is a side-effect-free test depending on the values of these variables, then we may easily transform a program segment of this form into a functional program.
Let us assume for simplicity that there is only one variable involved. There is no loss of generality because we can replace a finite set of variables with a record containing their values.
To put this in the context of PCF, suppose we have PCF expressions
\[\begin{split} &init:\sigma\\ &next:\sigma \rightarrow \sigma\\ &done:\sigma \rightarrow bool\\ \end{split}\]The first expression $init$ is the variable declared in the “Initialize” part. The second expression $next$ is the function that updates the value of $init$ as what have done in “Stmt” part. And the third expression $done$ is the function that outputs a boolean based on the value of $init$. So that the iteration could be written as the following C program using an additional variable $x$.
1
2
3
4
int x = init; // suppose init is of type int
while (! done(x)) {
x = next(x);
}
And this can be transformed into the recursion format with an additional function $f$ as follows.
1
2
3
4
5
int f(int x) {
if (done(x)) return x;
else return f(next(x));
}
int x = f(init);
We can do something similar in PCF by defining the expression \(loop\: init \: next \: done\) by
\[\begin{split} loop\: init \: next \: done \:\:\:\stackrel{\text{def}}{=}\:\:\: &\text{ letrec } f(x:\sigma) = \text{ if } (done \: x) \text{ then } x \text{ else } f \: (next \: x) \\ &\text{ in } (f \: init) \end{split}\]For easier understanding, you can think of $loop$ as a function that accepts three parameters: $init$, $next$, and $done$.
If we write \(next^n \:x\) for the result \(next\:(next\:(...(next\:x)...))\) of applying $next$ to $x$ a total of $n$ times, we have the following proposition.
(Proposition.) If \(done \: (next^i \: init) \twoheadrightarrow false\) for all $i < n$ and \(done \: (next^n \: init) \twoheadrightarrow true\), then
\[loop\: init \: next \: done \twoheadrightarrow next^n \: init\]The translation of iterative loops into recursive functions always produces a recursive function with a particular form. A recursive function with a definition of the form
\[f(x) = \text{ if } B \text{ then } M \text{ else } f(N) ,\]where neither $B$, $M$ nor $N$ contains $f$, is called a tail-recursive function.
In many modern languages, tail-recursive functions are often recognized by the compiler. This type of recursion will be compiled into efficient iterative code that does not require a new stack frame for each recursion call.
Total Recursive Functions
A commonly accepted belief, called Church’s thesis, is that every numeric function that is computable by any practical computer is recursive. This thesis was formulated in the 1930’s, before electronic computers, during a period when mathematicians were actively investigating the possibility and impossibility of solving problems by systematic algorithms.
One reason for believing Church’s thesis is that all of the formalisms for defining computable functions that were proposed in 1930’s, and since, give rise to the same set of functions on the natural numbers. The early formalisms include the recursive functions, Turing machines, and lambda calculus. It follows from Church’s thesis (although there is no way to prove something rigorously), that every partial or total function definable in PCF is recursive. And this gives evidence that every computable function on natural numbers is definable in PCF. In other words, at least for natural-number functions, PCF is a “universal” programming language. Besides, relying on undecidable properties of recursive functions, we can obtain interesting undecidability properties of PCF.
Church’s thesis has the limitation for function on types other than natural numbers. For basic data such as booleans, strings, or arrays of such data, it makes sense to think of the computable functions as precisely those functions we can compute when we code each boolean, string or array by a natural number. By this reasoning, we can see that any programming language that lets us associate natural numbers with its basic data types, and compute all recursive functions on the natural numbers, is “universal” for defining computable functions on all the basic data types.
However, for “infinite” values, such as functions, the issue is not as clear-cut. In particular, mathematical logicians have identified several distinct classes of “computable functions on the natural-number functions” and have not been able to prove that these are identical.
Definition of Total Recursive Functions
Since we have pairing in PCF, we will consider total recursive functions of more than one argument. A function $f$ is numeric if $f:\mathbb{N}^k \rightarrow \mathbb{N}$ for some $k > 0$. If $\mathcal{C}$ is a class of numeric functions, we say $\mathcal{C}$ is
- Closed under composition if, for every $f_1,…,f_l:\mathbb{N}^k \rightarrow \mathbb{N}$ and $g:\mathbb{N}^l \rightarrow \mathbb{N}$ from $\mathcal{C}$, the class $\mathcal{C}$ also contains the function $h$ defined by
- Closed under primitive recursion if, for every $f:\mathbb{N}^k \rightarrow \mathbb{N}$ and $g:\mathbb{N}^{k+2} \rightarrow \mathbb{N}$ from $\mathcal{C}$, the class $\mathcal{C}$ contains the function $h$ defined by
- Closed under minimization if, for every $f:\mathbb{N}^{k+1} \rightarrow \mathbb{N}$ such that \(\forall \: n_1,...,n_k\:.\:\exists \: m \:.\: f(m,n_1,...,n_k) = 0\), the class $\mathcal{C}$ contains the function $g$ defined by
These definitions may look quite wierd. You will understand their meaning better after reading the later definability proof section.
The class $\mathcal{R}$ of total recursive functions is the least class of numeric functions that contains the projection functions $\mathbf{Proj}_i^k(n_1,…,n_k)=n_i$, the successor function \(\lambda x:nat.\:x+1\), the constant zero function \(\lambda x:nat.\:0\), and that is closed under composition, primitive recursion, and minimization.
We can show that every total recursive function is definable in PCF. Formally put, for any natural number $n \in \mathbb{N}$, let us write $\lceil n \rceil$ for the corresponding numeral of PCF. We say a numeric function $f:\mathbb{N}^k \rightarrow \mathbb{N}$ is PCF-definable, or simply definable, if there is a closed PCF expression $M:nat^k \rightarrow nat$, where $nat^k$ is the $k$-ary product type $nat \times … \times nat$, such that
\[\begin{split} \\\forall \:n_1,...,n_k \in \mathbb{N}\:.\: M \: \langle \lceil n_1 \rceil,...,\lceil n_k \rceil \rangle = \lceil f(n_1,...,n_k) \rceil. \end{split}\]For a natural number $n$, its corresponding numeral $\lceil n \rceil$ is the symbol we write down in a text editor as part of PCF language.
Theorem 1
(Theorem.) Every total recursive function is definable in PCF.
(Proof.) To prove this, by the definition of total recursive functions, we must give the projection function $\mathbf{Proj}_i^k$, the successor function, and the constant zero function (i.e., define them as syntactic sugar in PCF), and show closure under composition, primitive recursion, and minimization. Following our previous description, we let
\[\begin{split} \mathbf{Proj}_1^1 \:&\stackrel{\text{def}}{=}\: \lambda x:nat.\:x\\ \mathbf{Proj}_1^k \:&\stackrel{\text{def}}{=}\: \lambda x:nat^k.\:\mathbf{Proj}_1x \quad \quad \quad \quad \quad \quad \quad(1 < k) \\ \mathbf{Proj}_i^k \:&\stackrel{\text{def}}{=}\: \lambda x:nat^k.\:\mathbf{Proj}_{i-1}^{k-1}(\mathbf{Proj}_2x) \quad \quad (1 < i \leq k) \\ succ \:&\stackrel{\text{def}}{=}\:\lambda x:nat.\:x+1\\ zero \:&\stackrel{\text{def}}{=}\:\lambda x:nat.\:0\\ \end{split}\]If $f_1,…,f_l:\mathbb{N}^k \rightarrow \mathbb{N}$ and $g:\mathbb{N}^l \rightarrow \mathbb{N}$ are represented by the PCF terms $M_1,…,M_l$ and $N$, respectively, then the function $h$ defined by composition is represented by the term
\[\lambda x:nat^k .\: N \: \langle M_1\:x ,..., M_l\:x \rangle.\]If $f:\mathbb{N}^k \rightarrow \mathbb{N}$ and $g:\mathbb{N}^{k+2} \rightarrow \mathbb{N}$ are represented by $M$ and $N$, then the function $h$ defined by primitive recursion is represented by
\[\lambda \langle x:nat,y:nat^k \rangle.\: prim \:(M \: y) \: (\lambda\langle m:nat,n:nat \rangle .\:N \:\langle m,\langle n,y \rangle \rangle) \: x,\]where $prim: \sigma \rightarrow (\sigma \times nat \rightarrow \sigma) \rightarrow nat \rightarrow \sigma$ is a function defined recursively for any $g:\sigma$, $h:\sigma \times nat \rightarrow \sigma$, and $n:nat$ as follows
\[\begin{split} &prim \: g \: h \: 0 = g \\ &prim \: g \: h \: (n+1) = h \: \langle prim \: g \: h \: n, n \rangle\\ \end{split}\]You may find that the function $prim$ is similar to the PCF expression \(loop\: init \: next \: done\) we introduced in the previous section. Because the creation of $prim$ is intended to model primitive recursions, i.e., “for” loops (that is, we know how many iterations we need before entering the loop).
For $prim$, the first argument $g$ corresponds to $init$, the second argument $h$ corresponds to $next$, and the last argument $n$ represents the number of iterations.
If $f:\mathbb{N}^{k+1} \rightarrow \mathbb{N}$ is represented by $M$, and for every $n_1,…,n_k$ there exists an $m$ such that $f(m,n_1,…,n_k)=0$, then the function $g$ defined by minimization is represented by
\[\lambda x:nat^k.\: search \: (\lambda n:nat . \: M \: \langle n,x \rangle),\]where $search$ is a syntactic sugar defined as follows.
\[\begin{split} search \:\stackrel{\text{def}}{=}\: & \lambda p:nat \rightarrow bool. \: \text{letrec } f(x:nat):nat = \\ & \text{if } (p \: x) \text{ then } x \text{ else } f\:(x+1) \: \text{ in }f \: 0 \end{split}\]You can think of $search$ as a function which accepts a function $p:nat \rightarrow bool$ as input, and outputs the smallest natural number $x$ such that \(p \: x \twoheadrightarrow true\).
Partial Recursive Function
In this section, we show that every partial recursive function is definable in PCF. Since it is generally believed that all mechanically computable functions are partial recursive functions, the main theorem of this section suggests that every function on the natural numbers that could be computed by any ordinary computer is definable in PCF. Two corollaries are that there is no algorithm to determine whether a PCF expression has a normal form and no algorithm to determine whether two PCF expressions are provably equal.
We first discuss the representation of partial functions, and then define the class of partial functions.
Partial Function
In mathematics, a partial function $f$ from a set $X$ to a set $Y$ is a function from a subset $S$ of $X$ (possibly the whole $X$ itself) to $Y$. If $S$ equals $X$, that is, if $f$ is defined on every element in $X$, then $f$ is said to be a total function. Total function is a kind of partial function.
Suppose we have some partial function $f: \mathbb{N} \rightarrow \mathbb{N}$ which we would like to represent by a PCF expression. We clearly want a closed term $M: nat \rightarrow nat$ such that $M : \lceil n \rceil$ gives the values of $f(n)$ when $f(n)$ is defined. However, it is not as clear what property $M$ should have if $f(n)$ is not defined on some values of $n$.
A convenient representation of undefinedness, or nontermination, is that $M : \lceil n \rceil$ should have no normal form when $f(n)$ is undefined. Following this thinking, we say a partial function $f:\mathbb{N}^k \rightarrow \mathbb{N}$ is PCF-definable, or simply definable, if there is a closed PCF expression $M:nat^k \rightarrow nat$ such that for all $n_1,…,n_k \in \mathbb{N}$ , we have
\[\begin{split} M \langle \lceil n_1 \rceil ,...,\lceil n_k \rceil \rangle = \begin{cases} \lceil f(n_1,...,n_k) \rceil & \text{if } f(n_1,...,n_k) \text{ is defined,}\\\\ \text{has no normal form} & \text{otherwise}. \end{cases} \end{split}\]Definition of Partial Recursive Functions
To show that every partial recursive function is definable in PCF, we give a precise definition of the class of all partial recursive functions. A partial function $f$ is numeric if $f:\mathbb{N}^k \rightarrow \mathbb{N}$ for some $k > 0$. If $\mathcal{C}$ is a class of partial numeric functions, we say $\mathcal{C}$ is
- Closed under composition if, for all partial functions $f_1,…,f_l:\mathbb{N}^k \rightarrow \mathbb{N}$ and $g:\mathbb{N}^l \rightarrow \mathbb{N}$ from $\mathcal{C}$, the class $\mathcal{C}$ also contains the partial function $h$ defined by
- Closed under primitive recursion if, for every $f:\mathbb{N}^k \rightarrow \mathbb{N}$ and $g:\mathbb{N}^{k+2} \rightarrow \mathbb{N}$ from $\mathcal{C}$, the class $\mathcal{C}$ contains the function $h$ defined by
- Closed under minimization if, for every $f:\mathbb{N}^{k+1} \rightarrow \mathbb{N}$ such that \(\forall \: n_1,...,n_k\:.\:\exists \: m \:.\: f(m,n_1,...,n_k) = 0\), the class $\mathcal{C}$ contains the function $g$ defined by
The class $\mathcal{PR}$ of partial recursive functions is the last class of partial numeric functions that contains the projection functions $\mathbf{Proj}_i^k(n_1,…,n_k)=n_i$, the successor function \(\lambda x:nat.\:x+1\), the constant zero function \(\lambda x:nat.\:0\), and that is closed under composition, primitive recursion, and minimization.
The only difference between the definitions of partial and total recursive functions is the discussion of undefined cases.
Theorem 2
(Theorem.) Every partial recursive function is definable in PCF.
(Proof.) The proof is similar to the proof of Theorem 1, except that the term representing a partial recursive function must not have a normal form when the partial function is undefined. We can see that this requires some changes by considering the composition case.
If $f,g: \mathbb{N} \rightarrow \mathbb{N}$ are unary partial recursive functions, represented by PCF terms $M$ and $N$, then in the previous proof, we represent the composition $h(n) = g(f(n))$ by the term \(\lambda x:nat.\: N \: (M \: x)\). However, this does not have the correct termination behavior when $f$ may be partial.
For example, let $g$ be the constant function $g(x) = 3$ and $f$ a partial function with $f(5)$ undefined. The ordinary mathematical convention is to consider $h(5) = g(f(5))$ undefined since $f(5)$ is undefined. However, the application \((\lambda x:nat.\: N \: (M \: x))\: 5\) reduces to $3$ in PCF.
A simple trick is to define a function $cnvg$ that may be used to force nontermination in PCF when required. We define a separate function $cnvg_k$ for each natural number $k>0$. We use $k$ here to specify the number of arguments. Specifically, if $f$ and $g$ are numeric functions of $k$ arguments, then \(cnvg_k \: f \: g\) will behave like $g$, except that an application to $k$ arguments will only have a normal form (or “halt”) when the application of $f$ has a normal form. For any $k>0$, the function $cnvg_k$ may be written as follows.
\[cnvg_k \: f \: g\: \stackrel{\text{def}}{=} \: \lambda x:nat^k.\: \text{ if } Eq? \: (f \: x) \: 0 \: \text{ then } g\:x \text{ else } g\:x\]For any $x$, if \(f \: x\) can be reduced to normal form then (whether this is equal to zero or not) the result is \(g \: x\). However, if \(f \: x\) cannot be reduced to a normal form, then the conditional can never be eliminated and \(cnvg_k \: f \: g\) will not have a normal form. Because we cannot reduce \(Eq? \: (f \: x) \: 0\) to $true$ or $false$ without reducing \(f \: x\) to normal form.
Using $cnvg$, we can define a composition $f$ and $g$ that is defined only when $f$ is defined. For example, if $f,g: \mathbb{N} \rightarrow \mathbb{N}$ are unary partial recursive functions represented by PCF term $M$ and $N$, we represent their composition by the term \(cnvg \: M \: (\lambda x:nat.\: N \: (M \: x))\).
The generalization to the composition of partial functions $f_1,…,f_l:\mathbb{N}^k \rightarrow \mathbb{N}$ and $g:\mathbb{N}^l \rightarrow \mathbb{N}$ is straightforward. And the remaining cases of the proof can be treated similarly, using $cnvg_k$ for appropriate $k$. $\blacksquare$
Corollaries
Theorem 2 has some important corollaries. Both of the corollaries below follow from a well-known undecidability property of recursive functions. Specifically, there is no recursive, or algorithmic, method for deciding whether a recursive partial function is defined on some argument. This fact is often referred to as the recursive unsolvability of the Halting Problem.
(Corollary 1.) There is no algorithm for deciding whether a given PCF expression has a normal form.
(Proof.) If there were such an algorithm, then by Theorem 2, we could decide whether a given partial recursive function was defined on some argument, simply by writing the function applied to its argument in PCF. $\blacksquare$
(Corollary 2.) There is no algorithm for deciding equality between PCF expressions.
(Proof.) If there were such an algorithm, then by Theorem 2, we could decide whether a given partial recursive function was defined on some argument. Specifically, given a description of a partial function $f$, we may produce $PCF$ term $M$ representing the application $f(n)$ by the straightforward algorithm outlined in the proof of Theorem 2, for any $n$. Then, using the supposed algorithm to determine whether \(\text{ if } Eq? \: (f \: x) \: 0 \: \text{ then } g\:x \text{ else } 0=0\), we could decide whether $f(n)$ is defined. $\blacksquare$