演算邏輯 Calculational Logic(一)若且唯若

最近準備一些教材,讀了 Roland BackhouseProgram 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 = 3true, 3 = 5false。很多人不知道這個意義下的 = 其實還滿足結合律:如果 (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),我們知道如果 mn 的奇偶同位相同,m+n 是偶數;反之 m+n 是奇數。如果讀成 (even (m + n) ≡ even m) ≡ even n,我們知道把 m 加上一個偶數(n)不會改變其奇偶性質。

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

參考資料

附註

  1. “Calculation” 常見的翻譯似乎是「計算」,但 “compute” 也翻成「計算」。「演算」比較強調推演的過程,似乎是合適的翻譯。不幸地, “arithmetics” 也常翻成「演算」。此外, “algorithm” 譯成「演算法」也是慣例。
This entry was posted in 計算算計 and tagged . Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

13 Comments