Verification of Recursively Defined Quantum Circuits
Mingsheng Ying, Zhicheng Zhang
TL;DR
This paper presents a proof system for formal verification of the correctness of recursively defined quantum circuits, and the soundness and (relative) completeness of the proof system are established.
Abstract
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and economically programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrating its effectiveness, a series of application examples of the proof system are given, including (multi-qubit) controlled gates, a quantum circuit generating (multi-qubit) GHZ (Greenberger-Horne-Zeilinger) states, recursive definition of quantum Fourier transform, quantum state preparation, and quantum random-access memories (QRAM).