pith. sign in

arxiv: 2605.17112 · v1 · pith:ZIA3DKC7new · submitted 2026-05-16 · 💻 cs.LO

A unification of graded and substructural logics

Peter Hanukaev , Harley Eades III This is my paper

Pith reviewed 2026-05-20 14:44 UTC · model grok-4.3

classification 💻 cs.LO
keywords graded typessubstructural logiclinear logicresource sensitivitycategorical semanticstype systemsmodal typessemiring grades
0
0 comments X

The pith

GRASS unifies graded and substructural logics into one type system that tracks variable usage with arbitrary algebraic grades while supporting restrictions on weakening and contraction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents GRASS as a type system that merges substructural logics, which restrict how variables can be duplicated or discarded, with graded systems that instead count variable uses according to some algebraic structure. This combination gives programmers fine-grained control so that different variables in the same program can obey different resource rules. The authors construct categorical semantics for GRASS and show that these semantics contain the semantics of several prior systems as special cases. A reader would care because resource-sensitive computations appear in areas from memory management to quantum computing, and a single framework could reduce the need to choose between competing styles of type discipline.

Core claim

GRASS is a type system incorporating mechanisms from both graded and substructural logics, allowing maximally flexible control over variable usage. It permits grades drawn from an arbitrary collection of grade algebras to coexist inside the same system, so different variables can be governed by different resource notions. On the level of categorical semantics, GRASS subsumes established systems such as LNL, Adjoint Logic, and mGL.

What carries the argument

The GRASS type system, which embeds both quantitative grading from semirings or algebras and substructural restrictions on contraction and weakening within a single syntax and its associated categorical semantics.

If this is right

  • Different variables within one program can be subject to distinct resource algebras without requiring separate languages or embeddings.
  • Categorical models of GRASS automatically provide models for LNL, Adjoint Logic, and mGL as instances.
  • The system supports resource tracking that is both quantitative and structural in the same derivation.
  • Arbitrary collections of grade algebras can be mixed inside one context without forcing a single global algebra.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Language designers could adopt GRASS as a common core and then instantiate only the grade algebras needed for a particular domain such as memory, energy, or information flow.
  • Type checkers built on GRASS might allow incremental addition of new resource disciplines by extending the collection of algebras rather than rewriting the core rules.
  • The categorical semantics suggest that future work could lift existing categorical constructions from the subsumed systems directly into the GRASS setting.

Load-bearing premise

A single coherent type system and its semantics can embed the core mechanisms of both graded and substructural approaches while preserving their individual properties and avoiding inconsistencies.

What would settle it

An explicit derivation or term that is valid in a standard graded system or a standard substructural system but cannot be typed in GRASS, or a semantic embedding of LNL, Adjoint Logic, or mGL that fails to preserve the expected morphisms.

Figures

Figures reproduced from arXiv: 2605.17112 by Harley Eades III, Peter Hanukaev.

Figure 1
Figure 1. Figure 1: Grass rules for well-formed types Var A ∈ Type(m) 1 | m ⊙ x : A ⊢m x : A Weak Weak(m) n ≤ m B ∈ Type(m) ρ | M ⊙ Γ ⊢n e : A ρ, 0 | M, m ⊙ Γ, x : B ⊢n e : A Cont q1, q2 ∈ Cont(m) ρ, q1, q2 | M, m, m ⊙ Γ, x : A, y : A ⊢n e : B ρ, q1 + q2 | M, m ⊙ Γ, z : A ⊢n [z/x , z/y]e : B Sub ρ ≤ σ ρ | M ⊙ Γ ⊢m e : A σ | M ⊙ Γ ⊢m e : A Unit.i ∅ | ∅ ⊙ ∅ ⊢m ⋆m : Im Unit.e σ | N ⊙ ∆ ⊢m e : Im ρ | M ⊙ Γ ⊢m t : A q ∈ Rm ρ, qσ |… view at source ↗
Figure 2
Figure 2. Figure 2: Grass typing rules Definition 3.5 Typing judgments in Grass have the form ρ | M ⊙ Γ ⊢m t : T. The roles of Γ, t, and T are as before. There are two new components in the judgment: The annotation m on the turnstile indicates that T ∈ Type(m), and we say that this typing judgment is made at mode m. The other new component is M, which is a list of modes, also called a mode vector. If ρ = (r1, . . . , rk ) and… view at source ↗
Figure 3
Figure 3. Figure 3: Grass βη-conversions linear terms may depend on non-linear variables, but not vice-versa, and was also observed by Pruiksma et al. [27], where it is called independence. The typing rules of Grass are set up to ensure that independence holds in all derivable judgments. In Grass, independence also ensures that all scalar multiplications occuring in the typing rules are well-defined (cf. Definition 3.3). We d… view at source ↗
Figure 4
Figure 4. Figure 4: Graded comonad coherence conditions Note that the requirement that this functor is colax monoidal already includes the above diagram. We include that diagram explicitly, since we cannot require that this functor be colax monoidal in the absence of the morphism w. These structures are related by the diagrams of [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Coherence laws on morphisms of exponential actions. Unlabelled arrows are the lax monoidal structure on [PITH_FULL_IMAGE:figures/full_fig_p011_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Coherence laws on µ. Lemma 4.10 Let (G, F, ℓ) and (G′ , F′ , ℓ′ ) be morphisms of actions over φ, and α: G → G′ a 2-cell in ExpAct. Then α induces a natural isomorphism β : F ′ → F which respects µ in the obvious way: F ′ (φ(q) ⊙ A) q ⊙ F ′ (A) F(φ(q) ⊙ A) q ⊙ F(A) µ β q⊙β µ ′ Definition 4.11 Recall that Grass is parametrized by a functor d: S → Mode where S is some preordered set. We have a projection fun… view at source ↗
Figure 7
Figure 7. Figure 7: Summary of named natural transformations in the categorical model for [PITH_FULL_IMAGE:figures/full_fig_p013_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Grass interpretation into a categorical model gave an account of the categorical semantics of our logic based on graded comonads. Our logic consists of multiple graded systems connected by morphisms of modes, and this design is mirrored in the categorical semantics. We introduced a novel notion of morphisms of graded comonads, and showed how it connects to the existing literature. We saw that categorical m… view at source ↗
read the original abstract

Type systems which account for resource sensitive computations can generally be split into two styles: First, substructural logics such as Linear Logic which seek to restrict weakening and contraction and reintroduce them in a controlled manner; And second, graded systems which allow weakening and contraction by default, but track the use of variables quantitatively in some algebraic structure -- usually a semiring. We present GRASS (Graded and substructural), a type system which incorporates mechanisms from both of these approaches, thus allowing maximally flexible control over variable usage. Furthermore, GRASS allows grades from an arbitrary collection of grade algebras to coexist in the same system, thus allowing different variables to be controlled with respect to different notions of resource within the same program. We develop the categorical semantics of \gyaru{}, and find that, on the level of categorical semantics, it subsumes multiple established systems such as LNL, Adjoint Logic, and mGL.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper introduces GRASS, a type system that unifies graded and substructural logics by parameterizing contexts with multiple independent grade algebras, allowing arbitrary collections of grades to coexist while recovering weakening/contraction control from both styles. It defines combined resource-usage rules and develops functorial categorical semantics, with explicit embeddings showing that GRASS subsumes LNL, Adjoint Logic, and mGL as special cases.

Significance. If the embeddings and semantic constructions hold, the work supplies a single, parameterizable framework that recovers several established resource-sensitive systems without loss of expressiveness. The explicit functorial semantics and recovery of prior systems as instances constitute a clear technical contribution to the unification of graded and substructural type theories.

major comments (1)
  1. [§4.3] §4.3, Definition 4.7: the combined grade algebra construction for multiple independent grades is stated to preserve the original substructural restrictions, but the proof sketch does not explicitly verify that the induced weakening/contraction rules coincide exactly with those of mGL when all but one grade algebra are taken to be the trivial semiring; this step is load-bearing for the subsumption claim.
minor comments (3)
  1. [§3.2] Notation for the multi-grade context judgment is introduced in §3.2 but the precise arity of the grade tuple is not restated in the typing rules of Figure 2, making it easy to misread how many independent grades are active in a given derivation.
  2. [§5] The categorical semantics section (§5) uses the same symbol for the functor interpreting a GRASS judgment and the functor interpreting an embedded LNL judgment; a distinct notation or explicit coercion would improve readability.
  3. [Theorem 5.4] Theorem 5.4 states that the embedding of Adjoint Logic is full and faithful, yet the proof only sketches the faithfulness direction; supplying the missing direction or a reference to a standard lemma would strengthen the result.

Simulated Author's Rebuttal

1 responses · 0 unresolved

Thank you for the positive review and the recommendation for minor revision. We address the single major comment below and have made the corresponding changes to the manuscript.

read point-by-point responses

  1. Referee: [§4.3] §4.3, Definition 4.7: the combined grade algebra construction for multiple independent grades is stated to preserve the original substructural restrictions, but the proof sketch does not explicitly verify that the induced weakening/contraction rules coincide exactly with those of mGL when all but one grade algebra are taken to be the trivial semiring; this step is load-bearing for the subsumption claim.

    Authors: We appreciate the referee highlighting this gap in the proof sketch. The comment is correct that an explicit verification is needed for the subsumption of mGL. In the revised version, we expand the proof in §4.3 to explicitly show that setting all but one grade algebra to the trivial semiring (where the only grade is 0 with no weakening or contraction beyond the base) induces exactly the weakening and contraction rules of mGL. This is done by demonstrating that the combined operations on grades reduce to the single algebra's rules, preserving the substructural restrictions precisely. We believe this strengthens the subsumption claim. revision: yes

Circularity Check

0 steps flagged

No significant circularity: new parameterized construction with explicit embeddings

full rationale

The paper defines GRASS by directly parameterizing typing contexts with an arbitrary collection of independent grade algebras and introducing combined usage rules that recover graded and substructural systems as special cases. The categorical semantics are built explicitly via functorial constructions that embed LNL, Adjoint Logic, and mGL while preserving their structural properties. No load-bearing step reduces to a self-definition, a fitted parameter renamed as a prediction, or a self-citation chain; the unification is a self-contained generalization whose correctness rests on the explicit rule definitions and semantic functors rather than on prior fitted results or imported uniqueness theorems from the same authors.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Based solely on the abstract, the paper relies on standard background from type theory and category theory; no specific free parameters or invented entities beyond the GRASS system itself are described.

axioms (1)
  • standard math Standard rules and constructions of type theory and categorical semantics
    The development of the categorical semantics for GRASS presupposes ordinary category-theoretic machinery.
invented entities (1)
  • GRASS type system no independent evidence
    purpose: Unify graded and substructural mechanisms with support for multiple grade algebras
    New combined system introduced by the paper.

pith-pipeline@v0.9.0 · 5679 in / 1214 out tokens · 50772 ms · 2026-05-20T14:44:04.570293+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

31 extracted references · 31 canonical work pages

  1. [1]

    and J.-P

    Abel, A. and J.-P. Bernardy,A unified view of modalities in type systems, Proceedings of the ACM on Programming Languages4, pages 1–28 (2020), ISSN 2475-1421. https://doi.org/10.1145/3408972

    work page doi:10.1145/3408972 2020

  2. [2]

    Free higher groups in homotopy type theory

    Atkey, R.,Syntax and Semantics of Quantitative Type Theory, in:Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 56–65, Association for Computing Machinery, New York, NY, USA (2018), ISBN 978-1-4503-5583-4. https://doi.org/10.1145/3209108.3209189

    work page doi:10.1145/3209108.3209189 2018

  3. [3]

    Gaboardi, J

    Azevedo de Amorim, A., M. Gaboardi, J. Hsu, S.-y. Katsumata and I. Cherigui,A semantic account of metric preservation, SIGPLAN Not.52, pages 545–556 (2017), ISSN 0362-1340. https://doi.org/10.1145/3093333.3009890

    work page doi:10.1145/3093333.3009890 2017

  4. [4]

    N.,A mixed linear and non-linear logic: Proofs, terms and models, in: L

    Benton, P. N.,A mixed linear and non-linear logic: Proofs, terms and models, in: L. Pacholski and J. Tiuryn, editors, Computer Science Logic, pages 121–135, Springer, Berlin, Heidelberg (1995), ISBN 978-3-540-49404-1. https://doi.org/10.1007/BFb0022251

    work page doi:10.1007/bfb0022251 1995

  5. [5]

    Dagnino, P

    Bianchini, R., F. Dagnino, P. Giannini and E. Zucca,A Java-like calculus with heterogeneous coeffects, Theoretical Computer Science971, page 114063 (2023), ISSN 0304-3975. https://doi.org/10.1016/j.tcs.2023.114063

    work page doi:10.1016/j.tcs.2023.114063 2023

  6. [6]

    Dagnino, P

    Bianchini, R., F. Dagnino, P. Giannini and E. Zucca,Multi-Graded Featherweight Java, in:37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 3:1–3:27, Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik (2023). https://doi.org/10.4230/LIPIcs.ECOOP.2023.3

    work page doi:10.4230/lipics.ecoop.2023.3 2023

  7. [7]

    Bierman, G. M. and V. d. Paiva,On an Intuitionistic Modal Logic, Stud Logica65, pages 383–416 (2000). https://doi.org/10.1023/A:1005291931660

    work page doi:10.1023/a:1005291931660 2000

  8. [8]

    Gaboardi, D

    Brunel, A., M. Gaboardi, D. Mazza and S. Zdancewic,A Core Quantitative Coeffect Calculus, in: Z. Shao, editor, Programming Languages and Systems, pages 351–370, Springer, Berlin, Heidelberg (2014), ISBN 978-3-642-54833-8. https://doi.org/10.1007/978-3-642-54833-8_19

    work page doi:10.1007/978-3-642-54833-8_19 2014

  9. [9]

    Capucci, M. and B. Gavranovi´ c,Actegories for the Working Amthematician(2024). ArXiv:2203.16351 [math]. https://doi.org/10.48550/arXiv.2203.16351

    work page doi:10.48550/arxiv.2203.16351 2024

  10. [10]

    Eades III, R

    Choudhury, P., H. Eades III, R. A. Eisenberg and S. Weirich,A graded dependent type system with a usage-aware semantics, Proceedings of the ACM on Programming Languages5, pages 1–32 (2021), ISSN 2475-1421. https://doi.org/10.1145/3434331

    work page doi:10.1145/3434331 2021

  11. [11]

    de Amorim, A. A., M. Gaboardi, E. J. Gallego Arias and J. Hsu,Really Natural Linear Indexed Type Checking, in: Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages, IFL ’14, pages 1–12, Association for Computing Machinery, New York, NY, USA (2014), ISBN 978-1-4503-3284-2. https://doi.org/10.1145/27...

    work page doi:10.1145/2746325.2746335 2014

  12. [12]

    Orchard, Flavien Breuvart, and Tarmo Uustalu

    Gaboardi, M., S.-y. Katsumata, D. Orchard, F. Breuvart and T. Uustalu,Combining effects and coeffects via grading, in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 476–489, Association for Computing Machinery, New York, NY, USA (2016), ISBN 978-1-4503-4219-3. https://doi.org/10.1145/2951913.2951939

    work page doi:10.1145/2951913.2951939 2016

  13. [13]

    Ghica, D. R. and A. I. Smith,Bounded Linear Types in a Resource Semiring, in: Z. Shao, editor,Programming Languages and Systems, pages 331–350, Springer, Berlin, Heidelberg (2014), ISBN 978-3-642-54833-8. https://doi.org/10.1007/978-3-642-54833-8_18

    work page doi:10.1007/978-3-642-54833-8_18 2014

  14. [14]

    Giannini, P. and G. Duso,Coeffects for MiniJava: Cf-Mj, in:Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs, FTfJP 2024, pages 30–36, Association for Computing Machinery, New York, NY, USA (2024), ISBN 979-8-4007-1111-4. https://doi.org/10.1145/3678721.3686232

    work page doi:10.1145/3678721.3686232 2024

  15. [15]

    Girard, Linear logic , Theor

    Girard, J.-Y.,Linear logic, Theoretical Computer Science50, pages 1–101 (1987), ISSN 0304-3975. https://doi.org/https://doi.org/10.1016/0304-3975(87)90045-4

    work page doi:10.1016/0304-3975(87)90045-4 1987

  16. [16]

    Baier and U

    Katsumata, S.-y.,A Double Category Theoretic Analysis of Graded Linear Exponential Comonads, in: C. Baier and U. Dal Lago, editors,Foundations of Software Science and Computation Structures, pages 110–127, Springer International Publishing, Cham (2018), ISBN 978-3-319-89366-2. https://doi.org/10.1007/978-3-319-89366-2_6

    work page doi:10.1007/978-3-319-89366-2_6 2018

  17. [17]

    M.,Doctrinal adjunction, in: G

    Kelly, G. M.,Doctrinal adjunction, in: G. M. Kelly, editor,Category Seminar, pages 257–280, Springer, Berlin, Heidelberg (1974), ISBN 978-3-540-37270-7. https://doi.org/10.1007/BFb0063105 16 Hanukaev, Eades III

    work page doi:10.1007/bfb0063105 1974

  18. [18]

    https://doi.org/10.2307/2310058

    Lambek, J.,The mathematics of sentence structure, The American Mathematical Monthly65, pages 154–170 (1958). https://doi.org/10.2307/2310058

    work page doi:10.2307/2310058 1958

  19. [19]

    https://doi.org/10.1007/978-1-4613-0041-0

    Lang, S.,Algebra, Springer New York (2002). https://doi.org/10.1007/978-1-4613-0041-0

    work page doi:10.1007/978-1-4613-0041-0 2002

  20. [20]

    Marshall, D

    Liepelt, V.-B., D. Marshall, D. Orchard, V. Rajani and M. Vollmer,On Graded Coeffect Types for Information-Flow Control, in: D. Orchard, T. Petricek and J. Singer, editors,Languages, Compilers, Analysis - From Beautiful Theory to Useful Practice: Essays Dedicated to Alan Mycroft on the Occasion of His Retirement, pages 114–148, Springer Nature Switzerland...

    work page doi:10.1007/978-3-032-08187-2_7 2026

  21. [21]

    https://hal.science/hal-00154229v1

    Melli` es, P.-A.,Categorical semantics of linear logic, in:Interactive models of computation and program behaviour, number 27 in Panoramas et Synth` eses, pages 1 – 196, Soci´ et´ e Math´ ematique de France (2009). https://hal.science/hal-00154229v1

    work page 2009

  22. [22]

    Eades III and D

    Moon, B., H. Eades III and D. Orchard,Graded Modal Dependent Type Theory, in: N. Yoshida, editor,Programming Languages and Systems, pages 462–490, Springer International Publishing, Cham (2021), ISBN 978-3-030-72019-3. https://doi.org/10.1007/978-3-030-72019-3_17

    work page doi:10.1007/978-3-030-72019-3_17 2021

  23. [23]

    Liepelt and H

    Orchard, D., V.-B. Liepelt and H. Eades III,Quantitative program reasoning with graded modal types, Language implementation for Quantitative Program Reasoning with Graded Modal Types3, pages 110:1–110:30 (2019). https://doi.org/10.1145/3341714

    work page doi:10.1145/3341714 2019

  24. [24]

    Orchard and A

    Petricek, T., D. Orchard and A. Mycroft,Coeffects: Unified Static Analysis of Context-Dependence, in: F. V. Fomin, R. Freivalds, M. Kwiatkowska and D. Peleg, editors,Automata, Languages, and Programming, pages 385–397, Springer Berlin Heidelberg, Berlin, Heidelberg (2013), ISBN 978-3-642-39212-2. https://doi.org/10.1007/978-3-642-39212-2_35

    work page doi:10.1007/978-3-642-39212-2_35 2013

  25. [25]

    Orchard and A

    Petricek, T., D. Orchard and A. Mycroft,Coeffects: a calculus of context-dependent computation, ACM SIGPLAN Notices 49, pages 123–135 (2014), ISSN 0362-1340, 1558-1160. https://doi.org/10.1145/2692915.2628160

    work page doi:10.1145/2692915.2628160 2014

  26. [26]

    https://doi.org/10.1023/A:1015186718090

    Petri´ c, Z.,Coherence in Substructural Categories, Studia Logica70, pages 271–296 (2002), ISSN 1572-8730. https://doi.org/10.1023/A:1015186718090

    work page doi:10.1023/a:1015186718090 2002

  27. [27]

    Chargin, F

    Pruiksma, K., W. Chargin, F. Pfenning and J. Reed,Adjoint logic(2018). https://www.cs.cmu.edu/~./fp/papers/adjoint18b.pdf

    work page 2018

  28. [28]

    Barthe and D

    Rajani, V., G. Barthe and D. Garg,A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs, Proc. ACM Program. Lang.8, pages 285:389–285:414 (2024). https://doi.org/10.1145/3689725

    work page doi:10.1145/3689725 2024

  29. [29]

    Uustalu, T. and T. Vene,Signals and Comonads, JUCS - Journal of Universal Computer Science11, pages 1310–1326 (2005), ISSN 0948-6968, 0948-695X. Number: 7. https://doi.org/10.3217/jucs-011-07-1311

    work page doi:10.3217/jucs-011-07-1311 2005

  30. [30]

    Uustalu, T. and V. Vene,Comonadic Notions of Computation, Electronic Notes in Theoretical Computer Science203, pages 263–284 (2008), ISSN 1571-0661. https://doi.org/10.1016/j.entcs.2008.05.029

    work page doi:10.1016/j.entcs.2008.05.029 2008

  31. [31]

    move scalars out of the tensor product,

    Vollmer, V., D. Marshall, H. Eades III and D. Orchard,A Mixed Linear and Graded Logic: Proofs, Terms, and Models, in: J. Endrullis and S. Schmitz, editors,33rd EACSL Annual Conference on Computer Science Logic (CSL 2025), volume 326 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 32:1–32:21, Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Info...

    work page doi:10.4230/lipics.csl.2025.32 2025