演算邏輯 Calculational Logic(二)騎士與惡棍之島
一個島上住著兩種人,騎士 (knight) 與惡棍 (knave) 。騎士總說實話,惡棍總說謊話,但從外表看不出誰是騎士或惡棍。某天,居民 A
和你說「B
剛剛說他自己是騎士」。由此你可知道 A
說的是實話還是謊話嗎?B
呢?傳說島上藏著金子,怎麼設計一個問題,查出傳言的真假呢?
一個島上住著兩種人,騎士 (knight) 與惡棍 (knave) 。騎士總說實話,惡棍總說謊話,但從外表看不出誰是騎士或惡棍。某天,居民 A
和你說「B
剛剛說他自己是騎士」。由此你可知道 A
說的是實話還是謊話嗎?B
呢?傳說島上藏著金子,怎麼設計一個問題,查出傳言的真假呢?
邏輯學家發展形式邏輯是為了研究邏輯本身,而演算邏輯的設計則是為了便於用邏輯來解決問題。
1969 年,C.A.R. Hoare 在 Communication of the ACM (12(10):576–580) 發表論文 An Axiomatic Basis for Computer Programming,在文中提出後來被稱作 Hoare 邏輯的一套公設系統, 被認為是計算科學史上最重要的幾篇論文之一。時間轉眼間過去了,今年已經是這篇論文的四十歲生日。
Mervyn Pragnell 從沒擔任過學術工作,也沒有發表過論文。但他把英國電腦科學的幾個關鍵角色介紹給彼此,同樣重要地,讓他們認識了 Alonzo Church 的 λ calculus.