ely*_*ner 63 formal-methods coq isabelle
与Coq相比,Isabelle/HOL证明助手是否有任何弱点和优势？
Art*_*rim 59
我对Coq很熟悉,并且对Isabelle/HOL没有太多经验,但我可能会有所帮助.也许在Isabelle/HOL上有更多经验的人可以帮助改善这一点.
这两个系统之间存在两大分歧:基础理论和交互风格.我将尝试简要概述每种情况下的主要差异.
Coq和Isabelle/HOL都基于强大的,非常富有表现力的高阶逻辑.但是,这些逻辑在一些功能上有所不同:
Coq的逻辑是一种依赖型理论,称为归纳结构的微积分(简称CIC)."依赖类型"在这里表示Coq中的类型可以引用普通值.例如,可以mult用类型编写矩阵乘法函数
mult : forall (n m p : nat), matrix n m -> matrix m p -> matrix n p
这个函数的类型表示它需要两个矩阵作为输入,一个是维度n x m,另一个是维度m x p,并返回一个维矩阵n x p.另一方面,Isabelle/HOL的理论并不具有依赖类型; 因此,不能编写mult与上述类型相同的函数.相反,人们必须编写一个适用于任何类型矩阵的函数,并在接收到正确种类的参数时证明该函数的后验某些属性.换句话说,在使用Isabelle/HOL时,需要将Coq类型中显示的某些属性断言为单独的定理.
虽然依赖类型对于某些事情很有意思,但它们一般都不是很有用.我的印象是有些人觉得它们使用起来非常复杂,并且在类型级别表达某些属性而不是将它们作为单独的定理表示的好处并不值得这种额外的复杂性.就个人而言,我喜欢在少数情况下使用依赖类型,当有明确的理由这样做时.
默认情况下,Coq的理论缺乏许多在数学实践中常见的推理原则,例如被排斥中间的法则(即,非建设性地推理的能力),延伸性(例如,能够说出产生相同结果的函数)他们自己是平等的,和选择的公理.另一方面,在Isabelle/HOL中,这些原则是内置的.
从理论上讲,这不是一个大问题,因为Coq的逻辑旨在让人们安全地将这些推理原则作为额外的公理添加.尽管如此,我的印象是在Isabelle/HOL上进行这种推理更容易,因为逻辑是从头开始构建的,以支持它们.
(您可能想知道将这些基本原理排除在Coq逻辑之外的原因是什么.动机是哲学的:在Coq的核心逻辑中,证明可以被视为可执行程序,这使得逻辑具有建设性的风格.拒绝被排除的原因例如,中间是一个析取的证明A \/ B对应于一个程序,该程序返回一个指示哪一个A或哪个B是真的;因此,被排除的中间将对应于一个程序,该程序决定了每个数学问题,这是不可能存在的.这个问题进一步讨论了这个问题.)
Coq和Isabelle/HOL都是互动定理证明.它们是用于编写关于它们的定义和证明的语言; 这些证明由计算机检查,以确保它们没有错误.在这两个系统中,人们通过给出解释如何证明某事的命令来记下证据.然而,每个系统上发生这种情况的方式各不相同.
Isabelle/HOL一般来说对"按钮式"校样自动化有更成熟的支持.例如,它带有着名的sledgehammer策略,它引用了几个外部自动定理证明器和求解器来试图证明一个定理.Coq还带有许多强大的证明自动化程序,例如omega或congruence,但它们并不普遍适用,并且许多可以通过Isabelle/HOL中的单个命令解决的定理在Coq中需要更明确的证明.
当然,这种便利需要付出代价.我被告知,在Isabelle/HOL中控制一个人的证据比较困难,因为系统试图自己做很多事情.在证明简单定理时这不是问题,但是当证明自动化不够强大并且你需要告诉定理证明如何更详细地进行时,它就成了一个问题.
支持用户定义的校对自动化程序时,情况有所不同.Coq带有一种用于编写证明的策略语言,称为Ltac,它本身就是一种编程语言.尽管Ltac存在一些设计问题,但它确实允许用户以轻量级方式编写相当复杂的证明自动化程序.对于较重的任务,Coq还允许用户使用Coq的实现语言OCaml编写插件.相比之下,在Isabelle/HOL中,没有像Ltac这样的高级自动化语言,用户可以通过插件编写自定义校对自动化程序的唯一方法.
小智 14
我将说明Isabelle/HOL的"按钮"功效的一个方面是它对Cantor的经典"对角化"论证的自动化(回想一下,这表明自然界没有从它的功率集中出现,或者更一般地,任何设置为其功率集.
theorem Cantor: "?f :: 'a ? 'a set. ?A. ?x. A = f x"
proof
assume "?f :: 'a ? 'a set. ?A. ?x. A = f x"
then obtain f :: "'a ? 'a set" where *: "?A. ?x. A = f x" ..
let ?D = "{x. x ? f x}"
from * obtain a where "?D = f a" by blast
moreover have "a ? ?D ? a ? f a" by blast
ultimately show False by blast
qed
我刚刚向您介绍的是将Cantor的经典论证翻译成Isabelle/HOL.毫无疑问,巧妙!Isabelle/HOL可以自动消除这种证据的洞察力,但是:
theorem "?f :: 'a ? 'a set. ?A. ?x. f x = A"
by best
theorem "?f :: 'a ? 'a set. ?A. ?x. f x = A"
by force
证明系统能够自动证明Cantor的陈述.对于研究人员来说,一方面这是有帮助的,但有一种感觉,这是一把双刃剑.我可以发现,作为对角化参数这样复杂的真实陈述可以被信任,可以在Isabelle/HOL内部得到证实,因为我的定理更加复杂.另一方面,我进一步研究由计算机的自动化进程驱动,我可以越来越少地解释为什么或者什么原理定理是真的.只有计算机知道为什么,只要我们可以问它!
由于"Isabelle/HOL"已经在问题中得到了解决,我将讨论Isabelle中使用的HOL逻辑,我认为这是用于与Coq进行比较的最佳逻辑.我不是类型系统和逻辑方面的专家,但我认为我在这里所说的是正确的,至少是近似的.这也是一个品味问题;-)我的回答可能是主观的.
最深刻的区别在于类型系统和逻辑.
我会说,对于那些知道ML族功能性语言的人来说更有自然力量(对知道SML的人来说更是如此)并且它使用务实的方法来解决问题,例如使用经典逻辑作为一个基础.它的类型系统接近Hindley Milner的类型系统并默认终止(如果它没有被用户修改).
另一方面,Coq更严格,使用直觉逻辑.它有一个具有多个订单的专用类型系统,并允许类型依赖,这可能更难以处理,并且在某些情况下可能是非终止的.它还允许人们从证据中提取程序(可能效率相对较低),这在Isabelle中是不可能直接实现的.