Lambda演算(二)归约!归约!归约!

(一)
这里先不列出λ项的正式定义,只记住λ表达式语义上的构造方式为:
  1. x
一个单独的变量名是一个λ项表达式;
  1. (λ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)。至于为什么,我们之后再讲。
  1. (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。
 
在这个例子中,不同的归约顺序得出了相同的结果,然而,这并不是普遍现象。这里面暗藏了一个计算机程序中常见的概念:作用域。
 
 
原文地址:https://www.cnblogs.com/liumuqiu/p/8965687.html