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.
Moshe Y. Vardi, EDIToR-IN-CHIEF