editor’s letter

DOI: 10.1145/1965724.1965725
Moshe Y. Vardi

Solving the unsolvable

On June 16, 1902, British philosopher Bertrand Russell sent a letter to Gottlob Frege, a German logician, in which he argued, by using what became known as “Russell’s Paradox,” that Frege’s logical system was inconsistent. The letter launched a “Foundational Crisis” in mathematics, triggering an almost anguished search for proper foundations for mathematics. In 1921, David Hilbert, the preeminent German mathematician, launched a research program aimed at disposing “the foundational questions once and for all.” Hilbert’s Program failed; in 1931, Austrian logician Kurt Goedel proved two incompleteness theorems that proved the futility of Hilbert’s Program.

Halting Problem—checking whether a given recursive function or Turing machine yields an output on a given input—is unsolvable.

The unsolvability of the Halting Problem, proved just as Konrad Zuse in Germany and John Atanasoff and Clifford Berry in the U.S. were embarking on the construction of their digital computers—the Z3 and the Atanasoff-Berry Computer—meant that computer science was born with a knowledge of the inherent limitation of mechanical computation. While Hilbert believed that “every mathematical problem is necessarily capable of strict resolution,” we know that

the unsolvable is a barrier that cannot be breached. When I encountered unsolvability as a fresh graduate student, it seemed to me an insurmountable wall. Much of my research over the years was dedicated to delineating the boundary between the solvable and the unsolvable.

It is quite remarkable, therefore, that the May 2011 issue of Communications included an article by Byron Cook, Andreas Podelski, and Andrey Rybalchenko, titled “Proving Program Termination” (p. 88), in which they argued that “in contrast to popular belief, proving termination is not always impossible.” Surely they got it wrong!

The Halting Problem (termination is the same as halting) is unsolvable! Of course, Cook et al. do not really claim to have solved the Halting Problem.

What they describe in the article is a
new method for proving termination
of programs. The method itself is not
guaranteed to terminate—if it did, this
would contradict the Church-Turing
Theorem. What Cook et al. illustrate
is that the method is remarkably effec-
tive in practice and can handle a large
number of real-life programs. In fact, a
software tool called Terminator, used
to implement their method, has been
able to find some very subtle termina-
tion errors in Microsoft software.