--- a/package.lisp Thu Mar 10 15:14:48 2016 +0000
+++ b/package.lisp Thu Mar 10 18:22:56 2016 +0000
@@ -6,5 +6,8 @@
(:use #:cl #:defstar #:bones.utils)
(:export #:unify
#:fail #:no-bindings
- #:*check-occurs*))
+ #:*check-occurs*
+ #:clear-db
+ #:fact #:rule
+ #:find-all #:query))
--- a/src/paip.lisp Thu Mar 10 15:14:48 2016 +0000
+++ b/src/paip.lisp Thu Mar 10 18:22:56 2016 +0000
@@ -2,7 +2,7 @@
;;;; Types
(deftype logic-variable ()
- 'keyword)
+ 'symbol)
(deftype binding ()
'(cons logic-variable t))
@@ -27,7 +27,10 @@
(defun* variable-p (term)
(:returns boolean)
"Return whether the given term is a logic variable."
- (keywordp term))
+ (and (symbolp term)
+ (equal (char (symbol-name term) 0)
+ #\?)))
+
(defun* get-binding ((variable logic-variable)
(bindings binding-list))
@@ -35,6 +38,12 @@
"Return the binding (var . val) for the given variable, or nil."
(assoc variable bindings))
+(defun* has-binding ((variable logic-variable)
+ (bindings binding-list))
+ (:returns boolean)
+ (not (null (get-binding variable bindings))))
+
+
(defun* binding-variable ((binding binding))
(:returns logic-variable)
"Return the variable part of a binding."
@@ -44,6 +53,7 @@
"Return the value part of a binding."
(cdr binding))
+
(defun* lookup ((variable logic-variable)
(bindings binding-list))
"Return the value the given variable is bound to."
@@ -55,10 +65,11 @@
(:returns binding-list)
"Add a binding (var . val) to the binding list (nondestructively)."
(cons (cons variable value)
- (if (and (eq bindings no-bindings))
+ (if (and (equal bindings no-bindings))
nil
bindings)))
+
(defun* check-occurs ((variable logic-variable)
(target t)
(bindings binding-list))
@@ -228,65 +239,97 @@
(mapc #'clear-predicate *db-predicates*))
+(defun unique-find-anywhere-if (predicate tree &optional acc)
+ (if (atom tree)
+ (if (funcall predicate tree)
+ (adjoin tree acc)
+ acc)
+ (unique-find-anywhere-if predicate
+ (first tree)
+ (unique-find-anywhere-if predicate (rest tree) acc))))
+
+(defun variables-in (expr)
+ (unique-find-anywhere-if #'variable-p expr))
+
(defun rename-variables (form)
"Replace all variables in the form with new (unique) ones."
- (sublis (mapcar #'(lambda (variable) (cons variable (gensym (string var))))
+ (sublis (mapcar #'(lambda (variable)
+ (cons variable (gensym (string variable))))
(variables-in form))
form))
+(defun prove-single-clause (goal bindings clause)
+ (let ((new-clause (rename-variables clause)))
+ (prove-all (clause-body new-clause)
+ (unify goal (clause-head new-clause) bindings))))
+
+(defun prove (goal bindings)
+ ;; We look up all the possible clauses for the goal and try proving
+ ;; each individually. Each one will give us back a list of possible
+ ;; solutions.
+ ;;
+ ;; Then we concatenate the results to return all the possible
+ ;; solutions.
+ (mapcan (curry #'prove-single-clause goal bindings)
+ (get-clauses (predicate goal))))
+
(defun prove-all (goals bindings)
"Returns a list of solutions to the conjunction of goals."
- ;; strap in, here we go.
- (labels ((prove-single-clause
- (goal clause bindings)
- "Try to prove a goal against a single clause using the given bindings.
+ (cond
+ ;; If something failed further up the pipeline, bail here.
+ ((eq bindings fail) fail)
- Return all possible solutions as a list of binding-lists.
+ ;; If there's nothing to prove, it's vacuously true. Return a list of the
+ ;; bindings as the result.
+ ((null goals) (list bindings))
- "
- ;; Try to prove a goal against a specific clause:
- ;;
- ;; (likes sally kim)
- ;; ((likes sally :x) (likes :x cats))
- ;;
- ;; To do this, we try to unify the goal with the head of the clause,
- ;; and then use the resulting bindings to prove the rest of the
- ;; items in the clause.
- ;;
- ;; First rename the variables in the clause, because they stand on
- ;; their own and shouldn't be confused with ones in the bindings.
- (let ((new-clause (rename-variables clause)))
- (prove-all (clause-body new-clause)
- (unify goal (clause-head new-clause) bindings))))
- (prove
- (goal bindings)
- "Try to prove a goal, using the given bindings.
+ ;; Otherwise we try to prove the first thing in the list. This gives us
+ ;; back a list of possible bindings we could use.
+ ;;
+ ;; For each possible solution to the head, we try using it to prove the
+ ;; rest of the goals and concatenate all the results. Failed attempts are
+ ;; represented as FAIL which is nil, so will collapse in the concatenation.
+ (t (mapcan #'(lambda (possible-solution)
+ (prove-all (rest goals) possible-solution))
+ (prove (first goals) bindings)))))
+
+(defun show-variables (variables solution)
+ (if (null variables)
+ (format t "~&Yes")
+ (dolist (var variables)
+ (format t "~&~A = ~A"
+ var (substitute-bindings solution var))))
+ (princ ";"))
- Return all possible solutions as a list of binding-lists.
+(defun clean-variables (variables solution)
+ (mapcar #'(lambda (var)
+ (cons var (substitute-bindings solution var)))
+ variables))
- "
- ;; We look up all the possible clauses for the goal and try proving
- ;; each individually. Each one will give us back a list of possible
- ;; solutions.
- ;;
- ;; Then we concatenate the results to return all the possible
- ;; solutions.
- (mapcan #'prove-single-clause (get-clauses (predicate goal)))))
- (cond
- ;; If something failed further up the pipeline, bail here.
- ((eq bindings fail) fail)
+(defun show-solutions (variables solutions)
+ (if (null solutions)
+ (format t "~&No.")
+ (mapc (curry #'show-variables variables)
+ solutions))
+ (values))
+
+(defun clean-solutions (variables solutions)
+ (mapcar (curry #'clean-variables variables)
+ solutions))
- ;; If there's nothing to prove, it's vacuously true. Return a list of the
- ;; bindings as the result.
- ((null goals) (list bindings))
+(defun top-level-prove (goals)
+ (show-solutions
+ (variables-in goals)
+ (prove-all goals no-bindings)))
- ;; Otherwise we try to prove the first thing in the list. This gives us
- ;; back a list of possible bindings we could use.
- ;;
- ;; For each possible solution to the head, we try using it to prove the
- ;; rest of the goals and concatenate all the results. Failed attempts are
- ;; represented as FAIL which is nil, so will collapse in the concatenation.
- (t (mapcan #'(lambda (possible-solution)
- (prove-all (rest goals) possible-solution))
- (prove (first goals) bindings))))))
+(defun top-level-find (goals)
+ (clean-solutions
+ (variables-in goals)
+ (prove-all goals no-bindings)))
+(defmacro query (&rest goals)
+ `(top-level-prove ',goals))
+
+(defmacro find-all (&rest goals)
+ `(top-level-find ',goals))
+
--- a/test/paip.lisp Thu Mar 10 15:14:48 2016 +0000
+++ b/test/paip.lisp Thu Mar 10 18:22:56 2016 +0000
@@ -17,6 +17,24 @@
`(is (eql bones.paip:fail (unify ',x ',y))))
+(defmacro with-db (rules &rest body)
+ `(progn
+ (clear-db)
+ ,@(mapcar #'(lambda (rule) `(rule ,@rule))
+ rules)
+ ,@body))
+
+
+(defmacro proves (query)
+ `(is-true (find-all ,query)))
+
+(defmacro not-proves (query)
+ `(is-false (find-all ,query)))
+
+(defmacro proves-with (query results)
+ `(is (set-equal ',results (find-all ,query)
+ :test #'alist-equal)))
+
;;;; Unification
(test constant-unification
(unifies 1 1 no-bindings)
@@ -30,33 +48,81 @@
(not-unifies () (a)))
(test variable-unification
- (unifies :x 1 ((:x . 1)))
- (unifies :x a ((:x . a)))
- (unifies :x :y ((:x . :y)))
- (unifies (:x (f :x)) (2 (f 2)) ((:x . 2)))
- (unifies (likes sally :thing)
- (likes :person cats)
- ((:thing . cats)
- (:person . sally)))
- (unifies (:x + :y)
+ (unifies ?x 1 ((?x . 1)))
+ (unifies ?x a ((?x . a)))
+ (unifies ?x ?y ((?x . ?y)))
+ (unifies (?x (f ?x)) (2 (f 2)) ((?x . 2)))
+ (unifies (likes sally ?thing)
+ (likes ?person cats)
+ ((?thing . cats)
+ (?person . sally)))
+ (unifies (?x + ?y)
(10 + (1 + 2))
- ((:x . 10)
- (:y . (1 + 2))))
- (unifies (:x + (:y + :z))
+ ((?x . 10)
+ (?y . (1 + 2))))
+ (unifies (?x + (?y + ?z))
(10 + (1 + 2))
- ((:x . 10)
- (:y . 1)
- (:z . 2)))
- (not-unifies (:x :x) (1 2))
- (not-unifies (:x :y :x) (1 1 3)))
+ ((?x . 10)
+ (?y . 1)
+ (?z . 2)))
+ (not-unifies (?x ?x) (1 2))
+ (not-unifies (?x ?y ?x) (1 1 3)))
(test occurs-unification
- (not-unifies :x (f :x))
- (not-unifies :x (f (:x 1)))
- (not-unifies :x (:x :x))
- (not-unifies :x (:x :y))
+ (not-unifies ?x (f ?x))
+ (not-unifies ?x (f (?x 1)))
+ (not-unifies ?x (?x ?x))
+ (not-unifies ?x (?x ?y))
(let ((*check-occurs* nil))
- (unifies :x (f :x) ((:x . (f :x))))
- (unifies :x (f (:x 1)) ((:x . (f (:x 1)))))
- (unifies :x (:x :x) ((:x . (:x :x))))
- (unifies :x (:x :y) ((:x . (:x :y))))))
+ (unifies ?x (f ?x) ((?x . (f ?x))))
+ (unifies ?x (f (?x 1)) ((?x . (f (?x 1)))))
+ (unifies ?x (?x ?x) ((?x . (?x ?x))))
+ (unifies ?x (?x ?y) ((?x . (?x ?y))))))
+
+
+;;;; Basic Proving
+(test prove-facts
+ (with-db (((likes kim cats))
+ ((likes tom cats)))
+ (proves (likes kim cats))
+ (proves (likes tom cats))
+ (not-proves (likes kim tom))
+ (not-proves (likes kim))))
+
+(test prove-rules-simple
+ (with-db (((likes kim cats))
+ ((likes sally ?x) (likes ?x cats)))
+ (proves (likes sally kim))
+ (not-proves (likes sally sally))))
+
+(test prove-member
+ (with-db (((member ?x (?x . ?tail)))
+ ((member ?x (?y . ?tail)) (member ?x ?tail)))
+ (proves (member 1 (1 2)))
+ (proves (member 2 (1 2)))
+ (proves (member (x) (1 (x) 2)))
+ (not-proves (member 1 ()))
+ (not-proves (member ?x ()))
+ (not-proves (member 1 (a b c)))
+ (proves-with (member ?x (1 2 3))
+ (((?x . 1))
+ ((?x . 2))
+ ((?x . 3))))
+ (proves-with (member ?x (1 1 1))
+ (((?x . 1))))
+ (proves-with (member (?x ?y) ((a b) (c d) 1))
+ (((?x . a) (?y . b))
+ ((?x . c) (?y . d))))))
+
+(test prove-last
+ (with-db (((last ?x (?x)))
+ ((last ?x (?y . ?tail)) (last ?x ?tail)))
+ (proves (last 1 (1)))
+ (proves (last 2 (1 2)))
+ (not-proves (last 1 ()))
+ (not-proves (last 1 ((1))))
+ (not-proves (last 1 (1 2)))
+ (proves-with (last ?x (1 2 3))
+ (((?x . 3))))
+ (proves-with (last ?x (1 (2 3)))
+ (((?x . (2 3)))))))