基于 LCF 架构的证明

前面几节介绍了写什么规约以及验证条件（VC）如何生成：分离逻辑提供断言语言，符号执行引擎把一段带标注的程序归约为若干条逻辑蕴含。还有一个问题没有回答：这些验证条件由谁来证明？ C* 把这项工作交给定理证明器。目前集成的证明器是 HOL Light，我们已在第一个 C* 程序中启动过它。 HOL Light 的设计可以追溯到 1970 年代的 Edinburgh LCF；它的健全性与可扩展性都来自同一套设计，通常称为 LCF 架构（LCF Architecture）。本节介绍这套架构与可编程证明的思想，以及 HOL Light 的高阶逻辑、定义机制和演绎证明过程。我们先从 LCF 与 HOL Light 的机制入手，把概念基础梳理清楚；C* 中具体的证明语法留到后续章节介绍。

交互式定理证明器允许用户一步步构造证明。随之而来的问题是：为什么可以相信它给出的“定理”真的是定理？如果证明器内部有错误，或者用户能绕过某条规则直接插入一个结论，那么它所给出的证明也就失去了意义。 Robin Milner 在 1970 年代的 Edinburgh LCF（LCF = Logic for Computable Functions）中给出的回答，至今仍是主流证明器的架构基础。

早期的证明检查器把整个证明完整保存在内存里，规模因此受限。 Gordon 在历史回顾中举了一个例子：数学讲师只用一小块黑板，每完成一步推导，就擦去中间过程，为下一步腾出空间，最后黑板上只留下结论。 LCF 采用了同样的做法：不保存完整的证明，只保存证明的结果，也就是定理。

Milner 的关键想法是把定理实现为一个名为 thmthm 的抽象数据类型（Abstract Data Type）。这个类型的预定义值是逻辑的公理（Axioms），对它的操作是推理规则（Inference Rules）；除此以外，没有其他方式可以构造这个类型的值。借助宿主语言严格的类型检查，我们就能保证：

能够生成 thmthm 的公理与推理规则共同构成系统的可信内核（Trusted Kernel）。内核之外的代码，无论实现了多么复杂的证明自动化，都无法自行构造 thmthm；要生成定理，最终都必须调用内核中的那几条规则。这样，相信证明器就归结为相信一小段内核代码，而这段代码足够小，可以逐行审查。

这套小内核 + 可编程外壳的设计后来被称为 LCF 方法（the LCF Approach），可以概括成两点：

1. 所有证明最终都归约到一小组原始推理（Primitive Inferences）；只要这个内核正确，推导出的结论就有保证。
2. 整个系统嵌入在一门功能强大的函数式编程语言之中，可以用它编写新的推理规则与证明过程；语言的类型约束保证这些扩展最终仍归约到那组原始规则。

第二点中的语言正是 ML，名字是“Meta Language”（元语言）的缩写，最初是为 LCF 设计的。这里需要区分两个层次：作为推理对象的逻辑叫对象语言（Object Language），用来编写推理过程与策略的编程语言叫元语言（Metalanguage）。 ML 采用强类型设计，是为了支持上述抽象类型机制；采用函数式设计，则是为了让证明策略能自然地表示为函数。

要让内核足够小，它所实现的逻辑本身就必须足够精简。HOL Light 名字中的 Light，很大程度上体现了其底层逻辑的简洁。

它的对象语言是高阶逻辑（Higher-order Logic），具体说是带多态类型变量（Polymorphic Type Variables）的简单类型论（Simple Type Theory），也就是简单类型 -演算以及多态。高阶指量词可以作用在函数和谓词上，而不仅是个体。

类型（Types）. 从两个原始类型出发：（布尔/命题）与 （个体）；由任意两个类型 、 可构造函数类型 。每个项都带有唯一确定的类型，类型系统会拒绝无意义的表达式。

项（Terms）. 项的形式只有四种，这一点也许出乎意料：

• 变量（Variable），如 ；
• 常量（Constant），如 ；
• 应用（Application），把函数作用于参数，如 ；
• -抽象（Abstraction），，表示给定 时返回 的函数。

其中一个关键设计也许最不符合直觉：公式就是布尔类型的项，并不单独构成一个语法范畴。命题 与数值 一样是项，只不过前者类型为 、后者类型为 。其他记号都是这四种项之上的语法糖：量词 实际上是将常量作用于抽象，即 ； 绑定则是一次 -应用。所有变量绑定都归约到 -绑定，因此内核只需处理这四种项。

以等式为基础（Equality-based）. HOL Light 核心逻辑里本质上只有一个预定义的逻辑常量：等号 （外加一个用于选择的算子 ）。布尔项之间的当且仅当 就是布尔类型上的等号。其余逻辑连接词都由等号定义，例如：

从这些定义出发，就能推导出通常的自然演绎规则。几乎所有原始规则都只涉及等式，逻辑也因此能够保持精简。

内核的核心就是那 10 条原始推理规则。断言写成一条相继式（Sequent） ，意为“在假设集 下，布尔项 成立”。下面列出其中几条有代表性的（记号 表示两个假设集的并）：

这些规则大多表达了等式的自反性、传递性和合同性，此外还有引入假设（ASSUME）与用等价改写（EQ_MP）。其余几条（MK_COMB、DEDUCT_ANTISYM_RULE、INST、INST_TYPE）分别处理函数应用的合同、由两个方向的蕴含导出等价，以及对项变量与类型变量的免捕获替换。 ABS 有一条附加条件： 不得在 中自由出现。这类条件是保证健全性所必需的，不能省略。

除了这 10 条规则，还在内核之外加入三条数学公理：外延性（-转换）、选择公理、无穷公理。其中，选择公理需要单独说明：HOL Light 的核心逻辑本身是构造性的，加入选择公理后才能推出排中律等经典逻辑原则。换句话说，逻辑的经典性是显式引入的，并非默认成立。

有了内核，如何发展出自然数、列表、实数这些丰富的数学结构？一个危险的做法是直接假设公理来刻画它们。多一条公理，就多一分引入矛盾的风险。 HOL 采用另一种方式：通过定义来扩展理论，而不增设公理。新的常量与类型只能以保守扩展（Conservative Extension）的方式引入。粗略地说，这相当于“为已有理论中的某个表达式取一个简写”，不会给逻辑增添新的内容，因此构造本身就保证了一致性。

常量定义. new_definitionnew_definition 接受一个方程 ，定义常量 并返回定理 ：

# let wordlimit = new_definition `wordlimit = 2 EXP 32`;;
val wordlimit : thm = |- wordlimit = 2 EXP 32

# let wordlimit = new_definition `wordlimit = 2 EXP 32`;;
val wordlimit : thm = |- wordlimit = 2 EXP 32

为什么这样不会破坏一致性？关键在于定义施加了限制，例如不允许把已有常量重新定义为其他内容：

# let wordlimit' = new_definition `wordlimit = 2 EXP 64`;;
Exception: Failure "new_definition: 'wordlimit' already defined".

# let wordlimit' = new_definition `wordlimit = 2 EXP 64`;;
Exception: Failure "new_definition: 'wordlimit' already defined".

如果允许重新定义，系统中就会同时有 与 ，从而推出 ，进而导出矛盾。定义原则所禁止的，正是这样未经论证就额外增加断言的做法。

类型定义. new_type_definitionnew_type_definition 从已有类型的一个非空子集出发，生成一个与该子集存在双射的新类型。这个子集由特征谓词刻画，且必须先证明其非空；双射两个方向的函数通常称为抽象函数与表示函数。此后，新类型上的任何概念都必须通过这两个函数显式定义，任何定理也都能转换回表示类型上证明。类型定义因此与常量定义一样是保守的：凡是借助新类型能证明的事实，都可以不用新类型，将命题相对化到那个子集上加以证明。新类型只是省去了这种相对化的麻烦。

回到 LCF 方法的第二点：证明本身就是元语言里的程序。这带来两种互补的证明方式。

前向证明（Forward Proof）. 从公理与已有定理出发，逐步施加推理规则推出新定理。在 HOL 中，一条推理规则就是一个返回 thmthm 的 ML 函数。例如，传递律 TRANSTRANS 的类型是 thm -> thm -> thmthm -> thm -> thm，它将 与 组合为 ：

# TRANS (ARITH_RULE `1 + 3 = 4`) (ARITH_RULE `4 = 2 + 2`);;
val it : thm = |- 1 + 3 = 2 + 2

# TRANS (ARITH_RULE `1 + 3 = 4`) (ARITH_RULE `4 = 2 + 2`);;
val it : thm = |- 1 + 3 = 2 + 2

后向证明（Backward Proof）. 前向证明往往不太符合直觉。我们更习惯从待证的结论出发，把它分解为更简单的子目标，直到这些子目标都能直接解决。这种目标导向（Goal-directed）的方式涉及两个概念：

• 目标（Goal）：一个待证的布尔项，连同一组可用的假设；
• 目标栈（Goalstack）：系统用来保存尚待证明的子目标的栈。

推动后向证明的工具叫策略（Tactic）：

用户不断施加策略来完成后向证明，系统则借助验证函数，把这个过程转换为内核的原始推理。因此，后向证明也必须经过可信内核，最终仍全部归约到那 10 条规则。

策略组合子（Tactical）. 策略也可以组合，用来组合策略的高阶函数叫策略组合子。最常用的有 THENTHEN（先施加前一个策略，再将后一个施加到产生的所有子目标上）、THENLTHENL（对不同子目标分别施加不同策略）、REPEATREPEAT（尽可能多次重复）、ORELSEORELSE（前者失败时尝试后者）。用它们可以把一系列证明步骤组合为一个紧凑的表达式。

在这套框架中，用户可以采用与内核规则相同的写法，编写自己的专用推理规则乃至判定过程；所有这些派生工具最终都由内核逐步展开为原始推理步骤。这样还可以把寻找证明与检查证明分开：用任意程序，甚至外部工具搜索证明，再把结果交给内核做形式化检查。

加载 HOL Light 后，我们使用的就是一个普通的 OCaml 读-求值-打印循环（REPL），其中已载入大量定理与证明工具。项写在反引号内，定理打印时以 |-|- 开头，这是推导符 的 ASCII 近似表示。

下面用后向方式证明加法交换律。proveprove 接受一个目标和一个策略，一次性给出定理：

# let ADD_SYM = prove
   (`!m n. m + n = n + m`,
    INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
val ADD_SYM : thm = |- !m n. m + n = n + m

# let ADD_SYM = prove
   (`!m n. m + n = n + m`,
    INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
val ADD_SYM : thm = |- !m n. m + n = n + m

逐步来看，INDUCT_TACINDUCT_TAC 对 使用数学归纳法，将目标分解为基本情况（）与归纳步骤两个子目标，并自动将归纳假设加入后者的假设列表；THENTHEN 将随后的策略施加到两个子目标上；ASM_REWRITE_TAC[...]ASM_REWRITE_TAC[...] 则用当前假设和一条更基本的定理 ADD_CLAUSESADD_CLAUSES 反复改写，卸除两个子目标。

若想观察中间过程，也可以在目标栈上逐步交互：gg 设置目标，ee 施加一个策略（expand），bb 撤销上一步（back up），top_thm()top_thm() 则在所有子目标都得到证明后返回定理。

# g `!m n. m + n = n + m`;;
val it : goalstack = 1 subgoal (1 total)
`!m n. m + n = n + m`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)
...

# g `!m n. m + n = n + m`;;
val it : goalstack = 1 subgoal (1 total)
`!m n. m + n = n + m`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)
...

不同形式的目标适合用不同的策略处理。下表汇总了本节提到的策略和几个常用的自动化策略：

不过，这种过程式证明脚本编写起来往往需要相当的耐心，阅读和修改也并不轻松。它本质上是一段高度过程式的程序，记录了怎么证，却未必能让人一眼看清楚证了什么。后续章节将从这里继续，介绍 C* 如何在这套 LCF 机制之上，为 C 程序验证提供更符合直觉的证明写法。

• LCF 架构将定理实现为抽象类型 thmthm，借助类型系统保证它只能由内核的公理与推理规则生成。这就是定理安全性，它将相信证明器归结为相信一小段内核代码；
• HOL Light 的高阶逻辑精简而以等式为基础：两个原始类型、四种项、公式即布尔项，连接词都由等号定义；
• HOL Light 的逻辑基础由一小组原始推理规则与三条数学公理组成，逻辑的经典性由选择公理显式引入；
• 新的常量与类型只能通过定义以保守扩展的方式引入（而非假设公理），构造本身就保证了一致性；
• 证明是元语言中的程序：前向证明施加规则，后向证明用策略分解目标，策略组合子则用来组合这些步骤。所有步骤最终都在内核中展开。