演算邏輯 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 未分類. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

13 Comments

  1. roy_hu
    Posted 二月 22, 2010 at 3:49 下午 | Permalink

    calculus台湾翻译是什么?大陆把calculus译为演算(在数学中被特定译为微积分),arithmetics译为算术或运算,algorithm译为算法。

    • Posted 二月 22, 2010 at 6:54 下午 | Permalink

      啊,其實差不多。講極限的那個 calculus 也是譯成「微積分」。至於 λ calculus 一般習慣是不翻譯,知道「λ演算」是什麼的人不多。我剛剛查一下發現 arithmetics 翻譯成「算術」的也不少。

      Calculation 翻譯成演算不知好不好,和 calculus 撞詞也是個問題。話說回來,很多字典仍不把 "calculational" 當作一個字。可見這東西還真是小眾呀…

      又,我後來才知道大陸不說「若且唯若」,而是「當且僅當」。 :)

      • roy_hu
        Posted 二月 22, 2010 at 11:24 下午 | Permalink

        calculate确实不好翻译,大陆也是译为计算。为了区别,calculator译为计算器,computer译为计算机。

  2. Posted 二月 22, 2010 at 8:30 下午 | Permalink

    試著直覺理解四槓算子為何有結合律還沒有成果,好像一涉及 true & false 的 case analysis 就變得不太直覺,但這 case analysis 卻又是 classical logic 的重要特質(排中律?)。不過倒證明了 intuitionistic logic 上沒有 ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r)) 這個性質(其中 p ↔ q(p → q) ∧ (q → p) 的縮寫)─ 由此式可導出 Pierce’s law。但整個推導也就純粹是 natural deduction 硬做出來的,看不太出意義…

    愈來愈感受 intuitionistic logic 的直觀呀!XD

    • Posted 二月 22, 2010 at 8:31 下午 | Permalink

      唔,似乎用不同字體看會變成三槓算子或四槓算子 XD。

      • Posted 二月 22, 2010 at 10:03 下午 | Permalink

        對這三槓四槓我有一樣的疑問 囧…
        想說要 google 四槓,結果貼出去變三槓
        查了一下,U+2263 應該是四槓沒錯?怪哉

        • Posted 二月 23, 2010 at 10:22 上午 | Permalink

          啊,我想要的是三槓的耶。跟 Algebra of Programming 裡面用的一樣。等下我改改看好了…

    • Posted 二月 23, 2010 at 10:39 上午 | Permalink

      我也不知道有什麼「直覺理解」的方法。p ≡ (q ≡ r) 可以想成是 p 代表 qr 是否是一樣的。但要牽連到 (p ≡ q) ≡ r 除了分別討論一下 p 是 true 或 false(也就等於是在看真值表了)之外好像也沒什麼好解釋。

      古典邏輯咩,要從語意上去理解的話就只有看真值表囉。

      ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r)) 到 Pierce’s Law 那個,有空寫給大家看吧?

      直覺邏輯是以簡御繁,每個 connective 就一到兩條 introduction 和 elimination rules. 演算邏輯規則可多了。但應用範圍不太一樣。例如 p1 ≡ p2 ≡ p3 ... ≡ pn 中,任何變數若出現奇數次就可以拿到只剩下一個,出現偶數次就變成 true,這種東西用演算邏輯就很容易看出來。

      其實我主要有興趣的原因是演算邏輯的許多規則和做 relational program derivation 用的規則是一樣的。例如 p ⇒ q 的定義是 p ≡ p ∧ q. 把 換成 , 換成 , 就是一條每次出現時我都覺得「怎麼會想到」的規則。於是我想如果我當初早點學會這個的話,後者可能會學得比較好…

      • Posted 二月 23, 2010 at 2:47 下午 | Permalink

        ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r)) 到 Pierce’s Law 那個,有空寫給大家看吧?

        我寫了一份在這裡 (pdf)。因為 derivation trees 太寬了只好用橫式 A4… 雖然最終解釋應該不太可能避開真值表,但我另外導了一個看起來比較單純的等價式子,看看會不會比較容易解釋?

        然後我發現我把 Peirce’s law 拼錯了 XD。

        例如 p ⇒ q 的定義是 p ≡ p ∧ q. 把 換成 , 換成

        我相信 \wedge 是換成 \cap? :)

        • Posted 二月 23, 2010 at 5:31 下午 | Permalink

          Oops.. 對!應該是 .

    • Posted 三月 1, 2010 at 8:48 上午 | Permalink

      但整個推導也就純粹是 natural deduction 硬做出來的,看不太出意義…

      p, q, r 分別替換成 A, ⊥, ⊥ 呢?

      • Posted 三月 1, 2010 at 10:27 上午 | Permalink

        那會變成 ¬¬A ↔ A 嗎?(所以這是看出直覺邏輯的 ↔ 不應該滿足結合律的比較快的方法囉?)

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>