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

[AndrevanTonder]

On Thu, 15 Mar 2007, Robby Findler wrote:

> This is not an "optimization" in the usual sense of the word (altho
> one could make a case it is a cognitive optimization. Those seem good,
> however).

First, I suspect it may be incorrect.  Doesn't simple substitution destroy the 
correct behaviour of eq?

Second, I think it is a cognitive complication.  It introduces a distinction 
that is never mentioned in the informal semantics, in fact clashing with a 
strict reading of the latter.  A newcomer will see applications proceeding 
sometimes in one way and sometimes in another, depending on the presence of 
set! somewhere later in the code.  Comparison with the informal description 
will lead to more surprise.

> The rule is split like that to avoid complicating the semantics when
> no assignments happen. The overall goal is to make it easier to follow
> along with a reduction sequence and a simple substitution is easier to
> follow along with than putting the variable into the store and taking
> it back out again. At least it is in my experience.

This is not obvious to me.  Doesn't simple substitution have the danger of 
leading to exponential explosion in size due to unnecessary copying of the 
argument throughout the body?  I would think that this would happen for many 
common programs, making them harder to follow.

Andre