[PRL] structural operational semantics

[Dave Herman]

> It's still small-step in the sense that 
> you're left with something that might 
> allow further evaluation.  But, as I said 
> in my response to Will (which might not have 
> gone to the list), the evaluation of M 
> might make this a pretty chunky step.

Not at all. There's only one reduction step that has occurred, it's just 
that the structural rules reflect the evaluation of that step under a 
context. It's exactly the same relation as the compatible closure of the 
single-redex single-step relation.

The difference is just that the compatible closure is a modular way of 
building a larger relation from a smaller one, whereas the structural 
rules build up the larger relation all at once.

Or, as Will puts it:

> 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.

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

Dave