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

Question

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

The proof is straight-forward; what I don't understand is your question. Are you happy with the concept of a proof by contradiction? — Kerrek SB, Dec 06 '11 at 02:14
Kay, that's not correct: copying one page from an entire text, for purposes of commentary, is certainly fair use. — Charlie Martin, Dec 06 '11 at 02:17
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. — Adam Lear, Dec 06 '11 at 02:25
@MichaelHoffman No. [cstheory.se] is for **research-level** theoretical computer science, as indicated in its [FAQ](http://cstheory.stackexchange.com/faq). Explaining a proof in a textbook is not a research-level question. Officially, computer science questions are on-topic on [so], though there is a [proposed computer science site](http://area51.stackexchange.com/proposals/35636/computer-science-non-programming?referrer=4M74nqLafvszXN85c5ibxQ2) that would give them a better home. — Gilles 'SO- stop being evil', Dec 06 '11 at 02:36
Anna, I'mm grant that IANAL, but I am a professional writer and editor, and I certainly have no qualms at calling it fair use. For the fhols who voted to close, I've gone through this rant before, but look -- SO is a good resource for beginners, and something like the Halting Problem is a core thing to understand in computer science. Just because it's not coded in C doesn't mean it's not a good question. — Charlie Martin, Dec 06 '11 at 02:51
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?! — Shog9, Dec 06 '11 at 04:23
@Shog9 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. — Charlie Martin, Dec 06 '11 at 15:49
@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*. — Shog9, Dec 06 '11 at 18:44
@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. — Charlie Martin, Dec 06 '11 at 19:13

score 28 · Answer 1 · edited May 23 '17 at 12:03

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.

edited May 23 '17 at 12:03

Community

1
1

answered Nov 27 '13 at 01:50

Juan

14,840
23
98
182

8

+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. – Paul Manta Jan 25 '14 at 15:38
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](https://en.wikipedia.org/wiki/Halting_problem). – Yai0Phah Nov 09 '15 at 18:47
2

@FrankScience In fact, the recursion theorem guarantees the existence of a function with these semantics. – Yuval Filmus Nov 09 '15 at 20:58
@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. – Yai0Phah Nov 09 '15 at 21:21
@Gudradain, there is no recursion here. In the "halts" call just the function "deceiver" is passed as a parameter, but it's not called – Gonzalo Solera Feb 22 '18 at 23:11
This is a good enough demonstration, although it's not accurate to the Turing machine formulation of the problem. – user253751 Apr 19 '22 at 18:47

Charlie Martin · Accepted Answer · 2011-12-08T04:12:42.497

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.

edited Dec 08 '11 at 04:12

answered Dec 06 '11 at 02:16

Charlie Martin

107,118
23
189
257

1

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. – Cascabel Dec 06 '11 at 21:47
2

@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](http://en.wikipedia.org/wiki/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. – Gilles 'SO- stop being evil' Dec 06 '11 at 22:29
@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. – Cascabel Dec 06 '11 at 22:35
3

@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. – Charlie Martin Dec 06 '11 at 23:12
1

@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. – Charlie Martin Dec 06 '11 at 23:19
@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](http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/); he wrote the post in response to a Field's medalist, so confusing the two is nothing to be ashamed of. – ntc2 Jul 27 '13 at 00:51
Or else distinguishing the two is arrant pedantry. – Charlie Martin Jul 28 '13 at 01:58

polcott · Answer 3 · 2021-05-29T05:26:02.990

The following is based on the Sipser proof

I spent two years creating the (fully operational) x86utm operating system to concretely address the halting problem using a halt decider written in C. This partial halt decider invokes an x86 emulator to execute its input in debug step mode. The input is the machine address of the x86 function cast to a 32-bit unsigned integer.

It examines the complete execution trace of this input immediately after each x86 instruction is simulated. As soon as the partial halt decider recognizes a non-terminating behavior pattern it aborts the simulation and reports not-halting.

#define u32 uint32_t  

int D(u32 P)   // P is a machine address
{
  if ( H(P, P) ) 
    return 0   // reject when H accepts
  return 1;    // accept when H rejects
} 

int main() 
{   
  H((u32)D, (u32)D ); 
}

When H is a simulating halt decider H(D,D) rejects its input as a halting computation on the basis that H(D,D) specifies infinitely nested simulation to H unless H aborts its simulation of D(D).

_D()
[00000cd0](01)  55                      push ebp
[00000cd1](02)  8bec                    mov ebp,esp
[00000cd3](03)  8b4508                  mov eax,[ebp+08]
[00000cd6](01)  50                      push eax
[00000cd7](03)  8b4d08                  mov ecx,[ebp+08]
[00000cda](01)  51                      push ecx
[00000cdb](05)  e800feffff              call 00000ae0
[00000ce0](03)  83c408                  add esp,+08
[00000ce3](02)  85c0                    test eax,eax
[00000ce5](02)  7404                    jz 00000ceb
[00000ce7](02)  33c0                    xor eax,eax
[00000ce9](02)  eb05                    jmp 00000cf0
[00000ceb](05)  b801000000              mov eax,00000001
[00000cf0](01)  5d                      pop ebp
[00000cf1](01)  c3                      ret
Size in bytes:(0034) [00000cf1]

_main()
[00000d00](01)  55                      push ebp
[00000d01](02)  8bec                    mov ebp,esp
[00000d03](05)  68d00c0000              push 00000cd0
[00000d08](05)  68d00c0000              push 00000cd0
[00000d0d](05)  e8cefdffff              call 00000ae0
[00000d12](03)  83c408                  add esp,+08
[00000d15](02)  33c0                    xor eax,eax
[00000d17](01)  5d                      pop ebp
[00000d18](01)  c3                      ret
Size in bytes:(0025) [00000d18]

===============================
...[00000d00][00101730][00000000](01)  55                      push ebp
...[00000d01][00101730][00000000](02)  8bec                    mov ebp,esp
...[00000d03][0010172c][00000cd0](05)  68d00c0000              push 00000cd0
...[00000d08][00101728][00000cd0](05)  68d00c0000              push 00000cd0
...[00000d0d][00101724][00000d12](05)  e8cefdffff              call 00000ae0
Begin Local Halt Decider Simulation at Machine Address:cd0
...[00000cd0][002117d0][002117d4](01)  55                      push ebp
...[00000cd1][002117d0][002117d4](02)  8bec                    mov ebp,esp
...[00000cd3][002117d0][002117d4](03)  8b4508                  mov eax,[ebp+08]
...[00000cd6][002117cc][00000cd0](01)  50                      push eax
...[00000cd7][002117cc][00000cd0](03)  8b4d08                  mov ecx,[ebp+08]
...[00000cda][002117c8][00000cd0](01)  51                      push ecx
...[00000cdb][002117c4][00000ce0](05)  e800feffff              call 00000ae0
...[00000cd0][0025c1f8][0025c1fc](01)  55                      push ebp
...[00000cd1][0025c1f8][0025c1fc](02)  8bec                    mov ebp,esp
...[00000cd3][0025c1f8][0025c1fc](03)  8b4508                  mov eax,[ebp+08]
...[00000cd6][0025c1f4][00000cd0](01)  50                      push eax
...[00000cd7][0025c1f4][00000cd0](03)  8b4d08                  mov ecx,[ebp+08]
...[00000cda][0025c1f0][00000cd0](01)  51                      push ecx
...[00000cdb][0025c1ec][00000ce0](05)  e800feffff              call 00000ae0
Local Halt Decider: Infinite Recursion Detected Simulation Stopped 
...[00000d12][00101730][00000000](03)  83c408                  add esp,+08
...[00000d15][00101730][00000000](02)  33c0                    xor eax,eax
...[00000d17][00101734][00100000](01)  5d                      pop ebp
...[00000d18][00101738][00000058](01)  c3                      ret
Number_of_User_Instructions(23)
Number of Instructions Executed(23826)

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

3 Answers3

The following is based on the Sipser proof

Linked