[mercury-users] IEEE float (was: Newbie problem)

[Fergus Henderson]

On 16-Jun-1999, Richard A. O'Keefe <ok at atlas.otago.ac.nz> wrote:
> The classic example is numeric comparison.  In IEEE 754
> floating point arithmetic (supported by M68k, M88k, PowerPC,
> SPARC, Alpha, MIPS, 80*86/Pentium, &c), the negative clause
> 
> 
>     :- X >= Y, X < Y  %where% float(X), float(Y).
> 
> *is* true, but the disjunction
> 
>     X >= Y ; X < Y %where% float(X), float(Y).
> 
> is *false*.  A precicate such as
> 
>     :- pred max(float, float, float).
>     :- mode max(in, in, out).
> 
>     max(X, Y, Max) :- ( X >= Y -> Max = X ; X < Y, Max = Y ).
> 
> is *not* det, it is semidet.  And this was the case I was considering.
> Note that if you want to conclude that max/3 written as above is det,
> you *do* need to know that the disjunction is true, but you *don't*
> need to know that the negative rule is true.
> 
> Some of you may be scratching your heads over this, but IEEE floating
> point arithmetic, the kind of floating point arithmetic we have to
> live with on most of the machines Mercury is likely to be used on,
> has a class of values called NaNs, which do not compare less than,
> greater than, or equal to anything at all; they don't even compare
> equal to themselves.  Thus max(0.0/0.0, 0.0) will, and *should*,
> fail.

This is not entirely correct.

>From the Mercury library reference manual:

    % Note that implementations which support IEEE floating point
    % should ensure that in cases where the only valid answer is a "NaN"
    % (the IEEE float representation for "not a number"), the det
    % functions here will halt with a runtime error (or throw an exception)
    % rather than returning a NaN.  Quiet (non-signalling) NaNs have a
    % semantics which is not valid in Mercury, since they don't obey the
    % axiom "all [X] X = X".

So, even on machines which support IEEE floating point, the intent is that
the Mercury `float' type will never have any NaN values.

This design decision was arrived at after much thought.
However, I'd be very interested to hear any user feedback on this issue.

Note that unfortunately the current implementation does not yet fully
implement this intent -- the library reference manual goes on to explain
this:

    % XXX Unfortunately the current Mercury implementation does not
    % do that on all platforms, since neither ANSI C nor POSIX provide
    % any portable way of ensuring that floating point operations
    % whose result is not representable will raise a signal rather
    % than returning a NaN.  (Maybe C9X will help...?)
    % The behaviour is correct on Linux and Digital Unix,
    % but not on Solaris, for example.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------