量子最弱前置条件

论文信息（2006，MSCS 16(3):429–451）：Ellie D’Hondt、Prakash Panangaden。DOI；作者存档 PDF；早期 arXiv 版本

工作

本文为量子计算建立适合的 predicate transformer，尤其是 weakest precondition（wp）。给定程序的状态变换和一个后置谓词，wp 反向描述哪些输入状态足以保证该后置条件。作者证明状态变换语义与最弱前置条件语义之间存在 Stone 型对偶，并利用 Kraus 表示定理说明完全正映射具有相应的最弱前置条件；论文还把 Selinger 语言和 stabilizer 情形作为例子。

主要贡献

• 将最弱前置条件概念直接建立在量子计算语义上，而不是先化约为概率程序。
• 连接 state transformer 与 predicate transformer，给出 Stone 型对偶视角。
• 证明完全正映射的最弱前置条件存在，并以 Kraus 表示为基础。
• 把 Selinger 的量子语言和 stabilizer 情形纳入示例分析。

局限与适用范围

该框架主要处理以算子和完全正映射表示的量子程序；循环、递归、经典存储、非终止和数值近似需要额外的固定点或扩展。wp 公式提供语义推理工具，却不自动生成程序不变量、机器检查证明或硬件噪声保证。后置谓词和偏序的选择也会影响“最弱”的具体含义。

与其他工作的关系

本文直接支撑百科中的最弱前置条件页面，并把 QPL 语言 的超算子语义转成反向谓词变换。它与 命令式量子程序的推理 都关注程序逻辑，但前者强调 transformer 对偶和后置条件反推，后者更强调命令式程序的逻辑系统。后续量子霍尔逻辑和期望运行时间等工作可看作对该方向的扩展。

原论文

Ellie D’Hondt and Prakash Panangaden, Quantum Weakest Preconditions, Mathematical Structures in Computer Science 16(3), 429–451 (2006), DOI: 10.1017/S0960129506005251. 作者存档 PDF; 早期 arXiv 版本