Peter Schneider-Kamp
Jürgen Giesl
Alexander Serebrenik
Abstract
There are two kinds of approaches for termination analysis of logic programs: “transformational” and “direct” ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a Term Rewrite System (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic programs. (Most of them are restricted to well-moded programs.) In this article we improve these transformations such that they become applicable for any definite logic program. To simulate the behavior of logic programs by TRSs, we slightly modify the notion of rewriting by permitting infinite terms. We show that our transformation results in TRSs which are indeed suitable for automated termination analysis. In contrast to most other methods for termination of logic programs, our technique is also sound for logic programming without occur check, which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.
- Aguzzi, G. and Modigliani, U. 1993. Proving termination of logic programs by transforming them into equivalent term rewriting systems. In Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'93). Lecture Notes in Computer Science, vol. 761. Springer, 114--124. Google Scholar
Digital Library
- Apt, K. R. and Etalle, S. 1993. On the unification free Prolog programs. In Proceedings of the Symposium on Mathematical Foundations of Computer Science (MFCS'93). Lecture Notes in Computer Science, vol. 711. Springer, 1--19. Google ScholarDigital Library
- Apt, K. R. 1997. From Logic Programming to Prolog. Prentice Hall, London. Google ScholarDigital Library
- Arts, T. and Zantema, H. 1995. Termination of logic programs using semantic unification. In Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'95). Lecture Notes in Computer Science, vol. 1048. Springer, 219--233. Google ScholarDigital Library
- Arts, T. and Giesl, J. 2000. Termination of term rewriting using dependency pairs. Theoretical Comput. Sci. 236, 133--178. Google ScholarDigital Library
- Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press. Google ScholarDigital Library
- Bossi, A., Cocco, N., and Fabris, M. 1992. Typed norms. In Proceedings of the European Symposium on Programming (ESOP'92). Lecture Notes in Computer Science, vol. 582. Springer, 73--92. Google ScholarDigital Library
- Bruynooghe, M., Demoen, B., Boulanger, D., Denecker, M., and Mulkers, A. 1996. A freeness and sharing analysis of logic programs based on a pre-interpretation. In Proceedings of the International Static Analysis Symposium (SAS'96). Lecture Notes in Computer Science, vol. 1145. Springer, 128--142. Google ScholarDigital Library
- Bruynooghe, M., Gallagher, J. P., and Van Humbeeck, W. 2005. Inference of well-typings for logic programs with application to termination analysis. In Proceedings of the International Static Analysis Symposium (SAS'05). Lecture Notes in Computer Science, vol. 3672. Springer, 35--51. Google ScholarDigital Library
- 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 Trans. Program. Lang. Syst. 29, 2, Article 10. Google ScholarDigital Library
- Charatonik, W. and Podelski, A. 1998. Directional type inference for logic programs. In Proceedings of the International Static Analysis Symposium (SAS'98). Lecture Notes in Computer Science, vol. 1503. Springer, 278--294.Google Scholar
- Codish, M. and Taboch, C. 1999. A semantic basis for termination analysis of logic programs. J. Logic Program. 41, 1, 103--123.Google ScholarCross Ref
- Codish, M., Lagoon, V., and Stuckey, P. 2005. Testing for termination with monotonicity constraints. In Proceedings of the International Conference on Logic Programming (ICLP'05). Lecture Notes in Computer Science, vol. 3668. Springer, 326--340. Google ScholarDigital Library
- Codish, M., Lagoon, V., Schachte, P., and Stuckey, P. 2006. Size-Change termination analysis in k-bits. In Proceedings of the European Symposium on Programming (ESOP'06). Lecture Notes in Computer Science, vol. 3924. Springer, 230--245. Google ScholarDigital Library
- Codish, M. 2007. Collection of benchmarks. http://lvs.cs.bgu.ac.il/~mcodish/suexec/terminweb/bin/terminweb.cgi?command=examples.Google Scholar
- Colmerauer, A. 1982. Prolog and infinite trees. In Logic Programming, K. L. Clark and S. Tarnlund, Eds. Academic Press, Oxford, UK.Google Scholar
- Cortesi, A. and File, G. 1999. Sharing is optimal. J. Logic Program. 38, 3, 371--386.Google ScholarCross Ref
- De Schreye, D. and Decorte, S. 1994. Termination of logic programs: The never-ending story. J. Logic Program. 19-20, 199--260.Google ScholarCross Ref
- De Schreye, D. and Serebrenik, A. 2002. Acceptability with general orderings. In Computational Logic: Logic Programming and Beyond. Essays in Honour of Robert A. Kowalski, Part I, A. C. Kakas and F. Sadri, Eds. Lecture Notes in Computer Science, vol. 2407. Springer, 187--210. Google ScholarDigital Library
- Decorte, S., De Schreye, D., and Fabris, M. 1993. Automatic inference of norms: A missing link in automatic termination analysis. In Proceedings of the International Logic Programming Symposium (ILPS'93). MIT Press, Boston, 420--436. Google ScholarDigital Library
- Dershowitz, N. 1987. Termination of rewriting. J. Symb. Comput. 3, 1-2, 69--116. Google ScholarDigital Library
- Endrullis, J., Waldmann, J., and Zantema, H. 2006. Matrix interpretations for proving termination of term rewriting. In Proceedings of the International Conference on Automated Reasoning (IJCAR'06). Lecture Notes in Artificial Intelligence, vol. 4130. 574--588. Google ScholarDigital Library
- Gallagher, J. P. and Puebla, G. 2002. Abstract interpretation over non-deterministic finite tree automata for set-based analysis of logic programs. In Proceedings of the International Sympsium on Practical Aspects of Declarative Languages (PADL'02). Lecture Notes in Computer Science, vol. 2257. Springer, 243--261. Google ScholarDigital Library
- Ganzinger, H. and Waldmann, U. 1993. Termination proofs of well-moded logic programs via conditional rewrite systems. In Proceedings of the International Workshop on Conditional and Typed Rewriting Systems (CTRS '92). Lecture Notes in Computer Science, vol. 656. Springer, 430--437. Google ScholarDigital Library
- Geser, A., Hofbauer, D., and Waldmann, J. 2004. Match-Bounded string rewriting systems. Appl. Algebra Engin. Comm. Comput. 15, 3-4, 149--171.Google ScholarDigital Library
- Giesl, J., Thiemann, R., and Schneider-Kamp, P. 2005. The dependency pair framework: Combining techniques for automated termination proofs. In Proceedings of the International Conference on Logic Programming Artificial Intelligence and Reasoning (LPAR'04). Lecture Notes in Artificial Intelligence, vol. 3452. Springer, 301--331.Google Scholar
- Giesl, J., Schneider-Kamp, P., and Thiemann, R. 2006a. AProVE 1.2: Automatic termination proofs in the DP framework. In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'06). Lecture Notes in Artificial Intelligence, vol. 4130. Springer, 281--286. Google ScholarDigital Library
- Giesl, J., Swiderski, S., Schneider-Kamp, P., and Thiemann, R. 2006b. Automated termination analysis for Haskell: From term rewriting to programming languages. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA'06). Lecture Notes in Computer Science, vol. 4098. Springer, 297--312. Google ScholarDigital Library
- Giesl, J., Thiemann, R., Schneider-Kamp, P., and Falke, S. 2006c. Mechanizing and improving dependency pairs. J. Autom. Reason. 37, 3, 155--203. Google ScholarDigital Library
- Hirokawa, N. and Middeldorp, A. 2005. Automating the dependency pair method. Inf. Comput. 199, 1-2, 172--199.Google ScholarCross Ref
- Huet, G. 1976. Resolution d'equations dans les langages d'ordre 1, 2,…,ω. PhD thesis.Google Scholar
- Janssens, G. and Bruynooghe, M. 1992. Deriving descriptions of possible values of program variables by means of abstract interpretation. J. Logic Program.13, 2-3, 205--258. Google ScholarDigital Library
- Krishna Rao, M. R. K., Kapur, D., and Shyamasundar, R. K. 1998. Transformational methodology for proving termination of logic programs. J. Logic Program. 34, 1, 1--41.Google ScholarCross Ref
- Lagoon, V. and Stuckey, P. J. 2002. Precise pair-sharing analysis of logic programs. In Proceedings of the ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'02). ACM Press, New York, 99--108. Google ScholarDigital Library
- Lagoon, V., Mesnard, F., and Stuckey, P. J. 2003. Termination analysis with types is more accurate. In Proceedings of the International Conference on Logic Programming (ICLP'03). Lecture Notes in Computer Science, vol. 2916. Springer, 254--268.Google Scholar
- Lescanne, P. 1983. Computer experiments with the REVE term rewriting system generator. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL'83). ACM Press, New York, 99--108. Google ScholarDigital Library
- Leuschel, M. and Sørensen, M. H. 1996. Redundant argument filtering of logic programs. In Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'96). Lecture Notes in Computer Science, vol. 1207. Springer, 83--103. Google ScholarDigital Library
- Lindenstrauss, N., Sagiv, Y., and Serebrenik, A. 1997. TermiLog: A system for checking termination of queries to logic programs. In Proceedings of the International Conference on Computer Aided Verification (CAV'97). Lecture Notes in Computer Science, vol. 1254. Springer, 444--447. Google ScholarDigital Library
- Lu, L. 2000. A precise type analysis of logic programs. In Proceedings of the ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'00). ACM Press, New York, 214--225. Google ScholarDigital Library
- Marche, C. and Zantema, H. 2007. The termination competition. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA'07). Lecture Notes in Computet Science, vol. 4533. Springer, 303--313. Google ScholarDigital Library
- Marchiori, M. 1994. Logic programs as term rewriting systems. In Proceedings of the International Conference on Algebraic and Logic Programming (ALP'94). Lecture Notes in Computer Science, vol. 850. Springer, 223--241. Google ScholarDigital Library
- Marchiori, M. 1996. Proving existential termination of normal logic programs. In Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST'96). Lecture Notes in Computer Science, vol. 1101. Springer, 375--390. Google ScholarDigital Library
- Martin, J., King, A., and Soper, P. 1996. Typed norms for typed logic programs. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'96). Lecture Notes in Computer Science, vol. 1207. Springer, 224--238. Google ScholarDigital Library
- Mesnard, F. and Ruggieri, S. 2003. On proving left termination of constraint logic programs. ACM Trans. Comput. Logic 4, 2, 207--259. Google ScholarDigital Library
- Mesnard, F. and Bagnara, R. 2005. cTI: A constraint-based termination inference tool for ISO-Prolog. Theory Pract. Logic Program. 5, 1-2, 243--257. Google ScholarDigital Library
- Mesnard, F. and Serebrenik, A. 2007. Recurrence with affine level mappings is P-time decidable for CLP(R). Theory Pract. Logic Program. 8, 1, 111--119. Google ScholarDigital Library
- Nguyen, M. T. and De Schreye, D. 2005. Polynomial interpretations as a basis for termination analysis of logic programs. In Proceedings of the International Conference on Logic Programming (ICLP'05). Lecture Notes in Computer Science, vol. 3668. Springer, 311--325. Google ScholarDigital Library
- Nguyen, M. T., Bruynooghe, M., De Schreye, D., and Leuschel, M. 2006. Program specialisation as a pre-processing step for termination analysis. In Proceedings of the 8th International Workshop on Termination (WST'06). 7--11. http://www.easychair.org/FLoC-06/WST-preproceedings.pdf.Google Scholar
- Nguyen, M. T. and De Schreye, D. 2007. Polytool: Proving termination automatically based on polynomial interpretations. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). Lecture Notes in Computer Science, vol. 4407. Springer, 210--218. Google ScholarDigital Library
- Nguyen, M. T., Giesl, J., Schneider-Kamp, P., and De Schreye, D. 2008. Termination analysis of logic programs based on dependency graphs. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07). Lecture Notes in Computer Science, vol. 4915. Springer, 8--22. Google ScholarDigital Library
- Ohlebusch, E., Claves, C., and Marche, C. 2000. TALP: A tool for the termination analysis of logic programs. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA'00). Lecture Notes in Computer Science, vol. 1833. Springer, 270--273. Google ScholarDigital Library
- Ohlebusch, E. 2001. Termination of logic programs: Transformational methods revisited. Appl. Algebra Engin. Comm. Comput. 12, 1-2, 73--116.Google ScholarCross Ref
- Payet, E. and Mesnard, F. 2006. Nontermination inference of logic programs. ACM Trans. Program. Lang. Syst. 28, 2, 256--289. Google ScholarDigital Library
- van Raamsdonk, F. 1997. Translating logic programs into conditional rewriting systems. In Proceedings of the International Conference on Logic Programming (ICLP'97). MIT Press, Boston, 168--182.Google Scholar
- Schneider-Kamp, P., Giesl, J., Serebrenik, A., and Thiemann, R. 2007. Automated termination analysis for logic programs by term rewriting. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). Lecture Notes in Computer Science, vol. 4407. Springer, 177--193. Google ScholarDigital Library
- Serebrenik, A. and De Schreye, D. 2003. Proving termination with adornments. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'03). Lecture Notes in Computer Science, vol. 3018. Springer, 108--109.Google Scholar
- Serebrenik, A. and De Schreye, D. 2004. Inference of termination conditions for numerical loops in Prolog. Theory Pract. Logic Program. 4, 5-6, 719--751. Google ScholarDigital Library
- Serebrenik, A. and De Schreye, D. 2005a. On termination of meta-programs. Theory Pract. Logic Program. 5, 3, 355--390. Google ScholarDigital Library
- Serebrenik, A. and De Schreye, D. 2005b. Termination of floating point computations. J. Autom. Reason. 34, 2, 141--177. Google ScholarDigital Library
- Smaus, J.-G. 2004. Termination of logic programs using various dynamic selection rules. In Proceedings of the International Conference on Logic Programming (ICLP '04). Lecture Notes in Computer Science, vol. 3132. Springer, 43--57.Google ScholarCross Ref
- Tamary, L. and Codish, M. 2004. Abstract partial evaluation for termination analysis. In Proceedings of the International Workshop on Termination (WST'04) 47--50. http://aib.informatik.rwth-aachen.de/2004/2004-07.pdf.Google Scholar
- TPDB. 2007. The termination problem data base 4.0. http://www.lri.fr/~marche/tpdb/.Google Scholar
- Vaucheret, C. and Bueno, F. 2002. More precise yet efficient type inference for logic programs. In Proceedings of the International Static Analysis Symposium (SAS '02). Lecture Notes in Computer Science, vol. 2477. Springer, 102--116. Google ScholarDigital Library
- Walther, C. 1994. On proving the termination of algorithms by machine. Artif. Intell. 71, 1, 101--157. Google ScholarDigital Library
- Zantema, H. 1995. Termination of term rewriting by semantic labelling. Fundam. Inform. 24, 1-2, 89--105. Google ScholarDigital Library
Index Terms
- Automated termination proofs for logic programs by term rewriting
Recommendations
Automated termination proofs for haskell by term rewriting
There are many powerful techniques for automated termination analysis of term rewriting. However, up to now they have hardly been used for real programming languages. We present a new approach which permits the application of existing techniques from ...
Termination prediction for general logic programs
We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination proof approaches. We introduce an idea of termination prediction, which predicts termination of ...
Termination prediction for general logic programs
We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination proof approaches. We introduce an idea of termination prediction, which predicts termination of ...
Reviews
German Vidal
Analyzing the termination of programs is perhaps one of the most active research topics in most declarative programming languages. Within the logic programming paradigm, one can find two different types of approaches to analyze termination: direct approaches that deal with logic programs without any preprocessing, and transformational approaches that first transform them to term rewriting systems, and then analyze the termination of these systems. The transformational approach is particularly interesting, because it allows one to reuse the huge body of techniques and tools for analyzing the termination of term rewriting systems, perhaps the one setting where a lot of effort has been devoted to this kind of research. In this paper, the authors follow the transformational approach. In contrast to previous approaches in the literature, they impose no restrictions on the logic programs to be analyzed. In addition, the analysis of the transformed term rewriting systems can easily be automated using existing techniques and tools, such as the system AProVE [1], one of the most successful termination provers for term rewriting systems. A key idea in this paper is the discovery that variables in a logic programming language can be seen as infinite terms in the term rewriting framework. This idea is then combined with the use of argument filtering to get rid of these infinite terms, so that the analysis essentially boils down to an ordinary termination analysis for term rewriting systems over finite terms. In conclusion, this is a must-read paper for anyone who is interested in the termination analysis of logic programming languages. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments