nakayama-blog

p.269 append-to-form の説明がなんだか分かりにくかったので整理。

まず、p269 8行目の説明がわかりにくい。

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

ワケ　　　　　ワカ　　　　　ラン♪

論理的包含というのは "A ならば B" ということだ。つまり "A ならばB" と rule が何か関係していると言っている。のだが、rule のどこが A で どこが B に関係してるのか全然わからない。(長ったらしいだけで分からん説明)

とっとと答えを言うと、

「A ならば B」 
   ⇳
(rule B
      A)

という関係があるということだ。

たしかに、A が正しいときは B を出力し、Aが間違っているときは何も出力しないというのは、「A ならば B」 というルールを使って推論を実行しているようにも見える。

この関係にあてはめると、append の定義(前のブログでまとめる前の定義)

② (append v y) = z ならば (append (cons u v) y) = (cons u z)

は、rule を使って

(rule (append (cons u v) y) = (cons u z)
      (append v y) = z)

と書ける。もちろんこのままでは、ruleの文法に合わないので修正する。

(append a b) = c というのは (append-to-form a b c)と同じ意味である。
(cons a b) というのは (a . b)と同じ意味である。
ruleに出てくる変数には ? をつける。

なので

(rule (append-to-form (?u . ?v) ?y (?u . ?z))
      (append-to-form ?v ?y ?z))

となる。

また、単一の言明 A については

   A
   ⇳
(rule A)

という関係があるので、これを使って、appendの定義

①(append '() y) = y

は

(rule (append '() y) = y)

と書ける。また文法に合うように修正して

(rule (append-to-form '() ?y ?y))

となる。