On 3/15/07, David Van Horn <[EMAIL PROTECTED]> wrote:
Robby Findler wrote: > The formal semantics makes no claim to let you reason about the space > behavior of your program! > > You've said twice now that you think the formal semantics is > incorrect. Your explanations of why don't seem right to me, but they > are still vague. Please explain (unless you were talking about space > both times?)The specification of eqv? (9.6) requires: (let ((p (lambda (x) x))) (eqv? x x)) ===> #t But the substitution model and the eqv? rule in the formal semantics: P[(eqv? uproc uproc)] ---> unknown Seems to imply: (let ((p (lambda (x) x))) (eqv? x x)) ===> unknown The formal semantics is missing the location tags as described in 9.5.2, unless I am missing something (not unlikely).
You got it right. But "unknown" is the formal semantics way of saying "I don't cover that". That particular example wouldn't be difficult, tho. The reason it got dropped from the semantics is that it seems quite difficult (and without much value, relative to the difficulty) to cover when eqv? is allowed to return #f. Jacob and I did cover that in the r5 semantics, which appeared at the Scheme workshop. We're also working on a followup version of the r5 semantics that explains this in more detail. I hope you won't mind if I'll refer you to that (forthcoming) paper, for now. Robby _______________________________________________ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
