I encountered this result when working with $\lambda$-calculus (so every element I mention here was a $\lambda$-expression there [1]), but I will express everything with, more understandable to broader audience, notions of functions.


Definition 1
A numeral system is a sequence $d = d_0,d_1,\ldots$ such that there exist functions $S$ (successor) and $isZ$ (test for zero) such that $$S(d_n) = d_{n+1},$$ $$isZ(d_0) = T,\ \ isZ(d_{n+1}) = F.$$ where $T$ and $F$ are notions of true and false.

Definition 2
A numeric function $\varphi : \mathbb{N}^p \to \mathbb{N}$ is definable with respect to $d$ if there exists $f$ such that $$\forall (n_1,\ldots,n_p)\in \mathbb{N}^p\ \ f(d_{n_1},\ldots,d_{n_p}) = d_{\varphi(n_1,\ldots,n_p)}.$$

Definition 3
A numeral system $d$ is adequate if and only if all partial recursive functions are definable with respect to $d$.

My question (intro)

Proposition 1 (Proposition 6.4.3 in [1])
Let $d$ be a numeral system. $d$ is adequate if and only if there exists $P$ (predecessor) such that $$\forall n \in \mathbb{N}\ \ P(d_{n+1}) = d_n.$$

For the $\Rightarrow$ direction, it is sufficient to observe that predecessor is a partial recursive function. Specifically, it is a primitive recursion of zero function and first coordinate projection.

My question
How would one prove a $\Leftarrow$ direction? How is it even possible to have such a powerful result, that existence of one function leads to definability of all partial recursive functions?

[1] Hendrik Pieter Barendregt, The Lambda Calculus, 1984.


Recall that the set of partial recursive functions $\mathcal{R}$ is defined inductively by the following rules:

  • (zero) $\dfrac{}{\zeta : n \mapsto 0 \in \mathcal{R}}$
  • (successor) $\dfrac{}{\sigma : n \mapsto n + 1 \in \mathcal{R}}$
  • (projection) $\dfrac{}{\Pi_m^i : (n_1, \cdots n_m) \mapsto n_i \in \mathcal{R}}$
  • (composition) $\dfrac{\chi : \mathbb{N}^m \to \mathbb{N}, \psi_i : \mathbb{N}^k \to \mathbb{N} \in \mathcal{R} }{\phi : (n_1, \cdots n_k) \mapsto \chi(\psi_1(n_1, \cdots, n_k), \cdots \psi_m(n_1, \cdots, n_k)) \in \mathcal{R}}$
  • (primitive recursion) $\dfrac{\chi : \mathbb{N}^m \to \mathbb{N}, \psi : \mathbb{N}^{n+2} \to \mathbb{N} \in \mathcal{R} }{\phi : (k,n_1, \cdots n_m) \mapsto \begin{cases} \chi(n_1, \cdots n_m) & \text{ if } k=0 \\ \psi(\phi(k-1, n_1, \cdots, n_m),k-1, n_1 \cdots n_m ) & \text{ if } k > 0\\ \end{cases} \in \mathcal{R}}$
  • (minimalization) $\dfrac{\chi : \mathbb{N}^{m+1} \to \mathbb{N} \in \mathcal{R} }{\phi : (n_1, \cdots n_m) \mapsto k \text{, the least integer with } \chi(k,n_1, \cdots n_m) =0 \in \mathcal{R}}$

So we will prove the result by structural induction on $\mathcal{R}$.

  • Initial functions.

It is clear that $\zeta$ is defined by $\lambda x. d_0$, $\sigma$ by $S$, and $\Pi_m^i$ by $\lambda x_1 \cdots x_m . x_i$.

  • Composition

Suppose $\chi$ is defined by $f$ and $\psi_i$ by $g_i$.

Let $h$ be the term $\lambda x_1 \cdots x_k.f (g_1x_1 \cdots x_k) \cdots (g_mx_1 \cdots x_k)$. Then $h$ defines the function $\phi : (n_1, \cdots n_k) \mapsto \chi(\psi_1(\vec{n}), \cdots \psi_m(\vec{n}))$

  • Primitive recursion.

Suppose $\chi$ is defined by $f$ and $\psi$ by $g$.

Let's define the combinator $\textbf{r} = \lambda nfg.isZ\:n\:f\:(g \:(P\:n))$, with the property that:

$$ \textbf{r} \: d_n \:f \: g = \begin{cases} f & \text{ if } n = 0 \\ g \: (d_{n-1}) & \text{ if } n > 0 \end{cases} $$

Now let $h$ be the term $\textbf{y} \: (\lambda s y x_1 \cdots x_m . \textbf{r} \: y(f x_1\cdots x_m)(\lambda z.g (s z x_1 \cdots x_m)z x_1 \cdots x_m )$. Then $h$ defines $\phi: (k,n_1, \cdots n_m) \mapsto \begin{cases} \chi(n_1, \cdots n_m) & \text{ if } k=0 \\ \psi(\phi(k-1, n_1, \cdots, n_m),k-1, n_1 \cdots n_m ) & \text{ if } k > 0\\ \end{cases}$.

  • Minimalization

Suppose $\chi$ is defined by $f.

Let $g$ be the term $\textbf{y} (\lambda syx_1 \cdots x_m.isZ \: (f\: y\: x_1\cdots x_m) \: y\: (s\: (S \: y)\: x_1 \cdots x_m))$. Then take $h$ to be the term $g \: d_0$, and $h$ defines the function $\phi : (n_1, \cdots n_m) \mapsto k \text{, the least integer with } \chi(k,n_1, \cdots n_m) =0$.

By induction, every function in $\mathcal{R}$ is definable.

(I leave the proving the fact that the terms $h$ define the stated functions as an exercise!)

| cite | improve this answer | |
  • $\begingroup$ Oh, I see it now. Numeral system by definition has to have $S$ and $isZ$, so the only thing missing is $P$ to be used in the definition of primitive recursion. Thanks! $\endgroup$ – Sandro Lovnički Sep 13 '18 at 1:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.