[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

another nit

    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
    interns structures.

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.