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⊢e_{1}⇒n_{1} E⊢e_{2}⇒n_{2} where n_{3}=n_{1} op n_{2} 
Let 
E⊢e_{0}⇒n_{0} E{(x,n_{0})}⊢e_{1}⇒n_{1}

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.
Copyright © 2014 Barry Watson. All rights reserved.