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

*To*: "Arthur A. Gleckler" <scheme@x>*Subject*: Re: [Scheme-reports] Procedural equivalence: the last debate*From*: will@x*Date*: Tue, 4 Jun 2013 14:06:19 -0400 (EDT)*Cc*: William D Clinger <will@x>, scheme-reports <scheme-reports@x>*In-reply-to*: <2699306.2292471370369055520.JavaMail.root@zimbra>

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

- Prev by Date:
**Re: [Scheme-reports] Procedural equivalence: the last debate** - Next by Date:
**Re: [Scheme-reports] Procedural equivalence: the last debate** - Previous by thread:
**Re: [Scheme-reports] Procedural equivalence: the last debate** - Next by thread:
**Re: [Scheme-reports] Procedural equivalence: the last debate** - Index(es):