为什么逻辑连接词和布尔值在Coq中分开？

Question

我来自JavaScript/Ruby编程背景,我习惯这是真/假的工作原理(在JS中):

!true
// false
!false
// true

然后你就可以使用这些真/假值与&&像

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

所以,而不是(和其他逻辑/布尔运算符)是单个系统的一部分; 似乎"逻辑"系统和"布尔"系统是同一个系统.

但是,在Coq中,逻辑和布尔值是两个不同的东西.为什么是这样？下面的引用/链接演示了如何将定理与它们联系起来.

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

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有两个因为它们对不同的东西有用:布尔值对应于可以机械检查的事实(即,使用算法),而命题可以表达更多的概念.

严格来说,逻辑和布尔世界在Coq中并不是分开的:布尔世界是逻辑世界的一个子集.换句话说,你可以将短语作为布尔计算的每个语句都可以被视为一个逻辑命题(即类型的东西Prop):如果b : bool表示一个语句,我们可以断言这个语句是真的,说b = true是哪种类型Prop.

Coq对逻辑的不仅仅是布尔值的原因在于前面语句的相反之处并不成立:并非所有逻辑事实都可以被视为布尔计算.以不同的方式说,它是不是在正常的编程语言如Ruby和JavaScript布尔归入两种情况下bool,并Prop在勒柯克,因为PropS能表达的东西,在这些语言的布尔值不能.

为了说明这一点,请考虑以下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使用更传统的语言翻译谓词.如果这看起来很难,那不是偶然的:有可能证明我们不能编写一个程序,在这些语言中返回一个布尔值来测试一个操作是否可交换.您当然可以编写单元测试来检查特定输入是否为真,例如:

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

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

你可能想知道为什么我们打扰Coq中的布尔值,如果Props可以表达布尔可以做的一切.原因在于Coq是一种建设性的逻辑,这正是Vinz在他的评论中提到的.这个事实最广为人知的结果是,在Coq中我们无法证明以下直观原则:

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

这基本上说每个命题都是真或假."这怎么可能失败？",你可能会问自己.粗略地说,在构造逻辑(特别是Coq)中,每个证明都对应于我们可以执行的算法.特别是,当你证明格式的语句,A \/ B以建设性的逻辑,你可以提取从证明答案是否(总是终止)算法A或B持有.因此,如果我们能够证明上述原则,我们将有一个算法,给定一些命题,告诉我们该命题是否有效.然而,可计算性理论表明,由于不可判定性,这通常是不可能的:如果我们的P意思是"程序p停止输入x",被排除在外的中间人会产生一个停止问题的决定者,这个问题不可能存在.

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

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

因此,在Coq中,将布尔值视为命题的一个特例是有用的,因为它们允许其他命题不具有的推理形式,即案例分析.

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