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. Our contribution is twofold: (i) We simplify this 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) We extend the complete equational theory 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. 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）我们将完备等式理论扩展至带辅助比特或量子比特丢弃的量子电路，分别用于表示使用额外工作空间的量子计算与混合量子计算。我们证明，在这些更具表达力的设定下，剩余复杂规则可被大幅简化。为表达力丰富的量子电路模型建立简洁完备的等式理论，为量子电路推理开辟了新途径。这为电路优化、硬件约束满足及验证等多种编译任务提供了坚实的理论基础。