Header

译自 Elementary Tutorial on Normalization-by-Evaluation。除非特殊声明，下文中「我」指原文作者 Oleg Kiselyov。

导言

本教程的初衷是为本科生提供一个五分钟快速入门通过求值进行归一（Normalization by Evaluation, NbE）技术的教程。因为是入门教程，所以只要求读者拥有小学或以上的数学背景知识，也无需拥有任何编程经验，读者可以一边在海边玩贝壳游戏一边进行学习。游戏的规则很基础，但游戏本身并不总是简单。在海边玩贝壳游戏可能是一个很好的契机，让你认识到：计算、规约、归一，以及证明游戏规则具有推进性和保持性的过程，都不过是一种玩弄符号的游戏。

但总有人试图超越符号的表象，将其视为真实事物的投影；在看似随意的规则背后寻找直觉，试图把握无脑游戏的意义。这样的人无疑会发现 NbE——就像人们在历史上多次重复发现的那样，本教程就是要指导读者重新发现 NbE。

游戏设置

让我们从一个游戏/谜题开始，它是许多小学练习的简化版本。玩这个游戏需要用到袋子、贝壳和橡皮筋。

  • 袋子可以是空的，也可能内装有一个或多个贝壳

  • 贝壳是一种游戏代币，彼此之间不作区别

  • 「束」可以单指一个袋子，也可以通过用橡皮筋把另外两「束」扎起来作为一个新的束

我们将贝壳记作 #。在游戏中，两个「装有三个贝壳的袋子」可以视作同一个事物，并统一记作 [###]。而束的记法则是：把组成的两个束并排写在一起，中间用逗号隔开，然后两边加上圆括号。[##]，([##],[])，([##],([###],[#])) 都是合法的束，另外第一个例子也可以视为一个袋子。让我们较真一点：其他任何形式的记号都不是束（或者袋） ，像 [[]] 以及 (#, [&]) 就不是束，因为他们不是由方括号所包围的零个或多个 # 组成，也不是由圆括号包围的成对的方括号组成。

游戏的玩法是：给定一个束，找出一个「等价」或者说「相等」但更「简单」的束，并最终找到最简单的束——许多游戏甚至是学校里的练习题本质上都如此。例如，我们会得到一个形如 $5x-3=3x+7$ 的束，然后被要求找出与其等价且最简单的（在本例中，这样的束是 $x=5$）。

在开始游戏前，我们必须搞清楚两个束怎么才算「相等」，以及什么是「更简单」。

引用资料

我们的游戏实际上是 B. Pierce 所著的《Types and Programming Languages》中第 3 章内容的变体。这本书的本质是一些逐渐复杂化的玩弄符号的游戏的集合——尽管它自己没有如此声称。

相等

如何制定游戏规则，即定义束的「同一性」或者说「相等」完全取决于我们自己。我们可以一手指一个束然后声明它们相等，也可以把两个束分列 ~ 符号的两侧然后声明它们相等，如：([#],([##],[###])) ~ ([##],([#],[###]))。我们可能会声明很多类似这样的相等性，因此需要一种更简洁的写法。比如下面这样

  • 首先，声明 ([], [S]) 等于 [S]，其中 S 代表包括 0 在内的任意数量的贝壳。

  • 其次声明 ([#S],([T],[U])) ~ ([S],([#T],[U]))，其中 S、T 和 U 均代表任意数量的贝壳，而 #S 代表比 S 再多一个（#T 同理）。

  • 最后声明：在由两个袋组成的束中，袋的顺序并不重要。

这样就可以用较少的文字写出这一系列声明

(Ax0)  ([],[S]) ~ [S]
(Ax1)  ([#S],([T],[U])) ~ ([S],([#T],[U]))
(AxS)  ([S],[T]) ~ ([T],[S])

为了便于后面引用，我们给这些声明取名叫 (Ax0)、(Ax1) 和 (AxS) ，它们三个的组合则称为 (Ax01S)。这些都是所谓模板式声明（schematic declaration）：声明中的变量（variable）S、T 和 U 都代表任意数量的贝壳。使用变量简洁地代指（无限组）声明，就好比在自然语言中使用不定式和代词来陈述（无限多种）特定情况。举个例子，(Ax0) 可以用自然语言描述为：「一个任意的袋子和一个空袋组成的束等价于原来的袋子」。

我们还发现：一、声明任何一束等于它自己也很自然；二、在这些声明之中，声明的束的左右顺序也无关紧要。因此，我们采用下列规则（统称为 (Deduc)）扩充上述的声明集，其中，A、B 和 C 代表任意的束

(Refl)  A ~ A
(Symm)  If A ~ B then B ~ A
(Trans) If A ~ B and B ~ C then A ~ C
(Cong)  If A ~ B then (A,C) ~ (B,C) and (C,A) ~ (C,B)

举个例子：规则 (Trans) 指出，如果已经（通过应用声明集 (Ax01S) 和规则 (Deduc)）发现 A 等价于 B 且 B 等价于 C，那么可以声明 A 等价于 C。顺带一提，我们也可以不像上面一样通过逐一列举 (Deduc) 规则集来声明这些规则，而是称上述等式是关于相等性声明 (Ax01S) 的自反性（reflexive）、对称性（symmetric）、传递性（transitive）以及兼容性（compatible）的闭包（closure），即 (Ax01S) 的最小合同（smallest congruence）闭包。或者更简短地定义为：上述规则是 (Ax01S) 的一个（有限）等式理论（equational theory），下文也使用这个名称。

有的读者可能会注意到并质疑：「我们凭什么说 (Refl) 自然呢？」一个稍显敷衍的回答是：「根据经验，没有 (Deduc) 的游戏很无趣。」不过，读者可能已经察觉到：游戏不像我们（或者说语法方法论（syntactic approach）的支持者）所假装的那么随意或无脑。请保持这个想法。

我们可以随心所欲制定想要的游戏规则，尤其是像 (Ax01S) 这样的基础相等声明。相等真的那么随意吗？某些相等声明会比其他的相等声明更「错」或者更「差」吗？玩弄符号游戏的过程中不存在内在的「真」或「善」，你当然可以随意设定相等规则，不过有一种情况值得注意。

假设我们在 (Ax01S) 等式理论中再添加一个声明：

(AxU) ([#],[]) ~ ([],[])

一方面，通过 (Ax0) 可得 ([],[]) ~ []；而另一方面，通过 (AxS) 可得 ([#],[]) 等于 ([],[#]) 并且根据 (Ax0) 等于 [#]；那么根据 (Trans)，我们就得到了 [#] ~ []。根据上述步骤可以得出结论：所有的袋都相等。最终我们可以得出所有的束也都相等。

练习 1. 证明在等式理论 (Ax01S,AxU) 中所有的束都等于 []，因此所有的束都相等。可以从证明 [##] ~ [] 开始。

练习 2. 证明在等式理论 (Ax01S) 中：如果我们假设所有的袋都相等，那么所有的束都相等。

「(Ax01S,AxU) 中所有事物都相等」这一事实并不能用作批判该理论的论据：毕竟在游戏的层面上，没有好与坏之分，这是我们自己的游戏，我们可以为所欲为。然而，我们下意识地产生了一种感觉：退化的等式理论不是很有用，也不是很有趣。感想还是稍后再谈，现在我们要指出一个评价等式理论的质量的标准，即非平凡性（non-triviality）。

定义. 在非平凡的等式理论中，存在两个不相等的事物。

练习 3. 指出一个能证明 (Ax01S) 具有非平凡性的例子。

练习 4. 考虑等式理论 (Empty)，该理论在除了 (Deduc) 之外没有任何等价性声明。某种意义上，这个等式理论和平凡的 (Ax01S,AxU) 相反，是在哪种意义上？

练习 5. 证明在等式理论 (Ax01S) 中：对于任意的束 A 和 B（不只是袋），我们都有 (A,B) ~ (B,A)。稍后我们会再次讨论这个练习，但读者确实值得现在一试。

引用资料

在我们的游戏中，袋子里装的是贝壳，不是变量，束中也没有变量。变量只出现在相等性声明中，我们把变量用作一种修辞手段，从而简洁地陈述无限多个相等声明——有点类似于自然语言中的不定式。然而，在普适代数（universal algebra）领域的研究中，人们习惯于在项（term）的语法定义中加入变量。这种情况则需要在 (Deduc) 中加入一条规则：变量可以被任意的项替换（即实例化）。这条规则通常与 (Cong) 结合形成所谓替换（substitution）规则：用两个相等的项分别替换某个项中同一个变量，得到的两个新项相等。

必胜策略

在定义了「相等」之后，我们还要定义什么是「更简单」。定义「简单」很简单：对两个相等的束，用橡皮筋更少的那个就更简单。现在可以开始游戏了，谁能找到与任意给定的一个束相等且最简单的的束？

首先想到的一种策略是：对于给定的束，找出所有与其相等的束，然后选择其中最简单的。更具体来说，我们先拿一个大盒子，把最初的束放在里面，然后重复以下步骤：

  • 从盒子随机取一束，「复制」一份，然后把原来的束放回盒子。

  • 观察这个束或它的子束是否匹配 (Ax01S) 中的声明的左侧或右侧，如果匹配，那么用对应声明的另一侧替换匹配的部分。

  • 如果盒子里面还没有替换后的束，那么就把它放进盒子。

举个例子：假设我们手中有 ([##],[#])，这个束的子束 [#] 匹配规则 (Ax0) 即 ([],[#]) ~ [#] 的右侧。那么将其替换成对应的左侧得到 ([##],([],[#]))。最后把替换后的新束放进盒子。

这个琐碎的过程有一个非平凡的性质：根据规则集 (Ax01S) 和 (Deduc)，这个过程会且仅会生成出所有与最开始的束相等的束。事实上，正如 (Refl) 所描述的，最开始的束也在盒子里。因此 (Deduc) 规则集确实很自然，不是吗？读者请尝试说服自己：重复上述步骤一定次数后，盒子里会且仅会放有所有与原束相等的束。这是否很容易理解？

不难发现这种做法的弊端：这个过程会一直持续下去。上面所展示的，把 (Ax0) 的右侧替换为左侧的做法总是会把一个袋替换成束。我们不但停不下来，还会不断生成越来越复杂的束，与目标背道而驰。

仔细想想，并非所有的和某束相等的束我们都关心。我们只关心那些能引导我们实现目标的：比如一个更简单的束。因此生成等价束的过程应当更有针对性。我们刚才从右到左运用 (Ax01S) 生成束，但我们也可以从左到右的应用这条规则：从右到左的应用会加多一条橡皮筋，而从左到右的应用会减少一条橡皮筋，即简化了我们的束。但是，如何确定 (Ax1) 和 (AxS) 的应用方向，尤其在我们无法明显看出 (AxS) 是否简化了任何东西的情况下？这也引出了第二个问题：对于 (([#],[#]),([#],[#])) 这个束，我们无法按指定的方向应用 (Ax0)，而且也无法从任意方向应用 (Ax1) 和 (AxS)。我们就会得出结论：这是最简单的束——然后发现自己输掉了游戏。

练习 6. 你能找出和 (([#],[#]),([#],[#])) 相等的束吗？你用了哪些等式来证明相等？

下面是一个更详细的建议：

  • 按照上面确立的的方向（从左到右）应用 (Ax0)

  • 从左到右方向应用 (Ax1)

  • 将 (Symm) 和 (Trans) 应用到 (Ax0) 和 (AxS) 得到 ([S],[]) ~ [S]，然后从左右两个方向应用得到的等式

因此我们得到了以下用于生成新束的规则：

(R0)  ([],[S]) -> [S]
(R1)  ([#S],([T],[U])) -> ([S],([#T],[U]))
(R0S) [S]      -> ([S],[])
(RS0) ([S],[]) -> [S]

(R0)、(R1)、(R0S) 以及 (RS0) 也是为了方便引用取的名字，总称为 (R01S)。用 -> 而非 ~ 是为了确立这些规则的应用方向。因此，当给定一个束时，先找出一个符合上述规则的左侧的子束（变量用相应数量的贝壳替换），然后用对应的右侧替换之。尝试替换的过程中可能会有很多选择：例如，对于 ([#],([],[]))，下面的任意选择都是可行的。

  • 对整个束应用 (R1)（其中 S、T 和 U 代表 0 个贝壳）得到 ([],([#],[]))

  • 对子束 ([],[]) 应用 (R0) 或 (RS0) 得到 ([#],[])

  • 对任意的袋应用 (R0S) 从而得到 (([#],[]),([],[])) 或 ([#],(([],[]), [])) 或 ([#],([],([],[])))

现在再来看看我们能否简化之前的练习问题中的束。下面展示一部分简化过程中生成的束以及对应使用的规则：

(([#],[#]),([#],[#]))
-> (([#],[#]),([#],([#],[])))           由应用 (R0S) 得到
-> (([#],[#]),([],([##],[])))           由应用 (R1) 得到
-> (([#],[#]),([##],[]))                由应用 (R0) 得到
-> (([#],[#]),[##])                     由应用 (RS0) 得到

练习 7. 完成上面的例子并生成更简单的束。你能得到的最简单的的束是什么？

因为规则 (R01S) 本质上相当于我们提出的相等性声明中的一部分特定情况，所以应用这些规则肯定会产生在原来的等式理论中相等的束。在生成更简单的束方面，(R0S) 是一个例外：应用这一规则会生成一个更复杂的束，而且你可以反复应用这一规则。因此我们提出的规则体系广泛地说是不会停机的。

但是，在应用规则时存在一种选择方法：对于任意的束，这种方法都能通过有限的步骤得到最简单的等价束，我们称其为「必胜策略」。你能制定出这种策略吗？你能让自己相信这种策略总是有效吗？

练习 8. 回顾前面的练习「证明在等式理论 (Ax01S) 中：如果我们假设所有的袋都相等，那么所有的束都相等。」现在来看是不是容易多了？

练习 9. 你能想出另一种使用规则 (R01S) 的必胜策略吗？或者，你能找到另一种生成束的规则系统，从而使得无论如何应用这些规则，最终都会产生最简单的等价束？

练习 10. 从文章最一开始，我们就在讨论所谓「最简单的的等价束」。但一般来说我们不能保证一定存在这种束：与原束等价，且在定义意义上符合「最简单」的束可以有很多个（我们的游戏中，没有橡皮筋的就是最简单的）。读者是否能证明：我们的游戏中必然存在最简单的的束，即对于游戏中任意的束，都有唯一对应的最简单的束？

引用资料

从技术上，这些等式或说规则被称作约简规则（reduction）。而根据这些规则改写子项从而产生新的束（或者说新的项）的过程则称作项重写（term rewriting）。在理想情况下，无论我们如何选择策略，把对应的规则应用到适用的子项上，最终都能找到一个无法适用任何规则的项，即范式（normal form）。这也意味着所有的游戏策略最终都会获胜（如果我们的游戏目标是得到范式的话）。

上文提出的 (R01S) 系统并不理想：某些策略（如何应用规则的选择）会一直持续下去。此外，严格来说最简单的束也不是范式，因为你可以对其应用 (R0S)。在编程语言理论中很多的这种游戏里，我们的目标也不是要得到范式：通常有一个预先设定好的目标，根据这个目标来判断规约的结果。下一节我们将讨论这一切的「意义」——顺带一提，NbE 也适用于一些不太理想的系统，比如我们的系统。

通过组合 (Ax01S) 中的相等性声明，我们得到了约简规则 (R01S)。Knuth-Bendix 补全算法（Knuth-Bendix completion algorithm）正是这样一种将一组相等声明转换为理想的项重写系统的算法。除了这些相等性声明之外，项的「规约序」（即以「简单性」这一标准为项定义的排序）也是该算法的一个参数，该算法也不总能成功。这里我们虽然没有严格遵循这一算法，但也已说明了其关键步骤：确立方向、组合相等声明、然后丢弃一部分相等声明。

另一方面，与其从相等声明开始尝试补全出约简规则，我们可以反过来从约简规则开始补全相等声明：这样我们就可以把等式理论定义为包含约简规则的最小合同闭包——编程语言理论研究中常常这么做。

在 Prolog/Datalog 中，「生成所有与原始束相等的束，然后从中选择具有某些性质的束」这一过程称作自下而上的求值（bottom-up evaluation）。我们应当致力于只生成能让我们更接近目标的东西，这逻辑编程中通常称之为魔法集合重写（magic-set rewriting）。

这一切意味着什么？

我们尽力把这一切伪装为无脑摆弄袋子和贝壳的游戏，但偶尔也会怀疑我们制定的游戏规则是否「自然」、是否「良好」、是否「有趣」。有的人热衷于按照自己的价值观和直觉对事物进行类比；有的人把意义视为纯粹的「形而上学」并不屑一顾；而有的人则认为：「意义」也可以像其他数学理论一样被认真对待，形式化并严格使用。

在讨论装有贝壳的袋子时，我们很难不去想袋子中贝壳的具体数量，用这个数字在脑中给袋子「贴上标签」，并将其视作这个袋子的「意义」。同样，我们也可以用一束中所有袋子的贝壳的数量总和为这一束赋予意义。这是一个好的、有用的直觉吗？让我们来看看它是否兼容游戏的规则（等式理论）。

为了使讨论「意义」更精确，更简洁，我们需要引入一些记号：若 A 是一袋或一束，{A} 表示这个袋或束的意义，在本例中就是其中的贝壳总数。它有以下计算公式：

{ [] }    = 0
{ [#S] }  = 1 + { [S] }
{ (A,B) } = {A} + {B}

观察到：对于形如 (A,B) 的束，其意义仅由组成该束的 A 和 B 的意义决定，与 A 或 B 的形状、结构等其他性质无关。因此，意义是上下文无关的。举个例子：某束 ([##], ([###], [#])) 的意义是数字 6，无论它是单独作为一个束，还是作为另一个更大的束的构成部分，它的意义都是 6。我们为事物赋予意义的过程是模块化的，或严格来说「可组合的」。

现在我们来探求上面的相等性声明的意义，回顾规则 (Ax0): ([], [S]) ~ [S]，规则左侧的意义是 { ([], [S]) }，即 {[]} + {[S]}；经小学算术化简得到 {[S]}，即规则右侧部分的意义。当 (Ax0) 仅作为相等性声明时，它只是把两个束的记法分列在 ~ 的左右两侧，本身不存在真或假；而当我们把袋和束解释为数学时，(Ax0) 就意味着小学代数式 $0+x=x$，显然是一个真的等式。现在我们可以谈论何为真理了。

总之，对于 (Ax01S) 我们有以下解释：

$ \begin{align} \mathtt{(Ax0)} & & 0+x&=x & \\ \mathtt{(Ax1)} & & (1+x)+(y+z)&=x+((1+y)+z) & \\ \mathtt{(AxS)} & & x+y&=y+x & \\ \end{align} $

$x$，$y$，$z$ 是数字，它们分别代表袋子 [S]，[T]，[U] 的意义。这些式子同样是小学代数等式。

而对于 (Deduc) 有：

$ \begin{align} \mathtt{(Refl)} & & &⊢x=x & \\ \mathtt{(Symm)} & & x=y&⊢y=x & \\ \mathtt{(Trans)} & & (x=y)\wedge{}(y=z)&⊢ x=z & \\ \mathtt{(Cong)} & & x=y&⊢(x+z=y+z)\wedge{}(z+x=z+y) & \\ \end{align} $

这就是为何我们称 (Deduc) 规则集自然：它们都是关于数的相等性的真命题，事实上，也是关于普适相等性的真命题——反映了相等的基本直觉。

通过这些步骤为游戏中的袋或束赋予的意义（即自然数），和我们上面利用相等性声明所定义的一致。因此我们可以从技术上说：自然数以及把自然数作为「意义」赋予给游戏中和袋和束的方式是等式理论 (Ax01S) 的一个模型（model），我们将这个模型称为 (Nat01S)。因为 (Ax01S) 理论中的任何相等性声明都可以转换成 (Nat01S) 模型中的自然数的相等，所以当两个束在 (Ax01S) 中相等时，它们在 (Nat01S) 中对应的自然数也相等。由此可知：理论中相等的东西在「实践」（即在模型中）也相等。

那反过来，两个在 (Nat01S) 拥有相同意义，即对应的自然数相等的束在 (Ax01S) 中也相等吗？即如果 {A} = {B}，那么 A ~ B 是等式理论 (Ax01S) 的一个实例，或者是用 (Ax01S) 根据 (Deduc) 构造的组合吗？这看起来是一个有用、且相当有力的命题。那么它是真命题吗？如何证明它？

「在『实践』中相等的东西在理论中也相等」这一点在一般情况下很难证明。幸运的是，本文的例子中我们已经完成了这个艰巨的任务：我们已经发现了能「将任意束规约成对应等价束」的必胜策略（如何确切描述这一策略留作读者练习）。考虑两个具有相同意义的束 A 和 B：

  • 我们对 A 运用必胜策略从而得到 A'。

  • 回顾上文：「必胜策略」（即任意一种应用规约 (R01S) 的策略）必然会生成一个等价的束，因此有 A ~ A'。

  • 而对 B 应用必胜策略得到 B'，同上可得 B ~ B'。

  • 因为任何在理论中相等的东西，在理论的模型中都相等，所以有 {A} = {A'} 和 {B} = {B'}。

  • 又因为我们上面假设 {A'} = {B'}：即在模型 (R01S) 所赋予的意义中，袋 A' 和袋 B' 具有相同数量的贝壳，因此两个袋子完全一致。

  • 我们便可以得到 A ~ A' 以及 B ~ A'，并根据 (Symm) 和 (Trans) 最终得出结论 A ~ B。

上面证明的性质称为完备性（completeness），即 (Nat01S) 和 (Ax01S) 的相等概念完全重合。这个性质非常有用，因此被赋予了各种各样的名称，譬如：等式理论 (Ax01S) 是对于模型 (Nat01S) 的完备理论；(Ax01S) 对于 (Nat01S) 完备；(Ax01S) 是模型 (Nat01S) 的公理化（axiomization）。

练习 11. 证明在等式理论 (Ax01S) 中：对于任意束 A、B 和 C 都有 (A,(B,C)) ~ ((A,B),C)。

练习 12. 一个游戏可以有许多模型，使用什么模型则取决于我们对游戏的哪些方面感兴趣。下面是我们游戏的另一个模型：意义是布尔值 true 和 false，并按以下方式赋予给游戏中的元素：

{ [] }    = false
{ [#S] }  = not { [S] }
{ (A,B) } = xor {A} {B}

其中，not 代表布尔否定，xor 代表布尔异或。你要如何说服自己这也是 (Ax01S) 的一个模型？，(Ax01S) 对于这个模型完备吗？如果不是，应当向 (Ax01S) 添加什么从而使其对这个模型完备？

练习 13. 平凡的等式理论 (Ax01S,AxU) 的模型是什么？

练习 14. 下面是另一个模型：意义是整数，并按以下方式赋予给游戏中的元素：

{ [] }    = 0
{ [#] }   = 1
{ [##S] } = 2
{ (A,B) } = ({A} + {B}) mod 3

对于该模型完备的等式理论是什么？在该理论中，最简单的的束是什么？

通过求值进行归一

上面已经证明：等式理论 (Ax01S) 是一个对模型 (Nat01S) 完备的理论。这种完备性的一种应用是通过求值进行归一（Normalization by Evaluation, NbE）。考虑一个形如 (([#],[#]),([#],[#])) 的束。为了找到与之相等的最简束，我们可以运用上面所说的「必胜策略」——一般只需要很少的步骤就可以完成。而另一方面，我们也可以利用 (Nat01S) 模型找到这个束的意义：{(([#],[#]),([#],[#]))} = (1+1)+(1+1) = 4。然后运用简单的小学算术得到：有 4 个贝壳的袋 [####] 就是与原束相等的最简束。若 N 为一个自然数，令 !N 代表一个有 N 个贝壳的袋子 ，求任意束 A 的最简束的算法就是：!{A}。

NbE 是一种借助语义的力量赢得无脑游戏的方法。这就是对事物赋予「意义」的意义所在：意义可以将晦涩难懂的事物与熟悉的事物联系在一起。这样我们就可以依靠对数字等已有意义的对象的理解，利用我们的直觉与判断讨论真与善。

引用资料

下面用最通用的语言描述 NbE：为了对一系列对象组成的集合 $X$ 进行 NbE，我们要引入另一个意义集合 $M$，这两个集合之间有两个函数

$\mathrm{eval} : X→M \tag*{}\\ \mathrm{reify} : M→X \\ $ 集合 $M$ 应当有可（容易地）计算的相等性定义。之前的章节中，我们把 $\mathrm{eval}(x)$ 记作 {x}，$\mathrm{reify}(x)$ 记作 !x。它们应当满足以下自然的条件：$\mathrm{reify}$ 的定义域等于 $\mathrm{eval}$ 的值域（这样函数组合 $\mathrm{reify·eval}$ 才是良定义的），以及对于所有在 $\mathrm{reify}$ 定义域中的 $m$ 都有：$\mathrm{eval}(\mathrm{reify}(m))=m$。根据 NbE 的定义：对于集合 $X$ 中的任意元素 $x$ ，$x$ 的范式是 $\mathrm{reify}(\mathrm{eval}(x))$。

尽管这样求得的范式符合所谓「直觉」（在 $M$ 中的意义与原项相同，而且对任意的项执行一次或两次 NbE 的结果都一样），但它的实用性很弱。我们希望在集合 $X$ 中也把（而非只在集合 $M$ 中）$\mathrm{reify}(\mathrm{eval}(x))$ 所构造的范式和原项 $x$ 联系在一起，即在集合 $X$ 中有

$ \mathrm{reify}(\mathrm{eval}(x)) = x \tag*{} $

要做到这一点，我们必须先定义 $X$ 上的等价性——无论是通过相等性声明还是通过约简规则定义。或者，我们可以利用模型论（model theory）来定义 $X$ 的等价性：引入另一个「典范」的意义集合 $W$，以及从集合 $X$ 到集合 $W$ 的对应映射。如果 $X$ 中的两个元素在 $W$ 中有相同的含义，那么就可以说这两个元素是相等的。

历史关联

尽管形式主义方法（formalistic method），即我们上文所谈论的「无脑游戏」，常常与希尔伯特（David Hilbert）学派联系在一起。但这种方法最早的倡导者之一是哲学家 C. I. Lewis，他称这种方法是「逻辑方法的异端观点」，并简要概括如下：

A mathematical system is any set of strings of recognizable marks in which some of the strings are taken initially and the remainder derived from these by operations performed according to rules which are independent of any meaning assigned to the marks.
译：数学系统是一个由字符串组成的集合，其中字符串由「可被识别的标记」构成。一部分字符串是和数学系统与生俱来的，而其余的则根据一系列规则从最初的字符串中推导而出。推导规则应当与字符串中的标记被赋予的任何意义无关。

Emil Post 将这种「异端观点」奉为圭臬，他在不诉诸「意义」的前提下提出了这种系统的一致性和完备性标准。Post 还发明了最通用的操纵符号的框架：Post 系统（Post System）。Post 系统的推理规则现在已被人们所熟知——人们用这种推理规则定义文法、描述逻辑系统和类型系统的推导过程、描述编程系统的约简规则……以及最广泛的，用其在编程语言理论中表示算法。我们上面关于袋与束的游戏就是一个 Post 系统。Lewis 的「异端观点」已经被后人发展成为正统。

Lewis 的「异端观点」和希尔伯特主张的形式主义都根植于实证主义（Positivism）哲学。对于实证主义哲学家（维也纳学派）以及 20 世纪二三十年代的许多数学家来说：谈论意义和真理是一种「形而上学」，最好敬而远之。而 Alfred Tarski 提出的模型论则以数学上可接受的方式证明了：「意义」不但可以从数学的角度受到尊重，而且富有成效。NbE 也是这种论点的论据之一。

引用资料

  • Alasdair Urquhart: Emil Post

Handbook of the History of Logic. Volume 5. Logic from Russell to Church. Dov M. Gabbay and John Woods (Editors), 2008 Elsevier BV.

The Stanford Encyclopedia of Philosophy (Fall 2014 Edition), Edward N. Zalta (ed.)

  • Alfred Tarski: Truth and Proof

Scientific American, 1969, pp. 63-77.

The Stanford Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.)

延伸阅读与具体应用

这是一本关于 NbE 的详尽教程，需要读者拥有更多背景知识。发表于 APPSEM 2000: International Summer School on Applied Semantics, Advanced Lectures. Springer LNCS 2395, 2002, 137–192。

（译文暂缺）上文的约简规则语义也可以作为 NbE 的一种形式呈现。

（译文暂缺）用 NbE 优化数据库查询。

（译文暂缺）NbE 可用于优化概率程序：通过确切性推导来删除不必要的概率变量。

（译文暂缺）Danvy 的 TDPE 也是许多独立（重新）发现 NbE 的成果之一。

结论

我们在玩一个简单的游戏时，通过思考游戏的必胜招法与策略，最终发现了 NbE。尽管游戏很无脑，其规则也是任意制定的，但事实证明：我们可以寻找规则背后的意义，将游戏中的代币和招法与我们熟悉的事物建立联系，从而建立对游戏的直觉——并获得一种赢得游戏的方法。简而言之，NbE 是一种借助语义的力量赢得纯粹语法游戏的方法。

一旦我们开始思考符号或物体背后的意义，发现 NbE 就几乎不可避免。柏拉图《理想国》中的「洞穴隐喻」就已经向我们暗示了 NbE 的关键概念。近代以来，多个领域分别独自发现了 NbE，部分求值（Partial Evaluation）领域和类型论（Type Theory）领域就是其中两个例子。然而据我们所知，最早有书面记录可查的 NbE 发明者不是计算机科学家，而是一位哲学家：Per Martin Löf。