  The problem of determining whether or not any program terminates was shown to
be undecidable by Turing, but recent advances in the area have allowed this
information to be determined for a large class of programs. The classic method
for deciding whether a program terminates dates back to Turing himself and
involves finding a ranking function that maps a program state to a well-order,
and then proving that the result of this function decreases for every possible
program transition. More recent approaches to proving termination have involved
moving away from the search for a single ranking function and toward a search
for a set of ranking functions; this set is a choice of ranking functions and a
disjunctive termination argument is used. In this paper, we describe a new
technique for determining whether programs terminate. Our technique is applied
to the output of the distillation program transformation that converts programs
into a simplified form called distilled form. Programs in distilled form are
converted into a corresponding labelled transition system and termination can
be demonstrated by showing that all possible infinite traces through this
labelled transition system would result in an infinite descent of well-founded
data values. We demonstrate our technique on a number of examples, and compare
it to previous work.
