神奇的λ演算

短命女 2022-06-16 06:50 172阅读 0赞

现在时兴讲函数式编程，弄得如果不会写两句λ表达式你都不好意思跟人说自己是敲代码的。所以我也就趁着这阵风头，琢磨琢磨了这个函数式编程。怎么算来，也有个三年两载了，出师还不敢说，将将入门估计还算凑合。朋友说让给写篇文章或者翻译翻译哪个大佬的文章，盛情难却，就把刚学的这点水倒出来出出糗好了。

说函数式编程这个东西，根源来自于λ演算，虽然后面加了很多特性，但总归要从这里出发。关于λ演算这个东西，也是很有历史的，有兴趣了解相关历史的，可以参阅相关的wikipedia，这里就不多说了。咱们直奔主题。

### 引子 ###

说到 λ 演算，自然要从 λ 表达式说起。到底什么是 λ 表达式呢？其实很简单，就是一种特殊的语法所书写的匿名函数。

所谓匿名函数，就是说我们不需要给这个函数起个什么名字。这一点很重要，如果按照非匿名函数的观点，但凡是函数都需要有个名字，那么就很难和“函数是第一类对象”这样的观点兼容。毕竟，动态生成的无穷多种可能性的函数，我们总不能预先都给他们准备好名字是吧。更何况，就算有这个心思，也没这个可能，光一阶的函数的数量就已经高于整个实数的数量了，比实数少的自然数我们都列不完呢（虽说叫可列集，不过谁都没列完过），更何况是它了。

我们来看看一般目前的语言怎么去写匿名函数。其实这里有点倒因为果，毕竟是先有了λ演算，才有了现代语言中的这些匿名函数。不过便于理解起见，也就不管那么多了。先来看看JavaScript、Matlab和C\#几种语言的具体实现方式

// javascript var f = function (x) { return x+1; }

% Matlab
        f = (x) x + 1;

// C#
        Function<int, int> f = x => x + 1;

看，写起来都还算简单，不过数学家们有更偷懒的办法，他们把上面的函数用更加简化的方式来表示，只用一个关键字 'λ' 来表示对函数的抽象。还是上面这个函数，用不太规范的方式来表示下 λ 演算中对上述函数表达方式，大体上是这样

λ x. x+1

所谓的不规范的地方，主要就是这个加法运算，具体怎么不规范了，请看下节。

### 基本概念 ###

学界有个公认的观点，叫做“奥卡姆剃刀”原则，说如果有多种理论去解释相同的现象，假设最少的那个往往是最受欢迎的。

学程序设计的同好们都知道，学一门编程语言，我们总是要去了解这门语言中诸如数据类型、变量、常量、运算符、表达式这些原生定义的东西。这种东西就相当于上帝之手，设定了最基本的规则和假定，然后我们在它画的这个圈圈里面玩。

哲学上一个常识，内涵越小外延越大。我们搞了那么多的假定，往往就给自己做了很大的束缚。数学家不喜欢这么玩，所以构建这个λ演算的时候，更倾向于用尽可能少的原生性规则来进行限定。

于是，他们规定了一下最基本，最核心的三个基本假定，我们不妨理解为最基本的语法规则。

*  第一个就是所谓函数为第一类对象的原则，用文字陈述有点绕口，这么说的：“ 全体λ表达式构成Λ空间，λ表达式为Λ空间到Λ空间的函数 ”。  
    我曾经尝试过用C\#来表达这句话，居然通过编译了，贡献出来
    
        // C#
          delegate L L(L x);
    
    这说的是，定义了一个委托类型L，这种委托类型以一个类型为L的参数作为输入，返回一个L类型的返回值。所有L类型的实例，就构成了上述的Λ空间。
 *  第二个是函数的抽象原则，即对于一个λ表达式，不妨称为P，我们可以用一个字母代表哑元，不妨称为 x，使用抽象规则，我们可以构造出另一个λ表达式来，像这样
    
        λ x. P
    
    它表示我们构造了一个函数，这个函数以一个λ表达式输入，返回另一个λ表达式，这个返回值等于将P中所有非哑元的字母 x 用刚刚输入的那个表达式替换掉。  
    例如我们有几个表达式，P分别为
    
        x y z
          y (λ x. x)
    
    如果应用上述抽象规则，并用 x 标记新抽象的哑元，可以得到
    
        λ x. x y z
          λ x. y (λ x. x)
    
    如果应用某个不等于也不包含 x, y, z 字母的表达式 a 作为输入的话，上述两个λ表达式计算的结果应当分别为
    
        a y z
          y (λ x. x)
    
    为什么第二个里面的 x 仍然保留呢，就因为它是在 P 中的哑元，其实和P外的哑元是没关系的。可以用一个避免混淆的方式给它改改名字，比如说改成
    
        λ x. y (λ w.w)
    
    其实表达的是同一个意思，就好像这两个代码其实表达的运算是一个意思一样
    
        // javascript var f = function (x) { return x + 1; }; var g = function (y) { return y + 1; };
    
    哑元的更换，不影响 λ 表达式的所表达的含义。
 *  第三个规则比较直观，就是应用函数的规则，对于一个 λ 表达式 P 如果希望将另一个 λ 表达式 q 作为它的输入进行求值，我们简单的将他们左右并列书写即可
    
        P q
    
    这里不使用括号写法P(q)，因为我们后面可以看到，如果用上括号，我们会后悔的。注意到一个 λ 表达式应用一个 λ 表达式作为输入后，返回的还是一个 λ 表达式，它即可以作为函数再接受一个新的输入，比如说 r，就可以写成这样
    
        P q r
    
    这里就默认了左结合优先的自然的规则。它也可以作为输入，传递到另一个 λ 表达式中，比如说 S，就可以写成这样
    
        S (P q)
    
    因为前面提到了左结合优先的原则，所以这里这个括号就不可避免了。

这三个规则，就构成了λ演算的全部基石，有的作者用更加形式化的方式将他们整理起来，有的还甚至提炼出更加具体的一些法则，其实我觉得，从本质上讲，这三者其实是核心，外围的那些规则都是一些自然的辅助性衍生。如果希望看比较规范严谨的定义的，我推荐H. Simmons和A. Schalk写的[这本书][Link 1]，他们写的非常严谨，相当的棒。如果希望看稍微通俗一点，又不像我这样太通俗的，建议看看R. Rojas写的[这本][Link 2]，只有13页。如果还嫌长，看A. Jung的这篇10页的[小文][Link 3]也好。其实我都是从wikipedia上转摘来的，这几篇我看过觉得不错，更完整的书单还是建议去Lambda Calculus的页面看，毕竟萝卜青菜各有所爱嘛。

### Bool运算 ###

如果前面那些算看起来比较枯燥，让人看了有然并卵的感觉的话，那现在我们就算正式踏上了 λ 演算的神奇之旅了。我们先来看看最简单的情况，用上述定义的基本规则，我们来构造Bool运算。

首先是True和False，简写作 T 和 F，我们采用Church的方案（此大咖就是这整个神奇 的 λ 演算的发明人，我没看他的原文，就不厚着脸皮转引他的文章了）

T = λ x y. x
        F = λ x y. y

这里，使用了著名的柯里化技巧（Currying），用一元函数构造多元函数，展开来写 T 的定义应当是

T = λ x. (λ y. x)

表示的含义是 T 是这样一个函数，它接收任何一个输入 x，并会返回一个函数 λ y. x，这个被返回的函数接收另外一个输入 y，而不论这个输入 y 是什么，它返回第一个输入的参数 x .

同样，F 是这样一个函数，它的展开式写作

F = λ x. (λ y. y)

它接收 x 并返回 λ y. y，而后者接收什么就原模原样的返回什么。

这里 T 和 F 接受第一个参数后所返回的两个函数也很重要，可以分别称为常函数 λ y. x 和恒等函数 I = λ y. y。其实更常见的恒等函数写作 λ x. x，上一节我们提到过，变换哑元不改变函数含义。

站在柯里化技巧的基础上，我们可以重新将 T 理解为一个选择函数，它接收两个参数，而返回第一个参数。而 F 则相反，它返回第二个参数。

T a b = (λ x. (λ y. x)) a b = (λ y. a) b = a
        F a b = (λ x. (λ y. y)) a b = (λ y. y) b = b

在不影响理解的情况下，将重复书写的λ和不必要的括号都省略掉，就可以简略的书写柯里化技巧下的多元函数

T = λ x. (λ y. x) = λ x. λ y. x = λ x y. x
        F = λ x. (λ y. y) = λ x. λ y. y = λ x y. y

就是这一节我们前面所提到的 T 和 F 的定义。

从这里我们也可以看到， λ 演算的根本原则认为，函数是第一类对象，对于Bool量，我们确实用某种函数的方式定义了它们。但是，脱离于具体运算性质的Bool量并不能称之为真正的Bool量。所以我们还需要用λ表达式定义Bool运算，并且所定义的这些运算算子能够如同Bool代数中所设定的Bool运算算子的那些性质。（都是老理论了，看看wikipedia也没啥丢人的，想了解完整的Bool代数定义的同学看wikipedia对应页面即可。）

基本的Bool运算算子有三个，与 And，或 Or，非 Not。我们先来构造 And 算子。

And 算子是一个二元函数，它接收两个输入Bool量作为输入参数，只有两个参数同时为 T 时，返回值才是 T。所以基本的形式应当是这样的

And = λ x y. ?

关键是我们如何构造这个 ? 的表达形式。

如果关注过C语言等指令式语言的运算符&&的朋友应当知道，&&运算符其实并不是同时检查两边的参数的，它会先检查左侧参数，仅当左侧为 T 的时候才检查右侧参数，并将右侧参数的真假作为返回值返回，否则将直接返回 F。所以我们可以写这样的语句，用来避免Null Pointer这类错误

// Java
        if (obj != null && obj.success) {
          // TODO: ...
        }

这就可以启发我们把 And = λ x y. ? 运算设计为这样的机制：

*  若 x 为 F，则返回 F；
 *  若 x 为 T , 则返回 y 。

不过，等等，我们好像没有定义过条件选择指令阿，那该如何实现上面的这个设想呢? 还记得我们前面讨论 T 和 F 是两个选择函数吧，如果

x a b

这个表达式中 x 位置上放 T 就会选出 a，而放 F 就会选出 b 来。这不就是我们要的条件选择表达式吗？

所以让 ? 号部分构造成这样，就可以得到我们要的结果

? = x y F

来看看设想是否满足

*  当 x = F 时， ？ = F y F 选出 F，即返回的是 F；
 *  当 x = T 时， ？ = T y F 选出 y，即最终返回值根据 y 的真假而定。

正是我们所设想的那样，而且仅当 x 和 y 同时为 T 时才返回 T，其它情况都返回 F 。

所以 And 算子的正式定义可以为

And = λ x y. x y F

利用相同的思路，可以构造 Or 和 Not 算子

Or = λ x y. x T y
        Not = λ x. x F T

有兴趣的读者可以自行按照Bool逻辑来验证一下，进一步还可以尝试一下借助 And，Or，Not或者不借助它们直接用 T 和 F 来构造异或 Xor，同或 Nor算子，甚至构造蕴含算子从而走上数理逻辑和机器证明的[康庄大道][Link 4]。

### 自然数-加法与乘法 ###

现在继续我们的神奇之旅，我们来构造自然数，以及自然数之上的加法、乘法运算。

要构造自然数，首先需要明确到底什么是自然数，这一点要非常感谢皮亚诺大咖，早早的就把自然数的形式化定义（[皮亚诺公理][Link 5]）准备好了，深入一些的分析可以证明，下面我们所介绍的Church方案（对还是此大咖的神作），满足皮亚诺公理。

首先，给出自然数的 λ 表达式的定义

0 = λ f x. x
        1 = λ f x. f x
        2 = λ f x. f (f x)
        3 = λ f x. f (f (f x))
        ...
        N = λ f x. f^n x

可以发现，这里定义的自然数 0 和我们前面提到的 False 是同一个 λ 表达式。做编程的同学肯定感到很自然，我们在计算机上确实就是用 0 表示 False 的。

上面的定义的时候我们采取了一个简化写法，用 f^n 表示 f 函数连续迭代 n 次

f^n * = f (f (... (f *) ...))    # 这里 f 出现 n 次

为了避免混淆起见，我们指代非 λ 表达式的自然数 n 时采用小写字母，而指代 λ 表达式的自然数 N 时采用大写字母。

然后我们需要一个后继算子 inc，按照皮亚诺公理的要求每一个自然数存在一个后继自然数

inc N = N+1

这里用到 N+1 其实也并不严谨，毕竟我们没有定义加法呢，如此写仅仅是为了表示 inc 0 = 1，inc 1 = 2，并依次递推。

观察到自然数 N 现在其实是个函数，如果让它作用到某两个 λ 表达式 a 和 b 上，产生的效果是按照将 a 连续迭代的作用到 b 上n次

N a b = (λ f x. f^n x) a b = a^n b = a (a (... (a b) ...))    # 最右边一共出现 n 次 a

比如说可以试试 0，1，2

0 a b = (λ f x. x) a b = b
        1 a b = (λ f x. f x) a b = a b
        2 a b = (λ f x. f (f x)) a b = a (a b)

那么 inc N 所产生的这个 N 的后继，它作用到 a b 上应当比 N 多一次迭代映射即可，像这样

# inc N 展开式
        inc N a b = a (N a b)

所以将前面的 inc N 展开式两边用抽象法则连续抽象三次，就有

λ N a b. inc N a b = λ N a b. a (N a b)

而左边应用恒等式

P = λ x. P x

就可知

inc = λ N f x. f (N f x)

这就是Church方案下的后继算子。这里所用到的这个恒等式，这个可以自行证明，用的是广延意义下的等于概念： 若对于所有 x 都有 P x = Q x，则 P = Q 。

有了后继算子，就很方便构造加法和乘法算子。借助于后继算子来定义加法算子，然后再用加法算子来定义惩罚算子，就像我们在小学时第一次学习加法和乘法那样。不过直接借助于 N 的迭代展开作用来定义也未尝不可。前者可以留给读者当作脑筋健身操来玩玩，这里给出后者方案的定义来，读者可以自行验证一下

Add = λ N M f x. N f (M f x)
        Mult = λ N M f x. N (M f) x

### 自然数-前趋和减法 ###

为了定义减法我们首先需要定义一个前趋算子，前面其实都还算比较平铺自然，定义前趋算子的时候，需要稍微绕一点点弯，我们选择比较直白的一种绕法。

首先，定义一个数对算子 Pair，它的作用是将两个数 M 和 N 做成一组来用，定义如下

Pair = λ M N x. x M N
        [a, b] = Pair a b            # 数对的简写形式

可以用 T 和 F 算子来取出数对中的左支和右支

[a, b] T = Pair a b T = T a b = a
        [a, b] F = Pair a b F = F a b = b

稍微需要注意一点的是，这里的 T 和 F 算子是从右边作用过来的。  
（对头！你看见二叉树了！好眼力！！！）

注意到数对也是一个 λ 表达式

[a, b] = Pair a b = λ x. x a b

于是我们可以为它定义一个迭代算子 Phi，它负责将数对 \[N, M\] 迭代到 \[N+1, N\]

Phi = λ p. [inc (p T), p F]

比如说

Phi [0, 0] = [inc 0 , 0] = [1, 0]
        Phi [4, 3] = [inc 4, 4] = [5, 4]

这样我们就可以依据它来定义自然数的前趋算子 dec

dec = λ N. N Phi [0, 0] F

它的意思是把 Phi 连续 N 次作用到对数 \[0, 0\] 上，最后取出右支。我们来试一下，比如用 3 来输入

dec 3 = 3 Phi [0, 0] F = 2 Phi [1, 0] F  = Phi [2, 1] F = [3, 2] F = 2

很显然，这里就是利用了关系式（不太严谨地表示形式）

N Phi [0, 0] = [N, N-1]

特别的，对于自然数 0，依照皮亚诺公理，它没有前趋，而这里则用稍微变通一点的方式，设定了 0 的前趋就是 0 本身。（注意到我们目前仅仅是在讨论自然数，而不是整数）

dec 0 = 0 Phi [0, 0] F = [0, 0] F = 0

依照减法的原初定义，定义减法算子为

sub = λ N M. M dec N

即连续让 N 递减 M 次，注意到我们是在自然数范围内讨论，所以如果 M 比 N 大的话，最后结果不是负数而是 0 。

### 自然数-关系运算 ###

下面再来看一个逻辑判断算子，IsZero，当输入 0 时，它返回 T，输入其它自然数时返回 F，可以如此定义

IsZero = λ N. N F Not F

这里要用到我们把 F 当作成两个一元函数依次嵌套的理解来考虑

F x = λ x. x = I

并且，Not 算子也是个 λ 表达式，它是可以作为输入传递给别的 λ 表达式的，因此

IsZero 0 = 0 F Not F = Not F = T
        IsZero 2 = 2 F Not F = 1 F I F = F I F = I F = F

对于所有的大于 0 的自然数，N F Not 连续迭代之后必然返回 I，而 0 F Not 则返回 Not。

有了前面的准备，我们就可以定义小于等于算子Leq，大于算子Gt，大于等于算子Geq，小于算子Lq，等于算子 Eq和不等算子Neq了。这里给出前两者定义，后四者可以作为小游戏读者自行尝试构造一下。

Leq = λ N M. IsZero (sub N M)
        Gt = λ N M. Not (Leq N M)

### 不动点 ###

在数学上，我们经常会遇到不动点的概念。所谓不动点，即对某个函数 f(x) 存在这样的一个输入 x，使得函数的输出仍旧等于输入的 x 。形式化的表示即为

f(x) = x

比如说刚刚学过循环小数的小朋友们就很喜欢纠结这个问题

0.999... = 1

实际上这个可以用不动点的方式去理解，我们可以设 x = 0.999...，观察到 x 扩大到原来的10倍的时候再减去9，得到的仍旧是 x 本身，因此 x 是函数

f(x) = 10x - 9

的不动点，满足方程

x = f(x) = 10x - 9

简单的求解一下方程，就可以得到 x = 1的结论。

在前面的讨论中，我们曾接触过恒等算子 I = λ x. x ，对它而言任何一个 λ 表达式都是它的不动点。而对于一般性的 λ 表达式，寻找它对应的不动点，在后面的讨论中我们可以看到，是一个非常有意义的事情。

对于一般性的数学函数而言，不动点的存在性并不是一定的，比如说指数函数 ex，它就不存在不动点。而对于存在不动点的函数，寻找其不动点往往也是需要一定技巧的。但是那仅仅是对于一般意义的数学函数而言，在 λ 演算体系下，Λ空间中的每一个 λ 表达式都具有一个不动点。这来源于下面将要介绍的著名的不动点定理。

在介绍不动点定理之前，我们先来看一个比较有趣的 λ 表达式

ω = λ x. x x

它表示接受一个输入 x，返回 x 作用到 x 自身的结果。比如说

ω a = a a
        ω I = I I = I

现在要耍点赖皮了，我们让 ω 自己作用到自己身上，并按照应用函数的法则将其展开

ω ω = (λ x. x x) ω = ω ω

展开后竟然又还原回来了，这似乎和我们所说的不动点的重现机制很近似。

而事实上，几个比较著名的不动点算子的构造过程都借助了这种技巧。下面我们来看最著名的不动点算子 Y 组合子

Y = λ f. (λ x. f (x x)) (λ x. f (x x))

这里应用了两次自身作用自身的技巧，第一个是显式出现的 x x，而后者是整体上出现的

a = λ x. f (x x)
        Y = λ f. a a

给出了 Y 组合子，不动点定理其实就已经通过构造法得到了证明。不动点定理如此说：对于任意 λ 表达式 g，总存在不动点 x = Y g，使关系 g x = x 成立。简写作

g (Y g) = Y g

证明过程很简单

Y g = (λ f. (λ x. f (x x)) (λ x. f (x x))) g
            = (λ x. g (x x)) (λ x. g (x x))            # (a)
            = g ( (λ x. g (x x)) (λ x. g (x x)) )      # (b)
            = g Y g                                    # 将 (b) 中 (a) 重现的部分重新写作 Y g

除了 Y 组合子之外，其它比较著名的不动点算子还有

X = λ f. (λ x. x x) (λ x. f (x x))
        Θ = (λ x y. y (x x y)) (λ x y. y (x x y))

读者可以自行验证一下。更多的不动点组合子，还请参阅[相关wikipedia页面][wikipedia]。

### 递归函数 ###

有了不动点组合子，我们就能够构造可计算理论里面最关键的递归函数了。

递归是一种函数构造或者说编程技巧，使用这种技巧，我们能够极大程度的简化语言陈述方式，甚至可以将无法描述的无穷的概念通过有穷的语言描述出来。

比如说自然数集 N，我们用递归的方式描述它，可以这样说：令 N(n) 为从 n 开始，元素依次递增的集合

N(n) = { n } ∪ N(n+1)

则 N(0) 即自然数集 N。这里，定义 N(\*) 集合的过程中，用到了 N(\*) 自身的定义。

递归的过程并不能简单理解成循环论证的过程，我们可以将递归定义理解成为一种性质，只要某个事物满足我们所给出的这种递归形式的性质，我们即认为该事物满足我们的定义。使用这种方法，我们可以规避无穷无尽的溯源的困境，没必要讲清楚一个事物到底是什么，只需要讲清楚一个事物是什么样的即可。这样的一套思想，在数学上称之为 性质即定义 。

注意到每个自然数都具有一个后继，而且每个不同的自然数的后继都不相同，上述自然数集的描述方法，如果进行展开，我们将会永不休止的展开下去

N = N(0) = {
       0} ∪ N(1) = {
       0, 1} ∪ N(2) = ... = {
       0, 1, ..., n} ∪ N(n+1) = ...

对于即时求值策略的编程语言来说，这样一个过程，将会在定义 N 的时候造成死循环。当然，在数学上，我们不必机械的重复这样的死循环过程，正如我们上面用省略号的方式，用“依次类推”的方式结束这样的扩展过程。而对于[惰性求值策略][Link 6]的编程语言来说，这样一个问题是可以避免的，这里不再过多展开。

在 λ 演算中定义递归函数，构造的思路在很大程度上依赖了不动点算子的性质，实际上考虑不动点问题

x = f x

如果将其理解为定义式，左侧为定义的目标，而右侧为定义的内容，这个表述形式本身为一种递归形式的定义。

而通过上节我们可以知道，任何一个 λ 表达式 f 的不动点是很容易求得的，为 Y f，满足

Y f = f (Y f)

借助这样的一个从左到右展开的过程，我们就可以很方便的定义递归形式的函数，比如说我们定义前面提到的自然数集合，借助 Pair 算子来表达并集的含义，可以先定义一个辅助函数

g = λ f N. [N, f (inc N)]

而返回全体自然数集合的函数的则为

NaturalNumbers = Y g 0

我们来看一下它的逻辑过程（当然，我们没必要真的这样无穷展开下去，在实际中）

Y g 0 = g (Y g) 0              # 应用 Y g = g (Y g)
              = [0, Y g 1]
              = [0, g (Y g) 1]         # 再次应用 Y g = g (Y g)
              = [0, [1, Y g 2]]
              = [0, [1, [2, Y g 3]]]
              = ...

而对于指令式程序员理解习惯的递归函数，比如说 Sum(n) 这样的函数，也可以用相同的方式来进行定义

g = λ f N. IsZero N 0 (add n (f (dec N)))
        Sum = Y g

例如求 Sum(3)

Sum 3 = Y g 3
              = g (Y g) 3
              = g Sum 3
              = add 3 (Sum 2)
              = add 3 (g Sum 2)
              = add 3 (add 2 (Sum 1))
              = ...
              = add 3 (add 2 (add 1 0))
              = add 3 (add 2 1)
              = add 3 3
              = 6

具备了递归函数的构造能力，依据[可计算性理论][Link 7]，λ 演算体系便构成了图灵完备系统。所谓图灵完备系统，概括而论即任何可计算的函数，均可由此系统来构造。这个结论表明，λ 演算体系能够做到当前通用计算机所能够做到的一切。

### 结语 ###

至此，这篇不算怎么简短，但大体还算通俗的 λ 演算的介绍就终于告一段落了。

λ 演算神奇之处在于，通过最基本的函数抽象和函数应用法则，配套以适当的技巧，便能够构造出任意复杂的可计算函数。当然，如果要界定什么叫可计算函数，这就不是这篇通俗读物的设定范围了，较为全面而又概括性的巨额介绍还请读者自行参阅前述可计算性理论的页面。

当然，这短短几千字小文并没有囊括所有 λ 演算的研究成果，我也仅仅带领读者是管中窥豹而已。单就成熟了的领域而言，这篇文章也仅仅是入门性的涉及了非类型化 λ 演算的一部分而已。关于 λ 演算的可计算性分析，关于类型化 λ 演算，以及当代 λ 演算的最前沿进展方面，一来限于文章定位，二来也限于作者水平有限肚里没货了，就不在此摆弄了。若有兴趣的读者不妨沿着文章中给出的参考链接自行畅游一番。

最后，稍稍抒发一下我当初渐入门道时由衷的那番感触，当然这种感受随着越深入的探询仍在不断的加深，实可谓 λ 演算是于毫微之末成就壮丽山河的一个典型，着实让人赞叹智慧的神奇绚烂！

### 后记 ###

有朋友跟我说你这个写的不友好，太烧脑，我在偷偷笑。有人喜欢阳春白雪，有人喜欢荆棘丛中信步游，何必强求口味一致呢。我就属于后者，看文章收效上，喜欢挑战自我思维能力的同好还是挺多，不如分享点其它小小心得，一起来享受下大脑超频的乐趣吧。以下文章均是入选过首页推荐的文章，质量上该算还过得去，至于错别字嘛，呃 ~ ~ ~ ~ ~

[Link 1]: http://www.cs.man.ac.uk/~hsimmons/BOOKS/lcalculus.pdf
[Link 2]: http://www.inf.fu-berlin.de/inst/ag-ki/rojas_home/documents/tutorials/lambda.pdf
[Link 3]: http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf
[Link 4]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
[Link 5]: https://en.wikipedia.org/wiki/Peano_axioms
[wikipedia]: https://en.wikipedia.org/wiki/Fixed-point_combinator
[Link 6]: https://en.wikipedia.org/wiki/Lazy_evaluation
[Link 7]: https://en.wikipedia.org/wiki/Computability_theory