Environments

An environment is a mapping (partial function) from identifiers to denotations — either values directly, or storage locations that hold values (the location indirection matters for mutable variables and is the same idea used when relating Values and Storage to names). Formally, we can write an environment as ``` ρ : Identifier ⇀ Value (direct-value environments), or ρ : Identifier ⇀ Location (location environments, with a separate store σ : Location → Value) ``` The symbol `⇀` denotes a partial function — not every identifier need be in `ρ`'s domain. Looking up `x` in `ρ` is written `ρ(x)`, and it is undefined (an "unbound identifier" error) if `x ∉ dom(ρ)`. Crucially, environments are almost never built as one flat table. Programs are structured into nested scopes — blocks, `let`s, function bodies — and each nested scope contributes a new frame of bindings on top of an existing environment. This gives environments their essential recursive structure: ``` Environment = EmptyEnv | ExtendEnv(name, value, Environment) ``` An environment is either empty, or it is "some existing environment, plus one more binding on top." This is exactly the structure that makes shadowing fall out for free: if the same name is bound twice, the most recently added frame is found first, and older bindings are merely hidden, not destroyed. This is why environments naturally realize the scoping rules discussed in Names, Binding, and Scope rather than needing separate machinery. The final key concept is environment capture. When a function (or any expression with free variables) is created, an evaluator can either capture the environment that was live at that point — producing a closure — or defer environment lookup to whenever the function is later called. The former gives lexical (static) scoping; the latter gives dynamic scoping. This article treats environment mechanics generally; the consequences of when capture happens are the subject of Static vs Dynamic Scope and the step-by-step evaluation semantics built on top of environments are formalized in Evaluation and Reduction of Expressions.

An environment supports three core operations: 1. `empty()` — construct the environment with no bindings. 2. `extend(ρ, x, v)` — construct a new environment identical to `ρ` except that `x` now maps to `v` (shadowing any prior binding for `x`). This does not mutate `ρ`; it produces a new frame chained on top, so any other reference still holding `ρ` is unaffected. 3. `lookup(ρ, x)` — find the value bound to `x`, searching the most recently added frame first, and falling through to older frames on failure. Implemented as a linked chain of frames, this is: ``` PSEUDOCODE — Environment as a chain of frames structure Frame: name : Identifier value : Value # or Location, if using a separate store parent : Environment # pointer to the enclosing environment, or NIL Environment = Frame or NIL # NIL represents the empty environment function empty(): return NIL function extend(rho, x, v): f = new Frame f.name = x f.value = v f.parent = rho # chain onto the existing environment return f # rho itself is untouched (persistent structure) function lookup(rho, x): env = rho while env != NIL: if env.name == x: return env.value env = env.parent error "unbound identifier: " + x function update(rho, x, v): # only meaningful with location-indirection env = rho while env != NIL: if env.name == x: env.value = v # mutate in place — requires a store, not values directly return env = env.parent error "unbound identifier: " + x ``` Two evaluator rules show environments doing real work. First, evaluating a `let`: ``` function eval(expr, rho): match expr: case Num(n): return n case Var(x): return lookup(rho, x) case Add(e1, e2): return eval(e1, rho) + eval(e2, rho) case Let(x, e1, body): v1 = eval(e1, rho) # evaluate the bound expression in the OLD env rho' = extend(rho, x, v1) # build a strictly larger environment return eval(body, rho') # evaluate the body in the NEW env case Lambda(param, body): return Closure(param, body, rho) # CAPTURE the current environment case Apply(f, arg): closure = eval(f, rho) argVal = eval(arg, rho) rho'' = extend(closure.env, closure.param, argVal) # extend the CAPTURED env return eval(closure.body, rho'') ``` The `Lambda` and `Apply` cases are the heart of closures: a function value is not just its code, it is `(code, environment-at-creation)`. When the function is later applied, evaluation resumes not in the caller's environment but in the captured one, extended with the new argument binding. This single design decision is what gives lexically scoped languages their defining property — a function's free variables always resolve to bindings visible in its defining context, regardless of who calls it or from where.

Time complexity of `lookup`. In the naive chained-frame representation, `lookup(ρ, x)` walks the chain from the innermost frame outward, comparing names, so it costs O(d) where d is the lexical depth — the number of enclosing scopes between the lookup site and the frame that actually binds `x`. In the worst case (a variable bound only at the outermost global scope, referenced from deep inside nested functions), d equals the total nesting depth of the program, which is bounded by program size, so lookup is O(n) in the pathological worst case, but O(1) for locals in shallow scopes — which dominate in practice. This can be improved. Compilers typically perform a static resolution pass (Names, Binding, and Scope scope analysis) that computes, for every variable reference, its exact `(depth, slot)` coordinates at compile time. At run time the environment is then represented as an array of frames, each a flat array of slots, and lookup becomes: ``` function fastLookup(envArray, depth, slot): frame = envArray repeat depth times: frame = frame.parent return frame.slots[slot] ``` This costs O(d) to walk parent pointers (still proportional to lexical depth, not program size) but O(1) per frame with array indexing instead of chained name comparison, and d is now a small compile-time-known constant per call site, not something that grows with total program size. Many production implementations go further and "flatten" closures at compile time so that only free variables actually referenced are captured, bounding d by a small constant regardless of true lexical nesting.

Space complexity. Each `extend` allocates one new frame: O(1) additional space per binding, and a chain of k nested bindings occupies O(k) total. Because `extend` is non-destructive (persistent), old environments remain valid and reusable after being extended — this is exactly what closures rely on: capturing `ρ` and later extending it for a call does not corrupt the environment observed by other closures that captured the same `ρ`.

Correctness argument. The central invariant is: > At the point where an identifier `x` is evaluated, `lookup(ρ, x)` returns the value of the binding for `x` that is lexically closest — i.e., introduced by the innermost enclosing `let`/`lambda`/block containing that use of `x`. This is provable by structural induction on the evaluator's environment-construction rules:

• Base case (`Var(x)` at top level): `ρ` is whatever was passed in; `lookup` linearly scans from the head of the chain, so the first (= innermost, by construction) matching frame wins.
• Inductive step (`Let(x, e1, body)`): the evaluator builds `ρ' = extend(ρ, x, v1)` and evaluates `body` under `ρ'`. Any reference to `x` inside `body` finds the new frame before any older frame for `x` in `ρ`, because `extend` places the new frame at the head of the chain. By the induction hypothesis, any other variable reference inside `body` (for names not shadowed) correctly falls through to whatever `ρ` would have resolved, since the new frame simply doesn't match and the walk continues into `ρ`.
• Closures: `Lambda` stores `ρ` (not a symbol referring to "the environment at call time") inside the closure value. `Apply` extends that stored `ρ`, never the caller's environment. Hence free variables in a closure body always resolve relative to the environment live at the closure's creation — the defining property of lexical scoping — and this holds regardless of how many times or from where the closure is later called.

This gives a clean shadowing guarantee (inner bindings always win over outer ones for the same name, without special-casing) and a clean closure guarantee (captured environments are immutable snapshots of bindings, so functions keep working after their defining scope has "returned," which is the mechanism behind returning functions from functions).

Honest tradeoffs. Chained-frame environments with linear lookup are simple to implement and reason about, and are exactly right for a first interpreter or for a specification/semantics document. They are too slow for a production compiler, where the fixed-array/slot-resolved representation (or hashing frames, when scope shape is not statically known — e.g. `eval`, dynamically extensible objects) is preferred. Mutable-location environments (indirection through a store) are required to implement assignment and recursive bindings correctly, but they break the simple "environments are pure values" story and introduce aliasing concerns.

Trace the evaluator over: ``` let x = 1 in let f = fun y -> x + y in let x = 100 in f(10) ``` This program deliberately rebinds `x` after `f` is created, to show that closures freeze the environment at creation time, not at call time.

The final answer is `11`, not `110`. If environments were flattened into a single mutable global table (as a naive implementation might do), the second `let x = 100` would overwrite the first `x`, and the closure would see `x = 100` at call time, wrongly producing `110`. The chained, non-destructive, capture-at-creation environment model is precisely what prevents this bug — it is the mechanical reason lexically scoped closures behave the way programmers expect.

The environment concept crystallized from work connecting the Lambda Calculus-style substitution model of function application to efficient, implementable interpreters — replacing textual substitution with a chain of bindings resolved at run time.

Every interpreter for a lexically scoped language — Python, JavaScript, Scheme, OCaml, Java's local variable resolution — implements some form of the environment chain described here, whether as literal linked frames (simple interpreters, teaching languages) or as compiler-resolved array slots plus a "display" or activation record chain (production runtimes like V8, the JVM, or native-compiled OCaml). Closures in JavaScript, Python's nested functions, and Scheme's `lambda` all rely on capturing an environment at function-creation time; debugging tools that let you "inspect the closure scope" of a paused function are literally showing you that captured environment chain. Compiler back ends use static environment resolution (depth/slot analysis) to turn variable references into direct register or stack-offset accesses, which is why well-compiled local-variable access is O(1) rather than requiring any run-time name lookup at all. The environment abstraction is also the conceptual bridge to Static vs Dynamic Scope (where capture timing is the whole story) and to the formal step-by-step machinery of Evaluation and Reduction of Expressions, where environments appear as an explicit parameter threaded through every evaluation rule.

Ask the tutor: How would you modify the environment and closure rules above to correctly support `let rec`, and why does the naive `Let` rule fail for recursive functions?