基于 LCF 架构的证明

前面几节讲清楚了写什么规约以及验证条件（VC）如何生成：分离逻辑给出断言语言，符号执行引擎把一段带标注的程序归约为若干条逻辑蕴含。 但还有一个问题悬而未决——这些验证条件由谁来证明？ C* 把这项工作交给一个定理证明器；正如我们在 第一个 C* 程序 中启动过的那样，C* 当前集成的证明器是 HOL Light。 HOL Light 属于一个可以追溯到 1970 年代 LCF 的谱系，它的可靠性与可扩展性都来自同一套设计——通常称为 LCF 架构（LCF Architecture）。 本节介绍这套架构与可编程证明的思想，以及 HOL Light 的高阶逻辑、定义机制与演绎证明如何进行。 本节只停留在 LCF 与 HOL Light 的层面，暂不涉及 C* 中具体的证明语法——那是后续章节的内容，本节先把概念基础梳理清楚。

一个交互式定理证明器允许用户一步步构造证明。但随之而来的问题是：凭什么相信它给出的“定理”真的是定理？ 如果证明器内部有 bug，或者用户能绕过某条规则强行注入一个结论，那么它证明出来的东西就一文不值。 Robin Milner 在 1970 年代的 LCF（LCF = Logic for Computable Functions）中给出的回答，至今仍是主流证明器的架构基石。

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

真正的关键是 Milner 的一个巧思：把定理实现成一个抽象数据类型（Abstract Data Type），取名 thmthm。 这个类型的预定义值是逻辑的公理（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 的高阶逻辑精简而以等式为基础：两个原始类型、四种项、公式即布尔项，连接词都由等号定义；
• 内核是一小组原始推理规则加三条数学公理，逻辑的经典性由选择公理显式引入；
• 新的常量与类型只能以保守扩展的方式定义（而非假设公理），一致性因此在构造上得到保证；
• 证明是元语言里的程序：前向施加规则、后向用策略分解目标，策略组合子把步骤组合起来，一切最终都在内核里全部展开。