摘要

  • Edinburgh LCF 允许可编程 tactic 从目标向后搜索，但成功的搜索仍须通过 validation 回到受保护的推理规则；错误的 tactic 不会因此获得另一条伪造 theorem 值的路径。
  • theorem 抽象类型缩小了直接参与定理构造的可信代码面，却没有证明所选逻辑必然一致，也没有证明规格符合现实意图，更没有消除编译器、运行时与硬件假设。
  • 这段历史属于团队：Dana Scott 提供底层逻辑，Stanford LCF 在先，Michael Gordon、Christopher Wadsworth、Lockwood Morris、Malcolm Newey 与更广社群共同建设 Edinburgh LCF 和 ML；后继证明器继承并改写了这套思想，并非同一种架构的复制品。

最后一步与此前所有步骤不同

设想一个自动 tactic 把一个目标拆成若干子目标，尝试重写、回溯，再用组合策略继续搜索。它的日志很长，过程也可能相当有说服力。即使界面最后显示所有分支都已关闭，在 LCF 的意义上，这些事件本身仍不构成一个定理。

边界在随后才被跨越。tactic 返回一个 validation：它接收各个子目标的 theorem 值，并用这些值构造原目标的 theorem。当子目标都被证明后，validation 通过受保护的定理接口执行向前推理。若它做不到，无论搜索记录多么漂亮，都没有获得验收。

这是对一个实际设计难题的回答。交互式证明器必须允许用户表达新的证明方法，而这些方法可能复杂、实验性强，也可能含有错误。如果每个新程序都能任意生成定理，可信面会随着插件和策略不断膨胀。LCF 把定理构造放进一个通常称为 thm 的抽象类型里，只有公理和原始推理规则能够返回这种类型的值。

这并不使 tactic 自动正确。它可以选择不合适的子目标、无限运行、抛出异常，或者给出不能兑现承诺的 validation。关键的否定能力更窄：普通搜索代码不会因为复杂就获得备用构造器。错误通常表现为无法取得请求的 theorem，而不是取得伪造 theorem 的许可。

从证明检查器到可编程证明器

Milner 在 1972 年描述了一个针对 Dana Scott“可计算函数逻辑”的已实现证明检查器。Stanford 阶段提供了起点，但长证明暴露了低层检查繁琐、保存完整证明历史耗费内存等问题。Milner 1973 年转到 Edinburgh 后，项目逐步形成了更可编程的环境。

这不是孤胆发明家的故事。1979 年的权威专著 Edinburgh LCF 由 Michael J. C. Gordon、Robin Milner 与 Christopher P. Wadsworth 合著；1978 年的 ML 论文还署名 Lockwood Morris 与 Malcolm Newey。Paulson 的历史回顾记录了这条协作链，Gordon 的第一人称回忆则把 Stanford、Edinburgh 与后来 HOL 的发展连接起来。Dana Scott 的逻辑是最初被机械化的对象。

ML 最初就是“Meta Language”，让证明程序可以被编写。项、公式、目标和策略都能作为数据与函数处理。Milner 对多态类型纪律的研究后来形成独立而重大的编程语言贡献，他在 1978 年的论文中给出语义与语法健全性结果，并讨论在 Edinburgh LCF 中工作的 Algorithm W 方案。但历史归属必须精确：LCF、ML、tactic 设计和交互式证明由团队与研究社群共同推动；Milner 的架构洞见虽居核心，也不能抹去共同贡献。

于是，向前推理与向后搜索获得了不同角色。推理规则接收 theorem 值并返回新的 theorem 值；tactic 查看一个目标，提出子目标；validation 说明日后如何把这些子目标的 theorem 组合成原目标的 theorem；tactical 则以顺序、重复、选择等方式组合 tactic。tactical 扩展的是边界外的搜索表达能力，不是新的公理。

因此，大型搜索程序不必与定理构造器以同样方式被信任。搜索代码可以替换、调优或放弃，而验收接口可以相对稳定。恰当的总结不是“自动化是安全的”，而是“自动化可以提出候选；只有更小的接口可以授予持久类型”。

抽象类型买到的是什么

抽象数据类型隐藏内部表示，只开放指定操作。应用到定理上，用户代码可以持有和传递 theorem 值，却不能通过改写内部字段直接伪造新值。语言的类型抽象负责维护这条边界。

收益首先是架构性的。审查可以集中在较小的一组公理与推理规则实现，而不是每一个新写的 tactic。自动化仍可丰富，因为它的最终产物必须穿过共同路径。复杂代码的总量，不再等于直接决定定理是否存在的代码量。

“小内核”不能被浪漫化成“无需信任”。公理和规则必须对目标逻辑真正健全；抽象类型能阻止绕路，却不会自动证明某条原始规则选择或实现正确。类型抽象还依赖实现层忠实维持它，编译器缺陷、不安全逃生口、运行时故障与硬件错误都在逻辑接口之下。解析器与显示器也可能误导用户，即便存储的 theorem 构造无误。可信根被缩小，并未消失。

内核健全性也不等于逻辑一致性。健全规则是在给定语义或形式说明下保持有效性；一致性关心系统能否推出矛盾。两者的关系依赖额外假设，抽象类型本身不能承担这些证明。“这个值只能由这些函数生成”是构造来源的约束，不是这些函数都代表有效推理的独立证明。

证明与规格同样要分开。关于模型的 theorem 只确立形式化之内的推论。它不会自动说明模型准确捕捉了实际系统、环境、威胁、法规或人的意图。如果规格漏掉现实约束，一个完美内核仍可能完美地证明了错误的问题。形式验证强化已写出的约定，却不能凭空补回未写出的意图。

validation 为什么是铰链

validation 常被泛化成“检查”，但它的职责更具体。tactic 做向后转换：从一个目标得到一组子目标。validation 则向前工作：拿到子目标的 theorem 值，构造原目标的 theorem。向后搜索因此随身携带一份延期兑现的说明，说明成功最终如何被正当化。

所以，证明状态在界面上发生变化，并不等于证明已经发生。一个程序只是删除目标，不能算证明它；一个返回空子目标列表的程序，还必须提供无需虚构前提就能产生目标 theorem 的 validation。若组合无效，最终的向前构造就会失败。

tactical 在组合策略时继续维护这种纪律。顺序 tactical 可以先用一个 tactic，再把另一个 tactic 应用于得到的子目标；重复 tactical 可以在仍有进展时继续。它们的组合也必须组合 validation。控制层可以极其复杂，但验收依据仍沿组合结构回到原始推理操作。

这就是开篇场景的意义。搜索日志、绿色状态和漂亮脚本都是有用记录，却不是 theorem 值。活动证据与验收权限被刻意分开。边界不因计算量庞大而动摇，它只问：受保护构造器能否从已接受前提复现所声称的结论？

后继系统相关，但不相同

LCF 方法影响了一系列证明器。Gordon 把这条架构血脉带入 HOL，Paulson 先发展 Cambridge LCF，后又建立 Isabelle。Cambridge 对 HOL Light 的说明至今仍强调：系统可以扩展，而健全性依赖一个较小的可信核心。它们确实是后继者。

但继承不等于统一。Paulson 说明，Isabelle 让规则与证明状态共享表示，其向前与向后推理的基础不同于经典 LCF 每条规则一个函数的设计。基于构造类型论的系统可能保存 proof term，并以另一种方式依赖类型检查器；有些系统导出证书供独立重检。即便在 LCF 传统内部，不安全功能、证明记录、内核语言和重检方式也会改变可信边界。

准确的历史结论应当是：Milner 与 Edinburgh 团队展示了如何借助强类型抽象，把可扩展证明搜索与受保护定理构造分离；后来许多系统调整并采用了这条经验。不能据此声称所有现代证明助手都拥有同一种小内核，也不能仅凭使用 tactic 就认定系统采用 LCF 架构。

来源与论证边界

本文依据原始论文、大学档案与技术回顾，不是对当代证明器的安全审计，也不声称量过任何内核的代码行数。把共同验收规则保持得最小且可验证、同时允许未来搜索方法自由演进，是受 Lu Heng“最小初始规格”原则启发的编辑分析，不代表 Milner 对制度治理的公开立场。