Lesson 5.2 — Symbol tables: scope stacks, scope marks, persistent maps and de Bruijn indices¶

Techniques: a stack of hash tables (block-structured symbol tables, Dragon book §2.7; ALGOL 60 compilers), one hash table with scope marks and an undo log (Aho et al.; Clang's IdentifierResolver, GCC's binding chains), persistent maps — balanced trees with path copying and hash array mapped tries (Driscoll et al. 1989; Bagwell 2001), de Bruijn indices and levels, and the locally nameless representation (de Bruijn 1972; McBride & McKinna 2004; Charguéraud 2012) · Pebble implements: one hash table with scope marks (the reference resolveNames, exercise E1); all four in the comparison lab (SPEC, L1–L4) · Prerequisites: Lesson 5.1 · Time: 4 hours

Lesson 5.1 defined which declaration a use denotes. A compiler must also find it fast: a large C++ translation unit has millions of identifier occurrences, and an IDE re-resolves on every keystroke. A symbol table is the data structure that answers "what does x mean here?" while the resolver walks the program. This lesson compares four designs that make different operations cheap — lookup, entering and leaving a scope, keeping old versions — and a fifth idea that removes names altogether: de Bruijn indices, which replace every variable by the number of binders between it and its declaration.

1. Problem and motivation¶

The problem. A resolver walks the program in source order and issues a sequence of operations: enterScope, declare(name, d), lookup(name), exitScope. The symbol table must answer each lookup with the static binding of Definition 5.1.2. Beyond correctness, designs differ in the cost of each operation, in whether an old state can be kept after the walk moves on (needed for closures, IDE queries and incremental compilation), and in how they represent binding in the output: by pointer to a declaration, by name, or by a number.

Stack of hash tables¶

The textbook design keeps one table per open scope and a stack of tables; lookup searches from the innermost table outwards [ALSU07, §2.7]. It mirrors the block structure directly and makes leaving a scope trivial (pop one table), but a lookup of a global from depth \(\delta\) probes \(\delta + 1\) tables. Go's type checker (go/types.Scope, one map per scope with a parent pointer) and rustc's late resolver (a stack of ribs) use it.

Single table with scope marks¶

Compilers that care about lookup speed invert the structure: one hash table maps each name to the stack of its currently visible bindings, innermost on top, and an undo log records every declaration so that leaving a scope can remove exactly the bindings it added [ALSU07, §2.7; EaC3, Ch. 4]. Lookup is one probe at any depth. Clang's IdentifierResolver (each IdentifierInfo points to the chain of its visible declarations) and GCC's C front end (I_SYMBOL_BINDING, a chain through c_binding::shadowed) are this design, and so is the reference resolveNames.

Persistent maps¶

Both designs above mutate the table and undo the mutation later, so the table's state at a program point is gone once the walk passes it. A persistent map never changes: declare returns a new map that shares all unchanged parts with the old one [DSST89]. Each scope's environment is then an ordinary value that can be stored in a closure, a query cache or an IDE index. Balanced search trees with path copying give \(O(\log n)\) operations; Bagwell's hash array mapped tries (HAMTs) [Bag01] give practically constant-time ones and are the default maps of Clojure and Scala. GHC's renamer threads persistent environments (LocalRdrEnv) through its walk, and LLVM ships a persistent AVL map (llvm::ImmutableMap) used by the Clang Static Analyzer, which must keep thousands of program states alive at once.

De Bruijn indices and locally nameless terms¶

De Bruijn [dB72] observed that names are only there to connect uses to binders, and replaced each bound variable by a number: how many binders stand between the use and its binder. \x. \y. x becomes \. \. 1. Alpha-equivalent terms (equal up to renaming) become identical, so equality is a tree comparison, and substitution cannot capture. Proof assistants and core languages use it (Lean 4's Expr.bvar, Coq, Agda, Z3's quantifiers, rustc's DebruijnIndex for late-bound regions). Because indices are unreadable and awkward for free variables, the locally nameless representation keeps bound variables as indices and free variables as names [MM04, Cha12]; it is the standard in mechanized metatheory [ACPPW08].

2. Definitions and algorithms¶

Definition 5.2.1 (Symbol-table interface and its specification)

A symbol table supports enterScope(), exitScope(), declare(n, d) and lookup(n). Its abstract state is a list of finite maps (scopes) \(\sigma = \langle m_0, \dots, m_k \rangle\), innermost last: enterScope appends an empty map, exitScope removes the last map, declare(n, d) sets \(m_k[n] := d\), and \(\mathrm{lookup}(n) = m_j[n]\) for the largest \(j\) with \(n \in \mathrm{dom}(m_j)\) (or unbound). A resolver drives it with the resolution walk: visit the program in source order; enterScope at the start of each block; lookup at each use; declare at the end of each declaring statement (so the initializer does not see it, pebble-spec §6.3); exitScope at the end of each block.

Algorithm 5.2.2 (Stack of hash tables)

Input: the operation sequence of the resolution walk.
Output: an answer for each lookup.
Precondition: exitScope is never called on an empty stack.
Postcondition: each answer equals \(\mathrm{lookup}(n)\) of Definition 5.2.1.
Invariant: the stack holds one hash table per map of \(\sigma\), in order, with equal contents.

stack ← empty list of hash tables
enterScope():   push a new empty table on stack
exitScope():    pop stack
declare(n, d):  top(stack)[n] ← d            # replaces an earlier same-scope binding
lookup(n):      for T in stack from top to bottom:
                    if n ∈ T: return T[n]
                return unbound

Theorem 5.2.3 (The resolution walk computes static bindings)

Driving any implementation of Definition 5.2.1 with the resolution walk, the answer to the lookup at each use \(u\) is \(\mathrm{res}_s(u)\) (Definition 5.1.2).

Proof

Consider a use \(u\) and let \(B_0 \sqsupseteq B_1 \sqsupseteq \dots \sqsupseteq B_k = \mathrm{blk}(u)\) be the blocks enclosing \(u\), outermost first. Claim: when the walk reaches \(u\), \(\sigma = \langle m_0, \dots, m_k \rangle\) where \(m_i\) maps each name \(n\) to the last declaration of \(n\) among the statements of \(B_i\) that precede the statement of \(B_i\) containing \(u\). Proof of the claim by induction on the walk: the walk is in source order and blocks are properly nested, so every block opened before \(u\) and not yet closed is some \(B_i\) (a block closed before \(u\) does not enclose \(u\)), and they were opened in the order \(B_0, \dots, B_k\); each exitScope removes the map of a block that ended, with all its declarations. Inside \(B_i\), a declaration \(d\) is declared when its statement ends, which is before \(u\) exactly when that statement precedes \(u\)'s statement in \(B_i\), i.e. when \(d \prec u\) (Definition 5.1.1); a later same-scope declare of the same name overwrites the entry, so \(m_i[n]\) is the last one. Conclusion: the candidates \(C(u)\) are exactly the declarations of \(\mathrm{name}(u)\) recorded at any time in \(m_0, \dots, m_k\), and \(m_i[\mathrm{name}(u)]\) is the last candidate of \(B_i\). lookup returns \(m_j[\mathrm{name}(u)]\) for the largest (innermost) \(j\) that has one — the innermost block with a candidate and, in it, the last candidate: Definition 5.1.2. If no \(m_i\) has the name, \(C(u) = \emptyset\) and the answer is unbound.

Algorithm 5.2.4 (One hash table with scope marks and an undo log)

Input: the operation sequence of the resolution walk.
Output: an answer for each lookup.
Precondition: as in Algorithm 5.2.2.
Postcondition: each answer equals \(\mathrm{lookup}(n)\) of Definition 5.2.1.
Invariant: (I1) for every name \(n\), \(\mathrm{chain}[n]\) lists, oldest first, the declarations of \(n\) made in the currently open scopes, in declaration order; (I2) \(\mathrm{log}\) lists the names of those declarations in declaration order, and \(\mathrm{marks}[i]\) is the length the log had when the \(i\)-th open scope was entered.

chain ← hash table from names to stacks;  log ← empty list;  marks ← empty list
enterScope():   append |log| to marks
exitScope():    m ← pop marks
                while |log| > m:  n ← pop log;  pop chain[n]
declare(n, d):  push d on chain[n];  append n to log
lookup(n):      if chain[n] is non-empty: return top(chain[n])
                return unbound

Lemma 5.2.5 (Scope marks implement the abstract table)

Under the precondition, Algorithm 5.2.4 maintains (I1) and (I2), and \(\mathrm{top}(\mathrm{chain}[n]) = \mathrm{lookup}(n)\) of Definition 5.2.1.

Proof

By induction on the operations. enterScope adds a mark equal to \(|\mathrm{log}|\): no declaration belongs to the new scope yet. declare pushes on both structures, keeping the orders. exitScope: by (I2) the log entries above the popped mark are exactly the declarations of the innermost scope, and by (I1) each such declaration is on top of its name's chain at the moment it is popped — declarations are removed from the log in reverse order, and every declaration of name \(n\) made after \(d\) lies above \(d\) both in the log and in \(\mathrm{chain}[n]\). So exitScope removes exactly the innermost scope's declarations. For lookup: the abstract \(\mathrm{lookup}(n)\) is the binding of \(n\) in the innermost scope that has one, and within a scope the latest; by (I1), the most recently made declaration of \(n\) among the open scopes is on top of \(\mathrm{chain}[n]\), and it belongs to the innermost scope that declares \(n\) (declarations of later-opened scopes are made after those of earlier ones, and an inner scope is opened after the outer ones are). A same-scope redeclaration is later, hence on top, matching the overwrite in \(m_k[n]\).

Definition 5.2.6 (Persistent map, version, path copying)

A map data structure is persistent if every update returns a new version and leaves all earlier versions unchanged and usable. A balanced binary search tree becomes persistent by path copying: an insertion allocates a copy of every node on the root-to-leaf search path (with the rebalancing rotations applied to copies), and points the copies at the unchanged subtrees of the old version. A hash array mapped trie (HAMT) stores a map in a trie indexed by successive 5-bit chunks of the key's hash; each node holds a 32-bit bitmap of occupied slots and a compact array of children, and an update copies one node per trie level.

Algorithm 5.2.7 (Resolution with a persistent map)

Input: a program tree; a persistent map implementation (empty, insert, find).
Output: \(\mathrm{res}_s(u)\) for every use \(u\).
Precondition: insert(E, n, d) returns a map equal to \(E\) except that \(n \mapsto d\); \(E\) itself is unchanged.
Postcondition: every use is bound as by Theorem 5.2.3.
Invariant: the environment \(E\) passed to a statement \(s\) of block \(B\) maps each name to its static binding at the start of \(s\).

function Block(stmts, E):              # E: the environment at the block's start
    for s in stmts:
        E ← Stmt(s, E)                  # a declaring statement returns the extended map
    # nothing to undo: the caller still holds its own E

function Stmt(s, E):
    resolve every use u directly in s (not in nested blocks):  bind u to find(E, name(u))
    for every block C nested directly in s:  Block(C.stmts, E)
    if s declares d:  return insert(E, name(d), d)
    return E

Definition 5.2.8 (De Bruijn indices and levels; locally nameless terms)

For a term tree with binders (λ, let bodies), the binder depth of a node is the number of binders whose scope contains it. If a variable occurrence \(u\) at binder depth \(k\) is bound by a binder at depth \(\ell\) (the binder's own body starts at depth \(\ell + 1\)), its de Bruijn level is \(\ell\) and its de Bruijn index is \(k - \ell - 1\): the number of binders strictly between the use and its binder. A nameless term replaces every bound occurrence by its index and deletes binder names. A locally nameless term replaces bound occurrences by indices but keeps free variables as names; \(\mathrm{open}_x(\lambda.\, t)\) replaces the index that refers to the outermost binder of \(t\) by the name \(x\), and \(\mathrm{close}_x(t)\) is its inverse (it turns free \(x\) into that index).

Algorithm 5.2.9 (Named term to de Bruijn indices via levels)

Input: a term tree over Var, Lam, App, Let (the lab's Lam language).
Output: \(\mathrm{idx}(u)\) for every variable occurrence: its de Bruijn index, or "free".
Precondition: a let x = t1 in t2 binds x in t2 only.
Postcondition: \(\mathrm{idx}(u)\) satisfies Definition 5.2.8 for the static binding of \(u\).
Invariant: \(\mathrm{levels}[n]\) is the stack of levels of the binders of \(n\) enclosing the current node (innermost on top), and \(\mathit{depth}\) is the current binder depth.

depth ← 0;  levels ← hash table from names to stacks
function Walk(t):
    case t of
        Var n:        if levels[n] is empty: idx(t) ← free
                      else: idx(t) ← depth − top(levels[n]) − 1
        App t1 t2:    Walk(t1);  Walk(t2)
        Lam x. b:     Bind(x, b)
        Let x = a in b:  Walk(a);  Bind(x, b)
function Bind(x, b):
    push depth on levels[x];  depth ← depth + 1
    Walk(b)
    depth ← depth − 1;  pop levels[x]

Substitution on nameless terms needs two operations [dB72; TAPL, §6.2]. For \(d \in \mathbb{Z}\) and a cutoff \(c \ge 0\), the shift \(\uparrow^{d}_{c}\) adds \(d\) to every free index \(\ge c\):

\[ \begin{aligned} \uparrow^{d}_{c}(k) &= k \text{ if } k < c, \qquad k + d \text{ if } k \ge c \\ \uparrow^{d}_{c}(\lambda.\, t) &= \lambda.\, \uparrow^{d}_{c+1}(t) \qquad \uparrow^{d}_{c}(t_1\, t_2) = \uparrow^{d}_{c}(t_1)\; \uparrow^{d}_{c}(t_2) \end{aligned} \]

and substitution \([j \mapsto s]\,t\) replaces the free index \(j\) of \(t\) by \(s\):

\[ \begin{aligned} [j \mapsto s]\,k &= s \text{ if } k = j, \qquad k \text{ otherwise} \\ [j \mapsto s]\,(\lambda.\, t) &= \lambda.\, [j+1 \mapsto \uparrow^{1}_{0} s]\, t \qquad [j \mapsto s]\,(t_1\, t_2) = [j \mapsto s]\,t_1\; [j \mapsto s]\,t_2 \end{aligned} \]

A β-step is then \((\lambda.\, t)\; s \longrightarrow \uparrow^{-1}_{0}\bigl([0 \mapsto \uparrow^{1}_{0} s]\, t\bigr)\). Write \(\mathrm{FV}(t)\) for the set of free indices of \(t\): \(\mathrm{FV}(k) = \{k\}\), \(\mathrm{FV}(t_1\, t_2) = \mathrm{FV}(t_1) \cup \mathrm{FV}(t_2)\), \(\mathrm{FV}(\lambda.\, t) = \{\, k - 1 \mid k \in \mathrm{FV}(t),\ k \ge 1 \,\}\).

3. Worked example¶

Running example of Lesson 5.1, Algorithm 5.2.4 (one table, the undo log, the marks; the global scope is entered first):

step	operation	chain	log	marks
1	declare global x = d1	x: [d1]	x	0
2	enter fn g	x: [d1]	x	0 1
3	u1: lookup x → d1	x: [d1]	x	0 1
4	exit fn g	x: [d1]	x	0
5	enter fn f	x: [d1]	x	0 1
6	declare x = d2	x: [d1 d2]	x x	0 1
7	enter block	x: [d1 d2]	x x	0 1 2
8	u2: lookup x → d2	x: [d1 d2]	x x	0 1 2
9	declare x = d3	x: [d1 d2 d3]	x x x	0 1 2
10	u3: lookup x → d3	x: [d1 d2 d3]	x x x	0 1 2
11	exit block (pop log to 2)	x: [d1 d2]	x x	0 1
12	u4: lookup x → d2	x: [d1 d2]	x x	0 1
13	exit fn f (pop log to 1)	x: [d1]	x	0
14	enter fn main	x: [d1]	x	0 1
15	u5: lookup x → d1	x: [d1]	x	0 1
16	exit fn main	x: [d1]	x	0

Compare Lesson 5.1 §3: Algorithm 5.2.2 held the same bindings as a stack of tables ({x:d1} ▸ {x:d2} ▸ {x:d3} at step 10); here the stack is per name, so lookup is one probe while Algorithm 5.2.2 probes up to three tables for u2.

A Lam term, three ways. The lab's language; \(T\) = \x. (\y. x y) (\x. x z):

flowchart TD
  L1(["λx (node 0)"]) --> A1[App]
  A1 --> L2["λy"]
  A1 --> L3["λx"]
  L2 --> A2[App]
  A2 --> X1["x (use 1)"]
  A2 --> Y1["y (use 2)"]
  L3 --> A3[App]
  A3 --> X2["x (use 3)"]
  A3 --> Z1["z (use 4)"]

Persistent map (Algorithm 5.2.7). Versions of the environment, each built from its parent by one insert; nothing is ever removed:

version	built as	contents	used by
\(E_0\)	empty	{}	—
\(E_1\)	insert(\(E_0\), x, λx₀)	{x ↦ λx₀}	the application
\(E_2\)	insert(\(E_1\), y, λy)	{x ↦ λx₀, y ↦ λy}	use 1 → λx₀, use 2 → λy
\(E_3\)	insert(\(E_1\), x, λx₁)	{x ↦ λx₁}	use 3 → λx₁, use 4 → free

When the walk moves from \y. x y to \x. x z, it passes \(E_1\) again: \(E_2\) was never "undone", it is simply no longer referenced. In an AVL tree, \(E_2\) shares \(E_1\)'s node for x and adds one node; \(E_3\) replaces the node for x by a copy with a new value (shadowing is an update, not a push).

Path copying in detail — inserting the keys a, b, c into an empty persistent AVL tree (the lab's solution, PersistentMap::insert):

step	operation	new nodes	root of the new version	old versions
1	insert a into \(V_0\) = ∅	a₁	a₁ (leaf)	\(V_0\) = ∅
2	insert b into \(V_1\)	b₁, a₂ (copy of a₁ with right = b₁)	a₂	\(V_1\) = a₁ unchanged
3	insert c into \(V_2\)	c₁; b₂ (copy of b₁, right = c₁); rotation at a: a₃ (leaf), b₃ (left a₃, right c₁)	b₃	\(V_2\) = a₂ → b₁ unchanged

At step 3 the copy of a's path is right-heavy by 2, so the rebalancing rotation builds new nodes; c₁ is shared by the discarded b₂ and the final b₃, and a₁, a₂, b₁ still form the older versions.

De Bruijn indices (Algorithm 5.2.9), one row per event:

step	event	depth	levels	output
1	enter λx	0 → 1	x: [0]
2	enter λy	1 → 2	x: [0], y: [1]
3	use 1: x	2		\(2 - 0 - 1 = 1\)
4	use 2: y	2		\(2 - 1 - 1 = 0\)
5	leave λy	2 → 1	x: [0]
6	enter λx	1 → 2	x: [0, 1]
7	use 3: x	2		\(2 - 1 - 1 = 0\) (the inner x)
8	use 4: z	2		free
9	leave λx, leave λx	2 → 0	{}

Nameless: \(T = \lambda.\, (\lambda.\, 1\; 0)\; (\lambda.\, 0\; z)\). Renaming the inner x to w gives the same nameless term (Theorem 5.2.11), while \x. (\y. y x) (\x. x z) gives \(\lambda.\, (\lambda.\, 0\; 1)\; (\lambda.\, 0\; z)\) — different.

A β-step in de Bruijn form. Reduce \((\lambda.\, \lambda.\, 1\; 0)\; 5\), where \(5\) is a free index. \(\uparrow^{1}_{0} 5 = 6\); \([0 \mapsto 6](\lambda.\, 1\; 0) = \lambda.\, [1 \mapsto 7](1\; 0) = \lambda.\, 7\; 0\); \(\uparrow^{-1}_{0}(\lambda.\, 7\; 0) = \lambda.\, 6\; 0\), and \(6 - 1 = 5\) inside one binder is the original free index \(5\): the argument was not captured by the inner λ.

Try it

./course drill resolve-scopes --seed 7 --difficulty medium --solution prints the scope-stack trace of a generated program; the lab (ch05-bindbench) runs all three table designs on the same inputs.

4. Invariants and correctness¶

Stack of hash tables¶

Algorithm 5.2.2 keeps its invariant trivially (each operation does to the stack exactly what Definition 5.2.1 does to \(\sigma\)), so by Theorem 5.2.3 it computes static bindings. The only precondition that can fail in practice is an unmatched exitScope, which a resolver that pushes and pops in the same function (as the reference solution does) cannot produce.

Single table with scope marks¶

Lemma 5.2.5 shows that Algorithm 5.2.4 answers every lookup as Definition 5.2.1; with Theorem 5.2.3, it computes static bindings. The invariant it relies on — each exiting scope's declarations are on top of their chains — breaks if a declaration is ever added to a scope other than the innermost one; GCC's bind has a special path for exactly that case (implicit function declarations bound in the file scope), and the reference resolveNames avoids it by recording error symbols in a separate per-function set (Lesson 5.8).

Persistent maps¶

Proposition 5.2.10 (Persistent resolution is correct, and old versions survive)

(a) Algorithm 5.2.7 binds every use to \(\mathrm{res}_s(u)\). (b) An insertion into a persistent AVL tree of \(n\) keys allocates \(O(\log n)\) nodes and leaves every earlier version unchanged.

Proof

(a) By induction on the block structure, with the loop invariant of the algorithm box. Initialization: a block receives the environment at its start (the caller's environment at the statement containing the block). Maintenance: a declaring statement returns \(\mathrm{insert}(E, \mathrm{name}(d), d)\), so the next statement sees \(d\) and every earlier binding except those of \(\mathrm{name}(d)\), which \(d\) shadows (it is in the innermost block, and latest in it); a non-declaring statement returns \(E\). Uses inside \(s\) are resolved in \(E\), which excludes \(s\)'s own declaration (the initializer rule). So \(E\) at a use equals the abstract \(\sigma\) of Theorem 5.2.3 flattened (the innermost binding of each name), and \(\mathrm{find}(E, n)\) is \(\mathrm{lookup}(n)\). (b) An AVL tree of \(n\) keys has height at most \(1.44 \log_2(n + 2)\) [Knu98, §6.2.3]. Insertion copies the nodes on the search path — one per level — and a rebalancing step builds at most two more nodes out of copies (one single or double rotation per insertion). No existing node is written, so every version reachable from an old root is exactly as before.

De Bruijn indices and locally nameless terms¶

Theorem 5.2.11 (Nameless terms identify alpha-equivalent terms)

Two terms are alpha-equivalent (equal up to consistent renaming of bound variables, Theorem 5.1.10) if and only if they have the same shape, the same literals and free names, and the same de Bruijn index at every bound variable occurrence (Algorithm 5.2.9).

Proof

Algorithm 5.2.9's output at an occurrence depends only on the shape of the path from the root and on which binder statically binds the occurrence (its index counts binders between them; Definition 5.2.8), and Algorithm 5.2.9 computes that binder correctly by the argument of Theorem 5.2.3 applied to levels (a per-name stack, as in Algorithm 5.2.4). (⇒) A consistent renaming preserves the shape and, by Theorem 5.1.10, which binder binds each occurrence; so the indices are equal, and free names are untouched by definition. (⇐) Given equal shapes and indices, rename every binder of both terms to a fresh name determined by its position in the tree (for instance its preorder number). Each bound occurrence is then renamed to the name of the binder its index designates — the same position in both trees — so the two renamed terms are identical; each renaming is consistent, so the terms are alpha-equivalent to the same term.

Lemma 5.2.12 (Free indices under shifting)

For all \(t\), \(d\) and \(c\): \(\mathrm{FV}(\uparrow^{d}_{c} t) = \{\, k \in \mathrm{FV}(t) \mid k < c \,\} \cup \{\, k + d \mid k \in \mathrm{FV}(t),\ k \ge c \,\}\), provided \(k + d \ge 0\) for every \(k \in \mathrm{FV}(t)\) with \(k \ge c\).

Proof

By induction on \(t\). Index \(k\): immediate from the definition. Application: both sides distribute over \(\cup\). Abstraction: \(\mathrm{FV}(\uparrow^{d}_{c}(\lambda.\, t)) = \mathrm{FV}(\lambda.\, \uparrow^{d}_{c+1} t) = \{ k' - 1 \mid k' \in \mathrm{FV}(\uparrow^{d}_{c+1} t), k' \ge 1 \}\). By the induction hypothesis, \(k' \in \mathrm{FV}(\uparrow^{d}_{c+1} t)\) iff \(k' = k < c + 1\) or \(k' = k + d\) with \(k \ge c + 1\), for \(k \in \mathrm{FV}(t)\). Put \(m = k - 1\) (the free indices of \(\lambda.\, t\) are exactly these \(m\) for \(k \ge 1\)): the first case gives \(m < c\) (with \(k \ge 1\)), the second gives \(m + d\) with \(m \ge c\) (and \(k' \ge 1\) holds since \(k + d = (m + d) + 1 \ge 1\), because the proviso for \(\lambda.\, t\) gives \(m + d \ge 0\) for \(m \ge c\); the same inequality gives the proviso \(k + d \ge 0\) that the induction hypothesis for \(t\) at cutoff \(c + 1\) needs). That is the claimed set for \(\lambda.\, t\).

Lemma 5.2.13 (The de Bruijn substitution lemma: β-reduction is well defined)

For all \(t\), \(j \ge 0\) and \(s\): \(\mathrm{FV}([j \mapsto s]\, t) \subseteq (\mathrm{FV}(t) \setminus \{j\}) \cup \mathrm{FV}(s)\). Consequently, in \((\lambda.\, t)\, s \longrightarrow \uparrow^{-1}_{0}([0 \mapsto \uparrow^{1}_{0} s]\, t)\) the term being down-shifted has no free index \(0\), so the shift never produces a negative index, and the result's free indices are exactly those of \(\lambda.\, t\) and of \(s\) that the substitution kept.

Proof

By induction on \(t\), for all \(j\) and \(s\) simultaneously. Index \(k\): if \(k = j\) the result is \(s\); otherwise it is \(k \in \mathrm{FV}(t) \setminus \{j\}\). Application: by the hypothesis on both sides. Abstraction: \([j \mapsto s](\lambda.\, t) = \lambda.\, [j+1 \mapsto \uparrow^{1}_{0} s]\, t\). By the hypothesis, \(\mathrm{FV}([j+1 \mapsto \uparrow^{1}_{0} s]\, t) \subseteq (\mathrm{FV}(t) \setminus \{j+1\}) \cup \mathrm{FV}(\uparrow^{1}_{0} s)\), and by Lemma 5.2.12 \(\mathrm{FV}(\uparrow^{1}_{0} s) = \{ k + 1 \mid k \in \mathrm{FV}(s) \}\). Applying the λ-rule (drop \(0\), subtract \(1\)): the first part becomes \(\mathrm{FV}(\lambda.\, t) \setminus \{j\}\), the second becomes \(\mathrm{FV}(s)\). Consequence: with \(j = 0\) and \(\uparrow^{1}_{0} s\) in place of \(s\), the free indices of \([0 \mapsto \uparrow^{1}_{0} s]\, t\) lie in \((\mathrm{FV}(t) \setminus \{0\}) \cup \{ k + 1 \mid k \in \mathrm{FV}(s) \}\), none of which is \(0\); so \(\uparrow^{-1}_{0}\) satisfies the proviso of Lemma 5.2.12 and maps them to \(\mathrm{FV}(\lambda.\, t)\) and \(\mathrm{FV}(s)\) respectively.

Proposition 5.2.14 (Locally nameless: close undoes open)

If \(x\) does not occur free in \(\lambda.\, t\), then \(\mathrm{close}_x(\mathrm{open}_x(\lambda.\, t)) = \lambda.\, t\).

Proof

\(\mathrm{open}_x\) replaces exactly the occurrences of the index that refers to the λ (index \(k\) at binder depth \(k\) inside \(t\)) by \(x\); since \(x\) was not free, these are the only occurrences of \(x\) afterwards. \(\mathrm{close}_x\) replaces every free \(x\) at binder depth \(k\) by index \(k\) — exactly the positions just opened, with the same indices. Every other node is untouched by both. (The side condition is why locally nameless proofs pick \(x\) fresh, the "cofinite quantification" of [ACPPW08].)

5. Complexity¶

Variables: \(n\) identifier occurrences; \(\delta\) the scope nesting depth; \(s\) the number of names visible at a point; \(k\) the key length for hashing.

Technique	lookup	declare	enter / exit scope	keep an old version	space
Stack of hash tables	\(O(\delta)\) expected worst case (one probe per level)	\(O(1)\) expected	\(O(1)\) / \(O(1)\) (drop a table)	copy: \(O(s)\)	\(O(n)\)
One table + scope marks	\(O(1)\) expected	\(O(1)\) expected	\(O(1)\) / \(O(\text{declarations in the scope})\), amortized \(O(1)\)	impossible without copying: \(O(s)\)	\(O(n)\)
Persistent AVL tree	\(O(\log s)\)	\(O(\log s)\) time and new nodes	free (keep the parent's root)	free (Proposition 5.2.10)	\(O(n \log s)\) worst case, less with sharing
HAMT	\(O(\log_{32} s)\), practically constant	same, one node copy per level	free	free	\(O(n \log_{32} n)\)
De Bruijn conversion (Alg. 5.2.9)	\(O(1)\) expected per occurrence	\(O(1)\)	\(O(1)\)	— (the output is the result)	\(O(n)\)

Justification. Stack of tables: a lookup of a name declared only in the outermost scope probes all \(\delta + 1\) tables. Scope marks: each declaration is pushed once and popped once, so exits cost \(O(1)\) amortized over the walk. AVL: height \(\le 1.44 \log_2(s + 2)\) (Proposition 5.2.10). HAMT: the trie has depth \(\lceil \text{hash bits} / 5 \rceil\) and each level is one popcount plus one array access [Bag01].

Pathological family. \(P_d\) = \x0. \x1. ... \x{d-1}. x0 x1 ... x{d-1} (the lab's deepDistinctLam(d)): the use of \(x_i\) is at depth \(d\) and its binder at level \(i\), so the stack of tables probes \(d - i\) tables for it, \(\sum_{i=0}^{d-1}(d - i) = d(d+1)/2 = \Theta(d^2)\) in total; the persistent tree does \(\Theta(d \log d)\) and the level map \(\Theta(d)\). Measured by the lab's ch05-bindbench (reference solutions, RelWithDebInfo build, this course's Linux container): at \(d = 2000, 4000, 8000\) the stack of tables takes 8.1, 40.0 and 196.0 ms (×4.9 per doubling), the persistent map 1.6, 3.6, 8.2 ms and the de Bruijn levels 0.45, 0.98, 2.6 ms. On random, shallow programs (1 million nodes, 4 names) the three are within a factor of two (98, 108 and 53 ms): the asymptotic difference only shows with deep nesting.

Stack of hash tables¶

Chained scopes with parent pointers instead of an explicit stack (Go's types.Scope, Roslyn's Binder chain): the scope objects outlive the walk, so an IDE can ask "what is visible here?" later — at the cost of \(O(\delta)\) lookups.
Small scopes as vectors. Most blocks declare fewer than 8 names; a linear scan of a small vector beats hashing (rustc's ribs are FxIndexMaps, Clang's Scope keeps a SmallPtrSet of declarations for iteration).

Single table with scope marks¶

Binding chains threaded through the identifier (Clang, GCC): the "hash table" is the identifier table built by the lexer, so lookup costs no hashing at all — the token already points to its IdentifierInfo.
Undo logs in general: the same trail-and-restore idea appears in Prolog's trail, union-find with rollback, and SAT solvers' backtracking.

Persistent maps¶

Balanced trees vs HAMTs: trees give ordered iteration and deterministic output; HAMTs give fewer levels and better cache behavior [Bag01]. Okasaki's red-black trees are the classic functional implementation [Oka98].
Transient updates: Clojure's transients mutate a HAMT in place while no one else holds a reference, then freeze it; this recovers imperative speed for batch construction.

De Bruijn indices and locally nameless terms¶

Levels instead of indices: counting from the root instead of from the use makes weakening (adding binders underneath) free but shifting under substitution necessary; normalization-by-evaluation implementations use levels for values and indices for terms.
Locally nameless [Cha12], nominal techniques (Pitts' Nominal Isabelle) and higher-order abstract syntax (binders as host-language functions) trade readability, proof effort and performance; production proof assistants (Lean 4, Coq) use locally nameless terms with de Bruijn indices for bound variables.

7. In real compilers¶

Stack of hash tables¶

Go's type checker gives every scope its own map and a parent pointer (src/go/types/scope.go, Scope.Insert; LookupParent in src/go/types/scope2.go, go1.24.7 [GO-Scope]). rustc's late resolver keeps a Vec<Rib> per namespace, each rib an FxIndexMap from identifiers to resolutions, and searches it from the innermost rib (struct Rib, LateResolutionVisitor in compiler/rustc_resolve/src/late.rs, rustc 1.94.1 [RUSTC-Late]).

Go's scope tree and parent-chain lookup (go/types, Go 1.24)

Reproduce (go 1.24.7):

mkdir -p goscope && cd goscope && go mod init goscope >/dev/null 2>&1
cat > main.go <<'EOF'
package main

import (
    "fmt"
    "go/ast"
    "go/importer"
    "go/parser"
    "go/token"
    "go/types"
    "sort"
)

const src = `package p

var x = 1

func f(n int) int {
    x := n
    if n > 0 {
        x := x * 2
        return x
    }
    return x
}
`

func main() {
    fset := token.NewFileSet()
    file, _ := parser.ParseFile(fset, "p.go", src, 0)
    info := &types.Info{Uses: map[*ast.Ident]types.Object{}}
    conf := types.Config{Importer: importer.Default()}
    pkg, err := conf.Check("p", fset, []*ast.File{file}, info)
    if err != nil {
        panic(err)
    }
    var dump func(s *types.Scope, depth int)
    dump = func(s *types.Scope, depth int) {
        fmt.Printf("%*sscope %v names=%v\n", 2*depth, "", fset.Position(s.Pos()), s.Names())
        for i := 0; i < s.NumChildren(); i++ {
            dump(s.Child(i), depth+1)
        }
    }
    dump(pkg.Scope(), 0)
    type use struct {
        pos     token.Pos
        at, obj string
    }
    var uses []use
    for id, obj := range info.Uses {
        if _, ok := obj.(*types.Var); ok {
            uses = append(uses, use{id.Pos(), fset.Position(id.Pos()).String(), fmt.Sprintf("%s declared at %v", obj.Name(), fset.Position(obj.Pos()))})
        }
    }
    sort.Slice(uses, func(i, j int) bool { return uses[i].pos < uses[j].pos })
    for _, u := range uses {
        fmt.Printf("use %s -> %s\n", u.at, u.obj)
    }
    inner := pkg.Scope().Lookup("f").(*types.Func).Scope().Child(0).Child(0)
    _, obj := inner.LookupParent("n", token.NoPos)
    fmt.Println("LookupParent(n) from the if block finds", obj, "at", fset.Position(obj.Pos()))
}
EOF
go run .

Output (complete):

scope - names=[f x]
  scope p.go:1:1 names=[]
    scope p.go:5:1 names=[n x]
      scope p.go:7:2 names=[]
        scope p.go:7:11 names=[x]
use p.go:6:7 -> n declared at p.go:5:8
use p.go:7:5 -> n declared at p.go:5:8
use p.go:8:8 -> x declared at p.go:6:2
use p.go:9:10 -> x declared at p.go:8:3
use p.go:11:9 -> x declared at p.go:6:2
LookupParent(n) from the if block finds var n int at p.go:5:8

What to notice: every block has its own table of names (the package scope, the file, f's body with n and x, the if statement, the if block), linked by parent pointers; LookupParent walks outwards through them (Algorithm 5.2.2). The use at 8:8 — the right side of x := x * 2 — binds to the outer x: Go makes a short variable declaration visible only after it, like Pebble's let x = x + 1.

Single table with scope marks¶

Clang: IdentifierResolver::AddDecl and RemoveDecl (clang/lib/Sema/IdentifierResolver.cpp, LLVM 23.1.2 [CLANG-IdResolver]) maintain, for each IdentifierInfo, the chain of visible declarations; Sema::PushOnScopeChains adds a declaration to both the current Scope (the undo record) and the chain, and leaving a scope removes the scope's declarations from their chains (Sema::ActOnPopScope). GCC's C front end: bind pushes a c_binding onto I_SYMBOL_BINDING (name) and links it into the scope's list; pop_scope walks that list and restores each shadowed binding (gcc/c/c-decl.cc, gcc-15 [GCC-CDecl]). The reference resolveNames does the same with an llvm::StringMap (solutions/pebble/lib/Sema/Names/src/SymbolTable.h).

What Clang's single table computed: DeclRefExpr → VarDecl

Reproduce (clang 23.1.2; node addresses renumbered #1, #2, … by the perl filter so the output is deterministic):

cat > bind.c <<'EOF'
int x;
int f(void) {
  int x = 1;
  { int x = 2; x++; }
  return x;
}
EOF
clang-23 -fsyntax-only -Xclang -ast-dump -fno-color-diagnostics bind.c 2>&1 \
  | grep -E "VarDecl|DeclRefExpr" | perl -pe 's/0x[0-9a-f]+/$h{$&}||=("#".++$n)/ge'

Output (complete):

|-VarDecl #1 <bind.c:1:1, col:5> col:5 x 'int' external-linkage
    | `-VarDecl #2 <col:3, col:11> col:7 used x 'int' cinit
    | | `-VarDecl #3 <col:5, col:13> col:9 used x 'int' cinit
    |   `-DeclRefExpr #4 <col:16> 'int' lvalue Var #3 'x' 'int'
        `-DeclRefExpr #5 <col:10> 'int' lvalue Var #2 'x' 'int'

What to notice: three declarations of x share one IdentifierInfo; while the inner block is open its chain is #3 → #2 → #1, so x++ binds to #3 with one lookup; ActOnPopScope removes #3 from the chain at the }, so return x binds to #2. The AST records the answer as a pointer in each DeclRefExpr (Lesson 5.6 calls this AST annotation).

Persistent maps¶

GHC's renamer resolves local names in a LocalRdrEnv, a persistent map (OccEnv, a persistent map keyed by unique — an IntMap-based Patricia tree) extended with extendLocalRdrEnv and passed down the recursion (compiler/GHC/Types/Name/Reader.hs, compiler/GHC/Rename/Env.hs lookupLocalOccRn, ghc-9.4.7 [GHC-RdrEnv]); each binder gets a fresh unique, so after renaming, shadowing no longer exists. LLVM's ImmutableMap/ImutAVLTree (llvm/include/llvm/ADT/ImmutableMap.h, ImmutableSet.h [LLVM-ImmutableMap]) is a persistent AVL tree with path copying (Definition 5.2.6), used by the Clang Static Analyzer for program states.

GHC 9.4's renamer: every binder gets a unique

Reproduce (ghc 9.4.7; the uniques depend on the compiler build and can change between runs, the pattern of one unique per binder does not):

cat > Shadow.hs <<'EOF'
module Shadow where
f :: Int -> Int
f x = let x' = x + 1 in (\x -> x * x') (let x = 2 in x)
EOF
ghc -fforce-recomp -c -ddump-rn -dppr-debug Shadow.hs 2>&1 \
  | grep -oE "(\\\\ \()?x'?\{v [a-zA-Z0-9]+\}" | tr '\n' ' '; echo

Output (complete):

x{v au9} x'{v aua} x'{v aua} x{v au9} \ (x{v awN} x{v awN} x'{v aua} x{v awO} x{v awO} x{v awO}

What to notice: the three x binders become three different names (au9, awN, awO); each use carries the unique of the binder it resolved to, so x * x' inside the lambda uses awN (the lambda's x) while x + 1 uses au9 (the parameter). The renamer extended a persistent environment at each binder and never undid anything; the output needs no symbol table at all.

De Bruijn indices and locally nameless terms¶

Lean 4's Expr has a bvar constructor holding a de Bruijn index and fvar for free (locally named) variables — a locally nameless representation (src/Lean/Expr.lean, v4.19.0 [LEAN-Expr]). rustc represents late-bound regions and types with DebruijnIndex (compiler/rustc_type_ir/src/lib.rs, rustc 1.94.1 [RUSTC-TypeIR]). Z3 represents quantified variables as de Bruijn indices (class var in src/ast/ast.h, z3-4.15.3 [Z3-Ast]).

Z3 4.15: quantified variables are de Bruijn indices

Reproduce (CPython 3.11.15; z3-solver 4.15.3.0 from PyPI, run through uv):

cat > debruijn_z3.py <<'EOF'
import z3
print("z3", z3.get_version_string())
x, y = z3.Ints("x y")
f = z3.Function("f", z3.IntSort(), z3.IntSort(), z3.IntSort())
q = z3.ForAll([x], z3.ForAll([y], f(x, y) == f(y, x)))
print(q.sexpr())
inner = q.body()                      # ForAll y. f(x, y) == f(y, x)
body = inner.body()                   # f(x, y) == f(y, x): x and y are now bound variables
lhs = body.arg(0)
for a in lhs.children():
    print(a, "is_var:", z3.is_var(a), "de Bruijn index:", z3.get_var_index(a))
# Alpha-equivalent formulas are the same term: names are only for printing.
a, b = z3.Ints("a b")
q2 = z3.ForAll([a], z3.ForAll([b], f(a, b) == f(b, a)))
print("q.eq(q2) =", q.eq(q2), " hash equal:", q.hash() == q2.hash())
EOF
uv run --no-project --with z3-solver==4.15.3.0 python debruijn_z3.py

Output (complete, after uv's download lines):

z3 4.15.3
(forall ((x Int)) (forall ((y Int)) (= (f x y) (f y x))))
Var(1) is_var: True de Bruijn index: 1
Var(0) is_var: True de Bruijn index: 0
q.eq(q2) = False  hash equal: True

What to notice: inside the body, x (bound by the outer quantifier) is Var(1) and y is Var(0): de Bruijn indices (Definition 5.2.8). The names x, y survive only as annotations on the quantifier nodes, for printing: the alpha-equivalent q2 hashes identically (Theorem 5.2.11), and eq is false only because Z3's AST equality also compares those stored names.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Stack of hash tables	Exact static bindings (Theorem 5.2.3); scopes can be kept as objects	\(O(\delta)\) lookup · 196 ms at depth 8000 in the lab, \(\Theta(d^2)\) on \(P_d\)	Easy to list "names visible here" for suggestions	Lowest	Go, rustc ribs, Roslyn binders, teaching compilers
One table + scope marks	Exact (Lemma 5.2.5); state is destroyed as the walk moves on	\(O(1)\) lookup and amortized exit	Visible names = non-empty chains; suggestions need a scan	Low	Clang, GCC, `pebblec`
Persistent maps	Exact (Proposition 5.2.10); every version survives for free	\(O(\log s)\) (AVL) or near \(O(1)\) (HAMT) · 8.2 ms at depth 8000 in the lab	Environments can be stored in closures, IDE caches, error messages	Medium: a persistent tree or a HAMT library	GHC renamer, functional-language compilers, static analyzers (LLVM `ImmutableMap`), IDEs
De Bruijn indices / locally nameless	Alpha-equivalence is syntactic equality (Theorem 5.2.11); capture-free substitution (Lemma 5.2.13)	\(O(n)\) conversion · 2.6 ms at depth 8000 in the lab	Unreadable without names: keep names on binders for printing	Medium; shifting bugs are subtle	Proof assistants (Lean, Coq), SMT solvers, core IRs, type-level binders (rustc)

Choose a stack of tables when scopes must be first-class objects (IDE queries, parent-pointer lookup) and nesting is shallow. Choose one table with marks for a batch compiler's single resolution walk: it is the fastest and is what Clang, GCC and pebblec use. Choose a persistent map when environments escape the walk — closures in an interpreter, incremental or parallel resolution, analyzers that fork states. Choose de Bruijn indices (or locally nameless) when the program is transformed by substitution and compared up to renaming: type checkers of dependent types, optimizers of lambda-calculus IRs, and hash-consing of terms.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Stack of hash tables	`scope-stack-probes`, `stack-quadratic`	`resolve-scopes` (worked solution shows the stack)	`scope-stack`	lab L1
Single table with scope marks	`undo-log-state`, `find-clang-idresolver`	`resolve-scopes`	`scope-marks`	E1; lab (compare)
Persistent maps	`persistent-versions`, `path-copy-nodes`	— (the lab measures it; a drill would only repeat L2)	`persistent-map`	lab L2
De Bruijn indices and locally nameless terms	`debruijn-indices`, `debruijn-shift`	— (quiz computations and lab L3–L4)	`de-bruijn`	lab L3, L4

References¶

See the chapter references.

Lesson 5.2 — Symbol tables: scope stacks, scope marks, persistent maps and de Bruijn indices¶

1. Problem and motivation¶

Stack of hash tables¶

Single table with scope marks¶

Persistent maps¶

De Bruijn indices and locally nameless terms¶

2. Definitions and algorithms¶

3. Worked example¶

4. Invariants and correctness¶

Stack of hash tables¶

Single table with scope marks¶

Persistent maps¶

De Bruijn indices and locally nameless terms¶

5. Complexity¶

6. Variants and refinements¶

Stack of hash tables¶

Single table with scope marks¶

Persistent maps¶

De Bruijn indices and locally nameless terms¶

7. In real compilers¶

Stack of hash tables¶

Single table with scope marks¶

Persistent maps¶

De Bruijn indices and locally nameless terms¶

8. Comparison¶

9. Assessment¶

References¶