{"id":1069,"date":"2010-09-08T01:46:28","date_gmt":"2010-09-08T01:46:28","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/?p=1069"},"modified":"2010-09-08T01:46:28","modified_gmt":"2010-09-08T01:46:28","slug":"1069","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2010\/09\/08\/1069\/","title":{"rendered":"Turing Crackpottery!"},"content":{"rendered":"

One of the long-time cranks who’s commented on this blog is a bozo who goes by the name “Vorlath”. Vorlath is a hard-core Cantor crank, and so he usually shows up to rant whenever the subject of Cantor comes up. But last week, while I was busy dealing with the Scientopia site hosting trouble, a reader sent me a link to a piece Vorlath wrote about the Halting problem<\/a>. Apparently, he doesn’t like that proof either.<\/p>\n

Personally, the proof that the halting problem is unsolvable is one of my all-time favorite mathematical proofs. It’s incredibly simple – just a couple of steps. It’s very concrete<\/em> – the key to the proof is a program that you can actually write, easily, in a couple of lines of code in a scripting language. And best of all, it’s incredibly profound<\/em> – it proves something very similar to Gödel’s incompleteness theorem. It’s wonderful.<\/p>\n

To show you how simple it is, I’m going to walk you through it – in all of its technical details.<\/p>\n

<\/p>\n

Suppose I’ve got a program, $P$. I can treat the program P as a function, from its input to its output. Of course, not every program produces a result for every input. For example, I can write a program which takes an integer as a parameter, and never stops if its input is divisible by 2:<\/p>\n

\ndef RunForeverIfDivisibleByTwo(i):\n  if i % 2 == 0:\n    while True:\n      continue\n  else:\n    return i \/ 2\n<\/pre>\n
 The halting problem is basically a formal way of asking if you can tell whether or not an arbitrary<\/em> program will eventually halt.<\/p>\n
 In other words, can you write a program called a halting oracle, HaltingOracle(program, input)<\/code>, which returns true if program(input)<\/code> would eventually halt, and which returns false if it wouldn’t?<\/p>\n
 The answer is: no, you can’t.<\/p>\n
 Why not? We can finally get to the proof. Suppose, just suppose, that you could write a halting oracle. Then you could run it on any program at all, and see if it eventually halts. So, run it on this:<\/p>\n
\ndef Deciever(i):\n  oracle = i[0]\n  in = i[1]\n  if oracle(Deceiver, i):\n    while True:\n      continue\n  else:\n    return i\n<\/pre>\n
 So, the input to Deceiver<\/code> is actually a list of two elements: the first one is a proposed halting oracle. The second is another input. What the halting killer does is ask the Oracle: “Do you think I’ll halt for input i?”. If the oracle says, “Yes, you’ll halt”, then the program goes into an infinite loop. If the oracle says “No, you won’t halt”, then it halts. So no matter what the oracle says, it’s wrong.<\/p>\n
 So, if you come up with a halting oracle – a program that can tell whether or not other programs eventually halt – it will produce the wrong<\/em> result for Deceiver<\/code>. And that means that it’s not<\/em> a halting oracle – because there’s at least one program where it generates the wrong result.<\/p>\n
 That’s it. That’s the entire proof. And that little Python snippet up there? That’s a real<\/em> program that would work as a real counterexample for any real halting oracle!<\/p>\n
 See what I mean about it being very simple, and very concrete?<\/p>\n
 The reason that it’s so profound is that you can formulate any<\/em> mechanical proof process as a computer program. If a proof exists for a theorem, then you can write a program which searches for the proof, and will eventually find it. We can<\/em> do that. We can write a program which searches the entire space of first order predicate logic proofs, trying to find a proof for a specific theorem. If it’s a theorem of FOPL, it will<\/em> eventually find a proof. It might take a very, very long time. But if a statement isn’t<\/em> a valid theorem, then the program will never stop. It will keep searching, and searching, and searching. And if the program doesn’t stop, you can never actually conclude that “It’s not a theorem”, because if you just ran the program for another 10, or 100, or 1000 steps, it might<\/em> stop.<\/p>\n
 If you could solve the halting problem, then you could take a theorem proving program for a specific logical domain, and given any statement, determine whether or not it was a provable theorem – by asking the halting oracle whether the program would halt on that input! (See what I mean about it being like Gödel?)<\/p>\n
 So – Vorlath doesn’t like this proof. He thinks it’s really no good. And so, he sets out to show that it’s incorrect. And the way he does that is… by showing that a halting oracle will generate the wrong result for some inputs!<\/p>\n
 Seriously. He’s basically taking the validity<\/em> of the proof, and using it to conclude that there’s something wrong with the proof.<\/p>\n
 The way that he does this is by claiming that the program – the Deciever<\/code> above – doesn’t have a well-defined result. Because since we don’t know what the halting oracle will produce, we don’t know what the program will do. We don’t know whether the program will halt or not, because we don’t know whether the halting oracle will say<\/em> that it will halt. It’s got nothing to do with whether or not we can determine whether or not a given program will halt – the entire problem is that we don’t know what the Oracle will answer. If we knew what the Oracle would answer, then we’d know whether the program would halt.<\/p>\n
 In his words:<\/p>\n
\n
 The issue here is that this is not a proof by contradiction at all. In fact, we can show this quite clearly by using an Enabler program that does exactly what the F function says (including the Oracle).<\/p>\n
\nProgram Enabler(Function F)\n{\n  If (!F(Enabler,F)) while(true);\n}\n<\/pre>\n
 The only thing that changed is that we negated the value returned by F. Here, the Enabler program does exactly what the Oracle says it will do when F is set to the Oracle program. Unfortunately, it is still undecidable because we still don’t know which answer the Oracle will return. This is why the Deceiver program is indeterminate. It is not because of the bogus contradiction.<\/p>\n<\/blockquote>\n
 The problem with Vorlath’s whole argument is that he doesn’t seem to understand what the halting problem is<\/em>. The question isn’t “Can I look at a specific program, and figure out if it halts?” The question is, “Can I write a program that can tell whether any<\/b> other program will halt?<\/em>“.<\/p>\n
 His argument basically says that in the proof<\/em>, we, as humans reading the proof, can’t say what the halting oracle will return, and that therefore, the halting program is indeterminate, and that that’s the cause of the contradiction.<\/p>\n
 That’s not it at all.<\/p>\n
 The halting problem is a question of whether or not a program<\/em> can tell whether any<\/em> program will halt. And the halting proof is remarkably concrete. Write a program that you believe will correctly determine whether or not other programs halt – and the deciever will<\/em> work – it will produce a behavior different than what the oracle predicts. The oracle will<\/em> be wrong for the deceiver. But if you take Vorlath’s Enabler<\/code>, and run it through the oracle? It will work: it will do exactly what the Oracle says it will do. The oracle will be right<\/em>. It doesn’t matter what the oracle thinks Enabler<\/code>: in a real program, whatever the oracle answers is what Enabler<\/code> will do. Enabler isn’t indeterminate: for any given oracle, it will do exactly what the oracle predicts. It may do different things for different oracles – but that’s perfectly all right. It doesn’t matter whether we<\/em> as humans can look at it on paper, and tell whether it can halt. The question is, when the oracle produces a prediction – however it does it – will that prediction be correct? And if you run the enabler through a specific oracle? Its prediction will be correct; if you run the deceiver through a specific oracle, its prediction will be incorrect<\/em>. That’s the whole point.<\/p>\n
 Anyway… from here, Vorlath goes into a pointless sidetrack working through a specific table-based example that purportedly demonstrates the problem. This, again, demonstrates that he really doesn’t even understand what the halting proof is supposed to prove. Remember, it proves that a halting oracle will always get the wrong answer for some programs. That’s all it proves; that’s all it has to prove. So, in his own words:<\/p>\n
\nSo what is going on?  The issue is not about being able to calculate the halting status of a given function.  It is solely about definitions.  Can we define a value to be used both as input to a decision and as the conclusion of that decision?  The answer is that it is foolish to rely on this.  That’s all the halting problem is about.  We can still calculate the halting status of every input just as long as we don’t attach meaning (definitions) to those inputs (especially if we try to relate those values to the halting status.\n<\/p><\/blockquote>\n
 This couldn’t possibly be more wrong. This has nothing to do with
\ndefinitions. And it doesn’t have anything to do with being able to determine the halting status of a particular function. It has to do with whether a program<\/em> can make a correct prediction about another program<\/em>. It’s about very concrete programs. He doesn’t like the recursive nature of the solution – but real computer programs can be fully recursive<\/em>. I can<\/em> take a halting oracle program, and pass it to a halting oracle program. I can take a halting oracle, and use it as a parameter to a concrete deceiver program. You can’t escape this trap.<\/p>\n
 In fact, there’s even a whole fascinating research area that’s built on this sort of meta-circularity, where you pass the code of a program as parameter to that program. There’s a nifty idea called partial evaluation<\/em>. In partial evaluation, you can take a program which is basically a sort of static program optimizer, and by running it on itself<\/em>, you can turn an interpreter into a compiler. It actually works<\/em>. It’s a bit hard to follow. But it works<\/em>. There are really people working on building compilers this way! There’s a book on it, available here<\/a>. And I’ll probably write a post about it at some point.<\/p>\n
 So? Vorlath: moron. His counter to the halting proof? It’s not a counter: it’s an example of how the halting proof produces the right result. His distinction between definition and computation? Totally bogus.<\/p>\n
 On the other hand.. Alan Turing? Genuis. Halting proof? Really cool. Recursive meta-programming? Super cool.<\/p>\n","protected":false},"excerpt":{"rendered":"
One of the long-time cranks who’s commented on this blog is a bozo who goes by the name “Vorlath”. Vorlath is a hard-core Cantor crank, and so he usually shows up to rant whenever the subject of Cantor comes up. But last week, while I was busy dealing with the Scientopia site hosting trouble, a […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[2,7],"tags":[119,138,171,175,249],"class_list":["post-1069","post","type-post","status-publish","format-standard","hentry","category-bad-math","category-bad-software","tag-cantor-crank","tag-crackpottery","tag-godel","tag-halting-problem","tag-turing"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/s4lzZS-1069","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1069","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=1069"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1069\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=1069"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=1069"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=1069"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}