[PRL] structural operational semantics (fwd)

[Richard Cobbe]

On Tue, May 23, 2006 at 02:39:26PM -0700, Paul A. Steckler wrote:
> Forwarding, per Will's request.
> 
> --
> >From will at ccs.neu.edu  Tue May 23 14:10:43 2006
> To: steck at stecksoft.com
> Subject: Re: [PRL] structural operational semantics
> Paul Steckler wrote:
> > Wait, I thought some of Plotkin's rules have antecedents, 
> > meaning it's not entirely small-step.
> 
> The antecedents take only one step, and the only purpose
> of the rules that have antecedents is to surround that one
> step with an arbitrary context.
> 
> This is quite different from evaluation contexts that have
> a single well-defined hole.  With a structural operational
> semantics, execution can proceed at various sites in an
> interleaved fashion, nondeterministically.

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

For the untyped call-by-value lambda calculus:

    v ::= \x.M
    M ::= v | x | M M

First, unspecified order with contexts:

    E ::= [] | (E M) | (M E)

    E[\x.M v] --> E[M[v/x]]

Under this system, (\w.w \x.x) (\y.y \z.z) could reduce in two different
ways:
    (\w.w \x.x) (\y.y \z.z) --> \x.x (\y.y \z.z)
                            --> \x.x \z.z  
                            --> \z.z
or
    (\w.w \x.x) (\y.y \z.z) --> (\w.w \x.x) \z.z
                            --> \x.x \z.z
                            --> \z.z

Now, fully-specified structural operational semantics:

    \x.M v --> M[v/x]

       M1 --> M1'
    ----------------
    M1 M2 --> M1' M2

       M2 --> M2'
     --------------
     v M2 --> v M2'

Here, because of the way I've written the last inference rule, you may
not reduce in the operand position until the operator is already a
value.  This imposes a unique order of evaluation on (closed) terms;
proof by structural induction on the term.

Richard