October 2004, 91pp.
The size-change termination principle \cite is a simple criterion for program termination, originally described for first-order functional programs. A program is size-change terminating if any infinite call sequence would result in an infinite decrease of a well-founded parameter. This is a powerful and simple termination analysis, so that it identifies termination for a substantial and natural class of programs. In addition, its extensional power is the class of mutual recursive functions.
The ideas underlying the size-change termination analysis have been applied recently to develop a termination analysis for the pure untyped lambda calculus. Again, this is a powerful method, proving termination of lambda expressions containing even the Y fixpoint combinator.
We bridge the gap between the two analyses by developing a termination analysis of a call-by-value, higher order functional language. This is an application of the ideas used in the lambda calculus analysis, which it subsumes. It is also a useful step in applying this analysis to real functional programs.