为什么逻辑连接词和布尔值分设于勒柯克？ [英] Why are logical connectives and booleans separate in Coq?

问题描述

我来自一个JavaScript / Ruby编程背景并习惯了对这个是怎么真/假作品（JS中）：

 ！真
//假
！假
//真
 

然后就可以使用这些真/假值与＆放大器;＆安培; 像

  VAR一个= TRUE，B = FALSE;
一个与放大器;＆放大器; ！B：
 

所以的和的和的不的（和其他逻辑/布尔操作）是一个系统的一部分;这似乎是逻辑系统和布尔的系统是同一个。

不过，在勒柯克，逻辑和布尔值是两回事。为什么是这样？下面的引文/链接演示了如何定理是必要的关联起来。

  

我们已经看到了几个地方，类似的结构可以在勒柯克的计算（类型）和逻辑（命题）的世界中找到。下面是多了一个：布尔运算符和b和ORB显然是逻辑连接词∧和∨的类似物。这种类比可以通过以下定理，它显示了如何知识关于某些投入约这些输入命题事实和b和ORB的行为翻译变得更precise

 定理andb_prop：∀bC，
  ANDB B C = TRUE→B =真∧C =真。
 

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

解决方案

的从本质上讲，勒柯克既有因为它们是不同的东西有用：布尔值对应于可机械地进行检查（即用一种算法）的事实，而命题不能前preSS更多的概念。的

严格地说，逻辑和布尔世界中不勒柯克分开：布尔世界是逻辑世界的一个子集。换句话说，每一个可以短语作为布尔运算可以被看作是一个逻辑命题陈述（即类型的东西道具）：如果乙：BOOL 重新presents一份声明中，我们可以断言，这种说法说是真实的 b = TRUE ，这是类型道具。

的原因有更多在勒柯克到逻辑不仅仅是布尔值是previous语句的逆不成立：不是所有的逻辑事实可以看作是布尔运算的。以不同的方式说，它是不是这样的，在正常的编程语言如Ruby和JavaScript布尔归入两个布尔和道具在勒柯克，因为道具 S能恩preSS的东西，在这些语言布尔不能。

要说明这一点，考虑以下勒柯克predicate：

 定义交换【T】（OP：笔 - ＆GT;笔 - ＆GT; T）：道具：=
  FORALL x和y，运算x和y =运算Y X。
 

顾名思义，这predicate称，运营商运是可交换的。在编程语言中许多运营商是可交换的：采取乘法和加法以上的整数，例如。事实上，勒柯克我们可以证明下面的语句（我相信这些都是在软件基础本书的例子）：

 引理plus_comm：可交换加。证明。 （*。*）QED。
引理mult_comm：可交换MULT。证明。 （*。*）QED。
 

现在，再想想你将如何在更传统的语言翻译了predicate像可交换。如果这似乎很难，这不是偶然的：它可以证明我们不能写一个程序返回这些语言的布尔测试操作是否是可交换与否。你当然可以写的单元测试的检查这一事实是否是特定输入真实的，例如：

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

不过，如果你的运营商，投入无限多的作品，这些单元测试只能覆盖所有可能的情况下，一小部分。因此，测试始终是一定比一个完整的正式证明弱。

您可能想知道为什么我们懒得勒柯克具有布尔值，如果道具 S能恩preSS的一切，布尔可以。其原因是，勒柯克是的建设性的逻辑的，这是什么Vinz在他的评论暗示。这一事实的最有名的后果是，在勒柯克我们不能证明以下直观的原则：

 定义excluded_middle：=
  FORALL病人：道具，P \\ /〜P。
 

基本上说，每一个命题是真或假。 怎么会这样可能会失败？，你可能会问自己。粗略地说，建设性的逻辑（和勒柯克尤其是），每一个证明对应的算法，我们可以执行。特别是，当你证明形式的语句 A \\ / B 以建设性的逻辑，你可以提取证明了这一点，回答是否<$的（总是终止）算法C $ C> A 或 B 保存。因此，如果我们能够证明上述原则，我们将有一个算法，给出了一些命题，告诉我们主张是否有效。可计算性理论可知，不过，这不是一般的，因为不可判定的可能：如果我们采取 P 来表示节目 P 停止输入 X ，排除中间会产生一个决胜局的停机问题，这是不能存在的。

现在，什么是关于勒柯克布尔有趣的是，由建设，他们允许使用排中，因为他们的做的对应的算法，我们可以运行。具体来说，我们可以证明如下：

 引理excluded_middle_bool：
  FORALL乙：BOOL，B =真\\ / negb B =真。
证明。前奏B：销毁B： SIMPL;汽车。 QED。
 

因此​​，在勒柯克是有用的考虑布尔作为命题的一个特例，因为它们允许推理形式的其他命题不这样做，即案例分析。

当然，你可以认为这要求每一个证明对应的算法是愚蠢的，而事实上大多数逻辑允许排中的原则。在默认情况下采用这种做法证明助手的例子包括伊莎贝尔/ HOL 和的开阳系统。在这些系统中，我们不必有布尔和命题之间的区别，它们被视为同样的事情。伊莎贝尔，例如，刚刚布尔，没有道具。 COQ，您还可以通过假定的公理，让您在一般主张进行案例分析模糊布尔和propostions，之间的区别。在另一方面，在这样的设置，当你写一个返回boolean值的功能，你可能不会得到的东西，你可以执行作为一个算法，而这是始终默认勒柯克的情况。

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;

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.

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.

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

解决方案

Essentially, Coq has both because they are useful for different things: booleans correspond to facts that can be checked mechanically (i.e., with an algorithm), whereas propositions can express more concepts.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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