论文标题
Birkhoff-Von Neumann量子逻辑作为量子程序的断言语言
Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs
论文作者
论文摘要
需要具有量子变量的一阶逻辑作为一种断言语言，以指定和推理量子程序的各种属性（例如正确性）。令人惊讶的是，文献中缺少这样的逻辑，现有的一阶Birkhoff-von Neumann量子逻辑仅处理经典变量和对它们的量化。在本文中，我们通过引入birkhoff-von neumann量子逻辑的一阶扩展，并在量子变量上引入了birkhoff-von neumann量子逻辑的一阶扩展。列出了示例以表明我们的逻辑特别适合指定量子计算和量子信息中研究的一些重要属性。我们将此逻辑进一步纳入量子hoare逻辑中，作为断言逻辑，以便它可以扮演与经典hoare逻辑的一阶逻辑相似的角色，用于分离逻辑。特别是，我们展示了如何使用它来定义和得出某些适应规则的量子概括，这些规则已应用于显着简化经典程序的验证。可以预期，本文定义的断言逻辑（具有量子变量的一阶量子逻辑）可以与各种量子程序逻辑相结合，以作为可靠的逻辑基础，可以在该基础上使用COQ和ISABELLE/HOL等证明助手来构建验证工具。
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.
