# 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 at 20:03
Essentially, yes. Thanks. – user1366423 Jan 11 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.
 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)? – user1366423 Jan 11 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 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? – user1366423 Jan 13 at 8:48