Reuse of Results in Termination Analysis of Typed Logic Programs

  • Maurice Bruynooghe
  • Michael Codish
  • Samir Genaim
  • Wim Vanhoof
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


Recent works by the authors address the problem of automating the selection of a candidate norm for the purpose of termination analysis. These works illustrate a powerful technique in which a collection of simple type-based norms, one for each data type in the program, are combined together to provide the candidate norm. This paper extends these results by investigating type polymorphism. We show that by considering polymorphic types we reduce, without sacrificing precision, the number of type-based norms which should be combined to provide the candidate norm. Moreover, we show that when a generic polymorphic typed program component occurs in one or more specific type contexts, we need not reanalyze it. All of the information concerning its termination and its effect on the termination of other predicates in that context can be derived directly from the context independent analysis of that component based on norms derived from the polymorphic types.


Logic Program Function Symbol Type Information Type Rule Type List 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K. R. Apt. Introduction to logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 495–574. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.Google Scholar
  2. 2.
    A. Bossi, N. Cocco, S. Etalle and S. Rossi. On modular termination proofs of general logic programs. Theory and Practice of Logic Programming, 2(3):263–291, 2002.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    A. Bossi, N. Cocco, and M. Fabris. Proving termination of logic programs by exploiting term properties. In S. Abramsky and T.S.E. Maibaum, editors, Proceedings of Tapsoft 1991, volume 494 of Lecture Notes in Computer Science, pages 153–180. Springer-Verlag, Berlin, 1991.Google Scholar
  4. 4.
    A. Bossi, N. Cocco, and M. Fabris. Typed norms. In B. Krieg-Brückner, editor, Proceeedings ESOP’ 92, volume 582 of Lecture Notes in Computer Science, pages 73–92. Springer-Verlag, Berlin, 1992.Google Scholar
  5. 5.
    M. Bruynooghe, M. Codish, S. Genaim, and W. Vanhoof. Reuse of results in termination analysis of typed logic programs. Technical Report, July, 2002.Google Scholar
  6. 6.
    M. Bruynooghe, W. Vanhoof, and M. Codish. Pos(t): Analyzing dependencies in typed logic programs. In Perspectives of System Informatics, 4th International Andrei Ershov Memorial Conference, (PSI). Lecture Notes in Computer Science, vol. 2244. Springer-Verlag, 406–420.Google Scholar
  7. 7.
    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.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    D. De Schreye, C. Verschaetse, and M. Bruynooghe. A framework for analysing the termination of definite logic programs with respect to call patterns. In ICOT, editor, Proc. of the Fifth Generation Computer Systems, FGCS92, pages 481–488. ICOT, 1992.Google Scholar
  9. 9.
    S. Decorte, D. De Schreye, and H. Vandecasteele. Constraint based automatic termination analysis of Logic Programs. ACM Trans. Program. Lang. Syst., 21(6):1137–1195, November 1999.Google Scholar
  10. 10.
    S. Decorte and D. De Schreye. Demand-driven and constraint-based automatic left-termination analysis for logic programs. In Naish [24], pages 78–92.Google Scholar
  11. 11.
    S. Decorte, D. De Schreye, and M. Fabris. Automatic inference of norms: A missing link in automatic termination analysis. In D. Miller, editor, Logic Programmin-Proceedings of the 1993 International Symposium, pages 420–436, Vancouver, Canada, 1993. MIT Press.Google Scholar
  12. 12.
    S. Decorte, D. De Schreye, and M. Fabris. Integrating types in termination analysis. Technical Report CW 222, K.U.Leuven, Department of Computer Science, January 1996.Google Scholar
  13. 13.
    J. Gallagher and G. Puebla. Abstract Interpretation over Non-Deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs. In Shriram Krishna-murthi and C. R. Ramakrishnan, editors, Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19–20, 2002, volume 2257 of Lecture Notes in Computer Science, pages 243–261. Springer, 2002.Google Scholar
  14. 14.
    S. Genaim, M. Codish, J. Gallagher, and V. Lagoon. Combining norms to prove termination. In Agostino Cortesi, editor, Third International Workshop on Verification, Model Checking and Abstract Interpretation, volume 2294 of Lecture Notes in Computer Science, pages 126–138. Springer-Verlag, January 2002.CrossRefGoogle Scholar
  15. 15.
    R. Giacobazzi, S. K. Debray, and G. Levi. Generalized semantics and abstract interpretation for constraint logic programs. The Journal of Logic Programming, 25(3):191–247, Dec. 1995.Google Scholar
  16. 16.
    A. King, K. Shen, and F. Benoy. Lower-bound time-complexity analysis of logic programs. In Jan Maluszynski, editor, International Symposium on Logic Programming, pages 261–276. MIT Press, November 1997.Google Scholar
  17. 17.
    V. Lagoon and P. Stuckey. A framework for analysis of typed logic programs. In FLOPS, volume 2024 of Lecture Notes in Computer Science, pages 296–310. Springer-Verlag, Berlin, 2001.Google Scholar
  18. 18.
    N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of logic programs. In Naish [24], pages 63–77.Google Scholar
  19. 19.
    J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 2 nd edition, 1987.zbMATHGoogle Scholar
  20. 20.
    K. Marriott and H. Søndergaard. Precise and efficient groundness analysis for logic programs. ACM Letters on Programming Languages and Systems, 2(1–4):181–196, 1993.CrossRefGoogle Scholar
  21. 21.
    J. Martin and A. King. Typed norms for typed logic programs. In Logic Program Synthesis and Transformation. Springer-Verlag, August 1996. Available at
  22. 22.
    F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logi programs. In Static Analysis Symposium, 2001.Google Scholar
  23. 23.
    A. Mycroft and R.A. O’Keefe. A Polymorphic Type System for Prolog. Artificial Intelligence 23(3): 295–307 1984.zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    L. Naish, editor. Proceedings of Fourteenth International Conference on Logic Programming, Leuven (Belgium), 1997. The MIT press.Google Scholar
  25. 25.
    Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 29(1–3):17–64, October–November 1996.Google Scholar
  26. 26.
    W. Vanhoof and M. Bruynooghe. When size does matter-Termination analysis for typed logic programs. Logic Based Program Synthesis and Transformation, LOPSTR 2001, Revised Papers, LNCS, Springer 2002. To appear.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Maurice Bruynooghe
    • 1
  • Michael Codish
    • 2
  • Samir Genaim
    • 2
  • Wim Vanhoof
    • 1
  1. 1.Department of Computer ScienceKatholieke Universiteit LeuvenHeverleeBelgium
  2. 2.Department of Computer ScienceBen-Gurion University of the NegevBeer-ShevaIsrael

Personalised recommendations