How does this proof, that the halting problem is undecidable, work?
Asked Answered
B

2

19

I'm going over the proof for The Halting Problem in Intro to the Theory of Computation by Sipser and my main concern is about the proof below:

If TM M doesn't know when it's looping (it can't accept or reject which is why a TM is Turing Recognizable for all strings), then how would could the decider H decide if M could possibly be in a loop? The same problem will carry through when TM D does its processing.

the halting problem is undecideable

Barbiturism answered 6/12, 2011 at 1:59 Comment(8)
The proof is straight-forward; what I don't understand is your question. Are you happy with the concept of a proof by contradiction?Phosphoroscope
Kay, that's not correct: copying one page from an entire text, for purposes of commentary, is certainly fair use.Overjoy
As a community moderator, I don't have the authority to judge whether or not this constitutes a copyright violation. All copyright violations should be reported to Stack Exchange, Inc. in the form of a DMCA takedown notice from a copyright holder.Sluff
@MichaelHoffman No. Theoretical Computer Science is for research-level theoretical computer science, as indicated in its FAQ. Explaining a proof in a textbook is not a research-level question. Officially, computer science questions are on-topic on Stack Overflow, though there is a proposed computer science site that would give them a better home.Basutoland
Ok, first off: this is on-topic. Second: pasting a scan of a textbook page is decidedly uncool - I don't care whether or not it's a copyright violation or not, but come on... If you expect us to read it, at least have the grace to quote or paraphrase the relevant portion as actual bonafide text. Finally: we're not here to do your homework for you. For pity's sake, dude... Show your work! What do you think?!Egghead
@Egghead the question is about the specifics of the proof offered. Paraphrasing would very likely mask the question, and since OP is clearly new at this whole proof thing, might simply make the question incomprehensible. This seems like the perfect way to ensure that we're able to see what OP is asking.Overjoy
@CharlieMartin - that's understandable, but... it also reminds me of the folks who post screenshots of their editor because they can't figure out Markdown formatting. A clever solution no doubt, but not terribly friendly to readers who might actually want to copy, quote, or even... search.Egghead
@Shog9, I understand, but in this particular case, esp. since reproducing the mathematical notation w/in markdown would be an interesting problem in itself, I think this is the right choice.Overjoy
O
19

This is a "proof by contradiction", a reductio ad absurdum. (Latin phrases are always good in theory classes... as long as they make sense, of course.)

This program H is just a program with two inputs: a string representing a program for some machine, and an input. For purposes of the proof, you simply assume the program H is correct: it simply will halt and accept if M accepts with w. You don't need to think about how it would do that; in fact, we're about to prove it can't, that no such program H can exist, ...

BECAUSE

if such a program existed, we could immediately construct another program H' that H couldn't decide. But, by the assumption, there is no such program: H can decide everything. So, we're forced to conclude that no program defined as we defined H is possible.

By the way, the reductio method of proof is more controversial than you might expect, considering how often its used, especially in Computer Science. You shouldn't be embarrassed to find it a little odd. The magic term is "non-constructive" and if you feel really ambitious, ask one of your professors about Errett Bishop's critique of non-constructive mathematics.

Overjoy answered 6/12, 2011 at 2:16 Comment(7)
I'm a little perplexed by your assertion that proofs by contradiction are controversial. They're quite commonplace in mathematics, and are completely logically sound. This isn't really the forum for a discussion, but the way you've written it seems dangerous: it could lead an inexperienced reader to conclude that there might be something wrong with results proved by contradiction. From very quick reading, it sounds like the "controversy" is about whether proofs by contradiction are elegant and good for teaching, and also like Bishop was possibly criticizing other things as well.Paquin
@Jefromi No, the controversy is not about teaching, it is about the foundations of mathematics. If you're curious, the place to start would be intuitionism, though the WP article is hardly enlightnening. I'd say the controversy is a bit dated; all these logics can be used to build one another anyway. Intuitionistic logic has in a sense made a comeback as a practical tool to model computer-assisted proofs.Basutoland
@Gilles: Okay. My quick reading was perhaps too quick, then. But I stand by my argument that one should be careful suggesting that proof by contradiction is a controversial idea in the context of mathematics. As you say, the controversy is dated, and doesn't affect validity of proofs.Paquin
@Jefromi, I said "more controversial than you might think." Now, I'm a logician of sorts and interested in foundational stuff, so I pay more attention to it than some, but the point was that it's not actually unreasonable to wonder if reductio proofs are quite legit. To a beginner, they do smack of circularity.Overjoy
@Giles, I'm not really comfortable with identifying constructivism with intuitionism; intuitionism is rather a subset of constructivism. I'd instead take it as based on rejection of the Law of Excluded Middle. Another interesting view is in computable analysis; I'm very fond of it because, when an undergrad, I decided the whole discontinuity thing was silly and made an attempt at inventing computerable analysis independently. It wasn't successful, but it was fun to see it show up years later.Overjoy
@CharlieMartin This is NOT a proof by contradiction! It's simply a proof of a negation. Note that "undecidable" means "not decidable", and "not X" means "X is contradictory"; indeed, the proof starts with "We assume that A_TM is decidable and derive a contradiction". Andrej Bauer has a nice discussion of the distinction between proof by contradiction and proof of negation; he wrote the post in response to a Field's medalist, so confusing the two is nothing to be ashamed of.Sirajuddaula
Or else distinguishing the two is arrant pedantry.Overjoy
I
28

After reading this and trying to visualize the proof I came up with this code which is a simplified version of the code in this answer to a related question:

function halts(func) {
  // Insert code here that returns "true" if "func" halts and "false" otherwise.
}

function deceiver() {
  if(halts(deceiver))
    while(true) { }
}

If halts(deceiver) returns true, deceiver will run forever, and if it returns false, deceiver will halt, which contradicts the definition of halts. Hence, the function halts is impossible.

Infra answered 27/11, 2013 at 1:50 Comment(6)
+1 Very elegant and as far as I can tell (as a programmer and not a computer scientist), it is a correct illustration of why the halting problem is undecidable, even for programs that take no input.Han
I don't think it's a correct answer, since you cannot do things like invoking halts like halts(deceiver). You should invoke it with a specific code, like the one shown in Wikipedia.Pediment
@FrankScience In fact, the recursion theorem guarantees the existence of a function with these semantics.Detrude
@YuvalFilmus I don't know that theorem. After skimming the wiki page, it seems to me that the proof of the original halting problem just uses the same trick as Y-combinator does, but it uses the condition of existence of input data.Pediment
@Gudradain, there is no recursion here. In the "halts" call just the function "deceiver" is passed as a parameter, but it's not calledKorey
This is a good enough demonstration, although it's not accurate to the Turing machine formulation of the problem.Piccadilly
O
19

This is a "proof by contradiction", a reductio ad absurdum. (Latin phrases are always good in theory classes... as long as they make sense, of course.)

This program H is just a program with two inputs: a string representing a program for some machine, and an input. For purposes of the proof, you simply assume the program H is correct: it simply will halt and accept if M accepts with w. You don't need to think about how it would do that; in fact, we're about to prove it can't, that no such program H can exist, ...

BECAUSE

if such a program existed, we could immediately construct another program H' that H couldn't decide. But, by the assumption, there is no such program: H can decide everything. So, we're forced to conclude that no program defined as we defined H is possible.

By the way, the reductio method of proof is more controversial than you might expect, considering how often its used, especially in Computer Science. You shouldn't be embarrassed to find it a little odd. The magic term is "non-constructive" and if you feel really ambitious, ask one of your professors about Errett Bishop's critique of non-constructive mathematics.

Overjoy answered 6/12, 2011 at 2:16 Comment(7)
I'm a little perplexed by your assertion that proofs by contradiction are controversial. They're quite commonplace in mathematics, and are completely logically sound. This isn't really the forum for a discussion, but the way you've written it seems dangerous: it could lead an inexperienced reader to conclude that there might be something wrong with results proved by contradiction. From very quick reading, it sounds like the "controversy" is about whether proofs by contradiction are elegant and good for teaching, and also like Bishop was possibly criticizing other things as well.Paquin
@Jefromi No, the controversy is not about teaching, it is about the foundations of mathematics. If you're curious, the place to start would be intuitionism, though the WP article is hardly enlightnening. I'd say the controversy is a bit dated; all these logics can be used to build one another anyway. Intuitionistic logic has in a sense made a comeback as a practical tool to model computer-assisted proofs.Basutoland
@Gilles: Okay. My quick reading was perhaps too quick, then. But I stand by my argument that one should be careful suggesting that proof by contradiction is a controversial idea in the context of mathematics. As you say, the controversy is dated, and doesn't affect validity of proofs.Paquin
@Jefromi, I said "more controversial than you might think." Now, I'm a logician of sorts and interested in foundational stuff, so I pay more attention to it than some, but the point was that it's not actually unreasonable to wonder if reductio proofs are quite legit. To a beginner, they do smack of circularity.Overjoy
@Giles, I'm not really comfortable with identifying constructivism with intuitionism; intuitionism is rather a subset of constructivism. I'd instead take it as based on rejection of the Law of Excluded Middle. Another interesting view is in computable analysis; I'm very fond of it because, when an undergrad, I decided the whole discontinuity thing was silly and made an attempt at inventing computerable analysis independently. It wasn't successful, but it was fun to see it show up years later.Overjoy
@CharlieMartin This is NOT a proof by contradiction! It's simply a proof of a negation. Note that "undecidable" means "not decidable", and "not X" means "X is contradictory"; indeed, the proof starts with "We assume that A_TM is decidable and derive a contradiction". Andrej Bauer has a nice discussion of the distinction between proof by contradiction and proof of negation; he wrote the post in response to a Field's medalist, so confusing the two is nothing to be ashamed of.Sirajuddaula
Or else distinguishing the two is arrant pedantry.Overjoy

© 2022 - 2024 — McMap. All rights reserved.