萩谷　昌己：ソフトウェア科学のための論理学

作成日：2013-02-12
最終更新日：

概要

ソフトウェア科学を研究する計算機科学者が知っておくべき数理論理学の素養とはどのようなものだろうか。 この問いに答えるための本である。 著者は言う。命題論理を含む一階述語論理は常識である。ここは必修編となっている。 次に、様相論理や動的論理、ホーア論理を上級編として紹介している。 選択編では直観主義論理とカテゴリー（圏）について説明がある。

なお、その後、本書の内容を一部含む、萩谷昌己・西崎真也「論理と計算のしくみ」が発売されている。

感想

この本では、必修編だけは真面目に勉強した。 学習のてびきでは これらを読まないなら、本書を買う価値がないとまで言い切っていたからである。 本書が出版されて１年間、毎朝ちびちびと勉強した。でもわからなかったなあ。

第１章 一階述語論理

通常論理学の本では、命題論理を述べたあとで述語論理に進むが、本書はいきなり一階述語論理を学ぶ。しかし、 この第１章の最後の節で命題論理についても触れられている。

\( (\forall x_0 ((\lnot \mathrm{human}( x_0)) \lor \mathrm{mortal} (x_0))) \)の構文木が p.14 の図 1.1 として出ている。 図 1.1 の配置とは異なるところは、 \( x \) の添字 0 が表示できず、やむを得ず x_0 としていることなどがある。

そのあたりの事情については、 二分木の表示に詳しく記す予定だ。

第２章　一階述語論理の演繹体系

推論規則

pp.39-40 にかけて、命題論理のシーケント計算における計８種類の推論規則が記述されている。 これらの推論規則の図の書き方がわからない。 そこで図の書き方は、田村直之先生による ソフトウェア科学特論: 命題論理の推論体系(tamura70.gitlab.io)

を参考にした。 そこで本書の８種類の推論規則が書けた。
\(\Infer{(\lnot \mathrm{右})}{\G \ra \D, \lnot A}{A, \G \ra \D} \)
\(\Infer{(\lnot \mathrm{左})}{\lnot A, \G \ra \D}{\G \ra \D, A} \)
\(\Infer{(\land \mathrm{右})}{\G \ra \D, A \land B }{\G \ra \D, A \AND \G \ra \D, B}\)
\(\Infer{(\land \mathrm{左})}{A \land B, \G \ra \D }{A , B, \G \ra \D}\)
\(\Infer{(\lor \mathrm{右})}{\G \ra \D, A \lor B}{\G \ra \D, A , B}\)
\(\Infer{(\lor \mathrm{左})}{A \lor B, \G \ra \D}{A, \G \ra \D \AND B, \G \ra \D}\)
\(\Infer{(\supset \mathrm{右})}{\G \ra \D, A \supset B}{A, \G \ra \D, B} \)
\(\Infer{(\supset \mathrm{左})}{A \supset B, \G \ra \D}{\G \ra \D, A \AND B, \G \ra \D}\)

証明

p.41 で、証明（証明図、証明木）の一例が示されている。以下引用する。

\[ \Infer{}{P \lor Q \ra Q \lor P}{ \Infer{}{P \lor Q \ra Q, P}{ P \ra Q, P \AND Q \ra Q, P }} \]

p.42 では、上記の証明でどの推論規則を使ったのかを明記をした図もある。

\[ \Infer{(\lor 右)}{P \lor Q \ra Q \lor P}{ \Infer{(\lor 左)}{P \lor Q \ra Q, P}{ P \ra Q, P \AND Q \ra Q, P }} \]

また、次の図も \( P \lor Q \ra Q \lor P \) の証明であるという。

\[\Infer{}{P \lor Q \ra Q \lor P }{\Infer{}{P \ra Q \lor P}{P \ra Q , P} \AND \Infer{}{Q \ra Q \lor P}{Q \ra Q , P} }\]

p.42 の中ほどの問には、上の証明において，どの推論規則が使われているかを確認せよ．とある。私の答は次の通りだ。

\[\Infer{(\lor 左)}{P \lor Q \ra Q \lor P }{\Infer{(\lor 右)}{P \ra Q \lor P}{P \ra Q , P} \AND \Infer{(\lor 右)}{Q \ra Q \lor P}{Q \ra Q , P} }\]

Wang のアルゴリズムの実装

ワングのアルゴリズム( Wang's algorithm ) という、トートロジ判定アルゴリズムが紹介されている。 Common Lisp の実装があったので真似てみたらできた。 これを Scheme や JavaScript で動かすのが目標である。

論理学における Wang のアルゴリズムを実装した。 といっても、本書の解答にあった LISP プログラムを真似しただけである。 なお、本書の実装では関数 memq が組み込まれていることが前提となっているが、 私がためした LISP の処理系の一つ、 CLisp では memq が備わっていないため、マクロを書いた。 マクロは On Lisp に基づいている。 


(defmacro memq (obj lst)
  `(member ,obj ,lst :test #'eq))

(defun intersect (x y)
  (if (null x)
      nil
    (if (memq (car x ) y)
        t
      (intersect (cdr x) y))))

(defun wang (l la r ra )
  (if (null l)
      (if (null r)
          (if (intersect la ra)
              t
            nil)
        
        (let ((r0 (car r)) (r1 (cdr r)) )
          (if (atom r0)
              (wang l la r1 (cons r0 ra))
            (case (car r0)
              (not (wang (cons (cadr r0) l) la r1 ra))
              (and (and (wang l la (cons (cadr r0) r1) ra)
                        (wang l la (cons (caddr r0) r1) ra)))
                   (or (wang l la
                            (cons (cadr r0) (cons (caddr r0) r1)) ra))
                  (implies (wang (cons (cadr r0) l) la
                                 (cons (caddr r0) r1) ra))))))
    
    (let ((l0 (car l)) (l1 (cdr l)))
          (if (atom l0)
              (wang l1 (cons l0 la) r ra)
            (case (car l0)
              (not (wang l1 la (cons (cadr l0) r) ra))
              (and (wang (cons (cadr l0) (cons (caddr l0) l1)) la r ra ))
              (or (and (wang (cons (cadr l0) l1 ) la r ra)
                       (wang (cons (caddr l0) l1 ) la r ra)))
              (implies (and (wang l1 la (cons (cadr l0) r) ra)
                            (wang (cons (caddr l0) l1) la r  ra))))))) )

数式

数式表示には、MathJaxを使っている。特に、証明図（証明）については、 MathJax4 を参照のこと。

書誌情報

書名ソフトウェア科学のための論理学
著者萩谷　昌己
発行日1994 年 1月 28日
発行元岩波書店
定価2913円（税別）
サイズ
ISBN4-00-010351-2
備考岩波講座　ソフトウェア科学　11
NDC

まりんきょ学問所 ＞ コンピュータの部屋 ＞ コンピュータの本 ＞ 萩谷　昌己：ソフトウェア科学のための論理学

MARUYAMA Satosi