<p>Yes, but you have to consider typed combinators. That is, you need to give <span class="math-container">$S$</span> and <span class="math-container">$K$</span>
the following type schemas:
<span class="math-container">$$
\begin{array}{lcl}
K &amp; : &amp; A \to B \to A \\
S &amp; : &amp; (A \to B \to C) \to (A \to B) \to (A \to C)
\end{array}
$$</span>
where <span class="math-container">$A, B$</span>, and <span class="math-container">$C$</span> are meta-variables which can be instantiated to any concrete type at each use.</p>
<p>Then, you want to add the type <span class="math-container">$\mathbb{N}$</span> of natural numbers to the language of types, and add the following combinators:
<span class="math-container">$$
\begin{array}{lcl}
z &amp; : &amp; \mathbb{N} \\ 
succ &amp; : &amp; \mathbb{N} \to \mathbb{N} \\ 
iter &amp; : &amp; \mathbb{N} \to (\mathbb{N} \to \mathbb{N} \to \mathbb{N}) \to \mathbb{N} \to \mathbb{N}
\end{array}
$$</span></p>
<p>The equality rules for the additions are:
<span class="math-container">$$
\begin{array}{lcl}
iter\;i\;f\;z &amp; = &amp; i \\
iter\;i\;f\;(succ\;e) &amp; = &amp; f(e,\;iter\;i\;f\;e)
\end{array}
$$</span></p>
<p>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 <em>Goedel's T</em>, the language of higher-type arithmetic. In Goedel's T, the typing for iteration is less limited:
<span class="math-container">$$
\begin{array}{lcl}
iter &amp; : &amp; A \to (A \to A) \to \mathbb{N} \to A
\end{array}
$$</span>
In T, you can instantiate <span class="math-container">$iter$</span> 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.</p>
<p>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 <span class="math-container">$\mathit{iter}$</span>. Then, we can define:</p>
<p><span class="math-container">$$
\begin{array}{lcl}
pred' &amp; = &amp; \lambda k.\;iter \;(z, z) \; (\lambda (n, n').\; (succ\;n, n))\;k\\
pred  &amp; = &amp; \lambda k.\;snd(pred'\;k)
\end{array}
$$</span></p>
<p>If you just have the nat-type iterator, then you already have the predecessor as <span class="math-container">$iter\;z\;K$</span>.</p>

CC BY-SA 3.0
2013-01-11T17:48:19.310Z
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
CC BY-SA 3.0
2013-01-11T19:33:02.770Z
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
CC BY-SA 3.0
2013-01-13T08:48:19.870Z
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
CC BY-SA 3.0
2014-07-24T14:15:16.880Z
How do you do the predecessor function with your system (function such that $0\mapsto 0$ and $(succ x)\mapsto x$ ?
Xoff
CC BY-SA 3.0
2014-07-27T17:03:54.043Z
@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
CC BY-SA 3.0
2014-07-27T17:23:39.377Z
@cody, Can't you give me a one line solution in a comment ?? :)
Xoff
CC BY-SA 3.0
2014-07-27T19:50:55.303Z
I didn't want to derail the conversation. It's a bit hard to understand at first read:
cody
CC BY-SA 4.0
2018-08-07T05:57:37.997Z
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
CC BY-SA 4.0
2022-01-26T12:46:57.657Z
I heard it said that the predecessor was invented on a dentist's chair.
Andrej Bauer
CC BY-SA 4.0
2013-01-10T21:31:37.983Z
2022-01-26T12:41:15.550Z
2022-01-26T12:41:15.550Z
Neel Krishnaswami
<p>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?</p>

CC BY-SA 3.0
2013-01-10T20:03:41.833Z
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
<lo.logic><computability>
Combinators for the Primitive Recursive Functions
NietzscheanAI
# Combinators for the Primitive Recursive Functions

(Asked by: username_0 on 2013-01-10)

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?

**Tags:** lo.logic, computability
> **Comments:**
> **username_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  

---

## 1 answers

### Answer by username_2 on 2013-01-10. Score: 19 | Accepted answer

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

> **Comments:**
> **username_0**: 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)?  
> **username_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  
> **username_0**: 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?  
> **username_3**: How do you do the predecessor function with your system (function such that $0\mapsto 0$ and $(succ x)\mapsto x$ ?  
> **username_4**: @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...  
> **username_3**: @cody, Can't you give me a one line solution in a comment ?? :)  
> **username_4**: I didn't want to derail the conversation. It's a bit hard to understand at first read:  
> **username_5**: 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)?  
> **username_1**: I heard it said that the predecessor was invented on a dentist's chair.  

---

