ch:graded-modal-dtt: graded modal dependent type theory

For subject $y$, the subject vector is $(0,0,1)$ and the subject-type vector is $(1,0,0)$. The triangular rows are $()$, $(1)$, and $(1,0)$: $a$ forms the types of both $x$ and $y$. Changing the subject to $x$ changes only the subject-grade vector, now $(0,1,0)$. The subject-type vector and every row of $\mathrm{\Delta }$ remain fixed; inside the changed vector, the $x$ and $y$ coordinates exchange zero and one.

Box introduction at grade two scales the producer demand from $\mathrm{\Delta }$ to $2\mathrm{\Delta }$. Rule G-Box-E adds that boxed-scrutinee vector once; its body binds the unboxed value at grade two but does not rescale the scrutinee. Hence the producer contribution remains $2\mathrm{\Delta }$, not $4\mathrm{\Delta }$. At grade zero the boxed scrutinee contributes $0\mathrm{\Delta }$. This equation is internal to the typing derivation. Without a defined erasure translation and an observational-soundness theorem it says nothing about whether a compiler evaluates or allocates the producer.

Invert box elimination and box introduction. If the body uses the unboxed variable at subject grade $s$ and its result type depends on it at grade $r$, the eliminator contributes $s{\tau }_s$ to its subject vector and $r{\tau }_s$ to its subject-type vector, where ${\tau }_s$ is the producer’s subject vector. Apply graded substitution to the body with the producer as substituend. Its conclusion contains exactly $\hat{\sigma }={\sigma }_1+s{\tau }_s,{\sigma }_2$ and $\hat{\rho }={\rho }_1+r{\tau }_s,{\rho }_2$, together with the discard/choose update of the context triangle. The box beta-equality rule relates the redex to this typed contractum, and equality inversion supplies preservation.

The hypotheses are: the exact ${\mathrm{GrTT}}^{0,1}$ syntax, only ${\mathsf{Type}}_0$ and ${\mathsf{Type}}_1$, no context variable of type ${\mathsf{Type}}_1$, the paper’s grade structure and rules, and beta reduction for functions, tensors, and boxes. Eta normalization concerns a reduction absent from that signature. Full GrTT admits universe stages and contexts excluded by the saturated-set induction. Conversion decidability also needs a decidable one-step relation and the appropriate confluence/completeness argument. Erasure soundness needs an operational erasure map and a relation between source and target observations. None is a consequence of beta strong normalization alone.

For context $A:{\mathsf{Type}}_0,B:{\mathsf{Type}}_0,p:{\mathsf{Pair}}_0(A,{◻}_{0}B)$, take triangular rows $()$, $(0)$, and $(1,1)$. The term uses only the pair, so ${\sigma }_s=(0,0,1)$; its result type is $A$, so ${\sigma }_t=(1,0,0)$. The weak-product zero is the dependency grade of the first component in the second component’s type. The ${◻}_0$ zero instead scales the subject demand of the packaged $B$ value. Thus one zero occupies a dependent-tensor type position and the other a modal subject-use position; neither is the ambient zero in ${\sigma }_t$ for the unused declaration $B$.

Let the unboxed producer have subject vector ${\tau }_s$ and type vector ${\tau }_t$. Box introduction gives the scrutinee subject vector $s{\tau }_s$. If the elimination result classifier depends on the opened value at grade $r$, substitution changes the body vectors to ${\sigma }_1+s{\tau }_s,{\sigma }_2$ and ${\rho }_1+r{\tau }_s,{\rho }_2$; ${\tau }_t$ is already the row forming the removed declaration. For the zero-based column $j$ of that declaration, the context triangle becomes $$\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }\mathrm{\backslash }j+({\mathrm{\Delta }}^{\prime }/j)\ast {\tau }_s.$$ Discard removes the old column for the bound value; choose collects each later use of that value; scaling and addition insert the producer’s dependencies. The box beta contractum has exactly these three components.

With natural grades, addition and multiplication count duplicated demand; for example $2(\alpha +\beta )=2\alpha +2\beta$. With the Boolean lattice, take join as addition and meet as multiplication; distributivity is again the common semiring calculation. “Used exactly twice” is meaningful only in the natural interpretation, while a confidentiality bound is meaningful only in the information-flow interpretation. An order-based approximation rule would require an explicit premise transporting a derivation from grade vector $\sigma$ to a larger vector ${\sigma }^{\prime }$. The frozen GrTT signature has no such rule, so the imported normalization theorem cannot be instantiated with that extension.