基于文本替换的解释器：递归定义与lambda演算的一些额外说明

基于文本替换的解释器：递归定义与lambda演算的一些额外说明2015-01-12这一篇接在第一篇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*}