Go backward to Altering the Properties of Stores Go up to Top Go forward to Non-strict Store Updates

Delayed Evaluation

How to rewrite a function application f(e)?

• Call-by-value simplification
  • e evaluated before f is executed;
  • Safe method if f is strict.
• Call-by-name simplification
  • f executed with non-evaluated e;
  • Safe method also if f is non-strict.

f: Nat_{_|_} -> Nat_{_|_}
f = lambda x. zero
f(_|_) = zero

E[[e]] = _|_
f(E[[e]]) -> ?

Simplification of argument may require infinite number of steps!