This problem can clearly be solved,
as we could simply always return “
unknown.” The challenge is to solve this
problem while keeping the occurrences of the answer “unknown” to within
a tolerable threshold, in the same way
that we hope Web browsers will
usually succeed to download Web pages,
although we know they will sometimes
fail. Note that the principled use of
unknown in tools attempting to solve
undecidable or intractable problems
is increasingly common in computer
science; for example, in program analysis, type systems, and networking.
In recent years, powerful new ter-
mination tools have emerged that re-
turn “unknown” infrequently enough
that they are useful in practice. 35 These
termination tools can automatically
prove or disprove termination of many
famous complex examples such as
Ackermann’s function or McCarthy’s
91 function as well as moderately sized
industrial examples such as Windows
device drivers. Furthermore, entire
families of industrially useful termi-
nation-like properties—called live-
ness properties—such as “Every call to
lock is eventually followed by a call
to unlock” are now automatically
provable using termination proving
techniques. 12, 29 With every month, we
now see more powerful applications
of automatic termination proving. As
an example, recent work has demon-
strated the utility of automatic ter-
mination proving to the problem of
showing concurrent algorithms to be
non-blocking. 20 With further research
and development, we will see more
powerful and more scalable tools.
Turing’s Classic Method
and Disjunctive
Well-Foundness
formally proving program termination amounts to proving the program’s transition
relation R to be well-founded. If (S, ≥) is a well-order then > is a well-founded relation.
furthermore, any map f into S defines a well-founded relation, by lifting > via f, that
is, {(s, t) | f (s) > f (t)}. turing’s method39 of proving a program’s transition relation R
well-founded amounts to finding a map f into a well-order, which defines a termination
argument T = {(s, t) | f (s) > f (t)}. to prove the validity of T we must show R ⊆ T. from the
well-foundedness of T and the fact that every sub-relation of a well-founded relation is
well-founded follows that R is well-founded.
In this article we are using the phrase disjunctive termination argument to refer to
a disjunctively well-founded transition invariant. 31 this is a finite union T1 ∪ . . . ∪ Tn of
well-founded relations that contains R+, which is the transitive closure of the transition
relation of the program, as a superset, such as, R+ ⊆ T1 ∪ . . . ∪ Tn.
Usually, each T1, . . . , Tn will be constructed as above via some map into a well-order.
note that the non-reflexive transitive closure (the + in R+) is crucial. It is not sufficient
to show that R ⊆ T1 ∪ . . . ∪ Tn,, as the union of well-founded relations is not guaranteed
to be well-founded. It is the transitive closure that makes checking the subset inclusion
more difficult in practice.
the recent approaches for proving termination for general programs3, 4, 9, 12, 14, 32 are
based on the proof rule of disjunctively well-founded transition invariants. the proof
rule itself is based on ramsey’s theorem, 34 and it has been developed in the effort to
give a logical foundation to the termination analysis based on size-change graphs. 24 the
principle expressed by the proof rule appears implicitly already in previously developed
termination algorithms for rewrite systems and logic and functional programs, see
refs10, 15, 17, 24.
Disjunctive termination arguments
Thirteen years after publishing his
original undecidability result, Turing
proposed the now classic method of
proving program termination. 39 His
solution divides the problem into two
parts:
Termination argument search: Find
a potential termination argument in
the form of a function that maps every
program state to a value in a mathematical structure called a well-order.
We will not define well-orders here,
the reader can assume for now that we
are using the natural numbers (a.k.a.
the positive integers).
Termination argument checking:
Proves the termination argument to
be valid for the program under consideration by proving that result of the
function decreases for every possible
program transition. That is, if f is the
termination argument and the program can transition from some state s
to state s¢, then f(s) > f( s¢).
(Readers with a background in logic
may be interested in the formal explanation contained in the sidebar here.)
A well-order can be thought of as a
terminating program—in the example of the natural numbers, the program is one that counts from some
initial value in the natural numbers
down to 0. Thus, no matter which initial value is chosen the program will
still terminate. Given this connection
between well-orders and terminating programs, in essence Turing is
proposing that we search for a map
from the program we are interested in
proving terminating into a program
known to terminate such that all steps
in the first program have analogous
steps in the second program. This
map to a well-order is usually called a
progress measure or a ranking function
in the literature. Until recently, all
known methods of proving termination were in essence minor variations
on the original technique.