Document Open Access Logo

On Doctrines and Cartesian Bicategories

Authors Filippo Bonchi , Alessio Santamaria , Jens Seeber, Paweł Sobociński

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.10.pdf
  • Filesize: 0.83 MB
  • 17 pages

Document Identifiers

Author Details

Filippo Bonchi
  • University of Pisa, Italy
Alessio Santamaria
  • University of Pisa, Italy
Jens Seeber
  • University of Pisa, Italy
Paweł Sobociński
  • Tallinn University of Technology, Estonia

Funding

Filippo Bonchi, Alessio Santamaria: Supported by the Ministero dell’Università e della Ricerca of Italy under Grant No. 201784YSZ5, PRIN2017 – ASPRA.
  • Sobociński, Paweł: Supported by the ESF funded Estonian IT Academy research measure (project 2014-2020.4.05.19-0001) and the Estonian Research Council grant PRG1210.

Acknowledgements

We thank Pino Rosolini and Fabio Pasquali for discussions that improved our understanding of doctrines.

Cite AsGet BibTex

Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On Doctrines and Cartesian Bicategories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.10

Abstract

We study the relationship between cartesian bicategories and a specialisation of Lawvere’s hyperdoctrines, namely elementary existential doctrines. Both provide different ways of abstracting the structural properties of logical systems: the former in algebraic terms based on a string diagrammatic calculus, the latter in universal terms using the fundamental notion of adjoint functor. We prove that these two approaches are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Categorical semantics
Keywords
  • Cartesian bicategories
  • elementary existential doctrines
  • string diagram

Metrics

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

Related Versions

References

  1. John Baez and Jason Erbele. Categories in control. Theory and Application of Categories, 30(24):836-881, 2015. URL: http://www.tac.mta.ca/tac/volumes/30/24/30-24abs.html.
  2. Filippo Bonchi, Joshua Holland, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Diagrammatic algebra: from linear to concurrent systems. Proc. ACM Program. Lang., 3(POPL):25:1-25:28, 2019. URL: https://doi.org/10.1145/3290338.
  3. Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On Doctrines and Cartesian Bicategories. arXiv:2106.08142 [cs, math], June 2021. URL: http://arxiv.org/abs/2106.08142.
  4. Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:23, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.13.
  5. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full Abstraction for Signal Flow Graphs. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 515-526, New York, NY, USA, January 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676993.
  6. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Deconstructing Lawvere with distributive laws. Journal of Logical and Algebraic Methods in Programming, 95:128-146, 2018. URL: https://doi.org/10.1016/j.jlamp.2017.12.002.
  7. Geraldine Brady and Todd Trimble. A string diagram calculus for predicate logic and C. S. Peirce’s system beta. Unpublished, available online at https://ncatlab.org/nlab/files/BradyTrimbleString.pdf, 2000.
  8. Geraldine Brady and Todd H. Trimble. A categorical interpretation of C.S. Peirce’s propositional logic Alpha. Journal of Pure and Applied Algebra, 149(3):213-239, June 2000. URL: https://doi.org/10.1016/S0022-4049(98)00179-0.
  9. Aurelio Carboni and Robert F.C. Walters. Cartesian Bicategories I. Journal of Pure and Applied Algebra, 49(1):11-32, 1987. URL: https://doi.org/10.1016/0022-4049(87)90121-6.
  10. Bob Coecke and Ross Duncan. Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics, 13(4):043016, April 2011. Publisher: IOP Publishing. URL: https://doi.org/10.1088/1367-2630/13/4/043016.
  11. Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński. Functorial semantics for partial theories. In Proceedings of the ACM on Programming Languages, volume 5, pages 57:1-57:28, January 2021. URL: https://doi.org/10.1145/3434338.
  12. Brendan Fong, Paweł Sobociński, and Paolo Rapisarda. A categorical approach to open and interconnected dynamical systems. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 495-504, New York, NY, USA, July 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2934556.
  13. Brendan Fong and David Spivak. String diagrams for regular logic (extended abstract). In John Baez and Bob Coecke, editors, Applied Category Theory 2019, volume 323 of Electronic Proceedings in Theoretical Computer Science, pages 196-229. Open Publishing Association, September 2020. URL: https://doi.org/10.4204/eptcs.323.14.
  14. Brendan Fong and David I Spivak. Graphical regular logic, 2019. URL: http://arxiv.org/abs/1812.05765.
  15. Thomas Fox. Coalgebras and cartesian categories. Communications in Algebra, 4(7):665-667, 1976. URL: https://doi.org/10.1080/00927877608822127.
  16. Peter Freyd and Andre Scedrov. Categories, Allegories, volume 39 of North-Holland Mathematical Library. Elsevier B.V, 1990. URL: https://www.sciencedirect.com/bookseries/north-holland-mathematical-library/vol/39/suppl/C.
  17. Dan R. Ghica and Achim Jung. Categorical semantics of digital circuits. In 2016 Formal Methods in Computer-Aided Design (FMCAD), pages 41-48, October 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886659.
  18. Nathan Haydon and Paweł Sobociński. Compositional Diagrammatic First-Order Logic. In Diagrammatic Representation and Inference, Lecture Notes in Computer Science, 11th International Conference, Diagrams 2020, Tallinn, Estonia,, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-54249-8_32.
  19. Stephen Lack. Composing PROPs. Theory and Application of Categories, 13(9):147-163, 2004. URL: http://www.tac.mta.ca/tac/volumes/13/9/13-09abs.html.
  20. F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50(5):869-872, 1963. Google Scholar
  21. F. William Lawvere. Adjointness in Foundations. Dialectica, 23(3/4):281-296, 1969. Publisher: Wiley. URL: https://doi.org/10.1111/j.1746-8361.1969.tb01194.x.
  22. F. William Lawvere. Diagonal arguments and cartesian closed categories. In Category Theory, Homology Theory and their Applications II, Lecture Notes in Mathematics, pages 134-145, Berlin, Heidelberg, 1969. Springer. URL: https://doi.org/10.1007/BFb0080769.
  23. F. William Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Alex Heller, editor, Applications of Categorical Algebra, volume 17, pages 1-14, New York, NY, 1970. American Mathematical Society. URL: https://doi.org/10.1090/pspum/017.
  24. Saunders MacLane. Categorical algebra. Bulletin of the American Mathematical Society, 71(1):40-106, 1965. URL: https://doi.org/10.1090/S0002-9904-1965-11234-4.
  25. Maria Emilia Maietti, Fabio Pasquali, and Giuseppe Rosolini. Triposes, exact completions, and Hilbert’s ε-operator. Tbilisi Mathematical Journal, 10(3):141-166, June 2017. Publisher: Tbilisi Centre for Mathematical Sciences. URL: https://doi.org/10.1515/tmj-2017-0106.
  26. Maria Emilia Maietti and Giuseppe Rosolini. Quotient Completion for the Foundation of Constructive Mathematics. Logica Universalis, 7(3):371-402, September 2013. URL: https://doi.org/10.1007/s11787-013-0080-2.
  27. Maria Emilia Maietti and Giuseppe Rosolini. Unifying Exact Completions. Applied Categorical Structures, 23(1):43-52, February 2015. URL: https://doi.org/10.1007/s10485-013-9360-5.
  28. Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica. The geometry of computation-graph abstraction. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 749-758. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209127.
  29. Evan Patterson. Knowledge representation in bicategories of relations, 2017. URL: http://arxiv.org/abs/1706.00526.
  30. Robin Piedeleu and Fabio Zanasi. A String Diagrammatic Axiomatisation of Finite-State Automata. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, pages 469-489, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-71995-1_24.
  31. Ahti-Veikko Pietarinen. The Logic of the Future, volume 1. De Gruyter, 2019. Google Scholar
  32. Jens Seeber. Logical completeness for string diagrams. PhD thesis, IMT Lucca, 2020. Google Scholar
  33. P. Selinger. A Survey of Graphical Languages for Monoidal Categories. In B. Coecke, editor, New Structures for Physics, volume 813 of Lecture Notes in Physics, pages 289-355. Springer, Berlin, Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
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