谓词逻辑速成
原文由 Hillel Wayne 于 发布,订阅该博客
我开始写Logic for Programmers是因为当时根本找不到适合程序员看的逻辑学资料——嗯,给程序员看的。现在书已经出版了,新的问题又来了:还是找不到好的、免费的、给程序员看的逻辑学资料。
所以,为了解决这个问题(顺便也给书做点宣传),我把《Logic for Programmers》第二章改成了这篇博客文章。所有脚注都是编辑性的补充说明,书里没有。1 祝阅读愉快!
第二章:逻辑学速成
形式逻辑是一个非常强大的工具,但它本身又非常简单。在这一章里,我们会循序渐进地介绍基本概念和语法,包括谓词、蕴含算子、集合以及集合量词。其中很多内容,有编程经验的你可能已经很熟悉了!
谓词
粗略地说,谓词就是返回布尔值的函数。作为程序员,你大概已经写过几十个谓词了。比如下面这些都是谓词:
Positive(x)当 x 大于 0 时为真。IsSum(x, y, z)当 x 加 y 等于 z 时为真。RAMAtLeast(c, r)当计算机c拥有至少r字节的物理内存时为真。
我之所以说“粗略地说”,是因为谓词是一个数学概念,而不是编程结构。程序中的函数必须提供计算结果的方法,而谓词只需要定义结果是什么。以 RAMAtLeast 为例,它的软件实现会取决于编程语言、操作系统,甚至具体的物理硬件。但作为谓词呢?计算机有这么多内存就是真,没有就是假。就这么简单。
这意味着谓词可以比编程函数更抽象,可以表达那些我们根本无法计算、或者至少暂时还不知道如何计算的东西。下面这些也都是合法的谓词:
CanRunProgram(c)当计算机c能够运行我们的程序时为真,无论“能够”最终被定义成什么。RainyDayInCa(date)当date这一天加拿大某地下过雨时为真。NotAlone()当外星人真的存在时为真。
另一方面,Positive(x) 很容易计算:只要检查 x > 0 是否成立就行。谓词的强大之处在于它能横跨整个抽象层次。为了区分抽象谓词和具体谓词,我们来引入一套写法:如果一个谓词是抽象的,我就用 `反引号` 把它的定义体包起来:
# concrete
Positive(x) = x > 0
IsSum(x, y, z) = x + y == z
# abstract
CanRunProgram(c) = `c can run our program`这并不是数学家的通用约定,但对我们的目的来说已经足够清晰。为了把谓词和像 add_two 这样的“普通”函数区分开,谓词一律用 大驼峰命名,函数一律用 下划线命名。
在你写过的程序里找几个谓词。它们是抽象谓词还是具体谓词?
解答
谓词通常是那些不改变程序或外部状态、只返回布尔值的函数。我最近写过的一个是 document_has_exactly_one_foo。你找到的谓词应该都属于具体谓词,因为“抽象”谓词本来就没法真正写成代码。不过在设计文档里,你倒是可能会看到一两个抽象谓词。
既然谓词返回布尔值,现在正好把布尔运算说清楚。不同的编程语言对“与”“或”(相容或)和“非”有不同的符号。数学家用 ∧、∨、¬。我不打算用这些,因为键盘上打不出来。取而代之,我们用 &&、|| 和 ! 作为符号。所以 X && !Y 的意思就是“X 为真且 Y 为假”。2
除了这三种常见的布尔算子,数学家还承认第四种,=>。不过在解释它的含义之前,我们先来练习一下刚学到的内容。
实践示例
谓词在我们用自然语言描述系统和用编程语言实现系统之间起到了桥梁作用。回到 CanRunProgram。我曾见过一个程序有这样的需求:
计算机必须拥有足够的内存,并且拥有高速 CPU 或优质显卡(GPU)。
我觉得这句话很含糊。在英语里听起来倒是挺自然,但一旦用逻辑形式化,问题就暴露出来了。我们先为每个子需求写一个谓词,像这样:
RAM(c) = `c has enough RAM`
CPU(c) = `c has a fast CPU`
GPU(c) = `c has a good GPU`这些谓词是抽象的,因为我们还不知道它们具体指什么。64GB 算“足够的内存”吗?32GB 呢?具体是多少对我们并不重要,因为仅凭这些就足以把 CanRunProgram 写成一个具体的数学表达式。
CanRunProgram(c) = RAM(c) && CPU(c) || GPU(c)现在问题更清楚了:a && b || c 到底应该理解为 (a && b) || c,还是 a && (b || c)?这个谓词写法不规范,我们可以用两种不同的方式让它变得明确:
# way 1
CanRunProgram(c) = RAM(c) && (CPU(c) || GPU(c))
# way 2
CanRunProgram(c) = (RAM(c) && CPU(c)) || GPU(c)两种理解用英语说都通!但在某些输入下,它们的输出完全不同。我们可以通过列出 RAM/CPU/GPU 的所有可能取值组合,看看它们对 CanRunProgram 的结果有何影响。这就是所谓的真值表。3
| R (RAM) | C (CPU) | G (GPU) | R && (C OR G) | (R && C) OR G |
|---|---|---|---|---|
| T | T | T | T | T |
| T | T | F | T | T |
| T | F | T | T | T |
| T | F | F | F | F |
| F | T | T | F | T |
| F | F | T | F | T |
| F | T | F | F | F |
| F | F | F | F | F |
有两种输入组合会让一种解释得到“假”,另一种得到“真”。很有可能,厂商写需求时想的是第一种意思,而我却理解成了第二种。我确信程序在我的电脑上能跑,结果却因为内存不足而失败,于是我觉得厂商骗了我。还是用数学方式来表达需求要好得多!
用形式逻辑来表达性质,比用非正式的英语要精确得多。为了教学方便,我们假设原本想表达的谓词是 (RAM(c) && CPU(c)) || GPU(c)。
我们将在《决策表》一章中用真值表来进行分情况分析。4
如果你在生成真值表时遇到困难,可以试试真值表生成器。我在这里提供了一个简单的工具。试试 p || !q,然后在此基础上多做些尝试。
为 !P && !Q 和 !(P || Q) 制作真值表。
解答
| P | Q | !P && !Q | !(P OR Q) |
|---|---|---|---|
| T | T | F | F |
| T | F | F | F |
| F | T | F | F |
| F | F | T | T |
两者是一样的。这就是德摩根定律。
条件谓词
接下来我们来给谓词做个变体。还是以 CanRunProgram 为例:有些程序有原生版和网页版。原生版会使用本地计算机的资源,而网页版则把大部分计算放在云端的某台机器上。所以原生版需要一台配置很高的电脑,而网页版在任何电脑上都能跑。
如果计算机运行的是原生版,那么它必须拥有足够的内存以及高速 CPU 或优质显卡(GPU)才能使用该程序。但如果运行的不是原生版,那就没问题。
为了对它建模,我们需要一个新的谓词 Native(p)。Native 是程序的属性,而不是计算机的属性,所以 CanRunProgram 接下来会同时依赖两者:
CanRunProgram(c, p) = `true unless Native(p),
in which case (RAM(c) && CPU(c)) || GPU(c)`这里我用了反引号,因为这个谓词有一半还是用非正式英语写的。实际上,我们已经有了让它变得具体所需的工具。每当 Native(p) 为假时,CanRunProgram(c, p) 就应该自动为真:我们根本不需要去看计算机的配置。
CanRunProgram(c, p) =
!Native(p) || ((RAM(c) && CPU(c)) || GPU(c))这是怎么起作用的?如果我们把右半部分抽出来作为一个新的谓词,比如 Beefy(c),得到 !Native(p) || Beefy(c),就更容易看明白了。下面是这个表达式的真值表(用 N(p) 表示 Native(p),用 B(c) 表示 Beefy(c)):
| N(p) | B(c) | !N(p) OR B(c) |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
当 Native(p) 为假时,无论 Beefy(c) 取什么值,!Native(p) || Beefy(c) 都是真。当 Native(p) 为真时,整个表达式的值就等于 Beefy(c) 的值。所以我们只有在运行原生版时才检查计算机配置,否则就直接忽略。
用 !P || Q 来表示“只有当 P 为真时才检查 Q”这一技巧在数学中极其常见。常见到数学家为它专门设了一个算子:=>,即蕴含算子。P => Q(“P 蕴含 Q”)就等同于 !P || Q。用这种写法,我们的谓词就是:
CanRunProgram(c, p) =
Native(p) => (RAM(c) && CPU(c)) || GPU(c)=> 的结合优先级比 && 和 || 更低:A && B => C 指的是 (A && B) => C,而不是 A && (B => C)。
蕴含算子非常强大,在很多场景下都派得上用场,比如编写规约或构建系统模型。此外,我们还可以用它来表示一个布尔命题比另一个“更强”。5 例如,“这段代码传入 0 时会崩溃”就比“这段代码有 bug”更强。如果它在某个输入上崩溃,那它肯定有 bug!但即使程序没有崩溃,它也可能存在像差一错误这样的 bug。用数学写法就是:
CrashesOnInput(code, 0) => HasBug(code)蕴含还有一个有用的性质是传递性。如果 P => Q 且 Q => R,那么我们就知道 P => R,无论 P、Q、R 具体是什么。比如,如果 CanRenderVideo(c) => CPU(c) && RAM(c),那么 CanRenderVideo(c) => CanRunProgram(c)。
假设我们再加两个条件,让 CanRunProgram 变成
CanRunProgram(c, p) =
`true unless Native(p) and either Q(p) or R(p),
in which case (RAM(c) && CPU(c)) || GPU(c))`用 => 来写出它。再不用 => 写一遍。哪一种更易读?
解答
Native(p) && (Q(p) || R(p)) => (RAM(c) && CPU(c)) || GPU(c)!(Native(p) && (Q(p) || R(p))) || ((RAM(c) && CPU(c)) || GPU(c))
我个人觉得(1)更易读,因为嵌套的表达式更少。
RAM(c) 表示“计算机 c 有足够的内存”。把它改成表示“计算机 c 有足够的内存来运行程序 p”。对其他谓词也做类似修改,并写出 CanRunProgram。
解答
CanRunProgram(c, p) =
Native(p) => (RAM(c, p) && CPU(c, p)) || GPU(c, p)- 用
=>写出表达式“如果Native(p)为真则Web(p)为假,且如果Web(p)为真则Native(p)为假”。 - 用
&&写出表达式“Native(p)和Web(p)不会同时为真”。 - 用
||写出表达式“Native(p)为假或Web(p)为假”。
解答
(Native(p) => !Web(p)) && (Web(p) => !Native(p))!(Web(p) && Native(p))!Native(p) || !Web(p)
来看这个谓词:
IfElse(c, x, y) =
(c => x) && (!c => y)假设 c、x 和 y 都是布尔值。
IfElse何时为真?何时为假?- 这像哪种常见的代码结构?
解答
(c => x) && (!c => y)等价于(!c || x) && (c || y)。逐一分析各种情况,你会发现当 c 为真且 x 为真,或 c 为假且 y 为真时,IfElse为真。顾名思义,
IfElse模拟的就是条件分支。
集合
谓词的输入默认是无类型的。在 CanRunProgram(c) 中,c 可以是一台计算机,也可以是一个机器人,或者数字 26,甚至是字符串“数字 26”。在编程中,我们会想给它加上类型,以明确应该只传入计算机。比如:
CanRunProgram(c) = `c is a computer`
&& ((RAM(c) && CPU(c)) || GPU(c))这样一来,即使我们把一块好显卡粘到一只贵宾犬身上,CanRunProgram(poodle) 仍然是假。为了让“c 是一台计算机”这个概念能在数学上表示,数学家引入了集合。集合是唯一值的无序聚集,比如“所有计算机”、“所有小于 500KB 的网页”或“所有合法的 Java 程序字符串”。按惯例,我们这样写集合的元素:
Computer = {my_laptop, your_laptop, your_other_laptop, ... }那么“c 是一台计算机”就等价于说“c 是集合 Computer 的一个元素”。我们把它写作 c in Computer。
CanRunProgram(c) = c in Computer && ((RAM(c) && CPU(c)) || GPU(c))为了让谓词定义更简洁,我借用一种常见的编程语法,把 CanRunProgram(c: Computer) 记作“c 必须是 Computer 的元素”,像这样:
CanRunProgram(c: Computer) = (RAM(c) && CPU(c)) || GPU(c)这样在编写带有多个受限参数的谓词时会更方便。
数学家把集合当作构建更复杂概念的数学基石。例如,他们可能会用集合来定义有序对,把 (a, b) 写成 {a, {b}},6 然后把列表 [a, b, c] 定义为有序对的集合 {(0, a), (1, b), (2, c)}。7 有了基于集合的列表“抽象”实现后,他们就可以丢掉集合,直接使用列表了。
作为程序员,我们在使用列表之前不需要先写出列表的形式化定义,本来就更倾向于直接使用这个更复杂的抽象。即便如此,集合仍然是一种有用的编程数据类型。我们会在下一章看到这一点。
集合运算
就像我们有数的算术和布尔值的算术一样,我们也有集合的算术。给定集合 {A, B} 和 {B, C},我们可以做的基本操作有:
- 并集:把它们拼成一个大集合:
{A, B} | {B, C} == {A, B, C} - 交集:找出共同的元素:
{A, B} & {B, C} == {B} - 差集:从一个集合中减去另一个:
{A, B} - {B, C} == {A}
我们还可以判断一个集合是否是另一个的子集。EvenIntegers 是 Integers 的子集,因为 EvenIntegers 的每个元素也都是 Integers 的元素。值 2 不是 Integers 的子集,但集合 {2} 是。子集类似于编程语言中的子类型。8 如果一门语言说“Rectangle 是 Shape 的子类型”,意思就是所有矩形的集合是所有图形集合的子集。我们会在更广义的“合约”主题中更详细地讨论子类型。
利用集合
ram、cpu和gpu来构造集合can_run_program,即所有满足CanRunProgram(c)的计算机的集合。给定集合
Child和Adult,用“集合互不重叠”的方式来表达“没有人既是儿童又是成年人”。你可以用{}表示空集。两个集合的对称差是恰好只属于其中一个集合的所有元素的集合。例如,
{A, B}和{B, C}的对称差是{A, C}。仅使用基本的集合运算,求任意集合S和T的对称差。
解答
can_run_program = (ram & cpu) | gpuChild & Adult == {}。另一种写法是Child - Adult == Child && Adult - Child == Adult。一种写法是
(S - T) | (T - S);另一种是(S | T) - (S & T)。
对集合进行映射和过滤也非常有用。标准的数学记法是 {f(x) | P(x)},但我发现初学者经常搞不清哪边是映射、哪边是过滤。所以在本书中,我会使用一种更直观的语法:
| 名称 | 语法 |
|---|---|
| 映射 | {x^2 for x in set} |
| 过滤 | {x in set: x > 2} |
| 映射并过滤 | {x^2 for x in set: x > 2} |
例如,所有偶数的集合是 {x in Int: x % 2 == 0},而所有偶数的平方根的集合是 {sqrt(x) for x in Int: x % 2 == 0}。这种写法有时被称为集合推导或集合构造记法。之后,集合推导将成为我们理解数据库查询的基础。
设 Images 是一个图像集合,其中每张图像是一条记录,包含名称、高度、宽度和以 KB 为单位的大小字段。请用集合推导写出:
- 所有图像名称的集合。
- 所有大于 10 KB 的图像的集合。
- 所有正方形图像的高度集合。
解答
{img.name for img in Images}{img in Images: img.size > 10}{img.height for img in Images: img.height == img.width}
量词
我们暂时离开软件需求,换一个问题。软件开发团队常常要求对主分支的改动必须先以拉取请求(pull request)的形式提出,并由另一名团队成员审查。更简洁地说:
拉取请求在合并前必须经过团队成员的审查。
假设我们有两个集合 PullRequest 和 Developer,可以在谓词中使用。我可以先用这些抽象谓词来表达这条规则:
ReviewedBy(pr: PullRequest, d: Developer) =
`d reviewed pull request pr`
CanMerge(pr: PullRequest) = `someone reviewed pr`这两个谓词都是抽象的,但我们似乎应该能通过 ReviewedBy 把 CanMerge 定义得更具体。
为此我们需要量词,也就是作用于整个集合的逻辑表达式。谓词逻辑中常见的量词有两个。我们先来看其中一个,some。
some
some x in set: P(x) 表示在集合 set 中至少存在一个 x 使得 P(x) 为真。
CanMerge(pr: PullRequest) =
some d in Developer: ReviewedBy(pr, d)我会这样读它:“对于拉取请求元素 pr,如果在开发者集合中至少存在一个元素 d 使得 ReviewedBy(pr, d) 为真,那么 CanMerge 为真”。或者更简单地说,“存在某个开发者审查了这个拉取请求”。

值 d 被称为变量。关键字 some 是在对集合 Developer 进行量化,或者说,它的作用域是这个集合。这使得我们对它的使用成为有界量词。更少见的情况下,一个表达式对我们任意指定的值都为真。例如,命题 some x in set: (P(x) && Q) 等同于 Q && some x in set: P(x),无论 set 是什么。在这种情况下,我们可以选择省略集合,直接写作:
(some x: (P(x) && Q)) == (Q && some x: P(x))这种 some 的用法没有限定在某个集合上,所以我们称之为无界量词。我们使用的几乎所有量词都是有界的。
为了防止出现可怕的数学灾难,我们只能对集合和值进行量化,不能对谓词量化。如果想了解更多关于这种可怕灾难的内容,请查看附录《超越逻辑》。
all
就目前而言,CanMerge 还是太宽松了。如果审查者发现了重大安全缺陷怎么办?如果有五名开发者审查了拉取请求,其中两人发现了问题呢?大多数公司会采用更严格的合并要求:
拉取请求必须至少经过一名团队成员的审查,并且所有审查者都必须批准,才能合并。
按照惯例,我们先把需求写成抽象谓词。
ApprovedBy(pr: PullRequest, d: Developer) = `d approved pr`
SomeoneReviewed(pr: PullRequest) =
some d in Developer: ReviewedBy(pr, d)
EveryoneApproves(pr: PullRequest) =
`everyone who reviewed pr also approved it`
CanMerge(pr: PullRequest) =
SomeoneReviewed(pr) && EveryoneApproves(pr)这正好让我们引入另一个量词:all。all x in set: P(x) 表示对于集合中的每一个 x,P(x) 都为真。有了它,我们的新谓词似乎可以这样写:
EveryoneApproves(pr: PullRequest) =
all d in Developer: Approved(pr, d)但这样写是错的:它要求每一位开发者都批准这个拉取请求,包括那些请病假或休产假的开发者。我们只想要求那些审查过该拉取请求的开发者都批准了它。我们可以用蕴含来修正。回想一下,P => Q 等同于 !P || Q。那么 ReviewedBy(pr, d) => Approved(pr, d) 的意思就是,要么 d 批准了这个拉取请求,要么他根本没有审查过。
EverybodyApproves(pr: PullRequest) =
all d in Developer: ReviewedBy(pr, d) => Approved(pr, d)我们经常用 => 来把 all 限制在元素的某个子集上。
大多数编程语言都有内置的量词函数,我们会在后面的章节中讨论。如果你的语言没有,通常也可以用循环来模拟量词。例如,你可以用这样的伪代码来实现 SomeoneReviewed:
fun SomeoneReviewed(pr: PR) {
for (d in developers) {
if(ReviewedBy(pr, d)) return true;
}
return false;
}我们为什么还需要 SomeoneReviewed?难道不是只要所有审查过 PR 的人都批准了,就一定有人审查过了吗?请找出 EveryoneApproved 为真而 SomeoneReviewed 为假的边界情况。
解答
如果没有任何开发者审查过这个 PR,那么 EveryoneApproved 为真(零个审查者全部批准了!),而 SomeoneReviewed 为假(没人审查)。
一般来说,all x in {}: P(x) 恒为真(无论 P 是什么),而 some x in {}: P(x) 恒为假。
设 Nat 为自然数集合:0、1、2 等。
- 写出逻辑命题“每个自然数都小于它自身加 1”。
- 写出逻辑命题“0 小于或等于每个自然数”。
解答
all x in Nat: x < x + 1all x in Nat: 0 <= x
- 写出逻辑命题“对于每一个 PR,都存在一名批准了它的开发者”。
- 写出逻辑命题“存在一名开发者审查过每一个拉取请求”。
两种情况都需要在一个量词内部嵌套另一个量词。
解答
all pr in PR: some d in Developer: ApprovedBy(pr, d)some d in Developer: all pr in PR: ReviewedBy(pr, d)
能力-保障权衡
既然已经见过 all 和 some,我想指出一个重要的现象:some x in set: P(x) 在大集合上更有可能为真,而 all x in set: P(x) 在小集合上更有可能为真。如果有两个不同的集合且 set1 是 set2 的子集,我们应该能找到某个谓词 P(x),使得 all x in set1: P(x) 成立,而 some x in set2: !P(x) 也成立。我们可以说 set1 保障了 P(x)。来看三个例子:
“所有 ASCII 字符”集合是“所有 Unicode 字符”集合的子集。ASCII 保障了每个可表示的字符恰好占一个字节,所以看到字符串
ABC我就能立刻知道它是三个字节。Unicode 则不提供这种保障,字符串ABC如果用的是西里尔字母,可能是六个字节。“对文件拥有只读权限时能做的事”这个集合,是“拥有完全访问权限时能做的事”集合的子集。只读访问保障了程序不会修改文件内容。而拥有完全访问权限时,任何有 bug 的程序都可能覆盖我们的数据。
“仅使用布尔值、与、或、非的所有逻辑公式”集合,是“所有逻辑公式”集合的子集。前者保障了每个公式都能转化为真值表。那你怎么为
some x in Nat: OddPerfectNumber(x)做真值表呢?你做不到。数学家至今都不知道它是真还是假!
与此同时,我们又需要 Unicode 来表示 emoji,需要写权限来更新数据,需要集合量词来表达大多数有趣的谓词。这就是能力-保障权衡:一种语言、格式或工具能做的事情越多,它能给我们的保障就越少。10
我们在本书的几乎每一章都会看到这种权衡。
重写规则
在本书开头我说过,逻辑之于布尔值,就如同算术之于数字。掌握算术能让我们化简数值表达式。例如,我们可以这样化简函数 f(x, y) = -10x + 2(y + 5x):
2(y + 5x)等同于2y + 10x。-10x + 2y + 10x等同于10x - 10x + 2y。- 前两项互为相反数,所以抵消了。
- 于是我们得到
f(x, y) = 2y。
在逻辑中,这些化简被称为重写规则。你小时候可能已经用过一条重写规则:
你道歉了吗?没有?那你是不是不不不不道歉?
这里的重写规则是 !!a == a。这意味着 !!(!!Sorry) 就等同于 Sorry。
我们在逻辑中常用的一些重写规则有:
| 名称 | 表达式 | 等价形式 |
|---|---|---|
| 德摩根定律 | !(p && q) | !p OR !q |
!(p OR q) | !p && !q | |
| 与/或分配律 | p && (q OR r) | (p && q) OR (p && r) |
p OR (q && r) | (p OR q) && (p OR r) | |
| 恒等律 | p OR false | p |
p && true | p |
蕴含算子也有重写规则。其中一条,逆否命题,对我们会非常有用。
| 名称 | 表达式 | 等价形式 |
|---|---|---|
| 定义 | p => q | !p OR q |
| 逆否命题 | p => q | !q => !p |
| 导出律 | (p && q) => r | p => (q => r) |
量词也有重写规则:
| 名称 | 表达式 | 等价形式 |
|---|---|---|
| 对偶性 | all x: !P(x) | !(some x: P(x)) |
some x: !P(x) | !(all x: P(x)) | |
| 分配律 | some x: (P(x) OR Q(x)) | (some x: P(x)) OR some x: Q(x) |
all x: (P(x) && Q(x)) | (all x: P(x)) && all x: Q(x) | |
| 常量提取 | all x: (P(x) OR Q) | Q OR all x: P(x) |
常量提取适用于任何与 || 或 && 搭配的量词。分配律则只适用于 some/|| 和 all/&&。
有些规则比其他规则更常用。接下来我们会大量使用德摩根定律、逆否命题和量词对偶性。更完整的列表见《重写规则》。即使是一些冷门的规则,在重构代码时也可能非常有用。
使用重写规则化简 !(some x: !P(x))。
解答
all x: P(x)为每条分配律各举一个现实生活中的例子。
解答
这是我想到的两个例子:
- “本周每天都温暖且晴朗”等同于“本周每天都温暖且每天都晴朗”。
- “有人有蓝眼睛或绿眼睛”等同于“有人有蓝眼睛或有人有绿眼睛”。
some 只对 || 满足分配律,all 只对 && 满足。请找出满足以下条件的谓词:
(some x: P(x)) && (some x: Q(x)) != some x: P(x) && Q(x)all x: P(x) || Q(x) != (all x: P(x)) || (all x: Q(x))
提示:在两种情况下,都让等式左边为真、右边为假。
解答
答案有很多,这里只给出两种(假设 Person 是所有曾活过的人的集合):
(some p in Person: Alive(p)) && (some p in Person: Dead(p))为真,some p in Person: (Alive(p) && Dead(p))为假。all p in Person: Alive(p) || Dead(p)为真,all p in Person: Alive(p) || all p in Person: Dead(p)为假。
定理
你可能听说过数学家会去证明定理。定理只是一个恒为真的数学命题,而证明则是一系列清晰的步骤,让你从已知为真的事实出发,最终说明该定理为真。
我列出的每一条重写规则都是定理,我们可以证明它们总是成立。以逆否命题为例。为了说明我们总能把 !Q => !P 重写为 P => Q,我们:
- 从
!Q => !P出发。 - 根据蕴含的定义得到
!!Q || !P。 - 去掉双重否定得到
Q || !P。 - 再次根据蕴含的定义得到
P => Q。
看,我们刚刚就写出了一个证明!试试反过来,从 P => Q 出发。
从 P => Q 出发,将其重写为 !Q => !P。
解答
先把它重写为 !P || Q。然后把 Q 替换为 !(!Q),得到 !(!Q) || !P。再把它重写为 !Q => !P。
大多数定理都可以用不止一种方式证明。下面是逆否重写规则的另一种完全不同的证明:
- 画出
P => Q和!Q => !P的真值表。 - 它们是一样的。
定理是数学的基础。定理告诉我们一个逻辑工具(比如逆否命题或德摩根定律)是否真的有效。我们可以不了解背后的定理就直接使用逻辑工具,就像我们知道 117*92 == 92*117 而无需先写出证明一样。不过,我们也可以证明关于代码的定理,这是一个专门的主题,我们会在单独的一章中讨论。
记法
数学家喜欢说逻辑是一门“语言”。语言的意义在于清晰地传达复杂的思想,而有时最好的方式就是创造新的词汇和语法。
在逻辑中也是如此,只要 1)保持一致、2)把记法解释清楚,我们就可以创造新的结构和公式写法。事实上,这还受到鼓励。例如,常规写法“1 到 10 之间的整数集合”会占用很多空间:
{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}如果我想更简洁一点,可以想一个简写:
{1, 2, 3, ... 100}如果想比这还要简洁,我可以定义新的语法:
1..=100 = {1, 2, 3, ... 100}
1..<100 = {1, 2, 3, ... 99}这还不是完全没有歧义:那 10..=9 是什么呢?我把它定义为空集:如果 a > b,那么 a..=b 为空。类似地,只要 a >= b,a..<b 就为空。
用 all 量词重写那条规则(即若 a > b,则 a..=b 为空)。假设 a 和 b 都在整数集合中。
解答
all a, b in Int: a > b => (a..=b == {})用集合过滤记法写出 1..=100。在集合 Int 上过滤。
解答
{x in Int: 1 <= x && x <= 100}写出 IsDivisibleBy(num, divisor),当 num 能被 divisor 整除时为真。使用 some 和 ..=。
解答
IsDivisibleBy(num, divisor) =
some x in 1..=num:
x*divisor == num我觉得非常有用的另一种记法是合取列表。复杂的系统往往有复杂的需求:
Rules = A && B && (C || D) && (E || (F && G))这样很难读!为了更易读,我们改成这样写:11
Rules =
1. A
2. B
3. || C
|| D
4. || E
|| a. F
b. G像 4. 这样的数字和像 a. 这样的字母永远表示“与”。如果我想列出“或”,我会始终使用 ||。
小结
- 谓词是定义在任意输入上的布尔函数。
- 集合是唯一元素的无序聚集。集合可以包含任意类型的值,但不能包含谓词。
- 量化表达式是对集合中每一个(或某一个)元素进行检查的表达式。
- 数学记法是灵活的。只要清晰、一致,我们就可以创造新的记法、算子和语法。
- 逻辑公式可以被重写和化简。
以下是我们学过的所有符号和语法:
- 谓词一律写作
TitleCase(x)。函数一律小写并使用snake_case(x)。 - 与、或、非:
&&、||、! - 蕴含:
=> - 集合的并、交、差:
|、&、- - 集合映射与过滤:
{x^2 for x in set: x > 2} - 量词:
all x和some x - 各种语法糖。
就是这些!这就是形式逻辑的全部基础。仔细想想,其实并不多。
当然,难点在于应用。知道除法是一回事,能意识到“把需要 5 个鸡蛋的配方改成只用 3 个鸡蛋”是除法问题则是另一回事。本书的其余部分就是要讲逻辑在哪些软件场景中有用,以及如何让它真正派上用场。让我们用逻辑来理解世界。
延伸阅读
囿于篇幅,本章只是对数理逻辑基础的概览。更深入、全面的论述包括(按复杂程度递增)Robert S. Wolf 的 A tour through mathematical logic、Michael Huth 和 Mark Ryan 的 Logic in Computer Science,以及 Richard Epstein 的 Classical Mathematical Logic。
我们介绍的逻辑被称为一阶逻辑,因为谓词不能作为集合中的值,也不能被传给其他谓词。高阶逻辑拥有更强的能力,但保障更少;更多信息请参见附录《超越逻辑》。不含谓词和量词、仅有布尔值与、或、非的逻辑被称为命题逻辑。
some 和 all 的正式名称分别是存在量词和全称量词。数学家使用符号 ∃ 和 ∀。量化表达式还有几种语法变体;更多内容请参见附录《数学记法》。
能力-保障权衡中的“能力”有时也被称为“表达能力”,比如最小能力原则(优先选择能完成任务的“能力最弱”的编程语言)。我也见过把“保障”称为“能力”的说法。由于“能力-能力权衡”容易引起混淆,本书将避免使用“能力”这个词。
Logic for Programmers 现已提供电子书和纸质书版本。访问官网了解更多!
- 先说清楚预期:本书基于经典一阶逻辑,因为这就足以支撑几百页的应用内容。书中没有构造性逻辑、没有 lambda 演算、没有 Curry-Howard 等等。目标读者是完全不懂数学的人。[返回]
- 我做过一个非常重要的设计决定:“书中使用的所有数学符号都必须能在标准美式键盘上打出”。大多数“正式”的数学符号是为手写设计的,在电脑上用起来要困难得多![返回]
- 这篇博文在表格中使用
OR而不是||,是因为||会破坏 Markdown 表格的格式。[返回] - 未展示:本书有大量索引和交叉引用;这里以及其他所有“这将在 XYZ 中有用”的注释在书中都标有对应章节的页码。[返回]
- 我最初在 newsletter《Some tests are stronger than others》中探讨过这个想法;本书第 4 章用它来引入属性测试。[返回]
- 好吧,嗯,在复审这篇文章时我才意识到我写错了,有序对真正的数学约定其实是
{{a}, {a, b}}。如果这毁了整本书的体验,我很抱歉。至少它现在已经在勘误里了。[返回] - 本书对列表采用从 0 开始的索引(除非在讨论采用其他约定的语言),并且自然数从 0 开始。数学的不同分支有不同的约定,我只是沿用了大多数程序员习惯的那一套。[返回]
- 本书没有涉及的一件事是类型论。这有几个原因,主要是我没能找到简洁性、实用性和真正用得上逻辑之间的恰当平衡。不过书中还是涵盖了一些基础内容,比如让非法状态不可表示和 Liskov 子类型。[返回]
- 制作这张图时我学到的一个极其诡异的事实:SVG 标准把“点”定义为 1 / 72 英寸,而 TeX 把“点”定义为 1 / 72.27 英寸。我在这里写了更多关于这段历史的内容。[返回]
- 给这个概念起个像样的名字花了我好久。我以前叫它能力-易处理性权衡,但书本身已经够装了。感谢Chelsea Troy 最终想出了一个可行的名字。[返回]
- 这是书里最好的点子。我太喜欢合取列表了。[返回]
随机一篇博客
评论
登录后参与讨论