functional-programming - 什么是 Lambda 可定义性？

Question

当我在阅读 lambda 演算时，遇到了Lambda 可定义性这个词。有人可以解释那是什么，因为我找不到任何好的资源。

谢谢

Answer 1

更一般地说，有一系列研究试图在广泛的语言类别中描述“lambda 可定义性”。“lambda 可定义性”本身通常与以集合形式给出的语言语义相关。对于T我们语言中的类型，将|T|其解释为一个集合。现在，取一个元素|T|-- 调用它e。我们想知道我们的语言中是否有一个术语——称之为x : T（T 类型的 x），这样 |x| 是e。如果有这样一个术语，那么我们说它t是 lambda 可定义的。

现在，在我们的完美世界中，当我们将一种语言解释为集合时，我们想说与每种类型关联的集合正是那些包含该类型的 lambda 可定义元素且仅包含 lambda 可定义元素（完整性）的集合. 这也很好，也许可以说我们可以提供一种算法来确定集合中声明的元素是否具有关联的 lambda 项（可判定性）。

现在，我们通常不只是建模成集合，而是建模成其他有趣的数学结构。而且我们不仅仅从 lambda 演算建模，而是从其他相关系统建模，例如 Plotkin 的 PCF 等。但研究中的属性通常仍称为“lambda-definability”。

经过几十年的研究，在这方面仍有许多悬而未决的问题和疑问——虽然某些低阶项已被证明具有可判定的 lambda 可定义性（经典结果涉及高达二阶的项），但许多项并没有产生这么容易。这篇论文（Ralph Loader 的“The Undecidability of lambda-Definability”）给出了一个重要的这种不可判定性结果并描述了一些后果：http ://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.6860

Answer 2

请参阅Church-Turing论文，其中 lambda 可定义函数（来自 Church）是那些为我们提供“有效可计算”函数的函数。图灵表明，可在图灵机上实现的程序等价于 lambda 可定义函数。