Go backward to Soundness Theorem Go up to Top Go forward to Declaration Unions

Lazy Evaluation and Copy Rule

• Two styles of function evaluations.
  1. Lazy (call by name).
  2. Eager (call by value).
• Lazy evaluation for abstractions is norm.
  • Body not computed until invocation.
• Example:
  • fun F = @loc₁+1
    in loc₁:=0; loc₁:=F; loc₂:=F+2.
  • @loc+1 is computed each time F is invoked.
• Lazy evaluation supports copy rule.
  • ...fun I=E ...in ...I ...
    = ......in ...E ...
  • Body of I is copied into places of invocation.
  • loc₁:=0; loc₁:=@loc₁+1; loc₂:=(@loc₁+1)+2.

Copy rule suits our intuition of abstractions as abbreviations!