Lisp松散地作为什么样的lambda演算的例子?

Lisp是一种动态类型语言,它是否大致对应于非类型lambda微积分?

是的,但只是粗略地说。在“纯”非类型化lambda微积分中,所有东西都被编码为函数。(你可以在谷歌上搜索流行的“教堂编码”和不太流行的“斯科特编码”。)Lisp有非功能数据,比如原子和数字等,所以这可以算作“非类型化lambda微积分用常量扩展”。

另一个重要区别是 估价顺序 . 减少lambda微积分项的规则是高度不确定性的。(有一个定理,即Church-Rosser定理,它松散地说,只要事物终止,评价顺序就不重要。)实际上,lambda术语通常使用最左边的最外面的,也就是“正常顺序”的约简,因为如果 任何 减缩策略终止了。 这与Lisp非常不同,Lisp总是在进行beta缩减之前将参数评估为正常形式。此评估顺序称为“按值调用”。

总之,lisp对应于 用常量扩展的非类型化、按值调用的lambda微积分 .

约翰·麦卡锡介绍了Lisp his April, 1960 paper "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I" . 以下段落摘自第6页:

e.功能和形式。在数学逻辑之外的“数学”中,不精确地使用“函数”这个词,并将其应用于形式是很常见的。 如Y ^二 +因为我们以后要用函数表达式来计算, 我们需要区分函数和形式以及表示- 这一区别。这个区别和描述它的符号,从 我们的偏离很小,这是由教会给出的[3]。
…
三。A.教堂,lambda转换的计算(普林斯顿大学 出版社,普林斯顿,新泽西州,1941年)。

这个 Wikipedia article on lambda-calculus 有教会出版物的历史。麦卡锡引用的1941年的论文似乎是关于 类型化的 lambda微积分,与维基百科文章的引言相矛盾。

这个 lambda Lisp中的关键字只能通过类比理解为指lambda微积分。Lisp lambda表达式是 anonymous function .

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

如果您想通过there类型系统识别lambda计算,那么lisp当然是它自己的。任何Lisp中的“lambda”关键字在scheme之前都是自命不凡的,而在scheme之后也有说不出的余地。使用“func”会更谦虚。Lisp主要是列表处理器,而不是“lambda演算”

我还写了一篇关于这一点的相当广泛的文章,试图说明为什么a:术语“函数式编程”毫无意义,b:为什么说“lambda微积分”而不是“类型系统”也是如此:

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

另外,请记住,在Lisp中,所有函数都有效 单一论证 只能拥有 列表 作为他们的论点。