有效的 Lambda 表达式

Question

我有两个关于 lambda 表达式有效性的问题。

首先，变量本身就是有效的 lambda 表达式（例如：λx）

其次，以这两个 lambda 表达式（λx.fxya 和 λz.fxya）为例。除了有界变量不同之外，它们是相同的。这会影响其有效性吗？

另外，如果这些都有效，有没有办法查看一些无效的 lambda 表达式，以便我可以了解有效和无效的表达式是什么样的？

Answer 1

这取决于您所说的有效的含义。让我们从“语法上有效”开始。有效 lambda 表达式的定义是归纳式的。

任何 term 本身就是一个有效的 lambda 表达式。这些是我们语言的原子，出于我们的目的，我们只会说所有小写字母都是有效术语。但实际上，只要您保持一致，您的条款可以是任何您选择的。
如果
```
α
```
和
```
β
```
是两个有效的 lambda 表达式，那么
```
α β
```
也是。我们将此称为 α 到
```
β
```
的
```
应用
```
。
如果
```
t
```
是某个 term （如上所定义）并且
```
α
```
是任何 lambda 表达式，则
```
λt. α
```
是有效的 lambda 表达式。我们将其称为 α 对术语
```
t
```
的
```
抽象
```
。

根据这个定义，

是一个有效的 lambda 表达式，因为它只是一个术语。

λf. f x

也是如此，

a b c d e f

也是如此。

λ x

本身并不是。它看起来像是一个抽象概念的开始，但我们从未完成它，所以它只是一个无意义的字母序列。然而，

本身就是一个表达式，

λx. x

也是一个表达式。

根据这个定义，

λx. f x y a

和

λz. f x y a

都是lambda表达式。具体来说，它们是几个术语应用的抽象。

现在，出于多种目的，我们还希望 lambda 表达式没有自由变量。自由变量是出现在它的任何抽象绑定之外的变量。与自由变量相反的是绑定变量。因此，在

λx. f x y a

中，

是绑定的（通过 lambda 抽象），而

、

和

是自由的。在

λz. f x y a

中，

、

和

都是免费的。拥有未使用的

抽象是完全可以接受的。