Papers
量子计算的 Lambda 演算
A Lambda Calculus for Quantum Computation
van Tonder 提出结合量子计算、线性 Lambda 演算和等式推理的量子演算模型。
论文信息（2004，SIAM Journal on Computing）：André van Tonder。DOI；arXiv
工作
本文把 Lambda 演算同时当作编程语言和推理代数，提出一个用于量子计算的量子 Lambda 演算。模型结合量子线路和量子图灵机的部分优点，使用与线性逻辑相关的线性 Lambda 演算处理量子资源，并给出计算模型和等式证明系统。作者还论证该演算与量子图灵机之间的对应关系。
主要贡献
- 提出可表达量子算法并支持程序推理的量子 Lambda 演算。
- 建立计算模型与等式证明系统，使程序等价可以在语法层讨论。
- 说明该演算与量子图灵机模型密切相关，并借用线性演算避免无条件复制量子资源。
局限与适用范围
演算的量子操作和等价推理主要服务于理论模型，不能直接说明某个硬件后端如何编译或执行程序。与许多早期模型一样，噪声、测量成本、设备连通性和工程语言接口需要另行定义。与量子图灵机的对应也属于模型层面的结果，不等于对所有实现的性能或正确性证明。
与其他工作的关系
它与 Selinger 的 QPL 语言 都研究量子数据和程序语义，但前者以 Lambda 演算、线性资源和等式证明为核心，后者更直接描述带控制结构的语言。它也可与 量子程序设计 的守卫命令方法比较，并为后来的量子函数式语言提供理论参照。Abramsky 与 Coecke 的 范畴语义 则从协议组合的抽象结构切入。
原论文
André van Tonder, A Lambda Calculus for Quantum Computation, SIAM Journal on Computing 33 (2004), 1109–1135, DOI: 10.1137/S0097539703432165. arXiv:quant-ph/0307150
本词条用于学习导览。正式引用与技术细节请以文末原始文献为准。
继续阅读量子协议的范畴语义→