D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation

TL;DR

D-Hammer is a novel tool that automates equational reasoning in labelled Dirac notation, streamlining proofs in quantum physics and computer science with an efficient, dependently-typed language and optimized implementation.

Contribution

It introduces the first automated proof support for labelled Dirac notation, combining a higher-order language with an efficient normalization algorithm.

Findings

Significantly outperforms existing tools like DiracDec on plain Dirac notation.

Supports complex, higher-order, dependently-typed expressions.

Demonstrates effectiveness on representative quantum notation examples.

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.