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.

Ticket 477: Formal Objection: Memoization is not possible in portable R7RS

2012-12-07 00:23:11
WG1 - Core
cowan
major
cowan
fixed
source
closed
2012-11-25 09:54:17
defect

Submitter's name: Mark H Weaver

Submitter's email: mhw at netris.org

Relevant draft: R7RS draft 7

Type: defect

Priority: major

Relevant section of draft: Equivalence predicates

Summary: Memoization is not possible in portable R7RS.

Introduction

Memoization requires an equality predicate that is guaranteed to return #f when its arguments are not operationally equivalent. The R6RS provides such a predicate (eqv?), but the R7RS draft does not.

The R7RS draft eqv? provides the needed guarantee only for IEEE-style flonums. For other inexact representations, the R7RS draft imposes a requirement that may conflict with the needed guarantee: it requires that if its arguments are non-IEEE-style inexact numbers and not both NaNs, then = and eqv? must agree.

Conflict Example 1: Signed zeroes

Signed zeroes are meant to preserve the sign in case of a numerical underflow, so that the correct branch is selected along a branch cut. For example, although (= -1.0+0.0i -1.0-0.0i) => #t :

(log -1.0+0.0i) => +πi (log -1.0-0.0i)` => -πi

This ensures that, in some numerical process, if variable z approaches -1.0 from the negative imaginary side, (log z) will not abruptly change from -πi to +πi when the imaginary part of z underflows.

More generally, the usual convention is that (f +0.0) evaluates the limit of (f x) where x approaches zero from above, and (f -0.0) evaluates the same limit from below.

Although the signed zeroes are traditionally associated with IEEE 754, they are a useful concept that might be included in any other inexact numerical representation.

In order to memoize log properly, it must be possible to distinguish -1.0+0.0i from -1.0-0.0i, although those two numbers are =.

Conflict Example 2: Multiple precision arithmetic

Implementations may provide multiple representations of inexact numbers with different precisions, and primitive arithmetic operations may compute a result whose precision depends on the precision of the arguments. For example (sqrt x), where (= x 2.0), may yield a different result depending on the precision of x.

In order to memoize sqrt properly, it must be possible to distinguish a low-precision representation of 2.0 from a high-precision representation of 2.0, although those two numbers are =.

History of eqv? on numbers

The RRRS was the first Scheme report to define eqv? (page 24). It defined eqv? on inexact numbers as follows (this is actually from its definition of eq?, but eqv? was defined as being the same as eq? for inexact numbers):

Returns #!true if obj1 is identical in all respects to obj2, otherwise returns #!false. If there is any way at all that a user can distinguish obj1 and obj2, then eq? will return #!false.

The R3RS explicitly defined EQV? in terms of operational equivalence:

The eqv? procedure implements an approximation to the relation of operational equivalence. It returns #t if it can prove that obj1 and obj2 are operationally equivalent. If it can't, it always errs on the conservative side and returns #f.

Here's the R3RS definition of operational equivalence:

Two objects are operationally equivalent if and only if there is no way that they can be distinguished, using Scheme primitives other than eqv? or eq? or those like memq and assv whose meaning is defined explicitly in terms of eqv? or eq?. It is guaranteed that objects maintain their operational identity despite being named by variables or fetched from or stored into data structures.

It then elaborates what this means for various types, including numbers:

Two numbers are operationally equivalent if they are numerically equal (see =, section see section 6.5.4 Numerical operations) and are either both exact or both inexact (see section see section 6.5.2 Exactness).

This elaboration is all that remained in the R4RS and R5RS.

The R6RS was the first report to explicitly discuss IEEE floating point numbers, signed zeroes, and multiple precisions. The authors recognized the inadequacy of the R5RS definition of eqv? in the presence of these new numbers, and changed the definition of eqv? on inexact numbers to one based on operational equivalence.

The R7RS working group has also recognized the inadequacy of the R5RS eqv?, and adopted language that provides the needed guarantee for IEEE-style floating point numbers. However, the current draft requires that implementations violate the needed guarantee for many types of non-IEEE numbers.

Proposed solutions

  1. Adopt the definition of eqv? on numbers attached below.
  1. Remove the clauses of the R7RS eqv? definition pertaining to non-IEEE-style inexact numbers, thus eliminating the conflict that prohibits implementations from providing the guarantee needed to implement portable memoization.

Proposed R7RS definition for eqv? on numbers

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.

The NaN problem

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 of the R6RS (page 37 of the PDF):

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

[...]

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)
owneralexshinncowan
statusnewaccepted
summaryFormal Comment: Memoization is not possible in portable R7RSFormal Objection: Memoization is not possible in portable R7RS
resolutionfixed
statusacceptedclosed

The R6RS semantics was adopted by the WG.