Go backward to Lazy Evaluation and Copy Rule Go up to Top Go forward to Declaration Sequences

Declaration Unions

Assume programs uses just D₁,D₂ for declarations.

• Copy rule:
  • define I₁=V₁, ..., define I_n=V_n in U
    => [V₁/I₁, ..., V_n/I_n]U.
  • Bodies V_j are substituted for invocations I_j in U.
  • Simultaneous substitutions V_j/I_j.
• Example:
  • fun A=1, fun B=@loc₁=0
    in while B do loc₁:=A+2 od
    => [1/A, @loc₁=0/B]
    while B do loc₁:=A+2 od
    = while @loc₁=0 do loc₁:=1+2 od

Easy to handle.