一句话:提出统一量子与经典计算的语言 Qunity,以统一语法和指称语义保证量子有效性,并可编译到 OpenQASM。
现有量子编程语言多将量子特性作为经典语言的附加组件,缺乏统一视角。Qunity 将量子计算视为经典计算的推广,提出统一语法:同一构造可同时具有量子与经典效应,例如用和类型实现线性算子直和、异常处理实现投影测量、别名引发纠缠。语言利用被忽视的 BQP 子程序定理,通过反计算垃圾输出从不可逆量子算法构造可逆子程序。论文给出 Qunity 的语法、类型系统与新型指称语义,保证程序量子力学有效,并展示其能清晰表达若干量子算法,且可编译到 OpenQASM 等低级量子比特电路语言,证明设计的可实现性。
We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax where familiar programming constructs can have both quantum and classical effects. For example, one can use sum types to implement the direct sum of linear operators, exception-handling syntax to implement projective measurements, and aliasing to induce entanglement. Further, Qunity takes advantage of the overlooked BQP subroutine theorem, allowing one to construct reversible subroutines from irreversible quantum algorithms through the uncomputation of "garbage" outputs. Unlike existing languages that enable quantum aspects with separate add-ons (like a classical language with quantum gates bolted on), Qunity provides a unified syntax and a novel denotational semantics that guarantees that programs are quantum mechanically valid. We present Qunity's syntax, type system, and denotational semantics, showing how it can cleanly express several quantum algorithms. We also detail how Qunity can be compiled into a low-level qubit circuit language like OpenQASM, proving the realizability of our design.
@article{paperbot2087,
title = {Qunity: A Unified Language for Quantum and Classical Computing},
author = {Finn Voichick and Liyi Li and Robert Rand and Michael Hicks},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571225}
}