量子计算二进片段中路径求和的重写与完备性

“路径求和”(Sum-Over-Paths)形式体系是一种符号化操作描述量子系统的线性映射的方法，也是此类系统形式化验证中的工具。我们在此给出该形式体系的一组新重写规则，并证明其对于“Toffoli-Hadamard”——量子力学中最简单的近似通用片段——是完备的。我们证明该重写是终止的，但非合流的（这由该片段的通用性所预期）。我们通过路径求和与图形语言ZH演算之间的联系做到这一点，并展示了该公理系统如何翻译至后者。我们给出了所呈重写规则的推广，在实践中试图化简项时可能有用，并展示了如何以图形方式理解这些新规则。我们展示了如何丰富重写系统以达成对量子计算二进片段的完备性，该片段尤其用于Quantum Fourier Transform，并通过向Toffoli-Hadamard门集添加$\pi$的二进倍数相位门获得。最后，我们展示了如何执行任意项的和与串接，这在为分析基于门的量子计算而设计的系统中并非原生功能，但在考虑基于哈密顿量的量子计算时是必需的。