“Turing’s work was of course a great contribution to the world of mathematics, but there is a question of exactly how it is related to the world of computing. – Wilkes
The undecidability of the halting problem for Turing machines is not relevant to computer programming and provides no information about whether there can be computer programs that automatically check the correctness of other computer programs. Knowing that some problem is Turing decidable or Turing undecidable doesn’t mean you know anything about how hard it is for actual computer programs on physical computers.
- A problem can be Turing decidable, even trivially Turing decidable, but impossible or infeasible for computer programs on physical computers.
- A problem can be Turing undecidable but solvable by computers in practice.
- Computer programs on physical computers are finite state, so their halting problems and correctness are trivially decidable by Turing machines.
Much of the confusion comes from sloppy definitions of “program” and “halting problem”. Martin Davis appears to have coined the term halting problem to refer to the problem of deciding whether a Turing machine ever halts when started with a particular configuration. That halting problem is not Turing decidable. There is no Turing machine which given input \((n,m)\) is guaranteed to decide whether Turing machine \(T_n\) with input \(m\) will eventually halt. But there are Turing machines which take input \((s,n,m)\) and decide if \(T_n\) halts within \(s\) steps (or \(2^s\) steps or \(10^{10^{100000\times s}}\)) steps. It is Turing trivial to determine whether a Turing machine halts within the expected lifespan of the Milky Way given the most optimistic non-zero time for each step to complete. For most purposes, a Turing machine that takes galactic time to complete a computation never completes it.
Even in foundations of mathematics, the difference between “never halts” and “takes too long” is not always important. Kurt Gödel wrote that if decision processes worked in linear or exponential time, “this would have consequences of the greatest importance . Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine. After all, one would simply have to choose the natural number n so large that when the machine does not deliver a result, it makes no sense to think more about the problem.”
It’s trivially Turing decidable whether a Turing machine can complete within some time using some fixed number of states but is it feasible for computer programs to decide that? It seems hard. The two criteria: “feasible for computer programs” and “Turing decidable” are very different. However, the critical importance of the halting problem for Turing machines in computer science is folkloric and anyone bringing up these pesky facts will likely get one of the standard confused responses
- Yes, actual computers are finite state, but golly they have a lot of states so it’s pretty much the same thing (nope).
- If someone keeps adding or swapping out CDs or disk drives, actual computers are really infinite state (that is a halting problem for a system comprised of a computer, an immortal person to swap CDs, infinite matter, and unlimited time).
- Turing machines are good models of real programs (perhaps, but the halting problem is not relevant to that use.).
- Python, or Lisp or Haskell or something, have unbounded integers. (No they do not.)
- etc.
Much of the confusion is caused by mixing-up informal explanations with mathematics. Turing’s Entscheidungsproblem paper proposes a specific model of “computable”, arguing that the informal notion of “algorithm” in mathematics can be formalized by a type of automata that is now known as Turing machine. Once this notion is made precise, it is possible to look at the properties of these algorithms and to prove some theorems about what Turing machines can and cannot compute. But “Turing machines” are not physical computers. The first sentence of the current Wikipedia page on “Halting Problem” is a good example of imprecision leading to error:
“In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running (i.e., halt) or continue to run forever. “
The definition of “computability theory” linked in the text starts “Computability theory, also known as recursion theory“, firmly placing the topic in metamathematics. But the definition of “computer program” linked in the text is concerned with programs on physical digital computers. Determining whether such a program halts is Turing Trivial yet the next sentence in the Wikipedia article jumps back to Turing machines:
“Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist”.
So we’ve jumped from recursion theory to computer programs on physical computers to calling Turing machines “programs”. And then a jump back:
“The theoretical conclusion of not solvable is significant to practical computing efforts, defining a class of applications which no programming invention can possibly perform perfectly.”
Nope. Similar sounding words don’t necessarily have the same meaning. A mathematical proof about the limitations of “computable functions” should not be handwaved around to show something about physical computers and programs running on those computers.