Structured Theorem for Quantum Programs and its Applications

This article proves a structured program theorem for flowchart quantum programs. The theorem states that any flowchart quantum program is equivalent to a single quantum program that repeatedly executes a quantum measurement and a subprogram, so long as the measurement outcome is true. Moreover, their expected runtime, variance, and general moments are the same. This theorem simplifies the quantum program's verification significantly.-We derive an analytical characterization of the termination problem for quantum programs in polynomial time. Our procedure is more efficient and accurate with much simpler techniques than the analysis of this problem, as described in [29].-We compute the expected runtime analytically and exactly for quantum programs in polynomial time. This result improves the methods based on the weakest precondition calculus for the question recently developed in [31, 34].-We show that a single loop rule is a relatively complete Hoare logic for quantum programs after applying our structured theorem. Although using fewer rules, our method verifies a broader class of quantum programs, compared with the results in [45] and [56].