patternMinor
Halting problem - one issue that's bothering me
Viewed 0 times
problemissuehaltingbotheringonethat
Problem
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?
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?
Solution
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).
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).
Context
StackExchange Computer Science Q#49793, answer score: 6
Revisions (0)
No revisions yet.