Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Halting Problem is (theoretically) decidable for such algorithms which termination may be proved in First Order Logic (FOL) because all true statements in FOL are recursively enumerable. It is correct?

I'm talking about programs in Turing-complete languages and use "realworldiness" property not in the sense of finiteness but in the sense of "be designed to some real purpose" and "be not specially cooked to require HOL for termination proof" (that allows potentially to require unprovable statements for termination proof).

As for argument that FOL is adequate for working with ordinary programs is a fact that there are plenty systems designed for industrial application for proving program properties that use only FOL (TLA+, for example).

To be precise, let set of real world programs be all programs that humans write for their utility for entire human history to the end of times.

Perhaps I must say even more precise: Can such property be existing that limits Turing-complete language in such way that termination of any program in language with that property can be proved in FOL but no programmer will be disturbed by that limitation?

And interesting satellite question: is absolutely minimal restriction of Turing-complete languages possible such that Halting Problem become decidable for restricted languages?

share|improve this question
3  
This is a fairly confused question. The set of programs that halt is already recursively enumerable, without needing proofs. The problem is that the set of non-halting programs is not recursively enumerable. You can definitely enumerate all the programs for which a proof exists that the program halts, yes. It would also be really helpful if you could define more clearly what you mean by "real world" examples. –  Thomas Andrews May 28 '11 at 19:55
    
@Thomas Andrews: I'm enumerating FOL theorems, not programs; I'm enumerating them until termination proof for given program will be found. What about "real world", I've add update. –  Vag May 28 '11 at 20:08
    
I'm enumerating them until termination or nontermination proof will be found. –  Vag May 28 '11 at 20:14
1  
Well, no program that any person ever writes is ever in a Turing complete language, since it only runs in machines that have finite memory. That said, a simple program that a person might want to write is to search for a proof of a theorem. If you could solve the halting problem, then the set of provable and disprovable theorems would be a recursive set, which it is not. –  Thomas Andrews May 28 '11 at 20:24
    
@Thomas Andrews: "Well, no program that any person ever writes is ever in a Turing complete language, since it only runs in machines that have finite memory". It is incorrect because you confused language and its implementation. Implementation is finite, language is Turing-complete. –  Vag May 28 '11 at 20:36
show 21 more comments

2 Answers

FO logic (to be precise, FO[<]) can express no more than star-free languages (McNaughton, Papert, 1971), a proper subset of regular languages. Therefore, I think any hope that FOL is sufficient to express all desired properties programs might have is misguided.

You have to be precise about what the Halting Problem really is and what its undecidability really implies: There can be no algorithm which uniformly decides for any input and any program wether it holds or not.

That does not mean that you can not decide termination for some program, or for (large) sets of programs. In fact, people do that, as exhibited by a recent article in Communications of the ACM.

share|improve this answer
    
Your first paragraph is interesting and informative (could you add some references please?), second and third are not useful -- they do not say anything new to me and do not shed light to the question. I ofter repeat the like to others myself. –  Vag May 29 '11 at 8:28
    
I do not know the precise reference, but I edited in what was given in lecture. As for the rest, I am unsure what your background is and how much you understand of TCS basics. Your profile says "programmer" and from the spread and kind of questions you have posted here recently (and the way you respond to answers), I get the impression that you went straight to "interesting" problems without bothering to study the basics. Maybe you would be better off taking up a book (e.g. Hopcroft & Ullman), catch up and revisit those questions then? –  Raphael May 29 '11 at 11:17
    
@Raphael: If my questions are so basic why just not cite answer from textbook of give a reference to specific paragraph in some textbook where the answer resides? –  Vag May 29 '11 at 13:16
    
@Raphael: And, to support you impressions, can you give exact citation of my words to show that I've missed something from the basics? –  Vag May 29 '11 at 13:18
    
The questions you state are not basic. As for your knowledge, I probably cannot cite anything particular. It is just that, as a three times TA of a basic TCS class, the kind of questions you ask in the comments and the way you argue screams "does not know what he is talking about!". I may be wrong; but my guess is you never took and passed a TCS course or read and understood a book like H&U. If I am right, you really should do so because you won't recognise correct (partial) answers anyway. If not, my bad. –  Raphael May 29 '11 at 18:31
show 1 more comment

The Halting Problem is solvable for linear bounded automaton, here is a reference.

A linear bounded automaton is a turing machine that has one tape of fixed size that the input is read in on and all computation is performed on it. The basic idea of the algorithm is that since there are only a finite amount of states, all states can be checked to see if they lead to termination. It is very much though a galactic algorithm with a horrible complexity.

On most "real-world" problems there are simpler programs that just look for common mistakes, such as forgotten conditions leading to infinite errors. Of course if you wrote a program looking trying to find a solution to Fermat's Last Theorem's Equation, it would probably say that it will halt (and depending on how much precision you've allowed it just might!).

share|improve this answer
    
I'm talking about programs in Turing Complete languages, not LBA-equivalent, see update. –  Vag May 28 '11 at 19:34
    
You were given an infinitely big class of problems (namely LBA-solvable ones) for which the Halting Problem can be solved. What more do you want? –  Raphael May 29 '11 at 11:20
    
@Raphael: There are lot of classic algorithms that use more intermediate storage than length of the input. It implies that LBA is not the case. –  Vag May 29 '11 at 13:26
    
So you are looking for an exact characterisation of the class of algorithms for which the halting problem can be solved? I do not know one exists, other than this one. Anyway, you question as I understand it does ask for classes for which the HP can be solved, and Jacob gave you one. –  Raphael May 29 '11 at 18:33
    
"So you are looking for an exact characterisation of the class of algorithms for which the halting problem can be solved?" Yes, well stated satellite question! "and Jacob gave you one" and it does not fit because it is too narrow: there are lot of "real world" algorithm out of it (for example, nfa2dfa). –  Vag May 30 '11 at 8:49
show 6 more comments

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.