![見出し画像](https://assets.st-note.com/production/uploads/images/112819420/rectangle_large_type_2_96137d809300e1bfabd7c72a6e109f0b.png?width=1200)
Prologで論理的にプログラミングを学んでいます(問合せ、回答)
AI言語Prologによるプログラミング学習の第3回です。テキストは、「地味に論理的」です。
内容は、Prologにおける問合せとその回答の仕組みです。
問合せ
問合せとは、例えば「駅Aとnearby関係にある駅はどれか?」というものである。Prologにおける問合せは、以下のように記述される。
?- nearby (駅A, W)
ここで、接頭語の'?-'は、問合せである(事実ではない)ことを表す。
この問合せに対する回答は、以下のように記述される。
{W->駅B}
これは、変数Wについての値(駅B)の代入を表す。この代入により、問合せの文
nearby (駅A, 駅B)
は真となる。
nearby関係が事実のリストで定義されている場合、問合せに回答することは容易である。問合せに整合する事実を探し出すだけでよい。
一方、規則が関連してくる場合、問合せへの回答には複数の工程を実行しなければならない。
まず、問合せ
?- nearby (駅A, W)
に答えるときには、それを規則
nearby (X, Y) :- connected (X, Y, L)
の結論(ここではnearbyです)に照らし合わせて、代入
{X->駅A, Y->W}
を引き出す。
次に、この代入を規則に対して行い、そのときの前提(ここではconnectedです)についての回答を探す。すなわち、問合せ
?- connected (駅A, W, L)
に対する回答を探す。
(これは、「任意の路線Lにより駅Aとconnected関係にあるのはどの駅か?」という問合せです。言い換えるなら「駅Aと直接接続されているのはどの駅か?」の問合せです。)
駅Aと直接接続された駅を発見できたなら、駅Aとnearby関係にある駅を発見したことになる。
つまり、直接接続についての事実を見つけることで、問合せの回答が得られる。
例えば、事実から得られた回答を
{W->駅B, L->路線L}
とする。
ここで、変数Lは最初の問合せには現れない。
そのため省略され、最終的な回答は
{W->駅B}
となる。
導出
以上の工程は、一般的な推論のパターンに従う。
つまり、問合せ
?- $${Q_1, Q_2, …, Q_n}$$
に回答するためには、まず$${Q_1}$$に整合する結論Aを有する規則
$${A\coloneq B_1, …, B_m}$$
を見つける。(所謂カットです。)
次に問合せ
?-$${B_1, …, B_m, Q_2, …, Q_n}$$
について、同様に回答を見つける。
この推論パターンは、導出と呼ばれる。導出は、論理式に対して、宣言的解釈(真偽のいずれかの値をとる)の他に、手続的な解釈を加えるものである。
背理法
導出による証明の過程では、背理法として知られる技術が用いられる。つまり、証明すべき式が偽であると仮定して矛盾が導かれることを示し、それにより実際には与式が真であることを証明する。
例えば、駅Aとnearby関係にある駅を知りたいとする。この文を否定すると、駅Aとnearby関係にある駅は存在しない、となる。
これは、論理では、結論が空である規則として表される。つまり、前提が真であることにより偽が導かれる規則である。
$${\coloneq}$$nearby (駅A, W)
($${\lnot\;p \stackrel{def}{\equiv} p\to\bot}$$のことだと思われます。)
矛盾があるときは、導出により空規則が導かれる。空規則は、前提が恒真、結論が恒偽である。空規則は、$${\Box}$$として記述される。
(ここの説明はよく分かりませんでした。もしかしたら、詳しい説明が後ほどにあるのかも知れません。)
グランドと成功集合
nearby関係についての二つの定義が同じものであることを示すために、グランド事実と成功集合を導入する。
(二つの定義は、nearby関係の事実のリストによる定義と、nearby関係とconnected関係の規則による定義です)
グランド事実は変数を持たない事実である。
成功集合は、Gをグランド事実とするときに問合せ
?-G
が成功するようなGの集合である。
nearby関係の事実はグランド事実であり、かつそれらの事実からは何も演繹されない。したがって、一つ目の定義による成功集合は、事実のリストの要素のみからなる。
二つ目の定義による成功集合は、上述の規則をconnected関係のグランド事実に適用することで構成される。
以上から、二つの定義は、それらが同じ成功集合を有するとき、(手続的に)同じであると言える。
練習問題
私は練習問題に対する驚くべき答案の作成をしたが、その証明木を記述するにはnoteの数式機能は貧弱すぎる。
まとめ
今回は、後半の説明が分かり難くかったです。特に導出と背理法の関係がよく分かりませんでした。
また、基礎となる証明体系がはっきりしないので、統語論的な部分の理解に不安があります。
あと練習問題は、答案作成を証明図でしたのですが、代入を書き込むことができなかったので記載するのを止めました。
次回は、再帰(もしくは帰納)について学ぶ予定です。
古往今来得ざれば即ち書き得れば即ち飽くは筆の常也。と云うわけで御座います、この浅ましき乞食めに何卒皆々様のご慈悲をお願い致します。