1

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

Cœur
  • 37,241
  • 25
  • 195
  • 267
Larry
  • 858
  • 10
  • 16
  • possible duplicate of [What exactly is the halting problem?](http://stackoverflow.com/questions/1111155/what-exactly-is-the-halting-problem) – cjhveal Jul 28 '15 at 18:52
  • I think halting problem has the input specified, but here I want to prove the existence of such input is undecidable. Of course, I may describe an algorithm that tries all possible inputs and argues that for all inputs whether program p halts is undecidable, thus my question is undecidable. But I do not think that's a formal proof. What do u think? – Larry Jul 28 '15 at 19:03
  • You might have better luck on the [theoretical computer science stack exchange](http://cs.stackexchange.com/). – cjhveal Jul 28 '15 at 19:10

1 Answers1

2

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.

lodrik
  • 472
  • 4
  • 8
  • Sorry for the late reply. I had a final exam this week and couldn't reply you in time. Your solution is brilliant. I didn't think I could reduce the question to the halting problem. May I ask how you came up with the thoughts ; ) Anyways, thank you very much. I understand the problem now! – Larry Aug 01 '15 at 01:07
  • But there are some programs that can be proven to halt, using [termination analysis](https://en.wikipedia.org/wiki/Termination_analysis). – Anderson Green Nov 30 '18 at 04:05