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

概要

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

感想

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

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

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

Wang のアルゴリズムの実装

論理学における Wang のアルゴリズムを実装した。 といっても、萩谷昌己氏の教科書をまねしただけである。 なお、同氏の実装では関数 memq が組み込まれていることが前提だが、 私がためした 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))))))) )
  
						

数式

数式表示には、ASCIIMathMLを使っている。

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