Search code examples
logiccomputer-sciencehalting-problemcomputability

Can a program decide whether an arbitrary program halts for SOME input?

Is there a program (may-halt? p) that can tell whether there exists an input so that (p input) halts?

I tried simple diagonalization, but it only tells me that (may-halt? diag-may-halt) must be true. It doesn't help proving whether the program exists or not.

Does such a program exist?

My diagonalization

Solution

  • Nope, may-halt? doesn't exist.

    (I don't think a direct proof by diagonalization would be less complex than the proof that the Halting problem is undecidable; otherwise that would be the standard example. Instead, let's reduce your problem to the Halting problem:)

    Suppose there was a program may-halt? p, that decides if program p halts for some input. Then define:

    halt? p x := may-halt? (\y -> if y==x then p x else ⊥)

    where the thing in braces is a derived program. Lets break it down: 

    halt? p x := may-halt? p'

    where p' is the program that (i) on input x computes p x, (ii) on any other input just loops around without terminating:

    p' y := if y==x then p x else ⊥

    Then may-halt? p' outputs true if and only if p x terminates.

    Thus, for any program p and input x, halt? p x would decide if p x terminates. But we know that that isn't possible, so may-halt? doesn't exist.