ch:quantitative-dependent-types: quantitative dependent type theory

Use the field ${\mathbb{F}}_2$: addition is exclusive-or and multiplication is conjunction. It is a two-element commutative semiring, but $1+1=0$ while neither summand is zero. In the application and pair cases of the zero-needs-nothing induction, a zero conclusion can therefore no longer be inverted to zero premise demands. For $\mathbb{N}$, a sum of naturals is zero only when both summands are zero, and a product is zero only when at least one factor is zero. Thus both positivity and the zero-product property hold.

Rule QTT-App scales the argument context by the binder quantity: $${\mathrm{\Gamma }}_1+3(2\mathrm{\Delta })={\mathrm{\Gamma }}_1+6\mathrm{\Delta }.$$ With binder quantity zero, the original argument premise is unavailable: the side condition requires the argument’s output quantity ${\sigma }^{\prime }$ to be zero exactly when the binder quantity or the application output quantity is zero. Here the application output is one, so $\pi =0$ forces ${\sigma }^{\prime }=0$. Replace $2\mathrm{\Delta }⊢u{:}^{1}A$ by an erased derivation $0{\mathrm{\Delta }}^{\prime }⊢u{:}^{0}A$. Rule QTT-App then gives ${\mathrm{\Gamma }}_1+0(0{\mathrm{\Delta }}^{\prime })={\mathrm{\Gamma }}_1$; an argument advertised at output quantity one cannot be silently discarded by this rule.

Alpha-rename the lambda-bound $y$ away from the free variables of the substituend. If the outer substituted variable has demand $\rho$, the body premise assigns it a demand that splits through the abstraction scalar. The induction hypothesis scales the substituend context by that body demand. Rebuilding QTT-Lam is licensed by $$\rho (\sigma \pi )=(\rho \sigma )\pi ,$$ an instance of associativity and commutativity of semiring multiplication. The alpha-renaming is performed before applying the induction hypothesis so that capture-avoiding substitution commutes with the remaining binder.

In the empty-vector branch, the index declarations have demand zero and the input spine is inspected once to choose the constructor. In the cons branch, write the context as $n{:}^0\mathsf{Nat},m{:}^0\mathsf{Nat},x{:}^{1}A,xs{:}^1\mathsf{Vec}(A,n),ys{:}^1\mathsf{Vec}(A,m)$; the recursive call consumes the positive-demand tail and the constructor consumes the head. Type formation may use $n,m$ arbitrarily while their run-time demand remains zero. Changing $n$ to demand one retains its representation at run time. It does not alter the formation or proof rules for natural-number equality, so it neither proves nor refutes $n+m=m+n$.

For application, split the substituted variable’s demand as ${\rho }_1+\pi {\rho }_2$. The two induction conclusions combine as $$({\mathrm{\Delta }}_1+{\rho }_1\mathrm{\Gamma })+\pi ({\mathrm{\Delta }}_2+{\rho }_2\mathrm{\Gamma })={\mathrm{\Delta }}_1+\pi {\mathrm{\Delta }}_2+({\rho }_1+\pi {\rho }_2)\mathrm{\Gamma },$$ using distributivity and then associativity/commutativity of addition. For tensor elimination, distribute the body’s two bound demands through the scrutinee context, reassociate the three context sums, and use substitution composition in the dependent result. In each rule, check separately that a zero output forces exactly the zero argument/scrutinee quantity required by its printed biconditional; positivity and zero-product are what permit that inversion.

In the zero–one–many algebra, $1+\omega =\omega$. An arbitrary-output substitution derivation at output $\omega$ can therefore present a premise whose variable demand is $\omega$ and try to split it as one use in one branch plus $\omega$ in another. Reconstructing the substitution needs to recover a subderivation at demand $1$ from the premise at demand $\omega$. The calculus has no subusage rule $1\le \omega$ that changes a derivation’s annotation, so the required premise cannot be obtained. Restricting output quantities to $0$ and $1$ removes the ambiguous $\omega$-output branch: zero uses the zero lemma, and one forces the unique resource-sensitive split used by the repaired substitution proof.