[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
new wording for eqv?
I approve of this. I'm not sure it's complete, but I suspect it's close
enough for all practical purposes.
Nothing is said about quoted structure; is this because the description
of QUOTE says enough?
I'm not happy about "print the same way", because printing is poorly
defined. I'd rather say "STRING=? of SYMBOL->STRING of obj1 and obj2 is
true".
Also, I don't think it specifies to what the following MAY evaluate:
(letrec ((f (lambda () (if (eqv? f g) 'both 'f)))
(g (lambda () (if (eqv? f g) 'both 'g))))
(eqv? f g))
Certainly, if F and G have different behavior, then the call to EQV? must
return false; but the question of whether they have different behavior
depends on what EQV? does. If I consider the report as a predicate to be
applied to <implementation, program, program's-input> tuples to
determine whether a particular implementation conforms on that program
with that input, then the report itself is underspecified. (Of course
conformance may not be a computable function, but that doesn't
bother me.)
Note that
(letrec ((f (lambda () (if (eqv? f g) 'f 'both)))
(g (lambda () (if (eqv? f g) 'g 'both))))
(eqv? f g))
isn't a problem since a proof by contradiction gives the answer:
if they are EQV?, then they do the same thing [def. of EQV?], which means
they do different things [def. of F & G], contradiction; therefore they
cannot be EQV?.
Should we add a caveat somewhere to the effect that if conformance
cannot be refuted, then it holds? Hmm, then if refutability cannot
be refuted, then, uhh...