Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

It is well known that primitive recursion is not powerful enough to express all functions, Ackermann function being probably the best known example.

Now, in the logic courses (that I have had look at) one always proceeded from primitive recursion to mu-recursion. In computer science terms this basicly means we are jumping from a formalism where programs are quaranteed to halt to a Turing-complete formalism where halting is a non-computable property i.e. we can't say for every program if it will eventually halt.

I got curious if there is any hierarchy between primitive recursion and mu-recursion. After a while I found a programming language called Charity. In Charity (according to Wikipedia) all programs are quaranteed to stop, thus its not Turing-complete, but, on the other hand, it is expressive enough to implement Ackermann function.

This suggests there is at least one level between mu-recursion and primitive recursion.

My question is: does there exists any other halt-for-sure formalisms that are more expressive than primitive recursion? Or, even better, does there exist some known hierarchies between mu-recursive and primitive recursive functions? I'm curious about how "much" we can compute with a formalism that guarantees halting.

share|improve this question
2  
This question appears to be very closely related: mathoverflow.net/questions/35461/… –  Chris Pressey Nov 29 '12 at 21:30

7 Answers 7

up vote 11 down vote accepted

I think it would also be reasonable to (explicitly) mention the functions definable by primitive recursion in higher types - instead of only defining functions $\mathbb{N}\to\mathbb{N}$ by primitive recursion, we may also define families of functions (i.e. functions $\mathbb{N}\to\mathbb{N^N}$) by primitive recursion (and, of course, even more complicated things).

As an example, let us first define an iteration function $g\colon\mathbb{N}\times\mathbb{N^N}\to\mathbb{N^N}$ by primitive recursion, by: \begin{array}{l} g(0,f) = i \qquad\qquad\text{(the identity function)}\\\\ g(n+1, f) = f\circ g(n, f) \end{array} We can then easily define a `curried' version of the Ackermann function as a function $A\colon\mathbb{N}\to\mathbb{N^N}$, by: \begin{array}{l} A(0) = S \quad\quad\text{(successor)}\\\\ A(n+1) = g(n, A(n)) \end{array}

This is quite popular with (some groups of) computer scientists, particularly those interested in functional programming, and some form of primitive recursion in higher types is behind the strength of the language Charity you mentioned (which also allows primitive recursion over other data structures than the natural numbers).

share|improve this answer
    
Thank you for adding this! I was sorry to see an answer accepted without this approach being mentioned, when it seems to me to be more useful for real programming. I wanted to mention it myself, but it was not something I was in a position to look up or work out myself when I made my original answer: I was invigilating an exam. –  Max Nov 29 '10 at 21:08
    
This is very helpful answer and I might have rushed when flagging answer (I wasn't expecting more answers). Thank you for writing this up anyway! Kow, do you happen to have any references in hand for any applications of this method? –  user10891 Dec 10 '10 at 18:07
1  
References is perhaps overstating it. I've learnt about it in the context of proof assistants for higher-order logic (e.g. Isabelle/HOL) and type theory (e.g. Coq). All these have extensive online documentation and examples (and have been used for major proofs, e.g. Gonthier's proof of the four color theorem). You might also look at the chapter on finite type arithmetic in Troelstra&van Dalen's Constructivism in Mathematics, Vol 2, for more background. It might also interest you to think about what can be done with an NNO in a Cartesian Closed Category -- exponentials are very useful. –  kow Dec 14 '10 at 15:49

Robin Chapman's answer is very apropos. Here is a theoretical answer that points out a subtlety in the question.

First, recall that the primitive recursive functions are the smallest class of functions on $\mathbb{N}$ that:

  • Includes the constant zero function, the successor function, and all projection functions;
  • is closed under composition;
  • and is closed under primitive recursion.

Let's call this class of functions $\operatorname{PR}(\emptyset)$. For any set $A$ of number theoretic functions, we can define a more general class $\operatorname{PR}(A)$ as the smallest class of functions that satisfies the above properties and also includes every function in $A$.

If every function in $A$ is computable, then every function in $\operatorname{PR}(A)$ is computable. Moreover, if every function in $A$ is total then every function in $\operatorname{PR}(A)$ is total.

It would be trivial, assuming $A$ is finite (or, more generally just explicitly enumerated), to create a programming language such that every program in the language computes a function in $\operatorname{PA}(A)$ and every such function has a program in the language. The language simply has primitives for all the functions in $A$ and for the basic primitive recursive functions, along with operators for composition and primitive recursion.

Therefore, one answer to "I'm curious about how "much" we can compute with a formalism that guarantees halting." is "For any total computable function there is such a formalism" and more generally this is true for any effective sequence of total computable functions.

The main thing that such a system cannot have is a universal function, provided the system has some basic closure properties.

Addendum

Since several people pointed out the same thing, I may as well add some value to the answer by including the standard proof of my remark about universal functions. A universal two-place function, for some system, is a function $g(i,k)$ such that for every one-place function $f(k)$ in the system there is some natural number $e$ with $\lambda k .f(k) = \lambda k. g(e,k)$. Suppose that $g$ is such a function; define a function $h$ as $h(k) = g(k,k) + 1$. Then $h$ has some index $e$. Thus $g(e,e) = h(e)$ by the definition of $g$ and $e$, and $h(e) = g(e,e) + 1$ by construction of $h$. This is impossible, so any system of total functions that allows me to form the functions like $h$ cannot have a universal function $g$.

In particular, for any class of functions $A$ and any function $g(j,i)$ in $\operatorname{PA}(A)$, the function $h(n) = g(n,n)+1$ is in $\operatorname{PR}(A)$. So this class will not have a universal function provided that every function in $A$ is total. Of course if you let $A$ be the set of all partial computable functions then $\operatorname{PR}(A)$ is also the set of all partial computable functions and so it does contain a universal function (which is not total).

From this point of view, the limitation is not on whether particular computable functions can be included; the limitation is on the internal structure of any particular effective class of functions.

share|improve this answer
    
Carl, it seems we came to the same conclusion. –  Joel David Hamkins Nov 17 '10 at 14:48
    
Yes, and Max also had the same insight, just in a more preliminary form. –  Carl Mummert Nov 17 '10 at 14:51
    
Ok, it surely seems I got the mathematical background well explained in these answers. Thanks to everybody for that. I'm not sure about the usual policy about the points and stuff, but as the fast growing hierarchy pointer happens to be pretty much what I was looking for I'll mark it as an answer. –  user10891 Nov 18 '10 at 10:37

You might look up fast-growing hierarchies.

share|improve this answer
    
At a high level, this is very much the answer, in that it allows us to capture the strength of theories described by certain amount of recursion, while being independent of the actual presentation of the version of recursion being allowed (instead, as a typical example, we have access to a limited amount of induction). –  Andres Caicedo Nov 17 '10 at 17:49
2  
But PR can extend to the side also, and not just upward; not every extension of PR involves fast-growing functions. For example, adding the characteristic function of a suitably generic real will not lead to any dominating functions at all. –  Joel David Hamkins Nov 23 '10 at 14:53

One can consider programming formalisms where a program is a pair (M, P), with M a Turing machine and P a proof that M halts on all inputs. Then, if the proof is correct, (M, P)(x) = M(x); if it is incorrect, (M, P)(x) = 0.

Alternatively, one can consider primitive recursion with an "oracle" function: so, for example, we can allow the Ackermann function in our recursion bounds. If we use a primitive recursive oracle, we gain no power; but as long as we use a computable function, our functions remain computable. This should give a hierarchy with respect to the oracles, but I'm not sure of the details.

share|improve this answer

The class PR of primitive recursive functions is the smallest class of functions containing a few simple functions (successor, zero, projection) and closed under composition and definition of functions by recursion.

If $f:\mathbb{N}^k\to \mathbb{N}$ is any function at all, one can form the class $PR(f)$ of functions that are primitive recursive relative to $f$, simply by adding $f$ as one of the simple functions and then closing under composition and recursion. If $f$ is total, then every function in $PR(f)$ is total, and if $f$ is computable, then every function in $PR(f)$ will be computable. This amounts to using $f$ as an oracle, as mentioned by Max. There is a clear hierarchy here, because if $f\in PR(g)$, then $PR(f)\subset PR(g)$, and this hierarchy amounts to something like the hierarchy of Turing degrees, but with primitive recursion.

More generally, for any set $F$ of functions, we may form $PR(F)$ by adding all the functions in $F$ and closing under composition and recursion, and we still have the hierarchy that if $F\subset PR(G)$, then $PR(F)\subset PR(G)$. This more general situation seems fully general, since if you have a class $F$ of functions containing all primitive recursive functions and closed under composition and recursion, then $F=PR(F)$, and so this hierarchy seems to capture all the classes that you might wish to consider.

share|improve this answer

Look for John Reynolds paper "Total functional programming" which is about a programming language in which only primitive recursive functions in a setting where higher-order types (like in Gödel's system T) are allowed. Maybe that resembles Charity which Kow mentioned. Reynolds cites a theorem (of Spector?) saying the functions his language can express are exactly the ones provably total in second-order arithmetic. That is enormous compared with Ackermann's function but still stops short of various total functions that can be implemented on general Turing machines.

share|improve this answer
    
You mean DA Turner's paper Total functional programming? –  Martin Berger May 5 at 10:51

Regarding hierarchy, it's basic result of recursion theory that every recursive function f, is expressible as:

$f(x_{0},…,x_{n}) = u(\mu y.(T(e_{f},\langle x_{0},…,x_{n}\rangle))$

where $T$, $u$ are fixed primitive recursive functions, and $e_{f}\in\mathbb{N}$ depends on $f$ (it is a code name describing how $f$ is built). (See any elementary text like Schönfield.)

Thus the hierarchy is pretty short.

share|improve this answer
1  
The question and answers are about the hierarchy that arises without the $\mu$-operator, closing under primitive recursion but not unbounded search. –  Joel David Hamkins Feb 7 '11 at 8:40

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.