Smallstep rules for the explicit-refs machine

================================================================

Expressions:

e ::= n | -(e1,e2)
      zero?(e1) | if e1 then e2 else e3
      x | let x = e1 in e2 | proc(x)e | (e1 e2)
      letrec {f(x)=e}* in e
      begin e; e* end
      newref e | deref e | setref e1 e2
      //---additional expression forms for values, introduced by substitution---//
      %loc(n)       // location values  
      %true              // boolean values
      %false             // 

Configurations:

C ::= <e, s>   where e is an expression and s is a store

================================================================

Values:

v ::= n 
      proc(x)e           // must be closed
      %true, %false
      %location(n)

================================================================

Frames and Reduction Contexts:

F ::= -([],e)		// diff1-frame
      -(v,[])		// diff2-frame
      zero?([])		// zero?-frame
      if [] then e1 else e2   // if-test-frame
      let id=[] in e2  	// let-rhs-frame
      ([] e2) 	   	// app-rator-frame
      (v [])		// app-rand-frame
      begin [] e* end	// begin-frame
      newref []
      deref []
      setref [] e2
      setref v1 []


K = F*

================================================================

Rules (using alternate grouping)


focus-up <[], v, s>  -> v

focus-down <K, n, s>              -> focus-up <K, n, s>
focus-down <K, proc(x)e, s>       -> focus-up <K, proc(x)e, s>
focus-down <K, %true, s> 	  -> focus-up <K, %true, s>
focus-down <K, %false, s>	  -> focus-up <K, %false, s>

focus-down <K, letrec D in e, s>  -> focus-down <K, reduce-letrec(e,D), s>

focus-down <K, -(e1,e2),s>        -> focus-down <K o -([],e2), e1, s>
focus-up <K o -([],e2), v1, s>    -> focus-down <K o -(v1,[]), e2, s>
focus-up <K o -(v1,[]), v2, s>    -> focus-up <K, p, s>  where p = v1-v2

focus-down <K, zero?(e1), s>      -> focus-down <K o zero?([]), e1, s>
focus-up   <K o zero?([]), v1, s> -> focus-up   <K, %true, s>    {or <K, %false, s>}

focus-down <K, if(e1,e2,e3), s>       -> focus-down <K o if([],e2,e3), e1, s>
focus-up   <K o if([],e2,e3), v1, s>  -> focus-down <K, e2, s>       {or <K, e3, s>}

focus-down <K, let x=e1 in e2, s>      -> focus-down <K o let x=[] in e2, e1, s>
focus-up   <K o let x=[] in e2, v1, s> -> focus-down <K, e2[v1/x], s>
// in explicit-refs, "let" doesn't allocate

focus-down <K, (e1 e2), s>             -> focus-down <K o ([] e2), e1, s>
focus-up   <K o ([] e2), v1, s>        -> focus-down <K o (v1 []), e2, s>
focus-up   <K o (proc(x)e []), v2, s>  -> focus-down <K, e2[v2/x], s>  

focus-down <K, begin e1 e* end, s>         -> focus-down <K o begin [] e*, e1, s>
focus-up   <K o begin [] empty, v1, s>     -> focus-up   <K, v1, s>
focus-up   <K o begin [] (e2 . e*), v1, s> -> focus-down <K o begin [] e*, e2, s>

focus-down <K, newref e, s>   -> focus-down <K o newref [], e, s>
focus-up   <K o newref [], v> -> focus-up   <K, %loc(n), s[n = v]> where n not in dom(s)

focus-down <K, deref e, s>            -> focus-down <K o deref [], e, s>
focus-up   <K o deref [], %loc(n), s> -> focus-up <K, v, s> where v = s(n)

focus-down <K, setref e1 e2, s>           -> focus-down <K o setref [] e2, e1, s>
focus-up   <K o setref [] e2, v1, s>      -> focus-down <K o setref v1 [], e2, s>
focus-up   <K o setref %loc(n) [], v2, s> -> focus-up   <K, 27, s[n=v2]>

================================================================

reduce-letrec:

letrec D in e -> e[f_i |-> proc (x_i) letrec D in e_i]_i
  where D = (f_i x_i e_i)_i

================================================================

No-dangling-pointers invariant:

INV(<e,s>): If %loc(n) appears in e or in the range of s, then n is in dom(s).

================================================================

Proposition:

If e contains no subterms of the form %loc(n), and <focus-down <e, empty>> ->* <dir, <e', s'>>,
then INV(<e',s'>) is true.

Proof:

By induction on the number of steps in the reduction.

Base Step: INV <e, empty> is true.

Induction Step: We must show that if INV(<e, s>) and <dir, <e, s>> ->
<dir', <e', s'>>, then INV(<e',s'>).  If %loc(n) appears in <e',s'>
then either it must have appeared in <e,s> or it must have been
introduced by the rule

focus-up <K o newref [], v> -> focus-up   <K, %loc(n), s[n = v]> where n not in dom(s)

If %loc(n) was in e or the range of s, then 

  n in dom(s) \subset dom(s').

If %loc(n) was introduced by the focus-up-newref rule, then n is in
dom(s').

So we're done.

================================================================