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.

翻译：量子分离逻辑（QSL）已被提出作为提升量子程序演绎推理可扩展性的有效工具。在QSL中，分离被解释为解纠缠，而框架规则引入了一种纠缠局部规范的概念（即仅讨论与程序所作用量子比特纠缠的量子比特）。本文识别了量子领域特有的两种局部性概念，并构建了一种新型量子分离逻辑——RapunSL，它能够可靠地将关于叠加态的推理约简为关于纯态的推理（基局部性），并将由测量产生的混合态推理约简为关于纯态的推理（结果局部性）。为此，我们引入了两种联结词：线性组合与混合，它们与分离结合显著提升了推理的可扩展性，我们通过一系列具有挑战性的案例研究对此进行了验证。