我開始寫作 Logic for Programmers 是因為當時根本找不到適合——呃——給程式設計師看的邏輯教材。現在書已經出版了，新的問題是：還是找不到好的免費邏輯教材給程式設計師看。

所以，為了解決那個問題（順便幫書打點廣告），我把《LfP》第二章改寫成一篇部落格文章。所有註腳都是編按，並未收錄在書中。¹ 請慢慢享用！

第 2 章：邏輯速成課

形式邏輯是非常強大的工具，但同時也非常簡單。在這一章中，我們將說明並解釋基本概念與語法，包括謂詞、蘊含運算子、集合以及集合量詞。其中許多概念，或許你從寫程式的經驗中就已經很熟悉了！

謂詞

粗略來說，謂詞就是一種會回傳布林值的函式。身為程式設計師，你大概已經寫過幾十個謂詞了。以下這些都是謂詞：

• 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 就好。謂詞的強大之處在於它能橫跨各種抽象層次。所以我們來引入一些語法，以區分抽象謂詞與具體謂詞。如果是抽象謂詞，我會把本體用 `backticks`（反引號）包起來：

# concrete
Positive(x) = x > 0
IsSum(x, y, z) = x + y == z

# abstract
CanRunProgram(c) = `c can run our program`

這不是數學家常用的慣例，但對我們的目的來說已經夠清楚了。為了區分謂詞和像 add_two 這種「一般」函式，謂詞一律採用 TitleCase，函式則一律採用 snake_case。

既然謂詞回傳的是布林值，現在正是把布林運算先講清楚的好時機。不同的程式語言對 AND、OR（包含的或）與 NOT 使用不同的符號。數學家用的是 ∧、∨ 和 ¬。我不會用這些符號，因為鍵盤上打不出來。相反地，我會用 &&、|| 和 ! 作為我們的符號。所以 X && !Y 的意思是「X 為真且 Y 為假」。²

除了常見的三種布林運算子之外，數學家還承認第四種：=>。不過在解釋它的意思之前，我們先來練習一下剛學到的東西。

實務範例

謂詞扮演了橋梁的角色，連接我們用自然語言描述系統的方式，以及我們用程式語言編碼的方式。讓我們回到 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 會得出什麼結果。這就叫做真值表。³

有兩組輸入會讓一種解讀得到「假」，另一種得到「真」。有可能廠商在寫需求時想的是第一種解讀，但我卻把它讀成第二種。我很確定程式在我的電腦上跑得動，結果卻因為記憶體不足而失敗，然後我就會覺得廠商騙了我。用數學來表達需求就清楚多了！

用形式邏輯來表達性質，比用非正式的英文更不容易產生歧義。為了教學方便，我們在此假設原本想表達的謂詞是 (RAM(c) && CPU(c)) || GPU(c)。

我們會在〈決策表〉這一章中，用真值表來進行案例分析。⁴

條件謂詞

現在來幫我們的謂詞做點變化。以 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)）：

當 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)。

蘊含運算子非常強大，在很多地方都派得上用場，例如撰寫規格或建立系統模型。其中一個用途是表示某個布林敘述比另一個「更強」。⁵ 舉例來說，「這段程式碼在傳入 0 時會當掉」就是比「這段程式碼有臭蟲」更強的敘述。如果它在某個輸入下會當掉，那它一定有臭蟲！但即使程式沒有當掉，它還是可能有像是差一錯誤（off-by-one error）之類的臭蟲。或者，用數學寫出來就是：

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(c, p) =
  `true unless Native(p) and either Q(p) or R(p),
  in which case (RAM(c) && CPU(c)) || GPU(c))`

CanRunProgram(c, p) =
  Native(p) => (RAM(c, p) && CPU(c, p)) || GPU(c, p)

IfElse(c, x, y) =
  (c => x) && (!c => y)

集合

謂詞的輸入預設是沒有型別的。在 CanRunProgram(c) 中，c 可以是一台電腦，但 c 也可以是一個機器人、數字 26，或字串「the number 26」。在寫程式時，我們會想給它一個型別，明確表示只應該傳入電腦。像是這樣：

CanRunProgram(c) = `c is a computer`
    && ((RAM(c) && CPU(c)) || GPU(c))

現在，即使我們把一張好的顯示卡黏在一隻貴賓狗身上，CanRunProgram(poodle) 仍然會是假。為了讓「c 是一台電腦」這個概念能用數學來表示，數學家使用集合。集合是無序且元素不重複的值的蒐集，例如「所有電腦」、「所有小於 500 KB 的網頁」或「所有合法的 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}}，⁶ 然後再把串列 [a, b, c] 定義為有序對的集合 {(0, a), (1, b), (2, c)}。⁷ 有了基於集合的串列「抽象」實作後，他們就可以拋開集合，直接操作串列。

身為程式設計師，我們在使用串列之前不需要先寫出它的形式化定義，反正我們本來就比較喜歡直接使用那種更複雜的抽象。即便如此，集合仍然是一種有用的程式資料型別。我們會在下一章看到這一點。

集合運算

就像我們有數字的算術和布林值的算術一樣，我們也有集合的算術。給定集合 {A, B} 和 {B, C}，我們可以做的基本操作有：

1. 將它們做聯集，也就是把它們併成一個大集合：{A, B} | {B, C} == {A, B, C}
2. 取交集，也就是找出共同的元素：{A, B} & {B, C} == {B}
3. 取差集，也就是從一個集合減去另一個集合：{A, B} - {B, C} == {A}

我們也可以測試一個集合是否是另一個集合的子集。EvenIntegers 是 Integers 的子集，因為 EvenIntegers 的每個元素也都是 Integers 的元素。值 2 不是 Integers 的子集，但集合 {2} 是。子集的概念類似於程式語言中的子型別。⁸ 如果一個語言說「Rectangle 是 Shape 的子型別」，意思是所有矩形的集合是所有形狀集合的子集。我們會在更廣泛的「契約」主題中更詳細地探討子型別。

要對集合做映射和過濾也非常有用。標準的數學寫法是 {f(x) | P(x)}，但我發現初學者常常搞不清楚哪一邊是映射、哪一邊是過濾。因此在這本書中，我會使用更明確的語法：

例如，所有偶數的集合是 {x in Int: x % 2 == 0}，而所有偶數的平方根所成的集合則是 {sqrt(x) for x in Int: x % 2 == 0}。這種寫法有時被稱為集合建構式或集合建構表示法。之後，集合建構式將成為我們理解資料庫查詢的基礎。

量詞

我們暫時離開軟體需求，來看看另一個問題。軟體開發團隊通常會要求對主程式碼的變更必須先以 pull request 的形式提出，並由另一位團隊成員審查。更簡潔地說：

在合併之前，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)

我會這樣唸：「如果在開發者集合中至少存在一個元素 d 使得 ReviewedBy(pr, d) 為真，那麼 CanMerge 對 pull request 元素 pr 為真」。或者簡單說就是「有某個開發者審查過這個 pull request」。

值 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 太寬鬆了。如果審查者發現了重大的安全性漏洞呢？如果有五位開發者審查了 pull request，其中兩位發現了問題呢？大多數公司會使用更嚴格的合併條件：

在合併之前，pull request 必須至少由一位團隊成員審查，且所有審查者都必須核准該請求。

按照慣例，我們先把需求寫成抽象謂詞。

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)

但這是錯的：它要求每一位開發者都要核准這個 pull request，包括請病假或正在休育嬰假的開發者。我們只想要求「審查過這個 pull request 的每一位開發者」都核准。我們可以用蘊含來修正這一點。回想一下，P => Q 的意思是 !P || Q。那麼 ReviewedBy(pr, d) => Approved(pr, d) 的意思是，要嘛 d 核准了這個 pull request，要嘛他根本沒有審查。

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;
}

能力與保證的取捨

現在我們已經看過 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)。來看看三個例子：

1. 集合「所有 ASCII 字元」是集合「所有 Unicode 字元」的子集。ASCII 保證了每個可表示的字元恰好佔用一個位元組，所以我看到字串 ABC 就能立刻知道它是三個位元組。Unicode 則沒有這種保證，字串 ABC 如果用的是西里爾字母，就可能是六個位元組。

2. 集合「擁有檔案唯讀權限時能做的事」是「擁有檔案完整權限時能做的事」的子集。唯讀權限保證程式不會改變檔案內容。而擁有完整權限時，任何有臭蟲的程式都可能覆寫我們的資料。

3. 集合「只使用布林值、AND、OR 和 NOT 的所有邏輯公式」是「所有邏輯公式」的子集。前者保證每個公式都可以轉成真值表。要怎麼為 some x in Nat: OddPerfectNumber(x) 製作真值表？你做不到。數學家到現在都還不知道它是真是假！

同時，我們需要 Unicode 來表示表情符號，需要寫入權限來更新資料，也需要集合量詞來表達大多數有趣的謂詞。這就是能力與保證的取捨：一個語言、格式或工具能做的事情越多，它能給我們的保證就越少。¹⁰

我們在這本書的幾乎每一章都會看到這種取捨。

重寫規則

在本書一開始，我說過邏輯就是布林值的數學，就像算術是數字的數學一樣。懂得算術能讓我們化簡數值表達式。例如，我們可以這樣化簡函式 f(x, y) = -10x + 2(y + 5x)：

1. 2(y + 5x) 等同於 2y + 10x。
2. -10x + 2y + 10x 等同於 10x - 10x + 2y。
3. 前兩項互為相反數，所以互相抵消。
4. 所以我們得到 f(x, y) = 2y。

在邏輯中，這些化簡被稱為重寫規則。你可能小時候就已經用過一個重寫規則了：

你覺得抱歉嗎？不覺得？那你是「不不不不」覺得抱歉嗎？

這裡的重寫規則是 !!a == a。這表示 !!(!!Sorry) 等同於 Sorry。

我們在邏輯中常用的一些重寫規則有：

蘊含運算子也有重寫規則。其中一個——逆否命題——對我們會非常有用。

而量詞也有重寫規則：

常數抽取對任何帶有 || 或 && 的量詞都適用。分配律則只對 some/|| 和 all/&& 適用。

有些規則比其他規則更常出現。接下來我們會大量使用迪摩根定律、逆否命題和量詞對偶性。更完整的清單請見〈重寫規則〉。即使是比較冷門的規則，對於重構程式碼也可能非常有用。

all x: P(x)

定理

你可能聽過數學家會試圖證明定理。定理只是一個永遠為真的數學敘述，而證明就是一組清楚的步驟，讓你從已知為真的事實出發，推導出該定理為真。

我列出的每一個重寫規則都是一個定理，而且我們可以證明它們永遠成立。以逆否命題為例。要證明我們永遠可以把 !Q => !P 重寫成 P => Q，我們可以：

1. 從 !Q => !P 開始。
2. 套用蘊含的定義，得到 !!Q || !P。
3. 消去雙重否定，得到 Q || !P。
4. 再次套用蘊含的定義，得到 P => Q。

鏘鏘，我們剛剛就寫出了一個證明！試試看反過來，從 P => Q 出發。

大多數定理都可以用不只一種方法來證明。以下是逆否命題重寫規則的另一種完全不同的證明：

1. 畫出 P => Q 和 !Q => !P 的真值表。
2. 它們是一樣的。

定理是數學的基礎。定理告訴我們一個邏輯工具（如逆否命題或迪摩根定律）是否真的有效。我們可以在不了解背後定理的情況下使用邏輯機制，就像我們知道 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 in Int: a > b => (a..=b == {})

{x in Int: 1 <= x && x <= 100}

IsDivisibleBy(num, divisor) =
  some x in 1..=num:
    x*divisor == num

我覺得非常有用的另一種表示法是合取清單。複雜的系統往往有複雜的需求：

Rules = A && B && (C || D) && (E || (F && G))

這樣很難讀！為了讓它更容易閱讀，我們改成這樣寫：¹¹

Rules =
  1. A
  2. B

  3. || C
     || D

  4. || E
     || a. F
        b. G

像 4. 和 a. 這樣的編號永遠代表 AND。如果我想要一個 OR 的清單，我永遠會使用 ||。

總結

• 謂詞是一種可以定義在任何輸入上的布林函式。
• 集合是無序且元素不重複的值的蒐集。集合可以包含任何型別的值，除了謂詞。
• 量化表達式是針對集合中每一個（或某一個）元素進行檢查的表達式。
• 數學表示法是很有彈性的。只要清楚且一致，我們就可以創造新的表示法、運算子和文法。
• 邏輯公式可以被重寫和化簡。

以下是我們學到的所有符號和語法：

• 謂詞一律寫成 TitleCase(x)。函式一律是小寫且為 snake_case(x)。
• AND、OR、NOT：&&、||、!
• 蘊含：=>
• 集合聯集、交集、差集：|、&、-
• 集合映射與過濾：{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。

我們所涵蓋的邏輯被稱為一階邏輯，因為謂詞不能作為集合中的值，也不能被傳入其他謂詞。更高階的邏輯擁有更多能力，但保證更少；更多資訊請見附錄〈Beyond Logic〉。沒有謂詞和量詞、只有布林值、AND、OR 和 NOT 的邏輯則被稱為命題邏輯。

some 和 all 的正式名稱分別是存在量詞和全稱量詞。數學家使用符號 ∃ 和 ∀。量化表達式有幾種不同的語法變體；更多內容請見附錄〈Math Notation〉。

能力與保證取捨中的「能力」有時也被稱為「表達能力」，例如 最小表達能力原則（選擇能解決問題的「表達能力最弱」的程式語言）。我也看過「保證」被稱為「表達能力」。由於「表達能力—表達能力取捨」這種說法很不清楚，我們在這本書中會避免使用「表達能力」這個詞。

Logic for Programmers 現已推出 電子書和紙本書。 到官網了解更多！

1. 先把期望說在前面：這本書是基於一階古典邏輯，因為這樣就足以支撐幾百頁的應用內容。書中沒有建構式邏輯、沒有 lambda 演算、沒有 Curry-Howard 等等。目標讀者是完全不懂任何數學的人。 [返回]
2. 我在這本書中做的一個非常重要的設計決定是「書中使用的所有數學都必須能在標準美式鍵盤上輸入」。大多數「正式」的數學符號是設計來手寫的，這讓它們在電腦上更難使用！ [返回]
3. 這篇部落格文章在表格中使用 OR 而不是 ||，是因為 || 會破壞 Markdown 表格的格式。 [返回]
4. 未顯示：這本書有大量的索引和交互參照；這裡以及所有其他「這在 XYZ 中會很有用」的註解都有對應其他章節的頁碼。 [返回]
5. 我最初是在電子報 Some tests are stronger than others 中探討這個想法的；書中第 4 章用它來引出屬性測試（property testing）。 [返回]
6. 好吧，呃，在審閱這篇文章時我才發現我寫錯了，有序對真正的數學慣例其實是 {{a}, {a, b}}。如果這毀了整本書，還請見諒。 至少它現在已經在勘誤表中了。 [返回]
7. 書中使用以 0 為起始的索引來表示串列（除非討論的語言另有規定），並且自然數從 0 開始。不同數學分支有不同的慣例，我只是沿用了大多數程式設計師習慣的寫法。 [返回]
8. 這本書沒有涵蓋的一件事是型別理論。這有幾個原因，主要是我找不到在簡潔性、實用性與「真的在用邏輯」之間的恰當平衡。書中有涵蓋一些基本概念，例如 讓不合法的狀態無法被表示和 Liskov 子型別。 [返回]
9. 我在製作這張圖時學到的一個極其詭異的事實：SVG 標準將一個「點」定義為 1 / 72 英吋，而 TeX 則將一個「點」定義為 1 / 72.27 英吋。 我在這裡寫了更多關於這段歷史的內容。 [返回]
10. 光是想出這個該死的名字就花了我好久。我以前都叫它能力—可處理性取捨，但這本書本來就已經夠自命不凡了。感謝 Chelsea Troy 終於想出了一個可行的名稱。 [返回]
11. 這是這本書裡最棒的點子。我超愛合取清單。 [返回]