On Termination of Logic Programs with Floating Point Computations

  • Alexander Serebrenik
  • Danny De Schreye
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


Numerical computations form an essential part of almost any real-world program. Traditional approaches to termination of logic programs are restricted to domains isomorphic to \( \mathcal{N} \) , more recent works study termination of integer computations. Termination of computations involving real numbers is cumbersome and counter-intuitive due to rounding errors and implementation conventions. We present a novel technique that allows us to prove termination of such computations. Our approach extends the previous work on termination of integer computations.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    ISO/IEC 10967-1:1994. Information technology—Language independent arithmetic—Part 1: Integer and floating point arithmetic. ISO/IEC, 1994.Google Scholar
  2. 2.
    ISO/IEC 13211-1:1995. Information technology—Programming languages— Prolog—Part 1: General core. ISO/IEC, 1995.Google Scholar
  3. 3.
    A. Aggoun, D. Chan, P. Dufresne, E. Falvey, H. Grant, W. Harvey, A. Herold, M. Geoffrey, M. Meier, D. Miller, S. Mudambi, S. Novello, B. Perez, E. van Rossum, J. Schimpf, K. Shen, P. A. Tsahageas, and D. H. de Villeneuve. ECL i PS e User Manual. Release 5.3, 2001.Google Scholar
  4. 4.
    Y. Aït Ameur, P. Cros, J. J. Falcón, and A. Gómez. An application of abstract interpretation to floating point arithmetic. In M. Billaud, P. Castéran, M.-M. Corsini, K. Musumbu, and A. Rauzy, editors, Actes WSA’92 Workshop on Static Analysis, volume 81–82 of Bigre, pages 205–212. Atelier Irisa, IRISA, Campus de Beaulieu, 1992.Google Scholar
  5. 5.
    K. R. Apt. From Logic Programming to Prolog. Prentice-Hall Int. Series in Computer Science. Prentice Hall, 1997.Google Scholar
  6. 6.
    K. R. Apt, E. Marchiori, and C. Palamidessi. A declarative approach for first-order built-inś in Prolog. Applicable Algebra in Engineering, Communication and Computation, 5(3/4):159–191, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    M. Brady. Open Prolog., 2001.
  8. 8.
    F. Bueno, D. Cabeza Gras, M. Carro, M. V. Hermenegildo, P. López-Garcýa, and G. Puebla. The Ciao Prolog system. Reference manual. Technical Report CLIP3/97.1, School of Computer Science, Technical University of Madrid (UPM), August 1997.
  9. 9.
    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
  10. 10.
    D. De Schreye, K. Verschaetse, and M. Bruynooghe. A framework for analyzing the termination of definite logic programs with respect to call patterns. In ICOT Staff, editor, Proc. of the Int. Conf. on Fifth Generation Computer Systems., pages 481–488. IOS Press, 1992.Google Scholar
  11. 11.
    S. Decorte and D. De Schreye. Termination analysis: some practical properties of the norm and level mapping space. In J. Jaffar, editor, Proc. of the 1998 Joint Int. Conf. and Symp. on Logic Programming, pages 235–249. MIT Press, June 1998.Google Scholar
  12. 12.
    S. Decorte, D. De Schreye, and H. Vandecasteele. Constraint-based termination analysis of logic programs. ACM TOPLAS, 21(6):1137–1195, November 1999.Google Scholar
  13. 13.
    N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A general framework for automatic termination analysis of logic programs. Appl. Alg. in Eng., Comm. and Computing, 12(1–2):117–156, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    M. H. Escard’o. PCF extended with real numbers. Theoretical Computer Science, 162(1):79–115, August 1996.Google Scholar
  15. 15.
    E. Goubault. Static analyses of the precision of floating-point operations. In P. Cousot, editor, Static Analysis, 8th International Symposium, volume 2126 of LNCS, pages 234–259. Springer Verlag, 2001.Google Scholar
  16. 16.
    E. Goubault, M. Martel, and S. Putot. Asserting the precision of floating-point computations: A simple abstract interpreter. In D. Le M’etayer, editor, Programming Languages and Systems, 11th European Symposium on Programming, volume 2305 of LNCS, pages 209–212. Springer Verlag, 2002.CrossRefGoogle Scholar
  17. 17.
    IEEE Standards Committee 754. IEEE Standard for binary floating-point arithmetic, ANSI/IEEE Standard 754-1985. Institute of Electrical and Electronics Engineers, New York, 1985. Reprinted in SIGPLAN Notices, 22(2):9–25, 1987.Google Scholar
  18. 18.
    IT Masters. MasterProLog Programming Environment., 2000.
  19. 19.
    G. Janssens, M. Bruynooghe, and V. Englebert. Abstracting numerical values in CLP(H, N). In M. V. Hermenegildo and J. Penjam, editors, Programming Language Implementation and Logic Programming, 6th International Symposium, PLILP’94, pages 400–414. Springer Verlag, 1994. volume 844 of LNCS.Google Scholar
  20. 20.
    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
  21. 21.
    P. J. Potts, A. Edalat, and M. H. Escard’o. Semantics of exact real arithmetic. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, pages 248–257. IEEE Computer Society Press, 1997.Google Scholar
  22. 22.
    S. Ruggieri. Verification and validation of logic programs. PhD thesis, Universit’a di Pisa, 1999.Google Scholar
  23. 23.
    A. Serebrenik and D. De Schreye. Inference of termination conditions for numerical loops in Prolog. In R. Nieuwenhuis and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, Proceedings, volume 2250 of LNCS, pages 654–668. Springer Verlag, 2001.CrossRefGoogle Scholar
  24. 24.
    A. Serebrenik and D. De Schreye. Non-transformational termination analysis of logic programs, based on general term-orderings. In K.-K. Lau, editor, LOPSTR 2001, 10th Int. Workshop, Selected Papers, volume 2042 of LNCS, pages 69–85. Springer Verlag, 2001.Google Scholar
  25. 25.
    Swedish Institute of Computer Science. SICStus User Manual. Version 3.9. 2002.Google Scholar
  26. 26.
    J. Vuillemin. Exact real computer arithmetic with continued fractions. IEEE Transactions on Computers, 39(8):1087–1105, August 1990.Google Scholar
  27. 27.
    Inc. Waterloo Maple. Maple 7, 2001.
  28. 28.
    W. Winsborough. Multiple specialization using minimal-function graph semantics. Journal of Logic Programming, 13(2/3):259–290, 1992.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Alexander Serebrenik
    • 1
  • Danny De Schreye
    • 1
  1. 1.Department of Computer ScienceK.U. LeuvenHeverleeBelgium

Personalised recommendations