21

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?

NietzscheanAI
  • 775
  • 4
  • 11
  • 1
    Is this what you are asking? http://mathoverflow.net/questions/48006/is-it-correct-to-state-that-basic-primitive-recursive-functions-are-in-fact-combi – Andrej Bauer Jan 10 '13 at 20:03

1 Answers1

19

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

David Sheets
  • 3
  • 2
Neel Krishnaswami
  • 32,528
  • 1
  • 100
  • 165
  • 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)? – NietzscheanAI Jan 11 '13 at 17:48
  • 2
    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: http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html – 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? – NietzscheanAI Jan 13 '13 at 08: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
  • @cody, Can't you give me a one line solution in a comment ?? :) – Xoff Jul 27 '14 at 17:23
  • I didn't want to derail the conversation. It's a bit hard to understand at first read: – cody Jul 27 '14 at 19:50
  • Do we need to manually add pairs (including the pair constructor and the two projection operators) in order for this language to be able to represent the predecessor function (or perform the $\mathbb{N} \simeq \mathbb{N} \times \mathbb{N}$ encoding and decoding)? – user76284 Aug 07 '18 at 05:57
  • I heard it said that the predecessor was invented on a dentist's chair. – Andrej Bauer Jan 26 '22 at 12:46