Abstract
Proofs of termination typically proceed by mapping program states to a well founded domain and showing that successive states of the computation are mapped to elements decreasing in size. Automated termination analysers for logic programs achieve this by measuring and comparing the sizes of successive calls to recursive predicates. The size of the call is measured by a level mapping that in turn is based on a norm on the arguments of the call. A norm maps a term to a natural number. The choice of the norm is crucial for the ability to prove termination. For some programs a fairly complex norm is required. The automated selection of an appropriate norm is a missing link in this research domain and is addressed in this paper. Our proposal is to use the type of a predicate to generate a number of simple norms and to try them in turn for proving the termination of the predicate. Given a term of a certain type, we consider a norm for each of its subtypes, a norm that counts the number of subterms of the term that are of the considered subtype.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Florence Benoy and Andy King. Inferring argument size relationships with CLP(R). In John P. Gallagher, editor, Logic Programming Synthesis and Transformation, LOPSTR’96, Proceedings, volume 1207 of LNCS, pages 204–223, 1997.
Annalisa Bossi, Nicoletta Cocco, and Massimo Fabris. Typed norms. In Bernd Krieg-Brückner, editor, ESOP’92, 4th European Symposium on Programming, Proceedings, volume 582 of LNCS, pages 73–92. Springer, 1992.
Maurice Bruynooghe, Wim Vanhoof, and Michael Codish. Pos(T): Analyzing dependencies in typed logic programs. In Dines Bjørner, Manfred Broy, and Alexander V. Zamulin, editors, Perspectives of System Informatics, PSI 2001, Revised Papers, volume 2244 of LNCS, pages 406–420. Springer, 2001.
Francisco Bueno, Maria J. García de la Banda, Manuel V. Hermenegildo, Kim Marriott, German Puebla, and Peter J. Stuckey. A model for inter-module analysis and optimizing compilation. In Kung-Kiu Lau, editor, Logic Based Program Synthesis and Transformation, LOPSTR 2000, Selected Papers, volume 2042 of LNCS, pages 86–102. Springer-Verlag, 2000.
Michael Codish and Cohavit Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming, 41(1):103–123, 1999.
Patrick Cousot and Nicholas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth annual ACM Symposium on Principles of Programming Languages, pages 84–96. ACM, 1978.
Danny De Schreye, Kristof Verschaetse, and Maurice Bruynooghe. A framework for analysing the termination of definite logic programs with respect to call patterns. In ICOT Staff, editor, Proc. of the Fifth Generation Computer Systems, FGCS92, pages 481–488. IOS Press, 1992.
Saumya K. Debray, Pedro López García, Manuel V. Hermenegildo, and Nai-Wei Lin. Estimating the Computational Cost of Logic Programs. In Baudouin Le Charlier, editor, Static Analysis, SAS’94, Proceedings, volume 864 of LNCS, pages 255–265. Springer Verlag, 1994. Invited Talk.
Stefaan Decorte, Danny De Schreye, and Massimo Fabris. Exploiting the power of typed norms in automatic inference of interargument relations. Report CW 246, Department of Computer Science, K.U. Leuven, Leuven, Belgium, January 1997.
Stefaan Decorte, Danny De Schreye, and Henk Vandecasteele. Constraint based automatic termination analysis of Logic Programs. ACM Transactions on Programming Languages and Systems, 21(6):1137–1195, November 1999.
Stefaan Decorte, Danny de Schreye, and Massimo Fabris. Automatic inference of norms: A missing link in automatic termination analysis. In Logic Programming-Proceedings of the 1993 International Symposium, pages 420–436. MIT Press, 1993.
N. Dershowitz, N. Lindenstrauss, Yehoshua Sagiv, and Alexander Serebrenik. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing, 12(1–-2):117–156, 2001.
John Gallagher and German Puebla. Abstract interpretation over nondeterministic finite tree automata for set-based analysis of logic programs. In Shriram Krishnamurthi and C. R. Ramakrishnan, editors, Practical Aspects of Declarative Languages, PADL 2002, Proceedings, volume 2257 of LNCS, pages 243–261. Springer Verlag, 2002.
Samir Genaim, Michael Codish, John Gallagher, and Vitaly Lagoon. Combining norms to prove termination. In A. Cortesi, editor, Verification, Model Checking and Abstract Interpretation, Third Int. Workshop, VMCAI 2002, Revised Papers, volume 2294 of LNCS, pages 126–138. Springer-Verlag, 2002.
Gerda Janssens and Maurice Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. J. Logic programming, 13(2&3):205–258, 1992.
Vitaly Lagoon and Peter J. Stuckey. A framework for analysis of typed logic programs. In Herbert Kuchen and Kazunori Ueda, editors, Functional and Logic Programming, FLOPS 2001, Proceedings, volume 2024 of LNCS, pages 296–310. Springer, 2001.
Naomi Lindenstrauss and Yehoshua Sagiv. Automatic termination analysis of logic programs. In Lee Naish, editor, Logic Programming, Proceedings of the Fourteenth International Conference on Logic Programming, pages 63–77. MIT Press, 1997.
P. Lopez, M. Hermenegildo, and S. Debray. A methodology for granularity-based control of parallelism in logic programs. Journal of Symbolic Computation, 21(4/5/6):715–734, 1996.
Jonathan Martin, Andy King, and Paul Soper. Typed norms for typed logic programs. In John P. Gallagher, editor, Logic Programming Synthesis and Transformation, LOPSTR’96, Proceedings, volume 864 of LNCS, pages 224–238. Springer-Verlag, 1996.
Frédéric Mesnard and Ulrich Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In Patrick Cousot, editor, Static Analysis, SAS 2001, Proceedings, volume 2126 of LNCS, pages 93–110. Springer 2001, 2001.
G. Puebla and M. Hermenegildo. Some issues in analysis and specialization of modular Ciao-Prolog programs. In M. Leuschel, editor, Proceedings of the Workshop on Optimization and Implementation of Declarative Languages, 1999. In Electronic Notes in Theoretical Computer Science, Volume 30 Issue No. 2, Elsevier Science.
Danny De Schreye and Stefaan Decorte. Termination of logic programs: the never-ending story. The Journal of Logic Programming, 19 & 20:199–260, May 1994.
Jan-Georg Smaus, Patricia M. Hill, and Andy King. Mode analysis domains for typed logic programs. In Annalisa Bossi, editor, Logic Programming Synthesis and Transformation, LOPSTR’99, Selected Papers, volume 1817 of LNCS, pages 82–101. Springer-Verlag, 2000.
Zoltan Somogyi, Fergus Henderson, and Thomas Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 29(1-–3):17–64, 1996.
Jeffrey D. Ullman and Allen Van Gelder. Efficient tests for top-down termination of logical rules. JACM, 35(2):345–373, 1988.
W. Vanhoof. Binding-time analysis by constraint solving: a modular and higher-order approach for Mercury. In M. Parigot and A. Voronkov, editors, Logic for Programming and Automated Reasoning, LPAR2000, Proceedings, volume 1955 of LNAI, pages 399–416. Springer, 2000.
Wim Vanhoof and Maurice Bruynooghe. Binding-time annotations without binding-time analysis. In Robert Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2001, Proceedings, volume 2250 of LNCS, pages 707–722. Springer, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vanhoof, W., Bruynooghe, M. (2002). When Size Does Matter. In: Pettorossi, A. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2001. Lecture Notes in Computer Science, vol 2372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45607-4_8
Download citation
DOI: https://doi.org/10.1007/3-540-45607-4_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43915-8
Online ISBN: 978-3-540-45607-0
eBook Packages: Springer Book Archive