演算邏輯 Calculational Logic(二)騎士與惡棍之島

一個島上住著兩種人,騎士 (knight) 與惡棍 (knave) 。騎士總說實話,惡棍總說謊話,但從外表看不出誰是騎士或惡棍。某天,居民 A 和你說「B 剛剛說他自己是騎士」。由此你可知道 A 說的是實話還是謊話嗎?B 呢?傳說島上藏著金子,怎麼設計一個問題,查出傳言的真假呢?

只要有耐心把各種狀況列出來作分析,這類邏輯問題總是可以找到解答的。既然演算邏輯號稱是為了應用設計的邏輯,以演算邏輯的眼光看這種問題,是否比較好解呢?

上次我們談到 這個運算元,知道它滿足交換律和結合律,是演算邏輯最基礎的運算元。在談騎士與惡棍問題之前,我們得先提另一條規則:

[const. true] true ≡ p ≡ p

如果讀解成 true ≡ (p ≡ p), 意思是 也滿足同一律:任何值都等於自己。如果讀解成 (true ≡ p) ≡ p,則是強調 true 的單位元素。

騎士與惡棍

我們將「A 是騎士」簡寫成 A. 如果 A 說了某個陳述 S, 我們無法知道 S 是否成立,但我們知道

A ≡ S

如果 A 是騎士,S 便是真的;如果 A 是惡棍,S便是假的。

假設我們問 A:「你是騎士嗎?」A 回答「是的。」這可以記成 A ≡ A. 然而,根據 [const. true] 規則,A ≡ A 可以化簡為 true. 意思是,在這個島上不管你問誰「你是騎士嗎」,對方都會回答是。

如果 A 說:「B 是騎士」呢? 這可以記成 A ≡ B. 我們仍不知道 B 到底是騎士還是惡棍,但我們可以知道 AB 是同一種人。

如果 A 說:「我和 B 是同一種人」呢?這可記成 A ≡ (A ≡ B)。我們算算看:

  A ≡ (A ≡ B)
=   { 結合律 }
  (A ≡ A) ≡ B
=   { [const. true] }
  true ≡ B
=   { [const. true] }
  B

啊,所以我們雖仍不知道 A 到底是騎士還是惡棍,卻可以知道 B 一定是騎士!

若不用演算邏輯,一般人的推理方式可能是把 A是騎士或惡棍、B是騎士或惡棍的四種可能性一一嘗試。由此我們可以體會到 Gries 所說「演算邏輯為解決問題而設計」的意思 — 利用 的性質,讓一個式子盛載多重的意義,因此我們可同時處理好幾種狀況,讓推理相當精簡迅速。當然,前提是要對邏輯規則夠熟練。

所以,要怎麼想出一個問題問 A,用來判斷島上到底有沒有金子呢?經過剛剛的討論,讀者也許已經可以猜得出來。但 Backhouse 建議我們避免瞎猜。我們應該用代數解未知數的方式把問題推演出來。把「島上有金子」這個命題記為 G. 我們希望問某個問題 Q, 如果 A 回答「是」,就表示島上有金子,反之則否:

  • 「A 對問題 Q 回答『是』」記為 A ≡ Q
  • 「A 對問題 Q 回答『是』,島上便有金子」應該是一個若且唯若的命題,寫成 G ≡ (A ≡ Q)

而根據交換律和結合律,G ≡ (A ≡ Q) 就是 Q ≡ (G ≡ A)。我們要問 A 的問題就是 G ≡ A:「『島上有金子』和『你是騎士』是不是等價的呢?」?

希望這個島上不論騎士或惡棍,邏輯都蠻不錯的,才聽得懂這種問題囉!

否定運算元

以上的討論只用了三條規則:交換律、結合律、和[const. true]. 結束本篇之前,我們再看一條關於false 與「否定」運算元 ¬ 的規則:

[negation] ¬p ≡ p ≡ false

把括號放在後面,¬p ≡ (p ≡ false)¬ 的定義;若讀解成 (¬p ≡ p) ≡ false,這條規則讓我們把算式中看到的 p¬p 兩兩消去成 false.

方才我們把「A 是騎士」記為 A,「A 是惡棍」自然是 ¬A 了。以下的練習除 3. 以外皆取自 Backhouse 的書。

  1. A 說:「我和 B 是不同種的。」由此我們可推導出什麼關於 AB 的資訊呢?
  2. 用上述的做法,推導出一個問題問A ,若 A 回答「是」,我們可得知 AB 真的不同種類。
  3. A 說:「B 說他是騎士。」由此我們可以得知什麼關於 AB 的訊息?如果 A 說:「B 說他是惡棍」呢?
  4. 試證明 ¬(p ≡ q) = (p ≡ ¬q)

參考資料

本文內容皆來自 Roland BackhouseProgram Construction: Calculating Implementations from Specifications 第五章。

This entry was posted in 計算算計 and tagged . Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

7 Comments