直觉幺正线性逻辑：纯量子高阶的证明论方法
Intuitionistic Unitary Linear Logic: A Proof-Theoretical Approach to Purely Quantum Higher-Order
浏览论文内容
中文总结 AI 辅助
本文针对线路模型无法表示非因果高阶量子过程的问题，提出基于柯里-霍华德对应的直觉幺正线性逻辑（IULL），证明其一致性、完备性及割规则可容许性，通过实例验证了方法的有效性。
中文摘要 AI 辅助
尽管量子计算的线路模型已成熟，但它无法表示量子开关等非因果高阶量子过程。文献中虽已考虑多种非因果量子计算模型，但相关方法仅聚焦于这类过程的物理性，运用矩阵等线性代数技术，虽具表达力，却仅能提供静态、整体的理解。本文提出一种非因果高阶量子过程的新形式体系，基于柯里-霍华德对应，提供兼具组合性与模块性的计算解释。特别地，我们提出直觉幺正线性逻辑（IULL），一种基于线性逻辑、聚焦于高阶项幺正性保持的逻辑；证明了IULL的一致性、相对于幺正算子的完备性及割规则的可容许性；最后通过用IULL重新审视已知非因果量子过程，讨论了该方法的有效性。
英文摘要
Although the circuit model for quantum computation is well established, it is incapable of representing non-causal higher-order quantum processes such as the quantum switch. If several models of non-causal quantum computation have been considered in the literature, the approaches have so far only been focusing on the physicality of such processes, using matrices and other techniques from linear algebra. If these approaches are expressive, they however only provide a static and monolithic understanding of these processes. In this article, we propose a new formalism for non-causal, higher-order quantum processes. Based on a Curry-Howard interpetation, our proposal offers a computational interpretation that is both compositional and modular. In particular, we present Intuitionistic Unitary Linear Logic (IULL), a logic based on linear logic focusing on conservation of unitarity for higher order terms. We prove the coherence of IULLL, its completeness with regard to unitaries, and the admissibility of its cut rules. We finally discuss the validity of our approach by revisiting known non-causal quantum processes with IULL.
发表机构
- Université Paris-Saclay, CentraleSupélec, CNRS, ENS Paris-Saclay, Inria（巴黎萨克雷大学、中央苏伊耶克学院、法国国家科学研究中心、巴黎萨克雷高等师范学院、法国国家信息与自动化研究所）
机构由 AI 辅助整理，请以论文原文为准。
