Logical Foundations of Quantitative Equality (long version)

Quantitative reasoning provides a flexible approach capable to deal with the uncertainty and imprecision that affects modern software systems due to their complexity. Its distinguishing feature is the use of distances, instead of equivalence relations, so that one can measure how much two objects are similar, rather than just saying whether they are equivalent or not. In this paper we aim at providing a solid logical ground to quantitative reasoning, using the categorical language of Lawvere's hyperdoctrines. The key idea is to see distances as equality predicates in Linear Logic. Adding equality to Linear Logic, however, is not as trivial as it might appear. The linear version of the usual rules for equality, asserting that it is reflexive and substitutive, has the consequence that equality collapses to an equivalence relation, as it can be used an arbitrary number of times. To overcome this issue, we consider the extension of Linear Logic with graded modalities and use them to write a resource sensitive substitution rule that keeps equality quantitative. We introduce a deductive calculus for (Graded) Linear Logic with quantitative equality and the notion of Lipschitz doctrine to give semantics to it. Main examples are based on metric spaces and Lipschitz maps and on quantitative realisability.