[mercury-users] float.m

[Richard A. O'Keefe]

There are some very strange comments in section 18 (float) of the Mercury
Library manual, and some of the modes are stranger still.

The comments basically express the view that because the IEEE 754
"numerical similarity" predicate does not obey the axioms for equality,
THEREFORE Mercury implementations should go out of their way to wreck
IEEE 754 conformance in another place entirely.

Well, if you try to pretend that -0.0 does not exist, you will be in for
a very hard time, and you will destroy some very carefully thought out
properties of IEEE arithmetic (including what's been decided for the
transcendental functions).

It would be far far simpler to say "because IEEE 754 numerical similarity
does not obey the axioms for equality, therefore it ISN'T equality".  (It's
not just -0.0.  It's NaNs as well.  I've been through all this while at
Quintus.)

I suggest therefore that the existing numerical similarity predicate
in Mercury, (=:=)/2, be brought back from retirement and be given the
role of "IEEE 754 similarity", while (=)/2 applied to floating-point
numbers should have the reading "bitwise identity", which is logically
defensible in any case and DOES have the required semantics.

We'd then have

    -0.0 = 0.0		  false
    -0.0 =:= 0.0	  true
    -0.0 \= 0.0		  true
    -0.0 =\= 0.0	  false

    X = 0.0/0.0, X = X	  true		(X is X, right?)
    X = 0.0/0.0, X =:= X  false		(NaNs aren't self-similar).

Getting this right requires *no* bending of IEEE 754 semantics anywhere,
which is good news for all calculations.  It only means that
 (float::in) = (float::in) has to be implemented by calling a bitwise
identity function, but then float = float comparisons, while technically
legal and perfectly reasonable if you know what you are doing, are
likely to be rare.

As for the modes, we find

    :- func float + float = float
    :- mode in    + in    = uo is det.	% fine
    :- mode uo    + in    = in is det.	% What???
    :- mode in    + uo    = in is det.  % What???

with similar uo?in=in, in?uo=in modes for -, *, and /

It is easy to find floating point numbers X and Y such that
    X + Y = X
so if you try
    X + Y = Z, X + W = Z, Y = W
the Y=W test will fail, because W is zero and Y isn't.
For example, X = 1.0e20, Y = 1.0e-20 will do nicely.

Similar examples can be found for -, *, and /.
In fact for * the example
	X * 0.0 = 1.0
should show that it won't work.  Even in IEEE arithmetic, try
	X * 0.0 = 1.0,
	X * 0.0 = Y,
	Y = 1.0
1.0/0.0 is +infinity, infinity*0 is NaN, and NaN is NOT equal to 1.0.

The only modes that make sense for the floating point operations are
the in?in=uo ones, the others should be deleted, and soon, before people
are suckered into using them.

(Note that these modes DO make sense in int.m, integer.m, and rational.m)

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------