functional-programming - 图灵机和 Lambda 微积分等价

Question

我想知道任何人都可以笼统地向我解释 Lambda 演算和图灵机等价的一些证明以及证明的一般方法。尽可能通俗易懂。

Answer 1

用非常基本的术语来说，您只需证明两件事：

1. 对于任何 lambda 项，都有一个图灵机可以计算相同的东西
2. 对于任何图灵机，都有一个计算相同事​​物的 lambda 项

当然，这里涉及到一些手动操作，因为您还需要考虑输入/输出的操作差异，但我们在这里不涉及。

在实践中，上述两个定理得到了建设性的证明，即通过实际给出一种将一个变成另一个的机械方式。所以基本上你给了两个编译器，以及它们的正确性证明。

为了获得良好的直觉，请考虑 lambda 演算和寄存器机器之间的类似等价定理。在这种情况下，摆脱了真实计算机的有限性，无类型 lambda 演算的解释器是一个方向的证明。我在这里指的是一个真实的、有形的程序，你可以运行它；例如，通过从函数式编程语言的编译器中删除类型检查器（它必然会嵌入一些 lambda 演算的类型化版本。

所以下次你运行 GHC 时，想想这个定理！

Answer 2

我相信门逻辑（硬件）、Lambda 演算（数学/抽象）和图灵机（抽象图像）从不同的角度来看是相同的操作。门逻辑是移位的位/电流。您可以自己手动实现（实验套件、面包板、硬件）或使用逻辑门模拟器（软件）对其进行测试。Lambda 演算是一个形式化的数学概念，用于证明您机械地执行的操作将始终具有相同的输出/结果。图灵机只是一个更抽象的解释这一点的方法，没有数学也没有盖茨。告诉你奶奶冯诺依曼架构，把数学、电气和软件工程留在实验室。在门逻辑中，您将创建一个锁存器，该锁存器将根据输入保持位/状态。在 lambda 演算中，每一位都是一个符号，而 lambda 本身就是转换/归约的符号。在图灵机中，位是寄存器。我通过 Principia Mathematica、Tractatus-Logico Philosophicus 和 Lambda Calculus 学到了这一点：最短的解释是最糟糕的，因为最抽象。您将需要时间观察树木，让它们变成森林。