article

The size-change principle for program termination

Authors:

Amir M. Ben-AmramAuthors Info & Claims

ACM SIGPLAN Notices, Volume 36, Issue 3

Pages 81 - 92

https://doi.org/10.1145/373243.360210

Published: 01 January 2001 Publication History

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.

References

[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.

[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.

Digital Library

[3]

Thomas Arts. Automatically Proving Termination and Innermost Normalisation of Term Rewriting Systems. PhD thesis, Universiteit Utrecht, 1997.

[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.

[5]

Anders Bondorf. Similix manual. Technical Report 91/9, DIKU, University of Copenhagen, Denmark, 1991.

[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.

Digital 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.

[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.

[9]

Arne J. Glenstrup. Terminator II: Stopping partial evaluation of fully recursive programs. Master's thesis, DIKU, University of Copenhagen, Denmark, 1999.

[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.

Digital Library

[11]

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM (CACM), 12(10):576-580, October 1969.

Digital 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.

Digital Library

[13]

Neil D. Jones. Computability and Complexity From a Programming Perspective. Foundations of Computing Series. MIT Press, 1997.

Digital 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.

[15]

Lutz Pliimer. Termination Proofs for Logic Programs, volume 446 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1990.

Digital 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.

Digital 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.

[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.

Digital 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.

Digital 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.

Digital Library

Cited By

Hanus M(2024)Improving Logic Programs by Adding FunctionsLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_2(27-44)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71294-4_2
Kristensen JKaarsgaard RThomsen M(2024)Jeopardy: An Invertible Functional Programming LanguageReversible Computation10.1007/978-3-031-62076-8_9(124-141)Online publication date: 29-May-2024
https://doi.org/10.1007/978-3-031-62076-8_9
Aziz B(2021)A process algebraic mutation framework with application to a vehicle charging protocolVehicular Communications10.1016/j.vehcom.2021.10035230(100352)Online publication date: Aug-2021
https://doi.org/10.1016/j.vehcom.2021.100352
Show More Cited By

Recommendations

The size-change principle for program termination
POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 36, Issue 3

March 2001

303 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/373243

Editors:
Cindy Norris
Appalachian State Univ., Boone, NC
,
James B. Fenwick
Appalachian State Univ., Boone, NC

Issue’s Table of Contents

POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2001
304 pages
ISBN:1581133367
DOI:10.1145/360204
Chairmen:
Chris Hankin
Imperial College, London, U. K.
,
Dave Schmidt
Kansas State Univ., Manhattan

Copyright © 2001 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2001

Published in SIGPLAN Volume 36, Issue 3

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

301
Total Citations
View Citations
2,646
Total Downloads

Downloads (Last 12 months)120
Downloads (Last 6 weeks)34

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hanus M(2024)Improving Logic Programs by Adding FunctionsLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_2(27-44)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71294-4_2
Kristensen JKaarsgaard RThomsen M(2024)Jeopardy: An Invertible Functional Programming LanguageReversible Computation10.1007/978-3-031-62076-8_9(124-141)Online publication date: 29-May-2024
https://doi.org/10.1007/978-3-031-62076-8_9
Aziz B(2021)A process algebraic mutation framework with application to a vehicle charging protocolVehicular Communications10.1016/j.vehcom.2021.10035230(100352)Online publication date: Aug-2021
https://doi.org/10.1016/j.vehcom.2021.100352
Aziz BAziz B(2021)Third Case Study: An Electric Vehicle Charging ProtocolFormal Analysis by Abstract Interpretation10.1007/978-3-030-91153-9_6(87-108)Online publication date: 14-Dec-2021
https://doi.org/10.1007/978-3-030-91153-9_6
Hainry EJeandel EPéchoux RZeyen O(2021)ComplexityParser: An Automatic Tool for Certifying Poly-Time Complexity of Java ProgramsTheoretical Aspects of Computing – ICTAC 202110.1007/978-3-030-85315-0_20(357-365)Online publication date: 20-Aug-2021
https://doi.org/10.1007/978-3-030-85315-0_20
Almeida AAyala-Rincón M(2020)Formalizing the dependency pair criterion for innermost terminationScience of Computer Programming10.1016/j.scico.2020.102474(102474)Online publication date: Apr-2020
https://doi.org/10.1016/j.scico.2020.102474
Cousot P(2020)On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational SemanticsLogic-Based Program Synthesis and Transformation10.1007/978-3-030-45260-5_1(3-18)Online publication date: 22-Apr-2020
https://doi.org/10.1007/978-3-030-45260-5_1
Chatterjee KFu HNovotný PHasheminezhad R(2018)Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic ProgramsACM Transactions on Programming Languages and Systems10.1145/317480040:2(1-45)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3174800
Morcillo PMoreno G(2018)Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic ProgramsInteractions Between Computational Intelligence and Mathematics10.1007/978-3-319-74681-4_5(57-78)Online publication date: 11-Mar-2018
https://doi.org/10.1007/978-3-319-74681-4_5
Rowe RBrotherston JBertot YVafeiadis V(2017)Automatic cyclic termination proofs for recursive procedures in separation logicProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs10.1145/3018610.3018623(53-65)Online publication date: 16-Jan-2017
https://dl.acm.org/doi/10.1145/3018610.3018623
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents