哪种类型的lambda微积分会宽松地成为一个例子？

Question

我正在尝试更好地了解Lambda演算中的类型如何发挥作用。诚然，很多类型的理论内容都超出了我的脑海。 LISP是一种动态键入的语言，这大致对应于未型的Lambda演算吗？还是我不知道某种“动态键入的lambda微积分”？

Answer 1

LISP是一种动态键入的语言，这大致对应于未型的Lambda演算吗？

是的，但大致。在“纯”未型lambda演算中，所有内容都被编码为函数。 （您可以使用谷歌搜索流行的“教堂编码”和较不受欢迎的“ Scott编码”。）LISP具有非功能性数据，例如原子和数字等，因此这将算作“未经类似的lambda cyculus随机扩展”。

另一个重要区别是 评估顺序. 。减少lambda-calculus术语的规则是高度非确定性的。 （有一个定理，教会定理，它宽松地说，只要事物终止，评估顺序就无关紧要。）实际上，使用最左边的“正常订单”减少，通常会减少lambda术语 任何 减少策略终止了这一点。这与LISP大不相同，LISP始终在减少β-减少Beta之前将参数评估为正常形式。该评估顺序称为“按值调用”。

总而言之，LISP对应于 带有常数扩展的未型，逐个通话的lambda微积分.

Answer 2

约翰·麦卡锡（John McCarthy）引入了LISP 他的1960年4月的论文“符号表达式的递归功能及其计算机计算，第一部分”. 。以下段落来自第6页：

e。功能和形式。在数学逻辑之外，在数学方面通常是不确定地使用“函数”一词，并将其应用于Y之类的表单² + x。因为我们稍后将用表达式计算功能的表达式，所以我们需要在函数和形式之间进行区分，并具有表达这种区别的符号。教会[3]给出了这种描述的区别和一种描述的符号。
...
3. A. Church，《兰巴达转换的微积分》（普林斯顿大学出版社，新泽西州普林斯顿，1941年）。

这 Wikipedia关于Lambda-Calculus的文章 有教会出版物的历史。麦卡锡（McCarthy）引用的1941年论文似乎是关于 打字 Lambda-Calculus，与Wikipedia文章的介绍矛盾。

这 lambda LISP中的关键字只能通过类比来理解为lambda-calculus。 lisp lambda表达是一种 匿名函数.

Answer 3

LISP不是“ lambda conculus”，我不知道什么是“ lambda colculus”。

如果您想通过类型系统识别lambda calculi，那么LISP当然是它的。在计划之前，任何LISP中的“ lambda”关键字肯定是自命不凡的，并且在计划之后，还有房间可以说。仅使用“弹药”会更谦虚。 LISP主要是列表处理器，而不是“ lambda conculus”

我还写了一篇相当广泛的文章，曾经尝试说明为什么a：“功能编程”一词毫无意义，b：为什么说“ lambda colculus”而不是“类型系统”也是如此：

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

另外，请记住，在LISP中，所有功能都是有效的 单个参数 而且只有 列表 作为他们的论点。