一句话：为 Sum-Over-Paths 提出新重写规则，并证明其在 Toffoli-Hadamard 及二进量子片段上的完备性。
本文研究用于符号化操作量子系统线性映射的 Sum-Over-Paths 形式及其重写系统。作者给出一组新的重写规则，并借助 Sum-Over-Paths 与图形语言 ZH-calculus 的联系，证明该规则集对 Toffoli-Hadamard 这一最简单的近似通用量子片段是完备的；同时证明重写终止但不合流，这与该片段的通用性相符。文中还给出规则的推广及图形解释，并将系统扩展至由加入二进 π 倍数相位门得到的二进片段（如量子傅里叶变换所用），以保持完备性。最后，作者说明如何对任意项进行求和与连接，从而支持基于哈密顿量的量子计算分析。
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.
@article{paperbot2772,
title = {Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing},
author = {Renaud Vilmart},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:20)2024}
}