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
1  
Is this what you are asking? mathoverflow.net/questions/48006/… –  Andrej Bauer Jan 10 '13 at 20:03
    
Essentially, yes. Thanks. –  user1366423 Jan 11 '13 at 17:46
add comment

1 Answer 1

up vote 12 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.

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)? –  user1366423 Jan 11 '13 at 17:48
1  
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? –  user1366423 Jan 13 '13 at 8:48
add comment

Your Answer

 
discard

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.