基于非幂等 Kleene 代数的量子程序代数推理
编程语言
2022-03-30 v2 量子物理
摘要
受基于 Kleene 代数的经典程序分析成功经验的启发，我们研究了量子程序的代数推理。此类的一个突出例子是著名的带测试的 Kleene 代数（KAT），它既提供了理论洞见也提供了实用工具。鉴于现有大多数方法都涉及指数大小的矩阵，代数推理的简洁性对于量子程序的可扩展分析尤为可取。然而，由于量子程序独特的量子特性（尤其在分支方面），KAT 的一些关键特性（包括幂等律和经典测试的优良性质）在量子程序语境中不再成立。我们提出非幂等 Kleene 代数（NKA）作为一种自然的替代方案，并确定了 NKA 的完备且可靠的语义模型及其量子解释。受 KAT 应用的启发，我们在 NKA 中给出了量子编译器优化和量子 while 程序正规形式的代数证明。此外，我们将 NKA 扩展为带测试的 NKA（即 NKAT），其中测试依据效应代数对量子谓词建模，并说明了如何将命题量子 Hoare 逻辑编码为 NKAT 定理。
引用
@article{arxiv.2110.07018,
title = {Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra},
author = {Yuxiang Peng and Mingsheng Ying and Xiaodi Wu},
journal= {arXiv preprint arXiv:2110.07018},
year = {2022}
}
备注
extended version, 23 pages, 6 figures, to appear at the 43rd ACM SIGPLAN PLDI 2022