Use a queues instead of lists for the logic frame pending predicates
I wonder if this is ACTUALLY faster, since often there will probably only be
a couple of entries in a particular predicate's list? But then again there are
some HUGE predicates (e.g. successor relations), so it'll benefit us there.
Either way, conceptually the thing should be FIFO, so as long as using queues
doesn't COST us performance I'm happy.
author |
Steve Losh <steve@stevelosh.com> |
date |
Tue, 05 Jul 2016 23:37:14 +0000 |
parents |
d8d6647dd9fb |
children |
5593ae4bcb5c |
(in-package #:bones.paip)
;;;; Types
(deftype logic-variable ()
'symbol)
(deftype binding ()
'(cons logic-variable t))
(deftype binding-list ()
'(trivial-types:association-list keyword t))
;;;; Constants
(define-constant fail nil
:documentation "Failure to unify")
(define-constant no-bindings '((:bones-empty-bindings . t))
:test 'equal
:documentation "A succesful unification, with no bindings.")
(defparameter *check-occurs* t
"Whether to perform an occurs check.")
;;;; Unification
(defun* variable-p (term)
(:returns boolean)
"Return whether the given term is a logic variable."
(and (symbolp term)
(equal (char (symbol-name term) 0)
#\?)))
(defun* get-binding ((variable logic-variable)
(bindings binding-list))
(:returns (or binding null))
"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."
(car binding))
(defun* binding-value ((binding binding))
"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."
(binding-value (get-binding variable bindings)))
(defun* extend-bindings ((variable logic-variable)
(value t)
(bindings binding-list))
(:returns binding-list)
"Add a binding (var . val) to the binding list (nondestructively)."
(cons (cons variable value)
(if (and (equal bindings no-bindings))
nil
bindings)))
(defun* check-occurs ((variable logic-variable)
(target t)
(bindings binding-list))
(:returns boolean)
"Check whether the variable occurs somewhere in the target.
Takes the bindings into account. This is expensive.
"
(cond
;; If the target is this variable, then yep.
((eql variable target) t)
;; The empty list doesn't contain anything.
((null target) nil)
;; The the target is a (different) variable that has a binding, we need to
;; check if the variable occurs in its bindings.
((and (variable-p target)
(get-binding target bindings))
(check-occurs variable (lookup target bindings) bindings))
;; If the target is a list, check if any of the elements contain the variable.
((listp target)
(or (check-occurs variable (first target) bindings)
(check-occurs variable (rest target) bindings)))
;; Otherwise we're safe.
(t nil)))
(defun unify (x y &optional (bindings no-bindings))
"Unify the two terms and return bindings necessary to do so (or FAIL)."
(flet ((unify-variable (variable target bindings)
(cond
;; If we've already got a binding for this variable, we can try to
;; unify its value with the target.
((get-binding variable bindings)
(unify (lookup variable bindings) target bindings))
;; If the target is ALSO a variable, and it has a binding, then we
;; can unify this variable with the target's value.
((and (variable-p target) (get-binding target bindings))
(unify variable (lookup target bindings) bindings))
;; If this variable occurs in the target (including in something
;; in its bindings) and we're checking occurrence, bail.
((and *check-occurs* (check-occurs variable target bindings))
fail)
;; Otherwise we can just bind this variable to the target.
(t (extend-bindings variable target bindings)))))
(cond
;; Pass failures through.
((eq bindings fail) fail)
;; Trying to unify two identical objects (constants or variables) can just
;; return the bindings as-is.
;;
;; ex: (unify :y :y) or (unify 'foo 'foo)
((eql x y) bindings)
;; Unifying a variable with something.
((variable-p x) (unify-variable x y bindings))
((variable-p y) (unify-variable y x bindings))
;; Unifying a non-variable with nil should fail, except for nil itself.
;; But that was handled with (eql x y).
((or (null x) (null y)) fail)
;; Unifying non-empty compound terms such as
;; (likes :x cats) with (likes sally :y).
((and (listp x) (listp y))
(unify (rest x) (rest y) ; Unify the tails with the bindings gotten from...
(unify (first x) (first y) bindings))) ; unifying the heads.
;; Otherwise we're looking at different constants, or a constant and a
;; compound term, so just give up.
(t fail))))
;;;; Substitution
(defun* substitute-bindings ((bindings binding-list)
(form t))
"Substitute (recursively) the bindings into the given form."
(cond ((eq bindings fail) fail)
((eq bindings no-bindings) form)
((and (variable-p form) (get-binding form bindings))
(substitute-bindings bindings
(lookup form bindings)))
((atom form) form)
(t (mapcar (curry #'substitute-bindings bindings) form))))
(defun unifier (x y)
"Unify x with y and substitute in the bindings to get the result."
(substitute-bindings (unify x y) x))
;;;; Database
;;; A clause is an assertion in the database. There are two types.
;;;
;;; A fact is the "base" clause:
;;;
;;; (likes kim cats)
;;;
;;; A rule is a way to deduce new facts from existing information:
;;;
;;; ((likes sally :x)
;;; (likes :x cats))
;;;
;;; Clauses are stored as lists. The head is the first item in the list, and
;;; it's "the thing you're trying to prove". You prove it by proving all the
;;; things in the tail of the list. For facts the tail is empty, so they are
;;; trivially proven.
;;;
;;; A predicate is the named head of a part of a clause. In `(likes sally :x)`
;;; the predicate is `likes`.
;;;
;;; Predicates are stored in the plists of their symbols, which is a little
;;; insane, but it's how Norvig did it so I'll do it like this for now.
(defvar *db-predicates* nil
"A list of all the predicates in the database.")
(defconstant clause-key 'bones.paip-clauses
"The key to use in the symbol plist for the clauses.")
(defun clause-head (clause)
(first clause))
(defun clause-body (clause)
(rest clause))
(defun get-clauses (pred)
(get pred clause-key))
(defun set-clauses (pred clauses)
(setf (get pred clause-key) clauses))
(defun predicate (relation)
(first relation))
(defun wildcard-variable-p (form)
(and (symbolp form) (string= (symbol-name form) "?")))
(defun replace-wildcard-variables (form)
(cond
((wildcard-variable-p form) (gensym "?"))
((atom form) form)
((consp form) (cons (replace-wildcard-variables (car form))
(replace-wildcard-variables (cdr form))))
(t (mapcar #'replace-wildcard-variables form))))
(defun add-clause (clause)
(let ((pred (predicate (clause-head clause))))
(assert (and (symbolp pred)
(not (variable-p pred))))
(pushnew pred *db-predicates*)
(set-clauses pred
(nconc (get-clauses pred) (list clause)))
pred))
(defun add-rule (clause)
(add-clause (replace-wildcard-variables clause)))
(defmacro rule (&rest clause)
`(add-rule ',clause))
(defun add-fact (body)
(add-clause (list (replace-wildcard-variables body))))
(defmacro fact (&rest body)
`(add-fact ',body))
(defun clear-predicate (predicate)
(setf (get predicate clause-key) nil))
(defun clear-db ()
(mapc #'clear-predicate *db-predicates*))
;;;; Proving
(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 variable))))
(variables-in form))
form))
(defun prove-clause (goal bindings other-goals clause)
(let ((new-clause (rename-variables clause)))
(prove-all (append (clause-body new-clause) other-goals)
(unify goal (clause-head new-clause) bindings))))
(defun prove (goal bindings other-goals)
"Return a list of possible solutions to the given goal."
(let ((clauses (get-clauses (predicate goal))))
(if (listp clauses)
(some (curry #'prove-clause goal bindings other-goals) clauses)
(funcall clauses (rest goal) bindings other-goals))))
(defun prove-all (goals bindings)
"Return a solution to the conjunction of goals."
(cond
;; If something failed further up the pipeline, bail here.
((eq bindings fail) fail)
;; If there's nothing to prove, it's vacuously true. Return the bindings as
;; the result.
((null goals) bindings)
(t (prove (first goals) bindings (rest goals)))))
;;;; Cleaning Solutions
(defun clean-variables (variables solution)
(mapcar #'(lambda (var)
(cons var (substitute-bindings solution var)))
variables))
;;;; Querying Interface
(defun continue-never ()
nil)
(defun continue-always ()
t)
(defun continue-ask ()
(case (read-char)
(#\; t)
(#\. nil)
(#\newline (continue-ask))
(otherwise
(format t " Type ; to see more or . to stop")
(continue-ask))))
(defun show-prolog-vars (variables bindings other-goals continue-p)
(if (null variables)
(format t "~&Yes")
(dolist (var variables)
(format t "~&~A = ~A"
var (substitute-bindings bindings var))))
(finish-output)
(if (funcall continue-p)
fail
(prove-all other-goals bindings)))
(defun show-prolog-vars-ask (variables bindings other-goals)
(show-prolog-vars variables bindings other-goals #'continue-ask))
(defun show-prolog-vars-all (variables bindings other-goals)
(show-prolog-vars variables bindings other-goals #'continue-always))
(defun show-prolog-vars-one (variables bindings other-goals)
(show-prolog-vars variables bindings other-goals #'continue-never))
(setf (get 'show-prolog-vars-ask clause-key) 'show-prolog-vars-ask)
(setf (get 'show-prolog-vars-all clause-key) 'show-prolog-vars-all)
(setf (get 'show-prolog-vars-one clause-key) 'show-prolog-vars-one)
(defun top-level-query (goals primitive)
(prove-all `(,@(replace-wildcard-variables goals)
(,primitive
,@(remove-if #'wildcard-variable-p (variables-in goals))))
no-bindings)
(format t "~&No."))
(defmacro query (&rest goals)
"Perform the query interactively."
`(top-level-query ',goals 'show-prolog-vars-ask))
(defmacro query-all (&rest goals)
"Perform the query and automatically show all results."
`(top-level-query ',goals 'show-prolog-vars-all))
(defmacro query-one (&rest goals)
"Perform the query and just show the first result."
`(top-level-query ',goals 'show-prolog-vars-one))
;;;; Finding Interface
(defparameter *results* nil)
(defun return-boolean (variables bindings other-goals)
(declare (ignore variables))
(setf *results* t)
(prove-all other-goals bindings))
(defun return-one-result (variables bindings other-goals)
(setf *results* (clean-variables variables bindings))
(prove-all other-goals bindings))
(defun return-all-results (variables bindings other-goals)
(declare (ignore other-goals))
(push (clean-variables variables bindings) *results*)
fail)
(setf (get 'return-one-result clause-key) 'return-one-result)
(setf (get 'return-all-results clause-key) 'return-all-results)
(setf (get 'return-boolean clause-key) 'return-boolean)
(defun top-level-find (goals primitive)
(let ((*results* (list)))
(prove-all `(,@(replace-wildcard-variables goals)
(,primitive
,@(remove-if #'wildcard-variable-p (variables-in goals))))
no-bindings)
*results*))
(defun return-one-for (goals)
(top-level-find goals 'return-one-result))
(defun return-all-for (goals)
(top-level-find goals 'return-all-results))
(defmacro return-one (&rest goals)
`(top-level-find ',goals 'return-one-result))
(defun raw-return-one (&rest goals)
(top-level-find goals 'return-one-result))
(defmacro return-all (&rest goals)
`(top-level-find ',goals 'return-all-results))
(defun raw-return-all (&rest goals)
(top-level-find goals 'return-all-results))
(defmacro provable-p (&rest goals)
`(top-level-find ',goals 'return-boolean))
(defun raw-provable-p (&rest goals)
(top-level-find goals 'return-boolean))