Specialization, staging, and dependent generated code

Scheme0 is the first-order, pure, call-by-value language of definition 127.1. The separate numeric projection definition 127.2 distinguishes a finite static environment. The online specializer’s conditional correctness equation is theorem 127.4; it asserts equality of results only when specialization and the indicated evaluations terminate. The size-controlled variant combines a finite memo table, a fuel counter, and the printed residualization transition. Its deterministic proof search terminates with either a derivation or a static failure; every returned derivation preserves the specialization equation by theorem 127.9. It is not a general termination theorem for source programs. The offline binding-time system has the exact static/dynamic rules of the chapter, with consistency and specialization soundness in lemma 127.13, theorem 127.15. A returned offline residual program is the finite, reachability-closed graph of definition 127.12, not merely the expression returned by one offline derivation. The pinned self-application witness proposition 127.17 combines the source recipe and concrete Scheme0 listing with recorded terminating executions of the annotated power program and the annotated specializer. It establishes structural fixed points for the power generator and cogen; it neither executes the annotated interpreter self-application nor transfers the local completed-graph theorem to the historical implementation. The three Futamura equations theorem 127.18 are conditional on the three named specializations terminating and satisfying the displayed historical mix equation; the pinned power witness discharges neither interpreter premise. The function-splitting transformation is locally justified by proposition 127.16: an explicit finite Scheme0 copying and call-site map collapses to the source program, simultaneous induction on finite evaluation derivations preserves every call, and the checked static copy specializes exponent four by the displayed offline rules. Chapter 17’s typed $F_{\omega }$ self-representation and chapter 25’s abstract interpretation provide conceptual boundaries, not discharged premises. The Agda companion is a proof-carrying online specializer for arithmetic and dynamic zero tests; it performs static folding and proves its finite mix equation but has no calls, memo table, fuel, or self-application. The Kappa companion computes a structured retained-call closure and proves no self-application theorem. At fuel zero, its residual program includes the call-reachable closure of every retained source function; completed memo equations alone are not sufficient.

SC-CBV has the exact call-by-value configurations of definition 128.1, together with the source’s complete R1–R20 driving ledger, splitting rules, folding relation, homeomorphic-embedding whistle, and most-specific generalization operation. The exact imported result has residual term $\rho ({\mathsf{D}}_{R,G,\rho }(e))$, including the residual-name closing operation $\rho$. The local ${\mathsf{drive}}_0$ projection covers only beta, known-case, and open-case nodes; theorem 128.2 is correspondingly local. The local theorem ledger contains the folding equation lemma 128.3, the well-quasi-order whistle property theorem 128.4, and the generalization witnesses lemma 128.5. The Kappa corpus executes the ordered R1–R20/A1–A4c rule-selection ledger, but does not recursively execute or certify that transformer. The imported total-correctness theorem theorem 128.14 applies only to the source’s finite-signature, pure SC-CBV algorithm with its exact driving, split, generalization, and memoization disciplines; it supplies termination, bidirectional may-termination, and the strong-improvement result of definition 128.6. It does not apply after deleting the whistle, changing call-by-value driving, or generalizing without the source invariant. The Agda file declares the embedding constructors and proves only reflexivity, numeral collapse, and one finite witness. The Kappa visualizer recursively checks embedding, exact local driving edges, a residual case, the full rule-selection ledger, and a finite fusion oracle; it is not a proof of the imported transformer. The local lemma 128.10 records the rule-by-rule strong-improvement step for every R1–R20/A1–A4c clause under recursive hypotheses indexed by their actual $(R_j,G_j,{\rho }_j)$ states. Its A4b case uses the extended allocation map ${\rho }^{\prime }$, prints and instantiates source Lemma A.1 with the empty value substitution and the exact global-unfold contraction, applies the source allocation bridge, and uses the local recursive-improvement theorem before returning to outer $\rho$; proposition 128.16 checks the corresponding free-variable invariant at each of those clauses. The displayed map–append equation is the residual of one finite process graph, not a general fusion theorem.

$\mathsf{Tstage}$ is the pure simply typed dual-context calculus printed in the chapter: ordinary variables inhabit $\mathrm{\Gamma }$, persistent variables inhabit $\mathrm{\Delta }$, and box introduction checks under an empty ordinary context. It has box/let-box and no quotation, escape, or CSP rule. Its dual substitution lemma lemma 129.1, local inert-label eliminability and persistence theorem 129.2, and subject reduction plus scope safety theorem 129.3. Davies–Pfenning’s actual two-level Mini-ML uses distinct compile-time and run-time judgments with functions, products, unit, naturals, case, fixed points, and up/down phase rules. The conservative embedding theorem theorem 129.4 proves both typing preservation and reflection; it is not a relabelling of $\mathsf{Tstage}$. Its target is the source’s implicit context-stack Mini-ML judgment with the complete function, fixed-point, product, unit, natural, case, box, and unbox rule families: box pushes an empty component and ${\mathsf{unbox}}_1$ pops one. The separate self-contained arithmetic instance is the commuting proposition proposition 129.7; its specialization lemma lemma 129.6 treats both static and dynamic operator clauses before the commuting consequence is assembled. Tan–Wei’s source-bounded card prints its surface and administrative syntax, both type-and-effect judgments, stage erasure, termination-based contextual observation, the step-indexed pure logical relation, and the world-indexed reference extension. The exact imported fundamental, soundness, one-step, and transitivity interfaces are lemma 129.11; their assembled staging-erasure consequence theorem 129.12 belongs only to that signature. The pure terminal declaration is Instar/TwoLevelRec/SemanticsPreservation/Preservation.lean: semantics_preservation.stepn.rep; the reference terminal declaration is the same suffix under Instar/TwoLevelFinal/. The comparison MetaML card’s persistent-value predicate contains exactly closed immutable base literals and closed location-free code; it has no function or reference clause. The tagless-final card fixes one algebra signature and computes its evaluator, serializer, and partial-evaluation interpretations. The modular optimizing-evaluator card independently composes atom, inline, fold, partially-static, conditional, CSE, and DCE reflection clauses before a default let-insertion clause. Its 67-test Scala artifact is executable evidence for the printed outputs, not a semantics-preservation theorem. The MacoCaml card fixes the paper’s quote, splice, code-generation, macro, import, heap-threading, and compiler-mode judgments; its empty-heap elaboration boundary is theorem 129.10. Tagless-final libraries, LMS, MetaOCaml, MacoCaml, and the bounded tower are comparison cards, not theorem transfers; the Amin–Rompf development retains eleven admitted obligations, so no tower-soundness theorem is imported from it. The pinned MetaOCaml and LMS archives were not executable on the audit host under their exact historical toolchains, and Appendix E records those gaps without turning a checkout into a test. The Kappa checker handles the finite typed fragment, its complete arithmetic binding-time card, and generated-code evaluation. The Agda companion checks both contexts, both substitutions, beta, and box beta.

The published source basis is the pure dependent multistage calculus ${\lambda }^{\mathsf{MD}}$ printed in the chapter, with stage words, term and stage abstraction/application, quotation and escape, dependent products, and the displayed full and staged reductions. The theorem-bearing corrected subsystem is ${\lambda }_{\mathsf{is}}^{\mathsf{MD}}$, not that exact card. Its simultaneous structural theorem lemma 130.3 treats context well-formedness separately and covers all six judgment families: kind formation, type kinding, term typing, kind equivalence, type equivalence, and term equivalence. It supplies weakening/exchange, ordinary substitution, stage substitution, and their commutation up to alpha-equivalence for each judgment family. The theorem-bearing inversion-stable fragment ${\lambda }_{\mathsf{is}}^{\mathsf{MD}}$ deletes only MD-QT-CSP, whose stage-order behavior invalidates code-head inversion; its code-head lemma therefore also states an explicit body-formation premise. Subject reduction is proved locally from substitution and inversion in theorem 130.5. The chapter defines and proves its own simply typed erasure simulation, then combines target normalization with a lexicographic stage-node/quotation-node measure. It proves multistep substitution compatibility for term-only full contexts. Exact syntactic confluence fails at the typed dependent-annotation peak of proposition 130.4. Binder-annotation erasure retains all computational and staging constructors; parallel reduction and a two-way lifting lemma prove confluence and unique full normal forms only modulo that erasure in theorem 130.7, theorem 130.11, corollary 130.12. The published proofs supply comparison points only; no changed-signature theorem or exact-confluence claim is imported. The book classifies constant-headed spines as final forms to repair the published staged-value grammar; adding only a bare constant would leave a function-typed constant application stuck. This local delta adds no full-reduction rule. Full contexts explicitly exclude binder annotations, types, and kinds; this boundary determines the term-only normalization and annotation-erased confluence statements. With code-head and quotation inversion plus unique staged decomposition lemma 130.1, lemma 130.2, theorem 130.15 prove staged progress and type safety corollary 130.16. Effects, recursion, dependent pattern matching, cross-stage persistence beyond the printed pure rule, and arbitrary generated declarations are outside the signature. The Kappa companion checks finite stage/context/type witnesses and evaluates its finite generated-code examples; it does not mechanize normalization or confluence. The Agda file combines a raw dependent index/type layer—including substitution beneath vector indices and dependent codomains—with a separate natural-stage-depth intrinsic term core having length-indexed vectors, explicit persistence, simultaneous substitution, typed beta and quote–escape steps, and preservation by construction. The two layers are not a full mutually intrinsic calculus and prove no theorem about arbitrary stage words, full dependent conversion, confluence, or normalization.