← 研踪 PaperTrailarXiv:2605.17112 · v4
A unification of graded and substructural logics
首次提交 2026-05-17 02:35
版本更新 2026-11-03 03:16
雷达观测 2026-11-04 23:40
摘要
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 GRASS, and find that, on the level of categorical semantics, it subsumes multiple established systems such as LNL, Adjoint Logic, and mGL.
作者备注：Conference: MFPS XLII; final version; 18 pages, version without appendices
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v4 · 2026-11-03 03:16 · 最新观测版本
A unification of graded and substructural logics
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 GRASS, and find that, on the level of categorical semantics, it subsumes multiple established systems such as LNL, Adjoint Logic, and mGL.
查看此版本解读 →查看此版本原文 ↗