演算邏輯 Calculational Logic（一）若且唯若

最近準備一些教材，讀了 Roland Backhouse 的 Program Construction: Calculating Implementations from Specifications 一書，其中有兩章講「演算邏輯 (calculational logic)」。¹ 覺得這是很有趣的資料，可惜沒有早點學到。

演算邏輯是另一種形式化的古典邏輯，先後由 Edsger Dijkstra, Carel Scholten （因此被稱作 Dijkstra-Scholten 邏輯）, David Gries, Wim H.J. Feijen, Netty van Gasteren, 和 Backhouse 等人提倡。Gries 說，邏輯學家發展形式邏輯是為了研究邏輯本身，而演算邏輯則是設計來解決問題的。我想這裡要加個但書：演算邏輯熟悉後確實很好用，但就和其他數學演算一樣，仍是要花點功夫去學，才能得心應手的。

以下的內容來自 Backhouse。

若且唯若

Backhouse 提到，在數學發展史中，不少重要的觀念往往很晚才被發現。「零」是個經典例子，希臘人甚至不把「一」當作數字，更別說零。「等於」的觀念更晚成型，= 符號到了 1557 年才由 Robert Recorde 在 The Whetstone of Witte 一書中採用。

一個概念往往要到有了符號後才成為可談論的東西。「等於」用符號 = 表示後，一些性質也比較容易表達。我們知道 ＝ 滿足交換律（若 a = b 成立，b = a 也成立）和遞移律（若 a = b, b = c, 則 a = c）。既然 ＝ 滿足遞移律，一般我們常寫「a = b = c」同時表達三件事情。 這種用法精簡地表達了很多性質，已經成為習慣，也有其方便性。

但另一種看法是把 = 當作傳回布林值的運算元：3 = 3 是 true, 3 = 5 是 false。很多人不知道這個意義下的 = 其實還滿足結合律：如果 (p = q) = r 為真，p = (q = r) 也為真，反之亦然。當然這時 p, q, r 都必須是布林值。讀者不妨代幾個布林值試試看，例如：(true = false) = false 成立，true = (false = false) 也成立。Backhouse 說，許多數學家都不知道這個性質，更別說計算科學家了。

為了區分這兩種用法，我們把第二種意義的「等於」（也是邏輯上的「若且唯若」）寫成 ≡。既然滿足結合律，≡ 連續出現時可不用加括號。算式 true ≡ false ≡ false 是成立的， true = false = false 則否。Backhouse 建議把 p ≡ q 念成 “p equivals q” . 至於中文該怎麼念… 請大家提供想法囉。

運算元 ≡ 和其結合律讓我們用精簡的符號承載大量的資訊。例如以下的式子：

even (m + n) ≡ even m ≡ even n

若讀成even (m + n) ≡ (even m ≡ even n)，我們知道如果 m 和 n 的奇偶同位相同，m+n 是偶數；反之 m+n 是奇數。如果讀成 (even (m + n) ≡ even m) ≡ even n，我們知道把 m 加上一個偶數(n)不會改變其奇偶性質。

在其他形式邏輯中，同樣的性質可能會用許多個狀況分析來證明：檢查一下 even m 且 even n 的情況、even m 且 odd n 的情況… 等等。當變數多、狀況更多，演算就難了。盡量使用結合律，避免使用狀況分析，是演算邏輯的主要風格。

參考資料

• Roland Backhouse, Program Construction: Calculating Implementations from Specifications.
• Edsger Dijkstra, Carel Scholten. Predicate calculus and program semantics.
• David Gries 的 Calculational Logic 簡介與參考資料。

附註

1. “Calculation” 常見的翻譯似乎是「計算」，但 “compute” 也翻成「計算」。「演算」比較強調推演的過程，似乎是合適的翻譯。不幸地， “arithmetics” 也常翻成「演算」。此外， “algorithm” 譯成「演算法」也是慣例。