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.
翻译:量子变量的第一阶逻辑需要用量子变量作为确定和推理量子程序各种属性(例如正确性)的判断语言。 令人惊讶的是, 文献中缺少这种逻辑, 而现有的第一阶Birkhoff- von Neumann 量子逻辑仅涉及古典变量和定量。 在本文中, 我们通过引入伯克霍夫- von Neumann 量子逻辑的第一阶扩展, 并采用通用和存在性量化的量子变量来填补这一空白。 举例显示, 我们的逻辑特别适合在量子计算和量子信息中具体研究的一些重要属性。 我们进一步将这种逻辑纳入量子 Hoare 逻辑, 作为一种理论逻辑, 这样它可以发挥类似于古典Hare逻辑和BI- logical 逻辑的类似作用。 特别是, 我们展示如何使用它来界定和得出某些适应规则的量子概观, 用来大大简化典型程序的核查。 人们预计, 本文中定义的逻辑逻辑―― 第一阶子逻辑和量子变量的逻辑, 可以与各种量子逻辑基础结合起来, 。