Hostname: page-component-7b7567c8c-mnklg Total loading time: 0 Render date: 2026-11-12T19:59:09.371Z Has data issue: false hasContentIssue false
  • English
  • Français

Polytool: Polynomial interpretations as a basis for termination analysis of logic programs

Published online by Cambridge University Press:  25 February 2010

MANH THANG NGUYEN,
DANNY DE SCHREYE,
JÜRGEN GIESL and
PETER SCHNEIDER-KAMP
MANH THANG NGUYEN
Affiliation:
Department of Computer Science, K. U. Leuven Celestijnenlaan 200A, B-3001, Heverlee, Belgium (e-mail: Danny.DeSchreye@cs.kuleuven.be)
DANNY DE SCHREYE
Affiliation:
Department of Computer Science, K. U. Leuven Celestijnenlaan 200A, B-3001, Heverlee, Belgium (e-mail: Danny.DeSchreye@cs.kuleuven.be)
JÜRGEN GIESL
Affiliation:
LuFG Informatik II, RWTH Aachen, Ahornstr. 55, 52074 Aachen, Germany (e-mail: giesl@informatik.rwth-aachen.de)
PETER SCHNEIDER-KAMP
Affiliation:
Department of Mathematics and Computer Science, University of Southern Denmark, Campusvej 55, DK-5230 Odense M, Denmark (e-mail: petersk@imada.sdu.dk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.

Keywords

termination analysisacceptabilitypolynomial interpretations

Information

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 11 , Issue 1 , January 2011, pp. 33 - 63
Copyright
Copyright © Cambridge University Press 2010

References

Apt, K. R. 1990. Logic programming. In Handbook of Theoretical Computer Science, Vol. B, Ed. van Leeuwen, Jan, MIT Press, 493–574.Google Scholar
Arts, T. and Giesl, J. 2000. Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 1–2, 133–178.Google Scholar
Borralleras, C., Lucas, S., Navarro-Marset, R., Rodríguez-Carbonell, E. and Rubio, A. 2009. Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In Proc. CADE ’09. Ed. Schmidt, Renate, LNAI, Springer-Verlag, vol. 5663, 294–305.Google Scholar
Bossi, A., Cocco, N. and Fabris, M. 1991 Proving termination of logic programs by exploiting term properties. In Proc. TAPSOFT ’91. Eds. Abramsky, S. and Maibaum, T., LNCS, Springer-Verlag, vol. 494, 153–180.CrossRefGoogle Scholar
Brauburger, J. and Giesl, J. 1998 Termination analysis by inductive evaluation. In Proc. CADE ’98. Eds. Kirchner, C. and Kirchner, H., LNAI, Springer-Verlag, vol. 1421, 254–269.Google Scholar
Bruynooghe, M., Codish, M., Gallagher, J. P., Genaim, S. and Vanhoof, W. 2007. Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems 29, 2, 10-es.Google Scholar
Bruynooghe, M., Gallagher, J. P. and Van Humbeeck, W. 2005. Inference of well-typings for logic programs with application to termination analysis. In Proc. SAS ’05. Eds. Hankin, C. and Siveroni, I., LNCS, Springer-Verlag, vol. 3672, 35–51.Google Scholar
Codish, M. and Taboch, C. 1999. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41, 1, 103–123.CrossRefGoogle Scholar
Contejean, E., Marché, C., Tomás, A. P. and Urbain, X. 2005. Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning 34, 4, 325–363.CrossRefGoogle Scholar
Decorte, S., De Schreye, D. and Fabris, M. 1993. Automatic inference of norms: A missing link in automatic termination analysis. In Proc. ILPS ’93. Ed. Miller, D., MIT Press, 420–436.Google Scholar
Decorte, S., De Schreye, D. and Vandecasteele, H. 1999. Constraint-based automatic termination analysis of logic programs. ACM Transactions on Programming Languages and Systems 21, 6, 1137–1195.CrossRefGoogle Scholar
Dershowitz, N. 1995. 33 examples of termination. In Proc. French Spring School in Theoretical Computer Science. Eds. Comon, H. and Jouannaud, J., LNCS, Springer-Verlag, vol. 909, 16–26.Google Scholar
Dershowitz, N., Lindenstrauss, N. and Sagiv, Y. 1997. What norms are useful for logic programs? In Proc. WST ’97. Transparencies available from URL: http://www.cs.huji.ac.il/~naomil/.Google Scholar
De Schreye, D. and Serebrenik, A. 2002. Acceptability with general orderings. In Computational Logic: Logic Programming and Beyond. Eds. Kakas, A. and Sadri, F., LNCS, Springer-Verlag, vol. 2407, 187–210.CrossRefGoogle Scholar
Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R. and Zankl, H. 2007. SAT solving for termination analysis with polynomial interpretations. In Proc. SAT ’07. Eds. Marques-Silva, J., Sakallah, K., LNCS, Springer-Verlag, vol. 4501, 340–354.Google Scholar
Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R. and Zankl, H. 2008. Maximal termination. In Proc. RTA ’08, 110–125.Google Scholar
Gallagher, J. P., Henriksen, K. S. and Banda, G. 2005. Techniques for scaling up analyses based on pre-interpretations. In Proc. ICLP ’05. Eds. Gabbrielli, M. and Gupta, G., LNCS, Springer-Verlag, vol. 3668, 280–296.Google Scholar
Giesl, J., Schneider-Kamp, P. and Thiemann, R. 2006a. AProVE 1.2: Automatic termination proofs in the dependency pair framework. In Proc. IJCAR ’06. Eds. Furbach, U. and Shankar, N., LNAI, Springer-Verlag, vol. 4130, 281–286.Google Scholar
Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S. 2006b. Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37, 3, 155–203.CrossRefGoogle Scholar
Giesl, J., Thiemann, R., Swiderski, S. and Schneider-Kamp, P. 2007. Proving termination by bounded increase. In Proc. CADE ’07. Ed. Pfenning, F., LNAI, Springer-Verlag, vol. 4603, 443–459.Google Scholar
Heaton, A., Abo-Zaed, M., Codish, M. and King, A. 2000. A simple polynomial groundness analysis for logic programs. Journal of Logic Programming 45, 1–3, 143–156.Google Scholar
Hirokawa, N. and Middeldorp, A. 2005. Automating the dependency pair method. Information and Computation 199, 1–2, 172–199.Google Scholar
Hong, H. and Jakuš, D. 1998. Testing positiveness of polynomials. Journal of Automated Reasoning 21, 1, 23–38.Google Scholar
Janssens, G. and Bruynooghe, M. 1992. Deriving descriptions of possible values of program variables by means of abstract interpretation. Journal of Logic Programming 13, 2–3, 205–258.Google Scholar
Lankford, D. S. 1979. On Proving Term Rewriting Systems are Noetherian. Tech. Rep., Mathematics Department, Louisiana Tech University, Ruston, LA.Google Scholar
Lindenstrauss, N. 2000. TermiLog: Termination analyzer for logic programs. URL: http://www.cs.huji.ac.il/~naomil/termilog.php.Google Scholar
Lindenstrauss, N. and Sagiv, Y. 1997. Automatic termination analysis of logic programs. In Proc. ICLP ’97. Ed. Naish, L., MIT Press, 63–77.Google Scholar
Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. 2004. Proving termination for logic programs by the query-mapping pairs approach. In Program Development in Computational Logic. Eds. Bruynooghe, M. and Lau, K., LNCS, Springer-Verlag, vol. 3049, 453–498.CrossRefGoogle Scholar
Lloyd, J. W. 1987. Foundations of Logic Programming. Springer Verlag, Berlin.Google Scholar
Mesnard, F. and Bagnara, R. 2005. cTI: A constraint-based termination inference tool for ISO-Prolog. Theory and Practice of Logic Programming 5, 1–2, 243–257.Google Scholar
Nguyen, M. T. 2009 Termination Analysis: Crossing Paradigm Borders. Ph.D. thesis, Department of Computer Science, K. U. Leuven, Belgium.Google Scholar
Nguyen, M. T. and De Schreye, D. 2005. Polynomial interpretations as a basis for termination analysis of logic programs. In Proc. ICLP ’05. Eds. Gabbrielli, M. and Gupta, G., LNCS, Springer-Verlag, vol. 3668, 311–325. Extended version appeared as Technical report, Department of Computer Science, K. U. Leuven, Belgium, URL: http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW412.pdf.Google Scholar
Nguyen, M. T. and De Schreye, D. 2007. Polytool: Proving termination automatically based on polynomial interpretations. In Proc. LOPSTR ’06. Ed. Puebla, G., LNCS, Springer-Verlag, vol. 4407, 210–218. Extended version appeared as Technical report, Department of Computer Science, K. U. Leuven, Belgium, URL: http://www.cs.kuleuven.be/~manh/polytool/publications/tech-reports/reportCW442.pdf.Google Scholar
Nguyen, M. T., Giesl, J., Schneider-Kamp, P. and De Schreye, D. 2008. Termination analysis of logic programs based on dependency graphs. In Proc. LOPSTR ’07. Ed. King, A., LNCS, Springer-Verlag, vol. 4915, 8–22.Google Scholar
Ohlebusch, E., Claves, C. and Marché, C. 2000. TALP: A tool for the termination analysis of logic programs. In Proc. RTA ’00. Ed. Bachmair, L., LNCS, Springer-Verlag, vol. 1833, 270–273.Google Scholar
Schneider-Kamp, P., Giesl, J. and Nguyen, M. T. The dependency triple framework for termination of logic programs. In Proc. LOPSTR ’09. LNCS. Forthcoming.Google Scholar
Schneider-Kamp, P., Giesl, J., Serebrenik, A. and Thiemann, R. 2009. Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic 11, 1. Preliminary version appeared in Proc. LOPSTR ’06, Ed. G. Puebla, LNCS, Springer-Verlag, vol. 4407, pp. 117–193, 2007.Google Scholar
Serebrenik, A. 2003. Termination Analysis of Logic Programs. Ph.D. thesis, Department of Computer Science, K. U. Leuven, Belgium. URL: http://www.cs.kuleuven.ac.be/publicaties/doctoraten/cw/CW2003_02.abs.html.Google Scholar
Serebrenik, A. and De Schreye, D. 2003. Hasta-La-Vista: Termination analyser for logic programs. In Proc. WLPE ’03. Eds. Mesnard, F. and Serebrenik, A., 60–74.Google Scholar
Steinbach, J. 1992. Proving polynomials positive. In Proc. FSTTCS ’92. Ed. Shyamasundar, R., LNCS, Springer-Verlag, vol. 652, 18–20.Google Scholar
Taboch, C., Genaim, S. and Codish, M. 2002. TerminWeb: Semantics-based termination analyser for logic programs. URL: http://www.cs.bgu.ac.il/~mcodish/TerminWeb.Google Scholar
Verschaetse, K. and De Schreye, D. 1991. Deriving termination proofs for logic programs, using abstract procedures. In Proc. ICLP ’91. Ed. Furukawa, K., MIT Press, 301–315.Google Scholar