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.