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

Question

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

谢谢

Answer 1

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

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

现在，通常我们不仅将模型建模为集合，而且还建模为其他有趣的数学结构。我们不仅仅从 lambda 演算建模，而是从其他相关系统(例如 Plotkin 的 PCF 等)建模。但是所研究的属性通常仍称为“lambda 可定义性”。

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