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

[AndrevanTonder]

On Thu, 15 Mar 2007, Robby Findler wrote:

>> 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.
>
> Substitution is a very simple way to think of function application,
> going back to some of our earliest exposure to mathematics in school
> (at least in this country).

I don't dispute that, but this is not how the text describes function 
application.

While being pedagogical is not a bad secondary goal, a formal semantics must be 
correct first.  I would like to be able to reason about the space behaviour of 
a program using the formal semantics.  Direct substitution can change a
program's space behaviour from polynomial to exponential.

Given this, as far a space behaviour is concerned, the current semantics is 
incorrect (compared with the body of the report).

Andre