appendix sectiontutorials

ch:mendler-recursion: ch:mendler-recursion

Problem and result. Implement capture-free renaming and substitution for the chapter’s nested de Bruijn terms. The accepted run substitutes free variable $7$ under one lambda, checks renaming identity and a two-step fusion instance, and rejects the unshifted mutation with capture-detected.

Representation. The executable image flattens $zeroV / sucV$ to de Bruijn naturals: Var index, App, and Lam. A depth parameter marks the first free index. This is portable Kappa, while the chapter’s indexed family is the mathematical representation that rules out ill-scoped terms by type.

First complete version. Define renameAt depth ren. Indices below depth remain bound; every other index is translated relative to the cutoff. Entering a lambda increments depth. Identity on the sample must leave the entire tree unchanged.

Remaining cases. Define cutoff-aware shifting and substitution:

case Var index ->
  if index == wanted + depth then
    shiftAbove depth 0 replacement
  else Var index
case Lam body ->
  Lam (substituteAt (Nat.Succ depth) wanted replacement body)

Check the printed image lam(app(zeroV,sucV(7))), then compare successive renamings $0 \mapsto 2 \mapsto 5$ with their composite.

A failing version. Insert the replacement without shiftAbove. Under the lambda its free indices are treated as though they were already in the extended context; the result differs from the named capture-free oracle and is rejected with capture-detected.

Acceptance test. Require the four exact verdict lines, the final four-case summary, and audit result [] under the commands recorded in appendix E.

Mathematical boundary. The corpus tests a flattened finite representation. It does not implement a rank-polymorphic Mendler combinator, prove parametricity or normalization, or establish renaming and substitution laws for all nested terms.