Document Open Access Logo

String Diagrams for Closed Symmetric Monoidal Categories

Authors Callum Reader , Alessandro Di Giorgio

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.12.pdf
  • Filesize: 2.73 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Categorical semantics
Keywords
  • diagrammatic languages
  • logic
  • lambda calculi

Metrics

Abstract

We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.

Cite As Get BibTex

Callum Reader and Alessandro Di Giorgio. String Diagrams for Closed Symmetric Monoidal Categories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.12

Author Details

Callum Reader
  • Tallinn University of Technology, Estonia
Alessandro Di Giorgio
  • Tallinn University of Technology, Estonia

Funding

  • Reader, Callum: Supported by the Estonian Research Council under Grant PSG764.
  • Di Giorgio, Alessandro: Supported by the European Union under Grant No. 101087529.

Acknowledgements

We would like to acknowledge Matt Earnshaw, Alkis Ioannidis, Mario Roman, Pawel Sobocinski and Simon Willerton for several helpful discussions. We are also grateful to the anonymous reviewers of CSL '26 for their insightful comments and feedback.

References

  1. Samson Abramsky and Bob Coecke. A categorical semantics of quantum protocols. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 415-425, 2004. URL: https://doi.org/10.1109/LICS.2004.1319636.
  2. Matteo Acclavio. Proof diagrams for multiplicative linear logic: Syntax and semantics. Journal of Automated Reasoning, 63(4):911-939, 2019. URL: https://doi.org/10.1007/S10817-018-9466-4.
  3. Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi. Rewriting for monoidal closed categories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs, pages 29:1-29:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.29.
  4. John C. Baez and Mike Stay. Physics, topology, logic and computation: A rosetta stone. Lecture Notes in Physics, 813:95-174, 2011. Google Scholar
  5. Justin Barhite. Bicategorical traces and cotraces, 2024. URL: https://arxiv.org/abs/2307.13070.
  6. Richard F Blute, J Robin B Cockett, Robert AG Seely, and Todd H Trimble. Natural deduction and coherence for weakly distributive categories. Journal of Pure and Applied Algebra, 113(3):229-296, 1996. Google Scholar
  7. Guillaume Boisseau and Pawel Sobocinski. String diagrammatic electrical circuit theory. In Kohei Kishida, editor, Proceedings of the Fourth International Conference on Applied Category Theory, ACT 2021, Cambridge, United Kingdom, 12-16th July 2021, volume 372 of EPTCS, pages 178-191, 2021. URL: https://doi.org/10.4204/EPTCS.372.13.
  8. Filippo Bonchi, Alessandro Di Giorgio, and Elena Di Lavore. A diagrammatic algebra for program logics. In International Conference on Foundations of Software Science and Computation Structures, pages 308-330. Springer Nature Switzerland Cham, 2025. URL: https://doi.org/10.1007/978-3-031-90897-2_15.
  9. Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawel Sobocinski. Diagrammatic algebra of first order logic. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1-15, 2024. URL: https://doi.org/10.1145/3661814.3662078.
  10. Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria. Deconstructing the calculus of relations with tape diagrams. Proceedings of the ACM on Programming Languages, 7(POPL):1864-1894, 2023. URL: https://doi.org/10.1145/3571257.
  11. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: rewriting with frobenius structure. J. ACM, 69(2):14:1-14:58, 2022. URL: https://doi.org/10.1145/3502719.
  12. 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 für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.13.
  13. Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. A categorical semantics of signal flow graphs. In Proceedings of the 25th International Conference on Concurrency Theory (CONCUR), pages 435-450. Springer, 2014. Google Scholar
  14. Pierre Clairambault and Simon Forest. The cartesian closed bicategory of thin spans of groupoids. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175754.
  15. J Robin B Cockett and Robert AG Seely. Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. Theory and Applications of categories, 3(5):85-131, 1997. Google Scholar
  16. Bob Coecke and Aleks Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. URL: https://doi.org/10.1017/9781316219317.
  17. Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories. arXiv preprint, 2020. URL: https://arxiv.org/abs/2010.13361.
  18. Kosta Dosen and Zoran Petrić. Proof-Net Categories. Polimetrica sas, 2007. Google Scholar
  19. Samuel Eilenberg and Norman Steenrod. Foundations of algebraic topology. Princeton University Press, 2015. Google Scholar
  20. Marcelo Fiore, Zeinab Galal, and Hugo Paquet. Stabilized profunctors and stable species of structures. Logical Methods in Computer Science, 20, 2024. URL: https://doi.org/10.46298/LMCS-20(1:17)2024.
  21. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77(1):203-220, 2008. Google Scholar
  22. Thomas Fox. Coalgebras and cartesian categories. Communications in Algebra, 4(7):665-667, 1976. URL: https://doi.org/10.1080/00927877608822127.
  23. Peter J Freyd and David N Yetter. Braided compact closed categories with applications to low dimensional topology. Advances in mathematics, 77(2):156-182, 1989. Google Scholar
  24. Ella Gale, Leo Lobski, and Fabio Zanasi. A categorical approach to synthetic chemistry. In International Colloquium on Theoretical Aspects of Computing, pages 276-294. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-47963-2_17.
  25. Richard Garner, Tom Hirschowitz, and Aurélien Pardon. Graphical presentations of symmetric monoidal closed theories. arXiv preprint arXiv:0810.4420, 2008. URL: https://arxiv.org/abs/0810.4420.
  26. Richard Garner, Tom Hirschowitz, and Aurélien Pardon. Variable binding, symmetric monoidal closed theories, and bigraphs. In International Conference on Concurrency Theory, pages 321-337. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_22.
  27. Dan Ghica and Fabio Zanasi. String diagrams for λ-calculi and functional computation. arXiv preprint, 2023. URL: https://arxiv.org/abs/2305.18945.
  28. Dan R. Ghica and Achim Jung. Categorical semantics of digital circuits. In 2016 Formal Methods in Computer-Aided Design (FMCAD), pages 41-48, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886659.
  29. Dominic JD Hughes. Simple free star-autonomous categories and full coherence. Journal of Pure and Applied Algebra, 216(11):2386-2410, 2012. Google Scholar
  30. Alan Jeffrey. Premonoidal categories and a graphical view of programs. Preprint, Dec, pages 80688-7, 1997. Google Scholar
  31. André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88(1):55-112, July 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
  32. André Joyal, Ross Street, and Dominic Verity. Traced monoidal categories. In Mathematical proceedings of the cambridge philosophical society, volume 119 (3), pages 447-468. Cambridge University Press, 1996. Google Scholar
  33. G.M. Kelly and S. Maclane. Coherence in closed categories. Journal of Pure and Applied Algebra, 1(1):97-140, 1971. URL: https://doi.org/10.1016/0022-4049(71)90013-2.
  34. Miguel L. Laplaza. Coherence for distributivity. In G. M. Kelly, M. Laplaza, G. Lewis, and Saunders Mac Lane, editors, Coherence in Categories, Lecture Notes in Mathematics, pages 29-65, Berlin, Heidelberg, 1972. Springer. URL: https://doi.org/10.1007/BFb0059555.
  35. Tom Leinster. Higher operads, higher categories. London Mathematical Society Lecture Note Series (298). Cambridge University Press, 2004. Google Scholar
  36. L. Méhats and S. Soloviev. Coherence in smccs and equivalences on derivations in imll with unit. Annals of Pure and Applied Logic, 147(3):127-179, 2007. URL: https://doi.org/10.1016/j.apal.2007.03.005.
  37. Paul-André Melliès. Functorial Boxes in String Diagrams. In Zoltán Ésik, editor, Computer Science Logic, Lecture Notes in Computer Science, pages 1-30, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11874683_1.
  38. Paul-André Melliès. Template games and differential linear logic. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785830.
  39. Ike Nassi and Ben Shneiderman. Flowchart techniques for structured programming. ACM Sigplan Notices, 8(8):12-26, 1973. URL: https://doi.org/10.1145/953349.953350.
  40. R. Penrose. Applications of negative dimension tensors. In D. J. A. Welsh, editor, Combinatorial Mathematics and its Applications, pages 221-244. Academic Press, 1971. Google Scholar
  41. James L Peterson. Petri nets. ACM Computing Surveys (CSUR), 9(3):223-252, 1977. URL: https://doi.org/10.1145/356698.356702.
  42. Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, and Fabio Zanasi. A complete axiomatisation of equivalence for discrete probabilistic programming. In European Symposium on Programming, pages 202-229. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-91121-7_9.
  43. Kate Ponto. Fixed point theory and trace for bicategories, 2008. URL: https://arxiv.org/abs/0807.1471.
  44. Kate Ponto and Michael Shulman. Traces in symmetric monoidal categories. Expositiones Mathematicae, 32(3):248-273, 2014. URL: https://doi.org/10.1016/j.exmath.2013.12.003.
  45. Callum Reader. Scalar enrichment and cotraces in bicategories, 2024. URL: https://arxiv.org/abs/2403.14475.
  46. Callum Reader and Alessandro Di Giorgio. String diagrams for closed symmetric monoidal categories, 2025. URL: https://arxiv.org/abs/2512.06499.
  47. Don D. Roberts. The Existential Graphs of Charles S. Peirce. De Gruyter Mouton, 1973. Google Scholar
  48. P. Selinger. A Survey of Graphical Languages for Monoidal Categories, 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.
  49. Michael Shulman. *-autonomous envelopes and conservativity. arXiv preprint arXiv:2004.08487, 2020. Google Scholar
  50. Aleksei Tiurin, Chris Barrett, Dan R Ghica, and Nick Hu. Equivalence hypergraphs: Dpo rewriting for monoidal e-graphs. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 209-222. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00023.
  51. Simon Willerton. Surface diagrams for closed monoidal categories. Private communication, 2025. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact