Declaration Sequences

Consider D_1;D_2 for declarations.

• Second copy rule:
  • (define I_1=V_1, ..., define I_n=V_n); D
    => define I_1=V_1, ..., define I_n=V_n,
    [V_1, ..., V_n/I_n]D.
  • Translation of D_1;D_2 into D_1,D_n by propagation of bindings of D_1 into D_2.
• Example:
  • fun A=@loc_2; fun B=A+1
    in loc_2:=A+B
    => fun A=@loc_2, [@loc_2/A](fun B=A+1)
    in loc_2:=A+B
    = fun A=@loc_2, fun B=[@loc_2/A](A+1)
    in loc_2:=A+B
    = fun A=@loc_2, fun B=@loc_2+1
    in loc_2:=A+B
    => [@loc_2/A, @loc_2+1/B]loc_2:=A+B
    = loc_2:=(@loc_2)+(@loc_2+1)