语义工程和PLT Redex

本书侧重于从抽象机器介绍编程语言, 愚以为某些内容尚待打磨, 并非易读. 本书分为三个部分, 第一部分介绍了操作语义和抽象机器, 第二部分引入了表达操作语义的工具PLT Redex, 第三部分呈现了PLT Redex的一些实际应用.

这本书我所喜欢的一个地方在于它的记号, 其用$X$表示变量的句法范畴. 当然, 根据上下文, $X$以及$X_1,X_2,\dots$也可以用来代表句法范畴$X$的一个元素. 小写字母被视为具体的字面上的变量, 例如$x,y,z,\dots$. 这和其他关于$\lambda$演算的书籍和论文都相当不同, 那里一般使用$x,y,z$表示变量的句法范畴, 又使用$x,y,z$代表任意一个变量, 或者说又作为代表变量的元变量使用. 这经常给我造成一些本来可以避免的困惑, 比如说我经常会问自己, 这个$\lambda$项里的$x$和$y$能够指代相同的变量吗? 一般而言, 有良心的作者其实至少会作出一些约定. 尽管如此, 有时这些约定反而给我造成了更大的困惑. 我总是感到他们完全没有考虑到这些事情, 而我好像就只是一个喜欢钻牛角尖的蠢货. 所以说, 当我看到有人和我一样认为有必要进行这种明确的区分时, 我的确感到相当高兴.

第1章 语义via句法

描述编程语言自句法始. 正如每个程序员所知, 语言的句法总以BNF (Backus-Naur Form) 语法的某种变体形式出现, 其枚举了符合语法的词汇和句子. 困难之处实际上在于刻画程序的意义, 即程序是如何进行计算的.

在这本书的第一部分, 我们建立了一个基于句法的语义描述方法. 我们从这样的观察开始, 即计算 (computation) 是对于算术 (calculation) 的一般化, 一个孩子所接受的算术训练从$1$加$1$等于$2$这样的材料开始. 诀窍在于看出这种形式的算术也可应用到程序上来.

程序的算术意味着观察一个表达式或者语句的句法, 然后将其与另一个表达式或者语句联系起来, 通常假定是更简单的. 对于表达式$1+1$而言, 前面的声明是容易理解的. 它等于$2$, 即$1+1$和$2$关联起来. 即便是函数应用于参数值也可以这种方式表达 [注记: 实际上, $+$本身即是一个二元函数]:$$\text{如果定义}f(x)=2\cdot x+55\text{, 那么}f(4)=2\cdot 4+55\text{.}$$

用数学语言来说, 我们是在以句法上的关系描述编程语言的语义. 对于学习函数式编程语言的人而言, 这种声明并不令人意外. 我们知道函数式编程并不超出将七年级代数转换为编程语言太多, 而代数定律不过就是将代数表达式相互联系起来的等式. 但或许令人惊讶的是, 以这种方法我们可以描述(几乎)所有编程语言的语义, 即便是那些含有命令式副作用的语言.

现在我们将引入我们的想法, 即必要的数学元知识, 从将句法定义为集合开始.

第1.1节 定义集合

BNF语法可有多种用途. 一种含义是字符串的集合. 另一种解释是树的集合, 其常被称为抽象句法(树). 本书我们总是指后者.

对于本章和下一章而言, 我们使用下面的BNF语法作为一个实际例子:$$\begin{array}{|rcl|}\hline B& =& \mathtt{t}\\ & |& \mathtt{f}\\ & |& (B•B)\\ \hline\end{array}$$我们将其当作以下施加于抽象句法树集合$B$上的约束的缩写:$$\begin{array}{c}\mathtt{t}\in B\\ \mathtt{f}\in B\\ a\in B\text{且}b\in B\Rightarrow (a•b)\in B\end{array}$$从技术上说, $B$是满足以上约束的最小集合. 为了构造这个集合, 我们先包括基本元素$\mathtt{t}$和$\mathtt{f}$, 然后归纳性地将其组合为复合元素.

记号: 我们有时用$B$表示集合$B$, 但是有时$B$又表示$B$的任意一个元素. 从上下文来看, 意义总是明确的. 有时我们将下标或者撇号附到集合的名字上以表示该集合的任意元素, 例如$B_1$或者$B^{\prime }$. 因此, 以上约束也可以写成$$\begin{array}{cl}\mathtt{t}\in B& \text{[a]}\\ \mathtt{f}\in B& \text{[b]}\\ (B_1•B_2)\in B& \text{[c]}\end{array}$$在有限的空间之中枚举出$B$的所有元素显然是不可能的:$$B=\{\mathtt{t},\mathtt{f},(\mathtt{t}•\mathtt{t}),(\mathtt{t}•\mathtt{f}),\dots \}$$然而, 给定某个树, 我们可以通过表明其满足约束而论证其的确属于$B$. 例如, $(\mathtt{t}•(\mathtt{f}•\mathtt{t}))$就在$B$中:$$\begin{array}{lll}\text{1.}& \mathtt{t}\in B& \text{根据[a]}\\ \\ \text{2.}& \mathtt{f}\in B& \text{根据[b]}\\ \text{3.}& \mathtt{t}\in B& \text{根据[a]}\\ \text{4.}& (\mathtt{f}•\mathtt{t})\in B& \text{根据2, 3, 以及[c]}\\ \\ \text{5.}& (\mathtt{t}•(\mathtt{f}•\mathtt{t}))\in B& \text{根据1, 4, 以及[c]}\end{array}$$通常这样的论证也可以安排成所谓的证明树的形式:

第1.2节 关系

第1.3节 作为等价关系的语义

第1.4节 语义via归约

第1.5节 上下文中的归约

第1.6节 求值函数

第1.7节 记号总结

第2章 分析句法性语义

一旦我们有了一个编程语言的一个句法和一个语义, 那么我们就可以提出问题, 进行实验, 以及考虑变种. 在本书的这部分里, 我们将检视编程语言理论学家会问出的最基本问题, 并研究我们该如何回答这些问题. 在本书的第二部分里, 我们将会引入一个用于对句法和语义进行实验的工具, 其通常有助于形成猜想和问题.

现在我们使用第一章所引入的句法和语义来描述我们会问什么种类的问题, 以及如何严格地回答它们. 本章的第二节将答案以数学定理和证明的形式呈现, 引入了对于本书该部分的剩余内容而言关键的证明概念.

第2.1节 从问题到数学声明

第一章定义了几个求值器 {译注: 其实就两个}, 包括

第2.2节 作为定理的回答

第3章 $\lambda$演算

第3.1节 函数和$\lambda$演算

第3.2节 $\lambda$演算: 句法和归约

$\lambda$演算的表达式的一般语法定义如下:$$\begin{array}{|rcl|}\hline M,N,L& =& X\\ & |& (\lambda X.M)\\ & |& (MM)\\ X,Y,Z& =& \text{一个变量: }x,y,\dots \\ \hline\end{array}$$以下是$M$的示例成员:$$x,(xy),(\lambda x.x),((xy)(zw)),(\lambda y.(\lambda z.y)),((\lambda y.(yy))(\lambda y.(yy)))$$第一个例子, 即$x$, 没有特定的直觉性意义, 因为$x$还未被定义. 类似地, $(xy)$的意义是$x$应用于$y$, 但是我们没有更多可说的了. 与之形成对比的是, 例子$(\lambda x.x)$与恒等函数相对应. 这个例子和前两个例子的不同之处在于$x$在前两个表达式里都是自由出现的, 而在后面的例子里是绑定出现的.

最后, 为了定义$\lambda$演算里的一般规约关系$\mathbf{n}$, 让我们首先定义三个简单的规约概念, 即$\alpha ,\beta ,\eta$.$$\begin{array}{|rcl|}\hline (\lambda X_1.M)& \alpha & (\lambda X_2.M[X_1\leftarrow X_2])\\ & & \text{如果}{X}_2\notin \mathcal{FV}(M)\\ ((\lambda X.M_1)M_2)& \beta & M_1[X\leftarrow M_2]\\ (\lambda X.(MX))& \eta & M\\ & & \text{如果}X\notin \mathcal{FV}(M)\\ \hline\end{array}$$

• $\alpha$对于一个函数的形式参数进行重命名.

第3.3节 编码布尔

第3.4节 编码序对

第3.5节 编码数字

第3.6节 编码和错误

第3.7节 递归

第3.8节 一致性和规范形式

第3.9节 规范形式和归约策略

第3.10节 历史

第4章 ISWIM

1950年代末期和1960年代早期, 人们发现了编程语言和$\lambda$演算的诸多方面之间的联系. 其动机从想要刻画Algol 60的语义演变为藉由已经充分理解了的数学系统来理解编程语言的面貌. 也就是说, 人们想要学会如何系统地设计编程语言.

第4.1节 ISWIM表达式

第4.2节 ISWIM的计算

第4.3节 $\alpha$, $\eta$和商

第4.4节 ${\mathtt{Y}}_{\mathtt{V}}$组合子

第4.5节 求值

第4.6节 一致性

第4.7节 观察等价

第4.8节 历史

第5章 一个抽象句法机器

第5.1节 标准归约

第5.2节 标准归约定理

第5.3节 对于观察等价进行推理

第5.4节 一致求值

第5.5节 历史

第6章 抽象寄存器机器

第6.1节 CC机器

第6.2节 SCC机器

第6.3节 CK机器

第6.4节 CEK机器

第6.5节 历史

第7章 尾调用和更多的空间节省

第7.1节 SECD机器

第7.2节 求值上下文的空间

第7.3节 环境的空间

第7.4节 历史

第8章 控制: 错误, 异常和延续

第9章 状态: 命令式赋值

第10章 简单类型ISWIM