Re: +-Inf and NaN

[Matt Kaufmann]

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)

So I don't think that any floating-point operation will return a NaN.
(I'd be very interested in a counterexample!)  So I think proposals 1)
and 2) are both fine as far as ACL2 is concerned.

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.

Thanks,
Matt
Camm Maguire <camm@maguirefamily.org> writes:

> Greetings!
>
> Matt Kaufmann <kaufmann@cs.utexas.edu> writes:
>
>> Hi Camm,
>>
>> Since this thread has discussed floating-point exceptions, I'll weigh
>> in only by requesting that such behavior will continue to be
>> configurable.  Specifically, in ACL2 built using GCL 2.6.12
>> (Version_2_6_13pre131), where compilation uses safety 0, then
>> evaluation of the following form at start-up gives the behavior I want
>> -- in particular, an error when there is floating-point overflow or
>> division by zero.
>>
>> (fpe:break-on-floating-point-exceptions
>>  :floating-point-overflow t
>>  :floating-point-invalid-operation t)
>>
>
> Agreed, this behavior isn't going anywhere.  The basic question is what
> the compiler should do with '= (or equivalent) when it knows its
> arguments are the same object.  In proposal 1), (double)NaN remains of
> type 'long-float, and the compiler will replace this call with t only at
> safety 0 *and* some bound is known on the argument.  In proposal 2)
> (double)NaN is of some type orthogonal to 'long-float, and the compiler
> always replaces the call with t at safety 0.  The first is less radical
> and almost surely will be the approach taken initially with 2.7.0,
> though the latter is conceptually cleaner.  In proposal 2), there will
> be a one line addition to the type checker skipping the error on NaN
> when running interpreted or compiled with safety depending on the fpe
> settings you show above.
>
> One downside of proposal 2) is that '+ and the like return '(or number
> new-type-for-nans)....
>
> I'm so sorry to have taken up so much attention on this.  The whole
> conversation arose due to one remaining testsuite failure in maxima when
> compiled with 2.7.0, in which the code relies on '(/= a a) as a NaN
> detector.  There are many simple ways around this without addressing the
> question more generally as I have posed.
>
> BTW, thanks for the NaN code in the various lisps attached!
>
> Take care,
>
>> For example, when I evaluate the definitions
>>
>> (defun f ()
>>   (let ((y (* most-positive-double-float most-positive-double-float)))
>>     (= (- y y) 0.0d0)))
>>
>> and
>>
>> (defun g ()
>>   (= (/ 0.0d0 0.0d0) 0.0d0))
>>
>> and then compile f and g, then the evaluations of (f) and (g) both
>> cause errors, which is what I want.  (If f and g are compiled in gcl
>> with safety 0 but are called without first calling
>> fpe:break-on-floating-point-exceptions, then there is no error.)
>>
>> By the way, you asked, regarding other Lisps:
>>
>>> Can one access/manipulate nan at the lisp prompt level?
>>
>> See attached, which I think answers your question positively for
>> LispWorks, Allegro CL, and CCL, but perhaps negatively for SBCL and
>> CMUCL.
>>
>> Thanks,
>> Matt
>> Camm Maguire <camm@maguirefamily.org> writes:
>>
>>> Greetings!
>>>
>>> Richard Fateman <fateman@gmail.com> writes:
>>>
>>>> I think that using exactly the same argument conventions and names as the 
>>>> library would be best.
>>>> so you overwrite one (or more) of the inputs, for the same reasons as mpfr 
>>>> does it,
>>>> to save memory allocation when possible.
>>>>
>>>> Possible glitch:  it assumes you will only pass arguments that are in 
>>>> memory, not on a stack.
>>>> Thus for actual use you may need to have a functional style program 
>>>> interface that puts the
>>>> arguments in memory.  I think that mpfr number structures have a size 
>>>> [maximum length] and
>>>> an actual size in use. So numbers and comparisons of them etc. must be
>>>> done by mpfr.
>>>
>>> Yes this is the rub, and I believe the basic issues are the same with
>>> floats as integers.  GCL stores immediate fixnums in one format, other
>>> fixnums in another, and bignums in a format directly accessible to gmp.
>>> We could expose both the raw gmp interface and the 'functional'
>>> interface which would load the first two into the third, but whether
>>> done under the hood or by the user directly, there is nothing to
>>> overwrite if fixnums are supplied as output arguments.  At the C level
>>> we have 5 bignum 'registers' which we do not expose to lisp, as if they
>>> contain fixnums the logic pertaining to the same will fail.  I suppose
>>> an expert user could make use of the registers and be careful not to
>>> refer to them until the gmp calculation is done.
>>>
>>> Take care,
>>>
>>>> RJF
>>>>
>>>> On Wed, Feb 28, 2024 at 12:55 PM Camm Maguire <camm@maguirefamily.org> 
>>>> wrote:
>>>>
>>>>  Greetings!
>>>>
>>>>  Richard Fateman <fateman@gmail.com> writes:
>>>>
>>>>  > Several of us here have worked on arbitrary-precision floats in Lisp
>>>>  > (generally used for longer than double, though I suppose shorter could
>>>>  > also be specified...), and I think the real win would be to make use
>>>>  > of the mpfr library (written in C with various assembly-language hacks
>>>>  > for different CPUs).
>>>>
>>>>  mpfr would be a straightforward extension to GCL, as we already use the
>>>>  gmp integer library, integrate it with our gbc/memory management, and
>>>>  export the functions at the lisp user level:
>>>>
>>>>  >(gmp:mpz_mul most-positive-fixnum most-positive-fixnum)
>>>>
>>>>  85070591730234615847396907784232501249
>>>>
>>>>  The only sensible way to interface to a library like this is to keep all
>>>>  the function names and calling syntax the same.  GMP is written with
>>>>  'side-effects', i.e. destructive modification of the supplied arguments
>>>>  one or more of which are considered outputs.  This is so the savvy user
>>>>  can avoid unnecessary allocations, which are effectively all that matter
>>>>  for performance.  Lisp is so functionally oriented, however, that it
>>>>  seemed better to me to take only input variables as arguments.  The
>>>>  natural alternative to the call above would take three arguments,
>>>>  overwrite the first, and return no values.  Your thoughts?
>>>>
>>>>  Take care,
>>>>  --
>>>>  Camm Maguire                                        camm@maguirefamily.org
>>>>  ==========================================================================
>>>>  "The earth is but one country, and mankind its citizens."  --  Baha'u'llah
>>>>
>>>
>>> --
>>> Camm Maguire                                            
>>> camm@maguirefamily.org
>>> ==========================================================================
>>> "The earth is but one country, and mankind its citizens."  --  Baha'u'llah
>>
>>
>
> --
> Camm Maguire                                      camm@maguirefamily.org
> ==========================================================================
> "The earth is but one country, and mankind its citizens."  --  Baha'u'llah