Termination of floating-point computations. (English) Zbl 1102.65054
Summary: 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 \((\mathbb N, >)\); more recent works study termination of integer computations where the lack of well-foundedness of the integers has to be taken into account. Termination of computations involving floating-point numbers can be counterintuitive because of 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.
MSC:
| 65G50 | Roundoff error |
References:
| [1] | Aggoun, A., Chan, D., Dufresne, P., Falvey, E., Grant, H., Harvey, W., Herold, A., Geoffrey, M., Meier, M., Miller, D., Mudambi, S., Novello, S., Perez, B., van Rossum, E., Schimpf, J., Shen, K., Tsahageas, P. A. and de Villeneuve, D. H. (2001) ECLiPSe User Manual. Release 5.3, European Computer-Industry Research Centre, Munich and Centre for Planning and Resource Control, London. |
| [2] | Aït Ameur, Y. (1999) Refinement of rational end-points real numbers by means of floating-point numbers, Sci. Comput. Programming 33(2), 133–162. · Zbl 0946.68006 · doi:10.1016/S0167-6423(98)00008-2 |
| [3] | Aït Ameur, Y., Cros, P., Falcón, J. J. and Gómez, A. (1992) An application of abstract interpretation to floating point arithmetic, in M. Billaud, P. Castéran, M.-M. Corsini, K. Musumbu and A. Rauzy (eds.), Actes WSA’92 Workshop on Static Analysis, Vols. 81/82 of Bigre, Atelier Irisa, IRISA, Campus de Beaulieu, pp. 205–212. |
| [4] | Apt, K. R. (1997) From Logic Programming to Prolog, Prentice-Hall Internat. Series in Comput. Sci., Prentice-Hall, Englewood Cliffs, NJ. |
| [5] | Apt, K. R., Marchiori, E. and Palamidessi, C. (1994) A declarative approach for first-order built-in’s in Prolog, Appl. Algebra Engrg. Comm. Comput. 5(3/4), 159–191. · Zbl 0815.68035 · doi:10.1007/BF01190828 |
| [6] | Apt, K. R. and Pedreschi, D. (1990) Studies in Pure Prolog: Termination, in J. W. Lloyd (ed.), Proc. Esprit Symp. on Comp. Logic, Springer-Verlag, Berlin, pp. 150–176. |
| [7] | Bagnara, R. (1999) Is ISO Prolog standard taken seriously?, Association for Logic Programming Newsletter 12(1), 10–12. |
| [8] | Benhamou, F., Bouvier, P., Colmerauer, A., Garetta, H., Giletta, B., Massat, J. L., Narboni, G. A., N’Dong, S., Pasero, R., Pique, J. F., Touravane abd Van Canegheme, M. and Vétillard, E. (1996) Le manuel de Prolog IV. PrologIA. |
| [9] | BIM (1995) ProLog by BIM, Release 4.1.0. |
| [10] | Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D. andRival, X. (2003) A static analyzer for large safety-critical software, in Proc. of the ACM SIGPLAN SIGSOFT Conf. on Programming Language Design and Implementation, ACM, pp. 196–207. · Zbl 1026.68514 |
| [11] | Bossi, A., Cocco, N. and Fabris, M. (1991) Proving termination of logic programs by exploiting term properties, in Proc. of CCPSD-TAPSOFT’91, Lecture Notes in Comput. Sci. 494, Springer-Verlag, Berlin, pp. 153–180. · Zbl 0967.68531 |
| [12] | Bruynooghe, M., Codish, M., Genaim, S. and Vanhoof, W. (2002) Reuse of results in termination analysis of typed logic programs, in M. V. Hermenegildo and G. Puebla (eds.), Static Analysis, 9th Internat. Symposium, Lecture Notes in Comput. Sci. 2477, Springer-Verlag, Berlin, pp. 477–492. · Zbl 1015.68505 |
| [13] | Bruynooghe, M., Vanhoof, W. and Codish, M. (2001) Pos(T): Analyzing dependencies in typed logic programs, in D. Bjørner, M. Broy and A. V. Zamulin (eds.), Perspectives of System Informatics, 4th Internat. Andrei Ershov Memorial Conference, PSI 2001, Akademgorodok, Novosibirsk, Russia, 2–6 July 2001, Revised Papers, Lecture Notes in Comput. Sci. 2244, Springer-Verlag, Berlin. · Zbl 1073.68557 |
| [14] | Bueno, F., Cabeza Gras, D., Carro, M., Hermenegildo, M. V., López-García, P. and Puebla, G. (1997) The Ciao Prolog system. Reference manual, Technical Report CLIP3/97.1, Technical University of Madrid. |
| [15] | Colón, M. A. and Sipma, H. B. (2001) Synthesis of linear ranking functions, in T. Margaria and W. Yi (eds.), Tools and Algorithms for the Construction and Analysis of Systems, 7th Internat. Conference, Lecture Notes in Comput. Sci. 2031, Springer-Verlag, Berlin, pp. 67–81. · Zbl 0978.68095 |
| [16] | Colussi, L., Marchiori, E. and Marchiori, M. (1995) On termination of constraint logic programs, in U. Montanari and F. Rossi (eds.), Principles and Practice of Constraint Programming – CP’95, Lecture Notes in Comput. Sci. 976, Springer-Verlag, Berlin, pp. 431–448. |
| [17] | Cousot, P. and Cousot, R. (1976) Static determination of dynamic properties of programs, in Proc. of the Second Internat. Symposium on Programming, Dunod, Paris, France, pp. 106–130. · Zbl 0393.68080 |
| [18] | Cousot, P. and Cousot, R. (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in Conf. Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, CA, ACM Press, New York, pp. 238–252. |
| [19] | Cousot, P. and Cousot, R. (2001) Verification of embedded software: Problems and perspectives, in: T. A. Henzinger and C. Meyer Kirsch (eds.), Embedded Software, Proc. of the First Internat. Workshop, EMSOFT 2001, Tahoe City, CA, USA, 8–10 October, 2001, Lecture Notes in Comput. Sci. 2211, Springer-Verlag, Berlin, pp. 97–113. · Zbl 1050.68522 |
| [20] | De Schreye, D. and Decorte, S. (1994) Termination of logic programs: The never-ending story, J. Logic Programming 19/20, 199–260. · Zbl 0820.68029 · doi:10.1016/0743-1066(94)90027-2 |
| [21] | De Schreye, D., Verschaetse, K. and Bruynooghe, M. (1992) A framework for analyzing the termination of definite logic programs with respect to call patterns, in I. Staff (ed.), Proc. of the Internat. Conf. on Fifth Generation Computer Systems, IOS Press, Amsterdam, pp. 481–488. · Zbl 0862.68016 |
| [22] | de Vries, F.-J. and Yamada, J. (1994) On termination of rewriting with real numbers, in M. Takeichi (ed.), Functional Programming II, Proc. of the 11th Annual Conference, Japan Society of Software Science and Technology, Kindai-kagaku-sya, pp. 233–247. |
| [23] | Decorte, S. and De Schreye, D. (1998) Termination analysis: Some practical properties of the norm and level mapping space, in J. Jaffar (ed.), Proc. of the 1998 Joint Internat. Conf. and Symposium on Logic Programming, MIT Press, Cambridge, MA, pp. 235–249. · Zbl 0949.68028 |
| [24] | Decorte, S., De Schreye, D. and Vandecasteele, H. (1999) Constraint-based termination analysis of logic programs, ACM TOPLAS 21(6), 1137–1195. · doi:10.1145/330643.330645 |
| [25] | Demmel, J. W. and Li, X. S. (1993) Faster numerical algorithms via exception handling, in E. E. Swartzlander, M. J. Irwin and J. Jullien (eds.), Proc. of the 11th IEEE Symposium on Computer Arithmetic, Windsor, Canada, IEEE Computer Soc. Press, Los Alamitos, CA, pp. 234–241. · Zbl 1073.68502 |
| [26] | Dershowitz, N., Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. (2001) A general framework for automatic termination analysis of logic programs, Appl. Algebra Engrg. Comm. Comput. 12(1/2), 117–156. · Zbl 0977.68052 · doi:10.1007/s002000100065 |
| [27] | Escardó, M. H. (1996) PCF extended with real numbers, Theoret. Comput. Sci. 162(1), 79–115. · Zbl 0871.68034 · doi:10.1016/0304-3975(95)00250-2 |
| [28] | Feret, J. (2004) Static analysis of digital filters, in D. A. Schmidt (ed.), Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Lecture Notes in Comput. Sci. 2986, Springer-Verlag, Berlin, pp. 33–48. · Zbl 1126.68347 |
| [29] | Flynn, M. and Oberman, S. (2001) Advanced Computer Arithmetic Design, Wiley, New York. |
| [30] | Fraley, R. and Walther, S. (1979) Proposal to eliminate denormalized numbers, ACM SIGNUM Newsletter 14(3S) (Special issue), 22–23. · doi:10.1145/1057520.1057523 |
| [31] | Frühwirth, T. W. (1998) Theory and practice of constraint handling rules. J. Logic Programming 37(1–3), Special Issue on Constraint Logic Programming, 95–138. · Zbl 0920.68029 · doi:10.1016/S0743-1066(98)10005-5 |
| [32] | Frühwirth, T. W. (2000) Proving termination of constraint solver programs, in K. R. Apt, A. C. Kakas, E. Monfroy and F. Rossi (eds.), New Trends in Constraints, Papers from the Joint ERCIM/Compulog-Net Workshop, Cyprus, Lecture Notes in Artificial Intelligence 1865, Springer-Verlag, Berlin. · Zbl 0987.68011 |
| [33] | Goldberg, D. (1991) What every computer scientist should know about floating point arithmetic, ACM Computing Surveys 23(1), 5–48; corrigendum: ACM Computing Surveys 23(3) (1991) 413. · doi:10.1145/103162.103163 |
| [34] | Goubault, E. (2001) Static analyses of the precision of floating-point operations, in P. Cousot (ed.), Static Analysis, 8th Internat. Symposium, Lecture Notes in Comput. Sci. 2126, Springer-Verlag, Berlin, pp. 234–259. · Zbl 0997.68518 |
| [35] | Goubault, E., Martel, M. and Putot, S. (2002) Asserting the precision of floating-point computations: A simple abstract interpreter, in D. Le Métayer (ed.), Programming Languages and Systems, 11th European Symposium on Programming, Lecture Notes in Comput. Sci. 2305, Springer-Verlag, Berlin, pp. 209–212. · Zbl 1077.68615 |
| [36] | Hauser, J. R. (1996) Handling floating-point exceptions in numeric programs, ACM Trans. Programming Languages Systems 18(2), 139–174. · doi:10.1145/227699.227701 |
| [37] | Holzbaur, C. (1995) OFAI CLP(Q,R) Manual, Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence, Vienna. |
| [38] | IEEE Standards Committee 754. (1985) IEEE Standard for binary floating-point arithmetic, ANSI/IEEE Standard 754-1985, Institute of Electrical and Electronics Engineers, New York. Reprinted in SIGPLAN Notices 22(2) (1987) 9–25. |
| [39] | ILOG. (2001) ILOG Solver 5.1 User’s Manual, ILOG s.a., http://www.ilog.com/. |
| [40] | ISO/IEC 10967 Committee. (1994) ISO/IEC 10967-1: 1994 Information technology – Language independent arithmetic – Part 1: Integer and floating point arithmetic, ISO/IEC. |
| [41] | ISO/IEC 10967 Committee. (2001) ISO/IEC 10967-2:2001 Information technology – Language independent arithmetic – Part 2: Elementary numerical functions, ISO/IEC. |
| [42] | ISO/IEC 13211 Committee. (1995) Information technology – Programming languages – Prolog – Part 1: General core, ISO/IEC. |
| [43] | IT Masters. (2000) MasterProLog Programming Environment, available at http://www.itmasters.com/. |
| [44] | Janssens, G. and Bruynooghe, M. (1992) Deriving descriptions of possible values of program variables by means of abstract interpretation, J. Logic Programming 13(2/3), 205–258. · Zbl 0776.68027 · doi:10.1016/0743-1066(92)90032-X |
| [45] | Janssens, G., Bruynooghe, M. and Englebert, V. (1994) Abstracting numerical values in CLP(H,N), in M. V. Hermenegildo and J. Penjam (eds.), Programming Language Implementation and Logic Programming, 6th Internat. Symposium, PLILP’94, Lecture Notes in Comput. Sci. 844, Springer-Verlag, Berlin, pp. 400–414. |
| [46] | Jones, N. D., Gomard, C. K. and Sestoft, P. (1993) Partial Evaluation and Automatic Program Generation, Prentice-Hall International, Englewood, Cliffs, NJ; available at http://www.dina.dk/\(\sim\)sestoft/pebook/. · Zbl 0875.68290 |
| [47] | Kowalski, R. A. and Kuehner, D. (1971) Linear resolution with selection function, Artificial Intelligence 2(3/4), 227–260 (Imperial College, London). · Zbl 0234.68037 · doi:10.1016/0004-3702(71)90012-9 |
| [48] | Leuschel, M., Martens, B. and De Schreye, D. (1998) Controlling generalisation and polyvariance in partial deduction of normal logic programs, ACM Trans. Programming Languages Systems 20(1), 208–258. · doi:10.1145/271510.271525 |
| [49] | Lindenstrauss, N. and Sagiv, Y. (1997) Automatic termination analysis of logic programs, in L. Naish (ed.), Proc. of the Fourteenth Internat. Conf. on Logic Programming, MIT Press, Cambridge, MA, pp. 63–77. |
| [50] | Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. (1998) Unfolding the mystery of Mergesort, in N. Fuchs (ed.), Proc. of the 7th Internat. Workshop on Logic Program Synthesis and Transformation, Lecture Notes in Comput. Sci. 1463, Springer-Verlag, Berlin, pp. 206–225. |
| [51] | Lloyd, J. W. (1987) Foundations of Logic Programming, Symbolic Computation, 2nd edn., Springer-Verlag, Berlin. · Zbl 0668.68004 |
| [52] | Martelli, A. and Monatanari, U. (1982) An efficient unification algorithm, ACM Trans. Programming Languages Systems (TOPLAS) 4(2), 258–282. · Zbl 0478.68093 · doi:10.1145/357162.357169 |
| [53] | Martin, J. C. and King, A. (2004) On the inference of natural level mappings, in M. Bruynooghe and K.-K. Lau (eds.), Program Development in Computational Logic, Lecture Notes in Comput. Sci. 3049, Springer-Verlag, Berlin. · Zbl 1080.68555 |
| [54] | MathWorks, T. (1999) MatLab Version 5.3.0.10183, The MathWorks http://www.mathworks.com/. |
| [55] | Mesnard, F. (1996) Inferring left-terminating classes of queries for constraint logic programs, in M. Maher (ed.), Proc. of the 1996 Joint Internat. Conf. and Syposium on Logic Programming, MIT Press, Cambridge, MA, pp. 7–21. |
| [56] | Mesnard, F., Neumerkel, U. and Payet, E. (2001) cTI: Un outil pour l’inférence de conditions optimales de terminaison pour Prolog, in P. Codognet (ed.), Dixièmes Journées Franco-phone de Programmation en Logique et Programmation par Contraintes, Hermés; available at http://www.univ-reunion.fr/\(\sim\)gcc/papers. |
| [57] | Mesnard, F. and Ruggieri, S. (2003) On proving left termination of constraint logic programs, ACM Trans. Comput. Logic 4(2), 207–259. · doi:10.1145/635499.635503 |
| [58] | Miné, A. (2004) Relational abstract domains for the detection of floating-point run-time errors, in D. A. Schmidt (ed.), Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Lecture Notes in Comput. Sci. 2986, Springer-Verlag, Berlin, pp. 3–17. · Zbl 1126.68353 |
| [59] | Monniaux, D. (2001) An abstract analysis of the probabilistic termination of programs, in P. Cousot (ed.), 8th Internat. Static Analysis Symposium (SAS’01), Springer-Verlag, Berlin, pp. 111–126. · Zbl 0997.68515 |
| [60] | Moore, R. E. (1966) Interval Analysis, Prentice-Hall, Englewood, Cliffs, NJ. · Zbl 0176.13301 |
| [61] | Older, W. and Benhamou, F. (1993) Programming in CLP(BNR), in Principles and Practice of Constraint Programming. |
| [62] | Payne, M. H. and Strecker, W. (1979) Draft proposal for a binary normalized floating point standard, ACM SIGNUM Newsletter 14(3S) (Special issue), 24–28. · doi:10.1145/1057520.1057524 |
| [63] | Pedreschi, D., Ruggieri, S. and Smaus, J.-G. (2002) Classes of terminating logic programs, Theory and Practice of Logic Programming 2(3), 369–418. · Zbl 1069.68537 · doi:10.1017/S1471068402001400 |
| [64] | Plümer, L. (1991) Automatic termination proofs for prolog programs operating on nonground terms, in Internat. Logic Programming Symposium, MIT Press, Cambridge, MA. |
| [65] | Potts, P. J., Edalat, A. and Escardó, M. H. (1997) Semantics of exact real arithmetic, in Proc. of the 12th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Soc. Press, pp. 248–257. |
| [66] | Puebla, G. and Hermenegildo, M. V. (1999) Abstract multiple specialization and its application to program parallelization, J. Logic Programming 41(2/3), 279–316. · Zbl 0944.68026 · doi:10.1016/S0743-1066(99)00031-X |
| [67] | Randimbivololona, F., Jones, N., Ferdinand, C., Wilhelm, R., Sagiv, M., Cousot, P., Goubault, E., Cousot, R., Deutsch, A. and Seidl, H. (2001) DAEDALUS: ValiDAtion of Critical softwarE by stAtic anaLysis and abstract teSting, available at http://dbs.cordis.lu/cordis-cgi/srchidadb?ACTION=D&SESSION=243382002-5-6&DOC=3&TBL=EN_PROJ&RCN=EP_RCN:60858&CALLER=PROJLINK_EN. |
| [68] | Robinson, J. A. (1965) A machine-oriented logic based on the resolution principle, J. ACM 12(1), 23–41. · Zbl 0139.12303 · doi:10.1145/321250.321253 |
| [69] | Ruggieri, S. (1997) Termination of constraint logic programs, in P. Degano, R. Gorrieri and A. Marchetti-Spaccamela (eds.), Automata, Languages and Programming, 24th Internat. Colloquium, ICALP’97, Lecture Notes in Comput. Sci. 1256, Springer-Verlag, Berlin, pp. 838–848. · Zbl 1401.68028 |
| [70] | Sahlin, D. (1993) Mixtus: An automatic partial evaluator for full Prolog, New Generation Computing 12(1), 7–51. · Zbl 0942.68516 · doi:10.1007/BF03038271 |
| [71] | Serebrenik, A. and De Schreye, D. (2001a) Inference of termination conditions for numerical loops in Prolog, in R. Nieuwenhuis and A. Voronkov (eds.), Logic for Programming, Artificial Intelligence, and Reasoning, 8th Internat. Conf., Proceedings, Lecture Notes in Comput. Sci. 2250, Springer-Verlag, Berlin, pp. 654–668. · Zbl 1275.68051 |
| [72] | Serebrenik, A. and De Schreye, D. (2001b) Non-transformational termination analysis of logic programs, based on general term-orderings, in K.-K. Lau (ed.), Logic Based Program Synthesis and Transformation, 10th Internat. Workshop, Selected Papers, Lecture Notes in Comput. Sci. 2042, Springer-Verlag, Berlin, pp. 69–85. · Zbl 1017.68033 |
| [73] | Serebrenik, A. and De Schreye, D. (2004) Inference of termination conditions for numerical loops in Prolog, Theory and Practice of Logic Programming 4(5/6), Special issue on Verification and Computational Logic, 719–751. · Zbl 1088.68029 · doi:10.1017/S1471068404002042 |
| [74] | SICS. (2004) SICStus User Manual, Version 3.11.1, Swedish Institute of Computer Science. |
| [75] | Skeel, R. (1992) Roundoff error and the patriot missile, SIAM News 25(4), 11. |
| [76] | Sohn, K. and Van Gelder, A. (1991) Termination detection in logic programs using argument sizes, in Proc. of the Tenth ACM SIGACT-SIGART-SIGMOD Symposium on Principles of Database Systems, ACM Press, New York, pp. 216–226. |
| [77] | Ullman, J. D. and Van Gelder, A. (1988) Efficient tests for top-down termination of logical rules, J. ACM 35(2), 345–373. · doi:10.1145/42282.42285 |
| [78] | United States General Accounting Office. (1992) Patriot Missile Defence. Software problem led to system failure at Dhahran, Saudi Arabia, No. 92-26 in GAO/IMTEC; also available at http://klabs.org/richcontent/Reports/Failure_Reports/patriot/patriot_gao_145960.pdf. |
| [79] | Van Hentenryck, P., Michel, L. and Deville, Y. (1997) Numerica: A Modeling Language for Global Optimization, MIT Press, Cambridge, MA. |
| [80] | Vanhoof, W. and Bruynooghe, M. (2002) When size does matter – Termination analysis for typed logic programs, in A. Pettorossi (ed.), Logic-based Program Synthesis and Transformation, 11th Internat. Workshop, LOPSTR 2001, Selected Papers, Lecture Notes in Comput. Sci. 2372, Springer-Verlag, Berlin, pp. 129–147. · Zbl 1073.68560 |
| [81] | Vellino, A. and Older, W. (1990) Extending Prolog with constraint arithmetic on real intervals, in IEEE Canadian Conf. on Electrical and Computer Engineering. |
| [82] | Verschaetse, K. and De Schreye, D. (1991) Deriving termination proofs for logic programs, using abstract procedures, in K. Furukawa (ed.), Logic Programming, Proc. of the Eigth Internat. Conference, MIT Press, Cambridge, MA, pp. 301–315. |
| [83] | Vuillemin, J. (1990) Exact real computer arithmetic with continued fractions, IEEE Trans. Comput. 39(8), 1087–1105. · doi:10.1109/12.57047 |
| [84] | Waterloo Maple, I. (2001) Maple 7, Consult http://www.maplesoft.com/. |
| [85] | Winsborough, W. (1992) Multiple specialization using minimal-function graph semantics, J. Logic Programming 13(2/3), 259–290. · Zbl 0776.68033 · doi:10.1016/0743-1066(92)90033-Y |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
