Document Open Access Logo

Quotients and Extensionality in Relational Doctrines

Authors Francesco Dagnino , Fabio Pasquali

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.25.pdf
  • Filesize: 0.96 MB
  • 23 pages

Document Identifiers

Author Details

Francesco Dagnino
  • DIBRIS, University of Genova, Italy
Fabio Pasquali
  • DIMA, University of Genova, Italy

Acknowledgements

We are grateful to the anonymous referees for their many useful comments. They have been very helpful in improving the paper.

Cite AsGet BibTex

Francesco Dagnino and Fabio Pasquali. Quotients and Extensionality in Relational Doctrines. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 25:1-25:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.25

Abstract

Taking a quotient roughly means changing the notion of equality on a given object, set or type. In a quantitative setting, equality naturally generalises to a distance, measuring how much elements are similar instead of just stating their equivalence. Hence, quotients can be understood quantitatively as a change of distance. Quotients are crucial in many constructions both in mathematics and computer science and have been widely studied using categorical tools. Among them, Lawvere’s doctrines stand out, providing a fairly simple functorial framework capable to unify many notions of quotient and related constructions. However, abstracting usual predicate logics, they cannot easily deal with quantitative settings. In this paper, we show how, combining doctrines and the calculus of relations, one can unify quantitative and usual quotients in a common picture. More in detail, we introduce relational doctrines as a functorial description of (the core of) the calculus of relations. Then, we define quotients and a universal construction adding them to any relational doctrine, generalising the quotient completion of existential elementary doctrine and also recovering many quantitative examples. This construction deals with an intensional notion of quotient and breaks extensional equality of morphisms. Then, we describe another construction forcing extensionality, showing how it abstracts several notions of separation in metric and topological structures.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Categorical semantics
Keywords
  • Quantitative Reasoning
  • Calculus of Relations
  • Hyperdoctrines
  • Metric Spaces

Metrics

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

References

  1. Jirí Adámek. Varieties of quantitative algebras and their monads. In Christel Baier and Dana Fisman, editors, Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022, pages 9:1-9:10. ACM, 2022. URL: https://doi.org/10.1145/3531130.3532405.
  2. Jiří Adámek, Matěj Dostál, and Jiří Velebil. Quantitative algebras and a classification of metric monads, 2023. URL: https://arxiv.org/abs/2210.01565.
  3. Hajnal Andréka, Steven Givant, Peter Jipsen, and Istvan Németi. On tarski’s axiomatic foundations of the calculus of relations. The Journal of Symbolic Logic, 82(3):966-994, 2017. Google Scholar
  4. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. An algebraic theory of markov processes. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 679-688. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209177.
  5. 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.
  6. Michael Barr. Relational algebras. In S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski, editors, Reports of the Midwest Category Seminar IV, pages 39-55, Berlin, Heidelberg, 1970. Springer Berlin Heidelberg. Google Scholar
  7. Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. Journal of Functional Programming, 13(2):261-293, 2003. URL: https://doi.org/10.1017/S0956796802004501.
  8. Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. Programming language techniques for differential privacy. ACM SIGLOG News, 3(1):34-53, 2016. URL: https://doi.org/10.1145/2893582.2893591.
  9. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. ACM Transactions on Programming Languages and Systems, 35(3):9:1-9:49, 2013. URL: https://doi.org/10.1145/2492061.
  10. Renato Betti and John Power. On local adjointness of distributive bicategories. Bollettino della Unione Matematica Italiana, 2(4):931-947, 1988. Google Scholar
  11. E. Bishop. Foundations of Constructive Analysis. McGraw-Hill series in higher mathematics. McGraw-Hill, 1967. Google Scholar
  12. E. Bishop and D. Bridges. Constructive Analysis. Grundlehren der mathematischen Wissenschaften. Springer Berlin Heidelberg, 2012. Google Scholar
  13. Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Pawel Sobocinski. On doctrines and cartesian bicategories. In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, volume 211 of LIPIcs, pages 10:1-10:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.10.
  14. A. Carboni and R. Celia Magno. The free exact category on a left exact one. Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics, 33:295-301, 1982. Google Scholar
  15. Aurelio Carboni and E.M. Vitale. Regular and exact completions. Journal of Pure and Applied Algebra, 125:79-117, 1998. Google Scholar
  16. Aurelio Carboni and Rober Walters. Cartesian bicategories I. Journal of Pure and Applied Algebra, 49(1-2):11-32, 1987. Google Scholar
  17. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 32-46. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_4.
  18. Francesco Dagnino and Fabio Pasquali. Logical foundations of quantitative equality. In Christel Baier and Dana Fisman, editors, Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022, pages 16:1-16:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533337.
  19. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proceedings of the ACM on Programming Languages, 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498692.
  20. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, 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.
  21. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 545-556. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009890.
  22. 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.
  23. Thomas M. Fiore, Nicola Gambino, and Joachim Kock. Monads in double categories. Journal of Pure and Applied Algebra, 215(6):1174-1197, 2011. URL: https://doi.org/10.1016/j.jpaa.2010.08.003.
  24. Jonas Frey. Triposes, q-toposes and toposes. Annals of Pure and Applied Logic, 166(2):232-259, 2015. URL: https://doi.org/10.1016/j.apal.2014.10.005.
  25. Peter J. Freyd and Andre Scedrov. Categories, allegories, volume 39 of North-Holland mathematical library. North-Holland, 1990. Google Scholar
  26. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 452-461. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209149.
  27. Francesco Gavazzo and Cecilia Di Florio. Elements of quantitative rewriting. Proceedings of the ACM on Programming Languages, 7(POPL):1832-1863, 2023. URL: https://doi.org/10.1145/3571256.
  28. Steven Givant. The calculus of relations as a foundation for mathematics. Journal of Automated Reasoning, 37(4):277-322, 2006. URL: https://doi.org/10.1007/s10817-006-9062-x.
  29. Dirk Hofmann, Gavin J Seal, and Walter Tholen. Monoidal Topology: A Categorical Approach to Order, Metric, and Topology, volume 153. Cambridge University Press, 2014. Google Scholar
  30. Martin. Hofmann. Extensional constructs in intensional type theory. CPHC/BCS Distinguished Dissertations. Springer-Verlag London Ltd., London, 1997. Google Scholar
  31. Bart P. F. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics. North-Holland, 2001. URL: http://www.elsevierdirect.com/product.jsp?isbn=9780444508539.
  32. Alexander Kurz and Jiri Velebil. Relation lifting, a survey. J. Log. Algebraic Methods Program., 85(4):475-499, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.08.002.
  33. Stephen Lack. A 2-Categories Companion, pages 105-191. Springer New York, New York, NY, 2010. URL: https://doi.org/10.1007/978-1-4419-1524-5_4.
  34. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 301-310. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.36.
  35. Joachim Lambek. Diagram chasing in ordered categories with involution. Journal of Pure and Applied Algebra, 143(1):293-307, 1999. URL: https://doi.org/10.1016/S0022-4049(98)00115-7.
  36. F. Wiliam Lawvere. Adjointness in foundations. Dialectica, 23:281-296, 1969. also available as Repr. Theory Appl. Categ., 16 (2006) 1-16. URL: https://doi.org/10.1111/j.1746-8361.1969.tb01194.x.
  37. F. William Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller, editor, Proceedings of the New York Symposium on Application of Categorical Algebra, pages 1-14. American Mathematical Society, 1970. Google Scholar
  38. F. William Lawvere. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano, 43:135-166, 1973. Google Scholar
  39. F.W. Lawvere. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano, 43:135-166, 1973. Google Scholar
  40. Maria Emilia Maietti, Fabio Pasquali, and Giuseppe Rosolini. Triposes, exact completions, and Hilbert’s epsilon-operator. Tbilisi Mathematical Journal, 10(3):141-166, 2017. URL: https://doi.org/10.1515/tmj-2017-0106.
  41. Maria Emilia Maietti and Giuseppe Rosolini. Elementary quotient completion. Theory Appl. Categ., 27(17):445-463, 2013. Google Scholar
  42. Maria Emilia Maietti and Giuseppe Rosolini. Quotient completion for the foundation of constructive mathematics. Logica Universalis, 7(3):371-402, 2013. URL: https://doi.org/10.1007/s11787-013-0080-2.
  43. Maria Emilia Maietti and Giuseppe Rosolini. Unifying exact completions. Appl. Categorical Struct., 23(1):43-52, 2015. URL: https://doi.org/10.1007/s10485-013-9360-5.
  44. M.E. Maietti and G. Rosolini. Relating quotient completions via categorical logic. In Dieter Probst and Peter Schuster (eds.), editors, Concepts of Proof in Mathematics, Philosophy, and Computer Science, pages 229-250. De Gruyter, 2016. Google Scholar
  45. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  46. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. On the axiomatizability of quantitative algebras. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005102.
  47. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Fixed-points for quantitative equational logics. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470662.
  48. C.-H. Luke Ong. Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005064.
  49. Charles S. Peirce. The logic of relatives. The Monist, 7(2):161-217, 1897. Google Scholar
  50. Andrew M. Pitts. Categorical logic. In Handbook of logic in computer science, Vol. 5, volume 5 of Handbook of Logic in Computer Science, pages 39-128. Oxford Univ. Press, New York, 2000. Google Scholar
  51. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Paul Hudak and Stephanie Weirich, editors, Proceedings of the 15th ACM International Conference on Functional programming, ICFP 2010, pages 157-168. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863568.
  52. D.S. Scott. A new category? Domains, spaces and equivalence relations. Available at http://www.cs.cmu.edu/Groups/LTC/, 1996. Google Scholar
  53. R. Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. URL: https://doi.org/10.1016/0022-4049(72)90019-9.
  54. A. Tarski and S.R. Givant. A Formalization of Set Theory Without Variables. Number v. 41 in A formalization of set theory without variables. American Mathematical Soc., 1988. Google Scholar
  55. Alfred Tarski. On the calculus of relations. Journal of Symbolic Logic, 6(3):73-89, 1941. URL: https://doi.org/10.2307/2268577.
  56. Albert Thijs. Simulations and fixpoint semantics. PhD thesis, Rijksuniversiteit Groningen, 1996. Google Scholar
  57. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331(1):115-142, 2005. URL: https://doi.org/10.1016/j.tcs.2004.09.035.
  58. Jaap van Oosten. Realizability: An Introduction to its Categorical Side, volume 152 of Studies in Logic and the Foundations of Mathematics. North Holland Publishing Company, 2008. Google Scholar
  59. Lili Xu, Konstantinos Chatzikokolakis, and Huimin Lin. Metrics for differential privacy in concurrent systems. In Erika Ábrahám and Catuscia Palamidessi, editors, Formal Techniques for Distributed Objects, Components, and Systems - 34th IFIP WG 6.1 International Conference, FORTE 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014. Proceedings, volume 8461 of Lecture Notes in Computer Science, pages 199-215. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43613-4_13.
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