Rewriting and resource-sensitive dependency

The local algebraic fragment has constant-headed, lambda-free, left-linear, algebraic rules whose free variables are exactly their telescope and whose two sides have one type. Raw reduction is independent of typing. Subject reduction additionally assumes product compatibility and permanent well-typedness in well-formed extensions. The conditional chain from confluence to product compatibility, subject reduction, and uniqueness of types uses permanent well-typedness; decidable conversion additionally needs effective one-step reduction and termination. Saillard’s stronger endpoint concerns higher-order rewriting modulo beta, not ordinary confluence of the union of beta and signature steps. The adequacy theorem is only for beta-eta-long normal terms in the displayed implicational encoding.

The calculus has parameter contexts, state-bearing terms, usage $\{0,1,\omega \}$, shape-indexed dependent linear functions and tensors, call-by-value evaluation, and common-value conversion of parameter indices. Its substitution theorem has three separate clauses: parameter into types, parameter into terms, and values into terms with only their shapes entering classifiers. The proved preservation and soundness results are restricted to the ${\mathrm{LD}}^1$ fragment in which every evaluated computational abstraction has binder index one. Semantic soundness ranges only over the exact Fu–Kishida–Selinger state–parameter fibration signature: pullback fibration over an LCCC, monoidal closed total category, monoidal preservation, cartesian-arrow tensor closure, fibered tensor–hom adjunction, and $p⊣\mathrm{♭}$. No normalization, canonicity, completeness, or compiler-erasure theorem is claimed, and no operational theorem for the $k=0,\omega$ application cases is asserted.

QTT contexts are semiring vectors with a fixed declaration spine. The substitution and zero-demand proofs require a commutative semiring satisfying positivity and the zero-product property, together with the printed zero-output biconditionals. Substitution multiplies the argument context by the binder demand. Beta preservation is limited to the displayed function and tensor fragment. Quantity zero is absence of run-time demand, not proof irrelevance or term equality; Idris 2 supplies implementation observations, not the metatheorem.

GrTT keeps a triangular declaration-type grade vector, a subject vector, and a subject-type vector. Its local substitution and preservation results use the displayed plain semiring, dependent function/tensor, and graded-box rules. The imported semantic-typing theorem and strong-normalization corollary are restricted to ${\mathrm{GrTT}}^{0,1}$: exactly two universes, no context variable of type ${\mathsf{Type}}_1$, and beta reduction only, without eta. They do not imply full-GrTT normalization, conversion decidability, logical consistency, erasure soundness, or run-time cost bounds. The Kappa corpus checks eight finite vector and triangular-traversal equations only.