[Scheme-reports] Proposed language for 'eqv?' applied to inexact real numbers

[Mark H Weaver <mhw@x>]

I have drafted a new definition of 'eqv?' for inexact real
numbers, to replace both the IEEE and non-IEEE clauses in
R7RS-draft-7.  I believe it overcomes the flaws of the R6RS
definition while remaining true to the principle of operational
equivalence, and without making assumptions about the numeric
representation(s).

The novel feature of this definition is the auxiliary predicate
/substantially different/, which is needed to gracefully avoid
circularities and the problems associated with NaNs, both of
which plagued the R6RS definition.

The NaN problem is addressed by making sure that no two NaNs are
/substantially different/ from each other.  The circularity
problem is addressed by defining /substantially different/ on
inexact numbers in terms of = instead of eqv?, provided that they
are not both NaNs.

Note that there is considerable freedom in how /substantially
different/ is defined.  As long as it is capable of making the
most coarse distinctions between numbers, that's good enough,
because it is always possible to choose a procedure 'f' that
amplifies even the finest distinction between any two inexact
numbers that are not operationally equivalent.

For example, suppose that in addition to the usual +0.0 and -0.0,
an experimental numeric representation was able to distinguish
(x/y+0.0) from (x/y-0.0) for any exact rational x/y.  It would
still be possible to amplify that distinction to an infinite
difference by subtracting x/y and then taking the reciprocal.

I struggled with the choice of operators to allow in the
construction of 'f', but came to realize that it doesn't matter
much.  The main requirements are that procedures should not cause
visible side effects, and that their return values should depend
only on their arguments, i.e. they should be pure functions.  It
needn't be a comprehensive set.  As long as one is able to
amplify arbitrary fine distinctions into coarse ones that are
/substantially different/, that's good enough.

Comments and suggestions solicited.

      Mark


Objects obj_1 and obj_2 are /substantially different/ if and only
if one of the following holds:

* obj_1 and obj_2 are both inexact real numbers, are not =, and
  are not both representations of NaNs.

* obj_1 and obj_2 are both inexact complex numbers whose real or
  imaginary parts are /substantially different/.

* obj_1 and obj_2 are not both inexact numbers, and are not eqv?.

Inexact real numbers x_1 and x_2 are /operationally equivalent/
if and only if for all procedures f that can be defined as a
finite composition of the standard numerical operations specified
in section 6.2.6, (f obj_1) and (f obj_2) are not /substantially
different/.

The eqv? procedure returns #t if one of the following holds:
[...]

* obj_1 and obj_2 are both inexact real numbers, are not both
  representations of NaNs, and the implementation can prove that
  obj_1 and obj_2 are /operationally equivalent/.

The eqv? procedure returns #f if one of the following holds:
[...]

* obj_1 and obj_2 are both inexact real numbers, are not both
  representations of NaNs, and the implementation cannot prove
  that obj_1 and obj_2 are /operationally equivalent/.

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