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.

翻译：“路径求和”形式化方法是一种符号化操控描述量子系统的线性映射的方式，也是该类系统形式化验证中使用的工具。本文给出该形式化方法的一组新改写规则，并证明其对“Toffoli-Hadamard”这一量子力学中最简单的近似通用片段具有完备性。我们证明该改写过程是终止的，但非合流（这由该片段的通用性所预期）。我们借助路径求和与图形化语言ZH演算之间的联系完成上述证明，同时展示该公理化如何转化至后者。我们给出了所提出改写规则的推广形式，这些推广在实际化简项时可能证明有用，并展示了如何从图形角度理解这些新规则。我们进一步说明如何丰富改写系统，使其对量子计算中（尤其在量子傅里叶变换中使用的）二元片段达到完备性——这些片段通过在Toffoli-Hadamard门集基础上添加相位门（相位为$\pi$的二元倍数）获得。最后，我们展示了如何对任意项执行求和与拼接操作——这一功能在设计用于分析基于门电路的量子计算的系统中并非原生支持，但在考虑基于哈密顿量的量子计算时却不可或缺。