量子编程的法则

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

【字体: 时间:2025年11月08日 来源:ACM Transactions on Software Engineering and Methodology

编辑推荐:

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

  

摘要

在本文中,我们研究了量子编程的基本规律。我们将Hoare等人提出的经典编程基本规律扩展到了量子计算环境中。这些规律描述了量子程序的代数特性,例如(量子)if语句的顺序组合的分配律,以及嵌套(量子)if语句的展开过程。同时,我们阐明了某些经典编程规律与其量子对应规律之间的细微差异。此外,我们推导出了量子while循环的不动点特征,并提出了量子编程中基于循环的尾递归实现方法。我们还建立了两个规范形式定理:一个针对量子电路,另一个针对有限量子程序。这些规律是在Coq证明辅助工具中形式化定义的,并且所有这些规律都经过了机械验证。作为我们理论的应用案例,我们给出了动态量子电路中延迟测量原理的形式化推导。
我们期望这些规律能够在量子编程的正确性保持转换、编译和自动代码优化中得到应用。特别是因为这些规律在Coq中经过了形式验证,因此可以在量子程序开发中放心地使用它们。
相关新闻
生物通微信公众号
微信
新浪微博
  • 搜索
  • 国际
  • 国内
  • 人物
  • 产业
  • 热点
  • 科普
  • 急聘职位
  • 高薪职位

知名企业招聘

热点排行

    今日动态 | 人才市场 | 新技术专栏 | 中国科学人 | 云展台 | BioHot | 云讲堂直播 | 会展中心 | 特价专栏 | 技术快讯 | 免费试用

    版权所有 生物通

    Copyright© eBiotrade.com, All Rights Reserved

    联系信箱:

    粤ICP备09063491号