【发布时间】：2012-07-07 09:43:50
【问题描述】：
在阅读 lambda 演算时，遇到了 Lambda 可定义性这个词。有人可以解释这是什么，因为我找不到任何好的资源。
谢谢
【问题讨论】：
-
能否给个报价和出处？
标签： functional-programming lambda-calculus
【发布时间】：2012-07-07 09:43:50
【问题描述】：
更一般地说，有一系列研究试图在广泛的语言类别中描述“lambda 可定义性”。 “lambda 可定义性”本身通常与以集合形式给出的语言语义相关。对于我们语言中的类型T，写|T| 将其解释为一个集合。现在，取一个|T| 的元素——称之为e。我们想知道我们的语言中是否有一个术语——称之为x : T（T 类型的x），这样|x|是e。如果有这样的术语，那么我们说t 是 lambda 可定义的。
现在，在我们的完美世界中，当我们将一种语言解释为集合时，我们想说与每种类型关联的集合正是那些包含该类型的 lambda 可定义元素的集合，并且仅 em> 可定义 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
【讨论】：
请参阅Church-Turing 论文，其中 lambda 可定义函数（来自 Church）是那些为我们提供 "effectively computable" 函数的函数。图灵表明，可在图灵机上实现的程序等价于 lambda 可定义函数。
【讨论】：