Go backward to Consequences of Correspondence Go up to Top Go forward to Proof of Correspondence

Semantics of Correspondence

• Lazy evaluation semantics of functions:
  • [[pi |- fun I₂=E: {I: tauexp}dec]]e s
       = ({I₂=f}, s)
       where f(s') = [[pi |- E: tauexp]]e s'
  • [[pi |- I₂: tauexp]]e s' = f(s')
       where (I₂=f) in e
• Semantics of expression parameters:
  • [[pi |- define I₁(I₂: tauexp) =
       U: {I₁: tauexp -> theta}dec]]e s
    = ({I₁=g}, s)
       where g f s'
          = [[pi -U- {I₂:tauexp} |- U: theta]](e -U- {I₂=f}) s'
  • [[pi |- invoke I₁(E): theta]]e s = g f s
       where (I₁=g) in e
       and f s' = [[pi |- E: tauexp]]e s'
  • [[pi |- I₂: tauexp]]e s' = f(s')
       where (I₂=f) in e