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.
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.
Categorical quantum mechanics and the Wolfram model offer distinct but complementary approaches to studying the relationship between diagrammatic rewriting systems over combinatorial structures and the foundations of physics; the objective of the present article is to begin elucidating the formal correspondence between the two methodologies in the context of the ZX-calculus formalism of Coecke and Duncan for reasoning diagrammatically about linear maps between qubits. After briefly summarizing the relevant formalisms, and presenting a categorical formulation of the Wolfram model in terms of adhesive categories and double-pushout rewriting systems, we illustrate how the diagrammatic rewritings of the ZX-calculus can be embedded and realized within the broader context of Wolfram model multiway systems, and illustrate some of the capabilities of the software framework (ZXMultiwaySystem) that we have developed specifically for this purpose. Finally, we present a proof (along with an explicitly computed example) based on the methods of Dixon and Kissinger that the multiway evolution graphs and branchial graphs of the Wolfram model are naturally endowed with a monoidal structure based on rulial composition that is, furthermore, compatible with the monoidal product of ZX-diagrams.
Diagrammatic representations of quantum algorithms and circuits offer novel approaches to their design and analysis.In this work, we describe extensions of the ZX-calculus especially suitable for parameterized quantum circuits, in particular for computing observable expectation values as functions of or for fixed parameters, which are important algorithmic quantities in a variety of applications ranging from combinatorial optimization to quantum chemistry.We provide several new ZX-diagram rewrite rules and generalizations for this setting.In particular, we give formal rules for dealing with linear combinations of ZX-diagrams, where the relative complex-valued scale factors of each diagram must be kept track of, in contrast to most previously studied single-diagram realizations where these coefficients can be effectively ignored.This allows us to directly import a number useful relations from the operator analysis to ZX-calculus setting, including causal cone and quantum gate commutation rules.We demonstrate that the diagrammatic approach offers useful insights into algorithm structure and performance by considering several ansätze from the literature including realizations of hardware-efficient ansätze and QAOA.We find that by employing a diagrammatic representation, calculations across different ansätze can become more intuitive and potentially easier to approach systematically than by alternative means.Finally, we outline how diagrammatic approaches may aid in the design and study of new and more effective quantum circuit ansätze.
We present a completely new approach to quantum circuit optimisation, based on the ZX-calculus. We first interpret quantum circuits as ZX-diagrams, which provide a flexible, lower-level language for describing quantum computations graphically. Then, using the rules of the ZX-calculus, we give a simplification strategy for ZX-diagrams based on the two graph transformations of local complementation and pivoting and show that the resulting reduced diagram can be transformed back into a quantum circuit. While little is known about extracting circuits from arbitrary ZX-diagrams, we show that the underlying graph of our simplified ZX-diagram always has a graph-theoretic property called generalised flow, which in turn yields a deterministic circuit extraction procedure. For Clifford circuits, this extraction procedure yields a new normal form that is both asymptotically optimal in size and gives a new, smaller upper bound on gate depth for nearest-neighbour architectures. For Clifford+T and more general circuits, our technique enables us to to `see around' gates that obstruct the Clifford structure and produce smaller circuits than naïve `cut-and-resynthesise' methods.
Quantum computing is an emerging computational paradigm with the potential to outperform classical computers in solving a variety of problems. To achieve this, quantum programs are typically represented as quantum circuits, which must be optimized and adapted for target hardware through quantum circuit compilation. We introduce ZX-DB, a data-driven system that performs quantum circuit simplification and rewriting inside a graph database using ZX-calculus, a complete graphical formalism for quantum mechanics. ZX-DB encodes ZX-calculus rewrite rules as standard openCypher queries and executes them on an example graph database engine, Memgraph, enabling efficient, database-native transformations of large-scale quantum circuits. ZX-DB integrates correctness validation via tensor and graph equivalence checks and is evaluated against the state-of-the-art PyZX framework. Experimental results show that ZX-DB achieves up to an order-of-magnitude speedup for independent rewrites, while exposing pattern-matching bottlenecks in current graph database engines. By uniting quantum compilation and graph data management, ZX-DB opens a new systems direction toward scalable, database-supported quantum computing pipelines.
The ZX-calculus is an algebraic formalism that allows quantum computations to be simplified via a small number of simple graphical rewrite rules.Recently, it was shown that, when combined with a family of "sum-over-Cliffords" techniques, the ZX-calculus provides a powerful tool for classical simulation of quantum circuits.However, for several important classical simulation tasks, such as computing the probabilities associated with many measurement outcomes of a single quantum circuit, this technique results in reductions over many very similar diagrams, where much of the same computational work is repeated.In this paper, we show that the majority of this work can be shared across branches, by developing reduction strategies that can be run parametrically on diagrams with boolean free parameters.As parameters only need to be fixed after the bulk of the simplification work is already done, we show that it is possible to perform the final stage of classical simulation quickly utilising a high degree of GPU parallelism.Using these methods, we demonstrate an average speedup factor of 78.3 ± 10.2 for certain classical simulation tasks vs. the non-parametric approach.
While the quantum circuit model remains the dominant framework for representing and executing quantum algorithms, it is not always the most optimal framework for representing the quantum circuit’s deeper structure. In a standard circuit diagram, computation is shown mainly as a time ordered sequence of gates acting on qubit wires. ZX calculus, by contrast, represents the same process using two families of generators, the Z spiders and the X spiders, together with wires and Hadamard structure, so that algebraic identities, entanglement structure, and rewrite based simplifications become visible directly in the diagram itself. ZX calculus is not another visual representation for the same quantum circuit we have been using, but a graphical calculus in which diagrams carry both computational meaning and transformation rules. This is also the reason for the name ZX ; the formalism is built around the interaction between Z -type and X -type observables, phases, and basis changes. By turning matrix manipulations into diagrammatic rewrites, ZX calculus reduces much of the redundancies and abstract nature usually associated with quantum computation and provides a more structural language for understanding, optimizing, and verifying quantum processes.