Document Open Access Logo

Resourceful Traces for Commuting Processes

Authors Matthew Earnshaw , Chad Nester , Mario Román

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.28.pdf
  • Filesize: 1.21 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Categorical semantics
Keywords
  • Mazurkiewicz traces
  • premonoidal categories
  • monoidal categories
  • effectful categories

Metrics

Abstract

We show that, when the actions of a Mazurkiewicz trace are considered not merely as atomic but as transformations from a specified type of inputs to a specified type of outputs, we obtain a novel notion of presentation for effectful categories (also known as generalized Freyd categories), a well-known algebraic structure in the semantics of side-effecting computation. Like the usual representation of traces as graphs, our notion of presentation gives rise to a graphical representation of morphisms in effectful categories. We use our presentations to give a construction of the commuting tensor product of free effectful categories, capturing the combination of systems in which the actions of each must commute with one another, while still permitting exchange of resources.

Cite As Get BibTex

Matthew Earnshaw, Chad Nester, and Mario Román. Resourceful Traces for Commuting Processes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.28

Author Details

Matthew Earnshaw
  • Tallinn University of Technology, Estonia
  • University of Tartu, Estonia
Chad Nester
  • University of Tartu, Estonia
Mario Román
  • University of Oxford, UK

Funding

  • Earnshaw, Matthew: Estonian Research Council grant PRG1210 and PRG2764.
  • Nester, Chad: Estonian Research Council grant PRG2764.
  • Román, Mario: Air Force Office of Scientific Research (AFOSR) award number FA9550-21-1-0038; Advanced Research + Invention Agency (ARIA), Safeguarded AI Programme.

Acknowledgements

The authors thank Niels Voorneveld for discussions, and the anonymous reviewers for their detailed comments and suggestions on the manuscript.

References

  1. Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. 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 10:1-10:18, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.10.
  2. Christian Choffrut and Robert Mercas. Contextual partial commutations. Discrete Mathematics & Theoretical Computer Science, 12, 2010. Google Scholar
  3. Mireille Clerbout and Michel Latteux. Semi-commutations. Information and computation, 73(1):59-74, 1987. URL: https://doi.org/10.1016/0890-5401(87)90040-X.
  4. Bob Coecke, Tobias Fritz, and Robert W Spekkens. A mathematical theory of resources. Information and Computation, 250:59-86, 2016. URL: https://doi.org/10.1016/J.IC.2016.02.008.
  5. Volker Diekert and Grzegorz Rozenberg. The Book of Traces. World Scientific, 1995. URL: https://doi.org/10.1142/2563.
  6. Matthew Earnshaw. Languages of String Diagrams. PhD thesis, Tallinn University of Technology, 2025. URL: https://doi.org/10.23658/TALTECH.2/2025.
  7. Matthew Earnshaw and Pawel Sobociński. String Diagrammatic Trace Theory. In MFCS, volume 272, 2023. URL: https://doi.org/10.4230/LIPIcs.MFCS.2023.43.
  8. Dominique Foata and Pierre Cartier. Problèmes combinatoires de commutation et réarrangements. Lecture notes in mathematics, 85, 1969. Google Scholar
  9. P. Freyd. Algebra valued functors in general and tensor products in particular. Colloquium Mathematicum, 14(1):89-106, 1966. URL: https://doi.org/10.4064/cm-14-1-89-106.
  10. Richard Garner and Ignacio López Franco. Commutativity. Journal of Pure and Applied Algebra, 220(5):1707-1751, 2016. Google Scholar
  11. Philip Hackney and Marcy Robertson. On the category of props. Applied Categorical Structures, 23(4):543-573, August 2015. URL: https://doi.org/10.1007/s10485-014-9369-4.
  12. Martin Hyland, Gordon Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical computer science, 357(1-3):70-99, 2006. URL: https://doi.org/10.1016/J.TCS.2006.03.013.
  13. Alan Jeffrey. Premonoidal categories and a graphical view of programs. Preprint, 1997. Google Scholar
  14. 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.
  15. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Information and Computation, 185(2):182-210, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00088-9.
  16. Antoni Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Report Series, 6(78), July 1977. URL: https://doi.org/10.7146/dpb.v6i78.7691.
  17. Antoni Mazurkiewicz. Basic notions of trace theory. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, pages 285-363, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  18. Paul-André Melliès. Local states in string diagrams. In Rewriting and Typed Lambda Calculi: Joint International Conference, pages 334-348. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_23.
  19. John Power. Premonoidal categories as categories with algebraic structure. Theoretical Computer Science, 278(1):303-321, 2002. Mathematical Foundations of Programming Semantics 1996. URL: https://doi.org/10.1016/S0304-3975(00)00340-6.
  20. John Power and Edmund Robinson. Premonoidal categories and notions of computation. Math. Struct. Comput. Sci., 7(5):453-468, 1997. URL: https://doi.org/10.1017/S0960129597002375.
  21. John Power and Hayo Thielecke. Closed freyd- and κ-categories. In Jirí Wiedermann, Peter van Emde Boas, and Mogens Nielsen, editors, Automata, Languages and Programming, pages 625-634, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. Google Scholar
  22. Mario Román. Promonads and string diagrams for effectful categories. In Applied Category Theory, volume 380 of Electronic Proceedings in Theoretical Computer Science, pages 344-361. Open Publishing Association, 2023. URL: https://doi.org/10.4204/EPTCS.380.20.
  23. Mario Román and Paweł Sobociński. String diagrams for premonoidal categories. Logical Methods in Computer Science, Volume 21, Issue 2, April 2025. URL: https://doi.org/10.46298/lmcs-21(2:9)2025.
  24. Sam Staton and Paul Blain Levy. Universal properties of impure programming languages. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 179-192, New York, NY, USA, 2013. Association for Computing Machinery. URL: https://doi.org/10.1145/2429069.2429091.
  25. Wieslaw Zielonka. Notes on finite asynchronous automata. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 21(2):99-135, 1987. URL: https://doi.org/10.1051/ITA/1987210200991.
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