ch:erasure-execution: ch:erasure-execution

Problem, result, and invariant. Delete static arguments while preserving the constructor and closure shapes needed by untyped execution. Maintain the invariant that every target constructor has its declared runtime arity and every closure environment has the stored runtime length; an erased variable never controls a runtime branch, and an erased application is accepted only when its erased lambda head is exposed as an administrative redex.

Representation tradeoff. A typed target such as System Fi can retain enough type structure for a target preservation theorem. The companion uses untyped algebraic values and tagged closures. The typed target offers stronger static guarantees; the untyped target makes the exact data erased from vectors and applications observable and matches the chapter’s Texec boundary.

First complete version. Build the three parts separately. First, mark every source variable, binder, constructor field and argument runtime or erased. Implement Rel-Pair/Rel-Fst/Rel-Snd before the eliminators, because the pair probe verifies that unmarked dependent components remain present. Represent retained reflexivity by $C_{\mathsf{refl}}$. Compile Boolean elimination to a case, erase identity proof and motive while substituting the endpoint into its branch. The primitive natural/vector occurrence-tag compiler remains outside this runner; the ordinary recursive declaration below exercises the same closure/call evaluator. An erased binder disappears; a visible erased administrative application keeps only its function, while a variable-headed erased application is rejected. Second, write the Texec evaluator for the chapter’s six target rules, with closed-value substitution, constructor blocks, case selection and closures carrying their captured environments. Third, erase the coiterator to a stream block holding a head thunk and a tail closure, and force exactly one of them per observation symbol.

Remaining cases. Do not implement append over the source terms; erase the recursive declaration, keeping only its runtime captures and runtime parameters, and let the evaluator run the compiled closure. The target arity then is the number of runtime parameters, and printing it makes the invariant observable. Make fuel a checked budget so exhaustion prints out-of-fuel and is distinguished from a stuck configuration. Add two target-shape probes: the visible erased redex erases to its body, while the variable-headed erased application is rejected before translation. Add a global constructor signature, pairwise-distinct branch-tag checking, retained-but-unused and unretained-used branch fixtures, an inconsistent binder fixture, and open lambda/case substitutions that force deterministic freshening.

Observable result. The exact run is

append-two-singletons=vcons(a,vcons(b,vnil))
append-runtime-arity=2
from-0=0,1,2,3
sigma-projections=a,b
bool-elim=suc(zero)
J-erasure=a
J-alpha=lam(y',y)
branch-alpha=case(K(a,b)){K(x'',x')=>pair(x,x')}
refl-value=refl
retained-unused-branch=zero
rejected: erased-branch-use at inconsistent relevance annotation
rejected: unretained-branch-use at inadmissible branch relevance at hiddenbox
rejected: inconsistent-constructor-signature at inconsistent constructor signature
rejected: duplicate-case-tag at duplicate case tag
rejected: inconsistent-binder-relevance at inconsistent relevance annotation
rejected: standalone-erased-lambda at no runtime relevance derivation
rejected: erased-boolean-branch at erased scrutinee proof
erased-application=f
rejected: non-administrative erased application
All 19 Chapter 126 corpus cases passed.

The fourth through tenth lines expose Sigma, Boolean, identity, freshening, reflexivity, and retained-field rule families. The twentieth line is the repository ownership marker; the inline test owns the entire exact transcript.

Eight failing versions. Retain erased binders in the target. The mutant still typechecks, but the compiled append now has runtime arity five against a two-argument call and gets stuck on an arity mismatch. The remaining independent mutants allow an erased scrutinee, derive branch arity from branch use, bypass branch admissibility, omit both freshening functions, ignore the binder environment, bypass constructor-signature comparison, and accept duplicate tags. Each changes its named observable while preserving Kappa typechecking.

Acceptance test. Run the four commands in subappendix E.5. Require a passing check, one passing inline test, the exact twenty-line run transcript, and an empty audit. Replay all eight mutations described in the artifact’s MUTATIONS.md. For each letter X, reproduce exact bytes without editing the accepted source by running

patch -s -o /tmp/ch126-X.kp corpus.kp < mutants/X.patch

and require the digest printed in subappendix E.5. Each resulting file must still check, must fail the exact stdout test, and must retain an empty audit. The accepted corpus.kp remains unchanged; rerun all four accepted commands after the eight replays.

Mathematical boundary. The runner checks finite instances of definition 126.3 and the constructor/closure representation invariant. Its append and stream outputs illustrate theorem 126.14, theorem 126.19; they do not prove either theorem or typed-target preservation. The evaluator’s substitution routine has open lambda and multi-binder case probes, but those finite tests are not evidence for a general open-target substitution theorem.