Laws of Quantum Programming

In this paper, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.'s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of quantum programs, such as the distributivity of sequential composition over (quantum) \({\mathbf{if}}\) -statements and the unfolding of nested (quantum) \({\mathbf{if}}\) -statements. At the same time, we clarify some subtle differences between certain laws of classical programming and their quantum counterparts. Additionally, we derive a fixpoint characterisation of quantum \({\mathbf{while}}\) -loops and a loop-based realisation of tail recursion in quantum programming. Furthermore, we establish two normal form theorems: one for quantum circuits and one for finite quantum programs. The theory in which these laws are established is formalised in the Coq proof assistant, and all of these laws are mechanically verified. As an application case of our laws, we present a formal derivation of the principle of deferred measurements in dynamic quantum circuits. We expect that these laws can be utilised in correctness-preserving transformation, compilation, and automatic code optimisation in quantum programming. In particular, because these laws are formally verified in Coq, they can be confidently applied in quantum program development.