3
$\begingroup$

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?

$\endgroup$
26
  • 3
    $\begingroup$ 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. $\endgroup$
    – Thomas Andrews
    May 28, 2011 at 19:55
  • $\begingroup$ @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. $\endgroup$
    – Vag
    May 28, 2011 at 20:08
  • $\begingroup$ I'm enumerating them until termination or nontermination proof will be found. $\endgroup$
    – Vag
    May 28, 2011 at 20:14
  • 1
    $\begingroup$ 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. $\endgroup$
    – Thomas Andrews
    May 28, 2011 at 20:24
  • $\begingroup$ @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. $\endgroup$
    – Vag
    May 28, 2011 at 20:36

2 Answers 2

Reset to default
3
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$
    – Vag
    May 29, 2011 at 8:28
  • $\begingroup$ 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? $\endgroup$
    – Raphael
    May 29, 2011 at 11:17
  • $\begingroup$ @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? $\endgroup$
    – Vag
    May 29, 2011 at 13:16
  • $\begingroup$ @Raphael: And, to support you impressions, can you give exact citation of my words to show that I've missed something from the basics? $\endgroup$
    – Vag
    May 29, 2011 at 13:18
  • $\begingroup$ 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. $\endgroup$
    – Raphael
    May 29, 2011 at 18:31
2
$\begingroup$

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

$\endgroup$
11
  • $\begingroup$ I'm talking about programs in Turing Complete languages, not LBA-equivalent, see update. $\endgroup$
    – Vag
    May 28, 2011 at 19:34
  • $\begingroup$ 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? $\endgroup$
    – Raphael
    May 29, 2011 at 11:20
  • $\begingroup$ @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. $\endgroup$
    – Vag
    May 29, 2011 at 13:26
  • $\begingroup$ 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. $\endgroup$
    – Raphael
    May 29, 2011 at 18:33
  • 1
    $\begingroup$ @Vag, if you want to be pedantic every real-world algorithm runs on a linear bounded automaton. This is immediate because there exists a finite amount of storage in the universe. $\endgroup$
    – JSchlather
    May 30, 2011 at 21:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .