Learning path

Full curriculum

Full curriculum

Unit content

Environments and stores in language semantics

Substitution is a useful mathematical model for pure variables, but real languages often separate names, values and mutable storage.

An environment $\rho$ maps names to semantic values or locations. A store $\sigma$ maps locations to the values currently held there.

For example, if

$$\rho(x)=\ell_1$$

and

$$\sigma(\ell_1)=5,$$

then evaluating x follows the environment to location $\ell_1$ and the store to value $5$.

Assignment changes the store while leaving the lexical binding intact:

$$\sigma' = \sigma[\ell_1\mapsto 6].$$

This distinction explains aliasing. If both $x$ and $y$ map to the same location, updating through one name is visible through the other.

Lexically scoped function values also need access to the bindings that were visible where the function was created. An environment provides the semantic structure needed to preserve those bindings after evaluation leaves the defining scope.

Environment-and-store semantics therefore gives a clean formal account of lexical lookup, mutation, references and aliasing without pretending that assignment is ordinary mathematical substitution.