Automatic uncomputation aims to provide programming-language-level support to facilitate the correct and safe use of ancilla qubits in quantum computing, but efforts have only been made for clean ancillas, leaving dirty ancillas unexplored.
We present a unified formalization of the uncomputation of both clean and dirty ancillas.
For the first time, we prove that checking the existence of uncomputation is coNP-hard.
We introduce two complementary synthesis-oriented existence checking methods: a syntax-directed static reasoning system and a rewrite-based normalization procedure (RwUn), together forming a top-down pipeline.
We implement RwUn in Qiskit. Compared to the state-of-the-art Reqomp, RwUn achieves 100% coverage on complex-dependency benchmarks, twice the coverage on random classical circuits, and about 50% coverage on random quantum circuits beyond the scope of existing methods, demonstrating broader applicability.