Size-change analysis is based on
size-change graphs giving local approximations to parameter size changes derivable from program syntax. The “size-change termination” principle
for a first-order functional language with well-founded data is: a program terminates on all inputs if
every infinite call sequence (following program control flow) would cause an infinite descent in some data values. Two termination detection algorithms
are given in [
9]: one involving Büchi automata that directly realizes the definition; and a more useful one involving a closure algorithm
on a set of size-change graphs.
Termination analysis based on this principle seems simpler, more general and more automatic than other work in the literature:
lexicographic orders, mutually recursive function calls and permuted arguments are all handled automatically and without special treatment, with no need for human-supplied argument orders, or theorem-proving search methods not certain to terminate at analysis
time.