Pattern graph rewrite systems
Aleks Kissinger (University of Oxford), Alex Merry (University of, Oxford), Matvey Soloviev (University of Cambridge)

TL;DR
This paper introduces pattern graphs, an extension of string graphs, enabling the expression of infinite families of rewrite rules with reusable subgraphs, significantly enhancing automated reasoning in diagrammatic theories.
Contribution
It extends string graph formalism to pattern graphs with !-boxes, allowing for more powerful and flexible graph rewriting systems for categorical quantum mechanics.
Findings
Pattern graphs can represent infinite rule families.
Pattern rewrite rules can be instantiated to concrete string graphs.
Demonstrated applications in categorical quantum mechanics.
Abstract
String diagrams are a powerful tool for reasoning about physical processes, logic circuits, tensor networks, and many other compositional structures. Dixon, Duncan and Kissinger introduced string graphs, which are a combinatoric representations of string diagrams, amenable to automated reasoning about diagrammatic theories via graph rewrite systems. In this extended abstract, we show how the power of such rewrite systems can be greatly extended by introducing pattern graphs, which provide a means of expressing infinite families of rewrite rules where certain marked subgraphs, called !-boxes ("bang boxes"), on both sides of a rule can be copied any number of times or removed. After reviewing the string graph formalism, we show how string graphs can be extended to pattern graphs and how pattern graphs and pattern rewrite rules can be instantiated to concrete string graphs and rewrite…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
