ch:rules-of-dtt: ch:rules-of-dtt

Problem and invariant. Construct the capture-avoiding substitution required by the seminar. Maintain the invariant that crossing a binder either proves the replacement variable fresh for that binder or first alpha-renames the binder to a fresh name.

Two representations. One can use named variables with explicit alpha-renaming, or de Bruijn indices with shifting. The finite companion uses numeric names and checks only the capture decision; the complete project extends that named representation with renaming and substitution. De Bruijn syntax removes alpha-renaming but moves the obligation to the shift and cutoff operations.

First complete version. Define free-variable occurrence and renaming first. Next implement substitution, choosing a fresh binder when the replacement would be captured. Finally traverse judgments and telescope entries in dependency order. Test each layer before extending the syntax.

Observable result. The accepted finite corpus checks $L(y.x)[y/x]$, $L(y.P(x;y))[z/x]$, the two-declaration substitution, and the capture-guard mutation. It prints four named PASS lines and then All 4 Chapter 71 corpus cases passed. A rejected input is represented by a false decision or None; the main oracle negates that result when rejection is expected.

A failing version. Invert the capture guard. The input $L(y.x)[y/x]$ then crosses the binder without renaming it and captures the inserted $y$. This mutation still typechecks, but the named oracle fails, so the inline test harness exits nonzero.

Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact five-line run transcript, and an empty audit. Restore the accepted source after replaying the mutation and repeat all four commands.

Mathematical boundary. The program decides the finite representation and cases just described. It does not prove the substitution equations of proposition 26.11 or the telescope-map laws; those results remain the chapter’s structural inductions.