一句话：形式化定义量子程序中脏量子比特借用的语义，提出安全反计算概念，并给出高效验证算法。
脏量子比特是指可从计算空闲部分借用的辅助量子比特，用于复用比特并减少对稀缺的干净量子比特的需求。但复用有效的条件是：脏量子比特的初始状态不能影响所在量子电路的功能，且使用后必须完全恢复其原始状态（包括纠缠），即安全反计算。本文形式化定义了量子编程语言中脏量子比特借用这一特性的语义，提出了量子程序中脏量子比特安全反计算的概念，并给出一种高效算法及实验结果，用于验证特定量子电路中脏量子比特的安全反计算。
Dirty qubits are ancillary qubits that can be borrowed from idle parts of a computation, enabling qubit reuse and reducing the demand for fresh, clean qubits---a resource that is typically scarce in practice. For such reuse to be valid, the initial states of the dirty qubits must not affect the functionality of the quantum circuits in which they are employed. Moreover, their original states, including any entanglement they possess, must be fully restored after use---a requirement commonly known as safe uncomputation. In this paper, we formally define the semantics of dirty-qubit borrowing as a feature in quantum programming languages, and introduce a notion of safe uncomputation for dirty qubits in quantum programs. We also present an efficient algorithm, along with experimental results, for verifying safe uncomputation of dirty qubits in certain quantum circuits.