LCF是Logic for Computable Functions (可计算函数逻辑)
的缩写. 与许多缩写一样, 它现在(至少对我们而言)所表示的含义已经比最初丰富了许多. 本文档所完整描述的机器实现系统LCF, 其目的在于探索一种特定逻辑的表达能力和演绎能力, 以及在该逻辑中进行证明时所产生的实际问题.
这两个目的在很大程度上是相互独立的. 关于与机器交互式地进行证明的风格等实际问题, 并不会因演绎演算的选择不同而有很大差异. 从原则上说, 我们可以给予用户以完全自由地描述这个演算的能力. 然而, 任何非常一般的系统都容易产生对于特定情况的低效处理, 故我们倾向于使得我们的系统面向一种特定的演算, 其被称为PPLAMBDA (Polymorphic Predicate \-calculus; 读者必须要习惯于本文使用\
代表lambda
). 我们将在引论的后面回到这一演算及其与程序设计的关系; 首先我们想讨论启发我们系统的设计的现实因素.
过去人们充分地探索过在计算机上做证明的两种极端风格. 第一种风格是自动定理证明
; 通常是编写一个通用的证明寻找策略, 用户的工作仅限于: 首先提交一些公理和一个要证明的公式, 其次(可能要)调整策略的某些参数以控制其搜索方法, 第三(可能要)在系统搜索证明的过程中响应系统的求助请求.
第二种风格是证明检查
; 用户提供一个声称的证明, 一步一步, 然后机器检查每个步骤. 在证明检查的最极端形式中, 每一步都是一条原始推理规则的应用, 尽管许多证明检验系统允许复杂的推理 (例如逻辑公式的化简) 在一步中完成. 这种风格的一个特点是证明是正向进行的, 从公理到定理; 而在自动定理证明器中, 内置策略通常是目标导向的 (传统上, 这是通过将目标公式的否定作为额外的公理
并试图产生矛盾来实现的).
毫无疑问, 在这两种风格之间存在许多折衷方式, 以试图消除各自最糟糕的特性——例如自动定理证明器低效的通用搜索策略, 以及直接证明检查的乏味和重复性. 我们系统的主要目的如下:
这些目标——尤其是提供一种元语言——源于1971-2年在斯坦福大学对PPLAMBDA的一个受限版本所做的早期实现 (参见参考文献中LCF Studies下所列条目). 在那个系统中, 元语言仅由少数几条简单命令组成, 例如用于执行基本推理或攻克基本策略中的目标. 人们很快发现, 将这些命令复合成复杂的推理规则和策略, 是开发更强大系统的关键因素.
在我们所提出的自然
证明风格中, 有三个重要元素. 最根本的是采用自然演绎, 即逻辑学家Gentzen和Prawitz所确立的那种意义上的自然演绎. 在这里, 推理规则起主导作用, 而非像Hilbert风格逻辑中那样以公理为主; 其重点在于假设的引入与消去, 从而避免在证明步骤中出现推出式 (implication) 的嵌套.
第二个元素是使用目标导向的证明过程或者说配方 (recipe). 当一个数学家问另一个人你对的证明是什么?
的时候, 他往往是问你是如何证明的?
; 也就是说, 逐步的形式证明不如证明的配方使他满意. 配方可以是类似于对于字符串的长度进行归纳, 然后分情况讨论并使用连接运算的结合律
这样的东西. 当然了, 这是非常模糊的; 对于什么情况进行讨论, 归纳的种类是什么, 等等. 但是如果我们继续施加压力, 那个人或许会给出更加详细的配方, 仍然保持相同的风格. 要义在于这样的配方, 或者说策略, 往往是由更小的配方通过组合构建而成的 (之后我们将会称这些东西为战术 (tactics) 而非策略). 我们可能会发现原始战术的数目是相当之少的, 而许多有趣的策略可以通过使用一些战术上的运算 (或许数目也不多) 构建而成. 我们将这些运算称为战略 (tacticals)
, 类比于泛函 (functionals).
因而设计ML的目的之一是使得编写战术和战略容易起来. 实际上为了达成这一目的并不需要什么非常特别的东西; 主要是需要能够处理高阶函数.
自然证明风格的第三个元素是强调理论结构. 数学中的许多定理依赖于先前理论中的结果; 存在一个自然的理论层次结构, 这一结构应当体现在人们与计算机 (或与图书馆和一沓纸) 进行多次交互会话以建立一系列有用定理的过程中. 关于计算的理论也不例外: 一个关于用ALGOL编写的程序的定理, 不仅依赖于程序中所使用的数据结构的理论, 还依赖于ALGOL本身的句法和语义理论. 当你进入LCF系统时, 首先会被问到是希望在一个已有的理论中工作, 还是创建一个新的理论; 如果选择后者, 你需要声明它所基于的父理论. 我们在下一节和附录1中的示例展示了这在实践中是如何运作的. 我们并不认为我们对理论的处理是完备的; 例如, 我们尚未考虑参数化地定义理论的方式. 要了解其用途, 可以考虑构建一个布尔代数理论. 一种方法是将其建立在交换幺半群理论的两个实例之上, 这两个二元运算有着不同的名字; 因此, 后者的理论应当在这个名字上进行参数化. 我们想要在理论的进一步发展中使用Burstall和Goguen的工作 (参见参考文献).
现在让我们来看逻辑与编程之间的关系, 并尝试将PPLAMBDA置于这一背景下. 首先, 演绎语言与编程语言之间存在很强的相似性: 两者都有精确的句法, 并且都有语义理论 (对于编程而言, 语义理论是较为晚近的发展). 另一方面, 也存在明显的不对称性. 对程序进行演绎推理是重要且自然的, 编写执行演绎的程序也同样如此, 但很难抗拒这样一种观念, 即声明性陈述和演绎是首要的; 我们总是希望推导关于程序的事实——即便是那些执行演绎的程序.
处理这种复杂关系的一种当前方法是, 避免将编程或演绎中的任何一方置于另一方之上, 而是将两者共同构建在一个既是声明性的又是命令性的形式系统中. 其结果被称为编程语言还是演绎系统并不重要, 而且这一方法的倡导者可能会认为这两种描述都有误导性. 他们的观点是, 好的编程应当始终伴随着演绎. 这一观点的有趣且各不相同的例子可见于Constable和O'Donnell的工作, Pratt的工作, 以及Rasiowa的工作 (参见参考文献).
另一方面, lambda演算中存在一种关于算法的典范演算 (至少对于顺序算法而言). Scott, Strachey及其后继者已经表明, 它足够丰富, 能够定义编程语言的句法和语义; 它也可能被用来描述硬件. 因此, 关于程序变换, 编程语言之间的翻译, 以及语言在计算机上的实现等问题, 可以在lambda项之间关系的演算中被形式化地表达和研究. 这正是PPLAMBDA的预期用途之一. 目前——尽管这可能是暂时的——上一段中提到的那些集声明性与命令性于一体的演算, 似乎更适合于验证特定的程序.
在我们看来, 这两种方法以及其他方法都必须加以采用, 以建立编程的理论, 偏好其中一种而排斥另一种是短视的.
我们希望在这一阶段执行一些简单的推理, 并展示如何在一种读者应当熟悉的演算中编写证明配方 (实际上, 它是PPLAMBDA的一个受限版本). 我们将只使用ML的一个片段. 我们的例子将展示ML的类型结构如何提供一种规范, 强调证明过程中涉及的句法对象和其他对象之间的区分; 它还将突显我们自然
证明风格中的一个重要要素——即定理的证明并非没有动机, 而是心中带着某种目的或目标来进行的.
让我们假设我们正在探索布尔代数的理论, 其已被我们命名为`BA`. 这意味着我们已经公理化了这个理论, 或许已经证明了一些重要的定理 例如deMorgan律, 以及否定的消去), 并且我们想要扩展我们在这种代数中工作的能力. 这种扩展的一部分显然是证明更多的定理; 另一重要的部分是定义证明方法, 或者过程, 或者策略, 作为元语言的实体——也就是说, 作为ML中的函数或者过程.
我们的公理已被命名, 并可藉由其名使用. 系统将这些公理以如下形式保存至`BA`理论文件里:
orcomm "!X.!Y. X + Y == Y + X"
andcomm "!X.!Y. X * Y == Y * X"
ordist "!X.!Y.!Z. X + (Y * Z) == (X + Y) * (X + Z)"
anddist "!X.!Y.!Z. X * (Y + Z) == (X * Y) + (X * Z)"
oride "!X. X + 0 == X"
andide "!X. X * 1 == X"
orinv "!X. X + -X == 1"
andinv "!X. X * -X == 0"让我们以最显然和初等的方法施行对于"-0 == 1"的证明, 使用公理`orcomm`, `oride`和`orinv`, 并且利用相等关系==的推理规则: 全称特化 (SPEC), 传递性 (TRANS), 对称性 (SYM). 我们首先将证明呈现为一个树, 以自然演绎的风格; 这将有助于读者跟上之后的ML会话.
我们将会在ML中执行这个证明. 在以下的每一步骤里, 用户都在系统的提示符#之后输入一个ML phrase, 然后系统会作出合适的响应.
#SPEC "0" (AXIOM `BA` `orinv`) ;;
]- "0 + -0 == 1" : thm(AXIOM ...)产生了定理]- "!X. X + -X == 1"作为其值 (通过访问这个理论的文件). 推理规则SPEC, 其(元)类型为term->(thm->thm), 生成了显示为这整个phrase的值的定理. 每个ML phrase的元类型 (整节我们都会使用这个术语, 以将ML中的类型和PPLAMBDA中的类型区分开来) 都可以从句法上确定, 并且总会由系统和phrase的值一起打印出来. 以上phrase牵涉的元类型还有term和token; "0"是具有元类型term的一个常量, 而`BA`和`orinv`则是元类型为token的常量 (于是AXIOM的元类型为token->(token->thm)). token是用来命名理论和公理的, 当然也有其他许多目的. 另一种元类型是form (公式的类型). "0==1"是一个具有此元类型的对象——但它绝不是具有元类型thm的对象; 定理和公式不同, 定理只能由推理规则计算出来. 系统通过在定理前打印]-以突显它们.下一步骤是特化`orcomm`以得到定理]- "-0 + 0 == 0 + -0", 并将其通过传递性和我们之前的定理组合起来 (之前的定义用it指代, 这是一个总是代表最后的ML表达式的值的元变量):
#TRANS(SPEC "0" (SPEC "-0" (AXIOM `BA` `orcomm`)), it) ;;
]- "-0 + 0 == 1" : thm`oride`于"-0", 然后将作为结果的等式通过对称规则逆转方向, 最后将其与我们最后证明的定理组合起来:TRANS(SYM(SPEC "-0" (AXIOM `BA` `oride`)), it) ;;
]- "-0 == 1" : thm`zeroinv`, 然后将其与`BA`的其他有趣定理存放在一起, 这些定理可以通过函数FACT访问——就像公理可用通过AXIOM访问.newfact(`zeroinv`, it) ;;
]- "-0 == 1" : thm现在我们将展示证明如何以目标导向的方式完成. 我们将目标设为把任意的一个布尔表达式t转换为一个等价的范式, 并且我们只在计算出一个定理]- "t == n"时才认为这个目标达成了, 其中n是一个合适的范式.
我们认为一个析取范式 (DNF) 是一个文字的合取 (*) 的析取 (+), 而一个合取范式 (CNF) 是一个文字的析取的合取, 其中文字是一个可能否定的原子 (, , 或是一个变量). 出于简单性的考量, 我们忽略了和的出现的去除, 也忽略了合取与析取里重复或者互补元素的去除.
这个问题的自动化方法当然是众所周知的, 但是我们会用它来刻画交互性的方法, 我们发现交互性的方法在更为复杂的情况下比较自然. 我们将会展示部分子目标方法 (之后我们将会称其为战术) 是如何编写的, 然后我们在我们的例子里展示如何将战术拼在一起以构成问题的一个完整策略.
以下是一个将项t转换为DNF dn的简单配方.
t是一个析取(t1+t2), 那么对于t1和t2分别得到其DNF dn1和dn2, 然后构成其析取(dn1+dn2);t是一个合取(t1*t2), 那么对于t1和t2分别得到其DNF dn1和dn2, 然后构成其合取(dn1*dn2), 接着通过重复运用`anddist`将其转换为DNF;t是一个否定(-t1), 对于t1得到其CNF cn1, 然后通过重复运用deMorgan律和否定消除来将(-cn1)转换为DNF;t是原子性的, 那么dn就是t本身.为了形式化我们的配方, 我们可以设我们的目标具有形式
(t, b)b是真值true, 如果t要被转换为DNF, 是真值false则t要被转换为CNF. 于是, 我们定义元类型goal = term # boolbool是一个原始元类型, 但是其和我们这个例子的主题没什么关系.) 现在我们可以将配方的子句(i)想成是一个部分子目标方法——之所以说是部分, 是因为其只在具有下列形式的目标上工作:(t1+t2, true)b的值都是一样的. 我们的目的是单独编写这些战术; 之后我们将会把它拼在一起以产生一个完整的策略.更仔细地考虑子句(i). 其告诉我们要产生什么子目标, 即(t1, true)和(t2, true); 其也非形式化地告诉了我们在达成子目标的情况下如何达成原本的目标. 更形式化地说, 基于推理的语言, 其告诉我们如何由形式为]- "t1 == dn1"和]- "t2 == dn2"的定理推出定理
]- "t1 + t2 == dn1 + dn2"这将我们导向设战术为这样的东西, 对于一个目标, 产生一个子目标的列表和一个澄清 (validation) ——即由子目标的达成推出原本目标的方法. 但是达成应该是定理, 所以说一个澄清不过就是一个(导出)推理规则. 因此, 我们定义元类型
tactic = goal -> (goal list # validation)
validation = thm list -> thmORCONG, 其表达了==相对于+是一个congruence. PPLAMBDA演算的项是类型化\-演算的项, 外加不动点组合子. 每个类型都被解释为了一个域 (domain), 其是一个完备偏序 (也就是说, 域里存在一个最小元素, 并且升链有着最小上界).