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.
翻译:当前的量子程序编写仍处于较低的抽象层次——量子电路类似于汇编语言——即使是先进的量子编程语言中的酉算子部分本质上仍充当电路描述语言的角色。这种现状阻碍了可扩展性、清晰度以及对更高层次推理的支持。需要更抽象、更具表达力的量子编程构造。为此,我们引入了一种从“仅一种相位”生成酉算子的简洁语法:我们结合了捕获相位偏移的(全局)相位操作与通过模式匹配捕获子空间选择的量子版“if let”构造。这种最小化语言将关注点从量子门提升到特征分解、共轭变换和受控酉算子——这些是量子算法设计中常见的构建模块。我们通过多种方式展示了该语言的表达能力。首先,通过推导通用量子门集合,我们证明了该表示方法具有普适性。其次,我们展示了重要量子算法能够被自然且简洁地表达,包括Grover搜索算法、哈密顿量模拟、量子傅里叶变换、量子信号处理以及量子特征值变换。此外,我们建立了基于范畴量子力学的清晰指称语义。最后,我们实现了一个原型编译器,能够高效地将该语言的项翻译为量子电路,并证明其相对于这些语义的可靠性。这些成果共同表明,该构造为实现更抽象、结构化的量子编程提供了原则性且实用的途径。