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.
Asked By : jmite
Answered By : Gilles
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.)
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/11936
0 comments:
Post a Comment
Let us know your responses and feedback