技术摘要：分级逻辑与次结构逻辑的统一（Grass）

问题陈述

将程序变量视为资源已成为验证内存安全和信息流等正确性属性的核心。文献中主要有两种截然不同的方法：

1. 次结构逻辑：如线性逻辑等系统默认限制结构规则（弱化与收缩），并通过模态（例如“当然”模态 $!$）选择性地重新引入这些规则。尽管这些系统功能强大，但它们通常难以在一个框架内组合具有不同结构规则的不同逻辑，除非借助复杂的伴随关系。
2. 分级系统：这些系统默认允许结构规则，但使用源自代数结构（通常是半环）的“等级”来标注假设。等级对资源使用进行定量追踪（例如，通过加法实现收缩，通过零元素实现弱化）。尽管具有灵活性，但标准的分级系统通常假设单一的等级代数，并且可能缺乏对哪些特定变量可以进行收缩或弱化的细粒度控制，往往在单一代数体制下对所有变量进行统一处理。

本文解决的核心问题是缺乏一个统一的类型系统，能够同时支持：

• 在同一程序中支持多种不同的资源使用概念（不同的等级代数）。
• 对结构规则（弱化和收缩）进行细粒度控制，超越简单的布尔开关，允许特定的等级可收缩而其他等级不可收缩。
• 将这些功能无缝集成到单一的范畴语义中。

方法论

作者提出了 Grass（分级与次结构），这是一种通过以下机制统一上述方法的类型系统：

1. 模式与等级代数

Grass 由一组模式参数化。每个模式 $m$ 是一个三元组 $(R_m, \text{Cont}(m), \text{Weak}(m))$，其中：

• $R_m$ 是一个等级代数（一个预序半环）。
• $\text{Cont}(m) \subseteq R_m$ 是半环中的一个理想。该理想定义了相互可收缩的等级集合。
• $\text{Weak}(m) \in \{\text{true}, \text{false}\}$ 是一个布尔标志，指示该模式是否允许弱化。

这种结构允许细粒度的控制：收缩不是系统的全局属性，而是限制在特定模式的理想内的等级。弱化同样受到控制，但作者指出，由于包含规则，启用弱化允许在任何等级 $q \geq 0$ 引入未使用的变量。

2. 语法与类型规则

语法扩展了标准的分级模态类型，包括：

• 异构上下文：类型判定 $\rho \mid M \odot \Gamma \vdash_m t : T$ 包含等级向量 $\rho$ 和模式向量 $M$。上下文 $\Gamma$ 中的变量可以属于不同的模式，前提是遵守当前模式 $m$ 的结构规则。
• 用于模式转换的模态：
  • 丢弃（$\downarrow^q_{n \leq m}$）：将项从模式 $m$ 提升到一个“更严格”的模式 $n$（其中 $n \leq m$），并强制执行特定的使用等级 $q$。这推广了分级模态 $\Box_q A$。
  • 提升（$\uparrow^{m \leq n}$）：将项从更严格的模式 $n$ 提升到更宽松的模式 $m$。
• 结构规则：
  • 收缩：仅当被收缩变量的等级属于 $\text{Cont}(m)$ 中的元素时才允许。
  • 弱化：仅当 $\text{Weak}(m)$ 为真时才允许。
  • 代入：定义为处理不同模式与等级乘法之间的交互，确保保持“独立性”属性（来自更严格模式的项不能依赖于来自更宽松模式的变量）。

3. 范畴语义

作者基于分级线性指数余单子开发了范畴语义。

• 指数作用：对于每个模式 $m$，语义在对称幺半闭范畴（SMCC）上定义了一个指数作用。这涉及一个函子 $D: R_m^{op} \to \text{SMC}(C, C)$，配备用于收缩（$c$）和弱化（$w$）的自然变换，并满足相干性条件。
• 作用的态射：为了连接不同的模式，作者引入了指数作用之间态射的新概念。这些是配备“线性算子”自然变换 $\ell$ 的对称松弛幺半伴随 $F \dashv G$。这种结构在语法上对应于模态 $\downarrow$ 和 $\uparrow$。
• 模型：该语义表明，直觉主义逻辑、线性逻辑、相关逻辑和仿射逻辑的已知模型可以作为 Grass 模式的具体实例被恢复。此外，该语义涵盖了线性 - 非线性逻辑（LNL）、伴随逻辑和 mGL 等已建立的系统。

主要贡献与结果

1. 逻辑的统一：Grass 提供了一个单一框架，其中变量可以同时由不同的等级代数控制。例如，一个函数可以接受一个由“安全”代数分级的密钥（其中 $High$意味着安全上下文）和一个由“使用”代数分级的文件句柄（其中$1$ 意味着线性使用）。
2. 细粒度的结构控制：通过通过理想而非全局规则来定义收缩，Grass 允许了之前的分级系统难以表达的资源敏感区分。例如，两个线性使用的文件句柄（等级 1）不能收缩为一个无限制句柄（等级 $\omega$），从而防止了不安全的资源合并。
3. 现有系统的恢复：本文证明，通过实例化特定模式，Grass 可以恢复：
   • 直觉主义逻辑：模式 $U = (\top, \top, \text{true})$。
   • 线性逻辑：模式 $L = (\mathbb{N}, \{0\}, \text{false})$（具有离散序）。
   • 相关逻辑：模式 $R = (\top, \top, \text{false})$。
   • 仿射逻辑：模式 $A = (\{0, 1\}, \{0\}, \text{true})$。
   • LNL 和伴随逻辑：通过结合具有适当态射的模式。
4. 范畴正确性：作者证明了 $\beta$-和 $\eta$-转换相对于范畴语义是可靠的。项到范畴模型的解释保持了类型和分级。

意义与主张

本文声称，Grass 通过结合次结构逻辑和分级逻辑的机制，提供了对变量使用的“最大灵活控制”。其主要意义在于：

• 表达能力：它允许同一程序中的不同变量由不同的资源使用概念（例如安全与内存使用）支配，而无需单一的等级代数。
• 理论统一：它表明在范畴语义的层面上，Grass 通过将 LNL、伴随逻辑和 mGL 等已建立的系统视为模式和态射的特定配置，涵盖了这些系统。
• 新颖的语义：基于作用范畴（actegories）的分级余单子之间态射的引入，为推理不同资源逻辑之间的交互提供了新工具。

作者对实际实现保持谦逊，指出虽然该系统恢复并推广了已知逻辑，但当前的重点在于理论统一和范畴基础。他们建议未来的工作可以探索将这些经验教训应用于分级依赖类型，特别是解决将类型视为直觉主义（无分级）同时保持项为分级这一挑战。