This page provides an overview of the work done in the Automated Diagrammatic Reasoning theme, lists open problems and describes current work which is being undertaken.


Motivation


The ZX-calculus has been used to study and verify aspects of existing quantum protocols like Quantum Secret Sharing, Quantum Key Distribution and Superdense Coding, Quantum Direct Communication, Teleportation Protocols, Quantum Error Correcting Codes and others. Other diagrammatic languages, such as the GHZ/W calculus and the signal-flow calculus, can also be used to reason about their respective theories they represent.

However, manipulating large diagrams in these calculi manually is cumbersome and error-prone. The main motivation underpinning the work done in the Automated Diagrammatic Reasoning group is to develop formal theories, techniques and software tools to make this processes easier, less-error prone, more automated and verifiable.


Formal Theories


The ZX-calculus and other theories based on String Diagrams are described using certain topological notions which makes their formal representation in computer systems hard. In addition to that, describing rewriting schemas and families of diagrams using the familiar "dot-dot-dot" (…) notation is intuitive for people, but it is also informal and thus problematic for software implementations. As a result, the Automated Diagrammatic Reasoning group developed formal theories, like the theory of String Graphs and !-graphs which help to solve these problems.

String Graphs

String Graphs were originally introduced under the name "Open Graphs" in [1] [2]. Since then, the theory has been further developed and the term was changed to "String Graphs" in [3]. String Graphs are a discrete representation of String Diagrams and they were introduced in order to represent String Diagrams in a way that allows efficient automation by computer systems. String Diagrams were in turn introduced by Roger Penrose in [5] as a way to conveniently represent Abstract Tensor Systems.

!-graphs

!-graphs are an extension to String Graphs which allow for the formal representation of certain infinite families of diagrams.

!-graphs (pronounced bang graphs) were introduced in [4] under the name pattern graphs and were later renamed to their current name in Alex Merry’s DPhil thesis [6] which contains the most complete and detailed description of !-graphs.

A !-graph is a generalised string graph which allows us to represent infinite families of string graphs in a formal way. In addition to wire and box vertices, !-graphs also have a third type of vertices, called !-vertices. The edges coming out of a !-vertex determine a !-box whose contents can be copied infinitely many times (while preserving connection relations), thus allowing us to represent an infinite set of string graphs in a finite way.

The motivation behind !-graphs is to remove some of the informalities in expressing infinite families of rewrite rules and infinite families of diagrams using the "dot dot dot" (· · · ) notation in order to ease the development of software proof-assistants.


Current Research


The current theoretical research within this theme is done by Vladimir Zamdzhiev who is working on Graph Grammar extensions for String Graphs and David Quick who is working on non-commutative extensions for !-graphs. Aleks Kissinger is the main supervisor for both students.

Graph Grammar extensions for String Graphs

All quantum algorithms and many quantum protocols describe solutions for problems of variable sizes (the size of the input can be arbitrary large for example). In these cases, we have to reason about infinite classes of quantum operations. It is possible to do so in ZX using intuitive metalogical arguments, but this is not formal and implementing support for automated reasoning in software would be hard.

This limitation is partially addressed with !-graphs, which are also well implemented in Quantomatic. !-graphs represent infinite families of diagrams and !-graph rewrite rules allow us to reason about infite sets of graphs. However, there are important circuits and classes of circuits which cannot be represented with the help of this formalism (e.g. Quantum Fourier Transform on n qubits).

Naturally, we want to extend the formal expressive power of the ZX calculus (and other theories based on String Diagrams) and for that we have to consider more powerful structures. We believe that by using techniques from the Graph Grammar literature, we will be able to support reasoning for some classes of graphs that cannot be expressed using !-graphs.

For this reason, a suitable candidate for study is the class of context-free graph grammars and in particular, Vertex Replacement (VR) graph grammars. There certainly are more expressive kinds of graph grammars, but these grammars also have worse decidability, structural and complexity properties compared to VR grammars. It seems like a good idea to consider VR graph grammars first and identify interesting classes of diagrams which can be represented in such a way. This is the main body of proposed work for Vladimir Zamdzhiev's DPhil studies - designing a theory based around String Graphs and VR Graph Grammars with greater expresiveness compared to the theory of !-graphs.

This work is undertaken in the hope that it will lay down the mathematical foundations which are required to improve the automated reasoning capabilities and expressive power of proof assistants (like Quantomatic) so that they would be used more efficiently for the design and verification of (quantum) protocols and algorithms.

Non-commutative extensions for !-graphs

!-graphs were introduced as a way to reason with families of graphs in a more rigorous way than the informal 'dot dot dot' notation. The previous technique for reasoning with !-graphs was based on string graph representations, where edges attached to nodes do not have an order assigned to them. This limited its applications to commutative (or cocommutative) algebraic structures.

Since many topics of interest in categorical quantum mechanics and elsewhere rely on non-commutativity, we would like to extend the current graphical formalism to work with non-commutative diagrams. We refer to these families of diagrams as !-tensors. !-tensors allow nodes to have arbitrary arrangements of edges with fixed order.

One application of this is the ability to recursively define nodes of arbitrary arity from fixed arity nodes. This often allows us to replace an infinite class of diagram equations with a single !-tensor equation. Given recursively defined nodes we would then like to be able to prove diagrammatic equations involving them using induction. We are currently working on a natural deduction system to describe diagrammatic proof (with !-box induction).


Software Tools


The Quantomatic project is an initiative to develop software tools which help users work with string diagrams (e.g. ZX-calculus). The main software tool is called QuantoDerive (also known as Quantomatic). It has been developed with the goal to allow the user to perform human-guided and automated reasoning for the ZX-calculus and other theories based on String Diagrams.

The tool was successfully used for the verification of the 7-qubit Stean error-correcting code.

The main website of the project is: https://quantomatic.github.io/

Currently, there are three main subprojects.

QuantoDerive

QuantoDerive is the main GUI of the Quantomatic project. It provides a graphical interface which can be used to reason about String Diagram theories.

Overview of the features offered by QuantoDerive:

  • allows for diagram creation and manipulation, creating rewriting rules, performing diagrammatic reasoning using a system of rewriting rules
  • export to tikz/tikzit/LaTeX of graphs, derivations, rewriting rules, etc.
  • written in Scala and actively developed
  • easy to use and install (no compiling, just download zip/tarball and click on executable) on all platforms (GNU/Linux, OSX, Windows)
  • project is hosted on github and we make use of most of their fancy features — very easy to report bugs, complain, make suggestions, track how the project is going, etc.

QuantoCore

QuantoCore is the rewriting engine of the Quantomatic project. In a typical usage scenario, QuantoCore is controlled from the GUI (QuantoDerive) and the user doesn't directly interact with it. QuantoCore is the piece of software which does all of the complicated graph matching and rewriting operations which are then visualised by the GUI. It has been written in ML over many years.

QuantoTactic

QuantoTactic is a project idea which aims to bring integration of the Quantomatic components with standard theorem provers. The motivation behind this is to guarantee proof of correctness for derivations produced by Quantomatic. This is nice to have as Quantomatic is very complicated and large which means bugs are inevitable. In addition, such integration will also allow using theorem provers and their powerful tactics in order to search and discover proofs.

There is limited progress on the project and it is basically on hold for the time being

QuantoCoSy

QuantoCoSy is a small tool which generates rulesets from concrete models. It stands for "Conjecture Synthesis".


Papers


This is the list of all relevant papers for this line of research in historical order.


Talks


This is the list of all relevant talks for this line of research.


People



Bibliography
1. L. Dixon, R. Duncan, and A. Kissinger. Open Graphs and Computational Reasoning. Developments in Computational Models, 2010.
2. L. Dixon and A. Kissinger. Open Graphs and Monoidal Theories. 2010. http://arxiv.org/abs/1011.4114.
3. Aleks Kissinger. Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing. 2012. DPhil thesis. http://arxiv.org/abs/1203.0202.
4. Aleks Kissinger, Alex Merry, and Matvey Soloviev. Pattern graph rewrite systems. In Benedikt Löwe and Glynn Winskel, editors, Proceedings 8th International Workshop on Developments in Computational Models, Cambridge, United Kingdom, 17 June 2012, volume 143 of Electronic Proceedings in Theoretical Computer Science, pages 54–66. Open Publishing Association, 2012.
5. R. Penrose. Applications of negative dimensional tensors. In Combinatorial Mathematics and its Applications, pages 221–244. Academic Press, 1971.
6. Alexander Merry. Reasoning with !-Graphs. DPhil Thesis. 2014. http://arxiv.org/abs/1403.7828.