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