Lab 5 · One resolver, three symbol tables (and ★ scope graphs)¶

Chapter: 5 · Names, Scopes & Semantic Analysis · Lessons: 5.2 (symbol tables, de Bruijn indices), 5.3 (scope graphs) · Time: 6–10 hours (4–6 without the ★ part) · Tests: ./course test 5 (label ch05, tests ch05.Binders.* and ch05.lab.bench-smoke)

1. Goal¶

You write the same name resolver three times for Lam, a tiny lambda-calculus-like language with let, each time backed by a different symbol-table design from Lesson 5.2:

a stack of hash tables, searched from the innermost table outwards (Algorithm 5.2.2);
a persistent map that is never mutated: each binder creates a new version sharing structure with the old one (Algorithm 5.2.7);
de Bruijn indices: every bound variable becomes the number of binders between it and its binder (Definition 5.2.8, Algorithm 5.2.9).

The tests check that all three agree with the definition of static scoping on hand-written and random programs; you then use the nameless form to decide alpha-equivalence, and measure how the three designs scale with nesting depth. The ★ milestone resolves references in a small module language with nested modules, imports and qualified names by searching a scope graph (Definitions 5.3.5–5.3.6, Algorithm 5.3.7).

You design everything: the tables, the persistent structure (a balanced tree, a treap, a HAMT…), the traversal, the scope graph. The provided code is the contract headers, the parsers, printers and program generators, and the benchmark.

2. The Lam language (provided: `parseLam`, `printLam`, generators)¶

2.1 Syntax¶

term ::= '\' NAME '.' term            # lambda: binds NAME in the body
       | 'let' NAME '=' term 'in' term  # binds NAME in the second term only
       | atom { atom }                  # application, left-associative
atom ::= NAME | INT | '(' term ')'
NAME ::= [a-z_][A-Za-z0-9_']*   (not `let` or `in`)

# starts a comment. A lambda or let extends as far right as possible; write parentheses to use one as a function or an argument (printLam does).

2.2 Meaning of names (the specification the tests use)¶

A variable occurrence is bound by the nearest enclosing \x. or let x = … in whose name is its name, where a let encloses only its body (so let x = x in x has a free first x and a bound second one). Otherwise it is free. This is static scoping with shadowing (Definition 5.1.2).

2.3 The tree (`include/binders/Binders.h`)¶

A Program is a vector of Nodes plus a root index. Kinds: Var (a use: Name), Lit (Value), Lam (binder Name, body Kids[0]), App (Kids[0] applied to Kids[1]), Let (binder Name, bound term Kids[0], body Kids[1]). The parser numbers nodes in this order: a binder node first, then its parts; in an application chain f a b, the atoms f, a, b first, then App(f, a), then App(App(f, a), b). Do not depend on any node order except for reading the hand-written test expectations.

Generators: randomLam(seed, size, names) (many shadowed and some free names), deepDistinctLam(d) = \x0. … \x{d-1}. x0 x1 … x{d-1}, deepShadowLam(d) = \x. … \x. x x, and renameBinders(P) (a capture-free renaming of every binder to a fresh v<k>).

3. Requirements and contract¶

Implement, anywhere under src/, the four functions of include/binders/Binders.h:

using Binding = std::vector<int>;
Binding resolveWithScopeStack(const Program &P);     // L1
Binding resolveWithPersistentMap(const Program &P);  // L2
std::vector<int> toDeBruijn(const Program &P);       // L3
bool alphaEquivalent(const Program &A, const Program &B);   // L4

R1. resolveWithScopeStack returns, for every node index \(i\), the index of the Lam/Let node binding Nodes[i] if it is a Var, \(-1\) if the variable is free, and \(-1\) for every non-Var node. It uses a stack of hash tables, one per open binder, looked up from the top.
R2. resolveWithPersistentMap returns the same, using an immutable map: extending the environment for a binder must not modify any map a caller holds, and must not copy the whole map (at most \(O(\log n)\) new nodes per extension for a tree; one node per level for a HAMT). Nothing is ever "popped".
R3. toDeBruijn returns, for every node: for a bound Var, its de Bruijn index (the number of binders — Lams and Let bodies — strictly between the use and its binder; 0 = the nearest); \(-1\) for a free Var; \(-2\) for every other node.
R4. alphaEquivalent(A, B) is true iff the two programs have the same shape, the same literals, the same free variable names at corresponding positions, and the same de Bruijn index at every bound variable (Theorem 5.2.11). It must not compare binder names.
R5. All functions must handle P.Root == -1 (an empty program) and nesting depths of at least 10 000 without stack overflow in a default 8 MB stack (plain recursion is fine at that depth; a pathological 100 000 is not required).
R6. Performance targets (RelWithDebInfo, a laptop from 2020 or later; measured by ch05-bindbench in L5, not enforced by the tests): on deepDistinctLam(8000), the persistent map and the de Bruijn conversion must finish within 50 ms each; the stack of tables is expected to be quadratic there (the lab's point) but must finish within 2 s; on randomLam(1, 1000000, 4) each resolver must finish within 1 s.

4. What the tests check (`tests/ch05/unit/BindersTest.cpp`)¶

Test	Checks
`Provided_ParsePrintRoundTrip`, `Provided_GeneratorsAndRenaming`	the provided code (these pass before you start)
`L1_ScopeStack`, `L2_PersistentMap`	hand cases (shadowing, `let x = x in x`, free variables) and 300 random programs against an oracle that walks parent pointers (§2.2)
`L3_DeBruijnHandCases`, `L3_DeBruijnDenotesTheRightBinders`	exact index vectors for three terms; on 300 random programs, \(-2\) at every non-variable and indices that denote the oracle's binders
`L4_AlphaEquivalenceHandCases`, `L4_RenamingPreservesAndMutationBreaks`	eleven pairs; 200 random programs are equivalent to their renaming and not to a copy with one bound variable replaced by a free one
`L5_AllThreeAgreeOnDeepPrograms`	depths 1, 2, 500 and 3000 of both deep families, and a 200 000-node random program
`L6_*` (★)	§5
`ch05.lab.bench-smoke`	`ch05-bindbench --quick` runs and the three resolvers agree

Measurement (L5). Run build/<preset>/bin/ch05-bindbench and fill in:

program	nodes	scope stack (ms)	persistent (ms)	de Bruijn (ms)
random N=1000000
deep d=2000 / 4000 / 8000
shadow d=2000 / 4000 / 8000

Then answer: by what factor does each column grow when \(d\) doubles, and why (Lesson 5.2 §5)? Why does shadow not show the stack's quadratic behavior? The reference solutions measured 8.1 / 40.0 / 196.0 ms (stack), 1.6 / 3.6 / 8.2 ms (persistent AVL) and 0.45 / 0.98 / 2.6 ms (de Bruijn levels) on the deep family in the course's Linux container.

5. ★ Scope graphs for a module language (`include/binders/ScopeGraphs.h`, your code in `graphs/`)¶

5.1 The language (provided: `parseModules`)¶

program ::= item*
item    ::= 'module' NAME '{' item* '}' | 'def' NAME ';' | 'import' path ';' | 'ref' path ';'
path    ::= NAME ('.' NAME)*

parseModules builds scopes (0 = the file, one per module body, each with a parent), declarations (def and module, one namespace) and references (ref and import, in source order).

5.2 Meaning (R7)¶

Build the scope graph of Definition 5.3.6 and resolve with Algorithm 5.3.7:

Imports are resolved first, lexically: the first segment by the path \(P^{*} D\) from the import's scope (the nearest scope, going outwards through parents, that declares the name; imports are not used), each further segment by one \(D\) step in the body of the module the previous segment denotes. An import must end at a module (otherwise it is Unresolved); a resolved import adds an \(I\) edge from its scope to the module's body.
References resolve their first segment by \(P^{*} I^{?} D\) with the order \(D < I < P\): at each scope going outwards, the scope's own declarations win; if there are none, the declarations of the bodies imported into that scope (not what they import: imports are not transitive); if there are none, the parent. Further segments are one \(D\) step each, and every segment but the last must be a module.
The result for each element of Refs (imports included) is the index of the declaration of the last segment, Unresolved (−1), or Ambiguous (−2) when the most specific step finds more than one distinct declaration (two defs of one name in a scope, or one name through two imports).

std::vector<int> resolveScopeGraph(const ModProgram &P);   // L6

R8. \(O(\text{refs} \cdot \text{depth} \cdot \text{declarations per scope})\) is fine; the tests are small.

5.3 What the ★ tests check¶

L6_ScopeGraphHandCases (the example of Lesson 5.3 §3, ten references), L6_ScopeGraphAmbiguityAndCycles (mutually importing modules, ambiguity through two imports and two defs), L6_ScopeGraphRandomAgainstEnvironments (400 random programs against an independent environment-based oracle: \(\mathrm{env}(s) = D(s)\) shadowing \(\mathrm{Imp}(s)\) shadowing \(\mathrm{env}(\mathrm{parent}(s))\), Theorem 5.3.11).

6. Milestones¶

Milestone	Command	Passes when
L1	`ctest --preset linux -R 'Binders.L1'`	the scope stack agrees with the oracle
L2	`-R 'Binders.L2'`	the persistent map agrees
L3	`-R 'Binders.L3'`	indices are right
L4	`-R 'Binders.L4'`	alpha-equivalence is right
L5	`-R 'Binders.L5'` and `ch05-bindbench`	deep and large inputs; the table of §4 is filled in
L6 ★	`-R 'Binders.L6'`	scope graphs

(--preset macos on macOS.)

7. Hints¶

Hint 1 — where to start

All three resolvers are one recursive walk over the tree with a different environment. Write the walk once for the scope stack (push a table at Lam, and for Let only around the body), check it against the tests, then change the environment.

Hint 2 — the key idea

Persistent map: pass the environment by value (an index or pointer to an immutable root) down the recursion; a binder calls insert, which copies only the path to the key. An AVL tree or a treap with path copying is about 60 lines; store nodes in a std::vector arena and refer to them by index. De Bruijn: keep, per name, the stack of the levels (binder depths) of its enclosing binders; the index of a use at depth \(k\) bound at level \(\ell\) is \(k - \ell - 1\) (Definition 5.2.8).

Hint 3 — a design sketch

alphaEquivalent: compute toDeBruijn of both programs and walk the two trees in parallel from their roots (node indices differ between the programs, so compare structurally, not by index). ★ Scope graphs: a vector of scopes with parent index, declaration list and a list of imported bodies filled after the import pass; lookup(scope, name, useImports) loops outwards exactly as Algorithm 5.3.7.

8. Stretch goals¶

Replace the AVL tree by a HAMT and compare (Bagwell 2001, Lesson 5.2 §6).
Implement capture-avoiding substitution and β-reduction on de Bruijn terms (Lemma 5.2.13), and check that normalizing a random term and its renaming gives equal nameless terms.
★ Make imports transitive (\(P^{*} I^{*} D\)) and detect import cycles during resolution.