最近比较闲，打算整理一下之前学习的关于程序语言的知识。主要的内容其实就是一边设计程序语言一边写解释器实现它。这些知识基本上来自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
- 无限循环@_@
呼！总算写完。