用于量子计算的Lambda演算

经典lambda演算既可以看作一种编程语言，也可以看作一个用于推理计算的形式代数系统。它提供了一个与图灵机等价的计算模型，并且在经典计算理论中持续发挥着巨大的作用。我们提出，量子计算与其经典对应物一样，可能受益于一个适合表达和推理量子算法的lambda演算版本。在本文中，我们发展了一个量子lambda演算作为量子计算的替代模型，它结合了量子图灵机和量子电路模型的一些优点。该演算结果与线性逻辑研究中使用的线性lambda演算密切相关。我们为这个演算建立了一个计算模型和一个等式证明系统，并论证了它与量子图灵机等价。