Next: 7 組み込み述語
Up: 6 バックトラッキング
Previous: 6.1 Primitiveな述語
与えられたゴールを順にproveで調べるために，prove-allを定義する．
proveはバインディング情報を返す関数とし，nilを返せば証明が成り立ち，
failを返せば証明が失敗するという意味をもたせて以下のように定義する．
ゴールの述語名をゴールとするホーン節を取り出し，そういったホーン節がな
にもなければ証明できないということで，failを返す．そして，取り出し
たホーン節がアトムであるということは，primitiveな述語であるという意味
にしてありため，その際には，そのアトムが関数名であると思って実行する
(funcall部）．ホーン節がある場合には，順にそのクローズの内部の変数
を変えたものをprove-allで調べてゆき，fail以外のものが返るまで調べる．
クローズをすべて調べてすべてがfailを返した場合には，provはfailを返す．
failしないホーン節があるということは，
(defun prove-all (goals &optional bindings)
(cond
((eq bindings 'fail) 'fail)
((null goals) bindings)
(t (prove (first goals) bindings (rest goals)))))
(defun top-level-prove (goals)
(prove-all `(,@goals
(show-prolog-vars
,@(variables-in goals))))
(format t "~&No.")
(values))
(defun show-prolog-vars (vars bindings other-goals)
(cond
((null vars) (format t "~&Yes"))
(t (dolist (var vars)
(format t "~&~a = ~a" var
(substitute-bindings bindings var)))))
(cond
((continue-p) 'fail)
(t (prove-all other-goals bindings))))
(defun init-prolog ()
(clrhash *prolog-database*)
(setf (gethash 'show-prolog-vars *prolog-database*)
'show-prolog-vars)
)
(defun continue-p ()
(case (read-char)
(#\; t)
(#\. nil)
(#\newline (continue-p))
(otherwise
(format t " Type ; to see more or . to stop")
(continue-p))))
この手続きを使えば，ひとつの答が表示されると人間が次の答がほしければセ
ミコロンをいれ，いらなければピリオドをうつ．
たとえば，
(defun example2 nil
(init-prolog)
(<- (member ?item (?item . ?rest)))
(<- (member ?item (?x . ?rest)) (member ?item ?rest))
(<- (length () 0))
(<- (length (?x . ?y) (1+ ?n)) (length ?y ?n)))
とすると，
<cl> (example2)
LENGTH
<cl> (?- (length (a b c) ?x))
?X = (1+ (1+ (1+ 0)));
No.
<cl> (?- (length () 0))
Yes;
No.
<cl> (?- (length (a b) 2))
No.
<cl> (?- (length (a) (1+ 0)))
Yes;
No.
<cl> (?- (length ?x (1+ 0)))
?X = (?X1929);
No.
<cl> (?- (length ?x (1+ 0))
(member ?x ((a) (b) (c))))
?X = (A);
?X = (B);
?X = (C);
No.
<cl> (?- (length ?l (1+ (1+ 0))) (member a ?l))
?L = (A ?X278);
?L = (?X283 A);
No.
<cl>
という具合に走る．
generated through LaTeX2HTML. M.Inaba 平成18年5月7日