Go backward to Eager Evaluation Semantics Go up to Top Go forward to Lazy and Eager Evaluation Combined

Eager Evaluation Semantics

• Type semantics (contd)
  • eval({i:theta_i}_{i in I}) = { i: eval(theta_i) }_{i in I}
  • eval(theta₁ -> theta₂) = eval(theta₁) -> [[theta₂]]
  • eval(comm) = Store
  • eval(tauexp) = [[tau]]
• Properties:
  • Use store argument to force evaluation of phrases that bind to identifiers.
  • Soundness of typing rules preserved.
  • Copy rule does not hold.
• Strictness:
  • { I = bottom } = bottom
  • f bottom = bottom
• Non-termination arises in language!