Skip to main content
SpringerLink
Log in

Inference of Termination Conditions for Numerical Loops in Prolog

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2250))

Abstract

Numerical computations form an essential part of almost any real-world program. Clearly, in order for a termination analyser to be of practical use it should contain a mechanism for inferring termination of such computations. However, this topic attracted less attention of the research community. In this work we concentrate on automatic termination inference for logic programs depending on numerical computations. Dershowitz et al. [8] showed that termination of general numerical computations, for instance on floating point numbers, may be counter-intuitive, i.e., the observed behaviour does not necessarily coincide with the theoretically expected one. Thus, we restrict ourselves to integer computations only.

supported by GOA: “LP +: a second generation logic programming language”.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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 Int. Series in Computer Science. Prentice Hall, 1997.

    Google Scholar 

  2. K.R. Apt, E. Marchiori, and C. Palamidessi. A declarative approach for first order built-in’s in prolog. Applicable Algebra in Engineering, Communication and Computation, 5(3/4):159–191, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  3. A. Bossi and N. Cocco. Preserving universal temination through unfold/fold. In G. Levi and M. Rodrýguez-Artalejo, editors, Algebraic and Logic Programming,pages 269–286. Springer Verlag, 1994. LNCS 850.

    Google Scholar 

  4. L. Colussi, E. Marchiori, and M. Marchiori. On termination of constraint logic programs. In U. Montanari and F. Rossi, editors, Principles and Practice of Constraint Programming-CP’95,, pages 431–448. Springer Verlag, 1995. LNCS 976.

    Google Scholar 

  5. D. De Schreye, K. Verschaetse, and M. Bruynooghe. A framework for analyzing the termination of definite logic programs with respect to call patterns. In I. Sta., editor, Proc. of the Int. Conf. on Fifth Generation Computer Systems., pages 481–488. IOS Press, 1992.

    Google Scholar 

  6. S. Decorte, D. De Schreye. Termination analysis: some practical properties of the norm and level mapping space. In J. Jafar, editor, Proc. of the 1998 Joint Int.Conf. and Symp. on Logic Programming, pages 235–249. MIT Press, June 1998.

    Google Scholar 

  7. S. Decorte, D. De Schreye, and H. Vandecasteele. Constraint-based termination analysis of logic programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 21(6):1137–1195, November 1999.

    Article  Google Scholar 

  8. N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing, 12(1–2):117–156, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  9. N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of logic programs.In L. Naish, editor, Proc. of the Fourteenth Int. Conf. on Logic Programming, pages 63–77. MIT Press, July 1997.

    Google Scholar 

  10. F. Mesnard. Inferring left-terminating classes of queries for constraint logic programs.In M. Maher, editor, Proc. JICSLP’96, pages 7–21. The MIT Press, 1996.

    Google Scholar 

  11. C. Pollard and I. A. Sag. Head-driven Phrase Structure Grammar. The University of Chicago Press, 1994.

    Google Scholar 

  12. S. Ruggieri. Verification and validation of logic programs. PhD thesis, Universitá di Pisa, 1999.

    Google Scholar 

  13. A. Serebrenik and D. De Schreye. Inference of termination conditions for numerical loops. Technical Report CW 308, Departement Computerwetenschappen,K.U.Leuven, Leuven, Belgium, 2001.

    Google Scholar 

  14. A. Serebrenik and D. De Schreye. Non-transformational termination analysis of logic programs, based on general term-orderings. In K.-K. Lau, editor, Logic BasedProgram Synthesis and Transformation 10th International Workshop, Selected Papers, volume 2042 of Lecture Notes in Computer Science, pages 69–85. Springer Verlag, 2001.

    Google Scholar 

  15. L. Sterling and E. Shapiro. The Art of Prolog. The MIT Press, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, K.U. Leuven Celestijnenlaan 200A, B-3001, Heverlee, Belgium

    Alexander Serebrenik & Danny De Schreye

Authors
  1. Alexander Serebrenik
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Danny De Schreye
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Software, Technical University of Catalonia, Jordi Girona 1, 08034, Barcelona, Spain

    Robert Nieuwenhuis

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Serebrenik, A., De Schreye, D. (2001). Inference of Termination Conditions for Numerical Loops in Prolog. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_45

Download citation

  • DOI: https://doi.org/10.1007/3-540-45653-8_45

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42957-9

  • Online ISBN: 978-3-540-45653-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation