An Internal Language for Categories Enriched over Generalised Metric Spaces
Document Open Access Logo

An Internal Language for Categories Enriched over Generalised Metric Spaces

Authors Fredrik Dahlqvist, Renato Neves

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.16.pdf
  • Filesize: 0.77 MB
  • 18 pages

Document Identifiers

Author Details

Fredrik Dahlqvist
  • University College London, UK
Renato Neves
  • University of Minho, Braga, Portugal
  • INESC-TEC, Porto, Portugal

Funding

This work was financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-030947. This work was also financed by the UK Research Institute in Verified Trustworthy Software Systems, via project "Quantitative Algebraic Reasoning for Hybrid Programs", and by the Leverhulme Project Grant "Verification of Machine Learning Algorithms".

Acknowledgements

The authors are very grateful for the reviewer’s incisive feedback.

Cite As Get BibTex

Fredrik Dahlqvist and Renato Neves. An Internal Language for Categories Enriched over Generalised Metric Spaces. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.16

Abstract

Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale 𝒱, which covers the cases of (in)equations and (ultra)metric equations among others.
Our main result is the introduction of a 𝒱-equational deductive system for linear λ-calculus together with a proof that it is sound and complete (in fact, an internal language) for a class of enriched autonomous categories. In the case of inequations, we get an internal language for autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an internal language for autonomous categories enriched over (ultra)metric spaces.
We use our results to obtain examples of inequational and metric equational systems for higher-order programs that contain real-time and probabilistic behaviour.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • λ-calculus
  • enriched category theory
  • quantale
  • equational theory

Metrics

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

Related Versions

References

  1. Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G Riecke. A core calculus of dependency. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 147-160, 1999. Google Scholar
  2. Jiří Adámek, Chase Ford, Stefan Milius, and Lutz Schröder. Finitary monads on the category of posets, 2020. URL: http://arxiv.org/abs/2011.14796.
  3. Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic, pages 121-135. Springer, 1994. Google Scholar
  4. Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. Term assignment for intuitionistic linear logic (preliminary report). Citeseer, 1992. Google Scholar
  5. Lars Birkedal, Jan Schwinghammer, and Kristian Støvring. A metric model of lambda calculus with guarded recursion. In FICS, pages 19-25, 2010. Google Scholar
  6. Francis Borceux. Handbook of categorical algebra, volume 2 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994. Google Scholar
  7. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The affine case. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 633-644. IEEE, 2015. Google Scholar
  8. Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning About lambda-Terms: The General Case. In European Symposium on Programming, pages 341-367. Springer, 2017. Google Scholar
  9. Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. In Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'20), pages 57:1-29, New Orleans, January 2020. ACM. Google Scholar
  10. Fredrik Dahlqvist and Renato Neves. An internal language for categories enriched over generalised metric spaces, 2021. URL: http://arxiv.org/abs/2105.08473.
  11. Valeria De Paiva. Lineales: algebraic models of linear logic from a categorical perspective. In Proceedings of LLC8, 1999. Google Scholar
  12. Klaus Denecke, Marcel Erné, and Shelly L Wismath. Galois connections and applications, volume 565. Springer Science & Business Media, 2013. Google Scholar
  13. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. ACM SIGPLAN Notices, 51(9):476-489, 2016. Google Scholar
  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, pages 452-461, 2018. Google Scholar
  15. Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott. Continuous lattices and domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 2003. Google Scholar
  16. Jean-Yves Girard, Andre Scedrov, and Philip J Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical computer science, 97(1):1-66, 1992. Google Scholar
  17. Jean Goubault-Larrecq. Non-Hausdorff Topology and Domain Theory - Selected Topics in Point-Set Topology, volume 22 of New Mathematical Monographs. Cambridge University Press, March 2013. Google Scholar
  18. Dirk Hofmann and Pedro Nora. Hausdorff coalgebras. Applied Categorical Structures, 28(5):773-806, 2020. Google Scholar
  19. Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. Quantitative robustness analysis of quantum programs. Proceedings of the ACM on Programming Languages, 3(POPL):1-29, 2019. Google Scholar
  20. Gregory Maxwell Kelly. Basic concepts of enriched category theory, volume 64. CUP Archive, 1982. Google Scholar
  21. Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, June 1981. URL: https://doi.org/10.1016/0022-0000(81)90036-2.
  22. Neelakantan R Krishnaswami and Nick Benton. Ultrametric semantics of reactive programs. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pages 257-266. IEEE, 2011. Google Scholar
  23. Alexander Kurz and Jiří Velebil. Quasivarieties and varieties of ordered algebras: regularity and exactness. Mathematical Structures in Computer Science, 27(7):1153-1194, 2017. Google Scholar
  24. Joachim Lambek and Philip J Scott. Introduction to higher-order categorical logic, volume 7. Cambridge University Press, 1988. Google Scholar
  25. F William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del seminario matématico e fisico di Milano, 43(1):135-166, 1973. Google Scholar
  26. Fred E. J. Linton. Some aspects of equational categories. In Proceedings of the Conference on Categorical Algebra, pages 84-94. Springer, 1966. Google Scholar
  27. Saunders Mac Lane. Categories for the working mathematician, volume 5. springer, 1998. Google Scholar
  28. Ian Mackie, Leopoldo Román, and Samson Abramsky. An internal language for autonomous categories. Applied Categorical Structures, 1(3):311-343, 1993. Google Scholar
  29. Maria Emilia Maietti, Paola Maneggia, Valeria De Paiva, and Eike Ritter. Relating categorical semantics for intuitionistic linear logic. Applied categorical structures, 13(1):1-36, 2005. Google Scholar
  30. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 700-709, 2016. Google Scholar
  31. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. On the axiomatizability of quantitative algebras. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. Google Scholar
  32. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages, 3(ICFP):1-30, 2019. Google Scholar
  33. Jan Paseka and Jiří Rosickỳ. Quantales. In Current research in operational quantum logic, pages 245-262. Springer, 2000. Google Scholar
  34. 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, 2021. Google Scholar
  35. 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, pages 157-168, 2010. Google Scholar
  36. Jiří Rosickỳ. Metric monads, 2020. URL: http://arxiv.org/abs/2012.14641.
  37. Michael Shulman. A practical type theory for symmetric monoidal categories. arXiv preprint, 2019. URL: http://arxiv.org/abs/1911.00818.
  38. Isar Stubbe. An introduction to quantaloid-enriched categories. Fuzzy Sets and Systems, 256:95-116, 2014. Google Scholar
  39. Jiří Velebil, Alexander Kurz, and Adriana Balan. Extending set functors to generalised metric spaces. Logical Methods in Computer Science, 15, 2019. 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 About DROPS Imprint Privacy Contact