John Cowan <cowan@mercury.ccil.org> writes:

> Mark H Weaver scripsit:
>
>> 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/.
>
> What is the operational definition of "can prove"?  I say my
> implementation can't prove anything about inexacts, and then
> (eqv? inexact1 inexact2) always returns #f.

It is easy to prove that numbers represented by the same bit patterns
are operationally equivalent, given that the arithmetic operations are
all pure functions.  This "same bits" approach is a perfectly good way
to implement 'eqv?'.

Anyway, there is a longstanding precedent for this "implementation can
prove" language in section 1.1.  This text has not changed since the
RRRS:

   All objects created in the course of a Scheme computation, including
   procedures and continuations, have unlimited extent. No Scheme object
   is ever destroyed. The reason that implementations of Scheme do not
   (usually!) run out of storage is that they are permitted to reclaim
   the storage occupied by an object if they can prove that the object
   cannot possibly matter to any future computation.

You could just as easily say:

   What is the operational definition of "can prove"?  I say my
   implementation can't prove anything about whether an object matters
   to future computations, and then no memory will ever be freed.

      Mark

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