[PRL] structural operational semantics

[Paul A. Steckler]

Will wrote:

> > One key property of a structural operational semantics
> > is that the antecedent, if any, takes only a single step,
> > and the consequent merely surrounds the antecedent with
> > an arbitrary context.

And Dave chimed in:

> In other words, the compatible closure doesn't add any more 
> "computation," just context-plugging.

Right, I understand this point.  The real "computation" 
occurs at the leaves, and the rules with antecedents plug 
results into larger contexts.  You can view several levels 
of context as one big context.

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.

-- Paul