Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs

TL;DR

This paper introduces a first-order extension of Birkhoff-von Neumann quantum logic with quantifiers over quantum variables, enabling formal reasoning about quantum programs and properties, and integrating it into quantum Hoare logic for verification.

Contribution

It fills a gap by developing the first-order quantum logic with quantifiers over quantum variables and incorporates it into quantum Hoare logic for program verification.

Findings

Logic is suitable for specifying properties in quantum computation.

It enables defining quantum generalisations of classical verification rules.

Potential for building verification tools with proof assistants.

Abstract

A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties (e.g. correctness) of quantum programs. Surprisingly, such a logic is missing in the literature, and the existing first-order Birkhoff-von Neumann quantum logic deals with only classical variables and quantifications over them. In this paper, we fill in this gap by introducing a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables. Examples are presented to show our logic is particularly suitable for specifying some important properties studied in quantum computation and quantum information. We further incorporate this logic into quantum Hoare logic as an assertion logic so that it can play a role similar to that of first-order logic for classical Hoare logic and BI-logic for separation logic. In particular, we show how it can be used to define and derive quantum generalisations of some adaptation rules that have been applied to significantly simplify verification of classical programs. It is expected that the assertion logic defined in this paper - first-order quantum logic with quantum variables - can be combined with various quantum program logics to serve as a solid logical foundation upon which verification tools can be built using proof assistants such as Coq and Isabelle/HOL.