Skip to main content
SpringerLink
Log in

Unfolding the Mystery of Mergesort

  • Conference paper
  • First Online:
Logic Program Synthesis and Transformation (LOPSTR 1997)

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

Abstract

This paper outlines a fully automatic transformation for proving termination of queries to a class of logic programs, for which existing methods do not work directly. The transformation consists of creating adorned clauses and unfolding. In general, the transformation may improve termination behavior by pruning infinite branches from the LD-tree. Conditions are given under which the transformation preserves termination behavior. The work presented here has been done in the framework of the TermiLog system, and it complements the algorithms described in [12].

This research has been supported by grants from the Israel Science Foundation

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.

    Google Scholar 

  2. K. R. Apt and D. Pedreschi. Modular Termination Proofs for Logic and Pure Prolog Programs. In Advances in Logic Programming Theory, 183–229. Oxford University Press, 1994.

    Google Scholar 

  3. F. Benoy and A. King. Inferring Argument Size Relationships with CLP(R). LOPSTR’96. Springer Lecture Notes in Computer Science.

    Google Scholar 

  4. A. Bossi and N. Cocco. Preserving Universal Termination Through Unfold/Fold. ALP’94, 269–286. Springer Lecture Notes in Computer Science 850, 1994.

    Google Scholar 

  5. A. Brodsky and Y. Sagiv. Inference of Monotonicity Constraints in Datalog Programs. Proceedings of the Eighth ACM SIGACT-SIGART-SIGMOD Symposium on Principles of Database Systems, 1989, 190–199.

    Google Scholar 

  6. M. Codish and C. Taboch. A Semantic Basis for Termination Analysis of Logic Programs. ALP’97.

    Google Scholar 

  7. P. Cousot and R. Cousot. Abstract Interpretation and Application to Logic Programs. J. Logic Programming, 13:103–179, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  8. D. De Schreye and S. Decorte. Termination of Logic Programs: the Never-Ending Story. J. Logic Programming, 19–20:199–260, 1994.

    Google Scholar 

  9. M. Falaschi, G. Levi, M. Martelli and C. Palamidessi. Declarative Modeling of the Operational Behaviour of Logic Programs. Theoretical Computer Science, 69(3):289–318, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  10. A. Levy and Y. Sagiv. Constraints and Redundancy in Datalog. PODS’92, 67–80. ACM, 1992.

    Google Scholar 

  11. N. Lindenstrauss and Y. Sagiv. Checking Termination of Queries to Logic Programs. Available at http://www.cs.huji.ac.il/~naomil/

    Google Scholar 

  12. N. Lindenstrauss and Y. Sagiv. Automatic Termination Analysis of Logic Programs. ICLP’97. MIT Press, 1997.

    Google Scholar 

  13. N. Lindenstrauss and Y. Sagiv. Automatic Termination Analysis of Logic Programs (with Detailed Experimental Results). Available at http://www.cs.huji.ac.il/~naomil/

    Google Scholar 

  14. N. Lindenstrauss, Y. Sagiv, A. Serebrenik. TermiLog: A System for Checking Termination of Queries to Logic Programs. CAV’97. Springer Lecture Notes in Computer Science, 1997.

    Google Scholar 

  15. L. Plümer. Termination Proofs for Logic Programs. Springer Verlag, LNAI 446, 1990.

    Google Scholar 

  16. Y. Sagiv. A termination test for logic programs. In International Logic Programming Symposium. MIT Press, 1991.

    Google Scholar 

  17. SICStus Prolog User’s Manual, Release 3 # 3. Swedish Institute of Computer Science, 1995.

    Google Scholar 

  18. J. D. Ullman. Principles of Database and Knowledge-Base Systems, Vol. II. Computer Science Press, 1989.

    Google Scholar 

  19. J. D. Ullman and A. Van Gelder. Efficient Tests for Top-Down Termination of Logical Rules. Journal of the ACM, 35, 1988, 345–373.

    Article  Google Scholar 

  20. A. Van Gelder. Deriving Constraints among Argument Sizes in Logic Programs. Annals of Mathematics and Artificial Intelligence, 3:361–392, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  21. K. Verschaetse, S. Decorte and D. De Schreye. Automatic Termination Analysis. LOPSTR 92, ed. K. K. Lau and T. Clement. Workshops in Computing Series, Springer, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, Hebrew University, Jerusalem, Israel

    N. Lindenstrauss, Y. Sagiv & A. Serebrenik

Authors
  1. N. Lindenstrauss
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Y. Sagiv
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. A. Serebrenik
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Zurich, CH-8057, Zurich, Switzerland

    Norbert E. Fuchs

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lindenstrauss, N., Sagiv, Y., Serebrenik, A. (1998). Unfolding the Mystery of Mergesort . In: Fuchs, N.E. (eds) Logic Program Synthesis and Transformation. LOPSTR 1997. Lecture Notes in Computer Science, vol 1463. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49674-2_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-49674-2_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65074-4

  • Online ISBN: 978-3-540-49674-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation