Linear and affine term calculus

The core of chapter 18 is a monomorphic, pure, weak call-by-value calculus with atomic types, $1$, tensor, linear implication, additive sums, and a value-restricted exponential. Its two finite-map contexts are unrestricted $\mathrm{\Gamma }$ and exactly-once $\mathrm{\Delta }$; application and tensor split $\mathrm{\Delta }$, while both sum branches receive one common residual. The separate file extension fixes an infinite token set, finite live sets, and the three roots of definition 18.7. The affine, relevant, and unrestricted variants add only the structural deltas of definition 18.23.

Split refinement is lemma 18.2. Unrestricted and linear substitution are lemma 18.10, lemma 18.11; exact pathwise use is theorem 18.14. Pure preservation and progress are theorem 18.17, theorem 18.18. The file theorem theorem 18.20 preserves one placeholder per live token and forces an empty live set at a returned unit. All four regimes satisfy simultaneous and one-variable substitution lemma 36.27, lemma 36.28, identification lemma 36.29, and safety theorem 36.30. The explicit affine leak and relevant duplication traces of proposition 36.31 show why the exact-use and one-owner conclusions do not transfer to those regimes; they are not counterexamples to the strictly linear theorems. Principal reductions and one commuting conversion give only the displayed cut calculations, not full proof-net normalization. There is no recursion, state, borrowing, lifetime, concurrency, categorical semantics, or exact numeric-use judgment in the core calculus. The affine, relevant, and unrestricted regimes do not inherit the one-owner theorem.

Appendix E’s pinned Kappa corpus implements a syntax-directed consume-and-return checker and a fueled evaluator for the displayed object language. It accepts and evaluates swap, a sum with shared residual resources, bang-local copying, and read-close; it rejects linear duplication, linear discard, unequal case residuals, a dropped returned file, and effectful promotion. This is implementation evidence, not a mechanized proof of substitution, preservation, progress, cleanup, cut elimination, or any theorem about Kappa.

This is a separate dependent bidirectional calculus over rig-marked copies of one precontext, borrowing the later dependent-function vocabulary named in the chapter’s prerequisite firewall. Its source symbols are alpha-renamed to $\mathcal{Q},\mathrm{\Theta },\mathrm{\Xi },q,p$ to avoid the structural-regime subscript. Its result types may contemplate zero-priced variables that the run-time term cannot consume. The rigid version has no weakening; its ordered variant adds weakening under extra factorization, additive-splitting, monotonicity, and zero-reflection conditions. Quantity zero is therefore neither absence, discardability, nor proof irrelevance. At exactly this source signature, preservation is Corollary 36, unique erasure existence is Lemma 40 for $q\ne 0$, and a program step is simulated by source computation in Theorem 44 of [McB16]. The erasure theorems assume $q+p=0\Rightarrow q=0=p$, the book’s rendering of the source’s “absence of negation” condition. The ordered variant is the separate development in §12 of the source. None transfers to the core token machine, a graded-coeffect calculus, or dependent QTT without a translation.