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.
翻译:结构性逻辑自然地支持对公式的定量解释,因为它们被视为消耗的资源。距离是等同关系的定量对应物:它们测量两个对象的相似程度,而不是仅仅说它们是否等同。因此,它们为在次结构环境中模拟平等提供了自然的选择。在本文中,我们利用法律理论的绝对语言来发展这一理念。我们的工作是用分级模式来丰富线性逻辑的微小碎片,这需要为平等写出资源敏感替代规则,使其量化解释成为距离。我们引入了一种分级计算法和利普西茨理论的概念,以赋予它一个健全和完整的绝对语义。利普施茨理论的2类特性研究为我们提供了一种通用的构思,它为我们树立了基于衡量空间和量化真实性的例子。最后,我们展示了如何顺利地将我们的结果扩展为更丰富的次结构逻辑,直到带有量化的完整线性逻辑。