Francesco Dagnino ; Fabio Pasquali - Quantitative Equality in Substructural Logic via Lipschitz Doctrines

lmcs:10396 - Logical Methods in Computer Science, January 28, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:7)2025
Quantitative Equality in Substructural Logic via Lipschitz DoctrinesArticle

Authors: Francesco Dagnino ; Fabio Pasquali

    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.


    Volume: Volume 21, Issue 1
    Published on: January 28, 2025
    Accepted on: December 4, 2024
    Submitted on: November 30, 2022
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Category Theory

    Consultation statistics

    This page has been seen 98 times.
    This article's PDF has been downloaded 46 times.