量子循环程序

论文信息（正式版本：2010，Acta Informatica 47(4):221–250；预印本：2006）：Mingsheng Ying、Yuan Feng。arXiv:quant-ph/0605218

工作

本文把循环作为量子程序的一等构造，研究其迭代语义、终止性和 almost termination（几乎终止）。循环的每次迭代可以包含量子操作与测量分支，因而不能简单套用有限线路的矩阵乘法。论文建立相应的函数语义，并用量子游走说明循环模型的表达能力。

主要贡献

• 系统描述量子循环的计算过程和函数语义。
• 分析量子程序的终止与几乎终止行为。
• 处理测量分支和反复迭代带来的概率语义问题。
• 将量子循环框架应用到量子游走等示例。

局限与适用范围

循环语义依赖所选状态空间、测量规则和终止概率定义；论文模型不自动提供所有循环的不变量或可判定性结果。它是理想化语义，不包含设备噪声、运行时调度和硬件资源成本。将理论终止性结论转化为具体程序证明仍需额外的规范和推理工具。

与其他工作的关系

本文补足 指称语义 对循环和递归需要不动点处理的说明，并为 量子最弱前置条件 与 量子程序的 Floyd–Hoare 逻辑 提供循环语义背景。与 量子线路 的有限静态模型相比，量子循环程序可以表达动态迭代和终止行为。

原论文

Mingsheng Ying and Yuan Feng, Quantum Loop Programs, Acta Informatica 47(4), 221–250 (2010). arXiv:quant-ph/0605218