一句话：首次提出并证明量子电路的完备等式理论，使两个电路表示同一酉映射当且仅当可由这些等式互相变换。
本文研究如何为量子电路建立一套完备的等式推理系统，即判断两个量子电路是否表示同一酉变换。作者提出一组电路等式，证明其既是可靠的也是完备的：两个电路表示相同酉映射，当且仅当可通过这些等式相互转换。证明依赖于多控门的性质——这些门由基本门定义——以及将量子电路编码为线性光学电路的方案，而线性光学电路已被证明具有完备的公理化。该工作为量子电路提供了首个完备等式理论，也为量子程序等价性验证与优化提供了等式推理基础。
We introduce the first complete equational theory for quantum circuits. More precisely, we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations. The proof is based on the properties of multi-controlled gates – that are defined using elementary gates – together with an encoding of quantum circuits into linear optical circuits, which have been proved to have a complete axiomatisation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{ClementHMPV23,
title = {A Complete Equational Theory for Quantum Circuits},
author = {Alexandre Clément and Nicolas Heurtel and Shane Mansfield and Simon Perdrix and Benoît Valiron},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175801}
}