Document Open Access Logo

The Produoidal Algebra of Process Decomposition

Authors Matt Earnshaw , James Hefford , Mario Román

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2024.25.pdf
  • Filesize: 0.99 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • monoidal categories
  • profunctors
  • lenses
  • duoidal categories

Metrics

Abstract

We characterize a universal normal produoidal category of monoidal contexts over an arbitrary monoidal category. In the same sense that a monoidal morphism represents a process, a monoidal context represents an incomplete process: a piece of a decomposition, possibly containing missing parts. In particular, symmetric monoidal contexts coincide with monoidal lenses and endow them with a novel universal property. We apply this algebraic structure to the analysis of multi-party protocols in arbitrary theories of processes.

Cite As Get BibTex

Matt Earnshaw, James Hefford, and Mario Román. The Produoidal Algebra of Process Decomposition. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.25

Author Details

Matt Earnshaw
  • Tallinn University of Technology, Estonia
James Hefford
  • University of Oxford, UK
Mario Román
  • Tallinn University of Technology, Estonia

Funding

Matt Earnshaw and Mario Román were supported by the European Social Fund Estonian IT Academy research measure (project 2014-2020.4.05.19-0001). James Hefford is supported by University College London and the EPSRC [grant number EP/L015242/1].

Acknowledgements

We thank Pawel Sobocinski, Fosco Loregian, Chad Nester and David Spivak for discussion. We thank the CSL reviewers for suggestions that lead to considerable improvements.

References

  1. Samson Abramsky. What are the fundamental structures of concurrency?: We still don't know! In Luca Aceto and Andrew D. Gordon, editors, Proceedings of the Workshop "Essays on Algebraic Process Calculi", APC 25, Bertinoro, Italy, August 1-5, 2005, volume 162 of Electronic Notes in Theoretical Computer Science, pages 37-41. Elsevier, 2005. URL: https://doi.org/10.1016/j.entcs.2005.12.075.
  2. Samson Abramsky and Bob Coecke. Categorical quantum mechanics. In Kurt Engesser, Dov M. Gabbay, and Daniel Lehmann, editors, Handbook of Quantum Logic and Quantum Structures, pages 261-323. Elsevier, Amsterdam, 2009. URL: https://doi.org/10.1016/B978-0-444-52869-8.50010-4.
  3. Marcelo Aguiar, Mariana Haim, and Ignacio López Franco. Monads on higher monoidal categories. Applied Categorical Structures, 26(3):413-458, June 2018. URL: https://doi.org/10.1007/s10485-017-9497-8.
  4. Bruce Bartlett, Christopher L. Douglas, Christopher J. Schommer-Pries, and Jamie Vicary. Modular categories as representations of the 3-dimensional bordism 2-category, 2015. URL: https://arxiv.org/abs/1509.06811.
  5. Jean Bénabou. Distributors at work. Lecture notes written by Thomas Streicher, 11, 2000. Google Scholar
  6. Guillaume Boisseau and Jeremy Gibbons. What you needa know about yoneda: Profunctor optics and the yoneda lemma (functional pearl). Proceedings of the ACM on Programming Languages, 2(ICFP):1-27, 2018. Google Scholar
  7. Guillaume Boisseau, Chad Nester, and Mario Román. Cornering optics. In Proceedings Fifth International Conference on Applied Category Theory, ACT 2022, Glasgow, United Kingdom, 18-22 July 2022, volume abs/2205.00842, 2022. URL: https://doi.org/10.48550/arXiv.2205.00842.
  8. Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Graphical affine algebra. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-12. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785877.
  9. Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical conjunctive queries. In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 13:1-13:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.13.
  10. Thomas Booker and Ross Street. Tannaka duality and convolution for duoidal categories. Theory and Applications of Categories, 28(6):166-205, 2013. Google Scholar
  11. Kenta Cho and Bart Jacobs. Disintegration and Bayesian Inversion via String Diagrams. Mathematical Structures in Computer Science, pages 1-34, March 2019. URL: https://doi.org/10.1017/S0960129518000488.
  12. Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregiàn, Bartosz Milewski, Emily Pillmore, and Mario Román. Profunctor optics, a categorical update. CoRR, abs/2001.07488, 2020. URL: https://arxiv.org/abs/2001.07488.
  13. J. Robin B. Cockett and Stephen Lack. Restriction categories I: categories of partial maps. Theoretical Computer Science, 270(1-2):223-259, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00382-0.
  14. J. Robin B. Cockett and Craig A. Pastro. The logic of message-passing. Sci. Comput. Program., 74(8):498-533, 2009. URL: https://doi.org/10.1016/j.scico.2007.11.005.
  15. J. Robin B. Cockett and Robert A. G. Seely. Weakly distributive categories. Journal of Pure and Applied Algebra, 114(2):133-173, 1997. Google Scholar
  16. Bob Coecke, Tobias Fritz, and Robert W. Spekkens. A mathematical theory of resources. Inf. Comput., 250:59-86, 2016. URL: https://doi.org/10.1016/j.ic.2016.02.008.
  17. Geoffrey S. H. Cruttwell, Bruno Gavranović, Neil Ghani, Paul Wilson, and Fabio Zanasi. Categorical foundations of gradient-based learning. In European Symposium on Programming, pages 1-28. Springer, Cham, 2022. Google Scholar
  18. Brian Day. On closed categories of functors. In Reports of the Midwest Category Seminar IV, volume 137, pages 1-38, Berlin, Heidelberg, 1970. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0060438.
  19. Elena Di Lavore, Giovanni de Felice, and Mario Román. Monoidal streams for dataflow programming. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533365.
  20. Matt Earnshaw, James Hefford, and Mario Román. The produoidal algebra of process decomposition, 2023. URL: https://arxiv.org/abs/2301.11867.
  21. Matthew Earnshaw and Pawel Sobociński. Regular Monoidal Languages. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), volume 241 of Leibniz International Proceedings in Informatics (LIPIcs), pages 44:1-44:14, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.44.
  22. Brendan Fong and Michael Johnson. Lenses and learners. arXiv preprint, 2019. URL: https://arxiv.org/abs/1903.03671.
  23. J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(3):17-es, 2007. Google Scholar
  24. Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020. URL: https://arxiv.org/abs/1908.07021.
  25. Richard Garner and Ignacio López Franco. Commutativity. Journal of Pure and Applied Algebra, 220(5):1707-1751, 2016. Google Scholar
  26. Simon J. Gay and Malcolm Hole. Types and subtypes for client-server interactions. In S. Doaitse Swierstra, editor, Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, 22-28 March, 1999, Proceedings, volume 1576 of Lecture Notes in Computer Science, pages 74-90. Springer, 1999. URL: https://doi.org/10.1007/3-540-49099-X_6.
  27. Neil Ghani, Jules Hedges, Viktor Winschel, and Philipp Zahn. Compositional game theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 472-481. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209165.
  28. René Guitart. Tenseurs et machines. Cahiers de topologie et géométrie différentielle catégoriques, 21(1):5-62, 1980. URL: http://www.numdam.org/item/CTGDC_1980__21_1_5_0/.
  29. Masahito Hasegawa. Models of sharing graphs: a categorical semantics of let and letrec. PhD thesis, University of Edinburgh, UK, 1997. URL: http://hdl.handle.net/1842/15001.
  30. Jules Hedges. Coherence for lenses and open games. arXiv preprint, 2017. URL: https://arxiv.org/abs/1704.02230.
  31. James Hefford and Cole Comfort. Coend optics for quantum combs. arXiv preprint, 2022. https://arxiv.org/abs/2205.09027, URL: https://doi.org/10.48550/ARXIV.2205.09027.
  32. James Hefford and Aleks Kissinger. On the pre- and promonoidal structure of spacetime. arXiv preprint, 2022. URL: https://doi.org/10.48550/arXiv.2206.09678.
  33. Chris Heunen and Bart Jacobs. Arrows, like monads, are monoids. In Stephen D. Brookes and Michael W. Mislove, editors, Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 2006, Genova, Italy, May 23-27, 2006, volume 158 of Electronic Notes in Theoretical Computer Science, pages 219-236. Elsevier, 2006. URL: https://doi.org/10.1016/j.entcs.2006.04.012.
  34. Chris Heunen and Jesse Sigal. Duoidally enriched Freyd categories. arXiv preprint, 2023. URL: https://arxiv.org/abs/2301.05162.
  35. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  36. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  37. John Hughes. Generalising monads to arrows. Science of Computer Programming, 37(1-3):67-111, 2000. URL: https://doi.org/10.1016/S0167-6423(99)00023-4.
  38. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  39. Michael Johnson, Robert Rosebrugh, and Richard J. Wood. Lenses, fibrations and universal translations. Mathematical structures in computer science, 22(1):25-42, 2012. Google Scholar
  40. 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.
  41. Aleks Kissinger and Sander Uijlen. A categorical semantics for causal structure. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005095.
  42. Edward Kmett. lens library, version 4.16. Hackage https://hackage. haskell. org/package/lens-4.16, 2018, 2012. Google Scholar
  43. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. In Hans-Juergen Boehm and Guy L. Steele Jr., editors, Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, pages 358-371. ACM Press, 1996. URL: https://doi.org/10.1145/237721.237804.
  44. Fosco Loregian. (Co)end Calculus. London Mathematical Society Lecture Note Series. Cambridge University Press, 2021. URL: https://doi.org/10.1017/9781108778657.
  45. Paul-André Melliès and Noam Zeilberger. Parsing as a Lifting Problem and the Chomsky-Schützenberger Representation Theorem. In MFPS 2022-38th conference on Mathematical Foundations for Programming Semantics, 2022. Google Scholar
  46. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  47. David Jaz Myers. String diagrams for double categories and equipments, 2016. URL: https://doi.org/10.48550/arXiv.1612.02762.
  48. Chad Nester. Concurrent Process Histories and Resource Transducers. Logical Methods in Computer Science, Volume 19, Issue 1, January 2023. URL: https://doi.org/10.46298/lmcs-19(1:7)2023.
  49. Nelson Niu and David I. Spivak. Polynomial functors: A general theory of interaction. In preparation, 2022. Google Scholar
  50. Craig Pastro and Ross Street. Doubles for Monoidal Categories. arXiv preprint, 2007. URL: https://arxiv.org/abs/0711.1859.
  51. Ross Paterson. A new notation for arrows. In Benjamin C. Pierce, editor, Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), Firenze (Florence), Italy, September 3-5, 2001, pages 229-240. ACM, 2001. URL: https://doi.org/10.1145/507635.507664.
  52. Evan Patterson, David I. Spivak, and Dmitry Vagner. Wiring diagrams as normal forms for computing in symmetric monoidal categories. Electronic Proceedings in Theoretical Computer Science, pages 49-64, February 2021. Google Scholar
  53. Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. Profunctor optics: Modular data accessors. Art Sci. Eng. Program., 1(2):7, 2017. URL: https://doi.org/10.22152/programming-journal.org/2017/1/7.
  54. Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993, pages 376-385. IEEE Computer Society, 1993. URL: https://doi.org/10.1109/LICS.1993.287570.
  55. J. Postel. Transmission control protocol. RFC 793, RFC Editor, September 1981. URL: https://doi.org/10.17487/RFC0793.
  56. Mitchell Riley. Categories of Optics. arXiv preprint, 2018. URL: https://arxiv.org/abs/1809.00738.
  57. Mario Román. Comb Diagrams for Discrete-Time Feedback. CoRR, abs/2003.06214, 2020. URL: https://arxiv.org/abs/2003.06214.
  58. Mario Román. Promonads and string diagrams for effectful categories. In ACT '22: Applied Category Theory, Glasgow, United Kingdom, 18-22 July, 2022, volume abs/2205.07664, 2022. URL: https://doi.org/10.48550/arXiv.2205.07664.
  59. Mario Román. Open diagrams via coend calculus. Electronic Proceedings in Theoretical Computer Science, 333:65-78, February 2021. URL: https://doi.org/10.4204/eptcs.333.5.
  60. Davide Sangiorgi and David Walker. The Pi-Calculus - A theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  61. Patrick Schultz, David I. Spivak, and Christina Vasilakopoulou. Dynamical systems and sheaves. Applied Categorical Structures, 28(1):1-57, 2020. Google Scholar
  62. Brandon T. Shapiro and David I. Spivak. Duoidal structures for compositional dependence. arXiv preprint, 2022. URL: https://arxiv.org/abs/2210.01962.
  63. Michael Shulman. Categorical logic from a categorical point of view. Available on the web, 2016. URL: https://mikeshulman.github.io/catlog/catlog.pdf.
  64. Michael Shulman. Duoidal category (nlab entry), section 2, 2017. , Last accessed on 2022-12-14. URL: https://ncatlab.org/nlab/show/duoidal+category.
  65. David I. Spivak. The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits. CoRR, abs/1305.0297, 2013. URL: https://arxiv.org/abs/1305.0297.
  66. Ross Street. Monoidal categories in, and linking, geometry and algebra. Bulletin of the Belgian Mathematical Society-Simon Stevin, 19(5):769-820, 2012. Google Scholar
  67. André Videla and Matteo Capucci. Lenses for composable servers. CoRR, abs/2203.15633, 2022. URL: https://doi.org/10.48550/arXiv.2203.15633.
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