up vote 6 down vote favorite
1

So, I know that the halting problem is undecidable for Turing machines. The trick is that TMs can decide recursive languages, and can accept Recursively Enumerable (RE) languages.

I'm wondering, is there a more limited model of computation which accepts only recursive languages, and not RE? And if so, is there such a model which is always guaranteed to halt?

Obviously this model would be strictly less powerful than TMs and strictly more powerful than PDAs.

I'm open to a machine-style model, or a lambda-calculus style model.

As an example of what I'm thinking: the Coq language has a restriction that for any self-recursive calls, the first argument must be strictly decreasing in "size" i.e. if it is a natural number, it must be smaller, if it is a list, it must be shorter, etc. This guarantees that it always halts, but I have no idea if you can compute all of R this way.

share|cite|improve this question
  • 1
    You are not aware of that, but your question is probably answered by this one: there can be no useful model, arguably. – Raphael♦ May 12 '13 at 10:22
up vote 9 down vote accepted

Yes, there are as many models of R as there are of RE! Take a model of RE, and restrict it to the total elements of the model. For example, take Turing machines that halt. Or take total recursive functions. Or take your favorite programming language (idealized to remove memory limitations) but in addition to requiring that the source code be syntactically valid, also require that the program halt on every input.

The catch is that, since the halting problem is undecidable, for any model of R, given a recursive syntax for the elements, there cannot be any algorithm to decide whether a candidate element is valid. For example, a normal programming languages has syntactic rules, and sometimes a type system, to decide whether a program is well-formed; the parser or type checker implements a decision procedure to verify that the source code is an element of the language. If you want a programming language that is a model of RE rather than R, there is no way to decide whether some source code is a valid program.

Coq only allows a subset of all recursive functions: $\mathsf{Coq} \subsetneq \mathsf{R} \subsetneq \mathsf{RE}$. Both bounds of this inequality chain have decidable models but the middle item doesn't. Intuitively speaking, Coq only contains recursive functions whose termination can be proved by sufficiently simple arguments. While “sufficiently simple” covers just about anything mathematicians do, it is still very limited in a theoretical sense. (More precisely, Coq's theory is equivalent to I think the Peano axioms with a schema for recursion that goes up to a certain ordinal, but at that point it gets beyond my comprehension.)

share|cite|improve this answer
  • "For any model of R, given a recursive syntax for the elements, there cannot be any algorithm to decide whether a candidate element is valid." I don't buy this. Certainly, there's no algorithm which can look at an arbitrary model and tell whether it always halts or not, but I don't see why there couldn't be a specific model which has a specific proof that it always halts. Lots of programs have correctness or halting proofs, despite these problems being undecidable as a whole. – jmite May 10 '13 at 21:41
  • 3
    @jmite Ah, it's a case of an English setence not being precise enough to express quantifiers unambiguously. For any model, there is no algorithm such that for every candidate element, the algorithm decides whether that candidate is an element of the model. (On the other hand, for every model, for every candidate element, there is an algorithm that decides whether the candidate is an element: either the algorithm that always says yes works, or the algorithm that always says no works — the trick is to figure out which.) – Gilles♦ May 10 '13 at 21:47
  • It's even worse: any model for R is not even enumerable. (Does Coq allow more than primitive recursive functions?) – Raphael♦ May 12 '13 at 10:21
  • @Raphael Yes, Coq goes beyond PR, for example you can define Ackermann. All recursive definitions have to rely on structural induction, but you can not only to structural induction on inductive objects (which I believe would limit you to primitive recursive functions) but on any term including recursive functions. Or in other words nested fixpoints give you more than primitive recursion. – Gilles♦ May 12 '13 at 12:06
  • 1
    This is leading us somewhat astray, but Coq can allow you to write any function provably terminating in higher order arithmetic. This is certainly more than Peano arithmetic, and much, much, much higher than Ackerman for example. The proof is by a realizability argument, but in practice one may use well-founded recursion on a special datatype called WF I believe. – cody May 14 '13 at 21:07
up vote 3 down vote

For the reasons given by Gilles, there can't be a formal system that represents all total computations. If you had such a system, you'd have a system equivalent to all halting Turing machines. But the halting problem tells us that you can't decide if a machine halts or not, so you wouldn't be able to decide if an element (a Turing machine) belongs to the system or not.

However, you can get very close. Good formal models for this problem are (strongly) normalizing typed lambda calculi. This means that every term has a normal form - a definite result that you can obtain by a finite number of application of reduction rules. In other words, every computation has a result, every computation is total. The stronger system you have, the more total functions you can express in it (although you can never express all).

A nice example is System F, also known as the polymorphic lambda calculus. There is a theorem that says that

A function (on natural numbers) is expressible in System F if and only if it can be proved in the second order Peano arithmetic that the function is total.

This means that in System F you can express basically all imaginable total functions. So although you can't express all total function, you can express all total functions for which you can prove they're total, which is basically the best thing you can do.

There is a bit weaker system, Gödel's System T, for which there is a very similar theorem for first order Peano arithmetic. However this system is not as nice as System F. (In System F you can represent natural numbers, booleans etc. natively, while System T is constructed as the simply typed lambda calculus with externally added naturals and booleans. Also System F has type polymorphism, which makes it much more elegant in many cases.)

You can find all the details about these systems in Girard, Lafont and Taylor, Proofs and Types. Cambridge University Press, 1989, ISBN 0-521-37181-3.

Coq is based on a even stronger calculus of constructions, which is also strongly normalizing, so in Coq you can describe even more total functions.

share|cite|improve this answer

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.