Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
arXiv:2307.14223 · doi:10.46298/lmcs-20(1:20)2024
Abstract
The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear maps that describe quantum systems, and is a tool that is used in formal verification of such systems. We give here a new set of rewrite rules for the formalism, and show that it is complete for "Toffoli-Hadamard", the simplest approximately universal fragment of quantum mechanics. We show that the rewriting is terminating, but not confluent (which is expected from the universality of the fragment). We do so using the connection between Sum-over-Paths and graphical language ZH-calculus, and also show how the axiomatisation translates into the latter. We provide generalisations of the presented rewrite rules, that can prove useful when trying to reduce terms in practice, and we show how to graphically make sense of these new rules. We show how to enrich the rewrite system to reach completeness for the dyadic fragments of quantum computation, used in particular in the Quantum Fourier Transform, and obtained by adding phase gates with dyadic multiples of to the Toffoli-Hadamard gate-set. Finally, we show how to perform sums and concatenation of arbitrary terms, something which is not native in a system designed for analysing gate-based quantum computation, but necessary when considering Hamiltonian-based quantum computation.
arXiv commentarXiv admin note: text overlap with arXiv:2205.02600
References in corpus (15)
- Improved Simulation of Stabilizer Circuits
- Reducing T-count with the ZX-calculus
- A Simple Proof that Toffoli and Hadamard are Quantum Universal
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Interacting Hopf Algebras: the theory of linear systems
- Hypergraph Simplification: Linking the Path-sum Approach to the ZH-calculus
- A ZX-Calculus with Triangles for Toffoli-Hadamard, Clifford+T, and Beyond
- How to Sum and Exponentiate Hamiltonians in ZXW Calculus
- Formal Methods for Quantum Programs: A Survey
- Completeness of the ZH-calculus
- Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes
- Completeness of the Phase-free ZH-calculus
- Catalytic Embeddings of Quantum Circuits