Environment Based Dynamic Semantics

It is possible to give a relational semantics for the language FUN that uses environments. The relation ⇒ captures the dynamic semantics, that is to say the semantics of execution. The binary relation ⊢ is the environment relation, we write

E⊢e⇒n
      

to mean that when given the environment E the expression e evaluates to n. The inductive definition of ⇒ follows:

Expressions
Number	E⊢n⇒n
Variable	E⊢x⇒n if (x,n)∈E
Composite	E⊢e1⇒n1  E⊢e2⇒n2 -----------------    E⊢e1 op e2⇒n3 where n3=n1 op n2
Let	E⊢e0⇒n0  E{(x,n0)}⊢e1⇒n1 ----------------------------     E⊢let x = e0 in e1⇒n1

References

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.