This site is a static rendering of the Trac instance that was used by R7RS-WG1 for its work on R7RS-small (PDF), which was ratified in 2013. For more information, see Home. For a version of this page that may be more recent, see InexactEqvWeaver in WG2's repo for R7RS-large.

Inexact­Eqv­Weaver

cowan
2012-11-26 08:38:21
5history
source

Proposed R7RS definition for eqv? on numbers

[See #477 for detailed background]

Objects obj1 and obj2 are substantially different if and only if one of the following holds:

Inexact numbers z1 and z2 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 z1) and (f z2) either both raise exceptions or yield results that are not substantially different.

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

[...]

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

[...]

Rationale for the above definition

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 circularity problem is addressed by defining substantially different on numbers in terms of = instead of eqv?. The NaN problem (see below) is addressed by making sure that two numbers can only be substantially different from each other if at least one of them is = to itself.

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 should always be 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.

Note also that there is considerable freedom in the choice of procedures to allow in the construction of f. The main requirements are that they are sufficient to amplify arbitrary fine distinctions into coarse ones that are substantially different, and that the procedures are pure functions, i.e. they must not use eqv? or eq? (directly or indirectly), they must not cause visible side effects, and their return values must depend only on their arguments. It needn't be a comprehensive set.

Nontrivial changes in the formulation of eqv? since R6RS

Note: This clause was redundant, but is kept for the case of exact numbers, so that we may restrict our definition of the predicate "operationally equivalent" to inexact numbers only.

"[...] yield {the same,different} 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"

Rationale: If obj1 and obj2 are not numerically equal (and not both NaNs), it trivially follows that obj1 and obj2 are not operationally equivalent, since (+ obj_1) and (+ obj_2)are substantially different.

We now require only that the "implementations must be able to prove that two inexact numbers with the same internal representation are operationally equivalent.

Rationale: It may be difficult or impossible for the implementation to prove that two inexact numbers are operationally equivalent.