语义工程和PLT Redex

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

在这本书的第一部分, 我们建立了一个基于句法的语义描述方法. 我们从这样的观察开始, 即计算 (computation) 是对于算术 (calculation) 的一般化, 一个孩子所接受的算术训练从"

1

加

1

等于

2

"这样的材料开始. 诀窍在于看出这种形式的算术也可应用到程序上来.

程序的算术意味着观察一个表达式或者语句的句法, 然后将其与另一个表达式或者语句联系起来, 通常假定是更简单的. 对于表达式

1 + 1

而言, 前面的声明是容易理解的. 它等于

2

, 即

1 + 1

和

2

关联起来. 即便是函数应用于参数值也可以这种方式表达 [译注: 虽然

+

本身就是一个二元函数]:

f (4) = 2 ⁎ 4 + 55, 如果定义 f (x) = 2 ⁎ x + 55 .

用数学的语言来说, 我们是将编程语言的语义描述为其句法上的关系. 对于学过函数式编程语言的人而言, 这种声明并不令人意外. 我们知道函数式编程并不超出将七年级代数转换为编程语言太多, 而代数定律是将代数表达式互相联系起来的等式. [译注: 在某种意义上来说, 这句话是一种虚张声势.] 但令人惊讶的是, 这种方法具有描述(几乎)所有编程语言的语义的可能性, 即便是包含命令式副作用的语言.

现在我们来介绍这种想法, 从将句法定义为集合开始, 这是必要的数学元知识.

第1.1节定义集合

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

对于本章和下一章而言, 我们使用下面的BNF语法作为例子:

\begin{array}{rcl} B & = & t \\ | & f \\ | & (B • B) \end{array}

我们将其当作下列施加于抽象句法树集合

B

上的约束的缩写:

\begin{matrix} t \in B \\ f \in B \\ a \in B 且 b \in B \Rightarrow (a • b) \in B \end{matrix}

从技术上说,

B

是满足以上约束的最小集合. 为了构造这个集合, 我们先容纳基本元素

t

和

f

, 然后归纳地将其中的东西组合成复合元素.

记号: 我们有时用"

B

"表示"集合

B

", 但有时"

B

"也代表"

B

的任意一个元素". 从上下文来看, 含义总是明确的. 有时, 我们将下标或一撇附加在集合的名字上来集合的任意元素, 例如"

B_{1}

"或者"

B^{'}

". 因此, 以上约束也可以写成

\begin{matrix} t \in B & [a] \\ f \in B & [b] \\ (B_{1} • B_{2}) \in B & [c] \end{matrix}

在有限的空间之中枚举出

B

的所有元素显然是不可能的:

B = {t, f, (t • t), (t • f), \dots}

然而, 给定某个树, 我们可以通过论证它满足约束来证明其属于

B

. 例如,

(t • (f • t))

就在

B

中:

\begin{array}{l} 1. & t \in B & by [a] \\ 2. & f \in B & by [b] \\ 3. & t \in B & by [a] \\ 4. & (f • t) \in B & by 2, 3, and [c] \\ 5. & (t • (f • t)) \in B & by 1, 4, and [c] \end{array}

通常, 这样的论证也可以被安排成所谓的证明树的形式:

\frac{t \in B [a] \frac{f \in B [b] t \in B [a]}{(f • t) \in B} [c]}{(t • (f • t)) \in B} [c]

绝大多数时候, 证明树以没有标签的形式出现, 因为每一步通常都是显然的:

\frac{t \in B \frac{f \in B t \in B}{(f • t) \in B}}{(t • (f • t)) \in B}

第1.2节关系

关系是序对的集合. 例如, 我们可以将关系

R

定义成将

B

的每个元素与自身匹配的关系:

a \in B \Rightarrow ⟨ a, a ⟩ \in R

对于像

R

这样的二元关系, 与其记

⟨ a, a ⟩ \in R

, 不如写成

a R a

a \in B \Rightarrow a R a

甚至可以更简单

B_{1} R B_{1}

只要其被理解为

R

的定义. 实际上, 关系

R

是自反的, 对称的, 传递的, 即其满足以下三个约束条件:

\begin{array}{l} 一个关系 R 是自反的 & 当且仅当 & a R a (对于任意的 a 而言) \\ 一个关系 R 是对称的 & 当且仅当 & a R b \Rightarrow b R a \\ 一个关系 R 是传递的 & 当且仅当 & a R b 且 b R c \Rightarrow a R c \end{array}

如果一个关系是自然的, 对称的, 传递的, 那么其就被称为一个等价关系 (equivalence). 关系的特定名字, 例如

=

, 暗示了该关系是一个等价关系.

以下定义了一个关系

r

, 它既不自反, 对称, 也不传递.

\begin{matrix} (f • B_{1}) & r & B_{1} & [a] \\ (t • B_{1}) & r & t & [b] \end{matrix}

在规约语义的上下文中, 这样的关系被称为规约的概念. 对于该定义的一个小小的修饰可以产生一个自反关系

≍_{r}

\begin{matrix} (f • B_{1}) & ≍_{r} & B_{1} & [a] \\ (t • B_{1}) & ≍_{r} & t & [b] \\ B_{1} & ≍_{r} & B_{1} & [c] \end{matrix}

另一种定义

≍_{r}

的方法在于扩展

r

并显式约束新的关系为自反的:

\begin{matrix} B_{1} & ≍_{r} & B_{2} & 如果 B_{1} r B_{2} & [ab] \\ B_{1} & ≍_{r} & B_{1} & [c] \end{matrix}

因此关系

≍_{r}

是

r

的自反闭包. 我们还可以通过添加对称和传递约束来定义另一个关系:

\begin{matrix} B_{1} & \approx_{r} & B_{2} & 如果 B_{1} r B_{2} & [ab] \\ B_{1} & \approx_{r} & B_{1} & [c] \\ B_{2} & \approx_{r} & B_{1} & 如果 B_{1} \approx_{r} B_{2} & [d] \\ B_{1} & \approx_{r} & B_{3} & 如果 B_{1} \approx_{r} B_{2} 且 B_{2} \approx_{r} B_{3} & [e] \end{matrix}

关系

\approx_{r}

是

≍_{r}

的对称传递闭包, 并且它也是

r

的自反对称传递闭包或者说等价闭包.

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

B

和

r

的实际例子暗示了一个编程语言是如何通过句法以及句法上的关系定义的, 或者更确切地说, 作为一个抽象句法树上的集合

B

以及该集合上的一个关系

r

. 实际上, 或许机敏的读者可能开始怀疑

B

是布尔表达式的语法, 其中

t

代表

true

f

代表

false

•

代表"或"运算符. 关系

\approx_{r}

将具有相同(布尔)值的

B

表达式等同起来.

的确, 使用上面的约束, 我们可以表明

(f • t) \approx_{r} (t • t)

, 正如

false \lor true = true \lor true

\frac{(f • t) \approx_{r} t [a] \frac{(t • t) \approx_{r} t [b]}{t \approx_{r} (t • t)} [d]}{(f • t) \approx_{r} (t • t)} [e]

然而, 这并不能直接得出

•

和布尔"或"表现得完全一致. 如果我们希望建立这种联系, 那么我们不得不证明关于

•

的一般声明, 例如对于任意的表达式

B_{1}

有

(B_{1} • t) \approx_{r} t

换言之, 编程语言的语义和我们想要知道的这个语义的性质之间存在一般性的gap. 出于许多目的, 语义的性质和其将表达式或程序联系至的值一样重要. 例如, 如果

•

的确满足"或"的法则, 那么一个编译器或许可以安全地将

(B_{1} • t)

优化为

t

. 类似地, 如果编程语言的语义可以保证数字不会被加到任何非数字的东西上去, 那么语义的实现就无需检查加法运算的参数以保证它们都是数字.

第1.4节语义via规约

关系

\approx_{r}

让人想到小学里从算术和代数中学到的

=

. 正如在这种情况下我们教授学生出于各种目的都使用这样的等式推理, 我们可以使用

\approx_{r}

关系来证明特定表达式的等价性. 尽管如此, 在一般情况下, 这个关系并没有指明该如何从一个任意的

B

得到

t

或

f

——这是我们在构建一个语义的解释器时所真正需要的东西.

在这种意义下, 关系

r

实际上比

\approx_{r}

更有用. 在

r

的定义的两种情况下, 一个表达式都与另一个更小的表达式联系起来. 而且, 对于任何表达式

B

, 要么

B

是

t

或

f

, 要么

r

将

B

与至多一个另外的表达式联系起来. 因此, 我们可以将

r

想成是一个单步规约, 与解释器采取单一的求值步骤迈向最终的值对应起来.

使用

r

, 我们可以定义其自反传递闭包

𝕣

\begin{array}{l} B_{1} & 𝕣 & B_{1} \\ B_{1} & 𝕣 & B_{2} & 如果 & B_{1} r B_{2} \\ B_{1} & 𝕣 & B_{2} & 如果 & B_{1} 𝕣 B_{3} & 且 & B_{3} 𝕣 B_{2} \end{array}

这产生了一个多步规约关系. 特别地, 多步关系

𝕣

将一个表达式映射至许多其他的表达式, 但是

t

和

f

之中最多只能有一个.

关系

r

和

𝕣

被有意设计为非对称的, 这强调了求值具有特定的方向性. 例如, 给定表达式

(f • (f • (t • f)))

, 我们可以表明存在一个从它到

t

的规约序列:

\begin{array}{rcl} (f • (f • (t • f))) & r & (f • (t • f)) \\ r & (t • f) \\ r & t \end{array}

左列的空白隐式地被前一行的右列的表达式所填充. 于是, 每一行都是对于

(f • (f • (t • f))) 𝕣 t

的论证中的一步.

第1.5节上下文中的规约

表达式

((f • t) • f)

该怎样规约呢? 根据

r

或者

𝕣

, 它压根就不能规约. 从直觉上来说,

((f • t) • f)

应该被规约为

(t • f)

, 即根据

(f • t) r t

来简化第一个子表达式. 然而,

r

的定义中没有能够匹配

((f • t) • f)

作为源表达式的规则. 也就是说, 我们只能规约具有形式

(f • B)

或者

(t • B)

的表达式. 尽管最外层的

•

的右侧表达式可以是任意的, 但左侧的表达式必须是

t

或者

f

才行 [译注: 即才能规约].

如果我们希望将这样的

B

表达式规约为答案, 那么我们必须扩展

r

关系为另一个能够支持子表达式规约的关系.

\begin{matrix} B_{1} & \to_{r} & B_{2} & 如果 & B_{1} r B_{2} & [a] \\ (B_{1} • B_{2}) & \to_{r} & (B_{1}^{'} • B_{2}) & 如果 & B_{1} \to_{r} B_{1}^{'} & [b] \\ (B_{1} • B_{2}) & \to_{r} & (B_{1} • B_{2}^{'}) & 如果 & B_{2} \to_{r} B_{2}^{'} & [c] \end{matrix}

关系

\to_{r}

是

r

的兼容闭包. 类似于

r

\to_{r}

是一个单步规约关系, 但是

\to_{r}

允许对于表达式的任意子表达式进行规约. 可规约表达式 (reducible expression) 被称为redex, 而一个redex周围的文本被称为其上下文.

特别地, 关系

\to_{r}

包含

((f • t) • f) \to_{r} (t • f)

. 我们可以用以下证明树来说明这个包含:

\frac{\frac{(f • t) r t}{(f • t) \to_{r} t} [a]}{((f • t) • f) \to_{r} (t • f)} [b]

继续使用

\to

, 我们可以将

((f • t) • f)

规约至

t

\begin{array}{rcl} ((f • t) • f) & \to_{r} & (t • f) \\ \to_{r} & t \end{array}

最后, 如果我们将

↠_{r}

定义为

\to_{r}

的自反传递闭包, 那么我们就得到了

((f • t) • f) ↠_{r} t

. 因此,

↠_{r}

是由

r

生成的自然规约关系.

一般来说, 仅仅关系

r

的自反闭包

≍_{r}

, 等价闭包

\approx_{r}

, 以及自反传递闭包

𝕣

不是很有趣. 我们往往最感兴趣的是兼容闭包

\to_{r}

及其自反传递闭包

↠_{r}

. 这两种关系与表达式求值和解释的典型概念相对应. 而且,

\to_{r}

的等价闭包

=_{r}

也是有趣的, 因为其将产生相同结果的表达式联系起来.

第1.6节求值函数

↠_{r}

使我们接近了求值的有用概念, 但是我们还没有抵达那里. 尽管

((f • t) • f) ↠_{r} t

, 但是我们也有

((f • t) • f) ↠_{r} (t • f)

和

((f • t) • f) ↠_{r} ((f • t) • f)

. 然而, 对于一个求值器而言, 我们仅关心一个

B

是否能求值到一个结果以及这个结果是

f

还是

t

. 其他一切都是无关紧要的.

我们使用两个定义来形式化地陈述这个想法. 首先, 我们需要刻画我们所认为的

B

"程序"的结果

R

是什么.

\begin{array}{rcl} R & = & t \\ | & f \end{array}

显然,

R

是

B

的一个子集, 因为结果也是我们的"编程语言"的表达式.

我们的第二个定义将求值刻画为

{eval}_{r}^{↠_{r}}

关系, 其将每个表达式映射至一个结果.

{eval}_{r}^{↠_{r}} : B \to R, B \mapsto {\begin{matrix} f & 如果 B ↠_{r} f \\ t & 如果 B ↠_{r} t \end{matrix}

这里我们使用了另外的记号来定义关系, 这暗示了其为函数, 即将每个元素映射至最多一个元素的关系. [译注: 这是所谓的partial function.] 我们使用函数记号的原因在于, 若

{eval}_{r}^{↠_{r}}

作为求值器要make sense的话, 那么它就必然是一个函数 (至少对于确定性的编程语言而言).

这个关系的名字既有下标也有上标. 自然地, 前者只是在说这个函数基于关系

r

, 而后者是在告诉我们求值的定义基于关系

↠_{r}

. 我们用这两者来装饰函数的名字, 因为存在许多其他变种定义. 例如, 以下定义使用基于

r

的等价关系而不是自然规约关系.

{eval}_{r}^{=_{r}} (B) = {\begin{matrix} f & 如果 B =_{r} f \\ t & 如果 B =_{r} t \end{matrix}

等价关系

=_{r}

当然是

r

的兼容, 自反, 传递, 对称闭包. [译注: 更确切地说, 是兼容闭包的等价闭包, 因为这两个运算并不可以交换.] 通过

=_{r}

来定义一个求值函数表明了程序的计算真的就只是一般化了来源于代数的运算概念.

第1.7节记号总结

以下表格总结了我们到目前为止引入的概念和记号.

\begin{array}{l} 名字 & 定义 & 直觉 \\ - & 表达式语法的成员上的基本关系 & 没有上下文的单一"规约"步骤 \\ \to_{-} & 相对于表达式语法的 - 的兼容闭包 & 上下文中的单步规约 \\ ↠_{-} & \to_{-} 的自反传递闭包 & 复数求值步骤 (零或更多) \\ =_{-} & ↠_{-} 的对称传递闭包 & 将产生相同结果的表达式等同起来 \\ {eval}_{-}^{-} & 投影于某个范围的关系 & 基于 ↠_{-} 或者 =_{-} 的完全求值 \end{array}

[译注: 如果仅是对称闭包, 一般情况下并不保持传递性, 所以需要对称传递闭包.] 最终, 我们希望得到

{eval}_{-}

, 即一般的求值关系.

第2章分析句法性的语义

一旦我们有了一个编程语言的句法和语义, 我们可以提出问题, 进行实验, 以及考虑变体. 在本部分中, 我们将看看编程语言理论家会提出的最基本的问题, 并研究如何回答它们. 在本书的第二部分, 我们将引入对于句法和语义进行实验的工具, 通常其将有助于提出猜想和问题.

现在我们使用第一章引入的句法和语义以刻画我们可以提出什么样的问题以及如何严格地回答这些问题. 第一节展现了如何用数学术语提出关于语言的问题. 第二节用数学定理和证明刻画了回答, 引入了对于本书的剩余部分而言关键的证明技术.

第2.1节从问题到数学声明

第一章定义了数个求值器, 包括

{eval}_{r}^{↠_{r}}

. 从编程语言实现者的角度来看, 这个

{eval}_{r}^{↠_{r}}

函数使用了某种类似于机器的东西, 这个机器的初状态, 中间状态和终状态是

B

表达式, 而指令是

↠_{r}

关系. 它启动程序, 等待直至机器到达一个终状态 (

t

或

f

), 然后报告这个最终结果.

一个显然的问题是, 这个求值器是否对于某个固定的程序总是产生恰好一个结果. [译注: 从上下文看, 这里更确切的说法是产生至多一个结果, 因为产生恰好一个结果是更强的条件, 是说这个关系是一个total function.] 用数学术语来说, 我们是在问这个求值器是否是一个函数. 如果的确如此, 那么若我们观察到对于相同的程序产生了两个不同的结果, 那么就知道这个求值器的实现是错的.

现在回忆一下, 关系和函数都是序对的集合. 每个序对将一个输入和一个输出结合起来. 关系和函数的不同之处在于, 后者对于任何输入最多只包含一个相关的序对. 因此, 我们的第一个问题是在问以下声明是否成立:

第1章不止定义了一个求值器, 实际上定义了两个. 从理想来说, 这两个定义应该引入的是相同的函数. 也就是说, 这两个求值器对于相同的程序应该产生同样的结果. 证明这样一个声明将允许我们根据需要交换地使用这两个定义. 例如, 当与一个数学老师争辩时, 我们可以使用

{eval}_{r}^{=_{r}}

来刻画程序执行泛化了七年级代数. 而当与负责

B

编程语言实现的软件工程师讨论

B

的语义时, 或许我们应该使用

{eval}_{r}^{↠_{r}}

因此, 我们的第二个问题关心的是等式求值器

{eval}_{r}^{=_{r}}

和有向求值器

{eval}_{r}^{↠_{r}}

之间的关系. 更确切地说, 我们想要知道它们是否是相同的函数:

{eval}_{r}^{↠_{r}} = {eval}_{r}^{=_{r}}

若将函数视为序对的集合, 那么问题就变成了这两个集合是否包含相同的元素:

自然地, "有定义"这个表达暗示了另外一个问题, 即是否求值器对于所有可能的输入都产生一个输出. 这个陈述有一个直接的数学表达, 即

第2.2节作为定理的回答

既然我们已经理解了关于编程语言的句法和语义我们所能提问的最简单问题, 那么其回答显然应该是关于相应数学模型的定理. 我们的第一个定理是在陈述

{eval}_{r}^{=_{r}}

是一个(部分)函数.

从证明

{eval}_{r}^{=_{r}}

的定理开始, 我们遵循历史路线, 首先建立了等式演算的一致性. 一旦我们证明了这两个定义描述了相同的关系, 那么我们就知道

{eval}_{r}^{↠_{r}}

也是一个函数. 同样根据传统, 在显然的时候我们去掉了定理中的量词前缀 (对于所有, 存在), 并且我们使用函数式记号来表达结果存在且是一个特定的值.

证明2.1. 为了证明该定理, 我们假设对于某

B_{0}, R_{1}, R_{2}

有

{eval}_{r}^{=_{r}} (B_{0}) = R_{1}

且

{eval}_{r}^{=_{r}} (B_{0}) = R_{2}

. 基于假设, 现在我们试图证明

R_{1} = R_{2}

. 根据

{eval}_{r}^{=_{r}}

的定义, 我们知道

B_{0} =_{r} R_{1}

且

B_{0} =_{r} R_{2}

. 注意一下, 这里是

=_{r}

而不是

=

. 因为(根据定义)

=_{r}

是一个等价关系,

R_{1} =_{r} R_{2}

. 为了到达我们想要的结果

R_{1} = R_{2}

, 即

R_{1}

和

R_{2}

是等同的, 我们必须研究这个等价关系的性质和计算的性质. (未完待续)

◻

前述证明的最后论证要求我们研究对于

M, N \in B

而言的

M =_{r} N

的证明 (或者说证明树) 的形状. 既然

=_{r}

是单步规约关系

\to_{r}

的自反, 对称, 传递闭包, 证明

M =_{r} N

的计算包含有一系列两个方向上的这样的单步规约:

M \to L_{1} \to L_{2} \leftarrow L_{3} \to L_{4} \leftarrow \dots \leftarrow L_{5} \leftarrow N

[译注: 原谅我将本来二维的图片用这样的单行的数学符号表达, 但是图片的意图应该清晰地传达了.] 在这张图片里, 每个表达式

L_{i} \in B

而每个箭头都表示序列中的相邻项之间的一个

\to_{r}

关系. 形式地,

L_{i} \to L_{j}

与

L_{i} \to_{r} L_{j}

相对应.

来源于这张图片的关键性的洞察在于或许可以重塑这个计算, 使得所有的规约步骤都是从

M

到某个

L

以及从

N

到相同的

L

. 换言之, 如果

M =_{r} N

, 那么存在一个表达式

L

满足

M ↠_{r} L

且

N ↠_{r} L

M \to • \to • \to \dots \to L \leftarrow \dots \leftarrow • \leftarrow • \leftarrow N

如果我们能够证明对于两个等价的项总是存在这样一个

L

, 那么一致性的证明就结束了.

证明2.1. (剩下的证明) 回忆一下, 我们有

R_{1} =_{r} R_{2}

根据(尚未证明的)声明, 必然存在表达式

L

满足

R_{1} ↠_{r} L 且 R_{2} ↠_{r} L

但是,

R

的元素仅有

t

和

f

, 它们不可能被规约为除了自身以外的任何其他表达式 [译注: 严格说来, 这也需要证明, 但是使用简单的结构归纳即可], 因此

L = R_{1}

且

L = R_{2}

, 这意味着

R_{1} = R_{2}

◻

根据前面这样的推理, 我们将

{eval}_{r}^{=_{r}}

的一致性证明转换为了关于证明树的形状的声明, 即建立

M =_{r} N

之后我们能够重塑它的证明树. 这个关键性的洞察应该归功于Church和Rosser, 它们运用这个想法分析了被称为

λ

演算的语言的一致性 (这是下一章的主题). 据此, 这样的引理以他们的名字命名.

证明2.2. 既然给定了

M =_{r} N

, 以及

=_{r}

的定义归纳性地扩展

↠_{r}

为其对称传递闭包, 我们根据

M =_{r} N

的推导的结构 (也就是其证明树的结构) 上的归纳来证明该引理:

基本情形:
- $M ↠_{r} N$ 情形
  令 $L = N$ , 然后声明成立.
归纳情形:
- $M =_{r} N$ 因为 $N =_{r} M$ 情形
  根据归纳, 存在 $N =_{r} M$ 的一个 $L$ , 此即我们想要的 $L$ .
- $M =_{r} N$ 因为 $M =_{r} L_{0}$ 且 $L_{0} =_{r} N$ 情形
  根据归纳, 存在 $L_{1}$ 满足 $M ↠_{r} L_{1}$ 且 $L_{0} ↠_{r} L_{1}$ . 同样根据归纳, 存在 $L_{2}$ 满足 $N ↠_{r} L_{2}$ 且 $L_{0} ↠_{r} L_{2}$ . 用图像表示的话, 我们有:现在假设每当 $L_{0}$ 可以被规约为 $L_{1}$ 和 $L_{2}$ 时, 存在某个表达式 $L_{3}$ 满足 $L_{1} ↠_{r} L_{3}$ 且 $L_{2} ↠_{r} L_{3}$ , 那么我们想要证明的声明的确成立, 因为 $M ↠_{r} L_{3}$ 且 $N ↠_{r} L_{3}$ .

◻

又一次, 我们基于 (modulo) 另外一个关于规约系统的声明的证明完成了证明. 更确切地说, 我们假定如果遇到了左边的情况, 那么可以找到一个项

L^{'} \in B

使得我们能够构造右边的情况:这个性质被称为菱形性质, 因为这张图片需要"规约分支"能够被补全为菱形的形状. 当规约概念 (例如

r

) 的兼容闭包的自反传递闭包满足这样的性质时, 其被称为Church-Rosser的.

既然

L ↠_{r} M

由一系列

\to_{r}

证明步骤构成, 那么检查后者是否也满足菱形性质是很自然的事情. 如果的确如此, 那么我们可以将

\to_{r}

的小菱形组合起来获得

↠_{r}

的大菱形. 尽管菱形性质对于

\to_{r}

并不那么成立, 一个足够强的性质的确可以满足.

引理2.4. [ $\to_{r}$ 的类菱形性质]: 如果

L \to_{r} M

且

L \to_{r} N

对于

M \neq N

成立, 那么以下三个条件恰有一条可以满足:

$M \to_{r} N$ ;
$N \to_{r} M$ ;
存在 $L^{'}$ 使得 $M \to_{r} L^{'}$ 且 $N \to_{r} L^{'}$ .

换句话说, "规约分支"可以被补全为菱形, 或者存在"三角形"风格的补全方式.

证明2.4. 为了证明这条引理, 我们回忆一下

\to_{r}

被归纳性地定义为

r

的兼容闭包. 因此, 自然的处理方式为假定

L \to_{r} M

并于证明的结构上施行结构归纳:

基本情形:
- $L r M$ 情形
  根据r的定义, 存在两种子情形.
  - $L = (f • B_{0})$ 且 $M = B_{0}$ 情形
  - $L = (t • B_{0})$ 且 $M = t$ 情形
对于归纳情形, 不失一般性, 假定⟨L,N⟩∉r, 否则可以交换N和M.

◻

第3章

λ

演算

第3.1节函数和

λ

演算

λ

演算的句法提供了一种简单而规整的方法来待应用的函数, 抑或是作为其他函数的输入和输出的函数. 在

λ

演算之中, 对于这种函数的刻画专注于从参数到结果的规则, 而忽略了对于函数的命名, 以及其定义域和陪域. 例如, 一位数学家会将某个集合

A

上的恒等函数写成是

f : {\begin{matrix} A & \to & A \\ x & \mapsto & x \end{matrix}

而若用

λ

演算的句法的话, 则为

第3.2节

λ

演算: 句法和规约

第3.3节编码布尔

第3.4节编码序对

第3.5节编码数字

第3.6节编码和错误

第3.7节递归

第3.8节一致性和正规形式

第3.9节正规形式和规约策略

第3.10节历史

第4章 ISWIM

在1950年代晚期和1960年代早期, 人们发现编程语言和

λ

演算的诸多方面之间存在联系. 这里的动机是多样的, 有的只是想要刻画Algol 60的语义, 而有的是试图通过已经得到良好理解的数学系统来理解整个编程语言领域的面貌. 实际上, 人们希望学会如何系统设计编程语言.

Landin是这群研究者之中的新星. 他设计了一种被称为ISWIM的基于

λ

演算的语言, 并探索了其通过抽象或者说虚拟机器的应用和实现. 不严格地说, ISWIM几乎是一个函数式编程语言, Scheme编程语言是其最近的亲戚. [译注: 当然, 有的人可能认为Standard ML之类的语言比Scheme更加接近于ISWIM. 另外, ISWIM其实是一类语言, 而不是一个语言.]

虽然人们欣赏ISWIM的表达力并将其当作灵感的源泉, 人们也意识到ISWIM和

λ

演算之间的关系并不那么直接. Plotkin最终设计了

λ

演算的一个变种, 其与ISWIM有着直接而自然的对应关系. 他也表明了, 这种对应是一般性的原则. 他将这原则具体化为了ISWIM的两个变种: call-by-name和call-by-value.

这一章和接下来的一章里我们呈现了ISWIM, 其演算, 以及ISWIM和演算之间的关系. 具体来说, 本章呈现了ISWIM的句法和ISWIM的"算术"系统. 这包含一个求值器的定义以及对于这个求值器所定义的最广泛等式系统的探索. 接下来的一章展现了

λ

演算的一个元定理是如何自然地定义了ISWIM的一个高层次的抽象机器的.

第4.1节 ISWIM表达式

ISWIM是一族编程语言, 根据字面常量和原始运算符而有所不同. ISWIM族的每一语言都扩展了

λ

演算的句法以基本常量的集合

b

和一族多元函数

o^{n}

这里的

o^{n}

里的

n

不是确定的, 其代表了原始运算符的参数数目 (元数), 并且我们额外限制这个应用的实际参数的数目必须等于相应的原始运算符的元数.

为了明确起见, 我们使用

\begin{matrix} b & = & {⌈ n ⌉ | n \in ℤ} \\ o^{1} & = & {add1, sub1, iszero} \\ o^{2} & = & {+, -, ⁎, ↑} \end{matrix}

其中

⌈ n ⌉

是表示数字

n

的numeral.

FV

和

\cdot [\cdot \leftarrow \cdot]

可以自然地扩展至新的句法上来.

\begin{matrix} FV (b) & = & \emptyset \\ FV (X) & = & {X} \\ FV ((λ X . M)) & = & FV (M) - {X} \\ FV ((M_{1} M_{2})) & = & FV (M_{1}) \cup FV (M_{2}) \\ FV ((o^{n} M_{1} \dots M_{n})) & = & FV (M_{1}) \cup \dots \cup FV (M_{n}) \end{matrix}

\begin{matrix} b [X \leftarrow M] & = & b \\ X_{1} [X_{1} \leftarrow M] & = & M \\ X_{2} [X_{1} \leftarrow M] & = & X_{2}, 其中 X_{1} \neq X_{2} \\ (λ X_{1} . M_{1}) [X_{1} \leftarrow M_{2}] & = & (λ X_{1} . M_{1}) \\ (λ X_{1} . M_{1}) [X_{2} \leftarrow M_{2}] & = & (λ X_{3} . M_{1} [X_{1} \leftarrow X_{3}] [X_{2} \leftarrow M_{2}]) \\ 其中 \begin{matrix} X_{1} & \neq & X_{2} \\ X_{3} & \notin & FV ((λ X_{1} . M_{1})) \\ X_{3} & \notin & FV (M_{2}) \end{matrix} \\ (M_{1} M_{2}) [X \leftarrow M_{3}] & = & (M_{1} [X \leftarrow M_{3}] M_{2} [X \leftarrow M_{3}]) \\ (o^{n} M_{1} \dots M_{n}) [X \leftarrow M] & = & (o^{n} M_{1} [X \leftarrow M] \dots M_{n} [X \leftarrow M]) \end{matrix}

第4.2节使用ISWIM进行计算

受到Algol 60的call-by-value参数传递机制的启发, Landin以类似的方式设计了ISWIM的函数. 也就是说, 在ISWIM之中, 一个函数应用在函数取得控制之前对于其实际参数求值. 这么做可以消除在函数体中对于一个参数多次求值或者追踪一个参数是否已经被求值过了的开销. 这也排除了纯粹

λ

演算中的一些incongruities, 例如表达式

((λ x . ⌈ 1 ⌉) (sub1 (λ y . (λ x . y))))

将

sub1

应用于一个并非numeral的东西 [译注: 从句法上说], 会被call-by-value的参数传递机制发现. 而在纯粹

λ

演算之中, 这种错误应用 (mis-application) 因为可以直接施行

β

规约而不会被发现.

因为ISWIM的函数只接受被求值了的参数, 那么我们必须首先规定何谓值. 从直觉上说, 值是对其求值可以立即知道结果的项. [译注: 一般我们在操作语义之中采用这种观点, 在其他场合, 值还有另外的含义.] 或者说, 值是任意的表达式在规约过程之中的目的地. 我们定义值的集合如下:

\begin{array}{rcl} V, U, W & = & b \\ | & X \\ | & (λ X . M) \end{array}

基本的常量当然是值,

λ

抽象也是值, 不论其体的形状如何. 因此, Landin将函数作为第一级对象的想法引入了编程语言的研究之中. [译注: 至于第一级对象这个想法或者说术语, 最早提出者应该是Christopher Strachey, 他也算是指称语义学的奠基人之一.]

应用不可能是一个值, 因为它就像刻画计算的发动机一样. 变量也是值, 不过这值得额外的解释.

λ

演算中的变量有且只有一种目的: 作为形式参数 (formal argument) 或者说parameter. 对于一个程序员而言, parameter的作用在于为函数的实际参数充当占位符号 (place holder). 既然ISWIM的函数只能消化值, 那么变量就总是代表值. 因此, 我们暂时也将变量看成是值. 第4.7节回顾了这个决定.

基于对于值的刻画, 现在我们可以定义ISWIM的基本规约概念.

\begin{matrix} ((λ X . M) V) & β_{v} & M [X \leftarrow V] \end{matrix}

这个关系有别于

β

, 因为参数必须是

V

的成员. 在ISWIM中, 你不能将任意的项替换进函数的体里.

限制参数必须是一个值迫使参数表达式的规约在对于函数应用求值之前进行. 例如,

((λ X . ⌈ 1 ⌉) (sub1 (λ y . y)))

就不能被规约至

⌈ 1 ⌉

, 因为

(sub1 (λ y . y)) \notin V

除了函数应用, 计算ISWIM的系统还必须考虑原始运算. 既然ISWIM是随着常量集和原始运算符集的改变而变化的一族语言, 那么对于这些集合我们需要一个足够一般的规约概念, 因而我们引入了一个部分

δ

函数:

δ : o^{n} \times b \times \dots \times b \to V

也就是说,

δ

将

o^{n}

的元素和

n

个基本常量映射至一个值. 添加

δ

至演算引入了第二种规约概念.

对于我们之前约定好了的常量和运算符, 我们选择了以下具体的

δ

函数.

\begin{matrix} δ (add1, ⌈ m ⌉) & = & ⌈ m + 1 ⌉ \\ δ (sub1, ⌈ m ⌉) & = & ⌈ m - 1 ⌉ \\ δ (iszero, ⌈ 0 ⌉) & = & (λ x . (λ y . x)) \\ δ (iszero, ⌈ n ⌉) & = & (λ x . (λ y . y)) & , n \neq 0 \\ δ (+, ⌈ m ⌉, ⌈ n ⌉) & = & ⌈ m + n ⌉ \\ δ (-, ⌈ m ⌉, ⌈ n ⌉) & = & ⌈ m - n ⌉ \\ δ (⁎, ⌈ m ⌉, ⌈ n ⌉) & = & ⌈ m \cdot n ⌉ \\ δ (↑, ⌈ m ⌉, ⌈ n ⌉) & = & ⌈ m^{n} ⌉ \end{matrix}

第4.3节

α

η

和商

第5章抽象句法机器

ISWIM求值器的定义是优雅的, 但是难于实现. 为了确定一个程序的结果, 程序员可以自由地应用等式系统的规则以任意的顺序, 以任意的方向, 在程序的任意位置. 然而, 这种灵活性并非将求值器实现为(元)程序的良好基础. 根据一致性定理,

第6章抽象寄存器机器

第6.1节 CC机器

前一章的句法机器的每个求值循环中都需要执行三个步骤. 首先, 其需要判断程序是否是一个值; 如果是的话, 那么机器就停止了. 其次, 或者说程序并非一个值, 那么机器会将程序分成一个求值上下文

E

和一个应用

(U V)

或者

(o^{n} V_{1} \dots V_{n})

. 最后, 如果这个应用是一个

β_{v}

或者

δ

可规约表达式, 那么机器会构造contractum

M

, 然后填充求值上下文

E

以

M

. 这一步的结果是下一个机器状态, 于是求值循环又重新再来.

这个机器显见的低效之处在于反复将程序分成一个求值上下文和一个可规约表达式.

语义工程和PLT Redex

第1部分规约语义

第1章语义via句法

第1.1节定义集合

第1.2节关系

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

第1.4节语义via规约

第1.5节上下文中的规约

第1.6节求值函数

第1.7节记号总结

第2章分析句法性的语义

第2.1节从问题到数学声明

第2.2节作为定理的回答

第3章 $λ$ 演算

第3.1节函数和 $λ$ 演算

第3.2节 $λ$ 演算: 句法和规约

第3.3节编码布尔

第3.4节编码序对

第3.5节编码数字

第3.6节编码和错误

第3.7节递归

第3.8节一致性和正规形式

第3.9节正规形式和规约策略

第3.10节历史

第4章 ISWIM

第4.1节 ISWIM表达式

第4.2节使用ISWIM进行计算

第4.3节 $α$ , $η$ 和商

第5章抽象句法机器

第6章抽象寄存器机器

第6.1节 CC机器

第6.2节 SCC机器

第6.3节 CK机器

第6.4节 CEK机器

第6.5节历史

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

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

第9章状态: 命令式赋值

第10章简单类型ISWIM

语义工程和PLT Redex

第1部分 规约语义

第1章 语义via句法

第1.1节 定义集合

第1.2节 关系

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

第1.4节 语义via规约

第1.5节 上下文中的规约

第1.6节 求值函数

第1.7节 记号总结

第2章 分析句法性的语义

第2.1节 从问题到数学声明

第2.2节 作为定理的回答

第3章 λ演算

第3.1节 函数和λ演算

第3.2节 λ演算: 句法和规约

第3.3节 编码布尔

第3.4节 编码序对

第3.5节 编码数字

第3.6节 编码和错误

第3.7节 递归

第3.8节 一致性和正规形式

第3.9节 正规形式和规约策略

第3.10节 历史

第4章 ISWIM

第4.1节 ISWIM表达式

第4.2节 使用ISWIM进行计算

第4.3节 α, η和商

第5章 抽象句法机器

第6章 抽象寄存器机器

第6.1节 CC机器

第6.2节 SCC机器

第6.3节 CK机器

第6.4节 CEK机器

第6.5节 历史

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

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

第9章 状态: 命令式赋值

第10章 简单类型ISWIM

第1部分规约语义

第1章语义via句法

第1.1节定义集合

第1.2节关系

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

第1.4节语义via规约

第1.5节上下文中的规约

第1.6节求值函数

第1.7节记号总结

第2章分析句法性的语义

第2.1节从问题到数学声明

第2.2节作为定理的回答

第3章 $λ$ 演算

第3.1节函数和 $λ$ 演算

第3.2节 $λ$ 演算: 句法和规约

第3.3节编码布尔

第3.4节编码序对

第3.5节编码数字

第3.6节编码和错误

第3.7节递归

第3.8节一致性和正规形式

第3.9节正规形式和规约策略

第3.10节历史

第4.2节使用ISWIM进行计算

第4.3节 $α$ , $η$ 和商

第5章抽象句法机器

第6章抽象寄存器机器

第6.5节历史

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

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

第9章状态: 命令式赋值

第10章简单类型ISWIM