Lambda 演算/基本定义
第一个概念是抽象。它类似于定义函数。
- λx.M
这定义了一个函数，它接受一个参数 x 并返回一个项 M。Lambda 演算中的函数没有名称。
第二个概念是调用。它本质上是函数调用。
- M N
这将参数 N 绑定到项 M
- 项
- Lambda 演算中的项是定义的函数。项可能包含变量。
- 变量
- 变量可以代表任何项。项可能包含自由变量或绑定变量
- 绑定变量
- 绑定变量是将绑定到作为参数传递的某个项的变量。例如，在λx.xy中，x 是一个绑定变量。
- 自由变量
- 自由变量是项中任何未绑定到其他项的变量。例如，在λx.xy中，y 是一个自由变量。