Lambda演算归约！归约！归约！

Posted 2020-11-01 落叶维扬

（一）

这里先不列出λ项的正式定义，只记住λ表达式语义上的构造方式为：

1. x

一个单独的变量名是一个λ项表达式；

2. (λx.M)

该λ表示一个函数。其中 M 是这个函数的函数体，M 本身也是一个 λ项。

除了 x 之外，M 中可能还有其他变量名，λ 这个符号用于指示函数体 M 的参数为 x。

了便于理解，可以将 M 看作函数体，x 看作形参，即变量名。

 

例如：λx.x+3 即表示一个函数 f(x) = x+3，该函数会返回x与3相加的结果

要注意的是，我这里的写法并不规范，在λ表达式中，二元运算符是作为前缀的。x+3 应该写作 (+ x 3)。所以这个表达式的正规写法是 λx.(+ x 3)。至于为什么，我们之后再讲。

3. (M N)

其中 M，N 均为λ项表达式。

如果 M 本身是一个函数，我们说将函数 M 应用于 N。如果 M 不是函数，不接受参数，N 将在求值的过程中被忽略。

例如：（λx.(+ x 3) 4），其中M为表达式 λx.x+3，N 为 4。这个表达式表示将函数应用于 4，即f(4) 

 

所以一个典型的λ表达式具有如下形式：

 (λx.M) N，为了方便去掉括号写作 λx.M N

 

其中 M 是函数体，x 可以看作形参，即变量名， N 可以看作实参，即变量值。

 

函数本身也可以作为参数，例如（λx.x）（λx.(+x 3)),  表达式左边就是一个函数，这个函数将返回它自己的参数，将这个函数应用于我们之前说的函数 f，参数是 f，那么这个函数将返回 f。

 

如此一来，第一种形式的λ表达式代表一个变量；

第二种表达式代表一个函数；

第三种表达式则代表将函数应用于一个值，即一次函数调用。

 

（二）归约

第一种表达式的值即它本身；

第二种表达式的值表示这个函数本身；

因此，在讨论求值时，我们只关心第三种，即将一个函数应用于另一个λ表达式时，如何计算它的值。

 

如上所述，λ表达式的应用等效于一次函数调用。我们知道，调用函数的时候，会将所有的形参替换用实参的值，并返回计算结果。因此，我们说在表达式 λx.M N 中，函数体 M 里的 x 与表达式 N 绑定，M 中剩下未绑定的变量则是自由变量。

 

对 λx.M N 进行求值时，M 中所有的 x 都将被替换为 N。这一过程称为归约，归约后得到简化的λ表达式，可以进一步归约直至无法再归约，此时的表达式就是对原表达式进行求值的结果。

 

考虑一个函数 f(x)=x+3，写作λ表达式就是 (λx.(+x 3))。

如前所述，当我们想计算 f(4) 时，将函数应用于 4，表达式为 λx.(+ x 3) 4。

按照归约的法则，函数体 (+ x 3) 中的 x 被 4 替换，函数表达式变为 (+ 4 3)，结果为 7。

 

考虑另一个函数 g(y)=y*2，λ表达式 λy.(* y 2)。

如果我们想将函数 g 应用于 f(4) 的计算结果，即 g(f(4))，我们可以将 g 的λ表达式应用于上述表达式，即 λy.(* y 2)  (λx.(+ x 3) 4)

 

然后我们进行归约，这里有两种归约顺序。

 

一种是同之前一样，先计算右边表达式的值，即归约为 λy.(* y 2) 7。

然后将函数体 (* y 2) 中的 y 替换为 7，得到 (* 7 2)。

最终结果是 14。

 

另一种归约顺序是先计算最外层的应用，即将y替换为右边的表达式(λx.(+ x 3) 4)，得到归约后的表达式(* (λx.(+ x 3) 4) 2)。

再归约内层的应用，替换 x 得到 (* (+ 4 3) 2)。

最终结果为(* 7 2)=14。

 

在这个例子中，不同的归约顺序得出了相同的结果，然而，这并不是普遍现象。这里面暗藏了一个计算机程序中常见的概念：作用域。