ZX-Calculus and Extended Wolfram Model Systems II: Fast Diagrammatic Reasoning with an Application to Quantum Circuit Simplification

This article presents a novel algorithmic methodology for performing automated diagrammatic deductions over combinatorial structures, using a combination of modified equational theorem-proving techniques and the extended Wolfram model hypergraph rewriting formalism developed by the authors in previous work. We focus especially upon the application of this new algorithm to the problem of automated circuit simplification in quantum information theory, using Wolfram model multiway operator systems combined with the ZX-calculus formalism for enacting fast diagrammatic reasoning over linear transformations between qubits. We show how to construct a generalization of the deductive inference rules for Knuth-Bendix completion in which equation matches are selected on the basis of causal edge density in the associated multiway system, before proceeding to demonstrate how to embed the higher-order logic of the ZX-calculus rules within this first-order equational framework. After showing explicitly how the (hyper)graph rewritings of both Wolfram model systems and the ZX-calculus can be effectively realized within this formalism, we proceed to exhibit comparisons of time complexity vs. proof complexity for this new algorithmic approach when simplifying randomly-generated Clifford circuits down to pseudo-normal form, as well as when reducing the number of T-gates in randomly-generated non-Clifford circuits, with circuit sizes ranging up to 3000 gates, illustrating that the method performs favorably in comparison with existing circuit simplification frameworks, and also exhibiting the approximately quadratic speedup obtained by employing the causal edge density optimization. Finally, we present a worked example of an automated proof of correctness for a simple quantum teleportation protocol, in order to demonstrate more clearly the internal operations of the theorem-proving procedure.