Document Open Access Logo

On the Metric Nature of (Differential) Logical Relations

Authors Ugo Dal Lago , Naohiko Hoshino , Paolo Pistone

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.15.pdf
  • Filesize: 0.87 MB
  • 22 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.15.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Theory of computation → Equational logic and rewriting
Keywords
  • Differential Logical Relations
  • Quantales
  • Quasi-Metrics
  • Partial Metrics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Metric Nature of (Differential) Logical Relations. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.15

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Naohiko Hoshino
  • Sojo University, Kumamoto, Japan
Paolo Pistone
  • Université Claude Bernard Lyon 1, France

References

  1. Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, and C.-H. Luke Ong. Fixing incremental computation. In Luís Caires, editor, Proc. of ESOP 2019, pages 525-552. Springer, 2019. Google Scholar
  2. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Proc. of POPL 2017, pages 545-556. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009890.
  3. Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, and Francesco Gavazzo. On Feller continuity and full abstraction. Proc. ACM Program. Lang., 6(ICFP), August 2022. URL: https://doi.org/10.1145/3547651.
  4. Michael Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metric spaces. American Mathematical Monthly, 116:708-718, October 2009. URL: https://doi.org/10.4169/193009709X460831.
  5. Michael A. Bukatin and Joshua S. Scott. Towards computing distances between programs via Scott domains. In Sergei Adian and Anil Nerode, editors, Proc. of LFCS 1997, pages 33-43. Springer, 1997. URL: https://doi.org/10.1007/3-540-63045-7_4.
  6. Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation. In Proc. of PLDI 2014, pages 145-155. ACM, 2014. URL: https://doi.org/10.1145/2594291.2594304.
  7. Francesco Dagnino and Francesco Gavazzo. A fibrational tale of operational logical relations: Pure, effectful and differential. Logical Methods in Computer Science, 20(2), April 2024. URL: https://doi.org/10.46298/lmcs-20(2:1)2024.
  8. Fredrik Dahlqvist and Renato Neves. A complete v-equational system for graded lambda-calculus. In Marie Kerjean and Paul Blain Levy, editors, Proc. of MFPS XXXIX, volume 3 of EPTICS, 2023. URL: https://doi.org/10.46298/ENTICS.12299.
  9. Ugo Dal Lago and Francesco Gavazzo. Differential logical relations, Part II increments and derivatives. Theoretical Computer Science, 895:34-47, 2021. URL: https://doi.org/10.1016/J.TCS.2021.09.027.
  10. Ugo Dal Lago and Francesco Gavazzo. Effectful program distancing. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498680.
  11. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Proc. of ICALP 2019, volume 132 of LIPIcs, pages 111:1-111:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.ICALP.2019.111.
  12. Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Proc. of FSCD 2022, volume 228 of LIPIcs, pages 4:1-4:18, Dagstuhl, Germany, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.4.
  13. Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In Proc. of FSCD 2023, volume 260 of LIPIcs, pages 20:1-20:19, Dagstuhl, Germany, 2023. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.20.
  14. Derek Dreyer, Amal Ahmed, and Lars Birkedal. Logical step-indexed logical relations. In Proc. of LICS 2009, pages 71-80. IEEE, 2009. URL: https://doi.org/10.1109/LICS.2009.34.
  15. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. SIGPLAN Not., 48(1):357-370, January 2013. URL: https://doi.org/10.1145/2480359.2429113.
  16. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proc. of LICS 2018, pages 452-461. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209149.
  17. Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Proc. of CSL 2021, volume 183 of LIPIcs, pages 35:1-35:18, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.23.
  18. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. Google Scholar
  19. Jean Goubault-Larrecq. Non-Hausdorff Topology and Domain Theory: Selected Topics in Point-Set Topology. New Mathematical Monographs. Cambridge University Press, 2013. Google Scholar
  20. Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. In Proc. of CSL 2002, pages 553-568. Springer, 2002. URL: https://doi.org/10.1007/3-540-45793-3_37.
  21. Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson. Logical relations and parametricity - A Reynolds programme for category theory and programming languages. In Proc. of WACT 2013, volume 303 of ENTCS, pages 149-180. Elsevier, 2014. URL: https://doi.org/10.1016/J.ENTCS.2014.02.008.
  22. Dirk Hofmann, Gavin J Seal, and W Tholen. Monoidal Topology: a Categorical Approach to Order, Metric and Topology. Cambridge University Press, New York, 2014. Google Scholar
  23. Dirk Hofmann and Isar Stubbe. Topology from enrichment: the curious case of partial metrics. Cahiers de Topologie et Géométrie Différentielle Catégorique, LIX, 4:307-353, 2018. Google Scholar
  24. H.-P.A. Künzi, H. Pajoohesh, and M.P. Schellekens. Partial quasi-metrics. Theoretical Computer Science, 365(3):237-246, 2006. URL: https://doi.org/10.1016/j.tcs.2006.07.050.
  25. Roy L.Crole. Categories for Types. Cambridge University Press, 1993. Google Scholar
  26. Valentin Maestracci and Paolo Pistone. The Lambda Calculus Is Quantifiable. In Proc. of CSL 2025, volume 326 of LIPIcs, pages 34:1-34:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CSL.2025.34.
  27. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proc. of LICS 2016. IEEE Computer Society, 2016. Google Scholar
  28. Sparsh Mittal. A survey of techniques for approximate computing. ACM Comput. Surv., 48(4), March 2016. URL: https://doi.org/10.1145/2893356.
  29. Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In Proc. of LICS 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470696.
  30. Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In Proc. of TLCA 1993, volume 664 of LNCS, pages 361-375. Springer, 1993. URL: https://doi.org/10.1007/BFB0037118.
  31. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger. Proc. of ICFP 2010, pages 157-168, 2010. Google Scholar
  32. John C. Reynolds. Types, abstraction and parametric polymorphism. In R.E.A. Mason, editor, Information Processing '83, pages 513-523. North-Holland, 1983. Google Scholar
  33. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Logical bisimulations and functional languages. In Farhad Arbab and Marjan Sirjani, editors, Proc. of FSEN 2007, pages 364-379. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-75698-9_24.
  34. Michel P. Schellekens. A characterization of partial metrizability: domains are quantifiable. Theoretical Computer Science, 305(1-3):409-432, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00705-3.
  35. Michael B. Smyth. The constructive maximal point space and partial metrizability. Ann. Pure Appl. Log., 137(1-3):360-379, 2006. URL: https://doi.org/10.1016/j.apal.2005.05.032.
  36. Isar Stubbe. An introduction to quantaloid-enriched categories. Fuzzy Sets and Systems, 256:95-116, 2014. URL: https://doi.org/10.1016/j.fss.2013.08.009.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact