D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation

TL;DR

The paper tackles the challenge of automated equational reasoning in labelled Dirac notation, aimed at simplifying and verifying identities in quantum state descriptions and quantum programs. It introduces D-Hammer, a dependently typed, higher‑order language and proof system with a rigorous denotational semantics and a high-performance normalization procedure, implemented in C++. Empirical evaluation shows that D-Hammer outperforms the prior DiracDec tool on plain Dirac notation and can handle complex labelled Dirac notation examples, including those from quantum separation logic. The work advances automated reasoning in quantum formalisms, enabling scalable, reproducible proofs and facilitating integration with broader formal verification workflows.

Abstract

Labelled Dirac notation is a formalism commonly used by physicists to represent many-body quantum systems and by computer scientists to assert properties of quantum programs. It is supported by a rich equational theory for proving equality between expressions in the language. These proofs are typically carried on pen-and-paper, and can be exceedingly long and error-prone. We introduce D-Hammer, the first tool to support automated equational proof for labelled Dirac notation. The salient features of D-Hammer include: an expressive, higher-order, dependently-typed language for labelled Dirac notation; an efficient normalization algorithm; and an optimized C++ implementation. We evaluate the implementation on representative examples from both plain and labelled Dirac notation. In the case of plain Dirac notation, we show that our implementation significantly outperforms DiracDec.