Serebrenik A.Termination of a floating point computations

Condition (1) permits larger domains for r1 p, i.e., 0 < r1 p < 0:5. This larger domain does not allow us to prove termination as the minimum of

(1:05balance(1 0:5r1 p) 1)(1 0:5r1 p) balance

for balance 100 and 0 < r1 p < 0:5 is undefined. This example illustrates that the use of (2) instead of (1) can be crucial for proving termination. 2

Ideally, both constraint solving and finding the minimum should be done by the same software tool. Unfortunately, traditional constraint solvers such as CLP(Q,R) (Holzbaur, 1995) or ILOG (2001) cannot manage correctly positive numbers smaller than 1:0 10 10. The only notable exception is ECLiPSe. However, even ECLiPSe is not powerful enough to find the minimal value of a multi-variable function on a given domain. In general, finding minima of functions is a complex problem, and usually numerical methods only find local optima. Moreover, neither MatLab (MathWorks, 1999) nor Maple (Waterloo Maple, 2001) is suited to solving constraint satisfaction problems. Thus, at the moment, the only way to implement our approach is to combine different software tools.

6. Conclusion

We have presented an approach to the verification of termination for logic programs with computations depending on ¯oating point numbers. To the best of our knowledge ours is the first work in this domain. Our technique extends the adornments-based approach to termination analysis developed in the context of integer computations. Unlike the integer case, when purely mathematical objects have been considered, the current article concentrates on studying termination of inherently imprecise computations that involve ¯oating-point numbers. Our work can be seen as following a present-day trend in termination analysis of considering programs making use of more state-of-the-art programming techniques than in the past. This tendency can be illustrated, for instance, by recent results on termination of constraint logic programs (Mesnard and Ruggieri, 2003), constraint handling rules (Fr¨uhwirth, 2000), and numerical computations.

Termination of numerical computations was studied by a number of authors (Apt, 1997; Apt et al., 1994; Dershowitz et al., 2001; Serebrenik and De Schreye, 2001a). In (Apt, 1997), it is claimed that an unchanged acceptability condition can be applied to programs in pure Prolog with arithmetic by defining the level mappings on ground atoms with the arithmetic relation to be zero. This approach ignores the actual computation, and thus its applicability is restricted to programs using some arithmetic but whose termination does not depend on it, such as quicksort. Dershowitz et al. (2001) and Serebrenik

paper.tex; 30/03/2005; 11:34; p.31

and De Schreye (2004) restricted their attention to integer computations only. The approach of Dershowitz et al. (2001) was based on the query-mapping pairs formalism of (Lindenstrauss and Sagiv, 1997). However, it also inherited the disadvantages of (Lindenstrauss and Sagiv, 1997), such as a high computational price, which is inherent to this approach due to the repetitive fixpoint computations. Apt et al. (1994) provided a declarative semantics, the socalled Θ-semantics, for Prolog programs with first-order built-in predicates, including arithmetic operations. In this framework the property of strong termination, i.e., finiteness of all possible LD-derivations for all possible goals, was completely characterised based on an appropriately tuned notion of acceptability. This approach provides important theoretical results, but seems to be difficult to integrate with automatic tools. Moreover, termination has been studied with respect to ideal real numbers and not with respect to actual ¯oating point computations. Example 1 illustrates that these two notions of termination are orthogonal, i.e., there are examples that terminate with respect to the reals but not with respect to the ¯oating point numbers and vice versa. Hence, termination proofs obtained for computations with respect to the real numbers by the approach of Apt et al. (1994) cannot be reused to prove termination if ¯oating point numbers are considered. We believe that in order for a termination analyser to be of practical use, termination with respect to ¯oating point numbers should be considered.

More research has been done on termination analysis for constraint logic programs (Colussi et al., 1995; Fr¨uhwirth, 2000; Mesnard, 1996; Mesnard and Ruggieri, 2003; Ruggieri, 1997). However, the research was either oriented towards theoretical characterisations (Ruggieri, 1997) or restricted to domains isomorphic to (N; >) (Mesnard, 1996), such as trees and terms. Recently, in the journal revision (Mesnard and Ruggieri, 2003) of (Mesnard, 1996) and (Ruggieri, 1997), a possibility is mentioned of using abstraction functions other than combinations of term-size norm, list-length norm, identity function and null-function. However, the question of how these functions should be inferred automatically is not considered, and the cTI implementation (Mesnard et al., 2001) is restricted to the term-size norm as an abstraction function. Fr¨uhwirth (2000) studied termination of Constraint Handling Rules (Fr¨uhwirth, 1998) and suggested a variant of the recurrence condition of (Apt and Pedreschi, 1990) for this language. None of the authors who studied termination of CLP programs has considered imprecise computations and their impact on termination. It should also be noted that, while some of the authors study non-ideal constraints systems, the term non-ideal refers to the inability of the constraint system to decide whether a given constraint is true or false, and not to the approximation errors in computations.

Termination of rewriting with real numbers was studied by de Vries and Yamada (1994). They designed a term-rewriting system which mimicked the arithmetic computation of the positive reals with a finite number of digits,

paper.tex; 30/03/2005; 11:34; p.32

with addition and multiplication, and proved that it was terminating. However, they have not studied the termination of term-rewriting systems that use real numbers, rather than implementing them.

Researchers outside of the logic programming community (A¨ıt Ameur, 1999; A¨ıt Ameur et al., 1992; Escard´o, 1996; Goubault, 2001; Goubault et al., 2002; Potts et al., 1997; Vuillemin, 1990) have paid much more attention to ¯oating point arithmetic. However, most of the works of which we are aware concentrate on the precision of numerical computations. Some of them suggest alternative exact representations of real arithmetic, for example using continued fraction expansions (Vuillemin, 1990), sequences of linear maps (Escard´o, 1996), linear fractional transformations with non-negative integer coefficients (Potts et al., 1997) or intervals with ¯oating-point numbers as end-points (Moore, 1966; A¨ıt Ameur, 1999). The latter idea gained certain popularity also in the constraints logic programming community (Vellino and Older, 1990) and even led to a number of systems such as CLP(BNR) (Older and Benhamou, 1993), PrologIV (Benhamou et al., 1996) and ILOG (Van Hentenryck et al., 1997; ILOG, 2001). Other authors apply abstract interpretation (Cousot and Cousot, 1976; Cousot and Cousot, 1977) to infer whether precision might be lost (A¨ıt Ameur et al., 1992; Goubault, 2001). These works tend, however, to ignore the use of denormalised numbers and the to the nearest value rounding policy, both being decisions usually made by system implementors. Moreover, to the best of our knowledge, there is no work done to relate the precision results obtained with the techniques above to termination analysis.

Monniaux (2001) studied termination of probabilistic logic programs in the framework of DAEDALUS—the European project concerning the validation of critical software by static analysis and abstract testing (Randimbivololona et al., 2001). That work is almost unique in that it refers to the problem of using ¯oating point numbers instead of real numbers in the context of termination analysis, and that it discusses the implementation problems involved. The first problem mentioned is ensuring soundness of the system. The second and more annoying problem is “drift”, in which a sequence of real numbers that should appear to be stationary may be strictly ascending in the ¯oating point approximation. However, Monniaux does not present a solution to these problems, but hopes that the work on abstract domains for real numbers (A¨ıt Ameur et al., 1992; Goubault, 2001), discussed in the previous paragraph, will provide it. As we have already pointed out, current results do not consider yet the complexity of ¯oating point number systems in its entirety.

In our work, we assume that no ¯oating-point exceptions occur during the computation and that denormalised numbers are used to ensure gradual under¯ow. Alternative approaches to handling ¯oating-point exceptions such as “brute force” reevaluation and scaling, are discussed by (Hauser, 1996).

paper.tex; 30/03/2005; 11:34; p.33

34 Alexander Serebrenik and Danny De Schreye

Although exception handling is not a necessary feature, support for exception handling allows better optimisation for many numerical routines (Demmel and Li, 1993). Alternatively, one can try to proceed in two steps. First, we can verify absence of run-time errors that can result in exceptions being thrown (Min´e, 2004), and than analyse termination of the error-free computation by applying our technique. A special class of ¯oating point programs, so called digital filters, was recently studied by Feret (2004). He observed that lack of precise domains for digital filters was the cause of almost all false “potential over¯ow” messages reported by the system of (Blanchet et al., 2003). This observation led to a new abstract interpretation-based framework for designing new abstract domains.

Our study of termination was based on the notion of termination with respect to a set of queries. The idea behind this notion is that some queries may be of no importance for the user. Ruggieri (Ruggieri, 1997; Mesnard and Ruggieri, 2003) proposed an alternative way to distinguish between the relevant queries and the irrelevant ones. He extended the definition of a level-mapping to include a designated value of ∞, and suggested mapping important queries to the naturals and the non-important ones to ∞.

The key idea of splitting a predicate into cases was first mentioned by Ullman and Van Gelder (1988), where it was assumed that a preprocessor transforms a set of clauses into a new set, in which every subgoal unifies with all of the rules, i.e. clauses with non-empty bodies, for its predicate symbol. However, neither in this paper, nor in the subsequent one (Sohn and Van Gelder, 1991) was the proposed methodology presented formally. To the best of our knowledge, the first formal presentation of splitting in the framework of termination analysis is due to Lindenstrauss et al. (1998). Unlike in their work, a numerical and not a symbolic domain was considered in the current article. Distinguishing different subsets of values for variables, and deriving norms and level mappings based on these subsets, links our approach to the ideas of using type information in termination analysis for symbolic computations (Bruynooghe et al., 2002; Bruynooghe et al., 2001; Vanhoof and Bruynooghe, 2002). Indeed, adornments can be seen as types, refining the predefined type floating point numbers. Unlike these works, our work does not start with a given set of types, but for each program derives a collection of types relevant to this program.

The adorning process can be regarded as similar to multiple specialisation (Puebla and Hermenegildo, 1999; Winsborough, 1992). However, while traditionally termination analysis techniques were used for partial deduction purposes (Leuschel et al., 1998; Sahlin, 1993; Jones et al., 1993, Chapter 14), we reverse the relationship between the two and propose to apply a partial deduction technique to prove termination. Moreover, traditionally specialisation techniques are restricted to symbolic computations and, hence, are not immediately applicable in our case.

paper.tex; 30/03/2005; 11:34; p.34

We stress that although our results are couched in logic programming terminology, they are not limited to logic programming per se, as they focus on the properties of ¯oating point numbers and not on the language aspects of logic programs.

References

Aggoun, A., 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: 2001, `ECLiPSe User Manual. Release 5.3'. European Computer-Industry Research Centre, Munich and Centre for Planning and Resource Control, London.

AÈõt Ameur, Y.: 1999, `Re®nement of rational end-points real numbers by means of floatingpoint numbers'. Science of Computer Programming 33(2), 133–162.

AÈõt Ameur, Y., P. Cros, J. J. Falc´on, and A. G´omez: 1992, `An Application of Abstract Interpretation to Floating Point Arithmetic'. In: M. Billaud, P. Cast´eran, M.-M. Corsini, K. Musumbu, and A. Rauzy (eds.): Actes WSA'92 Workshop on Static Analysis, Vol. 81–82 of Bigre. pp. 205–212, Atelier Irisa, IRISA, Campus de Beaulieu.

Apt, K. R.: 1997, From Logic Programming to Prolog, Prentice-Hall International Series in Computer Science. Prentice Hall.

Apt, K. R., E. Marchiori, and C. Palamidessi: 1994, `A declarative approach for ®rstorder built-in's in Prolog'. Applicable Algebra in Engineering, Communication and Computation 5(3/4), 159–191.

Apt, K. R. and D. Pedreschi: 1990, `Studies in Pure Prolog: Termination'. In: J. W. Lloyd (ed.): Proceedings Esprit Symp. on Comp. Logic. Springer Verlag, pp. 150–176.

Bagnara, R.: 1999, `Is ISO Prolog standard taken seriously?'. Association for Logic Programming Newsletter 12(1), 10–12.

Benhamou, F., P. Bouvier, A. Colmerauer, H. Garetta, B. Giletta, J. L. Massat, G. A. Narboni, S. N'Dong, R. Pasero, J. F. Pique, M. Touravane abd Van Canegheme, and E. V´etillard: 1996, `Le manuel de Prolog IV'. PrologIA.

BIM: 1995, `ProLog by BIM'. Release 4.1.0.

Blanchet, B., P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min´e, D. Monniaux, and X. Rival: 2003, `A Static Analyzer for Large Safety-Critical Software'. In: Proceedings of the ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation. pp. 196–207, ACM.

Bossi, A., N. Cocco, and M. Fabris: 1991, `Proving Termination of Logic Programs by Exploiting Term Properties'. In: Proceedings of CCPSD-TAPSOFT'91, Vol. 494 of Lecture Notes in Computer Science. Springer Verlag, pp. 153–180.

Bruynooghe, M., M. Codish, S. Genaim, and W. Vanhoof: 2002, `Reuse of results in termination analysis of typed logic programs'. In: M. V. Hermenegildo and G. Puebla (eds.):

Static Analysis, 9th International Symposium, Vol. 2477 of Lecture Notes in Computer Science. pp. 477–492, Springer Verlag.

Bruynooghe, M., W. Vanhoof, and M. Codish: 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 International Andrei Ershov Memorial Conference, PSI 2001, Akademgorodok, Novosibirsk, Russia, July 2-6, 2001, Revised Papers, Vol. 2244 of Lecture Notes in Computer Science. Springer Verlag.

paper.tex; 30/03/2005; 11:34; p.35

Bueno, F., D. Cabeza Gras, M. Carro, M. V. Hermenegildo, P. L´opez-Garc´õa, and G. Puebla: 1997, `The Ciao Prolog system. Reference manual'. Technical Report CLIP3/97.1, Technical University of Madrid (UPM).

Col´on, M. A. and H. B. Sipma: 2001, `Synthesis of Linear Ranking Functions'. In: T. Margaria and W. Yi (eds.): Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, Vol. 2031 of Lecture Notes in Computer Science. pp. 67–81, Springer Verlag.

Colussi, L., E. Marchiori, and M. Marchiori: 1995, `On termination of constraint logic programs'. In: U. Montanari and F. Rossi (eds.): Principles and Practice of Constraint Programming - CP'95,, Vol. 976 of Lecture Notes in Computer Science. pp. 431–448, Springer Verlag.

Cousot, P. and R. Cousot: 1976, `Static determination of dynamic properties of programs'. In: Proceedings of the Second International Symposium on Programming. pp. 106–130, Dunod, Paris, France.

Cousot, P. and R. Cousot: 1977, `Abstract interpretation: a uni®ed lattice model for static analysis of programs by construction or approximation of ®xpoints'. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Los Angeles, California, pp. 238–252, ACM Press, New York, NY.

Cousot, P. and R. Cousot: 2001, `Veri®cation of Embedded Software: Problems and Perspectives'. In: T. A. Henzinger and C. Meyer Kirsch (eds.): Embedded Software, First International Workshop, EMSOFT 2001, Tahoe City, CA, USA, October, 8-10, 2001, Proceedings, Vol. 2211 of Lecture Notes in Computer Science. pp. 97–113, Springer Verlag.

De Schreye, D. and S. Decorte: 1994, `Termination of Logic Programs: The Never-Ending Story'. Journal of Logic Programming 19/20, 199–260.

De Schreye, D., K. Verschaetse, and M. Bruynooghe: 1992, `A Framework for Analyzing the Termination of De®nite Logic Programs with respect to Call Patterns'. In: I. Staff (ed.):

Proceedings of the International Conference on Fifth Generation Computer Systems. pp. 481–488, IOS Press.

de Vries, F.-J. and J. Yamada: 1994, `On termination of rewriting with real numbers'. In: M. Takeichi (ed.): Functional Programming II, Proceedings of the 11th Annual Conferencerence, Japan Society of Software Science and Technology. pp. 233–247, Kindai-kagaku-sya.

Decorte, S. and D. De Schreye: 1998, `Termination analysis: some practical properties of the norm and level mapping space'. In: J. Jaffar (ed.): Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming. pp. 235–249, MIT Press.

Decorte, S., D. De Schreye, and H. Vandecasteele: 1999, `Constraint-based Termination Analysis of Logic Programs'. ACM TOPLAS 21(6), 1137–1195.

Demmel, J. W. and X. S. Li: 1993, `Faster numerical algorithms via exception handling'. In: E. E. Swartzlander, M. J. Irwin, and J. Jullien (eds.): Proceedings of the 11th IEEE Symposium on Computer Arithmetic. Windsor, Canada, pp. 234–241, IEEE Computer Society Press, Los Alamitos, CA.

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

Escard´o, M. H.: 1996, `PCF Extended with Real Numbers'. Theoretical Computer Science 162(1), 79–115.

Feret, J.: 2004, `Static Analysis of Digital Filters'. In: D. A. Schmidt (ed.): Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Vol. 2986 of Lecture Notes in Computer Science. pp. 33–48, Springer Verlag.

paper.tex; 30/03/2005; 11:34; p.36

Flynn, M. and S. Oberman: 2001, Advanced Computer Arithmetic Design. J. Wiley.

Fraley, R. and S. Walther: 1979, `Proposal to Eliminate Denormalized Numbers'. ACM SIGNUM Newsletter 14(3S (Special issue)), 22–23.

FrÈuhwirth, T. W.: 1998, `Theory and Practice of Constraint Handling Rules'. Journal of Logic Programming 37(1–3), 95–138. Special Issue on Constraint Logic Programming.

FrÈuhwirth, 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, Vol. 1865 of Lecture Notes in Arti®cial Intelligence. Springer Verlag.

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): 413 (1991).

Goubault, E.: 2001, `Static Analyses of the Precision of Floating-Point Operations'. In: P. Cousot (ed.): Static Analysis, 8th International Symposium, Vol. 2126 of Lecture Notes in Computer Science. pp. 234–259, Springer Verlag.

Goubault, E., M. Martel, and S. Putot: 2002, `Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter'. In: D. Le M´etayer (ed.): Programming Languages and Systems, 11th European Symposium on Programming, Vol. 2305 of Lecture Notes in Computer Science. pp. 209–212, Springer Verlag.

Hauser, J. R.: 1996, `Handling Floating-Point Exceptions in Numeric Programs'. ACM Transactions on Programming Languages and Systems 18(2), 139–174.

Holzbaur, C.: 1995, `OFAI CLP(Q,R) Manual'. Technical Report TR-95-09, Austrian Research Institute for Arti®cial Intelligence, Vienna.

IEEE Standards Committee 754: 1985, IEEE Standard for binary ¯oating-point arithmetic, ANSI/IEEE Standard 754-1985. Institute of Electrical and Electronics Engineers, New York. Reprinted in SIGPLAN Notices, 22(2):9-25, 1987.

ILOG: 2001, `ILOG Solver 5.1 User's Manual'. ILOG s.a. http://www.ilog.com/.

ISO/IEC 10967 Committee: 1994, ISO/IEC 10967-1: 1994 Information technology— Language independent arithmetic—Part 1: Integer and ¯oating point arithmetic. ISO/IEC.

ISO/IEC 10967 Committee: 2001, ISO/IEC 10967-2:2001 Information technology— Language independent arithmetic—Part 2: Elementary numerical functions. ISO/IEC.

ISO/IEC 13211 Committee: 1995, Information technology—Programming languages— Prolog—Part 1: General core. ISO/IEC.

IT Masters: 2000, `MasterProLog Programming Environment'. Available at http://www.itmasters.com/.

Janssens, G. and M. Bruynooghe: 1992, `Deriving descriptions of possible values of program variables by means of abstract interpretation'. Journal of Logic Programming 13(2&3), 205–258.

Janssens, G., M. Bruynooghe, and V. Englebert: 1994, `Abstracting Numerical Values in CLP(H, N)'. In: M. V. Hermenegildo and J. Penjam (eds.): Programming Language Implementation and Logic Programming, 6th International Symposium, PLILP'94, Vol. 844 of Lecture Notes in Computer Science. pp. 400–414, Springer Verlag.

Jones, N. D., C. K. Gomard, and P. Sestoft: 1993, Partial Evaluation and Automatic Program Generation. Prentice Hall International. Available at http://www.dina.dk/ sestoft/pebook/.

Kowalski, R. A. and D. Kuehner: 1971, `Linear Resolution with Selection Function.'. Arti®cial Intelligence 2(3/4), 227–260. Imperial College, London.

Leuschel, M., B. Martens, and D. De Schreye: 1998, `Controlling generalisation and polyvariance in partial deduction of normal logic programs'. ACM Transactions on Programming Languages and Systems 20(1), 208–258.

paper.tex; 30/03/2005; 11:34; p.37

38 Alexander Serebrenik and Danny De Schreye

Lindenstrauss, N. and Y. Sagiv: 1997, `Automatic Termination Analysis of Logic Programs'. In: L. Naish (ed.): Proceedings of the Fourteenth International Conference on Logic Programming. pp. 63–77, MIT Press.

Lindenstrauss, N., Y. Sagiv, and A. Serebrenik: 1998, `Unfolding the Mystery of Mergesort'. In: N. Fuchs (ed.): Proceedings of the 7th International Workshop on Logic Program Synthesis and Transformation, Vol. 1463 of Lecture Notes in Computer Science. pp. 206–225, Springer Verlag.

Lloyd, J. W.: 1987, Foundations of Logic Programming, Symbolic Computation. Springer Verlag. Second Edition.

Martelli, A. and U. Monatanari: 1982, `An Ef®cient Uni®cation Algorithm'. ACM Transactions on Programming Languages and Systems (TOPLAS) 4(2), 258–282.

Martin, J. C. and A. King: 2004, `On the Inference of Natural Level Mappings'. In: M. Bruynooghe and K.-K. Lau (eds.): Program Development in Computational Logic, Vol.

Mesnard, F.: 1996, `Inferring left-terminating classes of queries for constraint logic programs'. In: M. Maher (ed.): Proceedings of the 1996 Joint International Conference and Syposium on Logic Programming. Cambridge, MA, USA, pp. 7–21, The MIT Press.

Mesnard, F., U. Neumerkel, and E. Payet: 2001, `cTI: un outil pour l'inf´erence de conditions optimales de terminaison pour Prolog'. In: P. Codognet (ed.): Dixi`emes Journ´ees Francophone de Programmation en Logique et Programmation par Contraintes. Herm´es. Available at http://www.univ-reunion.fr/ gcc/papers.

Mesnard, F. and S. Ruggieri: 2003, `On proving left termination of constraint logic programs'.

ACM Transaction on Computational Logic 4(2), 207–259.

Min´e, 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, Vol. 2986 of Lecture Notes in Computer Science. pp. 3–17, Springer Verlag.

Monniaux, D.: 2001, `An Abstract Analysis of the Probabilistic Termination of Programs'. In: P. Cousot (ed.): 8th International Static Analysis Symposium (SAS'01). pp. 111–126, Springer Verlag.

Moore, R. E.: 1966, Interval Analysis. Prentice-Hall.

Older, W. and F. Benhamou: 1993, `Programming in CLP(BNR)'. In: Principles and Practice of Constraint Programming.

Payne, M. H. and W. Strecker: 1979, `Draft Proposal for a Binary Normalized Floating Point Standard'. ACM SIGNUM Newsletter 14(3S (Special issue)), 24–28.

Pedreschi, D., S. Ruggieri, and J.-G. Smaus: 2002, `Classes of Terminating Logic Programs'.

Theory and Practice of Logic Programming 2(3), 369–418.

PlÈumer, L.: 1991, `Automatic Termination Proofs for Prolog Programs Operating on Nonground Terms.'. In: International Logic Programming Symposium. MIT Press.

Potts, P. J., A. Edalat, and M. H. Escard´o: 1997, `Semantics of Exact Real Arithmetic'. In:

Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science. pp. 248–257, IEEE Computer Society Press.

Puebla, G. and M. V. Hermenegildo: 1999, `Abstract Multiple Specialization and Its Applica-

able 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.

paper.tex; 30/03/2005; 11:34; p.38

Robinson, J. A.: 1965, `A Machine-Oriented Logic Based on the Resolution Principle'.

Journal of the Association for Computing Machinery 12(1), 23–41. Argonne National Laboratory and Rice University.

Ruggieri, S.: 1997, `Termination of Constraint Logic Programs'. In: P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela (eds.): Automata, Languages and Programming, 24th International Colloquium, ICALP'97, Vol. 1256 of Lecture Notes in Computer Science. pp. 838–848, Springer Verlag.

Sahlin, D.: 1993, `Mixtus: An Automatic Partial Evaluator for Full Prolog'. New Generation Computing 12(1), 7–51.

Serebrenik, A. and D. De Schreye: 2001a, `Inference of termination conditions for numerical loops in Prolog'. In: R. Nieuwenhuis and A. Voronkov (eds.): Logic for Programming, Arti®cial Intelligence, and Reasoning, 8th International Conferencerence, Proceedings, Vol. 2250 of Lecture Notes in Computer Science. pp. 654–668, Springer Verlag.

Serebrenik, A. and D. De Schreye: 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 International Workshop, Selected Papers, Vol. 2042 of Lecture Notes in Computer Science. pp. 69–85, Springer Verlag.

Serebrenik, A. and D. De Schreye: 2004, `Inference of termination conditions for numerical loops in Prolog'. Theory and Practice of Logic Programming 4(5&6), 719–751. Special issue Veri®cation and Computational Logic.

SICS: 2004, `SICStus User Manual. Version 3.11.1'. Swedish Institute of Computer Science. Skeel, R.: 1992, `Roundoff Error and the Patriot Missile'. SIAM News 25(4), 11.

Sohn, K. and A. Van Gelder: 1991, `Termination Detection in Logic Programs using Argument Sizes.'. In: Proceedings of the Tenth ACM SIGACT-SIGART-SIGMOD Symposium on Principles of Database Systems. pp. 216–226, ACM Press.

Ullman, J. D. and A. Van Gelder: 1988, `Ef®cient Tests for Top-Down Termination of Logical Rules.'. Journal of the ACM 35(2), 345–373.

United States General Accounting Of®ce: 1992, Patriot Missile Defence. Software problem led to system failure at Dhahran, Saudi Arabia, No. 92-26 in GAO/IMTEC. United States General Accounting Of®ce. Also available at http://klabs.org/richcontent/Reports/Failure Reports/patriot/patriot gao 145960.pdf.

Van Hentenryck, P., L. Michel, and Y. Deville: 1997, Numerica: A Modeling Language for Global Optimization. Cambridge, MA, USA: The MIT Press.

Vanhoof, W. and M. Bruynooghe: 2002, `When size does matter - Termination analysis for typed logic programs'. In: A. Pettorossi (ed.): Logic-based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Selected Papers, Vol. 2372 of

LNCS. pp. 129–147, Springer Verlag.

Vellino, A. and W. Older: 1990, `Extending Prolog with Constraint Arithmetic on Real Intervals'. In: IEEE Canadian Conference on Electrical and Computer Engineering.

Verschaetse, K. and D. De Schreye: 1991, `Deriving Termination Proofs for Logic Programs, Using Abstract Procedures'. In: K. Furukawa (ed.): Logic Programming, Proceedings of the Eigth International Conference. pp. 301–315, MIT Press.

Vuillemin, J.: 1990, `Exact Real Computer Arithmetic with Continued Fractions'. IEEE Transactions on Computers 39(8), 1087–1105.

Waterloo Maple, I.: 2001, `Maple 7'. Consult http://www.maplesoft.com/.

Winsborough, W.: 1992, `Multiple specialization using minimal-function graph semantics'.

Journal of Logic Programming 13(2/3), 259–290.

paper.tex; 30/03/2005; 11:34; p.39