26
$\begingroup$

"Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist"

Can I find a general algorithm to solve the halting problem for some possible program input pairs?

Can I find a programming language (or languages), where I for every kind of program in this language, it can decide if the program terminates or run forever?

Improve this question
$\endgroup$
3
  • $\begingroup$ Similar question: stackoverflow.com/questions/8412741/… $\endgroup$
    – SK-logic
    Commented Dec 8, 2011 at 18:12
  • 3
    $\begingroup$ CACM had a very interesting article in May: Proving Program Termination $\endgroup$
    – Christoph Walesch
    Commented Dec 10, 2011 at 18:33
  • 3
    $\begingroup$ "a general algorithm [...] for some possible program input pairs" -- that's close to being self-contradicting. I guess you want to restrict yourself to an infinite subclass of all programs? $\endgroup$
    – Raphael
    Commented Oct 4, 2012 at 9:44

6 Answers 6

Reset to default
27
$\begingroup$

Can I find a general algorithm to solve the halting problem for some possible program input pairs?

Yes, sure. For example you could write an algorithm that returns "Yes, it terminates" for any program which contains neither loops nor recursion and "No, it does not terminate" for any program that contains a while(true) loop that will definitely be reached and doesn't contain a break statement, and "Dunno" for everything else.

Can I find a programming language (or languages), where I for every kind of program in this language, it can decide if the program terminates or run forever?

Not if that language is Turing-complete, no.

However there are non-Turing complete languages like for example Coq, Agda or Microsoft Dafny for which the Halting Problem is decidable (and in fact is decided by their respective type systems, making them total languages (i.e. a program that might not terminate will not compile)).

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ The class of primitive-recursive functions is a well-known "programming language" for which the halting problem is trivially decidable. $\endgroup$
    – Raphael
    Commented Oct 4, 2012 at 9:49
  • $\begingroup$ There are several "total functional programming" languages in which all programs are provably terminating. $\endgroup$
    – Anderson Green
    Commented Dec 31, 2018 at 6:28
3
$\begingroup$

I think all the answers here completely and utterly miss the point. The answer to the question is: assuming the program is intended to halt, then yes you had better be able to show it stops. If you cannot show it stops easily then the program should be considered very badly written and rejected by Quality Control as such.

Whether you can actually write a suitable machine algorithm depends on the input programming language and how ambitious you are. It is a reasonable design goal for a programming language to make it easily possible to prove termination.

If the language is C++ you probably can't write the tool, indeed it is unlikely you'd ever get the parser going, let alone prove termination. For a better structured language, you should at be able to generate a proof, or at least do so with certain assumptions: in the latter case the tool should output these assumptions. A similar approach would be to include termination assertions in the language and use them in complex situations where the tool would trust the assertions.

The bottom line is that no one seems to understand that proof a program halts is indeed possible because (good) programmers intending to write such halting programs always do so intentionally and with a mental picture of why they terminate and act correctly: such code is deliberately written so it is clear that they halt and are correct and if a reasonable algorithm cannot prove this, possibly with some hints, then the program should be rejected.

The point: programmers don't write arbitrary programs, so the thesis of the halting theorem isn't satisfied and the conclusion doesn't apply.

Improve this answer
$\endgroup$
10
  • 4
    $\begingroup$ I think it's you who completely and utterly missed the point. The first paragraph of your answer doesn't apply to the question because it's asking about algorithms - not what a human can or can't proof. The rest of the answer answers the first paragraph of the question, i.e. whether an algorithm could proof termination for some programs. Everyone of the previous answers already said "yes" to that one. $\endgroup$
    – sepp2k
    Commented Jul 20, 2012 at 1:53
  • 3
    $\begingroup$ Your assertion that is possible to write an algorithm that can proof termination of every well-written program in a sufficiently simple Turing-complete language is just completely false. For every possible algorithm that tries to proof termination, there are problems where every program that solves that problem can't be proven to halt by that algorithm. So unless you're saying that every program solving that problem is badly written by definition (which would be ludicrous), that disproves your point. $\endgroup$
    – sepp2k
    Commented Jul 20, 2012 at 1:55
  • 1
    $\begingroup$ @Sam If someone asks me whether some code halts, I'll look at the code and try to figure it out. But I'm not an algorithm. And yes, it's possible to write an algorithm that can check whether a program halts for a lot of programs. But that's not what Yttrill said. Yttrill said it's possible for all well-written programs. And as I said in my previous comment, that is simply false unless you claim that certain problems can only be solved by badly written programs (which again would be ludicrous). $\endgroup$
    – sepp2k
    Commented Oct 3, 2012 at 19:34
  • 1
    $\begingroup$ @Sam "it seems straightforward to me that programs intentionally written to halt can be easily analyzed for halting conditions" -- if that were the case, why don't we have such tools? It's not as if people were not trying. (One culprit is method overriding: at compile time, you don't know all code that will be executed.) $\endgroup$
    – Raphael
    Commented Oct 5, 2012 at 9:39
  • 1
    $\begingroup$ @Sam "is there an infinite loop" is a hard thing to approach, even for real-world loop. Of course I was taught how to find loop-invariants, but that does not mean I can find one (easily) in many cases. As far as I know, guess & prove is the gold-standard these days. Again, if there were reasonably general algorithms, I would expect them to be included in major compiles or IDEs (which do perform some trivial, syntactical checks). Can you give a reference to a reasonably strong algorithm? $\endgroup$
    – Raphael
    Commented Oct 5, 2012 at 19:41
3
$\begingroup$

excellent and (prob unintentionally deep) question. there are indeed halting-detecting programs that can succeed on limited sets of inputs. its an active area of research. it has very strong ties to (automated) theorem proving areas.

however computer science does not appear to have an exact term for "programs" that "sometimes" succeed. the word "algorithm" is usually reserved for programs that always halt.

the concept seems to be distinctly different than probabilistic algorithms where CS theorists insist there be some known or computable probability on their succeeding.

there is a term semialgorithms that is used sometimes but its apparently a synonym for recursively enumerable or noncomputable.

so for purposes here, call them quasialgorithms. the concept is different than decidable vs undecidable.

one might say that one cannot compare quasialgorithms. but in fact there seems to be a natural hierarchy (a partial ordering) of these quasialgorithms. suppose a quasialgorithm $A$ can detect halting of some limited set of input programs say $X$. another one $B$ can detect halting of a set $Y$. if $X \subset Y$ ie $X$ is proper subset of $Y$ then $B$ is "more powerful" than $A$.

in CS this "quasi algorithm hierarchy" seems to be studied mostly only informally so far.

it shows up in busy beaver research[1] and the PCP problem[2]. in fact a DNA based computing attack on PCP can be seen as a quasialgorithm.[3] and its seen in other areas already noted such as theorem proving[4].

[1] New millenium attack on the busy beaver problem

[2] Tackling Posts correspondence problem by Zhao (v2?)

[3] Using DNA to solve the Bounded Post Correspondence Problem by Kari et al

[4] proving program termination by Cook et al, Comm. of the ACM

(so this is actually a very deep question that defn deserves to be on TCS.SE imho... maybe someone can re-ask it there in a way such that it fits & stays)

Improve this answer
$\endgroup$
6
  • $\begingroup$ ps as an impressive example of how powerful the quasialgorithms can be, the ACM ref pts out that ackermanns function can be proven to halt by a quasialgorithm, but it is larger than (not computable by) all primitive recursive functions. $\endgroup$
    – vzn
    Commented Oct 4, 2012 at 1:04
  • 1
    $\begingroup$ "the word "algorithm" is usually reserved for programs that always halt." -- I am not sure that is true. There are plenty of partially terminating algorithms around (esp. in verification) and I have never heard anybody not say "algorithm". $\endgroup$
    – Raphael
    Commented Oct 4, 2012 at 9:55
  • $\begingroup$ there are informal uses of "algorithm". "partially terminating" is ok but prob nonstd. as stated, there does not seem to be stdized term yet. wikipedia defines an algorithm as an effective method ie decidable with following characteristics (1) always give some answer rather than ever give no answer; (2) always give the right answer and never give a wrong answer; (3) always be completed in a finite number of steps, rather than in an infinite number; (4) work for all instances of problems of the class. $\endgroup$
    – vzn
    Commented Oct 4, 2012 at 14:55
  • $\begingroup$ and then later in the same article it says "A further elucidation of the term "effective method" may include the requirement that, when given a problem from outside the class for which the method is effective, the method may halt or loop forever without halting, but must not return a result as if it were the answer to the problem." ie it nearly contradicts itself !?! so clearly, remarkably, there is some real confusion on the key issue and existing terminology is not strict. note the word "algorithm" is close to more than a millenia old or so & has shifted substantially.... $\endgroup$
    – vzn
    Commented Oct 4, 2012 at 15:21
  • $\begingroup$ It's true: the traditional meaning is probably "effective method" in the way Wikipedia says (there is no contradiction in the sentence you quote; it's a bit unclear, though) -- people did not conceive functions/algorithms that did not terminate (for some inputs). I think this has shifted since the 1950s; as I said, today people clearly call a partially terminating method "algorithm". $\endgroup$
    – Raphael
    Commented Oct 4, 2012 at 22:32
2
$\begingroup$

As long as the programming language in question is sufficiently complex (i.e. if it is Turing complete), then there are always programs in the language which no program can prove to terminate.

Since all but the most primitive languages are Turing complete (it only takes something like variables and conditionals), you could really only build very small toy languages for which you could solve the halting problem.

Edit: In light of the comments, let me be more explicit: Any language that you might design for which you could solve the halting problem would necessarily have to be Turing-incomplete. This rules out any language that contains a suitable set of basic ingredients (e.g. "variables, conditionals and jumps", or as @sepp2k says, a generic "while"-loop).

Apparently there exist several practical "simple" languages like that (e.g. theorem solvers such as Coq and Agda). If those satisfy your notion of a "programming language", you might investigate whether they satisfy some sort of completeness, or whether the halting problem is solvable for them.

Improve this answer
$\endgroup$
5
  • 3
    $\begingroup$ "Since all but the most primitive languages are Turing complete (it only takes something like variables and conditionals)" That's not true. First of all you'd at the very least would need recursion or some form of looping construct (which should be as powerful as a while-loop - a simple counting loop is not enough). Second of all I don't think there are a lot of people who would call languages like Coq or Agda (which are total and thus not turing complete) primitive or toy languages. $\endgroup$
    – sepp2k
    Commented Dec 8, 2011 at 18:04
  • $\begingroup$ @sepp2k: Well, yes. Peano arithmetic is also quite useful and not Turing complete. A simplified statement, I suppose. If the OP is sufficiently familiar with the problem, she will hopefully be able to fill in the technical details. $\endgroup$
    – Kerrek SB
    Commented Dec 8, 2011 at 18:07
  • 3
    $\begingroup$ There is a huge gap between being "sufficiently complex" and being Turing-complete. Coq is complex indeed, and it is suitable for a very wide range of practical tasks. $\endgroup$
    – SK-logic
    Commented Dec 8, 2011 at 18:14
  • 1
    $\begingroup$ @Kerrek SB Well it is possible that Turing-complete language is used in ways which remain provable to termination. If you can prove that a recursive formula always approachs its terminating condition (like the factorial function) you could prove it terminates even though you wouldn't be able to handle every type of recursion. $\endgroup$
    – ArtB
    Commented Dec 8, 2011 at 20:44
  • $\begingroup$ @ArtB: Sure, there are always some programs that can be proven to terminate. The OP's first question might hint at that, though I'm not sure I follow it fully. For instance, you couldn't have a "generic algorithm" that determines if any given family of programs terminates, while conversely you could probably construct a restricted family of functions such that assuming a function belongs to that family, you could tell algorithmically whether it terminates. (I'm not sure whether that family can be non-trivial, though. I guess it can, but I can't make an example.) $\endgroup$
    – Kerrek SB
    Commented Dec 8, 2011 at 21:08
2
$\begingroup$

Consider some formal theory $T$. Consider TMs augmented with proofs in $T$ that they halt/do not halt. Then we can decide whether a given TM-proof pair is halting by verifying the proof. (The examples given in sepp2k's answer are special cases).

This is quite trivial. If we take the union of any c.e. subset of halting TMs and any c.e. subset of non-halting TMs, the result will be set of TMs for which the halting problem is decidable (run both machines in parallel, if the first one accept the TM halts, if the second one accepts then the machine does not halt). However this will not lead to much interesting languages.

The reason is simple: in practice, we usually don't care if a program halts on one particular input but when if it halts on set of inputs, and in that case we have a universal quantifier which cannot be verified as soon as programs are expressive enough. How expressive? A very small amount of expressiveness is sufficient (e.g. $\mathsf{ALogTime}$). As soon as the programs are powerful enough to express if a given string $c$ is a halting computation of a Turing machine $M$ on a blank input (a completely syntactic problem that can be solved quite easily) then the halting problem for those programs becomes undecidable.

Improve this answer
$\endgroup$
1
$\begingroup$

Yes you can, but I doubt it will be useful. You'd probably have to do it be case analysis and then you'd only be able to look for the most obvious cases. For example, you could grep a file for the code while(true){}. If the file has that code it will never terminate^. More generally you could say that a program with no loop or recursion will always terminate and there are several cases you could do that could guarantee that a program will or will not terminate, but for even a mid-size program this would be very difficult and in many cases would not be able to give you an answer.

tl;dr: Yes, but you won't be able to have it be useful for most useful programs.

^ Yes, technically if that code is not on the code-path or there are other threads it could still terminate, but I'm making a general point here.

Improve this answer
$\endgroup$
6
  • 4
    $\begingroup$ Why do you think Coq and Agda are not useful? You're overestimating the value of Turing-completeness. $\endgroup$
    – SK-logic
    Commented Dec 8, 2011 at 18:16
  • $\begingroup$ I've used Coq, but my claim remains since most commercial software is written in Java/C++/Ruby/C# for which my claims are true. The kind of programs 90% of people are interested in writing would not benefit. Basically, if you don't know of Coq/Agda etc you aren't the target market for it. $\endgroup$
    – ArtB
    Commented Dec 8, 2011 at 18:24
  • 5
    $\begingroup$ I'd say 99% of the real world programs would benefit from being implemented in a non-Turing-complete subset of a language. You won't implement, say, Ackermann function every day. 100% of CRUD does not need a "real" language. Data processing is almost always trivial. See the Terminator project - they're even serving a decent subset of possible C++ programms, which is more than enough for the real world stuff (including drivers and other low level code). $\endgroup$
    – SK-logic
    Commented Dec 8, 2011 at 18:54
  • $\begingroup$ Most real world projects want to reuse libraries that are written Turing-complete languages and use their IDEs and debuggers and tutorials. Yes, you could accomplish things in non-Turing languages, but I can't imagine some actually saying "I want to do X" and my answer being "Use Coq". ps- thanks for introducing me to The Terminator Project. $\endgroup$
    – ArtB
    Commented Dec 8, 2011 at 20:39
  • 4
    $\begingroup$ an unimaginably huge proportion of the business logic is implemented in a non-Turing-complete SQL already. And DSLs and eDSLs are on a rise now. So, soon most of the business apps programmers will forget about all the "general purpose" languages. $\endgroup$
    – SK-logic
    Commented Dec 8, 2011 at 20:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.