神奇的λ-calculus

高山仰止，景行行止。虽不能至，心向往之。

先人遗风

λ-calculus(英文做lambda calculus)于1930s由阿隆佐·邱奇所引入，彼时在数位天才思想家的推动下数理逻辑学科已初见成行，其中关于计算机数理逻辑的尤以戈特弗里德·莱布尼兹、乔治·布尔、格奥尔格·康托尔、大卫·希尔伯特、库尔特·哥德尔、艾伦·图灵、阿隆佐·邱奇等人备受推崇，紧随其后的冯·诺依曼、约翰·麦卡锡、丹尼尔·福瑞德曼等人亦令吾辈顶礼膜拜，他们的成果殷泽后世，歌功颂德、付梓文书都显得微不足道。

潜龙在渊

λ-calculus之所以有着诱人的魅力，在于它的简洁和强大。它可以被称为是最小的通用程序设计语言。它简洁到只包含两条变换规则:变量替换(笔者业余时间参译的魔法书繁体版中1.1.5节有对此的详细解释，贴出链接请看官们不吝斧正: 程序應用的置換模型、变量绑定以及一条函数定义方式。是的，没了。它的强大在于任何一个可计算函数都可以用它的形式来进行表达和求值，所以它是图灵完备的。相比今天各种流行程序语言中具有的以及时不时要新增的时髦语法和概念，基于λ-calculus发明的Lisp之流几乎让人觉得特别落后了(实际并不是这样，《黑客与画家》有对Lisp的高度褒奖，以及SICP使用Scheme，丹尼尔所著的各种Scheme书籍都是对Lisp的高度肯定)(Scheme是Lisp的一种方言)。

牛刀小试

λ-calculus表达式简短的语法规则使用BNF标记如下:

<expr> ::=  <constant>| <variable>| (<expr> <expr>)| (λ <variable>.<expr>)

其中

<constant>可以是诸如0、1这样的数字，或者预定义的函数: +、-、*等。

<variable>是x、y等这样的名字。

(<expr> <expr>)表示函数调用。左边的为要调用的函数，右边的为参数。

(λ <variable>.<expr>)被称为lambda抽象(lambda abstraction)，用以定义新的函数。

β-reduction

一个用来定义新函数的简单的lambda abstraction可以如下表达:

λx.x

它代表着一个调用求值为传入参数的函数(加上括号等价: (λx.x))，这个简陋的lambda abstraction展示了变量替换规则和函数定义方式。对函数的调用标记为(假设传入参数3进行调用):

(λx.x)3

以上调用求值为3。函数调用中参数替换过程又被称为β-reduction。

等价的Scheme代码为:

((lambda (x) x) 3)

等价的Python代码为:

(lambda x: x)(3)

可见Scheme的前缀式(s-表达式)与λ-calculus正有着异曲同工之妙。值得注意的是λ-calculus中的函数总是匿名(anonymously)的。

λx.x中λ为固定标记，标示着这是一个函数(function)，紧随其后的x为这个函数的形式参数(formal parameters)，.之后的x为这个函数的函数体。

α-conversion

比λx.x稍微复杂点的函数定义可以记为:

λx.xy

复杂在哪呢？λx.xy需要引入变量绑定(variable binding)的规则。其中x被称为绑定变量(binding variable)，而y则称为自由变量(free variable)。形式参数x的值将替换到在xy中的x上，而y的值却依λx.xy被调用时的上下文而定，这样的函数和其关联自由变量的引用作用域被称为闭包(closure)。

对λx.xy绑定变量x进行改名后可得到一个新的函数:

λz.zy

这个改写过程被称为α-conversion，因λx.xy与λz.zy是等价的，故这两个函数可被视为α-equivalent。

同理，如下lambda abstraction皆视为α-equivalent:

λx.xy = λw.wy = λt.ty = λz.zy

需要注意的λy.yy与上述lambda abstraction不等价，在α-conversion变换过程中不可将绑定变量与自由变量使用同样的名字标记。

柯里化

事实上在λ-calculus中总是只使用具有一个形式参数的函数，那具有多个形式参数的函数如何在λ-calculus中表达呢？例有如下函数:

λxy.x*x + y*y

可以将其改写为等价的如下函数:

λx.(λy.x*x + y*y)

这个过程被称为柯里化(currying)，与之相反的过程称为反柯里化。

分别对λxy.x*x + y*y和λx.(λy.x*x + y*y)传入x(10)、y(5)进行调用:

(λxy.x*x + y*y)(10,5)
= 10*10 + 5*5
= 125((λx.(λy.x*x + y*y))(10))(5)
= (λy.10*10 + y*y)(5)
= 10*10 + 5*5
= 125

可以发现currying中基本都会使用到closure。

霜刃初开

试着用λ-calculus来描述自然数(0,1,2,3,4,5…..)

设0为zero，suc(zero)表示1，suc(suc(zero))表示2，以此类推。在λ-calculus中通过lambda abstraction来定义zero:

λs.(λz.z)

通过上文的反柯里化可得:

λsz.z

1，即suc(zero)则为:

λsz.s(z)

2，即suc(suc(zero))则为:

λsz.s(s(z))

以此类推…

令suc，即s为:

s = λwyx.y(wyx)

则1，即suc(zero)，为:

1 = λsz.s(z) = s(zero) = (λwyx.y(wyx))(λsz.z)

将w替换为λsz.z:

1 = λsz.s(z) = s(zero) = λyx.y((λsz.z)yx)

将s替换y:

1 = λsz.s(z) = s(zero) = λyx.y((λz.z)x)

将z替换为x:

1 = λsz.s(z) = s(zero) = λyx.y(x)

还记得α-conversion？(λsz.s(z)与λyx.y(x)是α-equivalent的)

同理，则2，即suc(suc(zero))，为:

2 = λsz.s(s(z)) = s(s(zero)) = (λwyx.y(wyx))(λsz.s(z))
2 = λsz.s(s(z)) = s(s(zero)) = λyx.y((λsz.s(z))yx)
2 = λsz.s(s(z)) = s(s(zero)) = λyx.y((λz.y(z))x)
2 = λsz.s(s(z)) = s(s(zero)) = λyx.y(y(x))

以此类推，所冀成焉。

纳履踵决

最近读了马丁·戴维斯所著的《逻辑的引擎》，参译了SICP繁体版，呃……纯粹出于好玩:-)，再次浅薄地研究了一下λ-calculus，深感其美，固有此文。

数理逻辑学如大海般博奥，λ-calculus虽只是其中一支汪洋，却也深不可测。小子自知才疏学浅，文中所记内容虽考证再三，但仍心有余悸，若有所述不当之处恳请行家里手不吝斧正。我的电邮地址:[shawhen2012@hotmail.com](mailto: shawhen2012@hotmail.com)。