Prologで論理的にプログラミングを学んでいます（節形式論理：入門）

　AI言語Prologによるプログラミング学習の第2回です。テキストは、地味に論理的です。
　内容は、節形式論理の簡単な概要の入門編です。

路線図

　以下の説明の宇宙（言及の範囲）は、地下鉄の路線図である。
　路線図には路線、駅、乗り換え等の情報が含まれている。その情報を論理的文として捉えることを試みる。

connected事実

　路線図には、どの駅と駅とが、どの路線で直接に接続されているかが示されている。これより、以下の式が取り出される。

connected (駅A, 駅B, 路線L).

　（この式は、「二つの駅A, Bは路線Lにより直接に接続される」ことを意味します。言い換えれば「路線Lの駅A, Bは隣り合う」です。例えば、新幹線の新横浜駅と品川駅は、隣り合っているので、新幹線で直接接続されることになります。）

nearby事実

　二つの駅が同じ路線にあり、それらの間に存在する駅が高々一つであるとき、二つの駅は近い'nearby'であると定義する。

nearby (駅A, 駅B).

　（新幹線の例では、新横浜と品川、新横浜と東京はnearbyです。下りも同様です。）

nearby規則

　nearbyの式は、connectedの式から規則的に導き出される。
　具体的には、駅Xと駅Yが路線Lにより直接に接続されているならば、XとYはnearbyである。
　もしくは、駅Xと駅Zが路線Lで直接に接続され、かつ駅Zと駅Yが路線Lで直接に接続されるならば、XとYはnearbyである。

　これは、以下にのように形式化することができる。

nearby (X, Y) :- connected (X, Y, L).
nearby (X, Y) :- connected (X, Z, L), connected (Z, Y, L).

　これらの式において、記号':-'は「…ならば」として読め、connectedとの間の','は「かつ」として読める。
　（':-'は含意です。ただし、Prologの記法では前提と結論を前後逆さまに記述するので、結論:-前提となります。','はそのまま連言です。）
　（これら上下の式を結合する論理結合子についての言及はありませんが、連言で結ばれています。これについて「まとめ」に少し書きました。）

　大文字は、全称量化された変数である。例えば、二つ目の式の意味は、

　任意のX, Y, Z, Lについて、LによりXがZに直接接続され、かつLによりZがYに直接接続されるならば、XとYはLにより直接接続される

である。

定義の違い

　nearby関係について二つの定義をした。一つは、駅の対からなる単純なリストによる定義であり、そのリストの全ての対は互いにnearbyである。もう一つは、直接接続の点での定義である。
　前者の種類の式を、事実と呼び。後者の種類の式を、規則と呼ぶ。

事実
nearby (X, Y).
規則
nearby (X, Y) :- connected (X, Y, L).
nearby (X, Y) :- connected (X, Z, L), connected (Z, Y, L).

　事実は、無条件の真理である。
　一方、規則は条件付きの真理である。すなわち、前提が真と知られている場合に限り引き出される結論である。

　これら二つの定義は同値であることが求められる。

練習問題

　二つの駅が同じ、または別の路線にあり、それらの間に高々一つの駅が存在するとき、二つの駅は遠くない'not too far'であると定義する。
　述語not_too_farの規則を定義せよ。

答案

　nearbyとnot_too_farの関係を考えます。
　not_too_farは、路線に拘らず、二つの駅の位相的関係だけで定義されています。
　一方、nearbyは、not_too_farにおける駅の関係にさらに路線を同じものに限定した定義になっています。
　ここで、nerabyの定義を見ると

　nearby (X, Y) :- connected (X, Z, L), connected (Z, Y, L).

二つのconnectedで同じ束縛変数Lを用いることで、路線を同じものに限定しています。
　そこで、どちらかのconnectedにL以外の束縛変数を用いることで、not_too_farの定義になります。（もちろん新たな変数は全称量化子で束縛されます。）
　したがって、答えは、

not_too_far (X, Y) :- connected (X, Z, L), connected (Z, Y, K).
（さらに、直接接続されている駅も当然にnot_too_farなので）
not_too_far (X, Y) :- connected (X, Y, L).　

です。

---

まとめ

　今回は、節形式論理の入門について学びました。今回もテキストの説明が丁寧でわかりやすかったです。

　説明はわかりやすかったのですが、内容にはピンとこない箇所がありました。それは、connectedによるnearbyの定義です（今回の肝なのに）。

　「二つの駅が同じ路線にあり、それらの間に存在する駅が高々一つであるならば、二つの駅はnearbyである」を素直に式にするとすれば、

$${\forall x\forall y[\exist l(conneted (x, y, l) \lor \exist z(conneted (x, z, l)\land connected (z, y, l)))\to nearby(x, y)]}$$

になるのではないのでしょうか。

　ここから式を変形していくと、

$${\forall x\forall y[\neg\neg\exist l(conneted (x, y, l) \lor \exist z(conneted (x, z, l)\land connected (z, y, l)))\to nearby(x, y)]}$$

$${\forall x\forall y\forall z\forall l[(\neg conneted (x, y, l) \land \neg(conneted (x, z, l)\land connected (z, y, l))) \lor nearby(x, y)]}$$

$${\forall x\forall y\forall z\forall l[(conneted (x, y, l)\to nearby(x, y) ) \land ((conneted (x, z, l)\land connected (z, y, l))\to nearby(x, y) )]}$$

と、確かにテキスト通りの冠頭標準形になるのですが、しっくりきません。馴れの問題なのでしょうか。

　次回は、問合せと回答について学ぶ予定です。Prologの学習はこれまでの言語のなかで最も興味深いです。が、内容も深いです。次回の公開はいつになることやら…