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?
Tell me more
×
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.
|
|
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. |
|||||||
|
