boolean - 为什么 Coq 中的逻辑连接词和 boolean 值是分开的？

Question

我来自 JavaScript/Ruby 编程背景，并且习惯了 true/false 的工作方式(在 JS 中):

!true
// false
!false
// true

然后你可以使用这些真/假值 &&喜欢

var a = true, b = false;
a && !b;

So and and not(以及其他逻辑/boolean 运算符)是单个系统的一部分；似乎“逻辑”系统和“boolean ”系统是一回事。

然而，在 Coq 中，逻辑和 boolean 值是两个独立的东西。为什么是这样？下面的引用/链接演示了如何需要定理来将它们联系起来。

We've already seen several places where analogous structures can be found in Coq's computational (Type) and logical (Prop) worlds. Here is one more: the boolean operators andb and orb are clearly analogs of the logical connectives ∧ and ∨. This analogy can be made more precise by the following theorems, which show how to translate knowledge about andb and orb's behaviors on certain inputs into propositional facts about those inputs.

Theorem andb_prop : ∀b c,
  andb b c = true → b = true ∧ c = true.

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211

Answer 1

本质上，Coq 两者兼备，因为它们对不同的事情有用: boolean 值对应于可以机械检查的事实(即，使用算法)，而命题可以表达更多的概念。

严格来说，逻辑世界和 boolean 世界在 Coq 中并不是分开的: boolean 世界是逻辑世界的一个子集。换句话说，您可以将其表述为 boolean 计算的每个语句都可以视为一个逻辑命题(即 Prop 类型的东西): if b : bool代表一个陈述，我们可以通过说 b = true 来断定这个陈述是正确的。 , 类型为 Prop .

Coq 中的逻辑不仅仅是 boolean 值的原因是前一个语句的逆向不成立:并非所有逻辑事实都可以被视为 boolean 计算。换句话说，普通编程语言(如 Ruby 和 JavaScript)中的 boolean 值并不是同时包含 bool 的情况。和 Prop在 Coq 中，因为 Prop s 可以表达这些语言中 boolean 值不能表达的东西。

为了说明这一点，请考虑以下 Coq 谓词:

Definition commutative {T} (op : T -> T -> T) : Prop :=
  forall x y, op x y = op y x.

顾名思义，该谓词断言运算符 op是可交换的。编程语言中的许多运算符都是可交换的:例如，对整数进行乘法和加法。事实上，在 Coq 中我们可以证明以下陈述(我相信这些都是软件基础书中的例子):

Lemma plus_comm : commutative plus. Proof. (* ... *) Qed.
Lemma mult_comm : commutative mult. Proof. (* ... *) Qed.

现在，试着想想如何翻译像 commutative 这样的谓词。用更传统的语言。如果这看起来很困难，那并非偶然:可以证明我们无法用这些语言编写返回 boolean 值的程序来测试操作是否可交换。您当然可以编写单元测试来检查此事实对于特定输入是否正确，例如:

2 + 3 == 3 + 2
4 * 5 == 5 * 4

但是，如果您的运算符(operator)处理无限数量的输入，则这些单元测试只能涵盖所有可能情况的一小部分。因此，测试总是比完整的形式证明弱。

如果 Prop，你可能想知道为什么我们要在 Coq 中使用 boolean 值。 s 可以表达 boolean 值所能表达的一切。这样做的原因是 Coq 是一个 build 性的逻辑，这就是 Vinz 在他的评论中所暗示的。这一事实最广为人知的结果是，在 Coq 中我们无法证明以下直观原则:

Definition excluded_middle :=
  forall P : Prop, P \/ ~ P.

它本质上是说每个命题要么是真的，要么是假的。 “这怎么可能会失败？”，您可能会问自己。粗略地说，在构造逻辑(尤其是 Coq)中，每个证明都对应于我们可以执行的算法。特别是，当您证明形式为 A \/ B 的陈述时在构造逻辑中，您可以从该证明中提取(始终终止)算法来回答是否 A或 B持有。因此，如果我们能够证明上述原则，我们将有一个算法，该算法在给定某个命题时告诉我们该命题是否有效。然而，可计算性理论表明，由于不可判定性，这在一般情况下是不可能的:如果我们取 P表示“程序 p 在输入 x 时停止”，排中将产生 halting problem 的判定器，不能存在。

现在，Coq 中 boolean 值的有趣之处在于，通过构造它们允许使用排中，因为它们确实对应于我们可以运行的算法。具体来说，我们可以证明以下几点:

Lemma excluded_middle_bool :
  forall b : bool, b = true \/ negb b = true.
Proof. intros b; destruct b; simpl; auto. Qed.

因此，在 Coq 中，将 boolean 值视为命题的特例是有用的，因为它们允许其他命题所不具备的推理形式，即案例分析。

当然，你可以认为要求每个证明都对应一个算法是愚蠢的，事实上大多数逻辑都允许排中原则。默认情况下遵循此方法的证明助手示例包括 Isabelle/HOL和 Mizar系统。在这些系统中，我们不必区分 boolean 值和命题，它们被视为同一事物。例如，伊莎贝尔只有 bool ，并且没有 Prop . Coq 还允许您通过假设允许您对一般命题执行案例分析的公理来模糊 boolean 值和命题之间的区别。另一方面，在这种情况下，当您编写一个返回 boolean 值的函数时，您可能无法获得可以作为算法执行的内容，而在 Coq 中默认情况下总是如此。