Document Open Access Logo

On the Lattice of Program Metrics

Authors Ugo Dal Lago , Naohiko Hoshino , Paolo Pistone

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.20.pdf
  • Filesize: 0.86 MB
  • 19 pages

Document Identifiers

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Naohiko Hoshino
  • Sojo University, Japan
Paolo Pistone
  • University of Bologna, Italy

Funding

The first and third authors are partially supported by the ERC CoG DIAPASoN, GA 818616. The second author is supported by JSPS KAKENHI Grant Number JP21K11762.

Cite AsGet BibTex

Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.20

Abstract

In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie in between the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • Metrics
  • Lambda Calculus
  • Linear Types

Metrics

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

Related Versions

References

  1. S. Abramsky and R. Jagadeesan. New foundations for the geometry of interaction. Information and Computation, 111(1):53-119, 1994. URL: https://doi.org/10.1006/inco.1994.1041.
  2. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pages 545-556, New York, NY, USA, 2017. Association for Computing Machinery. Google Scholar
  3. Andrew Barber and Gordon D. Plotkin. Dual intuitionistic linear logic, 1996. Unpublished draft. An early version appeared as a technical report ECS-LFCS-96-347, LFCS, University of Edinburgh. Google Scholar
  4. Avrim Blum, Cynthia Dwork, Frank McSherry, and Kobbi Nissim. Practical privacy: The sulq framework. In Proceedings of the 24th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS 2005), pages 128-138, New York, NY, USA, 2005. Association for Computing Machinery. URL: https://doi.org/10.1145/1065167.1065184.
  5. Raphaëlle Crubillé and Ugo Dal Lago. On probabilistic applicative bisimulation and call-by-value λ-calculi. In Zhong Shao, editor, Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP 2014), volume 8410 of Lecture Notes in Computer Science, pages 209-228. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_12.
  6. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The affine case. In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), pages 633-644, USA, 2015. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2015.64.
  7. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The general case. In Hongseok Yang, editor, Proceedings of the 26th European Symposium on Programming Languages and Systems (ESOP 2017), Lecture Notes in Computer Science, pages 341-367, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-54434-1_13.
  8. Raphaëlle Crubillé, Ugo Dal Lago, Davide Sangiorgi, and Valeria Vignudelli. On applicative similarity, sequentiality, and full abstraction. In Roland Meyer, André Platzer, and Heike Wehrheim, editors, Proceedings of Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, volume 9360 of Lecture Notes in Computer Science, pages 65-82. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23506-6_7.
  9. Fredrik Dahlqvist and Renato Neves. An internal language for categories enriched over generalised metric spaces. In Florin Manea and Alex Simpson, editors, Proceedings of the 30th EACSL Annual Conference on Computer Science Logic, (CSL 2022), volume 216 of LIPIcs, pages 16:1-16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.16.
  10. Ugo Dal Lago and Francesco Gavazzo. Effectul program distancing. Proceedings of the ACM on Programming Languages, 6(POPL):1-30, 2022. URL: https://doi.org/10.1145/3498680.
  11. Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Amy P. Felty, editor, Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.4.
  12. Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the lattice of program metrics, 2023. URL: https://arxiv.org/abs/2302.05022.
  13. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full abstraction for probabilistic PCF. Journal of the ACM, 65(4), 2018. URL: https://doi.org/10.1145/3164540.
  14. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pages 452-461, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209149.
  15. Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Proceedings of the 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.23.
  16. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. Google Scholar
  17. Jean-Yves Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, editors, Proceedings of the Logic Colloquium '88, volume 127 of Studies in Logic and the Foundations of Mathematics, pages 221-260. North-Holland, 1989. Google Scholar
  18. Masahito Hasegawa. Models of Sharing Graphs: A Categorical Semantics of Let and Letrec. Springer-Verlag, Berlin, Heidelberg, 1999. Google Scholar
  19. Masahito Hasegawa. On traced monoidal closed categories. Mathematical Structures in Computer Science, 19(2):217-244, 2009. URL: https://doi.org/10.1017/S0960129508007184.
  20. J. M. E. Hyland and C. H. L. Ong. On Full Abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. URL: https://doi.org/10.1006/inco.2000.2917.
  21. André Joyal, Ross Street, and Dominic Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119(3):447-468, 1996. Google Scholar
  22. Shin-ya Katsumata. A double category theoretic analysis of graded linear exponential comonads. In Christel Baier and Ugo Dal Lago, editors, Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2018), pages 110-127, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89366-2_6.
  23. Soren Bogh Lassen. Relational Reasoning about Functions and Nondeterminism. PhD thesis, University of Aarhus, available at https://www.brics.dk/DS/98/2/BRICS-DS-98-2.pdf, 1998.
  24. Ian Mackie, Leopoldo Román, and Samson Abramsky. An internal language for autonomous categories. Applied Categorical Structures, 1:311-343, 1993. Google Scholar
  25. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), pages 1-10, New York, NY, USA, 2016. Google Scholar
  26. Robin Milner. Fully abstract models of typed λ-calculi. Theoretical Computer Science, 4(1):1-22, 1977. URL: https://doi.org/10.1016/0304-3975(77)90053-6.
  27. James Hiram Morris. Lambda-calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, available at https://dspace.mit.edu/handle/1721.1/64850, 1969.
  28. Paolo Pistone. On generalized metric spaces for the simply typed λ-calculus. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), pages 1-14. IEEE Computer Society, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470696.
  29. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), volume 45, pages 157-168, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1932681.1863568.
  30. Peter Selinger. A survey of graphical languages for monoidal categories. In Bob Coecke, editor, New Structures for Physics, volume 813 of Lecture Notes in Physics, pages 289-355. Springer-Verlag Berlin Heidelberg, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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