[r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations

From: David Van Horn <dvanhorn>
Date: Thu Mar 15 13:48:38 2007

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).

David
Received on Thu Mar 15 2007 - 13:48:24 UTC