# 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?

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} \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(e,\;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 Ackermann's function.

EDIT: Xoff asked how to encode the predecessor function. It follows via a standard trick of Kleene's. 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 already have the predecessor as $$iter\;z\;K$$.

• 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)? Jan 11, 2013 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/… Jan 11, 2013 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? Jan 13, 2013 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, 2014 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, 2014 at 17:03