Automating Equational Proofs in Dirac Notation

TL;DR

The first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski’s theorem, and it is proved that validity of equations can be decided efficiently, using term-rewriting techniques.

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.

Figures (13)

• Figure 1: Proof snippet of HHL algorithm in Quantum Hoare Logic. The snippet is taken from Zhou2023. Every application of structural rule (e.g., unitary) is interleaved with equational reasoning on Dirac notation. This example illustrates the prominence of equational reasoning.
• Figure 3: The inference rules of equational logic. $v(s)$ and $v(t)$ represent the result after substitution $v$. $f$ is an arbitrary symbol in the signature.
• Figure 4: Typing rules for DN.
• Figure 5: Denotational semantics of DN expressions. Symbol $D$ represents appropriate terms from the ket, bra, or operator sorts. As introduced in \ref{['sec:introduction-to-dirac-notation']}, states in ${\mathcal{H}}$ are represented by column vector, co-states in ${\mathcal{H}}^*$ by row vector, then all $\cdot$ above are interpreted as matrix multiplications, while $\otimes$ as Kronecker products.
• Figure 6: Axiomatic semantics of DN. Associativity is marked in blue, and commutativity is marked in red. Symbol $D$ represents appropriate terms from the ket, bra, or operator sorts. The type annotations for $\mathbf{0}$ and $\mathbf{1}$ follow the typing rule and are omitted here. The symbol $\vdash_{A_\textsf{DN}}$ is omitted for the axioms without conditions.

Theorems & Definitions (66)

• definition 1: Derivable equation and formula
• definition 2: Types
• definition 3: Expressions
• definition 4
• definition 5: Interpretation of types
• definition 6: Semantics of expressions
• definition 7
• lemma 1: Soundness of denotational semantics
• definition 8
• lemma 2: soundness of axiomatic semantics