The undecidability of the halting problem is not very important
Many a programmer, when confronted with a difficult computational problem, claim that it doesn’t make sense to investigate it further, since it is just a special case of the halting problem, and as proved by Turing back in the day, this is just not solvable in the general case. But I will try to show tha this is not a very useful or smart way of looking at things.
There are two important and opposite approaches that show the little utility of this thought process. They are two distinct attacks to the same area, both demostrably valid, and I hope to make them both easy to understand in this blog post.
The first issue involves the fact that, even if something is not tractable in the fully general case, it doesn’t mean there are not many useful cases where it’s not only perfectly tractable, but also well worth doing it. Let’s take static code analysis for example. Here is a nice piece of C code to find the maximum value in an array of unsigned integers:
1 2 3 4 5 6 |
unsigned int val = 0; for (int i = 0; i < N; +i) { if (array[i] > val) val = array[i]; } |
This code has a subtle but important bug: it will just never terminate. It’s actually an infinite loop. Why? Because the loop counter is not incremented. There is a typo, we missed a “+” sign in the “++i” expression, and thus the expression meant to increment the counter does nothing. Thus, the loop counter will stay at zero, and the code will loop until the sun goes nova.
Turing showed that, in the fully general case, it’s impossible to determine whether a given piece of code will terminate or not. But he did not determine, at all, it is impossible to write a tool that would detect this case, and diagnose, for sure, that this code is wrong and will crash the program that runs it.
Of course, most modern compilers will emit a diagnose of the simple typo above: “expression has no side effect”, or something similar. But this is not the point – there are many subtler cases of the same phenomenon, which can’t be easily detected by a compiler’s peephole code analysis, but which can be analyzed by sufficiently advanced tools. Fortunately, John Carmack recently bringing up static code analysis will hopefully help with interest, attention and funding towards this useful area, Gรถdel and Turing notwithstanding.
Now, let’s go to the second angle from which the though process described at the beginning of the post should be questioned. Let’s imagine designing a language that doesn’t allow non-terminating programs. By definition, this can’t be Turing-complete. And so we should be safe from programs that crash or hang indefinitely. Leaving aside the difficulty of even defining what “correctness” is for a program, we could think that we would have advanced a lot towards this goal. At least, our programs will be determined to complete. Following this direction, and trying to find ways to prove that certain classes of programs terminate, advanced terms and distinctions such as data and codata have been invented. A program that responds to an input stream should actually be allowed to run at least in proportion to the length of the input, and still be called correct!
Anyway, if this gets you excited, let me pop you bubble by introducing you to the beautifully named Ackerman function. I won’t go into the mathematical details, it’s just a perfectly well defined functions (or family of related functions, if you will), which can be simply calculated for any input, which involves some recursion. The beauty of it is the following: for small values of the input (say, 0 to 4), the function returns normal low values (1, 3, 7, 61…). But as soon as you try to calculate the function having as input 5, 6, or something higher, the result explodes, and there just aren’t enough atoms in the known universe to even print out the result. Actually, even if it is guaranteed to terminate, its calculation will keep chugging along the infinite loop seen above until the sun goes nova.
Isn’t it beautiful? As computer theorists, the first example loop and the Ackerman function with 10 as an input are completely different beasts. One is a demonstrably infinite loop that is guaranteed by theoretical reasons to arrive nowhere. And the other one is a demonstrably finite loop, which is also guaranteed by practical reasons to arrive nowhere.
We are still in the infancy of the field of computation and software development. We have achieved very little compared to what can be done, and many of today’s approaches need a lot of rethinking before we can move forward. The boundaries of functional programming, declarative programming, partial evaluation, speculative computation, etc… are often very hardly defined, and seem to leave very little room for improvements over current techniques. But the real value lies in the gaps between those, in combining the practical approaches of each, and thus it is really difficult to really see the shape of this “new programming”. But slowly, we advance, and in a few years, it will be obvious how 2012 is the stone age of programming.
We already have the words, we just need to find the way to put them together to read like “Hamlet”.
PS: I believe even genius Roger Penrose himself fell prey to a similar faux-pas in the central argument in this book “Shadows of the mind”. But this is fodder for another post some time in the future.
I completely agree with your conclusion, and I’m glad someone finally wrote about this, but I don’t know if I agree with you for the same reasons.
I admit I haven’t read Turing’s work directly, and someone correct me if I’m wrong, but from what I understand, the main insight that Turing gave us for the halting problem, is that for you to determine whether a program that uses N bits of state (i.e. memory) halts or not, then you need a decider (i.e. a program designed to decide whether its input halts or not) with at least N+1 bits of state.
As far as I understand, *that* is the real insight, which is not what most people understand as the halting problem.
Now of course, if you apply the above insight to a Turing machine, which is an imaginary machine with infinite memory and which will never exist in the real world, then of course to decide whether a program halts in the general case you need infinite amounts of memory in order to run the decider. Therefore, in a Turing machine (i.e. in Turing’s imaginary machine), it’s impossible to construct this decider.
But coming back to the real world, it is mathematically proven that for finite-state machines, i.e. machines with finite memory (or “computers”, as I like to call them), you can trivially decide whether a program halts or not, because if a program doesn’t halt then it eventually has to start repeating states (due to the machine having a finite number of possible states).
Of course, it might take you an intractable amount of time to reach that conclusion if you just use the most naive algorithm to determine if a certain state repeats itself, but it certainly is possible to design much more clever and faster algorithms that can determine that, sometimes in a very short amount of time.
The only thing that is mathematically proven is that to determine whether a program which uses N bits of memory halts, then in the worst case you need at least N+1 bits of memory to run the generic decider.
Thanks for your comment. As far as I understand, what Turing actually proved was that an algorithm that determines whether a given program halts can not exist at all. Of course, for a definition of program and computer that involve non-finite states.
And since even small amounts state very quickly pile-up to become impractically large to analyze, it can be trivial, but totally impractical to determine the behavior of a program on finite-state computers, such that we’re better off treating things with the same tools used to analyze programs running on non-finite-state machines.
It’s amazing how alike we think. ๐ I had almost the same thought when I read your first post on this subject (which I’ve also been thinking about: http://news.ycombinator.com/item?id=3507901), even wrote this little comment on Hacker News: http://news.ycombinator.com/item?id=3508365.
If you do decide to work on this let me know. I’d love to discuss some approaches… ๐
Bjorn, cool to read that and your comments! Indeed we are examining close areas with a similar take on things ๐
I’ve been thinking lately that, although it will take a long time, and I’m not too sure of the commercial approach (there is none within practical reach), working in this area will probably the Work of my life.
So yeah, I’ll keep writing here, and I hope to set up some open work & discussion area somewhere/somehow. But my available time is limited now, so for some time I’ll probably keep just posting articles every now and then.
I’ll definitely be really happy to discuss things and approaches!
Likewise, time very limited right now… But agree, this could be a worthwhile life’s work :), and the first problem is finding something within practical reach.
I’ve made a similar arguments using the Ackermann function. My conclusion is that “termination” is insufficient, that we need programming languages and type systems that enable us to control performance and meet real-time constraints. Long-running programs can be modeled as incrementally manipulating state resources in real-time. (The real win of such designs is a more formal, precise, logical approach to concurrency.)
Re: stone age of programming – I found this image a wonderful metaphor for certain areas of modern technology.
I agree with your analysis. There is so much to be done in the world of computation!
And I love the image. Bookmarking it for future use. Thanks!
Thank you so much for finally resolving the question in my mind (via Ackerman functions) that BLooP (bounded loop language) is not actually helpful. Sorry, but again this is from Godel, Escher, Bach–this time from chapter XIII (http://www.scribd.com/doc/6457786/Godel-Escher-Bach-by-Douglas-R-Hofstadter-).
Rick…I mean, um Gink