Document Open Access Logo

String Diagrams for Non-Strict Monoidal Categories

Authors Paul Wilson , Dan Ghica, Fabio Zanasi

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.37.pdf
  • Filesize: 0.82 MB
  • 19 pages

Document Identifiers

Author Details

Paul Wilson
  • University of Southampton, UK
Dan Ghica
  • University of Birmingham, UK
Fabio Zanasi
  • University College London, UK

Cite As Get BibTex

Paul Wilson, Dan Ghica, and Fabio Zanasi. String Diagrams for Non-Strict Monoidal Categories. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.37

Abstract

Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we provide a presentation by generators and relations of string diagrams for non-strict monoidal categories, and show how this construction can handle applications in domains such as digital circuits and programming languages. We prove the correctness of our construction, which yields a novel proof of Mac Lane’s strictness theorem. This in turn leads to an elementary graphical proof of Mac Lane’s coherence theorem, and in particular allows for the inductive construction of the canonical isomorphisms in a monoidal category.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • String Diagrams
  • Strictness
  • Coherence

Metrics

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

Related Versions

References

  1. Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi. Functorial string diagrams for reverse-mode automatic differentiation. CoRR, abs/2107.13433, 2021. URL: http://arxiv.org/abs/2107.13433.
  2. John C. Baez and Brendan Fong. A compositional framework for passive linear networks. Theory and Applications of Categories, 33(38):1158-1222, 2018. URL: https://doi.org/10.48550/arXiv.1504.05625.
  3. R.F. Blute, J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble. Natural deduction and coherence for weakly distributive categories. Journal of Pure and Applied Algebra, 113(3):229-296, 1996. URL: https://doi.org/10.1016/0022-4049(95)00159-X.
  4. Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Graphical affine algebra. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, June 2019. URL: https://doi.org/10.1109/lics.2019.8785877.
  5. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 515-526. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676993.
  6. Titouan Carette, Yohann DquotesingleAnello, and Simon Perdrix. Quantum algorithms and oracles with the scalable ZX-calculus. Electronic Proceedings in Theoretical Computer Science, 343:193-209, September 2021. URL: https://doi.org/10.4204/eptcs.343.10.
  7. Vikraman Choudhury, Jacek Karwowski, and Amr Sabry. Symmetries in reversible programming: From symmetric rig groupoids to reversible programming languages, 2021. URL: https://doi.org/10.48550/arXiv.2110.05404.
  8. Bob Coecke, Edward Grefenstette, and Mehrnoosh Sadrzadeh. Lambek vs. lambek: Functorial vector space semantics and string diagrams for lambek calculus. Ann. Pure Appl. Log., 164(11):1079-1100, 2013. URL: https://doi.org/10.1016/j.apal.2013.05.009.
  9. Bob Coecke and Aleks Kissinger. Picturing quantum processes: A first course in quantum theory and diagrammatic reasoning. Cambridge University Press, 2017. Google Scholar
  10. P. I. Etingof, Shlomo Gelaki, Dmitri Nikshych, and Victor Ostrik, editors. Tensor categories. Number volume 205 in Mathematical surveys and monographs. American Mathematical Society, 2015. URL: https://klein.mit.edu/~etingof/egnobookfinal.pdf.
  11. Dan R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 363-375. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190269.
  12. Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic semantics for digital circuits. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.24.
  13. Dan R. Ghica, George Kaye, and David Sprunger. Full abstraction for digital circuits, 2022. URL: https://doi.org/10.48550/arXiv.2201.10456.
  14. Peter Hines. Coherence and strictification for self-similarity, 2015. URL: http://arxiv.org/abs/1304.5954.
  15. A. Joyal and R. Street. Braided tensor categories. Advances in Mathematics, 102(1):20-78, 1993. URL: https://doi.org/10.1006/aima.1993.1055.
  16. André Joyal and Ross Street. The geometry of tensor calculus, i. Advances in Mathematics, 88(1):55-112, 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
  17. Yves Lafont. Towards an algebraic theory of Boolean circuits. Journal of Pure and Applied Algebra, 184(2-3):257-310, November 2003. URL: https://doi.org/10.1016/S0022-4049(03)00069-0.
  18. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1997. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  19. Paul-André Melliès. Functorial boxes in string diagrams. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 1-30. Springer, 2006. URL: https://doi.org/10.1007/11874683_1.
  20. Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010. URL: http://arxiv.org/abs/0908.3347.
  21. Michael Shulman. A practical type theory for symmetric monoidal categories, 2019. URL: https://doi.org/10.48550/arXiv.1911.00818.
  22. Stuart Sutherland, Simon Davidmann, and Peter Flake. SystemVerilog for Design Second Edition: A Guide to Using SystemVerilog for Hardware Design and Modeling. Springer Science & Business Media, 2006. Google Scholar
  23. Paul Wilson, Dan Ghica, and Fabio Zanasi. String diagrams for non-strict monoidal categories, 2022. URL: https://doi.org/10.48550/arXiv.2201.11738.
  24. Paul Wilson and Fabio Zanasi. The cost of compositionality: A high-performance implementation of string diagram composition, 2021. URL: http://arxiv.org/abs/2105.09257.
  25. Paul Wilson and Fabio Zanasi. Categories of differentiable polynomial circuits for machine learning, 2022. URL: https://doi.org/10.48550/arXiv.2203.06430.
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