Re: [PATCH] Handle products with exact 0 differently, etc

[Mark H Weaver]

I wrote:
>> Are you following specific references here?  FWIW, for cases like this,
>> the last para of R6RS 11.7.1 allows "either 0 (exact) or 0.0 (inexact)".
>
> Yes, the R6RS does allow (* 1.0 0) to be an exact 0, but that's because
> it also allows (* 0 +inf.0) and (* 0 +nan.0) to be an exact 0.  Section
> 11.7.4.3 provides the following examples:
>
>   (* 0 +inf.0)  ==>  0 or +nan.0
>   (* 0 +nan.0)  ==>  0 or +nan.0
>   (* 1.0 0)     ==>  0 or 0.0
>
> It follows from the rules of exactness propagation that (* 1.0 0) may be
> an exact 0 only if (* 0 X) is an exact 0 for _any_ inexact X.

I apologize, I should have admitted that I am going a bit further than
the R6RS strictly requires, based on my understanding of the rationale
behind exactness in Scheme.

It is true that both the R5RS and the R6RS specifically give (* 0 X),
for inexact X, as an example where it is permissible to return an exact
0, without mentioning any associated caveats, e.g. that one must also
make (* 0 +inf.0) and (* 0 +nan.0) be an exact 0 as well.

I suspect the reason that the R5RS did not mention these caveats is that
it does not specify anything about infinities or NaNs.  For example,
MIT/GNU Scheme evaluates (* 0 X) to exact 0 for inexact X, but that is
justified because its arithmetic operations do not produce infinities or
NaNs; they throw exceptions instead.

As for the R6RS, I confess that a strict reading of the exactness
propagation rule does allow (* 0 X) to be 0 for inexact 0, even
(* 0 +inf.0) yields something else.  That's because their rule requires
only that the same result is returned for all possible substitutions of
_exact_ arguments for the inexact ones.  Since the infinities and NaNs
are not exact, they are not considered as possible substitutions.

  One general exception to the rule above is that an implementation may
  return an exact result despite inexact arguments if that exact result
  would be the correct result for all possible substitutions of exact
  arguments for the inexact ones.

I think that the R6RS is wrong here.  As I understand it, the rationale
for the exactness system is to allow the construction of provably
correct programs, despite the existence of inexact arithmetic.  One
should be able to trust that any exact number is provably correct,
presuming that inexact->exact was not used of course.

Is there a compelling reason why (* 0 X) should yield an exact 0 for
inexact X?  Is there a reason more important than being able to trust
that exact values are provably correct?

    Best,
     Mark