这一篇接在第一篇lambda演算的后面。讲讲一些数学知识。
经常有些看似很容易理解的东西，一旦要描述得准确无误，就会变得极为麻烦。 软件工程里也有类似情况：20%的代码实现了核心功能，剩下80%的代码处理边界情况。 于是，所谓的准确描述里的大部分文字都在说明边界情况，核心概念只有寥寥几字——好比一件打满补丁的衣服，完全看不出原来的样子。 出现这种现象要么是人类的大脑有缺陷，难以严谨而又准确的理解概念，也就是说人类太笨； 要么就是语言系统有问题，难以简洁地表达概念，而发明不出新的语言系统的人类还是很笨。 无怪乎“人类一思考，上帝就发笑”。 这一节打算尽量严谨地描述$lambda$演算里的一些符号的含义，希望不会写得太繁琐。
递归定义
实数的链表$List$一般定义为： egin{equation*}egin{array}{lcl} List &=& {nil} \ &|& left<R, List ight> end{array}end{equation*} 其中，nil是一个空链表，$left<A, B ight>$表示包含$A$和$B$的二元组，$R$表示实数集合。
这个文法实际上是定义了一个集合$List$，我用集合运算的符号重写$List$的定义： egin{equation*}egin{array}{lcl} List &=& {{nil}} \ &cup& {left<r, l ight> | r in R, l in List} end{array} end{equation*} 这是个递归定义。 递归定义对于没接触过的人来说，其实是很难以理解的。 我们现在觉得递归定义很直观，或许只是{f习惯了}这种东西而已。 递归定义难以理解的地方在于，我们在描述定义的地方用到了被定义的事物本身。
比如说，我现在想知道$List$是什么。 这时我脑里有$List$这个符号，但是我还不知道$List$代表什么内容。 然后我就来看这个定义，结果看到定义里的第二行用到了$List$，但是我这时候还没不知道什么是$List$呢！
所以，为了具体解释递归定义到底定义了什么，我下面用一种构造性的方法来定义$List$。
首先，基础情况是空链表nil，构造一个只包含nil的集合，记为$List_0$。 [ List_0 = {{nil}} ] 向nil的添加一个元素可以生成只包含一个元素的链表。 所有只包含一个元素的链表的集合再并上$List_0$就是所有元素个数小于等于1的链表的集合，记为$List_1$。 egin{equation*}egin{array}{lcl} List_1 &=& {{nil}} \ &cup& {left<r, l ight> | r in R, l in List_0} end{array} end{equation*} 依此类推可以构造包含所有元素个数小于等于2的链表的集合$List_2$，所有元素个数小于等于3的链表的集合$List_3$…… 一般地，可以构造包含所有元素个数小于等于$i$（$i>0$）的链表的集合$List_i$： egin{equation*}egin{array}{lcl} List_i &=& {{nil}} \ &cup& {left<r, l ight> | r in R, l in List_{i-1}} end{array} end{equation*} 当$i$趋于无穷时，我们就得到了链表的集合$List$： [ List = lim_{i ightarrow infty}{List_i} ] 顺便一提，这里用到了极限，或许还得解释解释集合的极限是什么意思，这个极限收不收敛等问题。 不过，管他的，理解是什么意思就行。 可以看到，递归定义是一个涉及到“无穷”的定义。 很多东西一旦涉及到无穷就很麻烦。
在$List_i$的定义中让$i$趋向无穷看看会怎样？ 由于当$i$趋向无穷时有$List_i = List_{i-1} = List$，所以我们得到了$List$的递归定义。
下面用同样的思路描述了$lambda$演算的语法： egin{equation*}egin{array}{lcl} M_0 &=& X \ M_i &=& X \ &cup& {lambda x.m | x in X, m in M_{i-1}} \ &cup& {(m ; n) | m in M_{i-1}, n in M_{i-1}} \ M &=&displaystyle lim_{i ightarrow infty}{M_i} end{array} end{equation*}
归约派生的等价关系
数学让人如此讨厌大概是因为它严谨得像处女座一样。 在我们计算$lambda$演算的表达式时，我们这样写： egin{equation*}egin{array}{lcl} ((lambda y.lambda x.(x ; y) ; a) ; lambda z.z) &=& (lambda x.(x ; a) ; lambda z.z) \ &=& (lambda z.z ; a) \ &=& a end{array} end{equation*} 嗯？等号$=$具体是什么意思呢？它是$alpha$归约、$eta$归约和$eta$归约的某种混合。 下面解释“某种混合”具体是什么意思。
归约（$alpha$归约、$eta$归约和$eta$归约）实质上是一个集合，这个集合的元素是二元组$left<m, n ight>$。 这个二元组的意思是$m$可以归约到$n$。 这里混合这三种归约的关系记为符号$ ightarrow$。 “混合”是并集的意思。 $ ightarrow$定义为： egin{equation*}egin{array}{lcl} ightarrow &=& ightarrow_alpha cup ightarrow_eta cup ightarrow_eta end{array} end{equation*} 简单来说，就是$m ightarrow n$当且仅当$m ightarrow_alpha n$或$m ightarrow_eta n$或$m ightarrow_eta n$。
$ ightarrow$是不是$=$呢？ 如果是的话我就不会特地选用其他符号了。 我们知道，一个等价关系$=$是一个满足以下三种特性的关系：
- 自反性：$m = m$，也就是自己等于自己；
- 对称性：如果$m = n$，那么$n = m$；
- 传递性：如果$m = n$并且$n = l$，那么$m = l$。
用这三个特性扩展$ ightarrow$。扩展后的关系记为$approx$： egin{equation*}egin{array}{rcl} m &approx& m \ m ightarrow n &Rightarrow& m approx n \ m approx n &Rightarrow& n approx m \ m approx n, n approx l &Rightarrow& m approx l end{array} end{equation*}
$approx$还不是我们需要的等号$=$！ 看下面例子： egin{equation*}egin{array}{rclr} (underline{(lambda y.lambda x.(x ; y) ; a)} ; lambda z.z) &approx& (underline{lambda x.(x ; a)} ; lambda z.z) & ext{错！}\ (lambda y.lambda x.(x ; y) ; a) &approx& lambda x.(x ; a) & ext{对！} end{array} end{equation*} 看到这两个表达式的区别吗？ $approx$只能在“最外层”归约！它不能归约子表达式。
所以，还要在$approx$的基础上添加最后一个特性，添加后就是$=$了： egin{equation*}egin{array}{rcl} m approx m' &Rightarrow& m = m' \ m = m' &Rightarrow& lambda x.m = lambda x.m' \ m = m' &Rightarrow& (m ; n) = (m' ; n) \ n = n' &Rightarrow& (m ; n) = (m ; n') end{array} end{equation*} 在一个大的表达式中，除去一个子表达式以外的部分叫做这个子表达式的上下文。 上面这个特性的意思就是，一个子表达式的归约和它的上下文无关。
终于讲完$=$是什么意思了。 但是还有一个“小问题”。 $=$的计算过程并非唯一的。 比如下面这个例子： egin{equation*}egin{array}{lcl} (lambda x.x ; underline{(lambda y.y ; a)}) &=& underline{(lambda x.x ; a)} = a \ underline{(lambda x.x ; (lambda y.y ; a))} &=& underline{(lambda y.y ; a)} = a end{array} end{equation*} 一个先计算参数$(lambda y.y ; a)$，一个则先在最外层做归约。 计算过程不同产生一个问题： 不同计算过程计算出的答案是否是相同（允许$alpha$归约意义下的相同，如$lambda x.x$和$lambda y.y$算一样）的？ 关注程序语言这一领域的人或许有听过Church-Rosser定理。 这个定理的推论就是这个问题的肯定回答。