A First-order Logic for String Diagrams

Authors Aleks Kissinger, David Quick

Thumbnail PDF


  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Aleks Kissinger
David Quick

Cite AsGet BibTex

Aleks Kissinger and David Quick. A First-order Logic for String Diagrams. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 171-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation. While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes. In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic with conjunction, implication, and universal quantification over !-boxes. This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes. We then build a standard model for !L and give an example proof of a theorem for non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone.
  • string diagrams
  • compact closed monoidal categories
  • abstract tensor systems
  • first-order logic


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


  1. John C. Baez and Jason Erbele. Categories in control. Technical report, arXiv:1405.6881, 2014. Google Scholar
  2. F. Bonchi, P. Sobocinski, and F. Zanasi. A categorical semantics of signal flow graphs. In CONCUR'14: Concurrency Theory., volume 8704 of Lecture Notes in Computer Science, pages 435-450. Springer, 2014. Google Scholar
  3. B. Coecke. Quantum picturalism. Contemporary Physics, 51:59-83, 2009. arXiv:0908.1787. Google Scholar
  4. B. Coecke and R. Duncan. Interacting quantum observables. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, 2008. Google Scholar
  5. B. Coecke, R. Duncan, A. Kissinger, and Q. Wang. Strong complementarity and non-locality in categorical quantum mechanics. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 2012. arXiv:1203.4988. Google Scholar
  6. Lucas Dixon and Ross Duncan. Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation. AISC/MKM/Calculemus, pages 77-92, 2008. Google Scholar
  7. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129-146. Springer Berlin Heidelberg, 1999. Google Scholar
  8. Andre Joyal and Ross Street. The geometry of tensor calculus I. Advances in Mathematics, 88:55-113, 1991. Google Scholar
  9. D. Kartsaklis. Compositional Distributional Semantics with Compact Closed Categories and Frobenius Algebras. PhD thesis, University of Oxford, 2014. Google Scholar
  10. Aleks Kissinger. Abstract tensor systems as monoidal categories. In C Casadio, B Coecke, M Moortgat, and P Scott, editors, Categories and Types in Logic, Language, and Physics: Festschrift on the occasion of Jim Lambek’s 90th birthday, volume 8222 of Lecture Notes in Computer Science. Springer, 2014. arXiv:1308.3586 [math.CT]. Google Scholar
  11. Aleks Kissinger, Alex Merry, and Matvey Soloviev. Pattern graph rewrite systems. In Proceedings of DCM 2012, volume 143 of EPTCS, 2012. arXiv:1204.6695 [math.CT]. Google Scholar
  12. Aleks Kissinger and David Quick. Tensors, !-graphs, and non-commutative quantum structures. In Proceedings of the 11th workshop on Quantum Physics and Logic, QPL 2014, Kyoto, Japan, 4-6th June 2014., pages 56-67, 2014. arXiv:1412.8552 [cs.LO]. Google Scholar
  13. Aleks Kissinger and David Quick. Tensors, !-graphs, and non-commutative quantum structures (extended version), 2015. arXiv:1503.01348. Google Scholar
  14. Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning, 2015. arXiv:1503.01034. Google Scholar
  15. Alexander Merry. Reasoning with !-Graphs. PhD thesis, University of Oxford, 2014. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail