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$的二进倍数相位门得到，尤其在量子傅里叶变换中有所应用。最后，我们实现了任意项的求和与拼接运算——这在面向门基量子计算的分析系统中并非原生功能，却是研究哈密顿量量子计算所必需的。