ch:nominal-syntax: ch:nominal-syntax

Problem and result. Build a finite executable model that exposes the two obligations hidden by paper notation for nominal substitution: a binder removes its atom from support, and substitution must rename a binder that is free in the inserted term. The completed model also checks support transport by one transposition and the shadowing case.

Representation. Use four explicit atoms and nominal STLC terms with variable, application, and lambda constructors. Decide alpha-equivalence by comparing bound variables’ indices in paired binder stacks and free variables by atom equality. Keep freeOccurs separate from occurs: the first proposes the finite support, while the second reserves every name appearing in the bodies used by the deterministic fresh chooser. This conservative reservation makes the printed representative predictable.

First complete version. Implement the transposition on atoms, extend it structurally to terms, and check that the support of Lam A (App (Var A) (Var B)) is exactly the singleton containing B: modulo alpha-equivalence, check the three transposition generators on the complement of B, then check that swapping B with D changes the term. Transport by that last swap and repeat the generator and necessity checks for singleton support D. This is the finite equivariance probe.

Remaining cases. At a variable, replace exactly the target. At an application, propagate the first fresh-atom failure. At a lambda, stop when the binder shadows the target. If the binder occurs freely in the replacement, choose a reserved fresh atom, swap the old binder throughout the body, and continue. A fuel parameter makes this retry explicit and total in Kappa; the public wrapper’s bound exceeds every supplied term. Exhaustion returns NoFreshAtom, preserving the boundary between four test atoms and the chapter’s infinite atom set.

A failing version. Force substitution to descend when the binder equals the target. The program still checks, but the shadowing oracle changes to FAIL. Alternatively, remove binder renaming; the capture oracle then changes to FAIL.

Acceptance test and boundary. Require the four named PASS lines, the exact recorded summary, silent checking, and audit [] under the appendix E commands. The finite decisions illustrate support and capture avoidance; they do not prove least-support existence, nominal induction, recursion, typing preservation, or adequacy.