A key challenge of quantum programming is uncomputation: the reversible deallocation of qubits. And while there has been much recent progress on automating uncomputation, state-of-the-art methods are insufficient for handling today's expressive quantum programming languages. A core reason is that they operate on primitive quantum circuits, while quantum programs express computations beyond circuits, for instance, they can capture families of circuits defined recursively in terms of uncomputation and adjoints. In this paper, we introduce the first modular automatic approach to synthesize correct and efficient uncomputation for expressive quantum programs. Our method is based on two core technical contributions: (i) an intermediate representation (IR) that can capture expressive quantum programs and comes with support for uncomputation, and (ii) modular algorithms over that IR for synthesizing uncomputation and adjoints. We have built a complete end-to-end implementation of our method, including an implementation of the IR and the synthesis algorithms, as well as a translation from an expressive fragment of the Silq programming language to our IR and circuit generation from the IR. Our experimental evaluation demonstrates that we can handle programs beyond the capabilities of existing uncomputation approaches, while being competitive on the benchmarks they can handle. More broadly, we show that it is possible to benefit from the greater expressivity and safety offered by high-level quantum languages without sacrificing efficiency.

翻译：量子编程的一个关键挑战是反计算：量子比特的可逆释放。尽管近年来在自动化反计算方面取得了显著进展，但现有最先进方法仍不足以处理当前表达力丰富的量子编程语言。其核心原因在于这些方法仅能在原始量子电路层面操作，而量子程序能够表达超越电路的计算形式，例如可捕获基于反计算与伴随运算递归定义的电路族。本文提出了首个模块化自动方法，用于为表达力丰富的量子程序综合正确且高效的反计算。我们的方法基于两项核心技术贡献：(i) 一种能够捕获表达性量子程序并支持反计算的中间表示(IR)；(ii) 基于该IR的模块化算法，用于综合反计算与伴随运算。我们构建了完整的端到端实现方案，包括IR与综合算法的实现、从Silq编程语言表达性片段到IR的转换，以及基于IR的电路生成。实验评估表明，我们的方法能够处理超出既有反计算方法能力范围的程序，同时在现有基准测试中保持竞争力。更广泛而言，我们证明了在保持效率的同时，充分利用高级量子语言所提供的更强表达力与安全性是可行的。