Prologの表示的意味論

2013/08/25 @suharahiromichi

2014/04/19 @suharahiromichi、否定について補足

エルブラン・ベース

PrologのプログラムPにおいて、
変数を定数項(例：a、f(b))に置き換えて、
出現しうるすべての原始論理式（例：p(a,f(b))）の集合をエルブラン・ベース Bp で表す。

代入

代入Θを次の例のように定義する。Θcは節cをΘで置き換えた結果を示す。

    例：
    Θ =  [X:=0]                    （変数Xを0で置き換える）
    c =  n(s(X)) :- n(X)
    Θc = n(s(0)) :- n(0)

    例：
    Θ =  [X:=a, Y:=f(b)]           （変数Xをaで、Yをf(b)で置き換える）
    c =  p(X, Y) :- q(Y)
    Θc = p(f(a), b) :- q(b)

前向き推論をする関数

関数 Tp を次のように定義する。
これは、←(:-)の右から左に前向きに推論を1ステップ実行するものである。

Tp(M) = {A∈Bp | ∀Θ, ∀c∈P, (A:-B1,B2,..Bn) = Θc, B1,B2,..Bn∈M⊆Bp}

例は後半に示す。

最小エルブラン・モデル

プログラムPのモデルとなるエルブラン・ベース Bp の部分集合
i⊆Bp をエルブラン解釈という。そのうちモデルであるのもを
エルブラン・モデルMiという。エルブラン・モデルの交わりを
プログラムPの最小エルブラン・モデル Mp と呼ぶ。

Mp = ∩(i⊆Bp)Mi

最小不動点

Tpの最小不動点 Lfp(Tp) = Tp↑ω ⊆Bp を次のようにもとめる。

Tp↑0 = {}
Tp↑1 = Tp(Tp↑0) ∪ Tp↑0
Tp↑2 = Tp(Tp↑1) ∪ Tp↑1
Tp↑n+1 = Tp(Tp↑n) ∪ Tp↑n
Tp↑ω = ∪(n=0,∞)Tp↑n

エルブランの定理

以下は、互いに同値である。

Tp↑ω は、Tpの最小不動点 Lfp(Tp) である。
Tp↑ω は、プログラムPの最小エルブラン・モデルである。
A∈Tp↑ω の原始論理式Aは、プログラムPの論理的帰結である。
〜Aは、Pのすべてのエルブラン・モデルで真である。
P∪{〜A} は、エルブラン・モデルを持たない。
P∪{〜A} は、充足不可能である。
原始論理式Aは、プログラムPの反駁(refutation)になる。

Pの最小不動点Tpは、Pを前向き推論して得られた結果の集合であるから、
前向き推論は健全かつ完全である。

操作的意味論（概略）

レゾリューション

後向きの推論によって反駁を求めることをレゾリューションという。
レゾリューションはPrologの操作的意味を示している。
後向きの推論であっても、幅優先であれば前向き推論と同じ結果となる。
ゆえに、レゾリューション（後向き推論）も健全かつ完全である。

実際のProlog処理系

実際のProlog処理系はレゾリューションにおいて、
最左優先・深さ優先の計算規則をとるものである（詳細は別途）。
後半でPrologが不完全、
つまり「Prologでは求められない論理的帰結がある」ことの実例を示す。

ここでは単一化（ユニフィケーション）においてOccures Check（出現チェック）は行うものとする。
Occures Checkを省くと健全性も失われる。

最大不動点

Tpの最大不動点 Gfp(Tp) = Tp↓(ω+1) ⊆Bp を次のようにもとめる。
最小不動点と異なり Gfp(Tp)≠Tp↓ω である。

Tp↓0 = Bp
Tp↓1 = Tp(Tp↓0) ∩ Tp↓0
Tp↓2 = Tp(Tp↓1) ∩ Tp↓1
Tp↓n+1 = Tp(Tp↓n) ∩ Tp↓n
Tp↓ω = ∩(n=0,∞)Tp↓n
Gfp(Tp) = Tp↓(ω+1) = Tp(Tp↓ω)

エルブラン・ベースの部分集合の関係

プログラムPにおいて、次の関係が成立する。

{} ⊆ Tp↑ω ⊆ Gfp(Tp) ⊆ Tp↓ω ⊆ Bp

それぞれに含まれる原始論理式は、以下の意味をもつ(「-」は差集合）。

Tp↑ω ：プログラムPの論理的帰結である。
幅優先の探索（ハイパーレゾリューション）で証明できる。正しい。
Gfp(Tp) - Tp↑ω ：無限の探索木が作られる（無限ループ）。証明できない。
Tp↓ω - Gfp(Tp) ：無限のバックトラックが起きる。証明できない。
Bp - Tp↓ω ：有限の探索木で失敗する。有限失敗(Fp)。

否定との関係

それぞれに含まれる原始論理式Aの否定(~A)は、以下の意味をもつ。

Bp - Tp↑ω ：閉世界仮説に基づいて、~Aが推論される。
Bp - Gfp(Tp) ：エルブラン規則により、~Aが推論される（要補足）。
Bp - Tp↓ω ：失敗を否定とみなす規則により、~Aが推論される。

失敗を否定とみなす規則とは、原始論理式Aが3.(Fp = Bp - Tp↓ω)に含まれるとき、すなわち、
Aが有限失敗であるとき、その否定「~A」を証明できたとすることである。
Prologでは、このときの「~A」を「\+A」と表記する。

例1

プログラムP

プログラムPを以下とする。 ([文献1]p.158)

n(0).                           % (1)
n(s(X)) :- n(X).                % (2)
d(s(X)) :- d(X).                % (3)
loop1 :- loop1.                 % (4)
loop2 :- d(X), n(X).            % (5)

エルブラン・ベースBp

プログラムPのエルブラン・ベースBpは、

Bp = {loop1, loop2,
      n(0), n(s(0)), n(s(s(0))),....
      d(0), d(s(0)), d(s(s(0))),....}

関数Tp

関数Tpの実行例を示す。

Tp({loop1, d(0)}) = {loop1, d(s(0)), n(0)}

値の最初の要素は(4)、二番目は(3)、三番目は(1)の節を使う。

最小不動点

Tp↑0 = {}
Tp↑1 = {n(0)}
Tp↑2 = {n(s(0)), n(0)}
Tp↑3 = {n(s(s(0))), n(s(0)), n(0)}
Tp↑ω = {n(s(s(...(0)))), .... , n(s(s(0))), n(s(0)), n(0)}

最大不動点

Tp↓0 = Bp = {loop1, loop2, n(0), n(s(0)), n(...), ... , d(0), d(s(0)), d(...), ... }
Tp↓1      = {loop1, loop2, n(0), n(s(0)), n(...), ... ,       d(s(0)), d(...), ... }
Tp↓2      = {loop1, loop2, n(0), n(s(0)), n(...), ... ,                d(...), ... }
Tp↓ω      = {loop1, loop2, n(0), n(s(0)), n(...), ... ,                            }
Gfp(Tp)   = {loop1,        n(0), n(s(0)), n(...), ... ,                            }

Tp↓ω で、節3によってd(...)が消える。
Gfp(Tp)=Tp(Tp↓ω)で、節5によってloop2が消える。

Gfp(Tp) - Tp↑ω = {loop1} （無限ループ）
Tp↓ω - Gfp(Tp) = {loop2} （無限バックトラック）
Bp - Tp↓ω = {d(0), d(s(0)), ... } （有限失敗）

プログラム2

[文献2.]p.58

p(X, Z) :- q(X, Y), p(Y, Z).        % (1)
p(X, X).                            % (2)
q(a, b).                            % (3)

最小不動点は以下になる。

Tp↑1 = {q(a, b)}
Tp↑2 = {p(a, b), q(a, b)}
Tp↑ω = {p(a, b), q(a, b)}

p(a, b) は、Tpの最小不動点に含まれるので、論理的帰結である。
最左深さ優先の計算規則のとき、有限の木で反駁が求められる。しかし、
最右深さ優先の計算規則のとき（または、(1)節の尾部をp(Y,Z), q(X,Y)と逆にする）、
無限の木が作られ、証明が終わらない。
Prologの計算規則では求められない論理的帰結があること(Prologの不完全性)の例となる。

プログラム3

[文献2.]p.62

p(a, b).                             % (1)
p(c, b).                             % (2)
p(X, Z) :- p(X, Y), p(Y, Z).         % (3)
p(X, Y) :- p(Y, X).                  % (4)

最小不動点は以下になる。

Tp↑1 = {p(a, b), p(c, b)}
Tp↑2 = {p(b, a), p(b, c), p(a, b), p(c, b)}
Tp↑3 = {p(a, c), p(b, b), p(b, a), p(b, c), p(a, b), p(c, b)}
Tp↑ω = ...

p(a, c)は、Tpの最小不動点に含まれるので論理的帰結である。しかし、
Prologで深さ優先探索をおこなうがぎり、探索木は無限になり終了しない。
計算規則や節の順番を入れ替えても、深さ優先探索をする限り解消できない。これは、
Prologの計算規則では求められない論理的帰結があること(Prologの不完全性)の例となる。

プログラム4

[文献1]p.158

loop1 :- loop1.
loop3 :- loop1, loop0.
loop4 :- loop0, loop1.

最大不動点は以下になる。

Tp↓0 = Bp = {loop0, loop1, loop3, loop4}
Tp↓1      = {       loop1, loop3, loop4}
Tp↓2      = {       loop1              }
Tp↓ω      = {       loop1              }
Gfp(Tp)   = {       loop1              }

loop0, loop3, loop4 は、有限失敗（Fp = Bp - Tp↓ω）だが、
loop3は、最左深さ優先の計算規則の場合は探索木が無限になり、無限ループになる。
loop4は、最右深さ優先の計算規則の場合は探索木が無限になり、無限ループになる。

参考文献

萩谷、「論理プログラム混沌の中」bit Vol.16, No.6 共立出版
J.W.ロイド、佐藤他訳「論理プログラミングの基礎」産業図書
R.コワルスキ、浦監訳「論理による問題の解決」培風館、p.87、p.78訳注

以上