Lambda演算
Lambda演算是一个形式系统，它被设计出来用来研究函数定义，函数应用和递归。它是在二十世纪三十年代由Alonzo Church 和 Stephen Cole Kleene发明的。Church在1936年使用lambda演算来证明了判定问题是没有答案的。Lambda演算可以用来清晰的定义什么是一个可计算的函数。两个lambda演算表达式是否相等的问题不能够被一个通用的算法解决，这是第一个问题，它甚至排在停机问题之前。为了证明停机问题是没有答案的，不可判定性能够被证明。Lambda演算对于函数式编程语言（例如lisp）有重大的影响。
同时，数理逻辑中对于lambda演算的介绍就简单得多：
λ-演算可以说是最简单、最小的一个形式系统。它是在二十世纪三十年代由Alonzo Church 和 Stephen Cole Kleene发明的。至今，在欧洲得到了广泛的发展。可以说，欧洲的计算机科学是从λ-演算开始的，而现在仍然是欧洲计算机科学的基础，首先它是函数式程序理论的基础，而后，在λ-演算的基础上，发展起来的π-演算、χ-演算，成为近年来的并发程序的理论工具之一，许多经典的并发程序模型就是以π-演算为框架的。
这里不由得想起一位我尊敬的老师的博士毕业论文就是关于π-演算的，可惜这位老师已经去别的学校了。
Lambda演算表达了两个计算机计算中最基本的概念“代入”和“置换”。“代入”我们一般理解为函数调用，或者是用实参代替函数中的形参；“置换”我们一般理解为变量换名规则。后面会讲到，“代入”就是用lambda演算中的β-归约概念。而“替换”就是lambda演算中的α-变换。
Lambda演算系统的形式化定义
全书上面的对于lambda演算的定义不是很正规，但是说明性的文字较多。而数理逻辑中的定义很严密，不过没有说明不容易理解。我尽可能把所有资料结合起来说明lambda演算系统的定义。
字母表
lambda演算系统中合法的字符如下：
1. x1，x2，x3，…变元（变元的数量是无穷的，不能在有限步骤内穷举，这个很重要，后面有定理是根据这一点证明的）
2. à 归约
3. ＝ 等价
4. λ，（，） （辅助工具符号，一共有三个，λ和左括号右括号）
所有能够在lambda演算系统中出现的合法符号只有以上四种，其他符号都是非法的。例如λx.x+2，如果没有其他对于＋符号的说明，那么这就是一个非法的λ演算表达式。
λ-项
λ-项在一些文章中也称为λ表达式（lambda expression），它是由上面字母表中的合法字符组成的表达式，合法的表达式组成规则如下：
1. 任一个变元是一个项
2. 若M，N是项，则（MN）也是一个项 （function application，函数应用）
3. 若M是一个项，而x是一个变元，则（λx.M）也是一个项 （function abstraction，函数抽象）
4. 仅仅由以上规则归纳定义得到的符号串是项
说明1：λ-项是左结合的，意思就是若f x y都是λ-项，那么f x y＝(f x) y
说明2：(λx.M)这样的λ-项被称为函数抽象，原因是它常常就是一个函数的定义，函数的参数就是变量x，函数体就是M，而函数名称则是匿名的。用一个不恰当的比喻来说，我们通常认为的函数f(x)=x+2，可以被表达为λx.x+2。因为＋是未定义的，所以这个比喻只是为了方便理解而已。
说明3：MN这样的λ-项被称为函数应用，原因是它表达了将M这个函数应用到N这个概念。沿用上面的例子f(x)=x+2，那么f(2)=2+2；同样的λx.x+2表达了f(x)的概念，那么（λx.x+2）2表达了f(2)的概念。其中M＝λx.x+2，N＝2，所以MN＝（λx.x+2）2。
说明4：注意说明3只是为了方便理解，但是还存在很多与直观理解不符合的地方。例如xy也是一个合法的λ-项，它们也是MN形式的，不过x和y都仅仅是一个变量而已，谈不上函数代入。
上面是λ-项的形式化定义，有一些是可以与函数理论直观联系的，而另一些只是说明这
个λ-项是合法的，不一定有直观的字面意义。
公式
若M，N是λ-项，则MàN，M=N是公式。
λ-项中的变量自由出现法则
在一个λ-项中，变量要么是自由出现的，要么是被一个λ符号绑定的。还是以函数的方式来理解变量的自由出现和绑定。例如f(x)=xy这个函数，我们知道x是和函数f相关的，因为它是f的形参，而y则是和f无关的。那么在λx.xy这个λ-项中，x就是被λ绑定的，而y则是自由出现的变量。
直观的理解，被绑定的变量就是作为某个函数形参的变量，而自由变量则是不作为任何函数形参的变量。
Lambda变量绑定规则：
1. 在表达式x中，如果x本身就是一个变量，那么x就是一个单独的自由出现。
2. 在表达式λ x. E中，自由出现就是E中所有的除了x的自由出现。这种情况下在E中所有x的出现都称为被表达式中x前面的那个λ所绑定。
3. 在表达式(MN )中，变量的自由出现就是M和N中所有变量的自由出现。
另一种关于变量的自由出现的规则也许更直接：
1. free(x) = x
2. free(MN) = free(M) È free(N)
3. free(lx • M) = free(M) – {x}
为什么要花大力气来给出变量自由出现的规则，是因为后面的很多地方要用到变量的自由出现的概念。例如α-变换和β-归约。
例子：分析λf.λx.fx中变量的自由出现和绑定状况。
λf.λx.fx =λf.E, E=λx.fx
E=λx.A, A=A1A2, A1=f, A2=x
所以在A中f和x都是自由出现的，
所以E中x是绑定λ x
所以整个公式中f是绑定第一个λ f的。
λ x的控制域
来看两个λ-项，λx.xx和λx.(xx)有何不同？根据左结合的法则，λx.xx＝(λx.x)x，其中第一个x是被λ绑定的，而第二个x则是自由出现的。而λx.(xx)中两个x都是被λ绑定的。这表明了两个λ-项中λx的控制域是不同的。
我们知道谓词演算中量词也是有控制域的，λx的控制域与它们类似，这里就不给出详细的定义了。其实也很直观。
α-变换（α-conversion）
α-变换规则试图解释这样一个概念，λ演算中约束变量的名称是不重要的，例如λx.x和λy.y是相同的函数。因此，将某个函数中的所有约束变量全部换名是可以的。但是，换名需要遵循一些约束。
首先是一个说明：如果M，N是λ-项，x在M中有自由出现，若以N置换M中所有x的自由出现（M中可能含有x的约束出现），我们得到另一个λ-项，记为M[x/N]。
α-变换规则如下：
λx.M=λy.M[x/y] 如果y没有在M中自由出现，并且只要y替换M中的x，都不会被M中的一个λ绑定。
例子：λx.( λx.x)x = λy(λx.x)y
α-变换主要用来表达函数中的变量换名规则，需要注意的是被换名的只能是M（函数体）中变量的自由出现。
β-归约
β-归约表达的是函数应用或者函数代入的概念。前面提到MN是合法的λ-项，那么MN的含义是将M应用到N，通俗的说是将N作为实参代替M中的约束变量，也就是形参。β-归约的规则如下：
(λx.M)N à M[x/N] 如果N中所有变量的自由出现都在M[x/N]中保持自由出现
β-归约是λ演算中最重要的概念和规则，它是函数代入这个概念的形式化表示。
一些例子如下：
(lx.ly.y x)(lz.u) ® ly.y(lz.u)
(lx. x x)(lz.u) ® (lz.u) (lz.u)
(ly.y a)((lx. x)(lz.(lu.u) z)) ® (ly.y a)(lz.(lu.u) z)
(ly.y a)((lx. x)(lz.(lu.u) z)) ® (ly.y a)((lx. x)(lz. z))
(ly.y a)((lx. x)(lz.(lu.u) z)) ® ((lx. x)(lz.(lu.u) z)) a
需要多加练习才能习惯这种归约。
η-变换（η-conversion）
η-变换表达了“外延性”（extensionality）的概念，在这种上下文中，两个函数被认为是相等的“当且仅当”对于所有的参数，它们都给出同样的结果。我理解为，对于所有的实参，通过β-归约都能得到同样的λ-项，或者使用α-变换进行换名后得到同样的λ-项。
例如λx.fx与f相等，如果x没有在f中自由出现。
λ演算的公理和规则组成
这一段来自《数理逻辑与集合论》（第二版 清华大学出版社）。还修正了其中的一个错误。
1. (λx.M)N à M[x/N] 如果N中所有变量的自由出现都在M[x/N]中保持自由出现
2. MàM
3. MàN, NàL => MàL （原书中此处错误）
4. MàM’=>ZMàZM’
5. MàM’=>MZàM’Z
6. MàM’=>λx. M àλx. M’
7. MàM’=>M=M’
8. M=M’=>M’=M
9. M=N,N=L=>M=L
10. M=M’ => ZM = ZM’
11. M=M’ => MZ = M’Z
lambda编程12. M=M’ =>λx. M =λx. M’
如果某一公式MàN或者M=N可以用以上的公理推出，则记为λ├MàN和λ├M＝N。
范式
如果一个λ-项M中不含有任何形为((λx.N1)N2)的子项，则称M是一个范式，简记为n.f.。如果一个λ-项M通过有穷步β-归约后，得到一个范式，则称M有n.f.，没有n.f.的λ-项称为n.n.f.。
版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。
发表评论