Automating Equational Proofs in Dirac Notation
arXiv:2411.11617 · doi:10.1145/3704878
Abstract
Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the perspective of automated reasoning. We prove two main results: first, the first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski's theorem. Then, we prove that validity of equations can be decided efficiently, using term-rewriting techniques. We implement our equivalence checking algorithm in Mathematica, and showcase its efficiency across more than 100 examples from the literature.
61 pages, 14 figures, extending the article accepted at POPL'25, artifacts available at https://zenodo.org/records/13995586
References in corpus (21)
- Quantum algorithm for solving linear systems of equations
- Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- PyZX: Large Scale Automated Diagrammatic Reasoning
- A Verified Optimizer for Quantum Circuits
- QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity
- Quantum Relational Hoare Logic
- A Deductive Verification Framework for Circuit-building Quantum Programs
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
- Formal Verification of Quantum Programs: Theory, Tools and Challenges
- Lineal: A linear-algebraic Lambda-calculus
- symQV: Automated Symbolic Verification of Quantum Programs
- Quantitative Robustness Analysis of Quantum Programs (Extended Version)
- Relational Proofs for Quantum Programs
- Certified Quantum Computation in Isabelle/HOL
- Proving Quantum Programs Correct
- Two linearities for quantum computing in the lambda calculus
- Realizability in the Unitary Sphere
- Completeness for arbitrary finite dimensions of ZXW-calculus, a unifying calculus
- Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes