The size-change principle for program termination

The "size-change termination" principle for a first-order functional langua ge with well-founded data is: a program terminates on all inputs if every i nfinite call sequences (following program control flow) would cause an infi nite descent in some data values. Size-change analysis is based only on local approximations to parameter siz e changes derivable from program syntax. The set of infinite call sequences that follow program flow and can be recognized as causing infinite descent is an w-regular set, representable by a Buchi automaton. Algorithms for su ch automata can be used to decide size-change termination. We also give a d irect algorithm operating on "size-change graphs" (without the passage to a utomata). Compared to other results in the literature, termination analysis based on the size-change principle is surprisingly simple and general: lexical order s (also called lexicographic orders), indirect function calls and permuted arguments (descent that is not in-situ) are all handled automatically and w ithout special treatment, with no need for manually supplied argument order s, or theorem-proving methods not certain to terminate at analysis time. We establish the problem's intrinsic complexity. This turns out to be surpr isingly high, complete for PSPACE, in spite of the simplicity of the princi ple. PSPACE hardness is proved by a reduction from Boolean program terminat ion. An interesting consequence: the same hardness result applies to many o ther analyses found in the termination and quasi-termination literature.