Tuo*_*nen 11 functional-programming computability lambda-calculus turing-machines computation-theory
我正在尝试围绕 lambda 演算，以及它与语言、编译器和二进制代码的关系。lambda 演算等同于图灵机的实际含义是什么，它实际上在哪里表现出来？
我不明白 lambda 演算如何取代图灵机作为计算的理论模型。图灵机是关于改变状态的顺序指令，lambda 演算是关于对某些东西进行评估的表达式。它更抽象，就像它自己的编程语言，而不是如何实际计算某些东西、使事情发生的模型。或者让我们这样说：lambda 演算就像路线图，而图灵机就像汽车模型。这两个如何被认为是等价的？是否有可能在不实施图灵机的情况下在硬件上运行软件？
例如，lisp 编译器和语言如何与 lambda 演算相关？lambda演算在哪一层实现？就 lambda 演算的定义而言，实现是否纯粹？lambda 演算背后的理论在哪里以及如何将语法转换为正在运行的二进制文件？例如，在 lambda 演算中，数字被编码为应用于其他函数 n 次的特殊函数。然而在语法上，我们使用数字文字。所有这些公理在哪里使用？
在可计算性理论中，两种计算理论模型之间的等效性意味着它们可以解决同一组问题。您可以在图灵机中计算的任何内容，都可以使用 Lambda 演算进行计算，反之亦然。
我们如何证明这一点？可以说，如果我们可以用 lambda 演算对图灵机进行建模，那么显然 lambda 演算可以计算图灵机可以计算的所有内容。如果我们可以在图灵机上求解 lambda 演算，那么反之亦然。
这两种情况都是可能的，因此模型被认为是等效的。
当然，在实践中，一种模型对于某些用例来说可能更实用。今天的计算机基于 RAM 状态模型，而 RAM 状态模型又从图灵机的思想中提供了理论基础。Lambda 演算确实非常抽象，并且它并不容易在物理硬件中实现。然而，这两个模型都存在于同一计算类中，并且它们可以解决相同的问题，因此被称为等效的。
所有这些基础语言都是在计算机出现之前的时代引入的。研究的重点在于描述一类（数字）函数，这些函数在算法意义上看起来“直观”可计算，而不必通过自动设备进行计算。现在，事实证明 lambda 演算和图灵机，以及许多其他计算模型，如组合逻辑、Post 系统、广义递归函数等，都精确地表达了同一类可计算函数。这激发了丘奇的论点。
我同意你的观点，图灵机（如随机访问机）相对于其他模型具有更多的架构风格。事实上，正是这一点让起初有点怀疑的 Goedel 相信 Church 论文的有效性。
我也同意你的观点，即 lambda 演算不能取代图灵机作为计算的理论模型：在这样的操作中没有任何明显的好处。
同时，lambda 演算很有趣，而图灵机却非常无聊。它很有趣，正是因为它与图灵机处于极端相反的位置。我认为人们可以合理地争辩说，它是曾经设想过的最高级别的计算模型（并且可能永远是）。这就是为什么它对每个程序员来说都是一种具有挑战性和指导性的语言。