EQV? and procedures etc

[Jonathan A Rees <JAR@MIT-MC.ARPA>]

While we're stirring up the EQ? muck, I would like to stir up some EQV?
muck.

I would like it if the description of EQV? did NOT appeal to the
definition of EQ?.  In fact, I would like it to be deterministic.  That
is, while the meaning of (EQ? x y) is a function of an implementation,
the meaning of (CAR x) is not, and I would like EQV? to have the same
deterministic status as CAR.

A consequence of this is that unlike EQ?, the domain of EQV? would be
incomplete, that is, it might be an error to call it on certain
combinations of arguments.  For example, if both arguments are
procedures, or both arguments are inexact numbers, it should be
undefined (and implementations are permitted to signal an error).

Examples:  (EQV? 'A CAR)   =>  false   - different types
	   (EQV? (CONS 1 2) (CONS 1 2))   =>  false
	   (LET ((Z (FOO))) (EQV? Z Z))   =>  true
	       this would hold for any expression (FOO)
	   (EQV? (LAMBDA (X) X) (LAMBDA (Y) Y))
	        =>  wrong   - returning a consistent answer in all
		    implementations would impose horrible
		    constraints on implementations
	   (EQV? CAR CDR)  =>  wrong   - similarly
	   (EQV? #i1 #i1)  =>  wrong   - similarly

Of course, the exact behavior of EQV? in undefined situations is
unspecified; implementations may find it more efficient to fail to
detect domain errors than to detect them.

In other words, I want EQV? to strive to be the true mathematical
equality-of-denotation predicate which we would like to have but can't
(both for implementation and decidability reasons).  It would
necessarily then have an incomplete domain.

If people seriously object to this I won't bother trying to make it more
precise; if they don't, and someone wants it to be made more precise,
I'll try to do so.