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?


1 Answer 1


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$.

  • $\begingroup$ 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)? $\endgroup$ Jan 11, 2013 at 17:48
  • 2
    $\begingroup$ 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/… $\endgroup$ Jan 11, 2013 at 19:33
  • $\begingroup$ 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? $\endgroup$ Jan 13, 2013 at 8:48
  • $\begingroup$ How do you do the predecessor function with your system (function such that $0\mapsto 0$ and $(succ x)\mapsto x$ ? $\endgroup$
    – Xoff
    Jul 24, 2014 at 14:15
  • $\begingroup$ @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... $\endgroup$
    – cody
    Jul 27, 2014 at 17:03

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.