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.