M. H. van Emden

W. W. Edmonson, M. H. van Emden

If the non-zero finite floating-point numbers are interpreted as point intervals, then the effect of rounding can be interpreted as computing one of the bounds of the result according to interval arithmetic. We give an interval interpretation for the signed zeros and infinities, so that the undefined operations 0*inf, inf - inf, inf/inf, and 0/0 become defined. In this way no operation remains that gives rise to an error condition. Mathematically questionable features of the floating-point standard become well-defined sets of reals. Interval semantics provides a basis for the verification of numerical algorithms. We derive the results of the newly defined operations and consider the implications for hardware implementation.

A. Nait Abdallah, M. H. van Emden

This paper draws on diverse areas of computer science to develop a unified view of computation: (1) Optimization in operations research, where a numerical objective function is maximized under constraints, is generalized from the numerical total order to a non-numerical partial order that can be interpreted in terms of information. (2) Relations are generalized so that there are relations of which the constituent tuples have numerical indexes, whereas in other relations these indexes are variables. The distinction is essential in our definition of constraint satisfaction problems. (3) Constraint satisfaction problems are formulated in terms of semantics of conjunctions of atomic formulas of predicate logic. (4) Approximation structures, which are available for several important domains, are applied to solutions of constraint satisfaction problems. As application we treat constraint satisfaction problems over reals. These cover a large part of numerical analysis, most significantly nonlinear equations and inequalities. The chaotic algorithm analyzed in the paper combines the efficiency of floating-point computation with the correctness guarantees of arising from our logico-mathematical model of constraint-satisfaction problems.

M. H. van Emden

The CLP scheme uses Horn clauses and SLD resolution to generate multiple constraint satisfaction problems (CSPs). The possible CSPs include rational trees (giving Prolog) and numerical algorithms for solving linear equations and linear programs (giving CLP(R)). In this paper we develop a form of CSP for interval constraints. In this way one obtains a logic semantics for the efficient floating-point hardware that is available on most computers. The need for the method arises because in the practice of scheduling and engineering design it is not enough to solve a single CSP. Ideally one should be able to consider thousands of CSPs and efficiently solve them or show them to be unsolvable. This is what CLP/NCSP, the new subscheme of CLP described in this paper is designed to do.