一句话：为 ZX-Calculus 建立 Clifford+T 乃至无限制片段的完备公理化，并给出简化版本。
本文研究量子图示语言 ZX-Calculus 的完备性，即其等式理论能否捕捉所有量子力学推理。作者首先在已知完备的 Clifford 片段公理系统上增加公理，并借助与另一种完备图示语言之间的双向翻译，证明所得公理化对第一个近似通用片段 Clifford+T 完备。随后证明该公理系统的表达力超出 Clifford+T，可覆盖所谓的带 Clifford+T 常量的线性图。作者再利用该第三方语言的另一版本及适配的双向翻译，为无限制的完整 ZX-Calculus 建立完备公理化。文中还简要讨论新增公理，并为加入额外生成元的修改版语言给出更简单的完备公理化。
The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation for the so-called Clifford fragment of the language - a restriction that is not universal - by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T. We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language - and an adapted system of back-and-forth translation - to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1903-06035,
title = {Completeness of the ZX-Calculus},
author = {Emmanuel Jeandel and Simon Perdrix and Renaud Vilmart},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 2},
year = {2020},
doi = {10.23638/lmcs-16(2:11)2020}
}