Prerequisites. Direct starred prerequisites: Chapter 41. No later core chapter depends on this route.
A context annotation tells how an open term uses each assumption. It does not produce a first-class value that may be stored now and opened later at a specified grade. For example, knowing that a pair projection ignores its second component does not let the pair type itself record that local fact. Repeated projection and substitution must rediscover the usage from the whole derivation.
A graded modality internalizes the demand. The type ◻𝑠𝐴 packages an 𝐴-value for later use at grade 𝑠. Dependency creates a second demand: an assumption may occur in the subject and independently in the subject’s type. Both demands remain visible below.
Fix a semiring (R,+,0,⋅,1). Context addition and scalar multiplication use its operations pointwise. The paper calculus has no grade approximation rule: extending it to preordered semirings is an implementation extension and is outside the normalization theorem imported below.
A context has the form Γ=𝑥1:𝐴1,…,𝑥𝑛:𝐴𝑛. A vector 𝜎∈R𝑛 assigns a grade to each declaration. The context grade vector Δ has, at one-based position 𝑖, a row of length 𝑖−1. That row records how earlier assumptions form 𝐴𝑖. The typing judgment is (Δ∣𝜎𝑠∣𝜎𝑡)⊙Γ⊢𝑡:𝐴. The vector 𝜎𝑠 grades occurrences in the subject𝑡; the vector 𝜎𝑡 grades occurrences in the subject’s type 𝐴. All four vectors and contexts have the lengths forced by Γ.
Universe and variable typing make the three vectors concrete:
Δ⊙Γ⊢
(Δ∣0∣0)⊙Γ⊢𝖳𝗒𝗉𝖾𝑙:𝖳𝗒𝗉𝖾𝗌𝗎𝖼𝑙
G-Type
Δ1,𝜎,Δ2⊙Γ1,𝑥:𝐴,Γ2⊢|Δ1|=|Γ1|
(Δ1,𝜎,Δ2∣0|Δ1|,1,0∣𝜎,0,0)⊙Γ1,𝑥:𝐴,Γ2⊢𝑥:𝐴
G-Var
For 𝑎:𝖳𝗒𝗉𝖾0,𝑥:𝑎,𝑦:𝑎⊢𝑥:𝑎, the subject grades are (0,1,0): only 𝑥 occurs in the term. The subject-type grades are (1,0,0): only 𝑎 occurs in the classifier. The last row of Δ is (1,0), since 𝑎 forms the type of 𝑦 and 𝑥 does not. Collapsing these three vectors into one loses which occurrence belongs to the term, its type, or a later declaration.
This supplies a counterexample to a direct translation into the QTT judgment of definition 99.2. The independent GrTT classifier vector cannot be recovered after subject and classifier demands have been collapsed into one QTT usage vector. Conversely, QTT tensor elimination assigns quantities 𝜎𝜋 and 𝜎 to the two components, whereas G-Let below assigns one common subject grade. Neither rule card is obtained by erasing annotations from the other, and no translation theorem is claimed.
The core terms and types are 𝑡,𝐴,𝐵::=𝑥∣𝖳𝗒𝗉𝖾𝑙∣(𝑥:(𝑠,𝑟)𝐴)→𝐵∣𝜆𝑥.𝑡∣𝑡𝑢∣(𝑥:𝑟𝐴)⊗𝐵∣(𝑡,𝑢)∣𝗅𝖾𝗍(𝑥,𝑦)=𝑡𝗂𝗇𝑢∣◻𝑠𝐴∣𝖻𝗈𝗑𝑡∣𝗅𝖾𝗍𝖻𝗈𝗑𝑥=𝑡𝗂𝗇𝑢. In a function binder, 𝑠 is the use of 𝑥 in the function body and 𝑟 its use in 𝐵. A tensor binder needs only 𝑟, since 𝑥 is bound in the second component’s type rather than in a stored body.
The frozen paper core has its universe hierarchy and the displayed formers. The Gerty prototype adds a singleton unit type, preordered-semiring support, and other conveniences. Neither a unit nor a natural-number type former is silently added to the source signature used for preservation and normalization.
★☆☆ For 𝑎:𝖳𝗒𝗉𝖾0,𝑥:𝑎,𝑦:𝑎⊢𝑦:𝑎, compute the subject and subject-type vectors and the three rows of Δ. Change the subject to 𝑥 and identify exactly one vector component that changes.
The first premise exposes the grades forming the codomain. The argument’s subject vector 𝜎4 is scaled once for computational use and once for its substitution into that codomain; its own type vector 𝜎1 is the domain-formation vector already accounted for by the other premises.
For 𝜆𝑥.𝜆𝑦.𝑥, the inner binder has subject grade zero and type grade zero. Applying the function to any second argument therefore scales that argument’s subject and subject-type vectors by zero. This is a derivable statement about the term, not an operational erasure theorem.
The common grade 𝑠 on the two body binders is required because an arbitrary semiring sum cannot be inverted to recover separate component uses. Computation contracts 𝗅𝖾𝗍(𝑥,𝑦)=(𝑡,𝑢)𝗂𝗇𝑣⟶𝛽𝑣[𝑡/𝑥,𝑢/𝑦]. For closed 𝐴,𝐵, choosing 𝑟=𝑟′=0 and 𝑠=1 derives 𝗅𝖾𝗍(𝑥,𝑦)=𝑝𝗂𝗇(𝑥,𝑦):(𝑥:0𝐴)⊗𝐵: the body vector assigns grade one to both binders, and G-Let adds the scrutinee vector once. Replacing 𝑝 by a neutral variable leaves this eliminator stuck. The selected core contains the beta root above and no tensor eta rule.
Suppose the grade semiring is quantitative in the source’s sense: grade zero enforces that a subject is unused. Under this semantic hypothesis, the weak product𝐴×𝐵 is the special case (𝑥:0𝐴)⊗𝐵 with 𝑥∉FV(𝐵). We do not make this product identification for an arbitrary semiring. The calculus retains only G-Let; a first-projection term may still be underivable because that rule assigns one common inspection grade to both components. The graded modality below supplies the local zero-use fact needed for the projection example.
The body uses the unboxed 𝑥 at subject grade 𝑠; the result type uses the scrutinee at grade 𝑟. These contributions occupy different vectors. The source prints the body’s classifier as 𝐵[𝑥/𝑧]. Since 𝑧:◻𝑠𝐴 and 𝑥:𝐴, the displayed 𝐵[𝖻𝗈𝗑𝑥/𝑧] is the type-correct reading of that source rule. Computation is 𝗅𝖾𝗍𝖻𝗈𝗑𝑥=𝖻𝗈𝗑𝑡𝗂𝗇𝑢⟶𝛽𝑢[𝑡/𝑥]. For 𝑠=1, 𝑟=0, and closed 𝐴, the premises derive 𝑝:◻1𝐴⊢𝗅𝖾𝗍𝖻𝗈𝗑𝑥=𝑝𝗂𝗇𝑥:𝐴 with one subject use and zero subject-type use. A neutral 𝑝 makes the eliminator stuck. The selected core includes this beta root and no box eta equation.
With the natural-number semiring, ◻2𝐴 packages an 𝐴-value for two uses. A lattice semiring can instead read grades as security labels. These instantiations share semiring equations, but their intended observations differ; the calculus adds no implicit order-based approximation.
★★☆ Assume 2Δ⊢𝖻𝗈𝗑𝑡:◻2𝐴 is obtained by G-Box-I. Calculate the demand on Δ when one elimination uses the unboxed value twice. Repeat at grade zero and explain why the result is a typing calculation rather than proof that a compiler deletes 𝑡.
Substitution must update the triangular context vector as well as the two judgment vectors. If 𝑥 occurs in later declaration types, removing its column without redistributing the substituend’s dependencies loses precisely the information Δ was introduced to retain.
For a triangular context vector Δ′ and a zero-based column index 𝑗, Δ′\𝑗 removes column 𝑗 from each later row, while Δ′/𝑗 collects the removed entries. Thus a declaration at one-based position 𝑗+1 is removed at column index 𝑗. If 𝜎 is the grade vector used to construct a substituend, then Δ′\𝑗+(Δ′/𝑗)∗𝜎 removes the old dependency on 𝑥 and adds the dependencies of the substituend, each scaled by the former use of 𝑥. Short rows are padded on the right with zero before addition.
For a later type that uses 𝑥 twice, substituting a term with subject vector (0,1) replaces the removed entry 2 by 2(0,1)=(0,2). Merely deleting the entry would falsely declare the later type independent of the substituted term.
Suppose (Δ∣𝜏𝑠∣𝜏𝑡)⊙Γ1⊢𝑡:𝐴 and (Δ,𝜏𝑡,Δ′∣𝜎1,𝑠,𝜎2∣𝜌1,𝑟,𝜌2)⊙Γ1,𝑥:𝐴,Γ2⊢𝑢:𝐵. Assume the prefix vectors have length |Γ1|. Define 𝑗=|Γ1|=|Δ|, the zero-based column occupied by 𝑥 in every later row, and ̂Δ=Δ,Δ′\𝑗+(Δ′/𝑗)∗𝜏𝑠,̂𝜎=𝜎1+𝑠𝜏𝑠,𝜎2,̂𝜌=𝜌1+𝑟𝜏𝑠,𝜌2. Then (̂Δ∣̂𝜎∣̂𝜌)⊙Γ1,Γ2[𝑡/𝑥]⊢𝑢[𝑡/𝑥]:𝐵[𝑡/𝑥].
Proof. Induct on the typing derivation of 𝑢. The selected-variable case returns the premise derivation for 𝑡; its subject and subject-type vectors are scaled by the grades at the removed position. Another variable uses the corresponding row after discard, and choose inserts the dependencies of 𝑡 into its declared type.
In G-App, apply the induction hypotheses to the function and argument. The subject calculation uses distributivity: (𝜎1+𝑠𝜏𝑠)+𝑞(𝜎2+𝑠′𝜏𝑠)=𝜎1+𝑞𝜎2+(𝑠+𝑞𝑠′)𝜏𝑠. The subject-type vector has the same equation with its independent binder grade. Substitution composition aligns 𝐵[𝑣/𝑦][𝑡/𝑥] with 𝐵[𝑡/𝑥][𝑣[𝑡/𝑥]/𝑦]. The lambda case extends the triangular vector by one row and uses alpha-renaming. Tensor introduction and elimination use the same two vector equations, with the dependent-result substitution visible in the latter. Box introduction uses associativity of scalar multiplication; box elimination additionally uses the discard/choose equation for its dependent result type. Universes are closed and variables cover the base cases. Thus every rule reconstructs the displayed conclusion. ◻
Proof of Lemma 100.9 — Reduction gives typed equality
Proof. For function beta, use theorem 100.8 to type the contractum and apply the function beta-equality rule. Tensor and box beta use the same substitution theorem, once for each bound component. A compatible reduction uses the corresponding equality congruence. These are all beta roots of definition 100.3. ◻
Proof. By lemma 100.9, the two terms are equal at 𝐴 under the original three grade components. Equality inversion returns a typing judgment for each endpoint, hence the required judgment for 𝑡′. ◻
★★☆ Prove the root box-beta case of theorem 100.10. Display the two scaled vectors in the elimination premise and identify their occurrences in the conclusion of theorem 100.8.
The fragment GrTT0,1 has exactly the two universe levels 𝖳𝗒𝗉𝖾0 and 𝖳𝗒𝗉𝖾1, and its contexts contain no variables whose type is 𝖳𝗒𝗉𝖾1. Its reduction relation is beta reduction for functions, tensors, and boxes. Eta equality is not part of this reduction relation.
The proof separates syntax into four disjoint stages. With all displayed judgments restricted to GrTT0,1, define 𝖪𝗂𝗇𝖽={𝐴∣∃Δ,𝜎,Γ.(Δ∣𝜎∣0)⊙Γ⊢𝐴:𝖳𝗒𝗉𝖾1},𝖳𝗒𝗉𝖾={𝐴∣∃Δ,𝜎,Γ.(Δ∣𝜎∣0)⊙Γ⊢𝐴:𝖳𝗒𝗉𝖾0},𝖢𝗈𝗇={𝑡∣∃Δ,𝜎𝑠,𝜎𝑡,Γ,𝐴.(Δ∣𝜎𝑠∣𝜎𝑡)⊙Γ⊢𝑡:𝐴,(Δ∣𝜎𝑡∣0)⊙Γ⊢𝐴:𝖳𝗒𝗉𝖾1},𝖳𝖾𝗋𝗆={𝑡∣∃Δ,𝜎𝑠,𝜎𝑡,Γ,𝐴.(Δ∣𝜎𝑠∣𝜎𝑡)⊙Γ⊢𝑡:𝐴,(Δ∣𝜎𝑡∣0)⊙Γ⊢𝐴:𝖳𝗒𝗉𝖾0}. These stage definitions are source Definition C.1, and the imported classification result is source Lemma C.2. It gives 𝖪𝗂𝗇𝖽∩𝖳𝗒𝗉𝖾=∅ and 𝖢𝗈𝗇∩𝖳𝖾𝗋𝗆=∅.
Let 𝖲𝖭 be the set of terms admitting no infinite beta-reduction sequence. The base set 𝖡 is the least set satisfying these eight clauses: variables, 𝖳𝗒𝗉𝖾0, and 𝖳𝗒𝗉𝖾1 lie in 𝖡; if 𝑡1∈𝖡 and 𝑡2∈𝖲𝖭, then 𝑡1𝑡2∈𝖡; if 𝑡2∈𝖡 and 𝑡1∈𝖲𝖭, each tensor let and box let with scrutinee 𝑡1 and body 𝑡2 lies in 𝖡; if their constituents are strongly normalizing, dependent function types, dependent tensor types, and box types lie in 𝖡.
A term’s key redex is the term itself when it is a beta redex; it is otherwise the unique key redex of the operator in an application or of the scrutinee in a tensor let or box let. Write 𝗋𝖾𝖽𝑘(𝑡) for its contraction. A set 𝑋 is saturated when 𝑋⊆𝖲𝖭,𝖡⊆𝑋,𝗋𝖾𝖽𝑘(𝑡)∈𝑋∧𝑡∈𝖲𝖭⟹𝑡∈𝑋. The collection 𝖲𝖠𝖳 of saturated sets interprets 𝖳𝗒𝗉𝖾0 at the kind stage; 𝖳𝗒𝗉𝖾1 has type interpretation 𝖲𝖭, while [[𝖳𝗒𝗉𝖾0]]𝜀 is the constant family 𝑋∈𝖲𝖠𝖳↦𝖲𝖭. Dependent functions use the corresponding candidate function space and tensors use Cartesian products. The interpretation erases box constructors because grades do not occur in beta reduction. This definition reproduces source Definitions C.3, C.4, and C.6, source Lemma C.7, and the universe clauses of Definitions C.8 and C.10 [MIO21].
The erasure in this proof is a device for proving membership in 𝖲𝖭. It is not a compiler semantics and does not establish that erasing boxes preserves observations, costs, or run-time access counts.
The proof mechanism is a saturated-set interpretation. Its valuation judgments must be stated before the theorem. A type valuation starts empty. For a declaration 𝑥:𝐴 with 𝐴:𝖳𝗒𝗉𝖾1, it extends 𝜀 by 𝑥↦𝑋 for an arbitrary 𝑋∈𝖪[[𝐴]]; for 𝐴:𝖳𝗒𝗉𝖾0, it extends the context without changing 𝜀. A valid term valuation starts empty. At a 𝖳𝗒𝗉𝖾1-classified declaration it extends 𝜌 by 𝑥↦𝑡 with 𝑡∈[[𝐴]]𝜀(𝜀(𝑥)); at a 𝖳𝗒𝗉𝖾0-classified declaration it instead requires 𝑡∈[[𝐴]]𝜀. Write these judgments as Δ⊙Γ⊧𝜀 and Δ⊙Γ⊧𝜀𝜌, respectively. The term ((𝑡))𝜌 is 𝜌(𝑡) with tensor lets translated to substitutions and graded boxes erased. These are inductive judgments on the same triangular context Δ, not an informal class of closing maps. The remaining kind-, type-, and term-interpretation clauses are imported at the signatures below, where 𝖱𝖺𝗐𝖳𝖾𝗋𝗆 is the set of raw terms generated by definition 100.3: 𝖪[[−]]:𝖪𝗂𝗇𝖽→𝖲𝖾𝗍,[[−]]𝜀:𝖪𝗂𝗇𝖽∪𝖳𝗒𝗉𝖾∪𝖢𝗈𝗇→𝖲𝖾𝗍,((−))𝜌:𝖪𝗂𝗇𝖽∪𝖳𝗒𝗉𝖾∪𝖢𝗈𝗇∪𝖳𝖾𝗋𝗆→𝖱𝖺𝗐𝖳𝖾𝗋𝗆. from Definitions C.8–C.12 [MIO21]. Their supplied consequence is Lemma C.16: interpreted constructors inhabit the corresponding kind interpretation and interpreted types yield saturated candidates.
The source semantic judgment (Δ∣𝜎𝑠∣𝜎𝑡)⊙Γ⊧𝑡:𝐴 has two clauses. If 𝐴:𝖳𝗒𝗉𝖾1, every valid (𝜀,𝜌) satisfies ((𝑡))𝜌∈[[𝐴]]𝜀([[𝑡]]𝜀). If 𝐴:𝖳𝗒𝗉𝖾0, every such valuation satisfies ((𝑡))𝜌∈[[𝐴]]𝜀. This is Definition C.13 of the source at its exact restricted signature; the load-bearing induction occupies its Theorem C.17.
Proof of Theorem 100.13 — Imported semantic typing
Proof. This is Theorem 3 of Moon–Eades–Orchard, with its complete induction in their Appendix C, Theorem C.17 [MIO21]. Their Δ, subject vector, and subject-type vector are exactly those of definition 100.2; their function and tensor cases are the rules of definition 100.4, definition 100.5. Their box cases are the rules of definition 100.6 under the type-correct reading of G-Box-E recorded after that rule. The import is restricted exactly as in definition 100.11. In particular, it imports neither arbitrary universe levels nor variables of type 𝖳𝗒𝗉𝖾1. Those identifications instantiate every premise and give the stated conclusion. ◻
Proof of Corollary 100.14 — Beta strong normalization
Proof. This is the source’s Strong Normalization Corollary immediately after Theorem 3, imported with its open-term conclusion [MIO21]. The source defines canonical elements of 𝖪[[𝐴]] and a valid term valuation, then invokes semantic typing. Its corollary asserts 𝑡∈𝖲𝖭 for the source term itself even though the displayed semantic judgment constrains ((𝑡))𝜌; that transfer is inherited from the source’s corollary and is not reproved here. ◻
The two-universe restriction and exclusion of 𝖳𝗒𝗉𝖾1-typed variables are substantive hypotheses of this proof. Removing them invalidates the well-founded stage analysis; no stronger theorem is claimed here. Strong normalization alone is neither decidability of conversion without a decidable one-step system and confluence proof, nor logical consistency without the remaining canonical-forms argument.
★★☆ List the exact hypotheses of corollary 100.14. For each of the following conclusions—eta normalization, full-GrTT normalization, conversion decidability, and erasure soundness—name a missing premise or a signature mismatch that prevents it from following from the corollary.
Fix a quantitative grade semiring. Let 𝖯𝖺𝗂𝗋0(𝐴,𝐵) abbreviate the weak product (𝑥:0𝐴)⊗𝐵, and package the second component at grade zero: 𝖿𝗂𝗋𝗌𝗍:𝖯𝖺𝗂𝗋0(𝐴,◻0𝐵)→𝐴. The program is 𝜆𝑝.𝗅𝖾𝗍(𝑥,𝑦)=𝑝𝗂𝗇𝗅𝖾𝗍𝖻𝗈𝗑𝑧=𝑦𝗂𝗇𝑥. Rule G-Let binds 𝑥:𝐴 and 𝑦:◻0𝐵 at the same inspection grade, namely one. The zero is introduced earlier: G-Box-I gives the packaged second component subject vector 0𝛽=0. Thus an input pair constructed from component-demand vectors 𝛼 and 𝛽 has vector 𝛼+0𝛽, and the common grade of G-Let yields 1(𝛼+0𝛽)=𝛼. Without ◻0, the strong tensor eliminator assigns the same inspection grade to both components and cannot derive this projection for every semiring. The modality is therefore doing type-theoretic work: it packages the local zero-use fact.
The calculation does not promise that a concrete run time skips construction of the second component. Such a result needs an operational erasure map and an observational-equivalence proof. The saturated-set proof of corollary 100.14 erases modalities for a different purpose.
★★☆ Give all three grade components Δ,𝜎𝑠,𝜎𝑡 for 𝖿𝗂𝗋𝗌𝗍 in a context containing 𝐴:𝖳𝗒𝗉𝖾0, 𝐵:𝖳𝗒𝗉𝖾0, and the input pair. Identify the zero generated by the weak product and the zero generated by ◻0; they occupy different positions.
★★☆ Reconstruct graded substitution for a box elimination whose result type depends on the scrutinee at grade 𝑟. Compute the subject and subject-type vectors separately, then compute the discard/choose update to the triangular context vector.
★★★ Instantiate the rule card once with natural-number grades and once with the Boolean information-flow lattice semiring. Give one semiring calculation valid in both instances and one observational reading meaningful in only one instance. Identify the additional approximation rule that would be required to use the lattice order, and explain why the imported normalization theorem does not cover that extension.
★★★Practical project.grtt-modal-grade-calculator Implement in Agda or Kappa subject, subject-type, and triangular context grade vectors over natural numbers. Implement application scaling and the discard/choose substitution operation while maintaining the invariant that one-based row 𝑖 of the triangular vector has length 𝑖−1. On the named cases modal-first, substitute-twice, and bad-row-length, print respectively subject demand (1,0), substituted dependency (0,2), and bad-row-length rejected: shape. Store the subject and subject-type vectors in one judgment record. A mutation that copies the subject vector into the subject-type field must fail the named separation oracle. The program checks finite grade equations; it does not prove preservation or strong normalization.
Sources. The three-vector judgment, graded function and tensor binders, modality, substitution operations, and preservation proof follow Moon, Eades, and Orchard [MIO21]. The exact strong-normalization boundary is stated before their proof and its conclusion is Corollary 1 on p. 21 of the pinned paper: beta reduction in the two-universe GrTT0,1 fragment with no variables of 𝖳𝗒𝗉𝖾1. Gerty v0.1.0 supplies implementation evidence only; its unit, natural-number, implicit-grade, and solver features are not silently added to that theorem’s signature.