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:

Expressions
Number	`n⇒n`
Composite	`e₁⇒n₁ e₂⇒n₂ ------------- e₁ op e₂⇒n₃` where `n₃=n₁ op n₂`
Let	`e₀⇒n₀ e₁,x,n₀⇒_se₁' e₁'⇒n₁ ---------------------------- let x = e₀ in e₁⇒n₁`

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

References

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