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