Refinement calculus of quantum programs with projective assertions

TL;DR

This paper develops a refinement calculus framework for quantum programs using projective assertions, providing semantics, refinement rules, and a Python tool to support correct quantum program development.

Contribution

It introduces a novel refinement calculus for quantum programs with projective assertions, including semantics, rules, and a prototype tool for stepwise development.

Findings

Semantics for quantum nondeterministic programs using super-operators

Refinement rules based on dual semantics for correctness

Practical examples and a Python tool for quantum program development

Abstract

Refinement calculus provides a structured framework for the progressive and modular development of programs, ensuring their correctness throughout the refinement process. This paper introduces a refinement calculus tailored for quantum programs. To this end, we first study the partial correctness of nondeterministic programs within a quantum while language featuring prescription statements. Orthogonal projectors, which are equivalent to subspaces of the state Hilbert space, are taken as assertions for quantum states. In addition to the denotational semantics where a nondeterministic program is associated with a set of trace-nonincreasing super-operators, we also present their semantics in transforming a postcondition to the weakest liberal postconditions and, conversely, transforming a precondition to the strongest postconditions. Subsequently, refinement rules are introduced based on these dual semantics, offering a systematic approach to the incremental development of quantum programs applicable in various contexts. To illustrate the practical application of the refinement calculus, we examine examples such as the implementation of a $Z$-rotation gate, the repetition code, and the quantum-to-quantum Bernoulli factory. Furthermore, we present Quire, a Python-based interactive prototype tool that provides practical support to programmers engaged in the stepwise development of correct quantum programs.