我是 Lambda 微积分的新手。 我读过definition of lambda expression on Wikipedia。
Lambda 表达式集 Λ 可以归纳定义：
- 如果x是一个变量，那么x ∈ Λ
- 若x为变量且M ∈ Λ，则(λx.M) ∈ Λ
- 如果 M, N ∈ Λ，则 (M N) ∈ Λ
规则 2 的实例称为抽象，规则 3 的实例称为应用程序。
当M是一个函数抽象，即(λx.E)的形式时，我知道规则2的含义.
但是M不是函数是什么意思呢？比如，只是一个变量x或者一个非函数表达式x + y
【问题讨论】：
x + y 不是 lambda 表达式，所以这不会发生。
所以，当 M 是一个函数时，(M N) 的含义对你来说是很清楚的。 为简单起见，让我们考虑恒等式的情况，即 M = I = \x.x.
(*) (\x.x) N
减少到 N。 假设现在你想让你的程序更通用一点。你 不想只将标识应用于 N，而是应用通用函数 f 您将其作为输入。因此，您将 \x.x 替换为 f 并抽象 整个学期w.r.t.女：
\f.f N
必须理解为\f.(f N)。很简单。
您现在可以将身份作为参数提供给上一个术语，以获得 等同于 (*) 的术语：
(\f.f N) \x.x = \x.x N
为了让事情变得更复杂，您可以想象处理您的输入 函数 f 在将其应用于 N 之前。例如，如果您期望一个二进制 (currified) 函数作为输入，您可能希望将 f 应用于“一对”参数 (N,N)，因为 f 是 currified，因此相当于将 N 作为参数传递了两次：
(**) \f. f N N
理解为\f。 ((f N) N)。因此，您清楚地看到了将应用程序置于其他应用程序的功能位置的意义。
要查看前面的示例，请使用术语 K = \x.\y.x，而不是恒等式。 K 吃了两个论据 广告返回第一个。如果您将 K 作为上一个术语的输入，您仍然会得到一个等效于 (*) 的术语
(\f.f N N) K = K N N = N
一般来说，编程语言是一种提供抽象的方式。 要对一个概念进行抽象，你首先需要一种给予的方式 概念实例的名称。例如，在命令式语言中，变量本质上是对存储单元的抽象。 要对功能进行抽象，您需要使用的可能性 函数的名称。 第二步，让概念“可表达”，即 提供一种允许动态合成的表达式语言 给定概念的新实例（在我们的例子中是新函数）。 lambda 演算只是一个核心演算，其中函数是（直接）可表达的。
【讨论】：
Lambda 演算包含上下文无关文法
E ::= v Variable
| λ v. E Abstraction
| E E Application
其中v 涵盖变量，以及 beta 和 eta 减少规则
(λ x. B) E -> B where every occurrence of x in B in substituted by E
λ x. E x -> E if x doesn't occur free in E
a 在λ b. b a 中免费，但在λ a. λ b. b a 中没有。两个归约规则都不适用的表达式是正规形式。
所以，如果 M N 不是 beta-redex (λ x. B) E，并且 M 和 N 都是范式，那么 M N 整体是不可约范式。
【讨论】：