# Combinators for the Primitive Recursive Functions

It is well-known that the S and K combinators are Turing Complete. Are there combinators that suffice to yield (only) the primitive recursive functions?

-
Is this what you are asking? mathoverflow.net/questions/48006/… – Andrej Bauer Jan 10 '13 at 20:03
Essentially, yes. Thanks. – user217281728 Jan 11 '13 at 17:46

Yes, but you have to consider typed combinators. That is, you need to give $S$ and $K$ the following type schemas: $$\begin{array}{lcl} K & : & A \to B \to A \\ S & : & (A \to B \to C) \to (A \to B) \to (A \to C) \end{array}$$ where $A, B$, and $C$ are meta-variables which can be instantiated to any concrete type at each use.

Then, you want to add the type $\mathbb{N}$ of natural numbers to the language of types, and add the following combinators: $$\begin{array}{lcl} z & : & \mathbb{N} \\ succ & : & \mathbb{N} \to \mathbb{N} \\ iter & : & \mathbb{N} \to (\mathbb{N} \to \mathbb{N}) \to \mathbb{N} \to \mathbb{N} \end{array}$$

The equality rules for the additions are: $$\begin{array}{lcl} iter\;i\;f\;z & = & i \\ iter\;i\;f\;(succ\;e) & = & f(iter\;i\;f\;e) \end{array}$$

It's much easier to read the programs you write, if you just write programs in the simply-typed lambda calculus, augmented with the numerals and iteration. The system I've described is a restriction of Goedel's T, the language of higher-type arithmetic. In Goedel's T, the typing for iteration is less limited: $$\begin{array}{lcl} iter & : & A \to (A \to A) \to \mathbb{N} \to A \end{array}$$ In T, you can instantiate $iter$ at any type, not just the type of natural numbers. This takes you past primitive recursion, and lets you define things like Ackerman's function.

EDIT: Xoff asked how to encode the predecessor function. It follows via a standard trick. To explain, I'll use lambda-notation for this (which can be eliminated with bracket-abstraction), since that's far more readable. First, assume that we have pairs and the more general type for $\mathit{iter}$. Then, we can define:

$$\begin{array}{lcl} pred' & = & \lambda k.\;iter \;(z, z) \; (\lambda (n, n').\; (succ\;n, n))\;k\\ pred & = & \lambda k.\;snd(pred'\;k) \end{array}$$

If you just have the nat-type iterator, then you need to exploit the isomorphism that $\mathbb{N} \simeq \mathbb{N} \times \mathbb{N}$, which is annoying but poses no fundamental obstacle.

-
So this is less than Turing-complete by virtue of the restriction to typed combinators? Can the type variables (recursively) denote functions over type variables (e.g. A = D -> E for some types D and E)? – user217281728 Jan 11 '13 at 17:48
Yes, they can. The restriction to typed $S$ and $K$ makes this language into a combinatory presentation of the simply-typed lambda calculus, which is known to terminate despite having higher-order functions. You can see how to translate STLC into categorically-inspired combinators in this blog post of mine: semantic-domain.blogspot.com/2012/12/… – Neel Krishnaswami Jan 11 '13 at 19:33
Neel, thanks. Would I be right in thinking that it's possible to represent z, succ and iter in terms of S and K via the Church numeral encoding? – user217281728 Jan 13 '13 at 8:48
How do you do the predecessor function with your system (function such that $0\mapsto 0$ and $(succ x)\mapsto x$ ? – Xoff Jul 24 '14 at 14:15
@Xoff: the predecessor function has a well known linear-time definition in terms of iter. This could be the object of a question on cs.stackexchange.com... – cody Jul 27 '14 at 17:03