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