Is there an always-halting, limited model of computation accepting $R$ but not $RE$?

Question

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.

Answer 1

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

Answer 2

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.