Prologは定理証明系として、健全だが完全ではない
2013/08/15 @suharahiromichi
2014/04/19 @suharahiromichi、追記
2014/04/27 @suharahiromichi、Qiitaに投稿、後半を削除。
Prologの健全性と完全性
健全性と完全性
第一階述語論理（Horn節に限定）の定理証明系として、Prologは健全だが、完全ではない。
- 健全性：××が健全とは、全ての、××で証明できる論理式は、充足可能な論理式である。
- 完全性：××が完全とは、全ての、充足可能な論理式は、××で証明できる論理式である。
- 「全ての」は論理式にかかる。
- 「充足可能」とは、変数に具体的な値を当てはめて、と言い換えてよい。ただし述語論理なので、一般に変数のとりうる範囲は無限である。
- 「証明できる」とは、有限の証明がある、と言い換えてよい。
- 健全性と完全性は、「逆」の関係にある。
導出原理(Resolution)
Resolutionは、健全かつ完全である。
コワルスキの「論理による問題の解決」([文献1.])には、
証明手続の完全性を保証するためには、
探索空間が完全であるばかりでなく、
探索戦略もすべての場合を尽くさなければならない。
と書いてある。この本はPrologについて述べてはいないことに注意。
もう少し厳密にいうと、ResolutionにおけるSLD反駁そのものは計算規則について独立、つまり、導出のステップにおいて次にゴールのどの述語を展開するかを規定しない。
つまり、コワルスキは計算規則が適切であるならば完全だ、と言っているわけだ。
Prolog
Prologは、深さ優先探索をするので、完全性が保証されない。
Prologは、Resolutionにおける節の選択を、最左から深さ優先で探索することで実行するものである。SLD反駁の計算規則を厳密に定めたものがPrologであるといえる。
健全性はResolutionの場合と同様に成立する。ひとたび証明できてしまえば同じであるため。
例1
ゴールの最左の論理式が無限に展開できてしまう場合は証明が終わらず、その論理式は証明できないことになる。これは完全性に対する反例になっている。
「論理プログラミングの基礎」にある例 ([文献2.]p.59、表記は改めた)：
p(X, Z) :- q(X, Y), p(Y, Z).
p(X, X).
q(a, b).
?- p(X, b).
これは、X=aの解があるが、第一節を
p(X, Z) :- p(Y, Z), q(X, Y).
とするか、または、最右から深さ優先で探索すると、探索木の展開が無限になり、証明できない。
例2
Prologのようなシーケンシャルな探索をおこなう限り、証明できないプログラムが存在する。
「論理プログラミングの基礎」にある例 ([文献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.
?- p(a, c). % goal
これは、
p(a, c)
p(a, Y) , p(Y, c)
p(a, b) , p(c, Y)
(成功) p(c, b)
(成功)
と探索木が展開でき成功する。
これは人間が介入して恣意的に解いた場合であり、[文献2.]では「探索規則がフェアである」という（可能性を見過ごさないということ）。
しかし、シーケンシャルな探索はフェアではないので、3.を繰り返すか、4.を繰り替えしてしまい、終了しない。これも完全性に対する反例になっている。
出現チェック(Occurs Check)
ResolutionにおいてOccurs Checkを省くと健全性が失われる。
「論理プログラミングの基礎」にある例 ([文献2.]p.49、表記は改めた)：
test :- p(X, X).
p(X, f(X)).
?- test.
Occurs Checkをしない場合、p(X, X)とp(X, f(X))が一致してしまい、結果はyesとなる。これは、健全性に対する反例になっている。
Occurs Checkを省いても証明できる論理式が減ることはないので、完全性が失われることはない。
失敗による否定
失敗を否定とみなす規則とは、論理式Aの否定(~A)が証明できることを、Aがシーケンシャルな検索で失敗する（有限失敗）と定めることである。
有限失敗と否定の関係について、エルブラン・ベースを使った説明は以下を参照のこと。
http://qiita.com/suharahiromichi/items/eb619df5ffecadc1d763
参考文献
- R.コワルスキ、浦 監訳「論理による問題の解決」培風館
- J.W.ロイド、佐藤 他訳「論理プログラミングの基礎」産業図書
以上