Chin Soon Lee
ABSTRACT
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.
- 1.Andreas Abel and Thorsten Altenkirch. A semantical analysis of structural recursion. In Abstracts of the Fourth International Workshop on Termination WST'99: pages 24-25. unpublished: May 1999.Google Scholar
- 2.Peter Hoist Andersen and Carsten Kehler Hoist. Termination analysis for offline partial evaluation of a higher order functional language. In Static Analysis, Proceedings of the Third International Symposium, SAS '96, Aachen, Germany, Sep 24-26, 1996, volume 1145 of Lecture Notes in Computer Science, pages 67-82. Springer, 1996. Google ScholarDigital Library
- 3.Thomas Arts. Automatically Proving Termination and Innermost Normalisation of Term Rewriting Systems. PhD thesis, Universiteit Utrecht, 1997.Google Scholar
- 4.Thomas Arts and Jiirgen Giesl. Proving innermost termination automatically. In Proceedings Rewriting Techniques and Applications RTA '97, volume 1232 of Lecture Notes in Computer Science, pages 157-171. Springer, 1997. Google Scholar
- 5.Anders Bondorf. Similix manual. Technical Report 91/9, DIKU, University of Copenhagen, Denmark, 1991.Google Scholar
- 6.Wei Ngan Chin and Siau Cheng Khoo. Calculating sized types. In Julia Lawall, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, Boston, Mass., USA. ACM, 2000. Google ScholarDigital Library
- 7.Michael Codish and Cohavit Taboch. A semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints. In Michael Hanus, Jan Heering, and Karl Meinke, editors, Algebraic and Logic Programming, 6th International Joint Conference, ALP '97-HOA '97, Southampton, U.K., September 3-5, 1997, volume 1298 of Lecture Notes in Computer Science, pages 31-45. Springer, 1997. Google Scholar
- 8.Jiirgen Giesl. Termination analysis for functional programs using term orderings. In Alan Mycroft, editor, Proc. 2nd Int'l Static Analysis Symposium (SAS), Glasgow, Scotland, volume 983 of Lecture Notes in Computer Science, pages 154-171. Springer-Verlag, September 1995. Google Scholar
- 9.Arne J. Glenstrup. Terminator II: Stopping partial evaluation of fully recursive programs. Master's thesis, DIKU, University of Copenhagen, Denmark, 1999.Google Scholar
- 10.Arne J. Glenstrup and Neil D. Jones. BTA algorithms to ensure termination of off-line partial evaluation. In Perspectives of System Informatics, Proceedings of the Second International Andrei Ershov Memorial Conference, Akademgorodok, Novosibirsk, Russia, Jun 25-28, 1996, volume 1181 of Lecture Notes in Computer Science, pages 273-284. Springer, 1996. Google ScholarDigital Library
- 11.C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM (CACM), 12(10):576-580, October 1969. Google ScholarDigital Library
- 12.Carsten Kehler Hoist. Finiteness analysis. In John Hughes, editor, Functional Programming Languages and Computer Architecture, Cambridge, Massachusetts, August 1991, volume 523 of Lecture Notes in Computer Science, pages 473-495. Springer, 1991. Google ScholarDigital Library
- 13.Neil D. Jones. Computability and Complexity From a Programming Perspective. Foundations of Computing Series. MIT Press, 1997. Google ScholarDigital Library
- 14.Naomi Lindenstrauss and Yehoshua Sagiv. Automatic termination analysis of Prolog programs. In Lee Naish, editor, Proceedings of the Fourteenth International Conference on Logic Programming, pages 64-77, Leuven, Belgium, Jul 1997. MIT Press.Google Scholar
- 15.Lutz Pliimer. Termination Proofs for Logic Programs, volume 446 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1990. Google ScholarDigital Library
- 16.S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319-327, IEEE, 1988.Google ScholarDigital Library
- 17.Yehoshua Sagiv. A termination test for logic programs. In Vijay Saraswat and Kazunori Ueda, editors, Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA, Oct 28-Nov 1, 1991, pages 518-532. MIT Press, 1991.Google Scholar
- 18.A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Biichi automata with applications to temporal logic. Theoretical Computer Science, 49:217-237, 1987. Google ScholarDigital Library
- 19.Chris Speirs, Zoltan Somogyi, and Harald Sondergaard. Termination analysis for Mercury. In Pascal Van Hentenryck, editor, Static Analysis, Proceedings of the 4th International Symposium, SAS '97, Paris, France, Sep 8-19, 1997, volume 1302 of Lecture Notes in Computer Science, pages 160-171. Springer, 1997. Google ScholarDigital Library
- 20.Joachim Steinbach. Automatic termination proofs with transformation orderings. In Jieh Hsiang, editor, Rewriting Techniques and Applications, Proceedings of the 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, volume 914 of Lecture Notes in Computer Science, pages 11-25. Springer, 1995. Google ScholarDigital Library
Index Terms
- The size-change principle for program termination
Recommendations
The size-change principle for program termination
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 ...
Proving termination of context-sensitive rewriting by transformation
Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite ...
Proving Termination of Context-Sensitive Rewriting with MU-TERM
Context-sensitive rewriting (CSR) is a restriction of rewriting which forbids reductions on selected arguments of functions. Proving termination of CSR is an interesting problem with several applications in the fields of term rewriting and programming ...
Comments