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
_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
