83

Isabelle/HOL 校对助手和 Coq 相比有什么弱点和强项吗？

4

3 回答 3

82

我对 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 还附带了许多强大的证明自动化程序，例如omegaor congruence，但它们并不普遍适用，并且在 Isabelle/HOL 中可以通过单个命令解决的许多定理需要在 Coq 中进行更明确的证明。

当然，这种便利是有代价的。有人告诉我，在 Isabelle/HOL 中很难控制自己的证明，因为系统试图自己做很多事情。这在证明简单定理时不是问题，但是当证明自动化不够强大并且您需要告诉定理证明者如何更详细地进行时，它就会成为问题。

当支持用户定义的证明自动化程序时，情况会有所不同。Coq 带有一种用于编写证明的策略语言，称为 Ltac，它本身就是一种编程语言。尽管 Ltac 存在一些设计问题，但它确实允许用户以轻量级的方式对相当复杂的证明自动化程序进行编码。对于较重的任务，Coq 还允许用户使用 Coq 的实现语言 OCaml 编写插件。相比之下，在 Isabelle/HOL 中，没有像 Ltac 这样的高级自动化语言，用户编写自定义证明自动化程序的唯一方法是使用插件。

于 2015-05-11T04:13:33.103 回答
24

我将说明 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

我刚刚向您介绍的是将康托尔的经典论点翻译成 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

证明系统能够自动证明康托尔的陈述。对于研究人员来说，一方面这是有帮助的，但在某种意义上这是一把双刃剑。我发现像对角化参数这样复杂的真实陈述可以被信任在 Isabelle/HOL 内部得到证明是有帮助的，因为我的定理因此更加复杂。另一方面，随着计算机自动化进步的推动，我在研究中走得越远，我就越不能解释为什么这个定理是正确的，或者因为什么原理是正确的。只有计算机知道为什么，如果我们能问它！

于 2017-08-14T11:31:17.750 回答
13

由于“Isabelle/HOL”在问题中是精确的，我将讨论 Isabelle 中使用的 HOL 逻辑，我认为这是与 Coq 进行比较的最佳逻辑。我不是类型系统和逻辑方面的专家，但我认为我在这里所说的是正确的，至少大致上是正确的。这当然也是一个品味问题；-) 我的回答可能是主观的。

最深刻的区别在于类型系统和逻辑。

我想说的是，对于了解 ML 家族的功能语言的人（甚至对于了解 SML 的人来说更是如此），它的优势是更自然，并且它使用务实的方法来解决问题，例如使用经典逻辑作为一个依据。它的类型系统接近于 Hindley Milner 的类型系统并且默认终止（如果它没有被用户修改）。

另一方面，Coq 更加严格并且使用直觉逻辑。它有一个专门的类型系统，有几个订单，并允许类型依赖，这可能更难以处理，并且在某些情况下可能是非终止的。它还允许人们从证明中提取程序（这可能效率相对较低），这在 Isabelle 中是无法直接实现的。

于 2015-05-10T22:36:42.617 回答