Go backward to Eager Evaluation Go up to Top Go forward to Semantics of Eager Evaluation

Semantics of Lazy Evaluation

• Store is given when function is invoked.
  • [[p |- define I=U: {I:H}dec]]e s = {I=f},
    where f s' = [[p |- U:H]]e s'.
  • [[p |- invoke I:H]]e s = f s,
    where (I=f) in e.
• Soundness of copy rule:
  • [[ |- define I_j=V_j in C: comm]]
    = [[{} |- [V_j/I_j]C: comm]]{}.
• Relation to core language:
  • Core semantics [[.]]_c, extended semantics [[.]]_a.
  • If C contains no identifiers, then [[C: comm]]_c = [[p |- C: comm]]_a e, for e consistent with p.
• Copy rule semantics:
  • [[ |- define I₁=V₁, ..., I_n=V_n in C: comm]]_a = [[ [V_j/I_j]C: comm]]_c.

Copy rule simpler than basic semantics!