Synthesising Graphical Theories

TL;DR

This paper adapts conjecture synthesis to diagrammatic theories in monoidal categories, enabling automated generation of graphical identities, demonstrated through a theory for entangled quantum states.

Contribution

It introduces a method to automatically synthesize diagrammatic theories using graph rewrite systems, extending conjecture synthesis to this domain.

Findings

Successfully synthesised a graphical theory for entangled quantum states.

Demonstrated the method's ability to generate useful diagrammatic identities.

Extended conjecture synthesis technique to diagrammatic and graph rewrite systems.

Abstract

In recent years, diagrammatic languages have been shown to be a powerful and expressive tool for reasoning about physical, logical, and semantic processes represented as morphisms in a monoidal category. In particular, categorical quantum mechanics, or "Quantum Picturalism", aims to turn concrete features of quantum theory into abstract structural properties, expressed in the form of diagrammatic identities. One way we search for these properties is to start with a concrete model (e.g. a set of linear maps or finite relations) and start composing generators into diagrams and looking for graphical identities. Naively, we could automate this procedure by enumerating all diagrams up to a given size and check for equalities, but this is intractable in practice because it produces far too many equations. Luckily, many of these identities are not primitive, but rather derivable from simpler ones. In 2010, Johansson, Dixon, and Bundy developed a technique called conjecture synthesis for automatically generating conjectured term equations to feed into an inductive theorem prover. In this extended abstract, we adapt this technique to diagrammatic theories, expressed as graph rewrite systems, and demonstrate its application by synthesising a graphical theory for studying entangled quantum states.