一句话：用 Lipschitz doctrine 为含分级模态的子结构逻辑建立定量等式（距离）的可靠完备范畴语义。
子结构逻辑将公式视为可消耗资源，因而适合对公式作定量解释；距离可视为等价关系的定量对应，用来刻画对象的相似程度。本文在 Lawvere doctrine 的范畴语言下，研究子结构逻辑中的等式应如何定量建模。作者在带分级模态的线性逻辑最小片段中工作，该模态用于写出资源敏感的等式替换规则，从而把等式解释为距离。文章给出演绎演算，并引入 Lipschitz doctrine 作为范畴语义，证明其可靠且完备。进一步，通过考察 Lipschitz doctrine 的 2-范畴性质，作者得到一种通用构造，可从度量空间与定量 realisability 等来源生成模型，并把结果扩展到更丰富的子结构逻辑，直至带量词的全线性逻辑。
Substructural logics naturally support a quantitative interpretation of formulas, as they are seen as consumable resources. Distances are the quantitative counterpart of equivalence relations: they measure how much two objects are similar, rather than just saying whether they are equivalent or not. Hence, they provide the natural choice for modelling equality in a substructural setting. In this paper, we develop this idea, using the categorical language of Lawvere's doctrines. We work in a minimal fragment of Linear Logic enriched by graded modalities, which are needed to write a resource sensitive substitution rule for equality, enabling its quantitative interpretation as a distance. We introduce both a deductive calculus and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. The study of 2-categorical properties of Lipschitz doctrines provides us with a universal construction, which generates examples based for instance on metric spaces and quantitative realisability. Finally, we show how to smoothly extend our results to richer substructural logics, up to full Linear Logic with quantifiers.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{DagninoP25,
title = {Quantitative Equality in Substructural Logic via Lipschitz Doctrines},
author = {Francesco Dagnino and Fabio Pasquali},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:7)2025}
}