SICP 読書ノート#65 - 4.4.1 プログラムとしての論理 (pp.269-270)

§4.4.1の続き「プログラムとしての論理」から。

プログラムとしての論理

規則は一種の論理的包含(logical implication)と見ることが出来る: 値のパターン変数への代入が, 本体を満足すれば, それは結論を満足する. 従って質問言語を, 規則に基づいて論理的推論(logical deductions)を実行する能力があると見ることが出来る.

冒頭からイミフです。

まずは論理的包含を調べてみました。

論理包含 - Wikipedia

… 2つの命題 P と Q に対する論理包含を P → Q などと書き、「P ならば Q」と読む。命題 P → Q に対し、P をその前件、Q をその後件などと呼ぶ。

これを規則(rule)で表すとこうです。

(rule Q P)

よって質問言語(query language)は論理的推論の実行能力があると結論づけているようです。

＊＊＊

次にappendの例。まずappendの実装を振り返ると、

(define (append x y)
  (if (null? x)
      y
      (cons (car x) (append (cdr x) y))))

という実装は、

xが()なら、(append x y) => y
xが任意のリストなら、(append x y) => ((car x) . (append (cdr x) y)

という定義づけを行ってる、とも言えます。

さらに、

xが()なら、(append x y) => y

の公理的定義は、本文の

任意のリストyについて, 空リストとyをappendするとyになる

に、

xが任意のリストなら、(append x y) => ((car x) . (append (cdr x) y))

は、

任意のu, v, yとzについて, vとyをappendしてzになるなら, (cons u v)とyをappendすると, (cons u z)になる.

に、相当します。

前者の条件はまあそのままですが、後者の条件はぱっと見よくわかりません。

もう少し噛み砕いて、

任意のu, v, yとzについて, vとyをappendしてzになる

を、(append v y) => z

(cons u v)とyをappendすると, (cons u z)になる

を、(append (u . v) y) => (u . z) と表し直してみます。

ここで x = (u . v)とすると、

(append x y) = (append (u . v) y) = (u . z) となり、
z = (append v y) から、
(u . z) = (u . (append v y)) = ((car x) . (append (cdr x) y)

と変形できます。

ゆえに、

xが任意のリストなら、(append x y) => ((car x) . (append (cdr x) y)

の公理的定義は、

任意のu, v, yとzについて, vとyをappendしてzになるなら, (cons u v)とyをappendすると, (cons u z)になる.

と表現できます。

＊＊＊

次に、上記の公理的定義を表す規則を質問システムに追加してみます。

規則やデータを動的に追加するには(assert! ...)が使えるようです。

;;; Query input:
(assert! (rule (append-to-from () ?y ?y)))

Assertion added to data base.

;;; Query input:
(assert! (rule (append-to-from (?u . ?v) ?y (?u . ?z))
               (append-to-from ?v ?y ?z)))

Assertion added to data base.

続けてappend-to-fromを実行させてみます。

;;; Query input:
(append-to-from (a b) (c d) ?z)

;;; Query results:
(append-to-from (a b) (c d) (a b c d))

;;; Query input:
(append-to-from (a b) ? (a b c d))

;;; Query results:
(append-to-from (a b) (c d) (a b c d))

;;; Query input:
(append-to-from ?x ?y (a b c d))

;;; Query results:
(append-to-from (a b c d) () (a b c d))
(append-to-from () (a b c d) (a b c d))
(append-to-from (a) (b c d) (a b c d))
(append-to-from (a b) (c d) (a b c d))
(append-to-from (a b c) (d) (a b c d))

本文の通りに動きました。ごいすー。

問題 4.61

リストの隣の要素を見つけます。

;;; Query input:
(assert! (rule (?x next-to ?y in (?x ?y . ?u))))

Assertion added to data base.

;;; Query input:
(assert! (rule (?x next-to ?y in (?v . ?z))
               (?x next-to ?y in ?z)))

Assertion added to data base.

;;; Query input:
(?x next-to ?y in (1 (2 3) 4))

;;; Query results:
((2 3) next-to 4 in (1 (2 3) 4))
(1 next-to (2 3) in (1 (2 3) 4))

;;; Query input:
(?x next-to 1 in (2 1 3 1))

;;; Query results:
(3 next-to 1 in (2 1 3 1))
(2 next-to 1 in (2 1 3 1))

問題 4.62

まず問題2.17の解答のlast-pairを見てみる。

(define (last-pair lst)
  (cond ((null? lst) nil)
        ((null? (cdr lst)) lst)
        (else (last-pair (cdr lst)))))

これを公理的定義で表すと、

任意のアトム(z . ())に対し、(last-pair (z . ())) => z
任意のリスト(u . v)に対し、 (last-pair v) => xとなるなら(last-pair (u . v)) => x

よって規則の実装は、

(rule (last-pair (?z . ()) ?z))
(rule (last-pair (?u . ?v) ?x)
      (last-pair ?v ?x))

質問システムに組み込んでテスト。

;;; Query input:
(assert! (rule (last-pair (?z . ()) ?z)))

Assertion added to data base.

;;; Query input:
(assert! (rule (last-pair (?u . ?v) ?x)
               (last-pair ?v ?x)))

Assertion added to data base.

;;; Query input:
(last-pair (3) ?x)

;;; Query results:
(last-pair (3) 3)

;;; Query input:
(last-pair (?x) 5)

;;; Query results:
(last-pair (5) 5)

;;; Query input:
(last-pair (23 72 149 34) ?x)

;;; Query results:
(last-pair (23 72 149 34) 34)

問題 4.63

grandson-ofとson-ofの規則はそれぞれ以下の通り。

(rule (grandson-of ?g ?s)
      (and (son ?f ?s)
           (son ?g ?f)))

(rule (son-of ?m ?s)
      (and (wife ?m ?w)
           (son ?w ?s))))

データベースと規則をassert!で表明。

(assert! (son Adam Cain))
(assert! (son Cain Enoch))
(assert! (son Enoch Irad))
(assert! (son Irad Mehujael))
(assert! (son Mehujael Methushael))
(assert! (son Methushael Lamech))
(assert! (wife Lamech Ada))
(assert! (son Ada Jabal))
(assert! (son Ada Jubal))

(assert! (rule (grandson-of ?g ?s)
               (and (son ?f ?s)
                    (son ?g ?f))))

(assert! (rule (son-of ?m ?s)
               (and (wife ?m ?w)
                    (son ?w ?s))))

テスト。個人的に聖書の知見は0だけど、たぶん動いてそう。

;;; Query input:
(grandson-of ?x ?y)

;;; Query results:
(grandson-of Mehujael Lamech)
(grandson-of Irad Methushael)
(grandson-of Enoch Mehujael)
(grandson-of Cain Irad)
(grandson-of Adam Enoch)

;;; Query input:
(son-of ?x ?y)

;;; Query results:
(son-of Lamech Jubal)
(son-of Lamech Jabal)