2026-08-17T10:24:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23630 2025-10-27T10:30:23Z ddc:004 open_access

On the Metric Nature of (Differential) Logical Relations Dal Lago, Ugo Hoshino, Naohiko Pistone, Paolo Differential Logical Relations Quantales Quasi-Metrics Partial Metrics Differential logical relations are a method to measure distances between higher-order programs. They differ from standard methods based on program metrics in that differences between functional programs are themselves functions, relating errors in input with errors in output, this way providing a more fine grained, contextual, information. The aim of this paper is to clarify the metric nature of differential logical relations. While previous work has shown that these do not give rise, in general, to (quasi-)metric spaces nor to partial metric spaces, we show that the distance functions arising from such relations, that we call quasi-quasi-metrics, can be related to both quasi-metrics and partial metrics, the latter being also captured by suitable relational definitions. Moreover, we exploit such connections to deduce some new compositional reasoning principles for program differences. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ugo Dal Lago and Naohiko Hoshino and Paolo Pistone 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.15 urn:nbn:de:0030-drops-236300 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.15 eng https://creativecommons.org/licenses/by/4.0/legalcode