Tags:graded modalities, hyperdoctrine, linear logic, lipschitz doctrine, quantitative equality and quantitative reasoning
Abstract:
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 solid logical ground to quantitative reasoning with distances, using the categorical language of Lawvere's hyperdoctrines. The key idea is to see distances as equality predicates in Linear Logic. We use graded modalitiess 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 define a sound and complete categorical semantics of it. We also describe a universal construction of Lipschitz doctrines, which generates examples based for instance on metric spaces and quantitative realisability.