函数式编程λ项的约简

向右看齐 2022-10-17 01:47 119阅读 0赞

在λ项上能够进行不一样的约简（reduction）操做，主要有以下3种。

α变换

α变换（α-conversion）的目的是改变绑定变量的名称，避免名称冲突。好比，咱们能够经过α变换把λx.x+1转换成λy.y+1。若是两个λ项能够经过α变换来进行转换，则这两个λ项是α等价的。这也是咱们上一节中提到的α等价的形式化定义。

对λ抽象进行α变换时，只能替换那些绑定到当前λ抽象上的变量。如λ抽象λx.λx.x能够α变换为λx.λy.y或λy.λx.x，可是不能变换为λy.λx.y，由于二者的语义是不一样的。λx.x表示的是恒等函数。λx.λx.x和λy.λx.x都是表示返回恒等函数的λ抽象，所以它们是α等价的。而λx.y表示的再也不是恒等函数，所以λy.λx.y与λx.λy.y和λy.λx.x都不是α等价的。

β约简

β约简（β-reduction）与函数应用相关。在讨论β约简以前，须要先介绍替换的概念。对于λ项M来讲，M\[x:=N\]表示把λ项M中变量x的自由出现替换成N。具体的替换规则以下所示。A、B和M是λ项，而x和y是变量。A≡B表示两个λ项是相等的。

1、x[x:=M]≡M：直接替换一个变量x的结果是用来进行替换的λ项M。
    
    
    2、y[x:=M]≡y（x≠y）：y是与x不一样的变量，所以替换x并不会影响y，替换结果仍然为y。
    
    
    3、(AB)[x:=M]≡(A[x:=M]B[x:=M])：A和B都是λ项，(AB)是λ项的应用。对λ项的应用进行替换，至关于替换以后再进行应用。
    
    
    4、(λx.A)[x:=M]≡λx.A：这条规则针对λ抽象。若是x是λ抽象的绑定变量，那么不须要对x进行替换，获得的结果与以前的λ抽象相同。这是由于替换只是针对M中x的自由出现，若是x在M中是不自由的，那么替换就不须要进行。
    
    
    5、(λy.A)[x:=M]≡λy.A[x:=M]（x≠y而且y∉FV(M)）：这条规则也是针对λ抽象。λ项A的绑定变量是y，不一样于要替换的x，所以能够在A中进行替换动做。

在进行替换以前，可能须要先使用α变换来改变绑定变量的名称。好比，在进行替换(λx.y)\[y:=x\]时，不能直接把出现的y替换成x。这样就改变了以前的λ抽象的语义。正确的作法是先进行α变换，把λx.y替换成λz.y，再进行替换，获得的结果是λz.x。

替换的基本原则是要求在替换完成以后，原来的自由变量仍然是自由的。若是替换变量可能致使一个变量从自由变成绑定，须要首先进行α变换。在以前的例子中，λx.y中的x是自由变量，而直接替换的结果λx.x把x变成了绑定变量，所以α变换是必须的。在正确的替换结果λz.x中，z仍然是自由的。

β约简用替换来表示函数应用。对((λV.E)E′)进行β约简的结果就是E\[V:=E′\]。如((λx.x+1)y)进行β约简的结果是(x+1)\[x:=y\]，也就是y+1。

η变换

η变换（η-conversion）描述函数的外延性（extensionality）。外延性指的是若是两个函数当且仅当对全部参数的结果相同时，才被认为是相等的。好比一个函数F，当参数为x时，它的返回值是Fx。那么考虑声明为λy.Fy的函数G。函数G对于输入参数x，一样返回结果Fx。F和G可能由不一样的λ项组成，可是只要Fx=Gx对全部的x都成立，那么F和G是相等的。

以F=λx.x和G=λx.(λy.y)x来讲，F是恒等函数，而G则是在输入参数x上应用恒等函数。F和G虽然由不一样的λ项组成，可是它们的行为是同样，本质上都是恒等函数。咱们称之为F和G是η等价的，F是G的η约简，而G是F的η扩展。F和G互为对方的η变换。