ReQWIRE: Reasoning about Reversible Quantum Circuits
ReQWIRE: Reasoning about Reversible Quantum Circuits
复制标题
ReQWIRE：可逆量子电路的推理
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Steve Zdancewic
中科院分区：
文献类型：
--
作者：
Robert Rand;Jennifer Paykin;Dong;Steve Zdancewic
常见的量子算法大量使用辅助：在某个状态初始化，然后返回到该状态并丢弃的划痕量子比特。现有的量子电路语言允许程序员断言量子位在被丢弃之前已经返回到|0>状态，从而允许进行一系列优化。然而，现有的语言不提供验证这些断言的工具，从而引入了潜在的错误来源。在本文中，我们提出了验证辅助在期望状态下被丢弃的方法，并使用这些方法实现了从经典函数到量子预言机的验证编译器。
Common quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit languages let programmers assert that a qubit has been returned to the |0> state before it is discarded, allowing for a range of optimizations. However, existing languages do not provide the tools to verify these assertions, introducing a potential source of errors. In this paper we present methods for verifying that ancillae are discarded in the desired state, and use these methods to implement a verified compiler from classical functions to quantum oracles.