Prologの表示的意味論

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


## エルブランの定理
以下は、互いに同値である。

1. Tp↑ω は、Tpの最小不動点 Lfp(Tp) である。
2. Tp↑ω は、プログラムPの最小エルブラン・モデルである。
3. A∈Tp↑ω の原始論理式Aは、プログラムPの論理的帰結である。
4. 〜Aは、Pのすべてのエルブラン・モデルで真である。
5. P∪{〜A} は、エルブラン・モデルを持たない。
6. P∪{〜A} は、充足不可能である。
7. 原始論理式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

![エルブラン・ベースの部分集合](https://raw.github.com/suharahiromichi/doc/master/cs_prolog_denotational_semantics.png "エルブラン・ベースの部分集合")

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

1. Tp↑ω             ：プログラムPの論理的帰結である。
幅優先の探索（ハイパーレゾリューション）で証明できる。正しい。

2. Gfp(Tp) - Tp↑ω   ：無限の探索木が作られる（無限ループ）。証明できない。

3. Tp↓ω   - Gfp(Tp) ：無限のバックトラックが起きる。証明できない。

4. Bp      - Tp↓ω   ：有限の探索木で失敗する。有限失敗(Fp)。


## 否定との関係

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

1. Bp - Tp↑ω      ：閉世界仮説に基づいて、~Aが推論される。

2. Bp - Gfp(Tp)    ：エルブラン規則により、~Aが推論される（要補足）。

3. 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は、最右深さ優先の計算規則の場合は探索木が無限になり、無限ループになる。


# 参考文献

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

以上