量子编程的法则

《ACM Transactions on Software Engineering and Methodology》：Laws of Quantum Programming

量子编程基本定律研究：扩展Hoare经典定律至量子场景，涵盖量子条件语句展开、循环归约及正规形式定理，通过Coq实现形式化验证，并应用推导动态量子电路的延迟测量原理。

　　

摘要

在本文中，我们研究了量子编程的基本规律。我们将Hoare等人提出的经典编程基本规律扩展到了量子计算环境中。这些规律描述了量子程序的代数特性，例如（量子）if语句的顺序组合的分配律，以及嵌套（量子）if语句的展开过程。同时，我们阐明了某些经典编程规律与其量子对应规律之间的细微差异。此外，我们推导出了量子while循环的不动点特征，并提出了量子编程中基于循环的尾递归实现方法。我们还建立了两个规范形式定理：一个针对量子电路，另一个针对有限量子程序。这些规律是在Coq证明辅助工具中形式化定义的，并且所有这些规律都经过了机械验证。作为我们理论的应用案例，我们给出了动态量子电路中延迟测量原理的形式化推导。

我们期望这些规律能够在量子编程的正确性保持转换、编译和自动代码优化中得到应用。特别是因为这些规律在Coq中经过了形式验证，因此可以在量子程序开发中放心地使用它们。