Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
Peter Holst Andersen and Carsten Kehler Holst. 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.
Thomas Arts. Automatically Proving Termination and Innermost Normalisation of Term Rewriting Systems. PhD thesis, Universiteit Utrecht, 1997.
Thomas Arts and Jürgen 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.
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.
Jürgen 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.
Arne J. Glenstrup. Terminator II: Stopping partial evaluation of fully recursive programs. Master’s thesis, DIKU, University of Copenhagen, Denmark, 1999.
Chin Soon Lee. Program termination analysis and the termination of offline partial evaluation. Ph.D. thesis, University of Western Australia.
Chin Soon Lee and Neil D. Jones and Amir Ben-Amram. The Size-Change Principle for Program Termination. In Hanne Riis Nielson, editor, ACM SIGPLAN Symposium on Principles of Programming Langages, London, England, pages 81–92. ACM Press, 2000.
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.
Lutz Plümer. Termination Proofs for Logic Programs, volume 446 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1990.
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.
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.
Chris Speirs, Zoltan Somogyi, and Harald Søndergaard. 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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jones, N.D. (2001). Program Termination Analysis by Size-Change Graphs (Abstract). In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_1
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive