40 Search Results for "Sobocinski, Pawel"

Volume

LIPIcs, Volume 35

6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands

Editors: Lawrence S. Moss and Pawel Sobocinski

Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2024.41
Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper)

Authors: Sam Ezeh

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We present Untangle, a Lean4 extension for Visual Studio Code that displays string diagrams for morphisms inside monoidal categories, allowing users to rewrite expressions by clicking on natural transformations and morphisms in the string diagram. When the the user manipulates the string diagram by clicking on natural transformations in the Graphical User Interface, it attempts to generate relevant tactics to apply which it then inserts into the editor, allowing the user to prove equalities visually by diagram rewriting.
Cite as

Sam Ezeh. Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 41:1-41:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ezeh:LIPIcs.ITP.2024.41,
  author =	{Ezeh, Sam},
  title =	{{Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{41:1--41:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.41},
  URN =		{urn:nbn:de:0030-drops-207690},
  doi =		{10.4230/LIPIcs.ITP.2024.41},
  annote =	{Keywords: Interactive theorem proving, Lean4, Graphical User Interface}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.5
The Flower Calculus

Authors: Pablo Donato

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce’s existential graphs. It works as a rewriting system over inductive objects called "flowers", that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.
Cite as

Pablo Donato. The Flower Calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{donato:LIPIcs.FSCD.2024.5,
  author =	{Donato, Pablo},
  title =	{{The Flower Calculus}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{5:1--5:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.5},
  URN =		{urn:nbn:de:0030-drops-203343},
  doi =		{10.4230/LIPIcs.FSCD.2024.5},
  annote =	{Keywords: deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.25
The Produoidal Algebra of Process Decomposition

Authors: Matt Earnshaw, James Hefford, and Mario Román

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

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

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)

Copy BibTex To Clipboard

@InProceedings{earnshaw_et_al:LIPIcs.CSL.2024.25,
  author =	{Earnshaw, Matt and Hefford, James and Rom\'{a}n, Mario},
  title =	{{The Produoidal Algebra of Process Decomposition}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.25},
  URN =		{urn:nbn:de:0030-drops-196688},
  doi =		{10.4230/LIPIcs.CSL.2024.25},
  annote =	{Keywords: monoidal categories, profunctors, lenses, duoidal categories}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.43
String Diagrammatic Trace Theory

Authors: Matthew Earnshaw and Paweł Sobociński

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We extend the theory of formal languages in monoidal categories to the multi-sorted, symmetric case, and show how this theory permits a graphical treatment of topics in concurrency. In particular, we show that Mazurkiewicz trace languages are precisely symmetric monoidal languages over monoidal distributed alphabets. We introduce symmetric monoidal automata, which define the class of regular symmetric monoidal languages. Furthermore, we prove that Zielonka’s asynchronous automata coincide with symmetric monoidal automata over monoidal distributed alphabets. Finally, we apply the string diagrams for symmetric premonoidal categories to derive serializations of traces.
Cite as

Matthew Earnshaw and Paweł Sobociński. String Diagrammatic Trace Theory. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 43:1-43:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{earnshaw_et_al:LIPIcs.MFCS.2023.43,
  author =	{Earnshaw, Matthew and Soboci\'{n}ski, Pawe{\l}},
  title =	{{String Diagrammatic Trace Theory}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{43:1--43:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.43},
  URN =		{urn:nbn:de:0030-drops-185770},
  doi =		{10.4230/LIPIcs.MFCS.2023.43},
  annote =	{Keywords: symmetric monoidal categories, Mazurkiewicz traces, asynchronous automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.44
Regular Monoidal Languages

Authors: Matthew Earnshaw and Paweł Sobociński

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We introduce regular languages of morphisms in free monoidal categories, with their associated grammars and automata. These subsume the classical theory of regular languages of words and trees, but also open up a much wider class of languages over string diagrams. We use the algebra of monoidal categories to investigate the properties of regular monoidal languages, and provide sufficient conditions for their recognizability by deterministic monoidal automata.
Cite as

Matthew Earnshaw and Paweł Sobociński. Regular Monoidal Languages. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 44:1-44:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{earnshaw_et_al:LIPIcs.MFCS.2022.44,
  author =	{Earnshaw, Matthew and Soboci\'{n}ski, Pawe{\l}},
  title =	{{Regular Monoidal Languages}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{44:1--44:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.44},
  URN =		{urn:nbn:de:0030-drops-168425},
  doi =		{10.4230/LIPIcs.MFCS.2022.44},
  annote =	{Keywords: monoidal categories, string diagrams, formal language theory, cartesian restriction categories}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.40
Diagrammatic Polyhedral Algebra

Authors: Filippo Bonchi, Alessandro Di Giorgio, and Paweł Sobociński

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
We extend the theory of Interacting Hopf algebras with an order primitive, and give a sound and complete axiomatisation of the prop of polyhedral cones. Next, we axiomatise an affine extension and prove soundness and completeness for the prop of polyhedra.
Cite as

Filippo Bonchi, Alessandro Di Giorgio, and Paweł Sobociński. Diagrammatic Polyhedral Algebra. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.FSTTCS.2021.40,
  author =	{Bonchi, Filippo and Di Giorgio, Alessandro and Soboci\'{n}ski, Pawe{\l}},
  title =	{{Diagrammatic Polyhedral Algebra}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.40},
  URN =		{urn:nbn:de:0030-drops-155511},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.40},
  annote =	{Keywords: String diagrams, Polyhedral cones, Polyhedra}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2021.10
On Doctrines and Cartesian Bicategories

Authors: Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We study the relationship between cartesian bicategories and a specialisation of Lawvere’s hyperdoctrines, namely elementary existential doctrines. Both provide different ways of abstracting the structural properties of logical systems: the former in algebraic terms based on a string diagrammatic calculus, the latter in universal terms using the fundamental notion of adjoint functor. We prove that these two approaches are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines.
Cite as

Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On Doctrines and Cartesian Bicategories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.10,
  author =	{Bonchi, Filippo and Santamaria, Alessio and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}},
  title =	{{On Doctrines and Cartesian Bicategories}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10},
  URN =		{urn:nbn:de:0030-drops-153656},
  doi =		{10.4230/LIPIcs.CALCO.2021.10},
  annote =	{Keywords: Cartesian bicategories, elementary existential doctrines, string diagram}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.30
Compositional Modelling of Network Games

Authors: Elena Di Lavore, Jules Hedges, and Paweł Sobociński

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
The analysis of games played on graph-like structures is of increasing importance due to the prevalence of social networks, both virtual and physical, in our daily life. As well as being relevant in computer science, mathematical analysis and computer simulations of such distributed games are vital methodologies in economics, politics and epidemiology, amongst other fields. Our contribution is to give compositional semantics of a family of such games as a well-behaved mapping, a strict monoidal functor, from a category of open graphs (syntax) to a category of open games (semantics). As well as introducing the theoretical framework, we identify some applications of compositionality.
Cite as

Elena Di Lavore, Jules Hedges, and Paweł Sobociński. Compositional Modelling of Network Games. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dilavore_et_al:LIPIcs.CSL.2021.30,
  author =	{Di Lavore, Elena and Hedges, Jules and Soboci\'{n}ski, Pawe{\l}},
  title =	{{Compositional Modelling of Network Games}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{30:1--30:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.30},
  URN =		{urn:nbn:de:0030-drops-134645},
  doi =		{10.4230/LIPIcs.CSL.2021.30},
  annote =	{Keywords: game theory, category theory, network games, open games, open graphs, compositionality}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.15
The Axiom of Choice in Cartesian Bicategories

Authors: Filippo Bonchi, Jens Seeber, and Paweł Sobociński

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
We argue that cartesian bicategories, often used as a general categorical algebra of relations, are also a natural setting for the study of the axiom of choice (AC). In this setting, AC manifests itself as an inequation asserting that every total relation contains a map. The generality of cartesian bicategories allows us to separate this formulation from other set-theoretically equivalent properties, for instance that epimorphisms split. Moreover, via a classification result, we show that cartesian bicategories satisfying choice tend to be those that arise from bicategories of spans.
Cite as

Filippo Bonchi, Jens Seeber, and Paweł Sobociński. The Axiom of Choice in Cartesian Bicategories. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2019.15,
  author =	{Bonchi, Filippo and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}},
  title =	{{The Axiom of Choice in Cartesian Bicategories}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.15},
  URN =		{urn:nbn:de:0030-drops-114439},
  doi =		{10.4230/LIPIcs.CALCO.2019.15},
  annote =	{Keywords: Cartesian bicategories, Axiom of choice, string diagrams}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.18
Nominal String Diagrams

Authors: Samuel Balco and Alexander Kurz

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
We introduce nominal string diagrams as string diagrams internal in the category of nominal sets. This requires us to take nominal sets as a monoidal category, not with the cartesian product, but with the separated product. To this end, we develop the beginnings of a theory of monoidal categories internal in a symmetric monoidal category. As an instance, we obtain a notion of a nominal PROP as a PROP internal in nominal sets. A 2-dimensional calculus of simultaneous substitutions is an application.
Cite as

Samuel Balco and Alexander Kurz. Nominal String Diagrams. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{balco_et_al:LIPIcs.CALCO.2019.18,
  author =	{Balco, Samuel and Kurz, Alexander},
  title =	{{Nominal String Diagrams}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.18},
  URN =		{urn:nbn:de:0030-drops-114466},
  doi =		{10.4230/LIPIcs.CALCO.2019.18},
  annote =	{Keywords: string diagrams, nominal sets, separated product, simultaneous substitutions, internal category, monoidal category, internal monoidal categories, PROP}
}
Document
Tool Paper
DOI: 10.4230/LIPIcs.CALCO.2019.20
CARTOGRAPHER: A Tool for String Diagrammatic Reasoning (Tool Paper)

Authors: Paweł Sobociński, Paul W. Wilson, and Fabio Zanasi

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
We introduce cartographer, a tool for editing and rewriting string diagrams of symmetric monoidal categories. Our approach is principled: the layout exploits the isomorphism between string diagrams and certain cospans of hypergraphs; the implementation of rewriting is based on the soundness and completeness of convex double-pushout rewriting for string diagram rewriting.
Cite as

Paweł Sobociński, Paul W. Wilson, and Fabio Zanasi. CARTOGRAPHER: A Tool for String Diagrammatic Reasoning (Tool Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 20:1-20:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sobocinski_et_al:LIPIcs.CALCO.2019.20,
  author =	{Soboci\'{n}ski, Pawe{\l} and Wilson, Paul W. and Zanasi, Fabio},
  title =	{{CARTOGRAPHER: A Tool for String Diagrammatic Reasoning}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{20:1--20:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.20},
  URN =		{urn:nbn:de:0030-drops-114482},
  doi =		{10.4230/LIPIcs.CALCO.2019.20},
  annote =	{Keywords: tool, string diagram, symmetric monoidal category, graphical reasoning}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.37
Bialgebraic Semantics for String Diagrams

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

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2019.37,
  author =	{Bonchi, Filippo and Piedeleu, Robin and Sobocinski, Pawel and Zanasi, Fabio},
  title =	{{Bialgebraic Semantics for String Diagrams}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.37},
  URN =		{urn:nbn:de:0030-drops-109398},
  doi =		{10.4230/LIPIcs.CONCUR.2019.37},
  annote =	{Keywords: String Diagram, Structural Operational Semantics, Bialgebraic semantics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.11
Rule Algebras for Adhesive Categories

Authors: Nicolas Behr and Pawel Sobocinski

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We show that every adhesive category gives rise to an associative algebra of rewriting rules induced by the notion of double-pushout (DPO) rewriting and the associated notion of concurrent production. In contrast to the original formulation of rule algebras in terms of relations between (a concrete notion of) graphs, here we work in an abstract categorical setting. Doing this, we extend the classical concurrency theorem of DPO rewriting and show that the composition of DPO rules along abstract dependency relations is, in a natural sense, an associative operation. If in addition the adhesive category possesses a strict initial object, the resulting rule algebra is also unital. We demonstrate that in this setting the canonical representation of the rule algebras is obtainable, which opens the possibility of applying the concept to define and compute the evolution of statistical moments of observables in stochastic DPO rewriting systems.
Cite as

Nicolas Behr and Pawel Sobocinski. Rule Algebras for Adhesive Categories. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{behr_et_al:LIPIcs.CSL.2018.11,
  author =	{Behr, Nicolas and Sobocinski, Pawel},
  title =	{{Rule Algebras for Adhesive Categories}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{11:1--11:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.11},
  URN =		{urn:nbn:de:0030-drops-96781},
  doi =		{10.4230/LIPIcs.CSL.2018.11},
  annote =	{Keywords: Adhesive categories, rule algebras, Double Pushout (DPO) rewriting}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.13
Graphical Conjunctive Queries

Authors: Filippo Bonchi, Jens Seeber, and Pawel Sobocinski

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The Calculus of Conjunctive Queries (CCQ) has foundational status in database theory. A celebrated theorem of Chandra and Merlin states that CCQ query inclusion is decidable. Its proof transforms logical formulas to graphs: each query has a natural model - a kind of graph - and query inclusion reduces to the existence of a graph homomorphism between natural models. We introduce the diagrammatic language Graphical Conjunctive Queries (GCQ) and show that it has the same expressivity as CCQ. GCQ terms are string diagrams, and their algebraic structure allows us to derive a sound and complete axiomatisation of query inclusion, which turns out to be exactly Carboni and Walters' notion of cartesian bicategory of relations. Our completeness proof exploits the combinatorial nature of string diagrams as (certain cospans of) hypergraphs: Chandra and Merlin's insights inspire a theorem that relates such cospans with spans. Completeness and decidability of the (in)equational theory of GCQ follow as a corollary. Categorically speaking, our contribution is a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations.
Cite as

Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CSL.2018.13,
  author =	{Bonchi, Filippo and Seeber, Jens and Sobocinski, Pawel},
  title =	{{Graphical Conjunctive Queries}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{13:1--13:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.13},
  URN =		{urn:nbn:de:0030-drops-96805},
  doi =		{10.4230/LIPIcs.CSL.2018.13},
  annote =	{Keywords: conjunctive query inclusion, string diagrams, cartesian bicategories}
}
  • Refine by Author
  • 7 Bonchi, Filippo
  • 7 Sobocinski, Pawel
  • 7 Sobociński, Paweł
  • 3 Kurz, Alexander
  • 3 Milius, Stefan
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 10 coalgebra
  • 6 string diagrams
  • 5 category theory
  • 3 bisimulation
  • 2 Cartesian bicategories
  • Show More...

  • Refine by Type
  • 39 document
  • 1 volume

  • Refine by Publication Year
  • 24 2015
  • 4 2019
  • 3 2021
  • 3 2024
  • 2 2018
  • Show More...

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 About DROPS Imprint Privacy Contact