Document Open Access Logo

Rewriting for Monoidal Closed Categories

Authors Mario Alvarez-Picallo , Dan Ghica , David Sprunger , Fabio Zanasi

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.29.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Author Details

Mario Alvarez-Picallo
  • Programming Languages Laboratory, Huawei Research Centre, UK
Dan Ghica
  • Department of Computer Science, University of Birmingham, UK
  • Programming Languages Laboratory, Huawei Research Centre, Reading, UK
David Sprunger
  • Department of Computer Science, University of Birmingham, UK
Fabio Zanasi
  • Department of Computer Science, University College London, UK

Funding

This work was supported by the Engineering and Physical Sciences Research Council [grant numbers EP/V001612/1 and EP/V002376/1].

Cite As Get BibTex

Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Rewriting for Monoidal Closed Categories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.29

Abstract

This paper develops a formal string diagram language for monoidal closed categories. Previous work has shown that string diagrams for freely generated symmetric monoidal categories can be viewed as hypergraphs with interfaces, and the axioms of these categories can be realized by rewriting systems. This work proposes hierarchical hypergraphs as a suitable formalization of string diagrams for monoidal closed categories. We then show double pushout rewriting captures the axioms of these closed categories.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • string diagrams
  • rewriting
  • hierarchical hypergraph
  • monoidal closed category

Metrics

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

References

  1. Beniamino Accattoli. Proof nets and the call-by-value λ-calculus. Theor. Comput. Sci., 606:2-24, 2015. URL: https://doi.org/10.1016/j.tcs.2015.08.006.
  2. Mario Alvarez-Picallo, Dan R Ghica, David Sprunger, and Fabio Zanasi. Functorial string diagrams for reverse-mode automatic differentiation. arXiv preprint arXiv:2107.13433, 2021. Google Scholar
  3. John Baez and Mike Stay. Physics, topology, logic and computation: a rosetta stone. In New structures for physics, pages 95-172. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12821-9_2.
  4. Guillaume Boisseau and Paweł Sobociński. String diagrammatic electrical circuit theory. arXiv preprint arXiv:2106.07763, 2021. Google Scholar
  5. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory II: rewriting with symmetric monoidal structure. CoRR, abs/2104.14686, 2021. Google Scholar
  6. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory III: confluence with and without Frobenius. Mathematical Structures in Computer Science, to appear, 2021. Google Scholar
  7. 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. Google Scholar
  8. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. ACM SIGPLAN Notices, 50(1):515-526, 2015. Google Scholar
  9. Roberto Bruni, Fabio Gadducci, and Alberto Lluch-Lafuente. An algebra of hierarchical graphs. In Martin Wirsing, Martin Hofmann, and Axel Rauschmayer, editors, Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers, volume 6084 of Lecture Notes in Computer Science, pages 205-221. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15640-3_14.
  10. Roberto Bruni, Fabio Gadducci, and Alberto Lluch-Lafuente. An algebra of hierarchical graphs and its application to structural encoding. Sci. Ann. Comput. Sci., 20:53-96, 2010. URL: http://www.info.uaic.ro/bin/Annals/Article?v=XX&a=2.
  11. Davide Castelnovo, Fabio Gadducci, and Marino Miculan. A new criterion for ℳ, 𝒩-adhesivity, with an application to hierarchical graphs, 2022. URL: https://doi.org/10.48550/ARXIV.2201.00233.
  12. Cliff Click and Michael Paleczny. A simple graph-based intermediate representation. In Michael D. Ernst, editor, Proceedings ACM SIGPLAN Workshop on Intermediate Representations (IR'95), San Francisco, CA, USA, January 22, 1995, pages 35-49. ACM, 1995. URL: https://doi.org/10.1145/202529.202534.
  13. Matteo Coccia, Fabio Gadducci, and Ugo Montanari. Gs.lambda theories: A syntax for higher-order graphs. In Richard Blute and Peter Selinger, editors, Category Theory and Computer Science, CTCS 2002, Ottawa, Canada, August 15-17, 2002, volume 69 of Electronic Notes in Theoretical Computer Science, pages 83-100. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80560-7.
  14. Bob Coecke and Ross Duncan. Interacting quantum observables. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, pages 298-310, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  15. Frank Drewes, Berthold Hoffmann, and Detlef Plump. Hierarchical graph transformation. J. Comput. Syst. Sci., 64(2):249-283, 2002. URL: https://doi.org/10.1006/jcss.2001.1790.
  16. Dan R. Ghica. Operational semantics with hierarchical abstract syntax graphs. In Patrick Bahr, editor, Proceedings 11th International Workshop on Computing with Terms and Graphs, TERMGRAPH@FSCD 2020, Online, 5th July 2020, volume 334 of EPTCS, pages 1-10, 2020. URL: https://doi.org/10.4204/EPTCS.334.1.
  17. 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.
  18. Dan R. Ghica, Koko Muroya, and Todd Waugh Ambridge. Local reasoning for robust observational equivalence. CoRR, abs/1907.01257, 2019. URL: http://arxiv.org/abs/1907.01257.
  19. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  20. Stefano Guerrini. A general theory of sharing graphs. Theor. Comput. Sci., 227(1-2):99-151, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00050-X.
  21. Ralf Hinze. Kan extensions for program optimisation or: Art and dan explain an old trick. In Jeremy Gibbons and Pablo Nogueira, editors, Mathematics of Program Construction - 11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012. Proceedings, volume 7342 of Lecture Notes in Computer Science, pages 324-362. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31113-0_16.
  22. Dominic Hughes. Simple free star-autonomous categories and full coherence. CoRR, 2005. URL: https://arxiv.org/abs/math/0506521.
  23. 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.
  24. Yves Lafont. Interaction nets. In Frances E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 95-108. ACM Press, 1990. URL: https://doi.org/10.1145/96709.96718.
  25. John Lamping. An algorithm for optimal lambda calculus reduction. In Frances E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 16-30. ACM Press, 1990. URL: https://doi.org/10.1145/96709.96711.
  26. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science & Business Media, 2013. Google Scholar
  27. 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.
  28. José Meseguer and Ugo Montanari. Petri nets are monoids. Information and Computation, 88(2):105-155, 1990. URL: https://doi.org/10.1016/0890-5401(90)90013-8.
  29. Koko Muroya and Dan R. Ghica. The dynamic geometry of interaction machine: A token-guided graph rewriter. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:7)2019.
  30. Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock. Synthesizing structured CAD models with equality saturation and inverse transformations. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 31-44. ACM, 2020. URL: https://doi.org/10.1145/3385412.3386012.
  31. Wojciech Palacz. Algebraic hierarchical graph transformation. J. Comput. Syst. Sci., 68(3):497-520, 2004. URL: https://doi.org/10.1016/S0022-0000(03)00064-3.
  32. Maciej Piróg and Nicolas Wu. String diagrams for free monads (functional pearl). In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 490-501. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951947.
  33. Ralf Schweimeier and Alan Jeffrey. A categorical and graphical treatment of closure conversion. In Stephen D. Brookes, Achim Jung, Michael W. Mislove, and Andre Scedrov, editors, Fifteenth Conference on Mathematical Foundations of Progamming Semantics, MFPS 1999, Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999, volume 20 of Electronic Notes in Theoretical Computer Science, pages 481-511. Elsevier, 1999. URL: https://doi.org/10.1016/S1571-0661(04)80090-2.
  34. Michael Shulman. *-autonomous envelopes and 2-conservativity of duals. CoRR, 2020. URL: http://arxiv.org/abs/2004.08487.
  35. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006. Google Scholar
  36. David Sprunger and Shin-ya Katsumata. Differentiable causal computations via delayed trace. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2019. Google Scholar
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