Substitution Based Dynamic Semantics

It is possible to give a relational semantics for the language FUN that uses substitutions. The relation captures the dynamic semantics, that is to say the semantics of execution. The relation s is the substitution relation. The inductive definition of follows:

Number n⇒n
Composite e1⇒n1  e2⇒n2
  e1 op e2⇒n3
where n3=n1 op n2
Let e0⇒n0  e1,x,n0se1'  e1'⇒n1
    let x = e0 in e1⇒n1

No rule is given for variables as it is assumed there are no free variables.


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