13
$\begingroup$

I'm currently teaching a class on computability and recently covered the proof that the halting problem is undecidable. I know of three major proof avenues that can be used here:

  1. Diagonalization - show that if the halting problem were decidable, we could build a machine that, if run on itself, is forced to do the opposite of what it says it will do.
  2. Recursion theorem - show that if the halting problem were decidable, then we could build a machine that obtains its own description, determines whether it halts on its input, then does the opposite.
  3. Reduction - show that some other undecidable problem reduces to the halting problem.

While I completely understand these proofs and think that they're mathematically beautiful, many of my students are having trouble with them because none of the proofs directly address why you can't tell if a program will halt. Nothing in the above proceeds along the line of "computations can evolve in a way that is so complicated that we can't predict what will happen when we start them up" or "machines can't introspective on themselves at that level of detail." I often give these intuitions to my students when they ask why the result holds, but I'm not aware of any formal proofs of that form.

Are there any proofs of the undecidability of the halting problem that directly explore why it's impossible for a program to decide what another program will do?

Thanks!

  • 2
    I would venture the claim that diagonalization and recursion are fundamental aspects of the undecidability of the halting problem and that this is a bad idea. I sympathize with the urge to make things easier for students, but sometimes you can't just rely on what students already know; sometimes they have to absorb a genuinely new and important concept. Perhaps other examples of similar proofs might be valuable: http://terrytao.wordpress.com/2009/11/05/the-no-self-defeating-object-argument/2012-05-27
  • 3
    *Some* programs can decide what another program will do. Depends very much on how restricted the notion of "another program" is.2012-05-27
  • 1
    @Qiaochu Yuan- I absolutely agree that these are fundamental concepts; I heavily stress diagonalization throughout the course. My intent with a proof of this sort would be to offer it in addition to and not as a replacement for the existing proofs.2012-05-27
  • 0
    Perhaps something that has a more concrete feel, like Goodstein's Theorem, would be a useful thing to talk about.2012-05-27
  • 3
    These proofs show that the Halting problem for turing machines isnt solvable by turing machines. There is no proof that "directly address *why* you can't tell if a program will halt", because its not necessarily true. But you can argue for it with the church-turing thesis.2012-05-27
  • 5
    See [this question](http://cstheory.stackexchange.com/q/2853/1546) on cstheory.SE.2012-05-27

3 Answers 3