Skip to main content
SpringerLink
Log in

Equational Reasoning with Context-Free Families of String Diagrams

  • Conference paper
  • First Online:
Graph Transformation (ICGT 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9151))

Included in the following conference series:

Abstract

String diagrams provide an intuitive language for expressing networks of interacting processes graphically. A discrete representation of string diagrams, called string graphs, allows for mechanised equational reasoning by double-pushout rewriting. However, one often wishes to express not just single equations, but entire families of equations between diagrams of arbitrary size. To do this we define a class of context-free grammars, called B-ESG grammars, that are suitable for defining entire families of string graphs, and crucially, of string graph rewrite rules. We show that the language-membership and match-enumeration problems are decidable for these grammars, and hence that there is an algorithm for rewriting string graphs according to B-ESG rewrite patterns. We also show that it is possible to reason at the level of grammars by providing a simple method for transforming a grammar by string graph rewriting, and showing admissibility of the induced B-ESG rewrite pattern.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    For colourability and cliques in string diagrams, we treat chains of wire-vertices as single edges.

References

  1. Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of 19th IEEE Symposium on Logic in Computer Science (2004)

    Google Scholar 

  2. Backens, M.: The zx-calculus is complete for stabilizer quantum mechanics. In: Proceedings of 9th Workshop on Quantum Physics and Logic QPL 2012 (2012)

    Google Scholar 

  3. Baez, J.C., Erbele, J.: Categories in control (2014). arXiv:1405.6881

  4. Bonchi, F., Sobociński, P., Zanasi, F.: Full abstraction for signal flow graphs. In: Principles of Programming Languages POPL 2015 (2015)

    Google Scholar 

  5. Coecke, B.: Quantum picturalism. Contemp. Phys. 51(1), 59–83 (2010)

    Article  Google Scholar 

  6. Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New J. Phys. 13(4), 043016 (2011)

    Article  MathSciNet  Google Scholar 

  7. Coecke, B., Duncan, R., Kissinger, A., Wang, Q.: Strong complementarity and non-locality in categorical quantum mechanics. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (2012)

    Google Scholar 

  8. Coecke, B., Grefenstette, E., Sadrzadeh, M.: Lambek vs. lambek: functorial vector space semantics and string diagrams for lambek calculus. Ann. Pure Appl. Log. 164(11), 1079–1100 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  9. Coecke, B., Kissinger, A.: The compositional structure of multipartite quantum entanglement. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 297–308. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Dixon, L., Kissinger, A.: Open-graphs and monoidal theories. Math. Struct. Comput. Sci. 23(4), 308–359 (2013)

    Article  MathSciNet  Google Scholar 

  11. Duncan, R., Perdrix, S.: Graph states and the necessity of euler decomposition. In: Ambos-Spies, K., Löwe, B., Merkle, W. (eds.) CiE 2009. LNCS, vol. 5635, pp. 167–177. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Joyal, A., Street, R.: The geometry of tensor calculus, i. Adv. Math. 88(1), 55–112 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kissinger, A., Merry, A., Soloviev, M.: Pattern graph rewrite systems. In: 8th International Workshop on Developments in Computational Models (2012)

    Google Scholar 

  14. Kissinger, A., Zamdzhiev, V.: !-graphs with trivial overlap are context-free. In: Rensink, A., Zambon, E. (eds.) Proceedings Graphs as Models, GaM 2015, London, UK, 11-12 April 2015, vol. 181. pp. 16–31 (2015). doi:10.4204/EPTCS.181.2

  15. Kissinger, A., Zamdzhiev, V.: Quantomatic: a proof assistant for diagrammatic reasoning (2015). arXiv:1503.01034

  16. Pratt, T.W.: Pair grammars, graph languages and string-to-graph translations. J. Comput. Syst. Sci. 5(6), 560–595 (1971)

    Article  MathSciNet  MATH  Google Scholar 

  17. Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1. World Scientific, Singapore (1997)

    Book  Google Scholar 

  18. Rozenberg, G., Welzl, E.: Boundary NLC graph grammars-basic definitions, normal forms, and complexity. Inf. Control 69(1–3), 136–167 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  19. Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) GTTCCS. LNCS. Springer, Heidelberg (1995)

    Google Scholar 

  20. Sobociński, P.: Representations of petri net interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 554–568. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Acknowledgements

We would like to thank the anonyomous reviewers for their feedback. We also gratefully acknowledge financial support from EPSRC, the Scatcherd European Scholarship, and the John Templeton Foundation.

Author information

Authors and Affiliations

  1. University of Oxford, Oxford, UK

    Aleks Kissinger & Vladimir Zamdzhiev

Authors
  1. Aleks Kissinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vladimir Zamdzhiev
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vladimir Zamdzhiev .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Sapienza Università di Roma, Rome, Italy

    Francesco Parisi-Presicce

  2. Angewandte Informatik 1, Universität Bayreuth, Bayreuth, Germany

    Bernhard Westfechtel

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Kissinger, A., Zamdzhiev, V. (2015). Equational Reasoning with Context-Free Families of String Diagrams. In: Parisi-Presicce, F., Westfechtel, B. (eds) Graph Transformation. ICGT 2015. Lecture Notes in Computer Science(), vol 9151. Springer, Cham. https://doi.org/10.1007/978-3-319-21145-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-21145-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-21144-2

  • Online ISBN: 978-3-319-21145-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation