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

From: Mikael Tillenius <mti>
Date: Thu Mar 15 13:21:39 2007

Thomas Lord wrote:
> AndrevanTonder wrote:
>> I would like to be able to reason about the space behaviour of a
>> program using the formal semantics.
>
> Please, no. That would mean that an implementation which did
> not exhibit the space behavior you predict that way is not conforming.
> It sounds to me like you want a mathematical model of space
> behavior *of some particular implementations* (and, you'd want
> a proof that that model is consistent with the formal semantics).
>
> The formal semantics should describe, as far as practical, the
> constraints that apply to all implementations -- but nothing
> more.
Please yes! ;-)

If space and time behaviour cannot be entirely ignored in real world
programming. While it is impossible to describe these in terms of
seconds and bytes a programmer must be able to know whether an algorithm
is O(1), O(n) or O(2^n) in terms of both space and time and this must be
the same on all reasonable implementations.

The report already recognizes this in some places, e.g. tail calls must
not consume any storage and vector-ref is faster than list-ref (most
probably O(1) and O(n)).

However, I recognize that this is rarely (if ever) part of a language
specification.

/Mikael
Received on Thu Mar 15 2007 - 13:24:03 UTC