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 $\pi$ 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.

翻译：“路径求和”形式化方法是一种符号化操作描述量子系统的线性映射的工具，常用于此类系统的形式化验证。本文为该形式化方法提供了一组新的重写规则，并证明该规则对量子力学中最简单的近似通用片段"托福利-哈达玛"是完备的。我们证明该重写系统是可终止的，但非合流（这源于该片段的通用性）。通过利用路径求和与图形化语言ZH演算之间的联系，我们展示了该公理化体系如何转化为后者。文中给出了所提重写规则的泛化形式，这些泛化在实际项化简中具有实用价值，并展示了如何以图形化方式理解这些新规则。我们进一步展示了如何丰富重写系统以实现量子计算对偶片段的完备性——该片段特别应用于量子傅里叶变换，通过在托福利-哈达玛门集上添加$\pi$的对偶倍数相位门获得。最后，我们展示了如何对任意项进行求和与拼接操作——这在专为分析基于门的量子计算设计的系统中并非原生功能，但在考虑基于哈密顿量的量子计算时必不可少。