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

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的和。
 
 
05-04 04:25