{"id":1085,"date":"2010-09-12T21:21:58","date_gmt":"2010-09-12T21:21:58","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/?p=1085"},"modified":"2010-09-12T21:21:58","modified_gmt":"2010-09-12T21:21:58","slug":"the-halting-problem","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2010\/09\/12\/the-halting-problem\/","title":{"rendered":"The Halting Problem"},"content":{"rendered":"<p> Some people expressed interest in seeing a full-out, formal presentation of the Halting problem proof. So, I&#8217;m going to walk through it. There are actually a lot of different versions of this proof; the one that I&#8217;m going to use is based on the one used by my grad-school theory professor, Dr. John Case. To be clear, I&#8217;m doing it from memory, so any errors are completely my own fault, not John&#8217;s!<\/p>\n<p> To start off, we need to define what a computing device is. In formal mathematical terms, we don&#8217;t care how it works &#8211; all we care about is what it can do in abstract tems.  So what we do is define something called an <em>effective computing device<\/em>. An effective computing device is any Turing equivalent computing device. An ECS is modelled as a two parameter function <img src='http:\/\/l.wordpress.com\/latex.php?latex=phi%20%3A%20%7Bcal%20N%7D%20times%20%7Bcal%20N%7D%20rightarrow%20%7Bcal%20N%7D&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='phi : {cal N} times {cal N} rightarrow {cal N}' style='vertical-align:1%' class='tex' alt='phi : {cal N} times {cal N} rightarrow {cal N}' \/>. The first parameter is an encoding of a program as a natural number; the second parameter is the input to the program. It&#8217;s also a natural number, which might seem limiting &#8211; but we can encode any finite data structure as an integer, so it&#8217;s really not a problem. The return value is the result of the program, if the program halts. If it doesn&#8217;t halt, then we say that the pair of program and input aren&#8217;t in the domain of <img src='http:\/\/l.wordpress.com\/latex.php?latex=phi&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='phi' style='vertical-align:1%' class='tex' alt='phi' \/>. So if you wanted to describe running the program &#8220;<img src='http:\/\/l.wordpress.com\/latex.php?latex=f&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='f' style='vertical-align:1%' class='tex' alt='f' \/>&#8221; on the input 7, you&#8217;d write that as <img src='http:\/\/l.wordpress.com\/latex.php?latex=phi%28f%2C%207%29&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='phi(f, 7)' style='vertical-align:1%' class='tex' alt='phi(f, 7)' \/>. And, finally, the way that we would write that a program <img src='http:\/\/l.wordpress.com\/latex.php?latex=p&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p' style='vertical-align:1%' class='tex' alt='p' \/> doesn&#8217;t halt for input <img src='http:\/\/l.wordpress.com\/latex.php?latex=i&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='i' style='vertical-align:1%' class='tex' alt='i' \/> as <img src='http:\/\/l.wordpress.com\/latex.php?latex=phi%28p%2C%20i%29%20%3D%20bot&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='phi(p, i) = bot' style='vertical-align:1%' class='tex' alt='phi(p, i) = bot' \/>.<\/p>\n<p> So now we&#8217;ve got our basic effective computing device. There&#8217;s one thing we still need before we can formulate the halting problem. We need to be able to deal with more parameters. After all &#8211; a halting oracle is a program that takes two inputs &#8211; another program, snd the input to that program. the easiest way to do that is to use something called a <em>pairing function<\/em>. A pairing functions is a one-to-one function from an ordered pair to an integer. There are lots of possible pairing functions &#8211; for example, you can convert both numbers to binary, left-pad the smaller until they&#8217;re equal length, and then interleave the bits. Given (9,3), you convert 9 to 1001, and 3 to 11; then you pad 3 to 0011, and interleave them to give you 10001011 &#8211; 139. We&#8217;ll write our pairing function as angle brackets around the two values: <img src='http:\/\/l.wordpress.com\/latex.php?latex=langle%20x%2Cyrangle&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='langle x,yrangle' style='vertical-align:1%' class='tex' alt='langle x,yrangle' \/>.<\/p>\n<p> With the help of the pairing function, we can now express the halting problem. The question is, does there exist a program <img src='http:\/\/l.wordpress.com\/latex.php?latex=O&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='O' style='vertical-align:1%' class='tex' alt='O' \/>, called a halting oracle, such that:<\/p>\n<p><center><img src='http:\/\/l.wordpress.com\/latex.php?latex=forall%20p%2C%20forall%20i%3A%20%28varphi%28O%2Clangle%20p%2Cirangle%29%20%3D%20left%7B%20%20%20%20begin%7Barray%7D%7Bl%7D%090%20mbox%7B%20if%20%7D%20varphi%28p%2C%20i%29%20%3D%20bot%20%5C%091%20mbox%7B%20if%20%7D%20varphi%28p%2Ci%29%20neq%20bot%20%20%20end%7Barray%7Dright.&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='forall p, forall i: (varphi(O,langle p,irangle) = left{    begin{array}{l}\t0 mbox{ if } varphi(p, i) = bot \\\t1 mbox{ if } varphi(p,i) neq bot   end{array}right.' style='vertical-align:1%' class='tex' alt='forall p, forall i: (varphi(O,langle p,irangle) = left{    begin{array}{l}\t0 mbox{ if } varphi(p, i) = bot \\\t1 mbox{ if } varphi(p,i) neq bot   end{array}right.' \/><\/center><\/p>\n<p> In english, does there exist a program <img src='http:\/\/l.wordpress.com\/latex.php?latex=O&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='O' style='vertical-align:1%' class='tex' alt='O' \/> such that for all pairs of programs p and inputs i, the oracle returns <img src='http:\/\/l.wordpress.com\/latex.php?latex=1&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='1' style='vertical-align:1%' class='tex' alt='1' \/> if <img src='http:\/\/l.wordpress.com\/latex.php?latex=varphi%28p%2C%20i%29&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='varphi(p, i)' style='vertical-align:1%' class='tex' alt='varphi(p, i)' \/> halts, and 0 if it doesn&#8217;t?<\/p>\n<p> Time, finally, for the proof. Suppose that we <em>do<\/em> have a halting oracle, O. That means that for any program <img src='http:\/\/l.wordpress.com\/latex.php?latex=p&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p' style='vertical-align:1%' class='tex' alt='p' \/> and input <img src='http:\/\/l.wordpress.com\/latex.php?latex=i&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='i' style='vertical-align:1%' class='tex' alt='i' \/>, <img src='http:\/\/l.wordpress.com\/latex.php?latex=varphi%28O%2C%20langle%20p%2C%20i%20rangle%29%20%3D%200%20iff%20varphi%28p%2Ci%29%3Dbot&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='varphi(O, langle p, i rangle) = 0 iff varphi(p,i)=bot' style='vertical-align:1%' class='tex' alt='varphi(O, langle p, i rangle) = 0 iff varphi(p,i)=bot' \/>.<\/p>\n<p> So, can we devise a program $p_d$ and input <img src='http:\/\/l.wordpress.com\/latex.php?latex=i&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='i' style='vertical-align:1%' class='tex' alt='i' \/> where <img src='http:\/\/l.wordpress.com\/latex.php?latex=varphi%28p_d%2C%20i%29%20%21%3D%20bot&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='varphi(p_d, i) != bot' style='vertical-align:1%' class='tex' alt='varphi(p_d, i) != bot' \/>,<br \/>\nbut <img src='http:\/\/l.wordpress.com\/latex.php?latex=varphi%28O%2C%20langle%20p%2C%20i%20rangle%29%20%3D%200&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='varphi(O, langle p, i rangle) = 0' style='vertical-align:1%' class='tex' alt='varphi(O, langle p, i rangle) = 0' \/>? <\/p>\n<p> Of course we can. We need a <img src='http:\/\/l.wordpress.com\/latex.php?latex=p_d&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p_d' style='vertical-align:1%' class='tex' alt='p_d' \/> which takes two parameters: an oracle, and an input. So it should be really simple right? Well, not quite as easy as it might seem. You see, the problem is, <img src='http:\/\/l.wordpress.com\/latex.php?latex=p_d&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p_d' style='vertical-align:1%' class='tex' alt='p_d' \/> needs to be able to pass <em>itself<\/em> to the oracle. But how can it do that? A program can&#8217;t pass <em>itself<\/em> into the oracle. Why not? Because we&#8217;re working with the program as a G&ouml;del number &#8211; and a program can&#8217;t contain its own G&ouml;del number. If it contained it, it would be larger than itself.  And that&#8217;s rather a problem.<\/p>\n<p> But there&#8217;s a nice workaround. What we care about is: is there <em>any combination<\/em> of program <em>and input<\/em> such that <img src='http:\/\/l.wordpress.com\/latex.php?latex=O&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='O' style='vertical-align:1%' class='tex' alt='O' \/> will incorrectly predict the halting status? So what we&#8217;ll do is just turn <img src='http:\/\/l.wordpress.com\/latex.php?latex=p_d&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p_d' style='vertical-align:1%' class='tex' alt='p_d' \/> into a parameter to itself. That is, we&#8217;ll look at a program <img src='http:\/\/l.wordpress.com\/latex.php?latex=p_d&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p_d' style='vertical-align:1%' class='tex' alt='p_d' \/> like the following:<\/p>\n<pre>\ndef deceiver(input):\n   (oracle, program) =  unpair(input)\n   if oracle(program, input):\n      while(True): continue\n   else:\n      halt\n<\/pre>\n<p> Then we&#8217;ll be interested in the case where the value of the <code>program<\/code> parameter is a G&ouml;del number of the deceiver <em>itself<\/em>.<\/p>\n<p> (As an aside, there are a variety of tricks to work around this. One of the more classical ones is based on the fact that for any given program, <img src='http:\/\/l.wordpress.com\/latex.php?latex=p&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p' style='vertical-align:1%' class='tex' alt='p' \/>, there are an <em>infinite<\/em> number of versions of the same program with different G&ouml;del numbers. Using that property, you can embed a program <img src='http:\/\/l.wordpress.com\/latex.php?latex=p_%7Bd_2%7D&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p_{d_2}' style='vertical-align:1%' class='tex' alt='p_{d_2}' \/> into another program <img src='http:\/\/l.wordpress.com\/latex.php?latex=p_%7Bd%7D&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p_{d}' style='vertical-align:1%' class='tex' alt='p_{d}' \/>. But there are a few other tricks involved in getting it right. It&#8217;s not simple &#8211; Alan Turing screwed it up in the first published version of the proof!)<\/p>\n<p> Now, when input = <img src='http:\/\/l.wordpress.com\/latex.php?latex=langle%20O%2C%20p_d%20rangle&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='langle O, p_d rangle' style='vertical-align:1%' class='tex' alt='langle O, p_d rangle' \/>, then <img src='http:\/\/l.wordpress.com\/latex.php?latex=O&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='O' style='vertical-align:1%' class='tex' alt='O' \/> will make the <em>wrong<\/em> prediction about what <img src='http:\/\/l.wordpress.com\/latex.php?latex=p_d&#038;bg=FFFFFF&#038;fg=000000&#038;s=0' title='p_d' style='vertical-align:1%' class='tex' alt='p_d' \/> will do. So &#8211; once again, we&#8217;re back where we were in the simpler version of the proof. A halting oracle is a program which, given <em>any<\/em> pair of program and input, will correctly determine whether that program will halt on that input. We&#8217;re able to construct a pair of program and input where the oracle <em>doesn&#8217;t<\/em> make the right prediction, and therefore, it <em>isn&#8217;t<\/em> a halting oracle.<\/p>\n<p> This version is more abstract, but it&#8217;s still got that wonderfully concrete property. Even in the most abstract way of talking about a computing device, if you&#8217;ve got something that you believe is a halting oracle, this shows you how to create a program that will prove that the halting oracle is <em>wrong<\/em>. So you can&#8217;t possibly create a halting oracle.<\/p>\n<p> And to be extra clear: this doesn&#8217;t rely on any ambiguities about definitions, or any distinction between values and meanings. It shows a way of producing a real, concrete counterexample for any purported halting oracle. No trickery, no fudging &#8211;  if you think you have a halting oracle, you&#8217;re wrong, and this proof shows you exactly how to create a program that will demonstrate that.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Some people expressed interest in seeing a full-out, formal presentation of the Halting problem proof. So, I&#8217;m going to walk through it. There are actually a lot of different versions of this proof; the one that I&#8217;m going to use is based on the one used by my grad-school theory professor, Dr. John Case. To [&hellip;]<\/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":[79],"tags":[],"class_list":["post-1085","post","type-post","status-publish","format-standard","hentry","category-computation"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-hv","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1085","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=1085"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1085\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=1085"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=1085"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=1085"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}