Papers
一种函数式量子编程语言
A Functional Quantum Programming Language
Altenkirch 与 Grattage 提出 QML，用有限类型、线性逻辑和范畴语义表达可逆与不可逆量子计算。
论文信息（正式版本：2005，LICS，pp. 249–258；预印本：2004）：Thorsten Altenkirch、Jonathan Grattage。DOI；arXiv:quant-ph/0409065
工作
本文提出 QML，一种面向有限类型量子计算的函数式语言。程序被解释为有限量子计算范畴中的态射，语义既要表达可逆量子门，也要表达测量等不可逆计算。语言使用一阶严格线性逻辑，把 weakening（显式丢弃）作为资源行为的一部分；严格程序不会引入退相干，因此可以保持叠加和纠缠。
主要贡献
- 提出把函数式语法、量子数据和有限类型结合起来的 QML 设计。
- 用范畴语义描述可由量子门实现的可逆与不可逆计算。
- 用严格线性逻辑区分可使用、可丢弃和必须保持的量子资源。
- 说明无退相干的严格程序如何保持叠加与纠缠。
局限与适用范围
QML 的对象主要是有限类型和理想化量子计算；范畴语义不等于某一硬件后端的编译器或噪声模型。线性规则说明资源使用，但不自动证明算法的复杂度、数值精度或设备执行正确性。不可逆操作、测量和丢弃的实现成本仍需单独分析。
与其他工作的关系
它把 QPL 语言 的类型化语言方向推进到函数式和范畴语义，并与 量子计算 Lambda 演算 共享线性资源的动机。与 带经典控制的量子 Lambda 演算 相比，QML 更突出有限类型、可逆性和严格程序。其组合式语义也可与 量子协议的范畴语义 对照。
原论文
Thorsten Altenkirch and Jonathan Grattage, A Functional Quantum Programming Language, in LICS 2005, pp. 249–258, DOI: 10.1109/LICS.2005.1. arXiv:quant-ph/0409065
本词条用于学习导览。正式引用与技术细节请以文末原始文献为准。
继续阅读带经典控制的量子计算 Lambda 演算→