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) 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 semantics as a distributive law for that monad. As a proof of concept, we provide bialgebraic semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory).
Bialgebraic foundations for the operational semantics of string diagrams / Bonchi F.; Piedeleu R.; Sobocinski P.; Zanasi F.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - ELETTRONICO. - 281:(2021), pp. 104767.1-104767.33. [10.1016/j.ic.2021.104767]
Bialgebraic foundations for the operational semantics of string diagrams
Zanasi F.
2021
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) 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 semantics as a distributive law for that monad. As a proof of concept, we provide bialgebraic semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory).File | Dimensione | Formato | |
---|---|---|---|
main (13).pdf
accesso aperto
Tipo:
Postprint
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione - Non commerciale - Non opere derivate (CCBYNCND)
Dimensione
973.35 kB
Formato
Adobe PDF
|
973.35 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.