[PRL] structural operational semantics

[William D Clinger]

Concerning nondeterministic interleaving of evaluation,
Richard wrote:
> But that's not a property only of structural operational semantics, is
> it?  I can write a semantics that uses evaluation contexts where the
> order of evaluation is unspecified, just as I can write a structural
> operational semantics where the order of evaluation is strictly
> specified. (Of course, the evaluation contexts in that case won't have
> a single well-defined hole, but that's not a requirement of the
> technique.)

No.  Yes.  Correct.

Paul wrote:
> If you wrote out the steps of an SOS evaluation, you'd 
> have to write out the derivations involving antecedents, 
> so you'd see chunkiness.  If you wrote out an evaluation
> of the same term using E[]'s, you wouldn't see those chunks, 
> because they're implicit in the grammar for evaluation 
> contexts.  The same computation may be going on in both 
> cases, but it's presented differently.

Not writing the derivations of an SOS evaluation that
involve antecedents is exactly the same as not writing
out the derivations that show your redex occurs within
a hole context.  Both shortcuts are commonly taken when
writing these things out.

Will