Values and Storage

In everyday speech we say "the variable `x` is `5`," blurring together three distinct things a language semantics must keep separate. A value is a self-contained, timeless piece of data — the integer `5`, the string `"cat"`, a function closure, a tuple. Values do not change; the value `5` is always `5`. A location (also called a cell, an address, or an l-value in C terminology) is a place where a value can be stored, and — critically — overwritten. A location has an identity that persists even as the value inside it changes. The store (sometimes called the memory or, in denotational semantics, a function `Store = Location → Value`) records, at each instant of execution, which value currently occupies which location. With this vocabulary, a variable is not a value — it is a name bound to something, and that something is either a value directly or a location. Languages differ starkly here. In a purely functional setting with no mutable variables, binding a name to a value is enough: `let x = 5` associates the name `x` with the value `5`, full stop, and there is no store to speak of (or the store is write-once). But as soon as a language has mutable variables — `x := x + 1` — a name must be bound to a location, because the whole point of assignment is that the same name can denote different values at different times. The location is the stable thing; the value it holds is what changes. This gives us the classic environment–store picture used throughout operational semantics: an environment maps names to locations (or, in value-oriented languages, to values), and a store maps locations to values. Reading a variable means looking up its location in the environment, then looking up that location's current value in the store — a two-step indirection. Assignment updates only the store, leaving the environment (the name-to-location binding) untouched — this is precisely why a `for` loop can reassign a counter without "re-binding" the variable each iteration. This decomposition also explains aliasing: if two names, perhaps in different scopes or under different parameter names, are bound to the same location, then mutating through one name is observable through the other, because they share one entry in the store. Understanding this store-sharing is the single most important prerequisite for reasoning about pointers, references, object mutation, and pass-by-reference parameter passing.

The cleanest way to see the mechanism is to model program state as a pair of maps and watch how each construct transforms them.

• Environment `ρ : Name → Location` — where does a name's storage live?
• Store `σ : Location → Value` — what value currently sits in a given storage cell?

Evaluating an expression that reads a variable `x` is a two-hop lookup: `σ(ρ(x))`. Executing an assignment `x := e` evaluates `e` to a value `v` using the current store, then produces a new store identical to the old one except that location `ρ(x)` now maps to `v`. The environment `ρ` is untouched — assignment never changes what location a name refers to, only what value that location holds. (Rebinding a name to a different location is a distinct operation — e.g., declaring a new local variable that shadows an outer one — and belongs to the theory of Environments.) Declaring a fresh mutable variable is the operation that actually grows the store: it allocates a brand-new location (one not already in the domain of `σ`), installs an initial value there, and extends the environment so the name maps to that fresh location. ``` // State: a pair (ρ, σ) // ρ : Name -> Location (environment: name to storage) // σ : Location -> Value (store: storage to current value) function EVAL(expr, ρ, σ): match expr: case Literal(v): return v case Variable(x): loc = ρ[x] // step 1: name -> location return σ[loc] // step 2: location -> value case BinOp(op, e1, e2): v1 = EVAL(e1, ρ, σ) v2 = EVAL(e2, ρ, σ) return APPLY(op, v1, v2) function EXEC(stmt, ρ, σ): match stmt: case Declare(x, initExpr): v0 = EVAL(initExpr, ρ, σ) loc = FRESH_LOCATION(σ) // pick l not in dom(σ) ρ' = ρ with x -> loc // extend environment σ' = σ with loc -> v0 // extend store return (ρ', σ') case Assign(x, rhsExpr): v = EVAL(rhsExpr, ρ, σ) loc = ρ[x] // location is unchanged σ' = σ with loc -> v // only the store changes return (ρ, σ') // environment unchanged case Seq(s1, s2): (ρ1, σ1) = EXEC(s1, ρ, σ) (ρ2, σ2) = EXEC(s2, ρ1, σ1) return (ρ2, σ2) case If(cond, sThen, sElse): if EVAL(cond, ρ, σ) is true: return EXEC(sThen, ρ, σ) else: return EXEC(sElse, ρ, σ) case While(cond, body): if EVAL(cond, ρ, σ) is true: (ρ1, σ1) = EXEC(body, ρ, σ) return EXEC(While(cond, body), ρ1, σ1) else: return (ρ, σ) ``` Two design points deserve emphasis. First, `Declare` extends both maps, while `Assign` extends neither — it only overwrites one entry of `σ`. This single asymmetry is the formal statement of "declaring makes a new box; assigning fills a box." Second, `FRESH_LOCATION` is what models allocation: every `Declare` (or, in a heap-based language, every object construction) manufactures a new identity in the store that nothing else aliases — until a reference to it is copied, at which point aliasing becomes possible. The same machinery explains aggregate values (arrays, records, objects). A language can treat a compound value as a single indivisible value copied wholesale (value semantics — as with C structs or Python tuples of immutables), or it can treat a variable holding a compound value as actually holding a reference: the store maps the variable's location to an address, and that address in turn is the base of a separate region of the store holding the object's fields. Assignment and parameter passing then only copy the reference (the address), not the object's fields — so two names can end up pointing at the same underlying object. This is exactly why Python lists and Java objects exhibit aliasing on assignment while Python ints and Java primitive `int`s do not.

Complexity. In a real implementation the environment is typically a symbol table (hash map or array indexed by compile-time-resolved offset) and the store is the runtime memory (stack frame slots plus heap). Variable lookup `σ(ρ(x))` is `O(1)` amortized with hashing, or genuinely `O(1)` worst-case when the compiler resolves names to fixed stack/frame offsets at compile time (as in C, Java locals, or Scheme with lexical addressing) — this is one of the main reasons compilers perform static Names, Binding, and Scope resolution ahead of execution rather than doing dynamic name lookup at every access. Assignment is `O(1)`: it is a single write into one store cell, `σ' = σ[loc ↦ v]`, regardless of how large the rest of the program's state is, because the store update is a localized, persistent-map-style overwrite (or, in a real machine, a literal memory write). Declaring a new variable is `O(1)` amortized for allocation (bump-pointer or free-list allocation on stack/heap), though heap allocation can incur `O(1)` amortized but occasionally `O(n)` costs when a garbage collector runs — a cost tied to storage reclamation, not to the value/location distinction itself. None of the core operations (read, write, declare) are asymptotically expensive; the model's cost is dominated by whichever allocation strategy (stack vs. heap) a language chooses, not by the conceptual store itself.

Correctness. The correctness property this model must guarantee is referential transparency of locations under non-aliasing, and predictable sharing under aliasing — informally: "a location's value only changes when an assignment targets that exact location (or aliases of it), and never as a side effect of unrelated operations." This can be stated as an invariant on the operational semantics above:

• Invariant (store locality): For any execution step that is not `Assign(x, …)` targeting location `ℓ = ρ(x)`, the value `σ(ℓ)` is unchanged across that step.
• Invariant (aliasing coherence): If `ρ(x) = ρ(y) = ℓ` at some point in execution, then for every subsequent step that does not rebind `x` or `y` to a different location, `EVAL(x) = EVAL(y)` always holds, because both expressions resolve to `σ(ℓ)`.

These invariants are exactly what the `EXEC` rules preserve by construction: `Assign` is the only rule that mutates `σ`, and it mutates precisely one entry, `ρ(x)`; every other rule (`Seq`, `If`, `While`, `EVAL`) either leaves `σ` untouched or threads it through unchanged except via nested calls to `EXEC` on `Assign`/`Declare`. A simple structural induction on the derivation tree of `EXEC` establishes that no rule can write to a location other than the one explicitly denoted by the assignment target, so the two invariants hold by construction, not merely by testing. This is precisely why the value/location/store separation is the correctness tool for reasoning about mutation: bugs from unintended sharing are, formally, violations of the aliasing-coherence invariant caused by two names unexpectedly denoting the same location.

Tradeoffs. Value semantics (copy on assignment/pass) buys safety — no spooky-action-at-a-distance mutation — at the cost of copying overhead for large aggregates, which is why languages default to reference semantics for big objects and value semantics for small scalars. Reference/aliasing semantics buys efficiency (`O(1)` sharing instead of `O(n)` copying) at the cost of surprising bugs when programmers forget two names share a location. No choice is universally "correct"; the store model simply makes the consequences of each choice precise enough to prove things about.

Trace the following program under the environment/store model, contrasting a value-semantics variable (`int`) with a reference-semantics variable (a list/array bound by reference), the exact situation that trips up learners moving from C-like scalars to Python/Java objects. ``` 1: a := 10 2: b := a // value semantics: copy 3: a := 99 4: L1 := [1, 2, 3] // list literal allocates heap object O1 5: L2 := L1 // reference semantics: copy the reference 6: L1[0] := 777 ```

The key contrast is visible in the last two rows: `b := a` copies the value `10` into a fresh location `ℓb`, so subsequent mutation of `a` cannot touch `b` — this is the "no aliasing" invariant holding because `ρ(a) ≠ ρ(b)`. But `L2 := L1` copies only the reference (`addr(O1)`) — both `ℓ1` and `ℓ2` store the same heap address, so `L1` and `L2` become aliases not of each other's variable location, but of the same underlying object. Mutating through `L1[0] := 777` writes into the shared heap object `O1`, which is why the change is visible through `L2` as well, even though line 6 never mentions `L2`. This is exactly the aliasing-coherence invariant from the previous section, instantiated one level deeper: the aliasing is at the object store, not the variable store, but the reasoning is identical — two names denote one storage cell, so mutation through either is visible through both.

The value/location/store distinction crystallized as programming languages moved from pure mathematical function evaluation toward stateful, imperative computation, and it became a central concern of formal semantics in the 1960s–70s.

Every general-purpose compiler and virtual machine implements this model concretely: stack frames and heaps are the store; symbol tables and register/offset allocation are the environment. Garbage collectors exist because the store must eventually reclaim locations no name can reach — a direct consequence of separating "location" from "name bound to it." Memory-safety bugs in C/C++ (dangling pointers, use-after-free, buffer overruns) are, formally, violations of the store-locality invariant: a name or pointer denotes a location whose lifetime has ended or whose bounds it has escaped. Languages like Rust encode ownership and borrowing rules specifically to enforce, at compile time, that aliasing of mutable locations is either forbidden or provably safe — a direct, modern engineering response to the aliasing-coherence problem described here. Debuggers, memory profilers, and "reference vs. value" documentation in Python, Java, and JavaScript all exist to help programmers reason correctly about exactly this distinction. It is also the conceptual seed for Environments (formalizing the name-to-location map as execution enters and leaves scopes) and for the operational semantics of Expressions and Statements (where statements are precisely the language constructs that transform the store).

Ask the tutor: How does this value/location/store model extend to explain closures capturing variables by reference versus by value?