Go backward to Declaration Unions Go up to Top Go forward to Substitutions

Declaration Sequences

Consider D₁;D₂ for declarations.

• Second copy rule:
  • (define I₁=V₁, ..., define I_n=V_n); D
    => define I₁=V₁, ..., define I_n=V_n,
    [V₁, ..., V_n/I_n]D.
  • Translation of D₁;D₂ into D₁,D_n by propagation of bindings of D₁ into D₂.
• Example:
  • fun A=@loc₂; fun B=A+1
    in loc₂:=A+B
    => fun A=@loc₂, [@loc₂/A](fun B=A+1)
    in loc₂:=A+B
    = fun A=@loc₂, fun B=[@loc₂/A](A+1)
    in loc₂:=A+B
    = fun A=@loc₂, fun B=@loc₂+1
    in loc₂:=A+B
    => [@loc₂/A, @loc₂+1/B]loc₂:=A+B
    = loc₂:=(@loc₂)+(@loc₂+1)