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

From: Mikael Tillenius <mti>
Date: Thu Mar 15 14:40:43 2007

Thomas Lord wrote:
>
> 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?
>
Isn't this part of why strings is so controversial. Different people
want to implement them in different ways and at the same time be able to
access parts of them in a efficient way.
> 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.
>
It would make it harder to use Scheme as a way to talk about algorithms
and their efficiency if we cannot do some basic assumptions about the
underlying Scheme implementation. Of course one could always say things
like: "On a reasonable implementation this algorithm would be O(n)".
> 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.
It is also interesting to watch how the user alters the semantics of a
program by terminating it prematurely when it fails to respond to user
interaction.

/Mikael
Received on Thu Mar 15 2007 - 14:43:24 UTC