Typed norms for typed logic programs

  • Jonathan C. Martin
  • Andy King
  • Paul Soper
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1207)


As typed logic programming becomes more mainstream, system building tools like partial deduction systems will need to be mapped from untyped languages to typed ones. It is important, however, when mapping techniques across that the new techniques should exploit the type system as much as possible. In this paper, we show how norms, which play a crucial role in termination analysis, can be generated from the prescribed types of a logic program. Interestingly, the types highlight restrictions of earlier norms and suggest how these norms can be extended to obtain some very general and powerful notions of norm which can be used to measure any term in an almost arbitrary way. We see our work on norm derivation as a contribution to the termination analysis of typed logic programs which, in particular, forms an essential part of offline partial deduction systems.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K.R. Apt and D. Pedreschi. Studies in pure Prolog: Termination. In Proceedings Esprit symposium on computational logic, pages 150–176, Brussels, November 1990. Springer-Verlag.Google Scholar
  2. 2.
    F. Benoy and A. King. Inferring argument size relations with CLP(\(\mathcal{R}\)). In LOP-STR'96. Springer-Verlag, 1996.Google Scholar
  3. 3.
    M. Bezem. Characterizing termination of logic programs with level mappings. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 69–80, Cleveland, Ohio, USA, 1989.Google Scholar
  4. 4.
    A. Bossi, N. Cocco, and M. Fabris. Typed norms. In ESOP'92, pages 73–92, 1992.Google Scholar
  5. 5.
    A. Bossi, N. Cocco, and M. Fabris. Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science, 124:297–328, 1994.Google Scholar
  6. 6.
    S. Decorte, D. de Schreye, and M. Fabris. Automatic inference of norms: A missing link in automatic termination analysis. In ILPS'93, pages 420–436, 1993.Google Scholar
  7. 7.
    S. Decorte, D. de Schreye, and M. Fabris. Exploiting the power of typed norms in automatic inference of interargument relations. Technical report, Dept. computer science, K.U.Leuven, 1994.Google Scholar
  8. 8.
    J. Gallagher and A. de Waal. Fast and precise regular approximations of logic programs. In ICLP'94, pages 599–613, 1994.Google Scholar
  9. 9.
    C. Gurr. A Self-Applicable Partial Evaluator for the Logic Programming Language Gödel. PhD thesis, University of Bristol, January 1994.Google Scholar
  10. 10.
    C. Gurr. Personal communication on the literature on termination analyses. September 1995.Google Scholar
  11. 11.
    P. M. Hill and J. W. Lloyd. The Gödel Programming Language. MIT Press, 1994.Google Scholar
  12. 12.
    G. Janssens and M. Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. J. Logic Programming, 13:205–258, 1992.MathSciNetGoogle Scholar
  13. 13.
    L. Plümer. Termination Proofs for Logic Programs. Springer-Verlag, 1990.Google Scholar
  14. 14.
    P. Van Hentenryck, A. Cortesi, and B. Le Charlier. Type Analysis of Prolog Using Type Graphs. In PLDI'94, pages 337–348. ACM Press, 1994.Google Scholar
  15. 15.
    P. Van Roy. A Prolog Compiler for the PLM. Master's thesis, Computer Science Division, University of California, Berkeley, 1984.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Jonathan C. Martin
    • 1
  • Andy King
    • 2
  • Paul Soper
    • 1
  1. 1.Department of Electronics and Computer ScienceUniversity of SouthamptonSouthamptonUK
  2. 2.Computing LaboratoryUniversity of Kent at CanterburyCanterburyUK

Personalised recommendations