Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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?

share|improve this question
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

1 Answer 1

up vote 15 down vote accepted

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.

share|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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