9
$\begingroup$

To my knowledge, halting problem asks if there exists a program that decides whether a program being tested, given some input data (no matter what program it is, or what input data we give) will terminate or not. The answer to this problem is 'no'. In other words, there is no 'single' program that can verify it for all possible pairs (some algorithm, some input data).

But it doesn't mean we can't decide if particular program X will terminate or not.

I can't comment other answers yet, but one of them brought my attention:

In practical terms, it is important because it allows you to tell your ignorant bosses "what you're asking is mathematically impossible".

Maybe you can tell me what that person meant? In my scenario, my ignorant boss can ask me to verify (actually, prove or disprove) if my program (that's a particular program) will terminate or not. And of course there are pairs (algorithm, input data) that can be proven to terminate (or never terminate).

The question is - can I prove it for every such pair (program, input data) separately? Even if the answer is yes, then there's a problem - there can be infinitely many 'input data'. So it's quite natural to ask - can I prove, for every algorithm, that this algorithm will terminate (or the opposite), no matter what input data I provide?

Improve this question
$\endgroup$
3
  • $\begingroup$ Whether we can find all such proofs is an issue of logics, I guess, but there certainly are many we have not found yet. $\endgroup$
    – Raphael
    Commented Nov 21, 2015 at 20:26
  • $\begingroup$ the halting problem is defined as a specific algorithm which can determine if any program will halt or not. Checking a specific program (or even multiple specific programs) with different algorithms whether they can halt or not is doable (the general case isnt) $\endgroup$
    – Nikos M.
    Commented Nov 26, 2015 at 7:09
  • $\begingroup$ cs.stackexchange.com/q/152064/755 $\endgroup$
    – D.W. ♦
    Commented Jun 8, 2022 at 5:12

3 Answers 3

Reset to default
6
$\begingroup$

No, you cant prove this for every algorithm (Turing machine). This becomes a question about the nature of proofs rather than a question about computation.

Consider the following Turing machine $M(x)$: check if there exists a proof for the statement $\forall x \hspace{1mm} M(x)$ halts, of length $\le |x|$ (for explanation on the self reference, see Klenee's recursion theorem). If such proof is found, get into an infinite loop (otherwise halt).

Clearly you cant prove $M(x)$ halts for all $x$, since if you can find a proof of length $p$, it wont halt for all inputs of size $\ge p$. In addition, you cant prove $M(x)$ doesn't halt for some $x$, since this would mean there exists a proof for the halting of $M$ on all inputs (contradiction). The situation here is, that if our axiom system is consistent, then $M(x)$ halts for all $x$, but you cant prove it (meaning you can prove in your theory $T$ that if $T$ is consistent then $\forall x \hspace{1mm} M(x)$ halts, but you cant prove it halts without this assumption, unless your system is inconsistent).

Improve this answer
$\endgroup$
7
  • $\begingroup$ This is the answer to 'can I prove, for every algorithm, that this algorithm will terminate (or the opposite), no matter what input data I provide?' - just to make sure. $\endgroup$
    – user4205580
    Commented Nov 21, 2015 at 20:14
  • $\begingroup$ Yes. Need more characters $\endgroup$
    – Ariel
    Commented Nov 21, 2015 at 20:19
  • $\begingroup$ You might also be interested in Godel's incompleteness results: basically, in any logical system that's powerful enough to talk about arithmetic, there are statements which are true which cannot be proven. $\endgroup$
    – Joey Eremondi
    Commented Nov 21, 2015 at 20:25
  • $\begingroup$ $M$ - turing machine, $x$ - its input. Then we run it with, say, $x=2$. The program translates to: "check if there exists a proof for the statement: for all $2$ M(2) halts, of length $\le 2$..." It doesn't quite make sense to say for all $2$. Or maybe it's not the way I should look at it. $\endgroup$
    – user4205580
    Commented Nov 21, 2015 at 21:09
  • $\begingroup$ The quantified variable is new, think about it as $\forall y M(y)$ halts. $x$ (the input) only appears as the limit on the length of the proof. $\endgroup$
    – Ariel
    Commented Nov 21, 2015 at 21:12
2
$\begingroup$

For one specific program, sure I can prove that the program will halt on all inputs: my program has "halt" as its first instruction.

Another example: I can have a specific program that is a Turing machine simulator (i.e. a universal Turing machine). It interprets its input as a description of a Turing machine, and the simulator simulates the machine running on a blank tape. So the simulator will stop if the machine being input stops, and will run for ever if the machine being input runs for ever. (If the input is not in the correct format to describe a Turing machine, the simulator stops.)

We know it is impossible to decide whether an arbitrary Turing machine halts when started on a blank tape. So for my specific simulator machine, there is no algorithm to decide what it does on arbitrary input.

I don't know if these two examples help.

Surely in many problem domains it is reasonable to be able to prove that specific programs terminate. If my program multiplies two matrices I would expect to be able to prove that there is no way it can go on for ever.

Improve this answer
$\endgroup$
2
$\begingroup$

I can at least clarify the hypothetical question the imaginary boss is presumed to ask which lead to this answer:

Can you design a program that takes this other program/template/database query/ etc. which always determines whether it terminates/raises an exception/runs out of memory?

The point of the impossibility proof is that such a task cannot be accomplished. Of course it's common knowledge today that such a task can be approximated quite well, i.e. it is possible to give an algorithm that determines whether a program is going to raise an exception, but sometimes answers "might raise an exception" even though the program doesn't do it in practice.

Some of these are harder to do in practice as well, e.g. termination is quite harder to prove than the absence of null pointer exception for "real world programs" (but equivalent in theory).

Improve this answer
$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.