科学哲学

译自 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 同理）。...