一句话：在 Linear Logic 中把距离视为相等谓词，用 graded modality 建立定量等式的证明系统与 Lipschitz doctrine 语义。
论文旨在为基于距离的定量推理提供逻辑基础，突破传统等价关系只能判断“是否相同”的局限。作者在 Linear Logic 中工作，采用 Lawvere doctrines 的范畴语言，将距离理解为线性逻辑中的相等谓词。通过 graded modalities 给出资源敏感的等式替换规则，使等式具有按距离度量的定量含义。文章提出带定量等式的 (Graded) Linear Logic 演绎演算，并引入 Lipschitz doctrine 作为范畴语义，证明该演算相对此语义的可靠性与完备性。最后给出 Lipschitz doctrine 的泛构造，从度量空间与定量可实现性等来源生成具体模型。
In quantitative reasoning one compares objects by distances, instead of equivalence relations, so that one can measure how much they are similar, rather than just saying whether they are equivalent or not. In this paper we aim at providing a logical ground to quantitative reasoning with distances in Linear Logic, using the categorical language of Lawvere’s doctrines. The key idea is to see distances as equality predicates in Linear Logic. We use graded modalities to write a resource sensitive substitution rule for equality, which allows us to give it a quantitative meaning by distances. We introduce a deductive calculus for (Graded) Linear Logic with quantitative equality and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. We also describe a universal construction of Lipschitz doctrines, which generates examples based for instance on metric spaces and quantitative realisability.