Bialgebraic Semantics for String Diagrams

Authors Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, Fabio Zanasi



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.37.pdf
  • Filesize: 0.71 MB
  • 17 pages

Document Identifiers

Author Details

Filippo Bonchi
  • University of Pisa, Italy
Robin Piedeleu
  • University College London, UK
Pawel Sobocinski
  • University of Southampton, UK
Fabio Zanasi
  • University College London, UK

Acknowledgements

RP and FZ acknowledge support from EPSRC grant EP/R020604/1.

Cite As Get BibTex

Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Bialgebraic Semantics for String Diagrams. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.37

Abstract

Turi and Plotkin’s bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental in showing that a semantic specification (a coalgebra) satisfies desirable properties: in particular, that it is compositional. 
In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of string diagrams, a graphical syntax that is increasingly used in the study of interacting systems across different disciplines. Our analysis relies on representing the two-dimensional operations underlying string diagrams in various categories as a monad, and their bialgebraic semantics in terms of a distributive law for that monad. 
As a proof of concept, we provide bialgebraic compositional semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory). Moreover, our approach reveals a correspondence between two different interpretations of the Frobenius equations on string diagrams and two synchronisation mechanisms for processes, à la Hoare and à la Milner.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • String Diagram
  • Structural Operational Semantics
  • Bialgebraic semantics

Metrics

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

References

  1. Samson Abramsky and Bob Coecke. A Categorical Semantics of Quantum Protocols. In LICS 2004, pages 415-425, 2004. URL: https://doi.org/10.1109/LICS.2004.1319636.
  2. John Baez and Jason Erbele. Categories In Control. Theory Appl. Categ., 30:836-881, 2015. URL: http://arxiv.org/abs/1405.6881.
  3. John Baez and Brendan Fong. A compositional framework for passive linear circuits. J. Complex Netw., 54:5, 2015. Google Scholar
  4. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, 1995. Google Scholar
  5. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, and Fabio Zanasi. Rewriting modulo symmetric monoidal structure. In LICS 2016, pages 1-10, 2016. Google Scholar
  6. Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi. Diagrammatic Algebra: from Linear to Concurrent Systems. In POPL 2019, page 25, 2019. Google Scholar
  7. Filippo Bonchi, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi. Bialgebraic Semantics for String Diagrams. CoRR, 2019. URL: http://arxiv.org/abs/1906.01519.
  8. Filippo Bonchi, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi. Graphical Affine Algebra. In To appear in LICS 2019, 2019. Google Scholar
  9. Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. A Categorical Semantics of Signal Flow Graphs. In CONCUR 2014, pages 435-450, 2014. Google Scholar
  10. Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. Full Abstraction for Signal Flow Graphs. In POPL 2015, pages 515-526, 2015. Google Scholar
  11. Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. The Calculus of Signal Flow Diagrams I: Linear relations on streams. Inf. Comput., 252:2-29, 2017. URL: https://doi.org/10.1016/j.ic.2016.03.002.
  12. Filippo Bonchi, Pawel Sobociński, and Fabio Zanasi. Deconstructing Lawvere with distributive laws. J. Log. Algebr. Meth. Program., 95:128-146, 2018. URL: https://doi.org/10.1016/j.jlamp.2017.12.002.
  13. Marcello M. Bonsangue, Helle Hvid Hansen, Alexander Kurz, and Jurriaan Rot. Presenting Distributive Laws. In Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings, pages 95-109, 2013. Google Scholar
  14. Roberto Bruni, Ugo Montanari, Gordon D. Plotkin, and Daniele Terreni. On Hierarchical Graphs: reconciling Bigraphs, Gs-monoidal Theories and Gs-graphs. Fundam. Inform., 134(3-4):287-317, 2014. Google Scholar
  15. Maria Grazia Buscemi and Ugo Montanari. A First Order Coalgebraic Model of pi-Calculus Early Observational Equivalence. In Lubos Brim, Petr Jancar, Mojmír Kretínský, and Antonín Kucera, editors, CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, volume 2421 of Lecture Notes in Computer Science, pages 449-465. Springer, 2002. URL: https://doi.org/10.1007/3-540-45694-5_30.
  16. Luca Cardelli and Andrew D. Gordon. Mobile ambients. Theor. Comput. Sci., 240(1):177-213, 2000. Google Scholar
  17. Giuseppe Castagna, Jan Vitek, and Francesco Zappa Nardelli. The Seal Calculus. Inform. Comput., 201(1):1-54, 2005. Google Scholar
  18. Bob Coecke and Ross Duncan. Interacting Quantum Observables. In ICALP 2008, pages 298-310, 2008. Google Scholar
  19. Robert De Simone. Higher-level synchronising devices in Meije-SCCS. Theor. Comput. Sci., 37:245-267, 1985. Google Scholar
  20. Pierpaolo Degano and Ugo Montanari. A model for distributed systems based on graph rewriting. J. ACM, 34(2):411-449, 1987. Google Scholar
  21. Brendan Fong, Paolo Rapisarda, and Paweł Sobociński. A categorical approach to open and interconnected dynamical systems. In LICS 2016, pages 1-10, 2016. Google Scholar
  22. Brendan Fong and David I. Spivak. Hypergraph Categories. CoRR, abs/1806.08304, 2018. URL: http://arxiv.org/abs/1806.08304.
  23. Fabio Gadducci and Ugo Montanari. The tile model. In Proof, Language and Interaction: Essays in Honour of Robin Milner, pages 133-166. MIT Press, 2000. Google Scholar
  24. Dan R. Ghica. Diagrammatic Reasoning for Delay-Insensitive Asynchronous Circuits. In Abramsky Festschrift, pages 52-68, 2013. URL: https://doi.org/10.1007/978-3-642-38164-5_5.
  25. Jan Friso Groote. Transition system specifications with negative premises. Theor. Comput. Sci., 118(2):263-299, 1993. Google Scholar
  26. David Harel. Statecharts: A visual formalism for complex systems. Sci. Comput. Program., 8(3):231-274, 1987. Google Scholar
  27. C. A. R. Hoare. Communicating Sequential Processes. Commun. ACM, 21(8):666-677, August 1978. Google Scholar
  28. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Inc., 1985. Google Scholar
  29. Martin Hyland and John Power. Lawvere theories and monads. In Computation, Meaning, and Logic, pages 437-458, 2007. Google Scholar
  30. Kurt Jensen. Coloured Petri nets: basic concepts, analysis methods and practical use, volume 1. Springer Science & Business Media, 2013. Google Scholar
  31. Piergiulio Katis, Nicoletta Sabadini, and Robert Frank Carslaw Walters. Span(Graph): an algebra of transition systems. In AMAST 1997, volume 1349 of LNCS, pages 322-336. Springer, 1997. URL: https://doi.org/10.1007/bfb0000479.
  32. Bartek Klin. Bialgebras for structural operational semantics: an introduction. Theor. Comput. Sci., 412(38):5043-5069, 2011. Google Scholar
  33. Ivan Lanese and Ugo Montanari. Hoare vs Milner: Comparing Synchronizations in a Graphical Framework With Mobility. Electr. Notes Theor. Comput. Sci., 154(2):55-72, 2006. URL: https://doi.org/10.1016/j.entcs.2005.03.032.
  34. Marina Lenisa, John Power, and Hiroshi Watanabe. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electr. Notes Theor. Comput. Sci., 33:230-260, 2000. Google Scholar
  35. Saunders Mac Lane. Categorical Algebra. B. Am. Math. Soc., 71:40-106, 1965. Google Scholar
  36. Robin Milner. A Calculus of Communicating Systems. Springer-Verlag, 1982. Google Scholar
  37. Robin Milner. Calculi for synchrony and asynchrony. Theor. Comput. Sci., 25(3):267-310, 1983. Google Scholar
  38. Robin Milner. The space and motion of communicating agents. Cambridge University Press, 2009. Google Scholar
  39. Dusko Pavlovic. Quantum and classical structures in nondeterministic computation. In QI 2009, pages 143-157, 2009. Google Scholar
  40. Wolfgang Reisig. Petri nets: an introduction, volume 4. Springer Science & Business Media, 2012. Google Scholar
  41. Jurriaan Rot. Enhanced Coinduction. PhD thesis, University of Leiden, 2015. Google Scholar
  42. Davide Sangiorgi and David Walker. PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  43. Peter Selinger. A survey of graphical languages for monoidal categories. Springer Lecture Notes in Physics, 13(813):289-355, 2011. Google Scholar
  44. Paweł Sobociński. A non-interleaving process calculus for multi-party synchronisation. In ICE 2009, pages 87-98, 2009. URL: https://doi.org/10.4204/EPTCS.12.6.
  45. Daniele Turi and Gordon Plotkin. Towards a mathematical operational semantics. In LICS 1997, pages 280-291, 1997. 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