Pith. sign in

REVIEW 3 major objections 5 minor 72 references

Quantum Uncomputation of Clean and Dirty Ancilla Qubits

T0 review · 3 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Deciding whether an ancilla can be uncomputed is coNP-complete for reversible Boolean circuits, yet rewrite-based normalization and template reasoning synthesize uncomputation for far more circuits than prior tools.

desk verdict The coNP-hardness result is real and the rewrite system is worth engaging; the empirical coverage claims cannot be independently checked until the artifact is released. read the letter →

arxiv 2608.09578 v1 pith:RSAN2B4C submitted 2026-08-10 cs.PL quant-ph

Chenke Liu , Li Zhou , Boning Meng This is my paper · ORCID
classification cs.PLquant-ph MSC 68Q1268Q1781P68
keywords quantumuncomputationdirtyancillacleancoNP-completenessreversibleBooleancircuitsrewrite-basednormalizationstaticreasoningsynthesis
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper gives a unified treatment of uncomputation for clean ancillas (initialized in |0>) and dirty ancillas (initialized in an unknown state), showing that in both cases the ancilla must be restored to the same state it started in, and that existence of such an operation is exactly the same decision problem. The central hardness claim is that for polynomial-size reversible Boolean circuits built from CCNOT and X gates, deciding whether uncomputation exists is coNP-complete, proved by reducing SAT to the question of whether a reversible Boolean function stays reversible after some inputs are fixed to 0. On the constructive side, the paper shows that uncomputation is guaranteed and regularly synthesizable whenever a circuit can be rewritten into a prefix-suffix normal form in which all ancilla-modifying gates sit at the tail; two systems, a template-based static checker and a rewrite-based normalizer, exploit this structure. The rewrite-based method succeeds on all 17 practical complex-dependency benchmarks, solves roughly twice as many random reversible circuits as the previous baseline, and handles about half of random quantum circuits that use phase gates. If correct, the paper makes automatic uncomputation of both clean and dirty ancillas a realistic compiler front-end problem.

What carries the argument

Two objects carry the argument. The first is the k-fixed reversible Boolean function f|_k, obtained by fixing k input bits of a reversible Boolean function to 0 and deleting the same outputs; deciding whether f|_k is reversible is exactly the uncomputation problem for qfree circuits, and the coNP-completeness proof reduces SAT to it via a controlled-SWAP gate built from a CNF formula on n+5 qubits. The second is the prefix-suffix normal form: a circuit is in normal form with respect to an ancilla when every gate that modifies the ancilla has only ancilla-modifying gates to its right, so the circuit splits into a working-qubit prefix that implements the functionality and an ancilla tail that can be inverted. The rewrite rules (R-1) to (R-6) push ancilla-modifying gates rightward, inserting compensating gates when a naive swap would change the semantics, and the no-aw-cycle condition on the circuit graph guarantees the rules never get stuck for qfree circuits. The static template system uses const, qfree, and CQBF properties of store-use and toggle-detection patterns to certify uncomputability and produce regular synthesis.

What would settle it

Build the controlled-SWAP circuit of Lemma 3.1 for a small satisfiable CNF and a small unsatisfiable CNF, and check on all inputs whether the swap fires exactly when the formula is true; if the n+5-qubit construction silently needs a sixth qubit preset to a known state, the reduction fails. A direct check of the hardness chain: for an unsatisfiable formula the 1-fixed reversible function must equal the identity, so any observed collision on the remaining inputs would falsify the claimed equivalence.

Watch

Extended reading notes

Core claim

The paper's central claim is that uncomputation existence is a single unified problem for clean and dirty ancillas, and that for reversible Boolean circuits of polynomial gate size this problem is coNP-complete. The reduction goes through the k-fixed reversible Boolean function: fix k input positions to 0, discard the corresponding outputs, and ask whether the remaining function is a bijection; uncomputation exists exactly when it is. The paper proves coNP-hardness by reducing SAT to non-reversibility of the 1-fixed function, using a polynomial-time construction of a CCNOT-and-X circuit implementing a controlled-SWAP conditioned on a CNF formula over n+5 qubits. On the constructive side, it proves that a qfree circuit is uncomputable if and only if it has a semantically equivalent prefix-suffix normal form, where the prefix acts on working qubits and the suffix modifies only ancillas; for general quantum circuits the normal form is a sufficient condition. Two synthesis-oriented existence checkers, the template-based static system TpUn and the rewrite-based normalizer RwUn, certify this normal form in different regimes and synthesize an uncomputation by inverting the ancilla tail. Empirically, the paper claims RwUn correctly uncomputes all 17 practical benchmarks with complex dependencies, about twice as many random reversible circuits as the baseline, and about half of random quantum circuits beyond the baseline's scope.

Load-bearing premise

The hardness result depends on the assumption that any CNF formula can be compiled, in polynomial time and using only CCNOT and X gates on n+5 qubits, into a circuit whose controlled swap fires exactly when the formula is satisfiable, with no extra qubit initialized to zero.

Editorial extensions

If this is right

  • Compiler-level uncomputation cannot be a complete, fully automatic polynomial-time pass for arbitrary reversible Boolean circuits; it must either accept a restricted fragment or solve a coNP-hard existence problem.
  • For classical reversible (qfree) circuits, uncomputability is equivalent to reachability of the prefix-suffix normal form, so the no-aw-cycle graph condition gives a structural test and uncomputation then reduces to inverting the tail.
  • Dirty ancillas can be uncomputed automatically whenever their usage follows the store-use/toggle-detection pattern, and the dirty-ancilla uncomputation is unique when it exists, giving a canonical synthesis target.
  • The rewrite-based method broadens automatic uncomputation beyond the previous baseline: full success on the 17 practical benchmarks, roughly double the success on random reversible circuits, and partial success on circuits with Z, S, and T gates.
  • Separating existence checking from synthesis lets a front-end accept a program only when a witness circuit is produced, keeping the back-end focused on optimization.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The coNP-completeness result suggests that a SAT-based decision procedure for k-fixed reversibility could serve as a complete fallback for the qfree fragment, complementing the incomplete rewrite approach.
  • Because the paper proves normal-form existence is necessary and sufficient for qfree circuits, complete rewriting systems for reversible circuits could turn uncomputation checking into a reachability problem with a known set of rules.
  • The store-use/toggle-detection pattern generalizes beyond these benchmarks: it could be exposed as a first-class language construction for dirty ancillas, making the safety argument part of the type system.
  • The Aw-Dep dependency-complexity metric used in the evaluation may itself be a predictor of synthesis hardness; testing it on a broader circuit corpus could give compiler authors a cheap way to decide when to attempt uncomputation.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper develops a unified framework for automatic uncomputation of clean and dirty ancilla qubits in quantum circuits. It formalizes when the functionality of a circuit is valid, proves that deciding uncomputation existence is coNP-hard for reversible Boolean circuits over CCNOT and X gates, and presents two synthesis-oriented existence checkers: a template-based static reasoning system (TpUn) and a rewrite-based normalization procedure (RwUn). The experimental section reports that RwUn outperforms the state-of-the-art Reqomp on practical and random benchmarks, claiming 100% coverage on 17 practical cases, roughly double the success rate on random qfree circuits, and about 50% success on random quantum circuits outside Reqomp's scope.

Significance. If the results are correct and the implementation is available, this is a useful step for quantum programming-language support: it gives the first coNP-hardness result for the uncomputation existence problem, unifies clean and dirty ancilla semantics, and provides a concrete synthesis pipeline with normal forms. The coNP-hardness reduction is detailed and appears substantially correct, and the rewrite rules are accompanied by nontrivial semantic proofs. The paper also gives a sufficient syntactic criterion (absence of aw-cycles) for RwUn to succeed, which is a valuable practical insight. However, the termination proof of the central normalization algorithm is not fully established as written, and the empirical claims are currently not independently verifiable because the artifact, benchmark code, and details of the filtering procedure are not provided.

major comments (3)
  1. [Section 6.3, Theorem 6.1; Appendix D.13, Lemma D.2] The termination proof of Algorithm 1 is incomplete. Lemma D.2 only treats circuits that contain exactly one violating pair and where that pair is at the end of the circuit. The step from this special case to termination for arbitrary circuits is asserted in the preamble of Appendix D.13 ('the global execution can be decomposed into a sequence of local subproblems') but no formal measure or inductive argument is given. Since termination is part of Theorem 6.1 and is a precondition for the synthesis theorem (Theorem 6.2) and for the experimental success claims, this gap is load-bearing. Please provide a complete termination proof or a revised statement that makes the termination assumption explicit.
  2. [Section 7, Benchmarks 2 and 3; Data-Availability Statement] The central practical claims are not reproducible from the manuscript. The implementation is not released, the random benchmarks use a single seed (42), the SAT filter used to select 'uncomputable' qfree circuits is not named, and Benchmark 3 is deliberately not filtered for uncomputability. Consequently, the reported 100% / 2x / 50% success rates could be affected by the particular seed, by the SAT solver's encoding, or by the unknown fraction of uncomputable circuits in Benchmark 3. Please release the artifact and benchmarks, report results over multiple seeds, and describe the SAT filter precisely; alternatively, substantially weaken the empirical claims to clearly verified case studies.
  3. [Appendix D.9, proof of Proposition 6.1] The proof that every uncomputable qfree circuit has a semantically equivalent circuit satisfying condition (2) of Proposition 6.1 is not self-contained. It invokes the canonical form of [Feng and Li 2025] and asserts that MPMCX gates in the 'head part' whose target is an ancilla can be implemented using only MCX gates controlled by another ancilla, but the required construction is not shown. This is a key characterization result for the normal-form approach, so the proof should either spell out the construction or give a precise reference to a theorem that does.
minor comments (5)
  1. [Section 6.2, heading] The heading 'Normal form of quantum circutis' contains a typo; it should read 'circuits'.
  2. [Section 3.1, Definitions 3.2 and 3.3] The displayed definitions of uncomputation read as if the uncomputation operator G_a is applied directly to the original input, rather than after the compute circuit G. Consider clarifying that G_a denotes the full uncomputed circuit (or state explicitly whether it is post-composed with G), since this affects the reading of Proposition 3.1.
  3. [Theorem 3.1 proof diagram] The text immediately below the circuit diagram says '4 Qubits c,d,e remain unchanged' but only three qubits c,d,e are listed; please fix the numbering or the list.
  4. [Appendix D.7.4 and D.10] There are minor typos such as 'simliar' and 'fixed function' used where 'fixed-input function' or similar is meant; a proofreading pass is needed.
  5. [Section 7.1, Aw-Dep definition] The Aw-Dep metric depends on a depth bound L=10 and on the cycle-gated source collection heuristic; the paper should state whether the reported conclusions are sensitive to L and to the choice of the bound.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the coNP-hardness reduction and rewrite-based synthesis are self-contained; the evaluation is empirical and not forced by construction.

full rationale

The paper's central derivation chain does not reduce to its own inputs. The coNP-hardness result (Theorem 3.1 and Corollary 3.1) is built on an external Barrington/Jordan construction (Lemma 3.1 and Corollary D.1), and the reduction from SAT to R-kRBF is explicitly proved with a self-contained collision argument for the 1-fixed RBF. The equivalences in Proposition 3.1 are formal consequences of the definitions of func, Uncomp, and Uncomp*, not hidden assumptions. The rewrite rules (R-1)–(R-6) are proved sound by direct basis-state calculations in Appendix D.12, and Theorems 6.1 and 6.2 are soundness and termination statements for the algorithm; no fitted parameters enter these theorems. The static reasoning system is likewise proved sound by structural induction from the template definitions. The empirical evaluation compares against the external Reqomp baseline and external benchmark circuits; the SAT filter in Benchmark 2 uses Proposition 3.2 to select genuinely uncomputable circuits, so the success-rate comparison is not a tautology. The only self-citations ([54], [61], [53]) support standard definitions or related work and are not load-bearing for the main contributions. No equation-level or definition-level circular step was found.

Assumptions & free parameters 3 free parameters · 6 assumptions · 0 invented entities

The theoretical core rests on standard complexity and reversible-circuit tools, such as Barrington's theorem, Jordan's construction, and Feng-Li canonical forms, rather than on fitted parameters. The evaluation uses hand-chosen settings, including seed 42, L=10, and a 30-second timeout, which affect reported numbers but not the soundness theorems. No new physical entities are introduced.

free parameters (3)
  • Aw-Dep depth bound L = 10
    Hyperparameter in the dependency-complexity metric used in Table 1 and Figure 10; changes reported Aw-Dep values and the explanation of coverage.
  • random benchmark seed = 42
    Seed for random circuit generation in Benchmarks 2 and 3; the specific benchmark set depends on it.
  • scalability timeout = 30 seconds
    Time budget for the scalability comparison in Table 1; affects which circuits count as solved.
assumptions (6)
  • standard math Barrington's theorem: width-5 branching programs evaluate NC^1 formulas in polynomial length
    Used in Lemma 3.1 to convert a CNF formula into a width-5 branching program of polynomial length.
  • standard math Jordan's construction: a width-5 branching program can be simulated by Fredkin gates on n+6 bits
    Basis for Lemma 3.1; the paper extends it to n+5 bits with X gates.
  • domain assumption No-deleting theorem of quantum mechanics
    Justifies why uncomputation may not exist and motivates the existence problem.
  • domain assumption Dirty ancilla functionality must be independent of the ancilla's initial state and equal to the clean functionality
    Definitional choice in Section 1 and Definition 3.3; the unified formalization depends on this semantics.
  • standard math Reversible Boolean circuits over X and CCNOT are universal for reversible functions without ancillas
    Used in Proposition 6.2 to synthesize the permutation h(0, middle dot) on the working register.
  • standard math Feng and Li canonical form for reversible circuits
    Used in the appendix proof of Proposition D.6 to decompose safe ancilla usage.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Quantum Uncomputation of Clean and Dirty Ancilla Qubits." pith.science (2026). https://pith.science/paper/RSAN2B4C

@misc{pith2026260809578,
  author       = {Pith},
  title        = {Pith review of: Quantum Uncomputation of Clean and Dirty Ancilla Qubits},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RSAN2B4C}},
  note         = {Machine review of arXiv:2608.09578}
}
read the original abstract

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 rewrite-based normalization algorithm (RwUn) and a template-based reasoning system (TpUn) that guarantees uncomputation through structured Store-Use patterns. We implement prototypes of both methods in Qiskit and Python. Compared to the state-of-the-art Reqomp~\cite{reqomp}, RwUn achieves 100% coverage on practical 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.

Figures

Figures reproduced from arXiv: 2608.09578 by the authors.

Figure 1
Figure 1. Circuit costs with and without dirty ancillas. The depths in [ [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. For applying four identical functionalities in parallel on four disjoint [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Selected rules 4.3 Automatic uncomputation—an overview Under the semantics above, checking validity coincides with checking existence of uncomputation. Beyond existence, we also emphasize synthesis. First, existence checking can be computationally expensive; it is therefore desirable to make this effort constructive, returning not only a yes/no answer but also a witness that can be turned into code. Second, even whe… view at source ↗
Figures from the paper (20 more)
Figure 4
Figure 4. Figure 4: Comparison of implementations for computing [PITH_FULL_IMAGE:figures/full_fig_p015_4.png]
Figure 6
Figure 6. Figure 6: Rewrite-based normalization on a running example. Each panel is the circuit after one rewrite step. [PITH_FULL_IMAGE:figures/full_fig_p019_6.png]
Figure 7
Figure 7. Figure 7: Regular synthesis once 𝐺 ′ is in normal form. Faded gates indicate removal. reduces to removing the last CCNOT gate, shown in gray.) For dirty ancillas, informally, we eliminate all gates that touch the ancillas. In the end, only C 3NOT[𝑞1, 𝑞2, 𝑞3, 𝑡] remains, which is…
Figure 8
Figure 8. Figure 8: From left to right: a mutual-control circuit [PITH_FULL_IMAGE:figures/full_fig_p021_8.png]
Figure 9
Figure 9. Figure 9: Illustration of Aw-Dep computation. We group all reported metrics as follows: • Aw-Dep: the maximum dependency-complexity among all ancillas of a circuit, since non￾uncomputability is typically driven by the “hardest” ancilla. • Aw-Cyc: whether an aw-cycle exists in a …
Figure 10
Figure 10. Figure 10: Uncomputation results of RwUn (Jointly) and Reqomp on random qfree circuits. The three columns correspond to increasing circuit width: small (5 working qubits + 5 ancillas), medium (40+40), and large (200+200). The four rows (top to bottom) report: (1) overall success…
Figure 11
Figure 11. Figure 11: Success rate of RwUn (Lifetime) and Reqomp on random quantum circuits (RQ1). introduced while rewriting. Reqomp, on the other hand, tends to be consistently scalable in most cases where it is applicable and outperforms RwUn on four cases. For Benchmarks 2 and 3, the a…
Figure 12
Figure 12. Figure 12: const rules Theorem A.1 (Soundness). If a circuit 𝐺 ∈ QCa is assigned a const property by the static reasoning system, then for every borrow substatement 𝐵 in 𝐺, ⟦𝐵⟧ ≠ ⊥; moreover, ⟦𝐺⟧ ≠ ⊥. A.4 Synthesis from Templates We give the complete definitions of the synthesis…
Figure 13
Figure 13. Figure 13: qfree rules takes as input a circuit 𝐺 ∈ QCa and recursively synthesizes its subcircuits as follows: TpSynth(skip) ≜ skip, TpSynth(𝑈 [𝑞]) ≜ 𝑈 [𝑞], TpSynth(𝐶1;𝐶2) ≜ TpSynth(𝐶1); TpSynth(𝐶2), TpSynth(qif 𝑞 then 𝐶1 else 𝐶0) ≜ qif 𝑞 then TpSynth(𝐶1) else TpSynth(𝐶0), TpSy…
Figure 14
Figure 14. Figure 14: QBF rules • Removing all C 𝑖NOT gates targeting ancillas in 𝐺 yields a circuit G such that ⟦G⟧ ∈ Uncomp(⟦𝐺⟧ , 𝑎). • Further removing all C 𝑖NOT gates that use ancillas as controls yields a circuit G ′ such that ⟦G′⟧ ∈ Uncomp∗ (⟦𝐺⟧ , 𝑎). Quantum circuits. Once 𝐺 is nor…
Figure 15
Figure 15. Figure 15: CQBF rules for 𝑉 ∈ {Z, S, T}. X[𝑝];𝑉 [𝑝] ≡ 𝑉 † [𝑝]; X[𝑝] CNOT[𝑝, 𝑡];𝑉 [𝑝] ≡ 𝑉 [𝑝]; CNOT[𝑝, 𝑡] CNOT[𝑝, 𝑡];𝑉 [𝑡] ≡ 𝑉 [𝑝];𝑉 [𝑡]; CV† [𝑝, 𝑡]; CV† [𝑝, 𝑡]CNOT[𝑝, 𝑡] X[𝑝]; CV[𝑝, 𝑡] ≡ CV[𝑝, 𝑡] † ;𝑉 [𝑡]; X[𝑝] X[𝑡]; CV[𝑝, 𝑡] ≡ CV[𝑝, 𝑡] † ;𝑉 [𝑝]; X[𝑝] CNOT[𝑝, 𝑎]; CV[𝑝, 𝑡] ≡ CV[𝑝…
Figure 16
Figure 16. Figure 16: Commutativity rules Algorithm 2 Rewrite-based phase reordering. Require: A quantum circuit 𝐺 in its normal form, acting on an ancillas 𝑎 and qubits 𝑞. 1: 𝐺 ′ ← 𝐺.copy() 2: while true do 3: Find the first C 𝑖NOT gate targeting an ancilla followed by a gate ∈ {Z, S, T, …
Figure 17
Figure 17. Figure 17: Rewrite-based phase reordering. In the above text, we gave a high-level presentation of the rewrite-based uncomputation procedure RwUn and its soundness result. Here we provide the complete formal definitions of all intermediate transformations, including NWsynth, NSy…
Figure 18
Figure 18. Figure 18: The circuit realizes an operation that applies [PITH_FULL_IMAGE:figures/full_fig_p039_18.png]
Figure 19
Figure 19. Figure 19: Multi-controlled-H written in QCa using clean and dirty ancillas: (a) direct implementation without uncomputation, (b) manual uncomputation expansion, and (c) with template-based borrow statements. 1 CX [ x2 , x3 ]; 2 borrow a1 store { 3 4 } use { 5 qif a1 then { 6 qi…
Figure 20
Figure 20. Figure 20: Comparison of incrementer implementations with automatic vs manual uncomputation [PITH_FULL_IMAGE:figures/full_fig_p042_20.png]
Figure 21
Figure 21. Figure 21: Compute the highest bit of the input integer [PITH_FULL_IMAGE:figures/full_fig_p042_21.png]
Figure 22
Figure 22. Figure 22: A compilation result of the HighestBitConstAdder into a circuit without uncomputation (left), and [PITH_FULL_IMAGE:figures/full_fig_p043_22.png]
Figure 23
Figure 23. Figure 23: A possible compilation with uncomputation result of the HighestBitConstAdder into a circuit. [PITH_FULL_IMAGE:figures/full_fig_p043_23.png]
Figure 24
Figure 24. Figure 24: The dependency-complexity of node a1(CX) is 1, computed by alternating positive even (blue) levels from shallow to deep. b1' a0(init) a1(CX) p1(CX) p0(init) a2(CX) { Lev0 r0(init) q0(init) +1 q1(CX) { Lev1 { Lev2 e1 e2 e3 [PITH_FULL_IMAGE:figures/full_fig_p064_24.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

72 extracted references · 33 canonical work pages

  1. [1]

    Chow, Antonio D

    Gadi Aleksandrowicz, Thomas Alexander, Panagiotis Barkoutsos, Luciano Bello, Yael Ben-Haim, David Bucher, Francisco Jose Cabrera-Hernández, Jorge Carballo-Franquis, Adrian Chen, Chun-Fu Chen, Jerry M. Chow, Antonio D. Córcoles-Gonzales, Abigail J. Cross, Andrew Cross, Juan Cruz-Benito, Chris Culver, Salvador De La Puente González, Enrique De La Torre, Del...

    2019

  2. [2]

    Matthew Amy, Martin Roetteler, and Krysta M. Svore. 2017. Verified Compilation of Space-Efficient Reversible Circuits. InComputer Aided Verification, Rupak Majumdar and Viktor Kunčak (Eds.). Springer International Publishing, Cham, 3–21

    work page 2017

  3. [3]

    In preparation

    Anonymous Author(s). In preparation. Circuit optimization via managing dirty ancillas. (In preparation)

    work page

  4. [4]

    Bennett, Richard Cleve, David P

    Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. DiVincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John A. Smolin, and Harald Weinfurter. 1995. Elementary gates for quantum computation.Phys. Rev. A52 (Nov 1995), 3457–3467. Issue 5. doi:10.1103/PhysRevA.52.3457 Quantum Uncomputation of Clean and Dirty Ancilla Qubits 27

    doi:10.1103/physreva.52.3457 1995

  5. [5]

    M Barrington

    David A. M Barrington. 1987.Bounded Width Polynominal Size Branching Programs Recognize Exactly Those. Technical Report. USA

    work page 1987

  6. [6]

    Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. 2020. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation(London, UK)(PLDI 2020). Association for Computing Machinery, New York, NY, USA, 286–300. doi:10.114...

    arXiv 2020

  7. [7]

    Baptiste Claudon, Julien Zylberman, César Feniou, Fabrice Debbasch, Alberto Peruzzo, and Jean-Philip Piquemal

    work page

  8. [8]

    Alexandre Clément, Noé Delorme, and Simon Perdrix. 2024. Minimal Equational Theories for Quantum Circuits. InProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science(Tallinn, Estonia)(LICS ’24). Association for Computing Machinery, New York, NY, USA, Article 27, 14 pages. doi:10.1145/3661814.3662088

    arXiv 2024

Show all 72 references
  1. [9]

    Alexandre Clément, Noé Delorme, Simon Perdrix, and Renaud Vilmart. 2024. Quantum Circuit Completeness: Extensions and Simplifications. In32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 288), Ani...

    2024 doi

  2. [10]

    Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoît Valiron. 2023. A Complete Equational Theory for Quantum Circuits. In2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–13. doi:10.1109/LICS56636.2023.10175801

    2023

  3. [11]

    Stephen A. Cook. 1971. The complexity of theorem-proving procedures. InProceedings of the Third Annual ACM Symposium on Theory of Computing(Shaker Heights, Ohio, USA)(STOC ’71). Association for Computing Machinery, New York, NY, USA, 151–158. doi:10.1145/800157.805047

    1971

  4. [12]

    Cuccaro, Thomas G

    Steven A. Cuccaro, Thomas G. Draper, Samuel A. Kutin, and David Petrie Moulton. 2004. A new quantum ripple-carry addition circuit. arXiv:quant-ph/0410184 [quant-ph] https://arxiv.org/abs/quant-ph/0410184

    2004 arXiv

  5. [13]

    Matthew DeCross, Eli Chertkov, Megan Kohagen, and Michael Foss-Feig. 2023. Qubit-Reuse Compilation with Mid-Circuit Measurement and Reset.Phys. Rev. X13 (Dec 2023), 041057. Issue 4. doi:10.1103/PhysRevX.13.041057

    2023 doi

  6. [14]

    1992.Rapid Solution of Problems by Quantum Computation

    D Deutsch and R Jozsa. 1992.Rapid Solution of Problems by Quantum Computation. Technical Report. GBR

    1992

  7. [15]

    Yongshan Ding, Xin-Chuan Wu, Adam Holmes, Ash Wiseth, Diana Franklin, Margaret Martonosi, and Frederic T. Chong

  8. [16]

    Thomas G. Draper. 2000. Addition on a Quantum Computer. arXiv:quant-ph/0008033 [quant-ph] https://arxiv.org/ abs/quant-ph/0008033

    2000 arXiv

  9. [17]

    Shiguang Feng and Lvzhou Li. 2025. A complete set of transformation rules for reversible circuits.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems(2025), 1–1. doi:10.1109/TCAD.2025.3641533

    2025

  10. [18]

    Edward Fredkin and Tommaso Toffoli. 1982. Conservative Logic.International Journal of Theoretical Physics21, 3-4 (1982), 219–253

    1982

  11. [19]

    Martin Fürer. 2009. Faster Integer Multiplication.SIAM J. Comput.39, 3 (2009), 979–1005. arXiv:https://doi.org/10.1137/070711761 doi:10.1137/070711761

    2009 doi

  12. [20]

    Craig Gidney. 2015. Constructing Large Controlled Nots. https://algassert.com/circuits/2015/06/05/Constructing- Large-Controlled-Nots.html. Accessed: 2025-09-05

    2015

  13. [21]

    Craig Gidney. 2018. Factoring with n+2 clean qubits and n-1 dirty qubits. arXiv:1706.07884 [quant-ph] https: //arxiv.org/abs/1706.07884

    2018 arXiv

  14. [22]

    Craig Gidney. 2018. Halving the cost of quantum addition.Quantum2 (June 2018), 74. doi:10.22331/q-2018-06-18-74

    2018 doi

  15. [23]

    Craig Gidney. 2019. Approximate encoded permutations and piecewise quantum adders. arXiv:1905.08488 [quant-ph] https://arxiv.org/abs/1905.08488

    2019 arXiv

  16. [24]

    Craig Gidney. 2019. Windowed quantum arithmetic. arXiv:1905.07682 [quant-ph] https://arxiv.org/abs/1905.07682

    2019 arXiv

  17. [25]

    Green, Peter LeFanu Lumsdaine, Neil J

    Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. Quipper: a scalable quantum programming language.SIGPLAN Not.48, 6 (June 2013), 333–342. doi:10.1145/2499370.2462177

    2013

  18. [26]

    Lov K. Grover. 1997. Quantum Mechanics Helps in Searching for a Needle in a Haystack.Phys. Rev. Lett.79 (Jul 1997), 325–328. Issue 2. doi:10.1103/PhysRevLett.79.325

    1997 doi

  19. [27]

    Thomas Häner, Martin Roetteler, and Krysta M. Svore. 2017. Factoring using 2n + 2 qubits with Toffoli based modular multiplication.Quantum Info. Comput.17, 7–8 (June 2017), 673–684

    2017

  20. [28]

    Kengo Hirata and Chris Heunen. 2025. Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime. Proc. ACM Program. Lang.9, POPL, Article 6 (Jan. 2025), 28 pages. doi:10.1145/3704842

    2025 doi

  21. [29]

    Bishop, John Lapeyre, Ali Javadi-Abhari, and Eddy Z

    Fei Hua, Yuwei Jin, Yanhao Chen, Suhas Vittal, Kevin Krsulich, Lev S. Bishop, John Lapeyre, Ali Javadi-Abhari, and Eddy Z. Zhang. 2023. CaQR: A Compiler-Assisted Approach for Qubit Reuse through Dynamic Circuit. InProceedings 28 Chenke Liu, Li Zhou, and Boning Meng of the 28th...

    2023

  22. [30]

    Zhenyu Huang, Fuxin Zhang, and Dongdai Lin. 2025. Constructing Quantum Implementations with the Minimal T-depth or Minimal Width and Their Applications. InAdvances in Cryptology – EUROCRYPT 2025, Serge Fehr and Pierre-Alain Fouque (Eds.). Springer Nature Switzerland, Cham, 155–185

    2025

  23. [31]

    Hanru Jiang. 2024. Qubit Recycling Revisited. 8, PLDI, Article 198 (June 2024), 24 pages. doi:10.1145/3656428

    2024 doi

  24. [32]

    Stephen P. Jordan. 2014. Strong equivalence of reversible circuits is coNP-complete.Quantum Info. Comput.14, 15–16 (Nov. 2014), 1302–1307

    2014

  25. [33]

    Tanuj Khattar and Craig Gidney. 2025. Rise of conditionally clean ancillae for efficient quantum circuit constructions. Quantum9 (May 2025), 1752. doi:10.22331/q-2025-05-21-1752

    2025 doi

  26. [34]

    Niels Kornerup, Jonathan Sadun, and David Soloveichik. 2025. Tight Bounds on the Spooky Pebble Game: Recycling Qubits with Measurements.Quantum9 (Feb. 2025), 1636. doi:10.22331/q-2025-02-18-1636

    2025 doi

  27. [35]

    Jiqi Li, Jingyi Mei, Wang Fang, and Ji Guan. 2026. Formal Verification of Quantum Ancilla Safety. InComputer Aided Verification (Lecture Notes in Computer Science, Vol. 16684), Eva Darulova, Anthony W. Lin, and Philipp Rümmer (Eds.). Springer Nature Switzerland, Cham, 326–348....

    2026 doi

  28. [36]

    Guang Hao Low, Vadym Kliuchnikov, and Luke Schaeffer. 2024. Trading T gates for dirty qubits in state preparation and unitary synthesis.Quantum8 (June 2024), 1375. doi:10.22331/q-2024-06-17-1375

    2024 doi

  29. [37]

    Alessandro Luongo, Antonio Michele Miti, Varun Narasimhachar, and Adithya Sireesh. 2025. Measurement-based uncomputation of quantum circuits for modular arithmetic. In2025 62nd ACM/IEEE Design Automation Conference (DAC). 1–7. doi:10.1109/DAC63849.2025.11132981

    2025

  30. [38]

    Ashley Montanaro and Tobias J. Osborne. 2008. Quantum boolean functions.Chic. J. Theor. Comput. Sci.2010 (2008). https://api.semanticscholar.org/CorpusID:15370057

    2008

  31. [39]

    Junhong Nie, Wei Zi, and Xiaoming Sun. 2024. Quantum circuit for multi-qubit Toffoli gate with optimal resource. arXiv:2402.05053 [quant-ph] https://arxiv.org/abs/2402.05053

    2024 arXiv

  32. [40]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2010.Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press

    2010

  33. [41]

    Alexandru Paler, Robert Wille, and Simon J. Devitt. 2016. Wire recycling for quantum circuit optimization.Phys. Rev. A94 (Oct 2016), 042337. Issue 4. doi:10.1103/PhysRevA.94.042337

    2016 doi

  34. [42]

    2021.Unqomp: synthesizing uncomputation in Quantum circuits(PLDI 2021)

    Anouk Paradis, Benjamin Bichsel, Samuel Steffen, and Martin Vechev. 2021.Unqomp: synthesizing uncomputation in Quantum circuits(PLDI 2021). Association for Computing Machinery, New York, NY, USA, 222–236. doi:10.1145/ 3453483.3454040

    2021

  35. [43]

    2024.Reqomp: Space-constrained Uncomputation for Quantum Circuits.Quantum8 (Feb

    Anouk Paradis, Benjamin Bichsel, and Martin Vechev. 2024.Reqomp: Space-constrained Uncomputation for Quantum Circuits.Quantum8 (Feb. 2024), 1258. doi:10.22331/q-2024-02-19-1258

    2024 doi

  36. [44]

    Alex Parent, Martin Roetteler, and Krysta M. Svore. 2015. Reversible circuit compilation with space constraints. arXiv:1510.00377 [quant-ph] https://arxiv.org/abs/1510.00377

    2015 arXiv

  37. [45]

    Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. 2019. ReQWIRE: Reasoning about Reversible Quantum Circuits.Electronic Proceedings in Theoretical Computer Science287 (Jan. 2019), 299–312. doi:10.4204/eptcs. 287.17

    2019 doi

  38. [46]

    2025.Ancilla-Free Quantum Adder with Sublinear Depth

    Maxime Remaud and Vivien Vandaele. 2025.Ancilla-Free Quantum Adder with Sublinear Depth. Springer Nature Switzerland, 137–154. doi:10.1007/978-3-031-97063-4_11

    2025 doi

  39. [47]

    Movahhed Sadeghi, Soheil Khadirsharbiyani, and Mahmut Taylan Kandemir. 2022. Quantum Circuit Resizing. arXiv:2301.00720 [cs.ET] https://arxiv.org/abs/2301.00720

    2022 arXiv

  40. [48]

    Ethan Schuchman and T. N. Vijaykumar. 2006. A program transformation and architecture support for quantum uncomputation. InProceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems(San Jose, California, USA)(ASPLO...

    2006

  41. [49]

    Raphael Seidel, Nikolay Tcholtchev, Sebastian Bock, and Manfred Hauswirth. 2023. Uncomputation in the Qrisp High-Level Quantum Programming Framework. Springer-Verlag, Berlin, Heidelberg, 150–165. doi:10.1007/978-3-031- 38100-3_11

    2023 doi

  42. [50]

    Ritvik Sharma and Sara Achour. 2025. Optimizing Ancilla-Based Quantum Circuits with SPARE.Proc. ACM Program. Lang.9, PLDI, Article 154 (June 2025), 25 pages. doi:10.1145/3729253

    2025 doi

  43. [51]

    Shende, Stephen S

    Vivek V. Shende, Stephen S. Bullock, and Igor L. Markov. 2005. Synthesis of quantum logic circuits. InProceedings of the 2005 Asia and South Pacific Design Automation Conference(Shanghai, China)(ASP-DAC ’05). Association for Computing Machinery, New York, NY, USA, 272–275. doi...

    2005

  44. [52]

    Peter W. Shor. 1997. Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer.SIAM J. Comput.26, 5 (1997), 1484–1509. arXiv:https://doi.org/10.1137/S0097539795293172 doi:10.1137/ Quantum Uncomputation of Clean and Dirty Ancilla Qubits 29...

    1997 doi

  45. [53]

    Bonan Su, Li Zhou, Yuan Feng, and Mingsheng Ying. 2024. BI-based Reasoning about Quantum Programs with Heap Manipulations. arXiv:2409.10153 [quant-ph] https://arxiv.org/abs/2409.10153

    2024 arXiv

  46. [54]

    Bonan Su, Li Zhou, Yuan Feng, and Mingsheng Ying. 2026. Borrowing Dirty Qubits in Quantum Programs. InProceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2(USA)(ASPLOS ’26). Association for Compu...

    2026

  47. [55]

    Xiaoming Sun, Guojing Tian, Shuai Yang, Pei Yuan, and Shengyu Zhang. 2023. Asymptotically Optimal Circuit Depth for Quantum State Preparation and General Unitary Synthesis.Trans. Comp.-Aided Des. Integ. Cir. Sys.42, 10 (Oct. 2023), 3301–3314. doi:10.1109/TCAD.2023.3244885

    2023

  48. [56]

    Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. 2018. Q#: Enabling Scalable Quantum Computing and Devel- opment with a High-level DSL(RWDSL2018). Association fo...

    2018

  49. [57]

    Yasuhiro Takahashi, Seiichiro Tani, and Noboru Kunihiro. 2010. Quantum addition circuits and unbounded fan-out. 10, 9 (Sept. 2010), 872–890

    2010

  50. [58]

    Tommaso Toffoli. 1980. Reversible Computing. InProceedings of the 7th Colloquium on Automata, Languages and Programming. Springer-Verlag, Berlin, Heidelberg, 632–644

    1980

  51. [59]

    Hristo Venev, Timon Gehr, Dimitar Dimitrov, and Martin Vechev. 2024. Modular Synthesis of Efficient Quantum Uncomputation.Proc. ACM Program. Lang.8, OOPSLA2, Article 345 (Oct. 2024), 28 pages. doi:10.1145/3689785

    2024 doi

  52. [60]

    Mingsheng Ying and Zhicheng Zhang. 2023. Quantum Recursive Programming with Quantum Case Statements. arXiv:2311.01725 [cs.PL] https://arxiv.org/abs/2311.01725

    2023 arXiv

  53. [61]

    Mingsheng Ying, Li Zhou, and Gilles Barthe. 2025. Laws of Quantum Programming.ACM Trans. Softw. Eng. Methodol. (Sept. 2025). doi:10.1145/3765903 Just Accepted

    2025 doi

  54. [62]

    Christof Zalka. 2006. Shor’s algorithm with fewer (pure) qubits. arXiv:quant-ph/0601097 [quant-ph] https://arxiv.org/ abs/quant-ph/0601097

    2006 arXiv

  55. [63]

    negatively controlled

    Ben Zindorf and Sougato Bose. 2025. Efficient Implementation of Multi-Controlled Quantum Gates. arXiv:2404.02279 [quant-ph] https://arxiv.org/abs/2404.02279 30 Chenke Liu, Li Zhou, and Boning Meng Appendices A Store–Use Templates with a Rule-based Static Reasoning System A cen...

    2025 arXiv

  56. [66]

    (⇒).Now assume 𝐺 is uncomputable

    By condition (1) the original circuit𝐺 has the same input–output behaviour on states with ancillas |0⟩𝑎, hence𝐺 is uncomputable as well. (⇒).Now assume 𝐺 is uncomputable. Work in the computational-basis picture: the reversible boolean function implemented by𝐺 maps classical in...

  57. [67]

    ApplyC𝑚NOT[𝑞,𝑎]: flips𝑎if all qubits in 𝑞1∪𝑞2 are 1: 𝑎′ =𝑎⊕(𝑥∧𝑦)

  58. [68]

    ApplyC𝑛NOT[𝑝,𝑡]: flips𝑡if all controls in 𝑞2∪{𝑎}∪ 𝑞3 are 1: 𝑡LHS =𝑡⊕(𝑦∧𝑎 ′∧𝑢)=𝑡⊕(𝑦∧(𝑎⊕𝑥∧𝑦)∧𝑢) 56 Chenke Liu, Li Zhou, and Boning Meng

  59. [69]

    ApplyC𝑛NOT[𝑝,𝑡]first: flips𝑡if all controls in 𝑞2∪{𝑎}∪ 𝑞3 are 1: 𝑡1 =𝑡⊕(𝑦∧𝑎∧𝑢)

  60. [70]

    ApplyC hNOT[(𝑞∪ 𝑝)/𝑎,𝑡], controlled on 𝑞1∪𝑞2∪𝑞3: 𝑡𝑅𝐻𝑆 =𝑡 2 =𝑡 1⊕(𝑥∧𝑦∧𝑢)=𝑡⊕(𝑦∧𝑎∧𝑢)⊕(𝑥∧𝑦∧𝑢)

  61. [71]

    Then the final𝑡value is 𝑡LHS =𝑡⊕(𝑦∧𝑎∧𝑢)⊕(𝑥∧𝑦∧𝑢)=𝑡 RHS

    ApplyC𝑚NOT[𝑞,𝑎]: flips𝑎if 𝑞1∪𝑞2 are all 1,𝑎 final =𝑎⊕𝑥∧𝑦. Then the final𝑡value is 𝑡LHS =𝑡⊕(𝑦∧𝑎∧𝑢)⊕(𝑥∧𝑦∧𝑢)=𝑡 RHS. Hence LHS and RHS produce identical outputs for all computational basis states, proving Eq. (R-2). □ D.13 Proof of Theorem 6.1 The termination argument for Algorith...

  62. [72]

    return path

    The procedure in Algorithm 2 effectively rewrites𝐺′ 2 into the form𝐷′;𝑃 described above. By cancelling𝑃—that is, removing all C𝑖 NOT gates targeting ancillas—we eliminate all modifications on ancillas while preserving the states of all other working qubits. Further removing C𝑖...

    2021

  63. [2020]

    In2020 ACM/IEEE 47th Annual International Symposium on Computer Architecture (ISCA)

    SQUARE: Strategic Quantum Ancilla Reuse for Modular Quantum Programs via Cost-Effective Uncomputation. In2020 ACM/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). 570–583. doi:10.1109/ ISCA45697.2020.00054

    2020

  64. [2024]

    doi:10.1038/s41467-024-50065-x

    Polylogarithmic-depth controlled-NOT gates without ancilla qubits.Nature Communications15, 1 (2024), 5886. doi:10.1038/s41467-024-50065-x

    2024 doi

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.