一句话：提出量子分离逻辑 RapunSL，引入线性组合与混合连接词，将叠加态与混合态推理归约为纯态推理。
量子分离逻辑（QSL）通过把分离解释为去纠缠，并借助 frame rule 支持仅涉及纠缠量子比特的局部规约，提升了量子程序演绎推理的可扩展性。本文识别出量子域独有的两类局部性：基局部性（basis-locality）与结果局部性（outcome-locality），并提出新型量子分离逻辑 RapunSL。其核心是引入线性组合与混合两个连接词，与分离结合后，可分别将叠加态上的推理可靠地归约到纯态，将测量产生的混合态上的推理归约到纯态。作者在一系列挑战性案例上验证了该逻辑，表明推理可扩展性显著提升。
Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement , and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL , which is able to soundly reduce reasoning about superposition states to reasoning about pure states ( basis-locality ), and reasoning about mixed states arising from measurement to reasoning about pure states ( outcome-locality ). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-23472,
title = {RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing},
author = {Yusuke Matsushita and Kengo Hirata and Ryo Wakizaka and Emanuele D'Osualdo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776648}
}