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）该完备等式理论可扩展至含有辅助量子比特或量子比特丢弃的量子电路，分别用于表示使用额外工作空间的量子计算以及混合量子计算。我们证明，在这些更具表达性的设定中，剩余的那个复杂规则可以极大简化，从而得到所有等式均作用于有界数量量子比特的等式理论。为高表达性量子电路模型建立简洁完备的等式理论，为量子电路推理开辟了新途径，并为电路优化、硬件约束满足与验证等多种编译任务提供了坚实的形式化基础。