Reasoning about Parallel Quantum Programs

Abstract

We initiate the study of parallel quantum programming by defining the operational and denotational semantics of parallel quantum programs. The technical contributions of this paper include: (1) find a series of useful proof rules for reasoning about correctness of parallel quantum programs; (2) prove a (relative) completeness of our proof rules for partial correctness of disjoint parallel quantum programs; and (3) prove a strong soundness theorem of the proof rules showing that partial correctness is well maintained at each step of transitions in the operational semantics of a general parallel quantum program (with shared variables). This is achieved by partially overcoming the following conceptual challenges that are never present in classical parallel programming: (i) the intertwining of nondeterminism caused by quantum measurements and introduced by parallelism; (ii) entanglement between component quantum programs; and (iii) combining quantum predicates in the overlap of state Hilbert spaces of component quantum programs with shared variables. Applications of the techniques developed in this paper are illustrated by a formal verification of Bravyi-Gosset-König's parallel quantum algorithm solving a linear algebra problem, which gives for the first time an unconditional proof of a computational quantum advantage.

Added an application on formal verification of Bravyi-Gosset-König's algorithm

References in corpus (10)

• Quantum entanglement
• Quantum Nonlocality without Entanglement
• Distributed Quantum Computation over Noisy Channels
• Separability of very noisy mixed states and implications for NMR quantum computing
• Quantum advantage with shallow circuits
• Concrete Categorical Model of a Quantum Circuit Description Language with Measurement
• Quantum marginal problem and N-representability
• Separable balls around the maximally mixed multipartite quantum states
• QWIRE Practice: Formal Verification of Quantum Circuits in Coq
• A Theorem Prover for Quantum Hoare Logic and Its Applications

Cited by in corpus (5)

• Quantum Hoare logic with classical variables
• QECV: Quantum Error Correction Verification
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
• Separation of gates in quantum parallel programming
• Formal Semantics of a Classical-Quantum Language