lisp - 什么类型的 lambda 演算会松散地成为 Lisp 的一个例子？

Question

我正试图更好地掌握类型在 lambda 演算中的作用。诚然，很多类型论的东西都超出了我的理解范围。 Lisp 是一种动态类型的语言，它会大致对应于非类型化的 lambda 演算吗？或者是否存在某种我不知道的“动态类型 lambda 演算”？

Answer 1

Lisp is a dynamically typed language, would that roughly correspond to untyped lambda calculus?

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

另一个重要的区别是评估顺序。减少 lambda 演算项的规则是高度不确定的。 (有一个定理，Church-Rosser 定理，它笼统地说只要事物终止，评估的顺序就无关紧要。)在实践中，lambda 项通常使用最左-最外层也称为“正常顺序”减少来减少，因为如果任何减少策略都会终止，那个会终止。这与 Lisp 非常不同，Lisp 总是在进行 beta 归约之前将参数评估为范式。这种评估顺序称为“按值调用”。

总而言之，Lisp 对应于一种无类型、用常量扩展的按值调用 lambda 演算。