Modular Synthesis of Efficient Quantum Uncomputation

TL;DR

This work targets the challenge of uncomputing quantum data in expressive programs beyond circuits. It introduces HQIR, a SSA-based intermediate representation that supports recursion, quantum and classical computation, and explicit uncomputation reasoning, including effects tracking and consumed vs conserved arguments. A modular algorithm synthesizes correct and efficient uncomputation by first generating explicit uncomputation (f^G) and then handling adjoints, with uncomputation erasure used to maintain efficiency. The authors implement an end-to-end pipeline from Silq fragments to HQIR and generated circuits, and demonstrate competitive performance against circuit-focused baselines while handling more expressive programs. Overall, the approach shows that higher expressivity and safety from high-level quantum languages can be achieved without compromising efficiency in uncomputation-heavy programs.

Abstract

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.

Figures (6)

• Figure 1: Iterate reversibly computes the $n$th iteration of the procedure $f(\textbf{in}\ x, \textbf{out}\ y)$, which reads $x$, and updates $y$ in-place. Here $n$ and $f$ hold classical data, while $x$ and $y$ hold quantum data. Input quantum parameters are not modified, output ones are expected in a zero state, and adjoint output ones are uncomputed to a zero state. Allocation and deallocation happens with two primitives: alloc pops a zeroed quantum register from the free list, while its adjoint alloc$^\dag$ pushes a zeroed quantum register back.
• Figure 2: A forget statement can be thought of a placeholder for yet to be synthesized uncomputation. That uncomputation can be delayed by throwing the data into a garbage bin using dispose.
• Figure 3: Our uncomputation synthesis approach for Etareti. Here, the bin operator binds a garbage bin to a variable, and its adjoint bin$^\dag$ unbinds one, uniquely identifying a computation-uncomputation pair. The pairing enables uncomputation erasure: the replacement of uncomputation with dispose. The resulting procedure accepts a garbage bin parameter to which temporary variables are disposed; the adjoint procedure accepts a bin$^\dag$ parameter from which garbage can be removed using the adjoint operation dispose$^\dag$.
• Figure 4: An example of a quantum circuit. CX is often written .
• Figure 5: Uncomputation circuit.