Lambda演算（一）大道至简

从选择信息专业开始到回炉读书为止，四舍五入码了八年代码。对于计算机科学的认知仅限于：

1）使用不一样语言实现特定功能

2）实现不一样算法以增进系统性能

3）搭建不一样架构进行组织管理

 

但从未思考一些本质问题，好比程序中的函数是什么？系统中的进程是什么？类是什么？这些经常使用概念，都会使用，也会用描述加以解释，但没有想过须要进行形式化的定义。所以，其实历来没有进过计算机科学的大门。

 

上两个学期修习了Principles of Programming Language, Logic两门课程，加之浏览了一些verification，type theory 和其余演算的内容，方觉任督二脉始通。要想练得精纯内功，输出难度和效率显然远高过输入。但愿在博客总结完成事后，能有透彻的理解。

 

开篇

一切计算机运算过程，均可以归约于最简单的模型，好比图灵机，好比Lambda演算。

 

Lambda演算, 出自Alonzo Church三十年代的书The Calculi of Lambda-Conversion。Alonzo设计Lambda演算的初衷，是为了以一种通用的形式化方式来表示复杂的计算过程。

 

假设有一群原始人，他们的数学系统里用+号来表示两数相加，却没有×号，那么他们想要表达乘这种运算的时候，只能用..+..+..这种表达式，或者用描述式的“十个加”，一旦他们引入了×号，就至关于有了一种形式化的方法来表达乘运算。

 

尽管现代数学系统里，除了加号和乘号以外，幂、积分、累加等等运算符号不停地被发明出来，可是想用它们组成表达式来表示一段计算机程序的运算过程，仍是显得无比繁琐。

 

Lambda演算使用了一套极其简单的符号系统：{λ, ., (, )}以及变量名，就能表示一切图灵可计算的问题的计算过程，所以，它是一种通用的形式化演算。

 

Alonzo证实了Lambda演算没法解决可断定性问题（Entscheidungsproblem） ，它所能实现的计算复杂度是与图灵机相等的。换句话说，Lambda演算和与图灵机等价。所以，它是图灵完备的。

 

下面开始理解Lambda演算： 

 

（一） 函数

数学中的函数，能够看做一种映射。计算机科学中的函数一样是一组映射规则，这种规则会将给定的值（参数）映射到结果（返回值）上。在计算机中，这个规则具体表现为一段操做。这段操做被应用于参数的过程称做归约，归约以后，原有的参数+操做表达式被简化成一个返回值。

 

这个函数（规则、操做、anything）能够表示为 f a。表达式左边f为函数名，右边a为形参名。

 

如同数学函数有定义域和值域，一个计算机函数所能做用的参数，也有必定范围。对于超出范围的a，f a是无心义的。

 

（二）多个参数

当一个函数有两个参数a，b时，写做 f a b，状况变得复杂了一些。令一个函数 g = f a，咱们能够发现，对于任意定义域内的g，均可以得出g b = f a b。所以，f a b 等价于（f a）b。左边括号里的整个表达式为一个函数（f a），右边为变量名b。

 

所以，对于有两个参数的函数，其归约过程等效于将函数f应用于第一个参数a，返回一个简化后的函数g，再将g应用于第二个参数b，返回计算结果。

 

更进一步，三个参数的函数f a b c 可拆解为单个参数（f a b）c，或两个参数（f a）b c。不管哪一种拆解方式，最终都归为((f a) b) c。

 

将该结论拓展至通常状况，任意多个参数的函数，最终均可以拆解为单个参数的函数组合。

 

（三）Lambda符号

假设咱们有一个函数f=x+1，在形式化的表达式中，将用具体的表达式x+1来替换f。假设这个函数是f=x，则以前的 f x, 写做 x x。咱们并没有法区分是在讨论变量x，仍是谈论一个将参数映射到它本身的函数 x。所以，Alonzo引入符号Lambda （λ）来区分这两种状况。

x 单纯表示一个变量x，λx.x表示一个函数，点号左边的x指定这个函数的形参是x，右边表示这个函数的表达式，表达式中的全部x都是形参，在将来的归约中，都会被实参替换。

 

举例来讲，λx.(x^2-1)，x是参数，x^2-1是函数表达式，表示这个函数返回参数值的平方减一。

 

根据（二）中有关多个参数的讨论，λx.λy.（x+y），则等效于λx.（λy.（x+y）），其中λy.（x+y）表示一个函数，这个函数返回参数与x的和，x在此处是一个值不定的量（变量），或者说还没有绑定值的名字，加上λx.部分后，λy.（x+y）中的x就成了另外一个形参，而这个函数返回的是参数x与参数y的和。