论文标题
ZX-Calculus的完整性
Completeness of the ZX-calculus
论文作者
论文摘要
ZX-Calculus是一种直观但在数学上严格的量子计算的图形语言，这对于量子电路的框架特别有力。 ZX-Calculus的完整性意味着任何具有$ n $的尺寸功率的矩阵都可以纯粹地衍生出$ n $。在本论文中，我们通过从另一种用于量子计算的图形语言的完整性结果的翻译（ZW-Calculus）的翻译结果给出了第一个完整的公理化。这为自动图形量子计算铺平了道路，借助某些软件（例如Quantomatic）。基于这种普遍的完整性，我们直接获得了Clifford+t量子力学的ZX-Calculus的完整公理化，该机制近似于通用量子计算，通过将复数环限制在与clifford+t片段相对应的ZW-calculus for the zw-calculus for pulincalculus for uniperary环的完整性上。此外，我们通过验证图解重写中的17个电路关系的完整集，证明了2 Qubit Clifford+T电路的ZX-Calculus（仅有9个规则）的完整性。除了与Qubit相关的形式主义中的完整结果外，我们还将Qubit稳定器量子力学的ZX-Calculus的完整性扩展到QUTRIT稳定器系统。最后，我们用一些示例显示了ZX-Calculus在广义补充性的证明中的应用，纠缠分类和Toffoli Gate的表示以及对UMA Gate的等价检查。
The ZX-calculus is an intuitive but also mathematically strict graphical language for quantum computing, which is especially powerful for the framework of quantum circuits. Completeness of the ZX-calculus means any equality of matrices with size powers of $n$ can be derived purely diagrammatically. In this thesis, we give the first complete axiomatisation the ZX-calculus for the overall pure qubit quantum mechanics, via a translation from the completeness result of another graphical language for quantum computing -- the ZW-calculus. This paves the way for automated pictorial quantum computing, with the aid of some software like Quantomatic. Based on this universal completeness, we directly obtain a complete axiomatisation of the ZX-calculus for the Clifford+T quantum mechanics, which is approximatively universal for quantum computing, by restricting the ring of complex numbers to its subring corresponding to the Clifford+T fragment resting on the completeness theorem of the ZW-calculus for arbitrary commutative ring. Furthermore, we prove the completeness of the ZX-calculus (with just 9 rules) for 2-qubit Clifford+T circuits by verifying the complete set of 17 circuit relations in diagrammatic rewriting. In addition to completeness results within the qubit related formalism, we extend the completeness of the ZX-calculus for qubit stabilizer quantum mechanics to the qutrit stabilizer system. Finally, we show with some examples the application of the ZX-calculus to the proof of generalised supplementarity, the representation of entanglement classification and Toffoli gate, as well as equivalence-checking for the UMA gate.
