Laws of Quantum Programming

TL;DR

This paper develops and formally verifies fundamental algebraic laws for quantum programming, extending classical laws to the quantum domain and enabling correctness-preserving transformations and optimizations.

Contribution

It introduces a comprehensive set of quantum programming laws, including laws for quantum if-statements, loops, and normal forms, all mechanically verified in Coq.

Findings

Formal laws for quantum programming are established and verified in Coq.

Derived a fixpoint characterization of quantum while-loops.

Presented a formal derivation of the principle of deferred measurements.

Abstract

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) if-statements and the unfolding of nested (quantum) 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 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.