简单易懂的程序语言入门小册子（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$ 演算只包含三种表达式。 形式化地定义 $\lambda$ 演算的语法如下：

下面给出几个 $\lambda$ 演算的表达式的例子：

$\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)$ 的精确定义）应该分成变量、函数和函数调用三种情况讨论：

替换

用记号 $M[X \leftarrow N]$ 表示在表达式 $M$ 中将自由变量 $X$ （如果有出现这个自由变量）替换成表达式 $N$ 。 更准确的定义如以下公式：

如果 $N$ 中没有自由变量 $X_1$ ，那么这个公式可以简化成：

归约

所谓归约，可以理解成求值，或者表达式化简（初中好像有学过代数表达式化简）。 $\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]$$
• $\beta$ 归约表示了函数调用过程，是最常用的归约。 $\beta$ 归约用函数调用的输入参数（实参）替换函数体中出现的参数变量（形参）： $$(\lambda X.M \; N) \rightarrow_\beta M[X \leftarrow N]$$
• $\eta$ 归约指： $$\lambda x.(f \; x) \rightarrow_\eta f$$ 这个有点怪，但仔细想想不难理解。

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

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

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

呼！总算写完。

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

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

原文：http://www.cnblogs.com/skabyy/p/3670193.html