paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Quantum Circuits Are Just a Phase

量子电路只是一个相位
POPL 10(POPL)2026匹配度 2/10 · 论文属于量子编程语言、范畴语义与编译器方向,与用户核心关注的 PL 与 AI/Agent、静态分析、浮点程序分析、贝叶斯程序分析交叉点几乎没有直接关联。仅在形式语义与可靠编译器的方法论上与用户的 PL 兴趣有微弱重叠,因此匹配度很低。引用 6 inbox
Chris Heunen, Louis Lemonnier, Christopher McNally, Alex Rice
crossref: 2026-09-10

AI 速览

一句话:提出仅用相位操作与 if-let 式子空间选择的量子编程原语,并给出范畴语义与可靠编译器。

当前量子程序多处于类似汇编的电路层,高级语言中的酉算子部分也基本等同于电路描述,阻碍可扩展性、清晰性与高层推理。论文提出一种极简语言,从“相位”生成酉算子:用全局相位操作刻画相位移动,用量子版“if let”通过模式匹配实现子空间选择,使关注点从门转向本征分解、共轭与控制酉。作者证明该表示通用,可导出通用量子门集;能自然简洁表达 Grover 搜索、哈密顿模拟、量子傅里叶变换、量子信号处理和量子本征值变换;给出基于范畴量子力学的指称语义,并实现原型编译器把项高效翻译为量子电路,且证明其相对该语义可靠。

问题
当前量子编程抽象层次低,酉算子部分基本等同电路描述,难以扩展、清晰表达和支持高层推理。
方法
提出由全局相位操作与量子版 if let 子空间选择构成的极简语言,从相位生成酉算子,并给出范畴量子力学指称语义与到量子电路的原型编译器。
评估
证明表示通用并可导出通用门集,展示多种量子算法可简洁表达,实现编译器并证明其相对指称语义可靠。
原文摘要(Abstract)

Quantum programs today are written at a low level of abstraction—quantum circuits akin to assembly languages—and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed. To this end, we introduce a simple syntax for generating unitaries from “just a phase”; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the “if let” construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design. We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover’s search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-2507-11676,
  title = {Quantum Circuits Are Just a Phase},
  author = {Chris Heunen and Louis Lemonnier and Christopher McNally and Alex Rice},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776731}
}