SearcharxivSearch

arXiv subjects

Huiling Wu

Publications and source records attributed to Huiling Wu.

2 recordsLinked to original sources

ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation

Quantum oracles are essential to many quantum algorithms, and their specifications may involve recursive control flow that depends on runtime quantum data. However, existing reversible compilation frameworks provide limited support for such quantum-controlled recursive structures. We present ReOC, a compilation framework that transforms high-level recursive oracle specifications with quantum control flow into reversible quantum programs. The framework comprises RQIMP, a high-level imperative source language for specifying recursive oracles, and a method of compiling programs in that language into RQC++, an existing high-level quantum recursive language with quantum control flow. In this way, we avoid the tedious and error-prone process of directly writing quantum oracles in RQC++. To manage static storage under dynamic quantum control, ReOC uses an indexed static-register discipline to isolate live variables across recursion layers, enabling safe register reuse while controlling quantum storage usage. Furthermore, to address the exponential time blow-up caused by naive uncomputation in recursive settings, ReOC employs a recursion-aware uncomputation strategy: temporary variables from recursive calls are cleaned using deferred strategies to control time overhead, while those from non-recursive statements are cleaned eagerly to reduce space usage. For linear recursion, this strategy yields overhead linear in recursion depth, parameterized by the per-layer register footprint and primitive-operation costs. Finally, we provide a mathematical proof of compilation correctness from RQIMP to RQC++, establishing semantic preservation and correct uncomputation of temporary quantum variables.

cs.PL

Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms. Moreover, we embed our logic into the proof assistant Coq. The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs.

cs.PL