Re: [Scheme-reports] Proposed language for 'eqv?' applied to inexact real numbers Mark H Weaver (12 Nov 2012 15:42 UTC)

Re: [Scheme-reports] Proposed language for 'eqv?' applied to inexact real numbers Mark H Weaver 12 Nov 2012 15:37 UTC

Hi Noah,

Noah Lavine <noah.b.lavine@gmail.com> writes:
> The definition you posted has the problem that two NaNs are never
> /substantially different/.

Yes.  This was intentional, and it is needed to avoid the fatal flaw
that Alex Shinn discovered in the R6RS definition.  He discovered
that the R6RS definition of 'eqv?' _never_ requires inexact number
objects to be 'eqv?', even to themselves.  For reference, I have
attached below a copy of an email I recently sent to the r6rs bugs
list describing this problem.

Because NaNs include a large /payload/ that is sometimes used to
record diagnostic information about where the error occurred, we
must make sure that no two NaNs are /substantially different/ from
each other.

Note that the only requirement of the /substantially different/
predicate is that if two inexact real numbers x_1 and x_2 are not
operationally equivalent, it must be possible to find some procedure
'f' (that can be defined as a finite composition of the standard
numerical operations) such that (f x_1) and (f x_2) are
/substantially different/.

To emphasize how much freedom we have here, I suspect that it would
be sufficient to define /substantially different/ as follows: obj_1
and obj_2 are /substantially different/ if one is a positive real
number and the other is a negative real number.

> I would like to suggest an alternate way of defining numbers,
> which I have actually been avoiding suggesting for quite a while,
> but I unfortunately see no way around. It goes something like
> this:

I will respond to the rest of your email later.

    Regards,
      Mark

From: Mark H Weaver <mhw@netris.org>
Subject: R6RS definition of 'eqv?' is broken for inexact numbers
To: bugs@r6rs.org
Date: Sun, 11 Nov 2012 19:49:19 -0500 (14 hours, 28 minutes, 15 seconds ago)

Hi,

Alex Shinn has brought it to my attention that the R6RS definition of
'eqv?' has a fatal flaw.  It is _never_ required to return #true when
applied to inexact number objects, even if both arguments are the same
object.

Here is the relevant excerpt from section 11.5 (page 37 of the PDF):

The eqv? procedure returns #t if one of the following holds:
[...]
* Obj1 and obj2 are both inexact number objects, are numerically equal
  (see =, section 11.7), and yield the same results (in the sense of
  eqv?) when passed as arguments to any other procedure that can be
  defined as a finite composition of Scheme’s standard arithmetic
  procedures.

The problem has to do with NaNs.  Since (= obj1 obj2) is needed for the
above condition to apply, and a NaN object is not '=' to itself, it
follows that (let ((x +nan.0)) (eqv? x x)) => unspecified.

Now consider an arbitrary finite inexact number object 'z'.  The R6RS
only requires (eqv? z z) => #t if the above condition applies, which in
turn requires that (eqv? (f z) (f z)) => #t for any procedure 'f' which
is "a finite composition of Scheme's standard arithmetic procedures."

This condition is never satisfied, because it is trivial to produce an
'f' that meets the above requirements and yet always returns +nan.0,
e.g.:

  (lambda (z) (/ (* z 0.0) 0.0))
  (lambda (z) +nan.0)

Another problem with the R6RS definition is that it is circular.

    Regards,
      Mark

_______________________________________________
Scheme-reports mailing list
Scheme-reports@scheme-reports.org
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports