为什么 Coq 中的逻辑连接词和布尔值是分开的? [英] Why are logical connectives and booleans separate in Coq?

问题描述

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

I come from a JavaScript/Ruby programming background and am used to this being how true/false works (in JS):

!true
// false
!false
// true

然后您可以将这些真/假值与 && 类似

Then you can use those true/false values with && like

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

所以 and 和 not(以及其他逻辑/布尔运算符)是单个系统的一部分；看起来逻辑"系统和布尔"系统是一回事.

So and and not (and other logical/boolean operators) are part of a single system; it seems like the "logical" system and the "boolean" system are one and the same.

然而，在 Coq 中，逻辑和布尔值是两个不同的东西.为什么是这样?下面的引用/链接演示了如何需要一个定理来关联它们.

However, in Coq, logics and booleans are two separate things. Why is this? The quote/link below demonstrates how a theorem is necessary to relate them.

我们已经看到在 Coq 的计算(Type)和逻辑(Prop)世界中可以找到类似结构的几个地方.这里还有一个:布尔运算符 andb 和 orb 显然是逻辑连接词 ∧ 和 ∨ 的类似物.这个类比可以通过以下定理变得更加精确，这些定理展示了如何将关于 andb 和 orb 在某些输入上的行为的知识转化为关于这些输入的命题事实.

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

推荐答案

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

严格来说，逻辑世界和布尔世界在 Coq 中并不是分开的:布尔世界是逻辑世界的一个子集.换句话说，可以将每个可以表述为布尔计算的语句都可以视为一个逻辑命题(即，Prop 类型的东西): if b : bool 表示声明，我们可以通过说 b = true 来断言这个声明是真的，它的类型是 Prop.

Strictly speaking, the logical and boolean worlds are not separate in Coq: the boolean world is a subset of the logical world. In other words, every statement that you can phrase as a boolean computation can be viewed as a logical proposition (i.e., something of type Prop): if b : bool represents a statement, we can assert that this statement is true by saying b = true, which is of type Prop.

在 Coq 中逻辑不仅仅是布尔值的原因是前面的语句的逆不成立:并非所有逻辑事实都可以被视为布尔计算.换句话说，普通编程语言(如 Ruby 和 JavaScript)中的布尔值不会同时包含 Coq 中的 bool 和 Prop，因为 Props 可以表达这些语言中布尔值无法表达的东西.

The reason there's more in Coq to logic than just booleans is that the converse of the previous statement does not hold: not all logical facts can be viewed as boolean computations. Put in a different way, it is not the case that booleans in normal programming languages such as Ruby and JavaScript subsume both bool and Prop in Coq, because Props can express things that booleans in these languages cannot.

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

To illustrate this, consider the following Coq predicate:

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

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

As the name suggests, this predicate asserts that an operator op is commutative. Many operators in programming languages are commutative: take multiplication and addition over integers, for instance. Indeed, in Coq we can prove the following statements (and I believe those are examples in the Software Foundations book):

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

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

Now, try to think how you would translate a predicate like commutative in a more conventional language. If this seems difficult, it is not by chance: it is possible to prove that we can't write a program returning a boolean in these languages to test whether an operation is commutative or not. You can certainly write unit tests for checking whether this fact is true for particular inputs, e.g.:

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

但是，如果您的操作员使用无限数量的输入，这些单元测试只能涵盖所有可能情况的一小部分.因此，测试总是比完整的形式证明要弱.

However, if your operator works with an infinite number of inputs, these unit tests can only cover a fraction of all possible cases. Therefore, testing is always necessarily weaker than a complete formal proof.

如果 Props 可以表达布尔值所能表达的一切，你可能想知道为什么我们还要在 Coq 中使用布尔值.原因是 Coq 是一个 建设性逻辑，这正是 Vinz 在他的评论中所暗示的.这个事实最广为人知的后果是，在 Coq 中我们无法证明以下直观原则:

You could wonder why we bother having booleans in Coq if Props can express everything that booleans can. The reason for that is that Coq is a constructive logic, which is what Vinz was alluding to in his comment. The most well-known consequence of this fact is that in Coq we cannot prove the following intuitive principle:

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

本质上说每个命题要么是真要么是假.这怎么可能失败?"，你可能会问自己.粗略地说，在构造逻辑(尤其是 Coq)中，每个证明都对应于我们可以执行的算法.特别是，当您在构造逻辑中证明 A /B 形式的语句时，您可以从该证明中提取(始终终止)算法来回答是否 A或 B 成立.因此，如果我们能够证明上述原理，我们将有一个算法，给定某个命题，告诉我们该命题是否有效.然而，可计算性理论表明，由于不可判定性，这通常是不可能的:如果我们将 P 表示程序 p 在输入 x"，排除的中间将产生 停止问题的决策者，该问题不存在.

which essentially says that every proposition is either true or false. "How could this possibly fail?", you might ask yourself. Roughly speaking, in constructive logics (and Coq in particular), every proof corresponds to an algorithm we can execute. In particular, when you prove a statement of the form A / B in a constructive logic, you can extract an (always terminating) algorithm from that proof that answers whether A or B holds. Hence, if we were able to prove the above principle, we would have an algorithm that, given some proposition, tells us whether that proposition is valid or not. Computability theory shows, however, that this is not possible in general because of undecidability: if we take P to mean "program p halts on input x", the excluded middle would yield a decider for the halting problem, which cannot exist.

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

Now, what's interesting about booleans in Coq is that by construction they allow the use of the excluded middle, because they do correspond to an algorithm we can run. Specifically, we can prove the following:

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

因此，在 Coq 中，将布尔值视为命题的特殊情况是有用的，因为它们允许进行其他命题所不具备的推理形式，即案例分析.

Thus, in Coq it is useful to consider booleans as a special case of propositions because they allow forms of reasoning that other propositions do not, namely, case analysis.

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

Of course, you can think that requiring that every proof correspond to an algorithm is silly, and indeed most logics allow the principle of the excluded middle. Examples of proof assistants that follow this approach by default include Isabelle/HOL and the Mizar system. In these systems, we don't have to have a distinction between booleans and propositions, and they are treated as the same thing. Isabelle, for instance, has just bool, and no Prop. Coq also allows you to blur the distinction between booleans and propostions, by assuming axioms that allow you to perform case analysis on general propositions. On the other hand, in such a setting, when you write a function that returns a boolean, you might not obtain something that you can execute as an algorithm, whereas this is always the case by default in Coq.

这篇关于为什么 Coq 中的逻辑连接词和布尔值是分开的?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！