[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Date: 27 Mar 86 12:01:15 PST (Thu)
From: willc%tekchips%tektronix.csnet at CSNET-RELAY.ARPA
Leibniz's definition of the identity of X and Y goes something like this:
X = Y iff for all properties P, P(X) = P(Y)
If X and Y are identical except for the fact that EQV? or EQ? can
distinguish them, then they're not identical. Hence I don't see why
implementations that disallowed SET-CAR! on quoted lists would be
required to say that (EQV? '(A) '(A)) is #!true.
Well, let Z be some object, and let P be the property of objects X for
which X = Z. Then your definition won't work, because it will be
circular. So we make sure that = doesn't occur in P, and we win.
That's how I define operational equivalence: let's write X = Y when X is
operationally equivalent to Y; I say X = Y iff for all programs P not
involving = (i.e. EQ?, EQV?, MEMQ, etc.), the value and effects of P(X)
are the same as the value and effects of P(Y).
Now = isn't computable, so we define EQV? to be an approximation to =
which in the case of = procedures might return false but will return
true in the cases that Sussman wants it to. So EQV? is a computable
approximation to =.
But by this definition, if it's an error to alter quoted structure, then
necessarily (eqv? '(a) '(a)). Thus my inquiry.
[I guess this begs the question of what "the same as" means, but I think
the definition can be made to work.]
With the current semantics of EQ? and EQV?, I don't believe there's
any hope for an implementation-independent description. I'm sorry.
I agree that EQV? can't be made to work the same in all implementations,
but I think my description captures something reasonable. I should have
been more explicit before.
Yes, it should be an error to clobber quoted structure. In the formal
semantics I use, however, it's simpler to allow side effects. (I don't
want to have to deal with a separate class of immutable structures.)
No, (EQV? '(A) '(A)) should not be required to return true in implementations
that forbid clobbering quoted structure. If it were, (EQV? X Y) would have
to return true if X were a list that was quoted in file "foo" and Y were a
list that was quoted in file "bar". I don't want to write a fasl loader that
Not so - if EQV? had a way to distinguish mutable from immutable data,
it could do exactly what it does with large numbers - a
non-constant-time comparison, similar what EQUAL? does. No interning
necessary, but either extra type codes or a disjoint region of memory in
order to be able to tell when it should do a pointer omparison and when
to look at the components.