语义工程和PLT Redex

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

第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}B& =& \mathtt{t}\\ & |& \mathtt{f}\\ & |& (B•B)\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}M,N,L& =& X\\ & |& (\lambda X.M)\\ & |& (MM)\\ X,Y,Z& =& \text{一个变量: }x,y,\dots \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$在前两个表达式里都是自由出现的, 而在后面的例子里是绑定出现的.

第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