将定量语义应用于高阶量子计算

论文信息（2014，POPL；预印本：2013）：Michele Pagani、Peter Selinger、Benoît Valiron。arXiv:1311.2290

工作

本文处理高阶量子计算的指称语义问题，目标是同时保留递归、无限数据类型和量子纠缠。作者使用定量语义与线性逻辑中的构造，为量子 Lambda 演算建立语义模型，试图克服以往工作要么限制在过小的有限片段、要么牺牲重要量子特征的困难。

主要贡献

• 为带递归和无限数据类型的高阶量子 Lambda 演算提出指称语义。
• 将定量语义中的线性逻辑构造用于量子计算。
• 在高阶语义中保留对纠缠等量子现象的表达能力。
• 说明高阶函数、递归与量子资源可以在统一模型中讨论。

局限与适用范围

该语义是理论模型，不是高阶量子语言的完整编译器或硬件实现。递归、无限数据和量子纠缠带来的数学结构仍要求明确的域、度量和近似解释；语义存在不自动给出程序终止、效率、数值误差或设备执行证明。

与其他工作的关系

本文延续 带经典控制的量子 Lambda 演算 与 QML 的函数式量子语言路线，并回应 QPL 对递归和语义的需求。与 量子循环程序 相比，本文关注高阶函数和无限数据的语义；与 Dagger 紧闭范畴与完全正映射 相比，它处理更高阶、带递归的量子程序。

原论文

Michele Pagani, Peter Selinger, and Benoît Valiron, Applying Quantitative Semantics to Higher-Order Quantum Computing, in POPL 2014. arXiv:1311.2290