论文标题
关于COQ中量子电路的符号推理
Symbolic Reasoning about Quantum Circuits in Coq
论文作者
论文摘要
量子电路是一个计算单元，可将输入量子状态转换为输出状态。自然推理其行为的方法是明确计算由其实施的统一矩阵。但是，当量子位数增加时，矩阵维度会呈指数增长，并且计算变得棘手。 在本文中，我们提出了一种符号方法来推理量子电路。它基于一系列涉及对向量和矩阵的基本操作的法律。这种符号推理比显式推理更好，并且非常适合在COQ中自动化，如某些典型示例所示。
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.
