Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory. We improve this completeness result in two ways: (i) We simplify the equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings, leading to equational theories where all equations act on a bounded number of qubits. The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

翻译：尽管量子电路在量子计算领域已普及数十年，但首个完整的量子电路方程理论直至近期才被提出。完备性确保量子电路上所有真实方程均可从该方程理论推导得出。我们从两方面改进这一完备性结果：（i）通过证明若干规则可从剩余规则推导，简化该方程理论——特别是三个最复杂规则中的两个被移除，第三个规则得到轻微简化；（ii）该完备方程理论可扩展至带辅助量子比特或量子比特丢弃的量子电路，分别表征需额外工作空间的量子计算及混合量子计算。我们证明在这类更具表达力的设定中，剩余的复杂规则可大幅简化，从而得到所有方程仅作用于有界数量量子比特的方程理论。为表达力丰富的量子电路模型构建简洁完备的方程理论，为量子电路推理开辟了新途径，并为电路优化、硬件约束满足及验证等编译任务提供了坚实的形式化基础。