简单易懂的程序语言入门小册子（1）：基于文本替换的解释器，lambda演算

最近比较闲，打算整理一下之前学习的关于程序语言的知识。主要的内容其实就是一边设计程序语言一边写解释器实现它。这些知识基本上来自Programming Languages and Lambda Calculi和Essentials of Programming Languages这两本书。

我还记得高中奥数竞赛培训时的老师这样说过：“解题时一定要抓住定义。” 编程和解题一样，也要抓住定义。所以在写解释器前，得先定义好这门要解释的程序语言。这门程序语言基于Lambda演算。

从\(\lambda\)演算讲起

真不想讲\(\lambda\)演算……算了，还是简要说明一下。\(\lambda\)演算之于程序语言中的地位好比集合论之于数学。正如每一本数学教材，都要从集合论开始；每一本程序语言教材，也要从\(\lambda\)演算讲起。不过话说回来，追根溯源\(\lambda\)演算也是从集合论搭起来。咱就不走那么远了，又累又没什么意思……

\(\lambda\)演算中的基本类型只有变量和函数两种。变量用大写字母\(X\)表示。像\(a,b,x,y,abc,...\)都是变量。一个函数包含两个元素：一个是函数参数（形参），它是一个变量；另一个元素是函数体，它是一个\(\lambda\)演算表达式（这里是递归定义）。用(lambda X M)表示一个函数，其中X是一个变量，M是一个\(\lambda\)演算表达式（别吐槽参数X那里少了个括号。）。为了描述的简洁，也用\(\lambda X.M\)表示一个函数。

举个例子，\(\lambda x.x\)是一个恒等函数\(f(x) = x\)。在数学上一般用\(f(a)\)表示函数调用，\(a\)是实参。在\(\lambda\)演算中把函数也放入括号，记为\((\lambda x.x \; a)\)。函数调用的计算方法是在函数体中用实参替换形参。在这个例子里\((\lambda x.x \; a) = a\)。这个计算过程称为归约。

\(\lambda\)演算的函数都只包含一个参数。如果要使用多参函数，可以用多个函数嵌套。下面是一个例子： \[ \lambda x.\lambda y.(x \; y) \] 这种技巧被称作currying。

从上面的讨论看出，\(\lambda\)演算只包含三种表达式。形式化地定义\(\lambda\)演算的语法如下： \begin{eqnarray*} M, N, L &=& X \\ &|& \lambda X.M \\ &|& (M \; N) \end{eqnarray*} 这里用大写字母\(M\)、\(N\)和\(L\)代表\(\lambda\)演算的表达式，这是个递归定义，第二行、第三行出现了\(M\)和\(N\)。第三行表达式是一个函数调用，一般要求处于函数位置的\(M\)应该要能归约成一个函数，否则归约就没法进行下去啦。

下面给出几个\(\lambda\)演算的表达式的例子： \begin{eqnarray*} & x \\ & \lambda x.x \\ & (\lambda x.x \; y) \\ & (\lambda x.(x \; x) \; \lambda x.x) \\ & (\lambda x.(x \; x) \; \lambda x.(x \; x)) \end{eqnarray*}

\(\lambda\)演算的归约依赖于替换操作。在介绍替换操作之前还得先介绍自由变量。

自由变量

考察一个表达式：\((\lambda x.(\lambda x.x \; x) \; a)\)。这个表达式归约到\((\lambda x.x \; a)\)。可以看到，在\(\lambda x.(\lambda x.x \; x)\)函数体\((\lambda x.x \; x)\)中参数位置的变量\(x\)和\(\lambda x.x\)中点后面的\(x\)是不一样的。参数位置中的\(x\)被替换成\(a\)，而\(\lambda x.x\)中点后面的\(x\)没有被替换。被替换的\(x\)称为表达式\((\lambda x.x \; x)\)的自由变量。在函数调用的替换过程中只有自由变量会被替换。

自由变量指一个表达式中没有受到约束的变量。约束指这个变量不是作为某个函数的参数而存在。如表达式\(\lambda x.(f x)\)中\(f\)是自由变量，\(x\)不是自由变量。用\(FV(M)\)表示表达式\(M\)中的所有自由变量的集合。

从这里开始，描述和\(\lambda\)演算有关的一些定义和算法将遵循\(\lambda\)演算的语法定义。所以计算\(FV(M)\)的算法（也是\(FV(M)\)的精确定义）应该分成变量、函数和函数调用三种情况讨论： \begin{eqnarray*} FV(X) &=& \{X\} \\ FV(\lambda X.M) &=& FV(M) \backslash \{X\} \\ FV((M \; N)) &=& FV(M) \cup FV(N) \end{eqnarray*}

替换

用记号\(M[X \leftarrow N]\)表示在表达式\(M\)中将自由变量\(X\)（如果有出现这个自由变量）替换成表达式\(N\)。更准确的定义如以下公式： \begin{eqnarray*} X_1[X_1 \leftarrow N] &=& N \\ X_2[X_1 \leftarrow N] &=& X_2 \\ &&其中X_1 \neq X_2 \\ (\lambda X_1.M)[X_1 \leftarrow N] &=& (\lambda X_1.M) \\ (\lambda X_1.M)[X_2 \leftarrow N] &=& (\lambda X_3.M[X_1 \leftarrow X_3][X_2 \leftarrow N]) \\ &&其中X_1 \neq X_2, X_3 \notin FV(N), X_3 \notin FV(M)\backslash\{X_1\} \\ (M_1 \; M_2)[X \leftarrow N] &=& (M_1[X \leftarrow N] \; M_2[X \leftarrow N]) \end{eqnarray*} 第四个公式看着比较复杂，其实是为了避免\(N\)中有自由变量\(X_1\)这种情况。举个例子，\(\lambda x.y[y \leftarrow (x x)]\)应该替换为\(\lambda z.(x x)\)。如果替换成\(\lambda x.(x x)\)就不对了。

如果\(N\)中没有自由变量\(X_1\)，那么这个公式可以简化成： \begin{eqnarray*} (\lambda X_1.M)[X_2 \leftarrow N] = (\lambda X_1.M[X_2 \leftarrow N]) \end{eqnarray*}

归约

所谓归约，可以理解成求值，或者表达式化简（初中好像有学过代数表达式化简）。 \(\lambda\)演算有三种归约方法。三种归约分别称为\(\alpha\)归约，\(\beta\)归约和\(\eta\)归约。名字看着很渗人，不表示这三种归约难以理解，只说明命名的人没有一颗爱玩的心。

\(\alpha\)归约的意思是，函数参数变量的变量名是什么无关紧要。比如\(\lambda x.x\)和\(\lambda y.y\)表示的同一个函数。这个归约很基本，但是几乎上不会被用到就是的了。 \[ \lambda X_1.M \rightarrow_\alpha \lambda X_2.M[X_1 \leftarrow X_2] \quad \text{其中}X_2 \notin FV(M)\]
\(\beta\)归约表示了函数调用过程，是最常用的归约。 \(\beta\)归约用函数调用的输入参数（实参）替换函数体中出现的参数变量（形参）： \[ (\lambda X.M \; N) \rightarrow_\beta M[X \leftarrow N] \]
\(\eta\)归约指： \[ \lambda X.(M \; X) \rightarrow_\eta M \quad \text{其中}X \notin FV(M)\] 这个有点怪，但仔细想想不难理解。

一个解释器的作用是输入一个表达式，输出该表达式归约到最简（不能再\(\beta\)归约）的形式。一般我们是希望这个最简形式能够是一个变量（\(X\)）或者一个函数（\(\lambda X.M\)），因为函数调用是用来让人进行\(\beta\)归约的。变量，或者函数，被称为“值”。但是也有些坏掉了的表达式像\((x \; x)\)，由于\(x\)是个变量而非函数，这个表达式没法再归约。通常这种表达式被认为非法的表达式。如果输出这种结果就表示输入程序有误，程序崩溃。另外有些表达式不能归约到某种最简形式，也就是无限循环（可怜的西西弗斯）。无限循环的一个经典例子是这个输入：\((\lambda x.(x \; x) \; \lambda x.(x \; x))\)。

一个解释器，给它一个输入，它会有以下三种情况：

输出一个值:-)
崩溃XD
无限循环@_@

呼！总算写完。

巴特西

简单易懂的程序语言入门小册子（1）：基于文本替换的解释器，lambda演算

从\(\lambda\)演算讲起

自由变量

替换

归约

最新文章

热门文章