Document Open Access Logo

A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations

Authors Guillaume Geoffroy, Paolo Pistone

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.23.pdf
  • Filesize: 0.58 MB
  • 18 pages

Document Identifiers

Author Details

Guillaume Geoffroy
  • University of Bologna, Department of Computer Science and Engineering, Italy
Paolo Pistone
  • University of Bologna, Department of Computer Science and Engineering, Italy

Funding

  • Geoffroy, Guillaume: ERC CoG 818616 "DIAPASoN", ANR 16CE250011 "REPAS".
  • Pistone, Paolo: ERC CoG 818616 "DIAPASoN", ANR 16CE250011 "REPAS".

Cite As Get BibTex

Guillaume Geoffroy and Paolo Pistone. A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.23

Abstract

Program semantics is traditionally concerned with program equivalence. However, in fields like approximate, incremental and probabilistic computation, it is often useful to describe to which extent two programs behave in a similar, although non equivalent way. This has motivated the study of program (pseudo)metrics, which have found widespread applications, e.g. in differential privacy. In this paper we show that the standard metric on real numbers can be lifted to higher-order types in a novel way, yielding a metric semantics of the simply typed lambda-calculus in which types are interpreted as quantale-valued partial metric spaces. Using such metrics we define a class of higher-order denotational models, called diameter space models, that provide a quantitative semantics of approximate program transformations. Noticeably, the distances between objects of higher-types are elements of functional, thus non-numerical, quantales. This allows us to model contextual reasoning about arbitrary functions, thus deviating from classic metric semantics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
Keywords
  • Simply typed λ-calculus
  • program metrics
  • approximate program transformations
  • partial metric spaces

Metrics

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

References

  1. S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum. Handbook of Logic in Computer Science: Volume 2. Background: Computational Structures. Handbook of Logic in Computer Science. Clarendon Press, 1992. URL: https://books.google.fr/books?id=zqkXKMNXVi0C.
  2. Mario Alvarez-Picallo and C.-H. Luke Ong. Change actions: models of generalised differentiation. In FOSSACS 2019, volume 11425 of LNCS, pages 45-61, 2019. Google Scholar
  3. Mário S. Alvim, Miguel E. Andrés, Konstantinos Chatzikokolakis, Pierpaolo Degano, and Catuscia Palamidessi. Differential privacy: On the trade-off between utility and information leakage. In Proceedings of the 8th International Conference on Formal Aspects of Security and Trust, FAST-11, pages 39-54, Berlin, Heidelberg, 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-29420-4_3.
  4. A. Arnold and M. Nivat. Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theoretical Computer Science, 11(2):181-205, 1980. URL: https://doi.org/10.1016/0304-3975(80)90045-6.
  5. 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. ACM Press, 2017. URL: https://doi.org/10.1145/3009837.3009890.
  6. Christel Baier and Mila E. Majster-Cederbaum. Denotational semantics in the cpo and metric approach. Theoretical Computer Science, 135(2):171-220, 1994. URL: https://doi.org/10.1016/0304-3975(94)00046-8.
  7. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '12. ACM Press, 2012. URL: https://doi.org/10.1145/2103656.2103670.
  8. Michael Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metric spaces. American Mathematical Monthly - AMER MATH MON, 116:708-718, October 2009. URL: https://doi.org/10.4169/193009709X460831.
  9. Michael A. Bukatin and Joshua S. Scott. Towards computing distances between programs via scott domains. In Sergei Adian and Anil Nerode, editors, Logical Foundations of Computer Science, pages 33-43, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  10. Y. Cai, P.G. Giarrusso, T. Rendel, and K. Ostermann. A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation. ACM SIGPLAN Not., 49:145-155, 2014. Google Scholar
  11. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory, pages 32-46, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. Google Scholar
  12. Maria Manuel Clementino, Dirk Hofmann, and Isar Stubbe. Exponentiable functors between quantaloid-enriched categories. Applied Categorical Structures, 17(1):91-101, 2009. URL: https://doi.org/10.1007/s10485-007-9104-5.
  13. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The affine case. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS '15, page 633?644, USA, 2015. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2015.64.
  14. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The general case. In Hongseok Yang, editor, Programming Languages and Systems, pages 341-367, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. Google Scholar
  15. J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 413-422, July 2002. URL: https://doi.org/10.1109/LICS.2002.1029849.
  16. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled markov processes. Theoretical Computer Science, 318(3):323-354, 2004. URL: https://doi.org/10.1016/j.tcs.2003.09.013.
  17. Pietro Di Gianantonio and Abbas Edalat. A language for differentiable functions. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, pages 337-352, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  18. Abbas Edalat and Martín Hötzel Escardó. Integration in real pcf. Information and Computation, 160(1):128-166, 2000. URL: https://doi.org/10.1006/inco.1999.2844.
  19. Martín Hötzen Escardó. A metric model of PCF. In Workshop on Realizability Semantics and Applications, 1999. Google Scholar
  20. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13. ACM Press, 2013. URL: https://doi.org/10.1145/2429069.2429113.
  21. 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 '18, page 452?461, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209149.
  22. Shafi Goldwasser and Silvio Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28(2):270-299, 1984. URL: https://doi.org/10.1016/0022-0000(84)90070-9.
  23. Jialiang He, Hongliang Lai, and Lili Shen. Towards probabilistic partial metric spaces: Diagonals between distance distributions. Fuzzy Sets and Systems, 370:99-119, 2019. Theme: Topology and Metric Spaces. URL: https://doi.org/10.1016/j.fss.2018.07.011.
  24. Barnaby P. Hilken. Towards a proof theory of rewriting: the simply typed 2λ-calculus. Theoretical Computer Science, 170(1):407-444, 1996. URL: https://doi.org/10.1016/S0304-3975(96)80713-4.
  25. 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
  26. 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
  27. J.M.E. Hyland. The effective topos. In A.S. Troelstra and D. [van Dalen], editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 165-216. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70129-6.
  28. Gunther Jäger and T. M. G. Ahsanullah. Characterization of quantale-valued metric spaces and quantale-valued partial metric spaces by convergence. Applied General Topology, 19(1):129-144, 2018. Google Scholar
  29. Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metrizability in value quantales. Applied General Topology, 5(1):115-127, 2004. Google Scholar
  30. Dexter Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 22(3):328-350, 1981. URL: https://doi.org/10.1016/0022-0000(81)90036-2.
  31. Andreas Krause, Brendan McMahan, Carlos Guestrin, and Anupam Gupta. Robust submodular observation selection. Journal of Machine Learning Research (JMLR), 9:2761-2801, December 2008. Google Scholar
  32. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, pages 111:1-111:14, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.111.
  33. S. G. Matthews. Partial metric topology. Annals of the New York Academy of Sciences, 728(1):183-197, 1994. URL: https://doi.org/10.1111/j.1749-6632.1994.tb44144.x.
  34. Sparsh Mittal. A survey of techniques for approximate computing. ACM Comput. Surv., 48(4), 2016. Google Scholar
  35. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. SIGPLAN Not., 45(9):157-168, September 2010. URL: https://doi.org/10.1145/1932681.1863568.
  36. Bessem Samet, Calogero Vetro, and Francesca Vetro. From metric spaces to partial metric spaces. Fixed Point Theory and Applications, 2013(1):5, 2013. URL: https://doi.org/10.1186/1687-1812-2013-5.
  37. M. P. Schellekens. The correspondence between partial metrics and semivaluations. Theoretical Computer Science, 315(1):135-149, 2004. Google Scholar
  38. Stelios Sidiroglou-Douskos, Sasa Misailovic, Henry Hoffmann, and Martin Rinard. Managing performance vs. accuracy trade-offs with loop perforation. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ESEC/FSE ?11, pages 124-134, New York, NY, USA, 2011. Association for Computing Machinery. Google Scholar
  39. D. A. Simovici. On submodular and supermodular functions on lattices and related structures. In 2014 IEEE 44th International Symposium on Multiple-Valued Logic, pages 202-207, May 2014. URL: https://doi.org/10.1109/ISMVL.2014.43.
  40. Paul Taylor. A lambda calculus for real analysis. Journal of Logic and Analysis, 2(5):1-115, 2010. Google Scholar
  41. Franck van Breugel. An introduction to metric semantics: operational and denotational models for programming and specification languages. Theoretical Computer Science, 258(1):1-98, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00403-5.
  42. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, pages 421-432, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  43. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331(1):115-142, 2005. Automata, Languages and Programming. URL: https://doi.org/10.1016/j.tcs.2004.09.035.
  44. Edwin Westbrook and Swarat Chaudhuri. A semantics for approximate program transformations, 2013. URL: https://arxiv.org/abs/1304.5531.
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 About DROPS Imprint Privacy Contact