Document Open Access Logo

Nominal String Diagrams

Authors Samuel Balco, Alexander Kurz

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2019.18.pdf
  • Filesize: 8.41 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Theory of computation → Models of computation
  • Theory of computation → Logic
  • Mathematics of computing
Keywords
  • string diagrams
  • nominal sets
  • separated product
  • simultaneous substitutions
  • internal category
  • monoidal category
  • internal monoidal categories
  • PROP

Metrics

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

Abstract

We introduce nominal string diagrams as string diagrams internal in the category of nominal sets. This requires us to take nominal sets as a monoidal category, not with the cartesian product, but with the separated product. To this end, we develop the beginnings of a theory of monoidal categories internal in a symmetric monoidal category. As an instance, we obtain a notion of a nominal PROP as a PROP internal in nominal sets. A 2-dimensional calculus of simultaneous substitutions is an application.

Cite As Get BibTex

Samuel Balco and Alexander Kurz. Nominal String Diagrams. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CALCO.2019.18

Author Details

Samuel Balco
  • Department of Informatics,University of Leicester, United Kingdom
Alexander Kurz
  • Department of Computer Science, Chapman University, Orange California, USA

Acknowledgements

We are greatful to Fredrik Dahlqvist, Giuseppe Greco, Samuel Mimram, Drew Moshier, Alessandra Palmigiano, David Pym, Mike Shulman, Pawel Sobocinski, Thomas Streicher, Georg Struth, Apostolos Tzimoulis and Fabio Zanasi for discussions on the topic of this paper.

References

  1. John C. Baez, Brandon Coya, and Franciscus Rebro. Props in Network Theory. Theory and Applications of Categories, 33, 2018. URL: http://www.tac.mta.ca/tac/volumes/33/25/33-25abs.html.
  2. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, PawełSobociński, and Fabio Zanasi. Rewriting Modulo Symmetric Monoidal Structure. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 710-719, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2933575.2935316.
  3. Filippo Bonchi, PawełSobociński, and Fabio Zanasi. The Calculus of Signal Flow Diagrams I. Inf. Comput., 252(C):2-29, February 2017. URL: https://doi.org/10.1016/j.ic.2016.03.002.
  4. 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.
  5. Pierre-Louis Curien and Samuel Mimram. Coherent Presentations of Monoidal Categories. Logical Methods in Computer Science, 13(3):1-38, September 2017. URL: https://doi.org/10.23638/LMCS-13(3:31)2017.
  6. Brijesh Dongol, Victor B. F. Gomes, and Georg Struth. A Program Construction and Verification Tool for Separation Logic. In Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings, pages 137-158, 2015. URL: https://doi.org/10.1007/978-3-319-19797-5_7.
  7. Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, and Vlasta Sikimić. Multi-type display calculus for dynamic epistemic logic. Journal of Logic and Computation, 26(6):2017-2065, December 2014. URL: https://doi.org/10.1093/logcom/exu068.
  8. Murdoch J. Gabbay and Andrew M. Pitts. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing, 13(3):341-363, July 2002. URL: https://doi.org/10.1007/s001650200016.
  9. D. Galmiche, D. Méry, and D. Pym. The Semantics of BI and Resource Tableaux. Mathematical. Structures in Comp. Sci., 15(6):1033-1088, December 2005. URL: https://doi.org/10.1017/S0960129505004858.
  10. Dan R. Ghica and Aliaume Lopez. A structural and nominal syntax for diagrams. In Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3-7 July 2017., pages 71-83, 2017. URL: https://doi.org/10.4204/EPTCS.266.4.
  11. Bart Jacobs. Categorical Logic and Type Theory. Studies in logic and the foundations of mathematics. Elsevier Science, 1999. Google Scholar
  12. 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.
  13. Steve Lack. Composing PROPs. Theory and Applications of Categories, 13:147–163, 2004. URL: http://www.tac.mta.ca/tac/volumes/13/9/13-09abs.html.
  14. Yves Lafont. Towards an algebraic theory of Boolean circuits. Journal of Pure and Applied Algebra, 184:257-310, 2003. URL: https://doi.org/10.1016/S0022-4049(03)00069-0.
  15. Saunders Mac Lane. Categories for the Working Mathematician. Springer New York, 1978. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  16. Saunders MacLane. Categorical algebra. Bull. Amer. Math. Soc., 71(1):40-106, January 1965. URL: https://doi.org/10.1090/S0002-9904-1965-11234-4.
  17. Peter W. O'Hearn and David J. Pym. The Logic of Bunched Implications. The Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  18. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139084673.
  19. P. Selinger. A Survey of Graphical Languages for Monoidal Categories, pages 289-355. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  20. Thomas Streicher. Fibred Categories à la Jean Bénabou, 1999. URL: http://arxiv.org/abs/arXiv:1801.02927.
  21. Apostolos Tzimoulis. Algebraic and Proof-Theoretic Foundations of the Logics for Social Behaviour. PhD thesis, Delft University of Technology, 2018. URL: https://doi.org/10.4233/uuid:e67e7724-b378-4ca3-ad4e-c40df245af5e.
  22. Fabio Zanasi. Interacting Hopf Algebras- the Theory of Linear Systems. Theses, Ecole normale supérieure de lyon - ENS LYON, October 2015. URL: https://tel.archives-ouvertes.fr/tel-01218015.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact