;;; Prolog in Lisp: February 14th 2017 - February 18th 2017

;;;

;;; From Peter Norvig's book: Chapter 11

;;; "

Paradigms of Artificial Intelligence Programming"

;;;

;;; Unification, Prolog, Resolution, inference control strategies

;;;

;;; Posted:

; http://interweave-consulting.blogspot.co.uk/2017/02/a-simple-prolog-interpreter-in-lisp.html

;;;

;;; Reminder: (how to load and access files)

;;;

; (load "C:\\Users\\HP Owner\\Google Drive\\Lisp\\Prog-Prolog\\Prolog-in-Lisp.lisp")

;;;

;;; --- Unification ---

;;;

(defconstant +fail+ nil "Indicates pat-match failure.")

(defconstant +no-bindings+ '((t . t))

"Indicates pat-match success but with no variables.")

(defun variable-p (x) ; Symbol -> Bool

"Is x a variable, a symbol beginning with '?'"

(and (symbolp x) (equal (char (symbol-name x) 0) #\? )))

(defun get-binding (var bindings)

"Find a (variable . value) pair in a binding list."

(assoc var bindings))

(defun binding-val (binding)

"Get the value part of a single binding."

(cdr binding))

(defun lookup (var bindings)

"Get the value part (for var) from a binding list."

(binding-val (get-binding var bindings) ))

(defun extend-bindings (var val bindings)

"Add a (var . value) pair to a binding list, remove (t . t)"

(cons (cons var val) (if (equal bindings +no-bindings+) nil bindings)))

(defparameter *occurs-check* t "Should we do the occurs check?")

(defun unify (x y &optional (bindings +no-bindings+)) ; -> Bindings

"See if x and y match with given bindings"

(cond ((eq bindings +fail+) +fail+)

((eql x y) bindings)

((variable-p x) (unify-variable x y bindings))

((variable-p y) (unify-variable y x bindings))

((and (consp x) (consp y))

(unify (rest x) (rest y)

(unify (first x) (first y) bindings) ) )

(t +fail+) ) )

(defun unify-variable (var x bindings) ; -> Bindings

"Unify var with x, using (and maybe extending) bindings"

(cond ((get-binding var bindings)

(unify (lookup var bindings) x bindings))

((and (variable-p x) (get-binding x bindings))

(unify var (lookup x bindings) bindings))

((and *occurs-check* (occurs-check var x bindings))

+fail+)

(t (extend-bindings var x bindings))))

(defun occurs-check (var x bindings) ; -> Bool

"Does var occur anywhere 'inside x'?"

(cond ((eq var x) t)

((and (variable-p x) (get-binding x bindings))

(occurs-check var (lookup x bindings) bindings))

((consp x) (or (occurs-check var (first x) bindings)

(occurs-check var (rest x) bindings)))

(t nil)))

(defun unifier (x y )

"Return something that unifies with both x and y (or +fail+)"

(subst-bindings (unify x y) x ) )

(defun subst-bindings (bindings x) ; Bindings x Term -> Term

"Substitute the value of variables in bindings into x,

taking recursively bound variables into account"

(cond ((eql bindings +fail+) +fail+ )

((eql bindings +no-bindings+) x)

((and (variable-p x) (get-binding x bindings))

(subst-bindings bindings (lookup x bindings) ))

((atom x) x)

( t (cons (subst-bindings bindings (car x))

(subst-bindings bindings (cdr x )) ) ) ) )

;;; --- Now let's try unify on some examples ---

;

; (setf b '((?Z . ?X) (?Y . 4) (?X . 3)))

; (subst-bindings b '?y) ; => 4

; (subst-bindings b '?z) ; => 3

; (subst-bindings b '(f ?z ?y)) ; => (F 3 4)

;

; (unify '(?x ?y a) '(?y ?x ?x)) ; => ((?Y . A) (? X . ?Y))

; (unify '?x '(f ?x)) ; => NIL (occurs check nil: ((?X F ?X)))

; (unify '(?x ?y) '((f ?y) (f ?x)) ; => NIL (occurs check)

; (unify '(?x ?y ?z) '((?y ?z) (?x ?z) (?x ?y))) => NIL (occurs check)

; (unify 'a 'a) ; => ((T . T))

;

; Finally, the function unifier calls unify and substitutes

; the resulting binding list into one of the arguments.

; The choice of x is arbitrary; an equal result would come

; from substituting the binding list into y.

; Here are some examples of unifier:

; (unifier '(?x ?y a) '(?y ?x ?x)) ; => (A A A)

; (unifier '((?a * ?x ^ 2) + (?b * ?x) + ?c) '(?z + (4 * 5) + 3)) ; =>

; ((?A * 5 ^ 2) + (4 * 5) + 3)

;;;

;;; ----------------- Prolog Interpreter -----------------

;;;

#|

From

Wikipedia: Clause (logic)
Every nonempty clause is logically equivalent to an implication of a head

from a body, where the head is an arbitrary literal of the clause and the

body is the conjunction of the negations of the other literals. That is,

if a truth assignment causes a clause to be true and none of the literals

of the body satisfy the clause, then the head must also be true.

This equivalence is commonly used in logic programming, where clauses are

usually written as an implication in this form. More generally, the head

may be a disjunction of literals. If b

_{1},...,b

_{m} are the literals in the body

of a clause and h

_{1},...,h

_{n} are those of its head, the clause is usually

written as follows:

h

_{1},...,h

_{n} <- b

_{1},...,b

_{m}
If n=1 and m=0, the clause is called a (Prolog) fact.

If n=1 and m>0, the clause is called a (Prolog) rule.

If n=0 and m>0, the clause is called a (Prolog) query.

If n>1, the clause is no longer Horn.

|#

;; --- Clauses are represented as (head . body) cons cells: example ---

;

; ( (member ?item (?item . rest))) ) ; fact

; ( (member ?item (?x . ?rest)) . ((member ?item ?rest))) ; rule

(defun clause-head (clause) (first clause)) ; Clause -> Literal

(defun clause-body (clause) (rest clause)) ; Clause -> Literal-list

;; Clauses are stored on the predicate's plist

(defun get-clauses (pred) (get pred 'clauses)) ; symbol -> Clause-list

(defun predicate (literal) (first literal)) ; Literal -> Symbol (predicate)

(defvar *db-predicates* nil

"A list of all predicates stored in the database")

(defmacro <- (&rest clause)

"Add a clause to the database"

`(add-clause ',clause))

; (macroexpand-1 '(<- (likes Kim Robin))) ; =>

; (ADD-CLAUSE (QUOTE ((LIKES KIM ROBIN)))) ; ... which is correct.

(defun replace-?-vars (exp)

"Replace any ? within exp with a var of the form ?123"

(cond ((eq exp '?) (gensym "?"))

((atom exp) exp)

(t (cons (replace-?-vars (first exp))

(replace-?-vars (rest exp))) )) )

(defun add-clause (clause)

"Add a clause to the data base, indexed by head's predicate"

;; The predicate must be a non-variable symbol.

(let* ((clause1 (replace-?-vars clause))

(pred (predicate (clause-head clause1))))

(assert (and (symbolp pred) (not (variable-p pred))))

(pushnew pred *db-predicates*)

(setf (get pred 'clauses)

(nconc (get-clauses pred) (list clause1))) pred) )

; (setf clause '((P ?x ?y) . ((Q ?x ?y))))

; (add-clause clause) ; => P

; *db-predicates* ; => (P)

; (get 'P 'clauses) ; (((P ?X ?Y) (Q ?X ?Y)))

(defun clear-db ()

"Remove all clauses (for all predicates) from the database"

(mapc #'clear-predicate *db-predicates*))

(defun clear-predicate (predicate)

"Remove the clauses for a single predicate"

(setf (get predicate 'clauses) nil) )

;;; So here is an example:

;;; clause = '((P ?x ?y) . ((Q ?x ?y)))

;;; goal = '(P a b)

;;;

;;; ----------------------------------------------------------------------------------

;;; and here is how 'prove' works:

;;;

;;; (get-clauses (predicate goal)) finds 'clause' = '((P ?x ?y) . ((Q ?x ?y)))

;;; 'clause' would then get variable-renamed -> new-clause

;;; Get binding from (unify goal (clause-head new-clause) bindings)

;;; Using that binding, try to prove clause body literals

;;; Return bindings (via prove-all)

(defvar *countr* 0) ; count how many times 'prove' is called

(defun count-prove-calls ()

(setf *countr* (1+ *countr*))

(format t "~& Call to prove = ~a" *countr*) )

(defun prove (goal bindings) ; Literal x Bindings -> Bindings

"Return a 1ist of possible solutions to goal"

(count-prove-calls)

(mapcan #'(lambda (clause)

(let ((new-clause (rename-variables clause)))

(prove-all (clause-body new-clause)

(unify goal (clause-head new-clause) bindings))))

(get-clauses (predicate goal))))

(defun prove-all (goals bindings) ; Literal-list x Bindings -> Bindings

"Return a list of solutions to the conjunction of goals"

(cond ((eql bindings +fail+) +fail+)

((null goals) (list bindings))

(t (mapcan #'(lambda (goal1-solution)

(prove-all (rest goals) goal1-solution))

(prove (first goals) bindings)))))

(defun rename-variables (x) ; clause -> clause (with vars renamed)

"Replace all variables in x with new ones"

(sublis (mapcar #'(lambda (var) (cons var (gensym (string var))))

(variables-in x))

x))

; (setf clause '((P ?X ?Y) (Q ?X ?Y)))

; (rename-variables clause) ; => ((P #:?X932 #:?Y933) (Q #:?X932 #:?Y933))

;

; (setf clause1 '((F (G ?x (H ?y)) (J ?u ?v))))

; (rename-variables clause1) ; => ((F (G #:?X872 (H #:?Y873)) (J #:?U874 #:?V875)))

; This version of ?- superseded by later definition below

; (defmacro ?- (&rest goals) `(prove-all ',goals +no-bindings+))

;;; --- Example ---

#|

(add-clause '((likes Kim Robin)))

(add-clause '((likes Sandy Lee)))

(add-clause '((likes Sandy Kim)))

(add-clause '((likes Robin cats)))

(add-clause '((likes Sandy ?x) (likes ?x cats)))

(add-clause '((likes Kim ?x) (likes ?x Lee) (likes ?x Kim)))

(add-clause '((likes ?x ?x)))

(prove '(likes Sandy ?who) +no-bindings+) ; =>

; (((?WHO . LEE))

; ((?WHO . KIM))

; ((#:?X846 . ROBIN)

; (?WHO . #:?X846))

; ((#:?X850 . CATS) (#:?X847 . CATS) (#:?X846 . SANDY) (?WHO . #:?X846))

; ((#:?X855 . CATS) (#:?X846 . #:?X855) (?WHO . #:?X846))

; ((?WHO . SANDY) (#:?X857 . SANDY)))

; -- and here with macros <- and ?- ---

(<- (likes Kim Robin))

(<- (likes Sandy Lee))

(<- (likes Sandy Kim))

(<- (likes Robin cats))

(<- (likes Sandy ?x) (1ikes ?x cats))

(<- (likes Kim ?x) (likes ?x Lee) (likes ?x Kim))

(<- (likes ?x ?x)

> (?- (likes Sandy ?who))

; (((?WHO . LEE))

; ((?WHO . KIM ) )

; ((?X2856 . ROBIN) (?WHO . ?X2856))

; ((?X2860 . CATS) (?X2857 . CATS) (?X2856 . SANDY) (?WHO . ?X2856))

; ((?X2865 . CATS) (?X2856 . ?X2865) (?WHO . ?X2856))

; ((?WHO . SANDY) (?X2867 . SANDY)))

|#

;;; --- TOP-LEVEL-PROVE ---

(defmacro ?- (&rest goals) `(top-level-prove ',(replace-?-vars goals)))

; (macroexpand-1 '(?- goals)) ; Check macro expands properly

(defun variables-in (exp)

"Return a list of all the variables in exp"

(unique-find-anywhere-if #'variable-p exp))

(defun unique-find-anywhere-if (predicate tree &optional found-so-far)

"Return a list of leaves of tree satisfying predicate, with duplicates removed"

(if (atom tree)

(if (funcall predicate tree) (adjoin tree found-so-far) found-so-far)

(unique-find-anywhere-if predicate (first tree)

(unique-find-anywhere-if predicate (rest tree) found-so-far)

)))

(defun top-level-prove (goals)

"Prove the goals, and print variables readably"

(show-prolog-solutions (variables-in goals) (prove-all goals +no-bindings+)))

(defun show-prolog-solutions (vars solutions)

"Print the variables in each of the solutions"

(if (null solutions)

(format t "~&No.")

(mapc #'(lambda (solution) (show-prolog-vars vars solution)) solutions))

(values))

(defun show-prolog-vars (vars bindings)

"Print each variable with its binding"

(if (null vars)

(format t "~&Yes")

(dolist (var vars)

(format t "~&~a = ~a" var (subst-bindings bindings var))))

(princ ";"))

;;; --- Examples ---

; Now let's try some queries:

;

; (?- (likes Sandy ?who))

;

; ?WHO = LEE;

; ?WHO = KIM;

; ?WHO = ROBIN;

; ?WHO = SANDY;

; ?WHO = CATS;

; ?WHO = SANDY;

;

;

; ( ?- (likes ?who Sandy))

;

; ?WHO = SANDY;

; ?WHO = KIM;

; ?WHO = SANDY;

;

; ( ?- (likes Robin Lee))

;

; No.

;

;---

;

;For a more sophisticated test, try the

Zebra Puzzle at:

;

; http://interweave-consulting.blogspot.co.uk/2017/02/the-zebra-puzzle-prolog-in-lisp.html

;

; ----------------- End ------------------