Go backward to Semantics of Correspondence Go up to Top Go forward to Parameter Lists

Proof of Correspondence

• Equality of meanings:
  • [[fun I₂ = E in ...: theta]e s
    = [[define I₁(I₂:tauexp) = ...
       in invoke I₁(E): theta]]e s

• [[fun I₂ = E in ...: theta]e s
  = [[pi₂|-...:theta]](e -U- {I₂=[[pi|-E:tauexp]]e})s
     where pi₂ = pi -U- {I₂:tauexp}
• [[def I₁(I₂:tauexp)=...in call I₁(E):theta]]e s
  = [[pi |- call I₁(E): theta]]e₁ s
     where pi₁ = pi -U- {I₁: tauexp -> theta},
     and e₁ = e -U- {I₁=g}
     and g f s'=[[pi₂-U-...:theta]](e-U-{I₂=f})s'
  = g f₁ s where f₁ s'=[[pi₁|-E:tauexp]]e₁ s'
  = [[pi₂ |- ...: theta]](e -U- {I₂=f₁}) s
  = [[pi₂ |- ...: theta]](e -U- {I₂=f₂}) s
     where f₂ s' = [[pi|- E: tauexp]]e s'
     (since I₁ does not appear in E)