A quantum circuit is a computational unit that transforms an input quantum state to an output one. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

翻译：量子电路是一个将输入量子状态转换为输出状态的计算单位。 解释其行为的自然方法是明确计算其行为所执行的单一矩阵。 但是,当Qqits数量增加时,矩阵维度会成倍增长,计算就会变得难以操作。 在本文中,我们建议对量子电路进行象征性的推理。 它基于一小套法律,涉及对矢量器和矩阵进行一些基本操纵。 这个象征性推理尺度比明确的要好,并且非常适合在 Coq 中自动操作, 正如一些典型的例子所证明的。