Unification of Floating Point Numbers

As far as unification is concerned, no type distinction is made between integers and floating point numbers, and no explicit type conversion is necessary when unifying an integer with a float. However, due to the finite precision representation of floating point numbers and cumulative round-off errors in floating point arithmetic, comparisons involving floating point numbers may not always give the expected results. An effort is made to minimize surprises by considering two numbers x and y (at least one of which is a float) to be unifiable if (| x| - | y|)/min(| x|,| y|) to be less than 10-5. However, this does not guarantee immunity against round-off errors. For the same reason, users are warned that indexing on predicate arguments (see Section [*]) may not give the expected results if floating point numbers are involved.