Re: +-Inf and NaN

[Camm Maguire]

Greetings!

Matt Kaufmann <kaufmann@cs.utexas.edu> writes:

> Hi Camm,
>
> Excellent.  ACL2 will evaluate the following at start-up.
>
> (fpe:break-on-floating-point-exceptions
>  :floating-point-overflow t
>  :division-by-zero t ; not sure this is actually needed
>  :floating-point-invalid-operation t)
>

Sounds good, but you might want to consider adding the other two with a
setting of nil so your behavior is immune to GCL changes in its default
configuration.  I don't plan on enabling traps by default at the moment
as it appears controversial, but that could change.


> That said, consider the following from the Common Lisp Hyperspec,
> Section 12.1.4.4 (Rule of Float Precision Contagion).
>
>    The result of a numerical function is a float of the largest format
>    among all the floating-point arguments to the function.
>
> This seems to argue for proposal 1), since when a NaN results from the
> application of a numerical function to double-float arguments, that
> NaN would apparently need to be of type double-float.

Yeah, I think 1) is the way to go for now, but the reading of this
section depends to my mind on whether NaN is a valid return, in which
case it is a number/float/long-float, or an error indicator, which can
be trapped or not.  Conceptually you might as well replace the NaN with
a common-lisp condition akin to


>(arithmetic-error-operands (make-condition 'floating-point-invalid-operation 
>:operands (list compiler::nan 1.0)))

(#<nan> 1.0)

and return this when not trapping, but defining some additional cell
containing the NaN result for use in subsequent processing.  The chief
argument against this appears to be performance.

Take care,
-- 
Camm Maguire                                        camm@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah