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

From: Thomas Lord <lord>
Date: Thu Mar 15 13:46:51 2007

Mikael Tillenius wrote:
> 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.

How would you reconcile your category of "reasonable implementation"
with all of the complexity-varying, all useful approaches to implementing
string-ref that people talk about?



>
> 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)).
>

Yes, some of that language probably needs cleaned-up, with particular
attention
to the "must v. should" distinction. My gosh, if we were to get to
that point
before the end of this year, in my view, it'll probably be evidence that
R6 is
shaping up nicely.

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

It may be handy to think about observables. In some sense, the meaning
of a program is how it modulates its output ports and responds to
modulations
of its input ports. There are some temporal constraints that relate those
but mostly in the sense of modeling causality, not performance. It's
useful
to talk about atemporal mathematical objects that relate those modulations
and that's the level of description I'd expect from a formal semantics.
Formal
operational models, of which it appears their can be many useful ones with
critical differences among them, are interesting when we can see that they
in fact satisfy the formal semantic constraints.

-t



> /Mikael
>
>
Received on Thu Mar 15 2007 - 13:56:08 UTC