Document Open Access Logo

Rewriting Modulo Traced Comonoid Structure

Authors Dan R. Ghica , George Kaye

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.14.pdf
  • Filesize: 1.01 MB
  • 21 pages

Document Identifiers

Author Details

Dan R. Ghica
  • University of Birmingham, UK
George Kaye
  • University of Birmingham, UK

Funding

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

Acknowledgements

Thanks to Chris Barrett for helpful comments.

Cite AsGet BibTex

Dan R. Ghica and George Kaye. Rewriting Modulo Traced Comonoid Structure. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.14

Abstract

In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting. We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • symmetric traced monoidal categories
  • string diagrams
  • graph rewriting
  • comonoid structure
  • double pushout rewriting

Metrics

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

Related Versions

References

  1. Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Functorial String Diagrams for Reverse-Mode Automatic Differentiation. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl endash Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.6.
  2. E. S. Bainbridge. Feedback and generalized logic. Information and Control, 31(1):75-96, May 1976. URL: https://doi.org/10.1016/S0019-9958(76)90390-9.
  3. 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, July 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2935316.
  4. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobociński, and Fabio Zanasi. String Diagram Rewrite Theory I: Rewriting with Frobenius Structure. Journal of the ACM, 69(2): 14:1-14:58, March 2022. URL: https://doi.org/10.1145/3502719.
  5. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory II: Rewriting with symmetric monoidal structure. Mathematical Structures in Computer Science, 32(4):511-541, April 2022. URL: https://doi.org/10.1017/S0960129522000317.
  6. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, and Fabio Zanasi. String diagram rewrite theory III: Confluence with and without Frobenius. Mathematical Structures in Computer Science, pages 1-41, June 2022. URL: https://doi.org/10.1017/S0960129522000123.
  7. A. Carboni and R. F. C. Walters. Cartesian bicategories I. Journal of Pure and Applied Algebra, 49(1):11-32, November 1987. URL: https://doi.org/10.1016/0022-4049(87)90121-6.
  8. Virgil Emil Căzănescu and Gheorghe Ştefănescu. Towards a New Algebraic Foundation of Flowchart Scheme Theory. Fundamenta Informaticae, 13(2):171-210, January 1990. URL: https://doi.org/10.3233/FI-1990-13204.
  9. Virgil Emil Căzănescu and Gheorghe Ştefănescu. Feedback, Iteration, and Repetition. In Mathematical Aspects of Natural and Formal Languages, volume Volume 43 of World Scientific Series in Computer Science, pages 43-61. World Scientific, October 1994. URL: https://doi.org/10.1142/9789814447133_0003.
  10. Lucas Dixon and Aleks Kissinger. Open-graphs and monoidal theories. Mathematical Structures in Computer Science, 23(2):308-359, April 2013. URL: https://doi.org/10.1017/S0960129512000138.
  11. Brendan Fong and David I. Spivak. Hypergraph categories. Journal of Pure and Applied Algebra, 223(11):4746-4777, November 2019. URL: https://doi.org/10.1016/j.jpaa.2019.02.014.
  12. Thomas Fox. Coalgebras and cartesian categories. Communications in Algebra, 4(7):665-667, January 1976. URL: https://doi.org/10.1080/00927877608822127.
  13. Tobias Fritz and Wendong Liang. Free gs-Monoidal Categories and Free Markov Categories. Applied Categorical Structures, 31(2):21, April 2023. URL: https://doi.org/10.1007/s10485-023-09717-0.
  14. Dan R. Ghica, George Kaye, and David Sprunger. A compositional theory of digital circuits. CoRR, abs/2201.10456, February 2023. URL: https://doi.org/10.48550/arXiv.2201.10456.
  15. Masahito Hasegawa. Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi. In Philippe de Groote and J. Roger Hindley, editors, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, pages 196-213, Berlin, Heidelberg, 1997. Springer. URL: https://doi.org/10.1007/3-540-62688-3_37.
  16. Masahito Hasegawa. On traced monoidal closed categories. Mathematical Structures in Computer Science, 19(2):217-244, April 2009. URL: https://doi.org/10.1017/S0960129508007184.
  17. Masahito Hasegawa, Martin Hofmann, and Gordon Plotkin. Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories. In Arnon Avron, Nachum Dershowitz, and Alexander Rabinovich, editors, Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Lecture Notes in Computer Science, pages 367-385. Springer, Berlin, Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-78127-1_20.
  18. Marvin Heumüller, Salil Joshi, Barbara König, and Jan Stückrath. Construction of Pushout Complements in the Category of Hypergraphs. Electronic Communications of the EASST, 39(0), September 2011. URL: https://doi.org/10.14279/tuj.eceasst.39.647.
  19. 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.
  20. André Joyal, Ross Street, and Dominic Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119(3):447-468, April 1996. URL: https://doi.org/10.1017/S0305004100074338.
  21. Aleks Kissinger. Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing. PhD thesis, University of Oxford, March 2012. URL: https://doi.org/10.48550/arXiv.1203.0202.
  22. Aleks Kissinger. Abstract Tensor Systems as Monoidal Categories. In Claudia Casadio, Bob Coecke, Michael Moortgat, and Philip Scott, editors, Categories and Types in Logic, Language, and Physics: Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, Lecture Notes in Computer Science, pages 235-252. Springer, Berlin, Heidelberg, 2014. URL: https://doi.org/10.1007/978-3-642-54789-8_13.
  23. Stephen Lack and Paweł Sobociński. Adhesive Categories. In Igor Walukiewicz, editor, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, pages 273-288, Berlin, Heidelberg, 2004. Springer. URL: https://doi.org/10.1007/978-3-540-24727-2_20.
  24. Stephen Lack and Paweł Sobociński. Adhesive and quasiadhesive categories. RAIRO - Theoretical Informatics and Applications, 39(3):511-545, July 2005. URL: https://doi.org/10.1051/ita:2005028.
  25. F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50(5):869-872, November 1963. URL: https://doi.org/10.1073/pnas.50.5.869.
  26. 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.
  27. Aleksandar Milosavljevic, Robin Piedeleu, and Fabio Zanasi. String Diagram Rewriting Modulo Commutative (Co)monoid Structure. CoRR, abs/2204.04274, March 2023. URL: https://doi.org/10.48550/arXiv.2204.04274.
  28. R. Rosebrugh, N. Sabadini, and R. F. C. Walters. Generic commutative separable algebras and cospans of graphs. Theory and Applications of Categories, 15:164-177, 2005. Google Scholar
  29. Ralf Schweimeier and Alan Jeffrey. A Categorical and Graphical Treatment of Closure Conversion. Electronic Notes in Theoretical Computer Science, 20:481-511, January 1999. URL: https://doi.org/10.1016/S1571-0661(04)80090-2.
  30. Peter Selinger. A Survey of Graphical Languages for Monoidal Categories. In Bob Coecke, editor, New Structures for Physics, Lecture Notes in Physics, pages 289-355. Springer, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  31. Peter Selinger. Finite dimensional Hilbert spaces are complete for dagger compact closed categories. Logical Methods in Computer Science, 8(3), August 2012. URL: https://doi.org/10.2168/LMCS-8(3:6)2012.
  32. Paul Wilson, Dan Ghica, and Fabio Zanasi. String Diagrams for Non-Strict Monoidal Categories. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 37:1-37:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl endash Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.37.
  33. Gheorghe Ștefănescu. Feedback Theories (A Calculus for Isomorphism Classes of Flowchart Schemes). Romanian Journal of Pure and Applied Mathematics, 35(1):73-79, 1990. 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 Imprint Privacy Contact