27

我试图更好地掌握类型如何在 lambda 演算中发挥作用。诚然，很多类型理论的东西都超出了我的想象。Lisp 是一种动态类型的语言，它会大致对应于无类型的 lambda 演算吗？还是有某种我不知道的“动态类型的 lambda 演算”？

4

3 回答 3

39

Lisp 是一种动态类型的语言，它会大致对应于无类型的 lambda 演算吗？

是的，但只是粗略的。在“纯”无类型 lambda 演算中，一切都被编码为函数。（你可以在谷歌上搜索流行的“Church 编码”和不太流行的“Scott 编码”。）Lisp 有非函数数据，比如原子和数字等，所以这可以算作“用常量扩展的无类型 lambda 演算”。

另一个重要的区别是评估顺序。减少 lambda 演算项的规则是高度不确定的。（有一个定理，Church-Rosser 定理，它松散地说，只要事情终止，求值顺序就无关紧要。）在实践中，通常使用最左外最上的“正常顺序”减少来减少 lambda 项，因为如果任何减少策略都会终止，就是这样。这与 Lisp 非常不同，Lisp 总是在进行 beta 缩减之前将参数评估为正常形式。此评估顺序称为“按值调用”。

总而言之，Lisp 对应于一个无类型的、按值调用的 lambda 演算，它扩展了 constants。

于 2010-05-01T18:38:44.103 回答
3

John McCarthy 在他 1960 年 4 月的论文“符号表达式的递归函数及其机器计算，第一部分”中介绍了 LISP 。以下段落来自第 6 页：

e. 功能和形式。在数学中——在数理逻辑之外——通常不精确地使用“函数”这个词并将其应用于诸如 y 2 + x 之类的形式。因为稍后我们将使用函数的表达式进行计算，所以我们需要函数和形式之间的区别以及表示这种区别的符号。Church [3] 给出了这种区别和描述它的符号，我们与此稍有不同。
...
3. A. CHURCH，Lambda 转换的微积分（普林斯顿大学出版社，新泽西州普林斯顿，1941 年）。

关于 lambda-calculus的Wikipedia 文章有 Church 出版物的历史。McCarthy 引用的 1941 年论文似乎是关于类型化的lambda 演算，与 Wikipedia 文章的介绍相矛盾。

Lisp 中的lambda关键字只能通过类比理解为指代 lambda 演算。Lisp lambda 表达式是一种匿名函数。

于 2010-05-01T15:16:59.270 回答
-6

Lisp 不是“lambda 演算”，我不知道“lambda 演算”是什么。

如果您想通过那里的类型系统识别 lambda 演算，那么 Lisp 当然是它自己的。在 Scheme 之前的任何 lisp 中的 'lambda' 关键字肯定是自命不凡的，在 Scheme 之后也有空间说它是。仅仅使用'func'会更谦虚。Lisp 主要是一个列表处理器，而不是“lambda 演算”

有一次我也写了一篇相当广泛的文章，试图证明为什么 A：“函数式编程”这个词没有意义，B：为什么说“lambda 演算”而不是“类型系统”也是如此：

http://blog.nihilarchitect.net/archives/289/on-functional-programming/

另外，请记住，在 Lisp 中，所有函数实际上都是单个参数，并且只能将列表作为参数。

于 2010-05-18T04:05:58.280 回答