Article

Testing for termination with monotonicity constraints

Authors:

Michael Codish,

Vitaly Lagoon,

Peter J. StuckeyAuthors Info & Claims

ICLP'05: Proceedings of the 21st international conference on Logic Programming

Pages 326 - 340

https://doi.org/10.1007/11562931_25

Published: 02 October 2005 Publication History

Publisher Site

Abstract

Termination analysis is often performed over the abstract domains of monotonicity constraints or of size change graphs. First, the transition relation for a given program is approximated by a set of descriptions. Then, this set is closed under a composition operation. Finally, termination is determined if all of the idempotent loop descriptions in this closure have (possibly different) ranking functions. This approach is complete for size change graphs: An idempotent loop description has a ranking function if and only if it has one which indicates that some specific argument decreases in size. In this paper we generalize the size change criteria for size change graphs which are not idempotent. We also illustrate that proving termination with monotonicity constraints is more powerful than with size change graphs and demonstrate that the size change criteria is incomplete for monotonicity constraints. Finally, we provide a complete termination test for monotonicity constraints.

References

[1]

A. Brodsky and Y. Sagiv. Inference of monotonicity constraints in Datalog programs. In Proceedings of the Eighth ACM SIGACT-SIGART-SIGMOD Symposium on Principles of Database Systems, pages 190-199, 1989.

Crossref

Google Scholar

[2]

M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming, 41(1):103-123, 1999.

Google Scholar

[3]

N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing, 12(1-2):117-156, 2001.

Google Scholar

[4]

C. C. Frederiksen. A simple implementation of the size-change termination principle. Technical Report D-442, DIKU, Copenhagen University, Denmark, 2001.

Google Scholar

[5]

G. Frobenius. Über endliche gruppen. Sitzungsber. Preuss. Akad. Wiss. Berlin, pages 163-194, 1895.

Google Scholar

[6]

M. Gabbrielli and R. Giacobazzi. Goal independency and call patterns in the analysis of logic programs. In Proceedings of the Ninth ACM Symposium on Applied Computing, pages 394-399. ACM Press, 1994.

Crossref

Google Scholar

[7]

C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. ACM SIGPLAN Notices, 36(3):81-92, 2001. Proceedings of POPL'01.

Crossref

Google Scholar

[8]

N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of logic programs. In L. Naish, editor, Proceedings of the Fourteenth International Conference on Logic Programming, pages 63-77, Leuven, Belgium, 1997. The MIT Press.

Google Scholar

[9]

N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. Termilog: A system for checking termination of queries to logic programs. In O. Grumberg, editor, CAV, volume 1254 of Lecture Notes in Computer Science, pages 444-447. Springer, 1997.

Crossref

Google Scholar

[10]

A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In B. Steffen and G. Levi, editors, Verification, Model Checking, and Abstract Interpretation, 5th International Conference, volume 2937 of Lecture Notes in Computer Science, pages 239-251. Springer, 2004.

Google Scholar

[11]

F. Ramsey. On a problem of formal logic. In Proceedings London Mathematical Society, volume 30, pages 264-286, 1930.

Google Scholar

[12]

R. Thiemann and J. Giesl. Size-change termination for term rewriting. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA-03), volume 2706 of Lecture Notes in Computer Science, pages 264-278. Springer-Verlag, 2003.

Crossref

Google Scholar

[13]

D. Wahlstedt. Detecting termination using size-change in parameter values. Master's thesis, Göteborgs Universitet, 2000. http://www.cs.chalmers.se/~davidw/.

Google Scholar

Cited By

View all

Calautti MGreco STrubitsyna I(2017)Detecting Decidable Classes of Finitely Ground Logic Programs with Function SymbolsACM Transactions on Computational Logic10.1145/314380418:4(1-42)Online publication date: 16-Nov-2017
https://dl.acm.org/doi/10.1145/3143804
Calautti MGreco SMolinaro CTrubitsyna I(2015)Logic program termination analysis using atom sizesProceedings of the 24th International Conference on Artificial Intelligence10.5555/2832581.2832645(2833-2839)Online publication date: 25-Jul-2015
https://dl.acm.org/doi/10.5555/2832581.2832645
Ben-Amram AGenaim S(2014)Ranking Functions for Linear-Constraint LoopsJournal of the ACM10.1145/262948861:4(1-55)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2629488
Show More Cited By

Testing for termination with monotonicity constraints
1. Theory of computation

Recommendations

Size-Change Termination, Monotonicity Constraints and Ranking Functions
CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification

Size-change termination involves deducing program termination based on the impossibility of infinite descent. To this end we may use a program abstraction in which transitions are described by <em>monotonicity constraints</em> over (abstract) variables. ...
Inference of monotonicity constraints in datalog programs
PODS '89: Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems

Datalog (i.e., function-free logic) programs with monotonicity constraints on extensional predicates are considered. A monotonicity constraint states that one argument of a predicate is always less than another argument, according to some partial order. ...
Inference of monotonicity constraints in Datalog programs

Datalog (i.e., functionýfree logic) programs with monotonicity constraints on extensional predicates are considered. A monotonicity constraint states that one argument of a predicate or a constant is always less than another argument or a constant, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICLP'05: Proceedings of the 21st international conference on Logic Programming

October 2005

453 pages

ISBN:354029208X

Editors:
Maurizio Gabbrielli
Dipartimento di Scienze dell'Informazione, Universitá di Bologna, Italy
,
Gopal Gupta
Department of Computer Science, University of Texas at Dallas, Richardson, TX, Italy

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 02 October 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Calautti MGreco STrubitsyna I(2017)Detecting Decidable Classes of Finitely Ground Logic Programs with Function SymbolsACM Transactions on Computational Logic10.1145/314380418:4(1-42)Online publication date: 16-Nov-2017
https://dl.acm.org/doi/10.1145/3143804
Calautti MGreco SMolinaro CTrubitsyna I(2015)Logic program termination analysis using atom sizesProceedings of the 24th International Conference on Artificial Intelligence10.5555/2832581.2832645(2833-2839)Online publication date: 25-Jul-2015
https://dl.acm.org/doi/10.5555/2832581.2832645
Ben-Amram AGenaim S(2014)Ranking Functions for Linear-Constraint LoopsJournal of the ACM10.1145/262948861:4(1-55)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2629488
Riguzzi FSwift T(2014)Terminating Evaluation of Logic Programs with Finite Three-Valued ModelsACM Transactions on Computational Logic10.1145/262933715:4(1-38)Online publication date: 12-Sep-2014
https://dl.acm.org/doi/10.1145/2629337
Calautti MGreco STrubitsyna IPeña RSchrijvers T(2013)Detecting decidable classes of finitely ground logic programs with function symbolsProceedings of the 15th Symposium on Principles and Practice of Declarative Programming10.1145/2505879.2505883(239-250)Online publication date: 16-Sep-2013
https://dl.acm.org/doi/10.1145/2505879.2505883
Ben-Amram AGenaim S(2013)On the linear ranking problem for integer linear-constraint loopsACM SIGPLAN Notices10.1145/2480359.242907848:1(51-62)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429078
Ben-Amram AGenaim SGiacobazzi RCousot R(2013)On the linear ranking problem for integer linear-constraint loopsProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2429069.2429078(51-62)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2429069.2429078
Ben-Amram AGenaim SMasud A(2012)On the Termination of Integer LoopsACM Transactions on Programming Languages and Systems10.1145/2400676.240067934:4(1-24)Online publication date: 1-Dec-2012
https://dl.acm.org/doi/10.1145/2400676.2400679
Ströder TSchneider-Kamp PGiesl J(2010)Dependency triples for improving termination analysis of logic programs with cutProceedings of the 20th international conference on Logic-based program synthesis and transformation10.5555/2008282.2008294(184-199)Online publication date: 23-Jul-2010
https://dl.acm.org/doi/10.5555/2008282.2008294
Heizmann MJones NPodelski A(2010)Size-change termination and transition invariantsProceedings of the 17th international conference on Static analysis10.5555/1882094.1882098(22-50)Online publication date: 14-Sep-2010
https://dl.acm.org/doi/10.5555/1882094.1882098
Show More Cited By

Abstract

References

Cited By

Recommendations

Size-Change Termination, Monotonicity Constraints and Ranking Functions

Inference of monotonicity constraints in datalog programs

Inference of monotonicity constraints in Datalog programs

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations