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

From: AndrevanTonder <andre>
Date: Fri Mar 16 14:12:58 2007

On Fri, 16 Mar 2007, Robby Findler wrote:

> Okay, sure. You've said that several times now. I agree (for the
> second time): the semantics cannot be used to reason about space
> behavior!
>
> You also stated that the semantics gets sharing wrong. If all you mean
> is the below, then I understand what you mean there is nothing more to
> say, as far as I'm concerned.
>
> But, just in an attempt to be clear to you, I'm claiming that there is
> no observable way in which sharing is wrong.

Except for the incomplete implementation of EQV? on procedures, which you have
said is not technically wrong, but presumably can be observed not to give the
correct answer ;-)

But okay, I'll drop the space behaviour issue for now, given that it is
apparently and unfortunately not a design goal of the editors, after one final
remark: You could easily get a semantics with the space and sharing
behaviour that is implied by the discussion on procedure location tags and eqv?
by a very small modification whereby user procedure parameters are put in the
store (as pairs currently are) rather than substituted directly. Scalar values
and primitives could still be substituted directly, so the readability of many
simple reduction sequences would not be affected.

Given that this seems to be a trivial modification, I think
an implementation in which this behaviour is provided as an option would be
an easy thing to make available. It would be valuable to those of us who are
interested in reasoning about space.

Andre
Received on Fri Mar 16 2007 - 14:12:20 UTC