Go backward to Delayed Evaluation Go up to Top Go forward to Example

Non-strict Store Updates

May store operate on improper values?

• Store = Id -> Nat_{_|_}

  Improper values may be stored.

• update: Id -> Nat_{_|_} -> Store -> Store
  • update = lambda i. lambda n. lambda s. [ i |->n ]s
  • (update [[I]] (E[[E]]s) s) is defined even in the "loop forever situation" E[[E]]s = _|_.
  • Unevaluated expressions may be stored in s.
• E[[E]]s needs not be evaluated until use.
  • Delayed (lazy) evaluation.
  • Value must be determined with respect to the store that was active when [[E]] was saved.