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

From: Robby Findler <robby>
Date: Thu Mar 15 13:58:11 2007

On 3/15/07, David Van Horn <dvanhorn_at_cs.brandeis.edu> 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
Received on Thu Mar 15 2007 - 13:58:03 UTC