论文标题
扭曲：量子程序中纯度和纠缠的合理推理
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
论文作者
论文摘要
量子编程语言使开发人员能够为量子计算机实施算法，这些计算机承诺在经典棘手的任务中的计算突破。编程量子计算机需要意识到纠缠，这是量子量结果相关的现象。纠缠可以确定算法的正确性和编程模式的适用性。 在这项工作中，我们将纯度正式化为自动化量子程序纠缠的推理的核心工具。纯表达是一种表达式，其评估不受其不拥有的量子位的测量结果的影响，这意味着在计算中与任何其他表达式纠缠着纠缠的自由。 我们提出Twist，这是一种具有用于纯度的声音推理的类型系统的第一语言。类型系统使开发人员能够使用类型注释来识别纯表达式。扭曲还具有纯度断言操作员，该操作员说明量子门输出中没有纠缠。为了彻底检查这些断言，Twist结合了静态分析和运行时验证的组合。 我们在模拟中评估了Twist的类型系统，并在量子程序的基准套件上进行分析，表明Twist可以表达量子算法，捕获编程错误，并支持几种语言不允许的程序，同时会导致运行时验证在不到3.5％的情况下引起运行时验证。
Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement, the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns. In this work, we formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation. We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification. We evaluate Twist's type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that several languages disallow, while incurring runtime verification overhead of less than 3.5%.
