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演算之间的联系实现上述证明，并展示了该公理化系统如何转化为ZH演算。我们还对提出的重写规则进行了泛化，这些泛化在实际化简项时可能发挥重要作用，并说明了如何从图形角度理解这些新规则。我们展示了如何丰富重写系统，使其对量子计算的二元片段达到完备性——这些片段特别用于量子傅里叶变换，通过向Toffoli-Hadamard门集合添加二元倍数π的相位门得到。最后，我们展示了如何执行任意项的求和与拼接操作，这在基于门量子计算分析设计的系统中非原生功能，但在处理基于哈密顿量的量子计算时却是必需的。