The problem with Turing’s method is that finding a single, or monolithic, ranking function for the whole program is typically difficult, even for simple programs. In fact, we are often forced to use ranking functions into well-orders that are much more complex than the natural numbers. Luckily, once a suitable ranking function has been found, checking validity is in practice fairly easy.

The key trend that has led toward
current progress in termination prov-
ing has been the move away from the
search for a single ranking function
and toward a search for a set of rank-
ing functions. We think of the set as a
choice of ranking functions and talk
about a disjunctive termination argu-
ment. This terminology refers to the
proof rule of disjunctively well-found-
ed transition invariants. 31 The recent
approaches for proving termination
for general programs3, 4, 9, 12, 14, 26, 32 are
based on this proof rule. The proof
rule itself is based on Ramsey’s theo-
rem, 34 and it has been developed in
the effort to give a logical foundation
to the termination analysis based on
size-change graphs. 24

figure 1. example program.

1

2

3

4

5

6

7

8

9

10

x : = input();
y : = input();
while x > 0 and y > 0 do
if input() = 1 then
x : = x – 1;
y : = y + 1;
else

y : = y – 1;
fi
done
user-supplied inputs are gathered via calls to the function input(). We assume that the variables
range over integers with arbitrary precision (in other words, not 64-bit or 32-bit integers). Assuming
that the user always eventually enters in a value when prompted via input(), does the program
terminate for all possible user-supplied inputs? (The answer is provided in a footnote below.)

figure 2. example program.

1

2

3

4

5

6

7

8

9

10

x := input();
y := input();
while x > 0 and y > 0 do
if input () = 1 then
x := x × 1;
y := input();
else

y := y – 1;
fi
done
This program is similar to Figure 1 where the command “y := y + 1;” replaced with
“y := input();”. no ranking function into the natural numbers exists that can prove the
termination of this program.

code fragment in Figure 1. In this code
the collection of user-provided input is
performed via the function input().
We will assume the user always enters
a new value when prompted. Further-
more, we will assume for now that vari-
ables range over possibly negative in-
tegers with arbitrary precision (that is,
mathematical integers as opposed to
32-bit words, 64-bit words, and so on).
Before reading further, please answer
the question: “Does this program ter-
minate, no matter what values the user
gives via the input() function?” The
answer is given below.c
Using Turing’s traditional method
we can define a ranking function from
program variables to the natural num-
bers. One ranking function that will
work is 2x + y, though there are many
others. Here we are using the formula
2x + y as shorthand for a function
that takes a program configuration
as its input and returns the natural
number computed by looking up the
value of x in the memory, multiply-
ing that by 2 and then adding in y’s
value—thus 2x + y represents a map-
ping from program configurations to
natural numbers. This ranking func-
tion meets the constraints required
to prove termination: the valuation of
2x + y when executing at line 9 in the
program will be strictly one less than
its valuation during the same loop
iteration at line 4. Furthermore, we
know the function always produces
natural numbers (thus it is a map into
a well-order), as 2x + y is greater than
0 at lines 4 through 9.

Automatically proving the validity of a monolithic termination argument like 2x + y is usually easy using tools that check verification conditions (for example, Slam2). However, as mentioned previously, the actual search for a valid argument is famously tricky. As an example, consider the case in Figure 2, where we have replaced the command “y := y + 1;” in Figure 1 with “y := input();”. In this case no function into the natural numbers exists that suffices to prove termination; instead we must resort to a lexicographic ranking function (a ranking function into ordinals, a more advanced well-order than the naturals).