[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...