Reasoning about Parallel Quantum Programs
share
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; and (2) prove a strong soundness theorem of these proof rules showing that partial correctness is well maintained at each step of transitions in the operational semantics of a parallel quantum program. 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. It seems that a full solution to these challenges and developing a (relatively) complete proof system for parallel quantum programs are still far beyond the current reach.
READ FULL TEXT