6.2 ゴールの問い合わせ

Next: 7 組み込み述語 Up: 6 バックトラッキング Previous: 6.1 Primitiveな述語

6.2 ゴールの問い合わせ

つぎに，与えられたゴールを順に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>

という具合に走ります．

Next: 7 組み込み述語 Up: 6 バックトラッキング Previous: 6.1 Primitiveな述語

generated through LaTeX2HTML. M.Inaba 平成18年5月21日