Re: [Scheme-reports] Procedural equivalence: the last debate

[will@x]

Arthur A. Gleckler quoting me:

> > 4.  Require eq? to return #f on procedure arguments unless eqv?
> > returns #t on those same arguments.
> >
> > 5.  Allow eq? to return #f on procedure arguments regardless of
> > what eqv? returns on those same arguments.
> >
> 
> Hi, Will.  Would you mind restating these?  I'm having trouble parsing them
> such that they are not contradictory.

Here's a restatement of both:

4.  If eqv? returns #f when given procedures p1 and p2 as arguments,
then eq? must also return #f when given procedures p1 and p2 as arguments.

5.  If eqv? returns #t when given procedures p1 and p2 as arguments,
then eq? may return #t or may return #f when given procedures p1 and p2
as arguments.

> Also, would you state precisely what you mean by "same arguments?"

That's subtle.  In fact, I think the notion of "same arguments" is too
subtle to define adequately without reference to a mathematical semantics
of some sort, and there are problems even then.

For the denotational semantics found in non-binding appendix A of
IEEE Std 1178, the arguments I'm talking about are the \epsilon_1
and \epsilon_2 seen in the definition of the eqv help function in
section A.4.  Those two arguments would be the same if and only if
their denotations are equal.

(The domain of expressed values E is defined in section A.2, along
with the subdomain F.  Although equality on F is undecidable, the
R5RS definition of the eqv help function looks only at the location
tags, where equality is decidable.)

Note that my proposal would involve changing the part of that help
function that deals with procedures.  Writing tag(e1) instead of
\epsilon_1 | F \downarrow 1, and similarly for tag(e2), and writing
untagged(e1) instead of \epsilon_1 | F \downarrow 2, and similarly
for untagged(e2), that part would change from

    send (tag(e1) = tag(e2) \rightarrow true, false)
         \kappa
to
    send (tag(e1) = tag(e2) \rightarrow true, imp(untagged(e1) = untagged(e2)))
         \kappa

where imp is a new, implementation-dependent help predicate that
satisfies the following axiom:

    if imp(f1, f2) = true, then (f1 = f2)

where the (f1 = f2) indicates equality on (E* -> K -> C).  Although
equality on (E* -> K -> C) is undecidable, implementations can satisfy
the axiom above by defining imp(f1, f2) = false.  With the lower-level
representations used by actual implementations, it would be possible
to recognize more equalities between procedures.

As in appendix A of the R5RS, writing a partially implementation-
dependent semantics for the eq? procedure is left as an exercise for
readers.

Making an equivalent change to the operational semantics of non-binding
appendix A of the R6RS should be easier in concept but more complicated
in practice, partly because that semantics did not retain the notion of
location tags for procedures.  I won't even attempt to explain how the
R6RS operational semantics could be changed to accomodate the proposed
semantics, but there's no fundamental problem here.

Will

_______________________________________________
Scheme-reports mailing list
Scheme-reports@x
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports