24
$\begingroup$

It's fairly simple to understand why the halting problem is undecidable for impure programs (i.e., ones that have I/O and/or states dependent on the machine-global state); but intuitively, it seems that a pure program's halting on an ideal computer would be decidable through e.g. static analysis.

Is this in fact the case? If not, what are some counterexamples or papers disproving this claim?

$\endgroup$
  • 35
    $\begingroup$ Note that the standard proofs that the halting problem is undecidable (such as the one described on wikipedia: en.wikipedia.org/wiki/Halting_problem#Sketch_of_proof) all work with models of computation that do not even attempt to represent I/O. And while e.g. Turing Machines are stateful, their behaviour is formally defined in terms of pure functions. So in some sense "pure programs on an ideal computer" is actually the setting in which the halting problem is usually proved undecidable. $\endgroup$ – Ben Sep 13 '16 at 4:41
  • 1
    $\begingroup$ What research have you done? Googling "Halting problem" should have already answered this question for you. $\endgroup$ – Jonathan Cast Sep 14 '16 at 14:49
38
$\begingroup$

Here is a proof of undecidability by reduction from the Halting problem.

Reduction: Given a machine $M$ and an input $x$, build a new Turing Machine $H$ which does not read any input, but writes $M$ and $x$ on the tape and simulates $M$ on $x$ until $M$ halts.

The behaviour of this new machine $H$ is independent of the input tape, so it is a pure Turing Machine on which only static analysis is applicable. If static analysis were sufficient, then it could show whether $H$ halts, which would show whether $M$ halts on $x$, which would solve the halting problem for impure machines, which we know is undecidable, and therefore your problem is undecidable too.

$\endgroup$
16
$\begingroup$

No it is not, and moreover it does not depend on I/O.

Simple counterexample: write a program to find a perfect odd number (this is an open problem: we do not know yet whether one exists) - it does not take any input and does not perform any impure tasks; it may halt when it finds one, or may work infinitely (in the case such a number does not exist). Now if static analysis was powerful enough to determine the halting case it would be used to answer this (and many more questions) where halting would mean positive existence of such a number and not halting would mean there is no such number, but unfortunately static analysis is not that powerful.

$\endgroup$
  • 18
    $\begingroup$ I don't really see the point in this answer. Just because currently we don't know whether such a number exists doesn't imply that it doesn't, nor that we couldn't in the future write a static analyzer that is able to decide this. A better alternative is to use some known undecidable problem. For example it's known that there is no program that can solve all diophantine equations, and solving such an equation is a similar task to the one shown in the answer. $\endgroup$ – Bakuriu Sep 13 '16 at 6:22
  • 2
    $\begingroup$ Well, if the Halting problem was decidable, then every problem would be decidable if we can put it into a form where we ask if a program halts or not. Or any question of the form: There is a countable set, and I can decide if any individual potential element is in the set or not. Is the set empty? Diophantine equations have a countable set of potential solutions, and I can check if each individual potential solution is a solution or not. If the Halting problem was decidable, Diophantine equations would be decidable. $\endgroup$ – gnasher729 Sep 13 '16 at 8:06
  • 10
    $\begingroup$ @gnasher729 Yes, and since they are not the Halting problem is undecidable. That's my point. While the statement in this answer has no real implication: "Consider this mathematical definition. Currently we have no idea whether a program deciding this will stop or not, but tomorrow a guy could find out that it does or does not and this answer becomes 100% meaningless". $\endgroup$ – Bakuriu Sep 13 '16 at 8:37
  • 6
    $\begingroup$ Isn't this a similar case to How can it be decidable whether π has some sequence of digits?, the halting problem is undecidable on classes of problems, not single problems. $\endgroup$ – npostavs Sep 13 '16 at 14:50
2
$\begingroup$

The classical proof by diagonalization is a pure machine, not only it is a pure Turing Machine, but it does not rely on "Open Problems".

In example, a Turing machine that executes the Collatz Conjecture has unkown halting status, but that relies on our ignorance about the Collatz Conjecture, one day we might proove that Collatz was right and then we would became able to decide the Halting status of the conjecture (Either for some inputs does not halt, or Always halts).

So the Collatz Conjecture could already answer your question (Temporarily at least), but it relies on something we don't know. Instead the classical proof is a solved problem: we already know that's undecideable.

$\endgroup$
0
$\begingroup$

Just for the record, the standard proof of the undecideability of the halting problem relies on the same idea as quines: that it's possible to write a program some sub-term of which evaluates to the source code for the whole program. Then, if there was a function halts that, given source code for a program, returned True if that program halted on all input and False otherwise, this would be a legal program:

prog() = if halts "prog" then prog() else ()

where "prog" would be some expression that evaluated to the source code for prog; however, you can quickly see that prog halts (for all inputs) iff it doesn't halt, which is a contradiction. Nothing in this proof relies on I/O in any way (do you need I/O to write a quine?).

By the way, you might want to look in to "dialog-based I/O" for further evidence that I/O is entirely irrelevant to your problem (basically, programs that do I/O can be reduced to programs that take input as (explicit) functional arguments and return output as (explicit) additional results in a lazy language). Unfortunately, I can't find a reasonable, un-biased (or pro-dialog) page on the web right now.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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