The size-change principle for program termination

By Chin Soon Lee, N. Jones, Amir M. Ben-Amram. ACM-SIGACT Symposium on Principles of Programming Languages, 2001

509 citations recorded by the source corpus.

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.Size-change analysis is based only on local approximations to parameter size 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 ω-regular set, representable by a Büchi automaton. Algorithms for such automata can be used to decide size-change termination. We also give a direct algorithm operating on "size-change graphs" (without the passage to automata).Compared to other results in the literature, termination analysis based on the size-change principle is surprisingly simple and general: lexical orders (also called lexicographic orders), indirect function calls and permuted arguments (descent that is not in-situ) are all handled automatically and without special treatment, with no need for manually supplied argument orders, or theorem-proving methods not certain to terminate at analysis time.We establish the problem's intrinsic complexity. This turns out to be surprisingly high, complete for PSPACE, in spite of the simplicity of the principle. PSPACE hardness is proved by a reduction from Boolean program termination. An ineresting consequence: the same hardness result applies to many other analyses found in the termination and quasitermination literature.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/ab8e798b8cf4b6ddc2bc80e5cdabbf6b9df14b0d

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Andrey Rybalchenko
2. Andreas Abel
3. Andreas Podelski
4. Sumit Gulwani
5. Trishul M. Chilimbi
6. Krishna K. Mehra

In Computational Theory and Mathematics

1. Andrey Rybalchenko
2. Andreas Abel
3. Andreas Podelski

Citations in the corpus

• Termination checking with types (2004, background): “Lee, Jones and Ben-Amram [ 30 ] investigate termination of untyped first-order functional programs via size-change graphs.”
• Transition invariants (2004, background): “The termination analysis for functional programs in [10] has been the starting point of our work.”