一句话：证明稳定子 ZX 演算多数重写规则必要，仅两条必要性待定；并表明辫式自治范畴足以恢复“仅连通性重要”元规则。
稳定子 ZX 演算是用于量子力学推理的严格图形语言，具有可靠性与完备性：两张图表示同一量子演化或状态，当且仅当可由图形重写规则互相变换。作者此前已通过减少重写规则数量简化了该演算而不失完备性。本文进一步研究这些剩余规则是否都必要，证明其中大多数确实必要，但留下两条规则的必要性作为开放问题；令人意外的是，其中之一是作为互补性公理化、ZX 演算基石的 bialgebra 规则。文章还表明，采用比通常紧致闭范畴更弱的辫式自治范畴作为环境范畴，即便不假设生成元的对称性，也足以恢复“仅连通性重要”这一元规则。
The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics. The language is sound and complete: one can transform a stabilizer ZX-diagram into another one using the graphical rewrite rules if and only if these two diagrams represent the same quantum evolution or quantum state. We previously showed that the stabilizer ZX-calculus can be simplified by reducing the number of rewrite rules, without losing the property of completeness [Backens, Perdrix & Wang, EPTCS 236:1--20, 2017]. Here, we show that most of the remaining rules of the language are indeed necessary. We do however leave as an open question the necessity of two rules. These include, surprisingly, the bialgebra rule, which is an axiomatisation of complementarity, the cornerstone of the ZX-calculus. Furthermore, we show that a weaker ambient category -- a braided autonomous category instead of the usual compact closed category -- is sufficient to recover the meta rule 'only connectivity matters', even without assuming any symmetries of the generators.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1709-08903,
title = {Towards a Minimal Stabilizer ZX-calculus},
author = {Miriam Backens and Simon Perdrix and Quanlong Wang},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:19)2020}
}