Paul Schlie wrote:
>> bear wrote:
>> ...
>> I think we come down to this point, and my final recommendation
>> on the matter - which is more broadly applicable than just talking
>> about nontermination itself. The standard needs to say explicitly
>> that if an implementation can prove that there is only one possible
>> return value from an error-free execution of some code, then
>> it may elide the execution of the code and return that value.
>> ...
>>
>
> (let wait-for-x () (if (not (eqv? (read-char) #\x)) (wait-for-x)))
>
> for example, can never be justifiably optimized away regardless of
> it's resulting value (if any).
>
> (As such expressions have both temporal and value state side effects;
> i.e. prevents execution from proceeding until some externally controlled
> event occurs, and modifying the sequential value state of port stream
> by in this example consuming all sequentially preceding characters and
> thereby modifying the port's logical state.)
>
>
>
Careful there.
Nobody seems to disagree that the '(read-char)' prevents the
loop from being optimized away in most cases (but consider a
virtual port which is not externally observable). Yet, you open
up a can of worms if you say "regardless of [the loop's] resulting
value."
The loop is always executed in the context of a continuation (or multiple
continuations of '(read-char)' can raise exceptions). The combination of
the loop with those continuations is itself the continuation(s) of whatever
invokes the loop.
When the loop is invoked, it is implicitly passed a parameter or parameters
which, informally speaking, represent various kind of mutable state. For
example, a "store" parameter captures what is knowable about all accessible
mutable objects in the program; similarly, we can imagine a "ports"
parameter
that tells us what we know about all of the ports.
"Returning from the loop" means invoking one of its continuations,
passing it updated values of implicit parameters like the "store" and the
"ports". What you are thinking of as "temporal and value state side
effects" is still, when we talk about the formal meaning of Scheme,
part of the "return values".
When you talk about "externally controlled events" that really
points to a challenge for defining what Scheme programs portably
mean. A formal[izable] mathematical model might include,
say, some kind of "trace" -- that is to say that the implicit "the state
of all the ports" parameter being passed around could include a list
of things that are known to have happened (or known to have possibly
happened) in what order (or possible orders) that could be externally
observable:
0. A character was read from port X.
1. Another character was read from port X.
2. Yet another character from port X.
[and then the loop terminated]
[somewhere in a continuation of the loop: ]
3. A character was written to port Y.
How should we define the rules for what that trace contains?
A naively operational approach (roughly how, for example, C is
defined) essentially specs out a reference implementation for the
language and says "Your implementation must produce the same
results as this one." (Of course, even in such an approach you can
tolerate ambiguity -- the reference implementation can be ambiguous
in some places and the rule can be that implementations are free to
choose from among the ambiguous possibilities.)
Definitions like that are expressed in terms of step-wise
temporal properties: "First, the READ-CHAR is evaluated,
then the IF, etc." You seem to want such a definition for
Scheme when you say "regardless of its return value."
A big problem with that approach is that it often doesn't clearly
(and even clearly often doesn't) give us what we need to prove
the equivalence of the reference implementation spec and an
actual implementation that may be based on very different
programming techniques. Why is that?
Well, given a particular program and a naive operational semantics,
if I want to know what I can say for sure about the trace of I/O
operations (for example), then initially all I can do is, kind of,
run the reference implementation and find out. I can do the same
thing for the proposed implementation whose conformance to the
spec we want to check. But, more, and some other kind of math
is needed if we want a general proof of the conformance of a
proposed implementation.
That "other kind of math," generally speaking, involves creating
axiomatic systems that characterize the classes of constructible
values, including both ordinary parameters and implicit ones
like "store" or "ports". You still wind up talking about and modeling
things like the temporal properties of observable side effects of
a program -- but in doing so, you're still talking about the "value
of an expression".
-t
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://lists.r6rs.org/pipermail/r6rs-discuss/attachments/20070309/fb24ffa4/attachment.htm
Received on Fri Mar 09 2007 - 13:24:18 UTC