Compound Definitions

In the language FUN definitions were introduced with the let construct. As programs often have many definitions, programming languages offer facilities to compound them. The original definition of FUN had only one phrase class:

Phrase class	Generic name	Phrase forms
Expressions	e∈Exp	x n e1 bop e2 let x = e0 in e1

The new phrase classes for FUN with compound definitions are:

Phrase class	Generic name	Phrase forms
Expressions	e∈Exp	x n e1 bop e2 let d in e
Definitions	d∈Def	x = e d1 ; d2 d1 and d2 d1 in d2

We have introduced sequential definitions, d1 ; d2, simultaneous definitions, d1 and d2, and private definitions, d1 in d2. Each definition creates an environment but just how this is done differs for each type of definition:

• d1 ; d2 imports values for the free variables in d1 from the enclosing environment and exports values for its defined variables into d2. Finally values are exported from both d1 and d2 with d2 taking precedence in the case of common variable names.
• d1 and d2 imports from the enclosing environment into d1 and d2 and exports from both but there can be no common variables names.
• d1 in d2 is similar to d1 ; d2 but exports are from d2 only.

The environment based dynamic semantics for FUN become:

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⊢d⇒E'  EE'⊢e⇒n -----------------------     E⊢let d in e⇒n
Definitions
Simple	E⊢e⇒n ----------------- E⊢x = e⇒{(x,n)}
Sequential	E⊢d1⇒E1  EE1⊢d2⇒E2 -------------------   E⊢d1 ; d2⇒E1E2
Simultaneous	E⊢d1⇒E1  E⊢d2⇒E2 -------------------   E⊢d1 and d2⇒E1E2 where dom(E1)∩dom(E1)=Ø
Private	E⊢d1⇒E1  EE1⊢d2⇒E2 -------------------    E⊢d1 in d2⇒E2

References

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