$ lambda xy.xy $和$ lambda x。 lambda y.xy $之间有区别吗？

Question

我目前正在学习Lambda演算，并想知道以下两种编写Lambda术语。

1. $ lambda xy.xy $
2. $ lambda x。 lambda y.xy $

您的含义或您降低beta的方式有任何差异，还是只有两种表达同一件事的方法？

特别是对配对创作的定义使我感到奇怪：

一对 = $ lambda xy。 lambda p.pxy $

Answer 1

这些只是符号的差异。 $λxyz.t$缩短了$λx.λy.λz.t$。这里没有魔术。

实际上，$ mbox {pair} =λxyp.pxy$，但您倾向于强调$ mbox {pair} ，t ，u $是函数$λp.ptu$，通过更改编写定义的方式。但这确实是一样的。

Answer 2

第一个是第二个的缩写。这是缩短表达式的常见句法惯例。

另一方面，如果您的语言中有元组，那么

1. $ lambda x。 lambda y.xy $和
2. $ lambda（x，y）.xy $。

在前一种情况下，我可以向该函数提供一个参数，并将结果函数传递给其他功能。在后一种情况下，必须立即提供这两个论点。当然，有一个函数可以应用于将1转换为2，反之亦然。这个过程称为 （联合国）咖喱.

您提到的$ text {pair} $的定义是对$ lambda $ -calculus的对概念的编码，而不是作为原始数据类型对（如上所述）。

Answer 3

将多个参数转换为具有单个参数的函数链的函数称为 咖喱. 。这两个函数本质上是相同的。

维基百科关于咖喱的文章