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

From: AndrevanTonder <andre>
Date: Thu Mar 15 12:34:58 2007

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
Received on Thu Mar 15 2007 - 12:34:24 UTC