review articles
DoI: 10.1145/1941487.1941509
In contrast to popular belief, proving
termination is not always impossible.
BY BYRon CooK, anDReas PoDeLsKI,
anD anDRe Y RYBaLChenKo
Proving
Program
termination
the ProGraM terMInatIon problem, also known
as the uniform halting problem, can be defined as
follows:
Using only a finite amount of time, determine
whether a given program will always finish running
or could execute forever.
This problem rose to prominence before the
invention of the modern computer, in the era of
Hilbert’s Entscheidungsproblem:a the challenge to
formalize all of mathematics and use algorithmic
means to determine the validity of all statements.
In hopes of either solving Hilbert’s challenge, or
showing it impossible, logicians began to search
for possible instances of undecidable problems.
Turing’s proof38 of termination’s undecidability is
the most famous of those findings.b
The termination problem is structured as an infinite
a In English: “decision problem.”
b There is a minor controversy as to whether or not Turing proved the undecidability in38. Technically
he did not, but termination’s undecidability is an easy consequence of the result that is proved. A
simple proof can be found in Strachey. 36
set of queries: to solve the problem
we would need to invent a method capable of accurately answering either
“terminates” or “doesn’t terminate”
when given any program drawn from
this set. Turing’s result tells us that
any tool that attempts to solve this
problem will fail to return a correct
answer on at least one of the inputs.
No number of extra processors nor
terabytes of storage nor new sophisticated algorithms will lead to the development of a true oracle for program
termination.
Unfortunately, many have drawn
too strong of a conclusion about the
prospects of automatic program ter-
mination proving and falsely believe
we are always unable to prove termi-
nation, rather than more benign con-
sequence that we are unable to always
prove termination. Phrases like “but
that’s like the termination problem”
are often used to end discussions that
might otherwise have led to viable par-
tial solutions for real but undecidable
problems. While we cannot ignore
termination’s undecidability, if we
develop a slightly modified problem
statement we can build useful tools.
In our new problem statement we will
still require that a termination prov-
ing tool always return answers that
are correct, but we will not necessarily
require an answer. If the termination
prover cannot prove or disprove termi-
nation, it should return “unknown.”
Using only a finite amount of time,
determine whether a given program
will always finish running or could
execute forever, or return the answer
“unknown.”
key insights
for decades, the same method was used
for proving termination. It has never been
applied successfully to large programs.
a deep theorem in mathematical logic,
based on Ramsey’s theorem, holds the
key to a new method.
IlluSTra TIon By Ma T THe W CooPer
the new method can scale to large
programs because it allows for the
modular construction of termination
arguments.