Refinement orders for quantum programs
Yuan Feng, Li Zhou
TL;DR
The paper develops a semantic, language-independent refinement framework for quantum programs, modeling deterministic programs as $\,\mathrm{CPTN}$-super-operators and nondeterministic programs as sets of such operators. It examines three families of quantum state predicates—projectors, effects, and sets of effects—and establishes how the choice of predicates interacts with total versus partial correctness to shape refinement orders. Key results connect refinement to intrinsic operator orders (e.g., complete positivity) for deterministic programs and to Hoare, Smyth, and EM domain orders for nondeterministic ones, while clarifying how predicate strength (projectors vs. single vs. sets of effects) changes refinement strength. The framework leverages Kraus representations, Choi isomorphism, and predicate transformers (wp, wlp, sp) to relate refinement to semantic transformations, providing a rigorous basis for quantum program verification and guiding the design of practical refinement calculi. Overall, the work clarifies how different quantum predicates influence refinement granularity and establishes foundational links between quantum operational semantics and classical verification concepts.
Abstract
Refinement is an influential technique used in the verification and development of computer programs. It provides a systematic and rigorous approach to software development through stepwise refinement, where a high-level abstract specification is progressively transformed into an implementation that meets the desired requirements. Central to this technique is the notion of a refinement order, which ensures that each refinement step preserves program correctness. Different orders can be defined with respect to partial and total correctness, as well as for deterministic and nondeterministic programs. In the realm of quantum programs, the theory becomes even more intricate due to the existence of various quantum state predicates, leading to different notions of specifications. This paper thoroughly explores different refinement orders for quantum programs and examines the relationships between them.