Ordered Adjoint Logic (Extended Version)

“有序伴随逻辑”技术摘要

问题陈述
有序逻辑和类型系统对于从计算语言学到安全协议执行等应用至关重要，在这些应用中，资源使用的顺序具有重要意义。在大多数表述中，有序类型也是线性的，要求资源必须恰好使用一次。虽然 Kanovich 等人先前的工作研究了通过线性有序逻辑中的次指数（subexponentials）来放松这一约束的演算，但这种方法依赖于一个所有推理都发生的“基础模式”。对于有序逻辑而言，该基础模式必须禁止所有结构规则（弱化、收缩、交换），从而导致应用程序频繁地进出这一限制性模式。此外，现有的次指数系统并未充分探索单向结构属性（例如，具有左移动性而无右移动性）的可能性。作者旨在推广这些框架，以支持具有不同细粒度结构属性的模式预序——包括对弱化、左/右收缩以及左/右移动性的独立控制——而无需依赖单一的限制性基础模式。

方法论
作者引入了有序伴随逻辑，这是一个结合了伴随模态的结构灵活性与有序逻辑的顺序约束的系统。该方法论分为两个主要阶段：

1. 序列演算表述：
   作者定义了一个序列演算，其中前件是带有标签假设的有序序列。结构规则并非全局的，而是由模式预序（$k \geq m$）管辖。每个模式 $m$ 关联一组结构属性 $\sigma(m) \subseteq \{W, C, M_{\leftarrow}, M_{\rightarrow}\}$（弱化、收缩、左移动性、右移动性）。

   • 移位模态：该系统不使用基础模式，而是利用移位模态（$\downarrow^k_m$ 和 $\uparrow^m_l$）在不同模式间切换推理。这些移位源自 Benton 的伴随逻辑，但被推广以处理有序语境。
   • 结构规则：作者将移动性和收缩分解为单向变体。移动性规则允许单个命题在前件序列中任意向左或向右移动，前提是命题的模式承认相应的方向性移动性。收缩被允许非局部地执行（合并非相邻的重复项），以确保截断消除，这与标准线性逻辑中的局部收缩不同。
   • 逻辑连接词：该语言包含有序蕴含（$\multimap$ 和 $\multimap$）、融合与扭曲合取以及移位。规则在其模式上是参数化的，并包含特定条件以确保在从结论读取到前提时保持模式独立性（例如，$k \geq m \geq r$）。

2. 自然演绎与可判定性：
   作者转向自然演绎表述，其中结构规则是隐式的，旨在为编程语言奠定基础。

   • 显式与隐式：最初，他们提出了一个带有显式结构规则的系统，以弥合与序列演算的差距。随后，他们定义了一个结构规则（弱化、收缩、移动性）为隐式的系统。
   • 证明检查算法：为了解决隐式结构规则引入的非确定性（特别是弱化的无界应用以及消除规则中变量的放置），作者定义了一个“范式”判据（$\Omega \gg_{\Gamma, r} \Omega_{nf}$）。该算法计算给定语境 $\Omega$、假设集 $\Gamma$ 和模式 $r$ 的所有可能范式（无重复变量的语境）集合。
   • 基于集的判据：自然演绎规则被提升为在范式语境集（$\Xi$）上操作。例如，合取引入计算语境集的笛卡尔积，而交集则用于需要语境一致性的规则（如加性合取）。

主要贡献

• 广义伴随逻辑：本文将伴随逻辑推广到有序环境，引入了模式预序，其中每个模式独立控制弱化、收缩和单向移动性。
• 单向结构属性：该系统明确建模并证明了左/右移动性和收缩作为独立的、分离的结构属性，这是先前次指数工作中预期但未探索的特性。
• 截断消除：作者证明了有序伴随序列演算允许截断消除（通过多重截断）和恒等消除，确立了该系统作为一个行为良好的逻辑框架。
• 证明检查的可判定性：本文提供了一个带有隐式结构规则的自然演绎系统，并证明了该系统的证明检查是可判定的。这是通过构建一个计算范式语境集的终止算法实现的。

结果

• 理论可靠性：序列演算被证明满足截断和恒等消除。自然演绎系统被证明相对于序列演算是可靠且完备的。
• 可判定性：计算范式（$NF_{\Gamma, r}(\Omega)$）的算法被证明是终止的。因此，在隐式自然演绎系统中检查证明的问题是可判定的。
• 子结构包含：结果暗示了子结构包含的可判定性，这是 QRTT 等语言类型检查算法的核心组件（该语言使用带有显式世界的克里普克语义）。

意义与主张
作者主张，有序伴随逻辑为一种富有表现力的伴随编程语言或逻辑框架提供了合适的基础。通过将结构属性与单一基础模式解耦并使用伴随移位，该系统允许在各种学科（线性、有序、无限制）中进行原生推理，并实现无缝切换。带有隐式结构规则的证明检查的可判定性被强调为迈向实现双向类型检查器的关键步骤，这些检查器能够处理函数式编程语言中代码的细粒度结构属性。论文指出，虽然决策过程已确立，但实际效率（例如，避免由不必要的弱化引起的指数级复杂度）仍是未来优化的主题。这项工作被定位为对 Kanovich 等人次指数有序逻辑的直接推广，以及对 Jang 等人伴随类型的扩展，使其包含顺序。