[PRL] structural operational semantics

[Paul A. Steckler]

Dave wrote:

> Are you being silly, or are you aware that that's a false dichotomy? 
> Gentzen-style inference rules are one way to set up the compatible 
> closure rules on a small-step semantics.

Me, silly?

>          M -> M'
>      ---------------
>      (v M) -> (v M')
> 
> That's still small-step.

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.

With evaluation contexts, there are no 
antecedents, so the steps are "smaller".

That's the point I was trying to convey.

-- Paul