Document Open Access Logo

On Quantitative Algebraic Higher-Order Theories

Authors Ugo Dal Lago, Furio Honsell, Marina Lenisa, Paolo Pistone

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.4.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Author Details

Ugo Dal Lago
  • Department of Computer Science and Engineering, University of Bologna, Italy
Furio Honsell
  • Department of Mathematical Sciences, Informatics and Physics, University of Udine, Italy
Marina Lenisa
  • Department of Mathematical Sciences, Informatics and Physics, University of Udine, Italy
Paolo Pistone
  • Department of Computer Science and Engineering, University of Bologna, Italy

Funding

Ugo Dal Lago’s and Paolo Pistone’s work was funded by ERC CoG 818616.

Cite As Get BibTex

Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.4

Abstract

We explore the possibility of extending Mardare et al.’s quantitative algebras to the structures which naturally emerge from Combinatory Logic and the λ-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results clearly delineating to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Theory of computation → Type theory
Keywords
  • Quantitative Algebras
  • Lambda Calculus
  • Combinatory Logic
  • Metric Spaces

Metrics

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

Related Versions

References

  1. Samson Abramsky, Esfandiar Haghverdi, and Philip J. Scott. Geometry of interaction and linear combinatory algebras. Math. Struct. Comput. Sci., 12(5):625-665, 2002. URL: https://doi.org/10.1017/S0960129502003730.
  2. André Arnold and Maurice Nivat. Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theor. Comput. Sci., 11:181-205, 1980. URL: https://doi.org/10.1016/0304-3975(80)90045-6.
  3. 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.
  4. Christel Baier and Mila E. Majster-Cederbaum. Denotational semantics in the CPO and metric approach. Theor. Comput. Sci., 135(2):171-220, 1994. URL: https://doi.org/10.1016/0304-3975(94)00046-8.
  5. Henk Barendregt. Lambda calculus, its syntax and semantics. North-Holland, 1985. URL: https://doi.org/10.2307/2274112.
  6. Henk Barendregt, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum. Lambda calculi with types. In Handbook of Logic in Computer Science, pages 117-309. Oxford University Press, 1992. Google Scholar
  7. Henk Barendregt, Wil Dekkers, and Statman Richard. Lambda calculus with Types. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139032636.
  8. Garrett Birkhoff. On the structure of abstract algebras. Mathematical Proceedings of the Cambridge Philosophical Society, 31(4):433-454, 1935. URL: https://doi.org/10.1017/S0305004100013463.
  9. Michael Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metric spaces. The American Mathematical Monthly, 116(8):708-718, 2009. URL: https://doi.org/10.4169/193009709X460831.
  10. Michael A. Bukatin and Joshua S. Scott. Towards computing distances between programs via scott domains. In Proc. of LFCS 1997, volume 1234 of LNCS, pages 33-43. Springer, 1997. URL: https://doi.org/10.1007/3-540-63045-7_4.
  11. 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.
  12. Davide Castelnovo and Marino Miculan. Fuzzy algebraic theories. In Proc. of CSL 2022, pages 13:1-13:17, Germany, 2022. LIPIcs. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.13.
  13. Maria Manuel Clementino and Dirk Hofmann. Exponentiation in V-categories. Topology and its Applications, 153(16):3113-3128, 2006. URL: https://doi.org/10.1016/j.topol.2005.01.038.
  14. 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.1201/9781498710404-10.
  15. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The general case. In Proc. of ESOP 2017, volume 10201 of LNCS, pages 341-367, Berlin, Heidelberg, 2017. Springer. URL: https://doi.org/10.1007/978-3-662-54434-1_13.
  16. Fredrik Dahlqvist and Renato Neves. An internal language for categories enriched over generalised metric spaces. In Proc. of CSL 2022, pages 13:1-13:17, Germany, 2022. LIPIcs. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.16.
  17. 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, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.111.
  18. Jaco de Bakker and Erik de Vink. Control Flow Semantics. MIT Press, Cambridge, MA, USA, 1996. Google Scholar
  19. Jaco de Bakker and John-Jules Charles Meyer. Metric semantics for concurrency. In Jaco de Bakker and Jan Rutten, editors, Ten Years of Concurrency Semantics: Selected Papers of the Amsterdam Concurrency Group, pages 104-130. World Scientific, Singapore, 1992. Google Scholar
  20. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  21. Martín Hötzen Escardó. A metric model of PCF. Unpublished note presented at the Workshop on Realizability Semantics and Applications, June 1999. Available at the author’s webpage., 1999. Google Scholar
  22. Raphael Espínola and Mohamed Amine Khamsi. Introduction to hyperconvex spaces. In Handbook of Metric Fixed Point Theory, pages 391-435. Springer Netherlands, Dordrecht, 2001. URL: https://doi.org/10.1007/978-94-017-1748-9_13.
  23. Jean-Yves Girard. Towards a geometry of interaction. Contemporary Mathematics, 92, 1989. Google Scholar
  24. Joseph A. Goguen and José Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307-334, 1985. URL: https://doi.org/10.1145/947864.947865.
  25. 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
  26. U. Höhle. M-valued sets and sheaves over integral commutative cl-monoids. In Stephen Ernest Rodabaugh, Erich Peter Klement, and Ulrich Höhle, editors, Applications of Category Theory to Fuzzy Subsets, pages 33-72. Springer Netherlands, 1992. URL: https://doi.org/10.1007/978-94-011-2616-8_3.
  27. Jonathan Katz and Yehuda Lindell. Introduction to Modern Cryptography. Chapman & Hall, 2nd edition, 2014. Google Scholar
  28. Robert Kelly, Barak A. Pearlmutter, and Jeffrey Mark Sisking. Evolving the incremental λ-calculus into a model of forward automatic differentiation (AD). ArXiv https://arxiv.org/abs/1611.03429, 2016.
  29. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proc. of LICS 2016. IEEE Computer Society, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  30. Simone Martini. Categorical models for non-extensional λ-calculi and combinatory logic. Math. Struct. Comput. Sci., 2(3):327-357, 1992. URL: https://doi.org/10.1017/S096012950000150X.
  31. Sparsh Mittal. A survey of techniques for approximate computing. ACM Comput. Surv., 48(4), 2016. URL: https://doi.org/10.1145/2893356.
  32. Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In Proc. of LICS 2021. IEEE Computer Society, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470696.
  33. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger. Proc. of ICFP 2010, pages 157-168, 2010. URL: https://doi.org/10.1145/1863543.1863568.
  34. 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.
  35. Franck van Breugel. An introduction to metric semantics: operational and denotational models for programming and specification languages. Theor. Comput. Sci., 258(1):1-98, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00403-5.
  36. Lofti A. Zadeh. Quantitative fuzzy semantics. Inf. Sci., 3(2):159-176, 1971. URL: https://doi.org/10.1016/S0020-0255(71)80004-X.
  37. Lofti A. Zadeh. Similarity relations and fuzzy orderings. Inf. Sci., 3(2):177-200, 1971. URL: https://doi.org/10.1016/S0020-0255(71)80005-1.
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