Skip to main content
SpringerLink
Log in

Termination analysis for Mercury

  • Logic Programming II
  • Conference paper
  • First Online:
Static Analysis (SAS 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1302))

Included in the following conference series:

Abstract

Since the late eighties, much progress has been made in the theory of termination analysis for logic programs. However, the practical significance of much of this work is hard to judge, since experimental evaluations rarely get published. Here we describe and evaluate a termination analyzer for Mercury, a strongly typed and moded logic-functional programming language. Mercury's high degree of referential transparency and the guaranteed availability of reliable mode information simplify termination analysis. Our analyzer uses a variant of a method developed by Plümer. It deals with full Mercury, including modules and I/O. In spite of these obstacles, it produces state-of-the-art termination information, while having a negligible impact on the running time of the compiler of which it is part, even for large programs.

This research has been supported by ARC grant no. A49601340.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt and D. Pedreschi. Reasoning about termination of pure Prolog programs. In Advances in Logic Programming Theory, pages 183–229. Oxford University Press, 1994.

    Google Scholar 

  2. Michel Berkelaar. lp-solve v. 2.0. ftp://ftp.es.ele.tue.ul/pub/lp-solve.

    Google Scholar 

  3. Roland N. Bol. Loop Checking in Logic Programming. PhD thesis, University of Amsterdam, The Netherlands, 1991.

    Google Scholar 

  4. 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, Proc. TAPSOFT'91, vol. 2, LNCS 494, pages 153–180. Springer-Verlag, 1991.

    Google Scholar 

  5. A. Bossi, N. Cocco, and M. Fabris. Typed norms. In B. Krieg-Brückner, editor, Proc. ESOP'92, LNCS 582, pages 73–92. Springer-Verlag, 1992.

    Google Scholar 

  6. A. Brodsky and Y. Sagiv. Inference of inequality constraints in logic programs (extended abstract). In Proc. Tenth ACM Symp. Principles of Database Systems, pages 227–240. ACM Press, 1991.

    Google Scholar 

  7. F. Bueno, M. Garcia de la Banda, and M. Hermenegildo. Effectiveness of global analysis in strict independence-based automatic program parallelization. In M. Bruynooghe, editor, Proc. ILPS'94, pages 320–336. MIT Press, 1994.

    Google Scholar 

  8. Danny De Schreye and Stefaan Decorte. Termination of logic programs: The neverending story. Journal of Logic Programming, 19/20:199–260, 1994.

    Google Scholar 

  9. Gerhard Gröger and Lutz Plümer. Handling of mutual recursion in automatic termination proofs for logic programs. In K. Apt, editor, Proc. Joint Int. Conf. Symp. Logic Programming, pages 336–350. MIT Press, 1992.

    Google Scholar 

  10. F. Henderson, T. Conway, Z. Somogyi, and D. Jeffery. The Mercury language reference manual. Technical Report 96/10, Dept. of Computer Science, University of Melbourne, 1996.

    Google Scholar 

  11. N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of logic programs (with detailed experimental results). http://www.cs.huji.ac.il/-naomil; Shorter version to appear in L. Naish, editor, Logic Programming: Proc. Int. Conf. Logic Programming, MIT Press, 1997.

    Google Scholar 

  12. Lutz Plümer. Termination Proofs for Logic Programs. LNAI 446. Springer-Verlag, 1990.

    Google Scholar 

  13. Kirack Sohn and Allen Van Gelder. Termination detection in logic programs using argument sizes (extended abstract). In Proc. Tenth ACM Symp. Principles of Database Systems, pages 216–226. ACM Press, 1991.

    Google Scholar 

  14. C. Speirs, Z. Somogyi, and H. Søndergaard. Termination analysis for Mercury. Technical Report 97/9, Dept. of Computer Science, University of Melbourne, 1997. http://www.cs.mu.oz.au/publications/tr_db/mu_97_09.ps.gz.

    Google Scholar 

  15. Jeffrey D. Ullman and Allen Van Gelder. Efficient tests for top-down termination of logical rules. Journal of the ACM, 35(2):345–373, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, University of Melbourne, 3052, Parkville, Vic., Australia

    Chris Speirs, Zoltan Somogyi & Harald Søndergaard

Authors
  1. Chris Speirs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zoltan Somogyi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Harald Søndergaard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Pascal Van Hentenryck

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Speirs, C., Somogyi, Z., Søndergaard, H. (1997). Termination analysis for Mercury. In: Van Hentenryck, P. (eds) Static Analysis. SAS 1997. Lecture Notes in Computer Science, vol 1302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032740

Download citation

  • DOI: https://doi.org/10.1007/BFb0032740

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63468-3

  • Online ISBN: 978-3-540-69576-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation