시대 배경

현재는 우수한 Prolog 처리계를 무료로 입수할 수 있게 되었습니다. 그런데, Prolog가 주목되기 시작한 쇼와 50년대 후반에는, 보통의 사람이 사용할 수 있는 Prolog 처리계는 전무였습니다. 대형기 위에서 Fortran에서 구현된 Prolog 정도밖에 없었다고 듣고 있습니다.

S 표현 Prolog

그런 시대, 쇼와 58년에 나카지마 히데유키 선생님의 「Prolog」가 출판되었습니다. 잘 된 입문서일 뿐만 아니라, 권말에 Lisp1.5 상당으로 쓰여진 Prolog 처리계가 게재되고 있었습니다. 원래 bit잡지에 연재된 것이 Version1에서 서적에 게재된 것은 Version2입니다. 비트 잡지의 기사에서 나카지마 선생님은 다음과 같이 말합니다.

또, Prolog를 사용해 보고 싶지만, 가까이에 처리계가 없다고 하는 분들을 위해, Lisp로 쓴 PortableProlog를 보여줄 예정이다. (다음 번) Lisp도 가까이 있지 않다고 하는 분은, 잠시 참으면, 반드시 Prolog의 처리계가 나돌게 될 것이다.

실제로, 그 몇 년 후, PC에서도 움직이는 Prolog-KABA나 RUN-Prolog가 입수 가능하게 되었습니다만, 그동안, Prolog는 어떤 것이다? 라는 흥미로부터 S식 Prolog를 움직여 보았던 분도 많았던 것이 아닐까 생각합니다.

허락

벌써 10년 이상 전이 될 것 같아요. 나는 이 Prolog를 Scheme에 이식한 것을 공개하고 싶고, 나카지마 선생님에게 연락했습니다. 선생님은 매우 상냥한 분으로, 쾌락 받았습니다. 나는 나중에 사양이 거대 해지고 복잡해지는 Scheme을 벗어나 ISLisp에 안주 지역을 발견했습니다. 자작의 ISLisp(EISL)의 테스트를 위해서 이식한 곳, 어떻게든 동작을 하고 있는 것 같습니다.

실행 예

起動
Easy-ISLisp Ver0.42
> T
> (prolog)
Portable Prolog (in ISLisp)
: 

member述語の定義、実行
: (assert (member *x (*x . *y)))
defined
T
: (assert (member *x (*x1 . *y))(member *x *y)) 
defined
T
: (member 2 (1 2 3))
T
: (member 4 (1 2 3))
NIL
: 

변수는 앞에 *를 붙입니다.

: (member *x (1 2 3))
T
: 

내장 술어는 Lisp 함수를 사용하여 정의됩니다.

: (assert (print *x) (call print *x))
defined
T
: (member *x (1 2 3))(print *x)
T

: *X

어라? , 표시되지 않습니다. 이식이 불완전할 수 있습니다.

계산도 Lisp 함수를 호출합니다.

: (assert (plus *x *y *z) (eval (+ *x *y) *z) (print *z))
defined
T
: (plus 1 2 *x)
3
NIL
: 

끝날 때는 halt로 하고 있습니다.

: (halt)
TNIL
> 

이 S식 Prolog는 쇼와 60년 정도에 제품으로서 판매된 LISP09라고 하는 것에 이식되어 PROLOG09로서 동작하고 있었습니다. 증명 부분을 어셈블러로 내장 함수로 하여 실행 속도를 올리고 있었습니다. 판매는 별광전자라는 곳에서 FLEX-DOS용이었다고 생각합니다.

상업

ISLisp라고 하는 국제 표준 규격에 끌어들여, 스스로도 처리계를 자작했습니다. Easy-ISlisp 약칭 EISL이라고합니다. Windows, Linux에서 작동합니다. 구조도 간단하기 때문에 Mac에서도 쉽게 컴파일 가능하다고 생각합니다. 전자 서적에서 소스 코드와 함께 판매하고 있습니다. 원한다면 읽으십시오.

코드

;;; protable prolog interpreter  ver2.0 by H.Nakashima 1983.04.09
;;;                                     modified for ISLisp by K.Sasagawa
;;;                                     modified Ver0.11 2016/10     

;;; usage
;;; (assert (member *x (*x . *y)))
;;; (assert (member *x (*x1 . *y))(member *x *y)) 
;;; 
;;; (assert (print *x) (call print *x))
;;; (assert (plus *x *y *z) (eval (+ *x *y) *z) (print *z))

(defglobal fetched-subst '())
(defglobal undo-list '())
(defglobal epilog nil)

(defun display (x)
  (format (standard-output) "~A" x))

(defun newline ()
  (format (standard-output) "~%"))

;;in ISLisp when cdr recieve nil, invoke error.
;;so, cdr* is compatible with Common Lisp
(defun cdr* (x)
  (if (null x)
      nil
      (cdr x)))

(defun caar (x)
  (car (car x)))

(defun cadr (x)
  (car (cdr* x)))

(defun cddr (x)
  (cdr* (cdr* x)))

(defun cddar (x)
  (cdr* (cdr* (car x))))

(defun prolog ()     
  (display "Portable Prolog (in ISLisp)")
  (set-up)
  (for ()
       (epilog) 
       (setq fetched-subst '())
       (setq undo-list '())
       (display (refutes (cons (read-with-prompt) '())
                         (cons '() '())
                         (cons '() '())
                         '())))
  (setq epilog nil))

(defun read-with-prompt ()
  (newline)
  (display ": ")
  (read))

(defun define-clause (clause)
  (let ((definition (property (caar clause) 'prolog)))  
    (if (not definition)
        (set-property (cons clause '()) (caar clause) 'prolog )
        (set-property (append definition (cons clause '()))(caar clause) 'prolog))
    (display "defined") (newline)
    t))

(defun refutes (clause old-subst new-subst cue)
  (cond ((null clause)
         (cond ((null cue) '*s*)
               (t (refutes (car (first cue))
                           (cdr* (first cue))
                           (cons '() '())
                           (cdr* cue)))))
        ((and (varp clause) (assignedp clause old-subst))
         (refutes (fetch-value clause old-subst)
                  fetched-subst
                  new-subst
                  cue))
        ((and (varp (first clause)) (assignedp (first clause) old-subst))
         (refutes (cons (fetch-value (first clause) old-subst) '())
                  fetched-subst
                  new-subst
                  (cons (cons (cdr* clause) old-subst cue))))
        (t
          (refute clause (property (caar clause) 'prolog) old-subst new-subst cue))))

(defun refute (clause definitions old-subst new-subst cue)
  (cond ((not definitions) ;;definition==nil means that clause is system predicate
         (cond ((and (try-sys (car clause) old-subst)
                     (refutes (cdr* clause)
                              old-subst
                              (cons '() '())
                              cue))
                t)
               (t (undo undo-list))))
        ;;else cluase is user defined predicate
        (t (resolve clause definitions new-subst old-subst cue))))


;;prove user defined predicate
(defun resolve (clause definitions new-subst old-subst cue)
         ;;if definition of clause is null, then end.
   (cond ((null definitions) nil)
         ;;check unification of head part. if unify head check body part.  
         ((and (unify (car clause) old-subst (caar definitions) new-subst)
               (refutes (cdr* (first definitions))
                        new-subst
                        (cons '() '())
                        (cons (cons (cdr* clause) old-subst) cue)))
          t)
         ;;if not unify, undo and check next definition
         (t (undo undo-list)
            (resolve clause (cdr* definitions) new-subst old-subst cue))))

;;unbind variables for back-track
(defun undo (u)
  (cond ((null u) (setq undo-list '()) nil)
        (t
          (set-cdr (cddar u)(car u))
          (undo (cdr* u)))))

(defun link (x x-subst y y-subst)
  (cond ((and (eq x y) (eq x-subst y-subst)) t)
        (t (setq undo-list (cons 
                             (set-cdr
                               (cons
                                 (cons x
                                       (cons (fetch y y-subst)
                                             fetched-subst))
                                 (cdr* x-subst))
                             x-subst)
                             undo-list)))))


(defun unify (x x-subst y y-subst)
  (cond ((varp x)
         (cond ((assignedp x x-subst)
                (unify (fetch x x-subst) fetched-subst y y-subst))
               (t (link x x-subst y y-subst))))
        ((varp y) (unify y y-subst x x-subst))
        ((atom x) (eql x y))
        ((atom y) nil)
        ((unify (car x) x-subst (car y) y-subst)
         (unify (cdr* x) x-subst (cdr* y) y-subst))
        (t nil)))


(defun fetch (x subst)
  (setq fetched-subst subst)
  (cond ((varp x)
         (let ((v (assoc x (cdr* subst))))
           (cond ((not v) x)
                 (t (setq fetched-subst (cddr v))
                    (fetch (second v) (cddr v))))))
        (t x)))

;;set system predicate
(defun set-up ()
  (set-property (lambda (form subst) (define-clause (fetch-value form subst)))
                'assert
                'primitive)

  (set-property (lambda (form subst) 
                  (let ((f (fetch-value (first form) subst)))
                    (apply (symbol-function f)
                             (mapcar (lambda (x) (fetch-value x subst))
                                     (cdr* form)))))
                'call
                'primitive)

  (set-property (lambda (form subst) (setq epilog t))
                'halt
                'primitive)

  (set-property (lambda (form subst)
                  (let ((f (fetch-value (car (first form)) subst)))
                    (cond ((unify (apply (symbol-function f)
                                         (mapcar (lambda (x) (fetch-value x subst))
                                              (cdr* (first form))))
                                  subst
                                  (second form)
                                  subst)
                           t)
                          (t nil))))
                'eval
                'primitive))

;;execute system predicate
(defun try-sys (form subst)
  (if (property (car form) 'primitive)
      (apply (property (car form) 'primitive) (list (cdr* form) subst))
      nil))

;;Is it variable? ex *x *y 
(defun varp (x)
  (and (symbolp x)
       (char= (aref (convert x <string>) 0) #\*)))

(defun assignedp (x subst)
  (assoc x (cdr* subst)))

(defun fetch-value (x subst)
  (cond ((varp x)
         (let ((v (assoc x (cdr* subst))))
           (if (not v)
               x
               (fetch-value (second v) (cddr v)))))
        ((atom x) x)
        (t (cons (fetch-value (car x) subst)
                 (fetch-value (cdr* x) subst)))))


(defun first (x)
  (car x))

(defun second (x)
  (cadr x))

(defun third (x)
  (caddr x))