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.

翻译：子结构逻辑天然支持公式的定量解释，因为公式被视为可消耗资源。距离是等价关系的定量对应物：它们度量两个对象的相似程度，而非仅仅判断其是否等价。因此，距离为子结构框架下的等式建模提供了自然选择。本文利用Lawvere学说的范畴语言发展这一思想。我们工作在线性逻辑的最小片段中，该片段通过分级模态进行扩展——这些模态是实现资源敏感等式替换规则所必需的，从而支持其作为距离的定量解释。我们同时引入演绎演算与Lipschitz学说概念，为其提供完备且可靠的范畴语义。对Lipschitz学说的2-范畴性质研究揭示了一种通用构造方法，可生成基于度量空间、定量可实现性等概念的实例。最后，我们展示了如何将结果平滑扩展至更丰富的子结构逻辑，直至包含量词的全线性逻辑。