;;;; -*- Mode: LISP; Syntax: Common-Lisp; Base: 10 -*- ;;;; --------------------------------------------------------------------- ;;;; File name: chainer.lsp ;;;; System: FIRE ;;;; Author: Praveen Paritosh ;;;; Created: October 23, 2001 21:05:00 ;;;; Purpose: Creates chainers for partitioned backchaining ;;;; --------------------------------------------------------------------- ;;;; Modified: Monday, May 31, 2004 at 17:38:47 by Kenneth Forbus ;;;; --------------------------------------------------------------------- (in-package :fire) (defvar *bc-chainer* nil "Temporary for storing chainer being loaded.") ;;; FIRE distinguishes between "reflexive" and "reflective" backchaining. ;;; "reflexive" backchaining is tightly resource limited, and is intended for ;;; those simple pieces of "glue" logic that are so important in handling the ;;; non-obvious. Reflexive backchaining is intended to gain efficiency at the cost ;;; of reduced coverage. ;;; "reflective" backchaining is when backchaining is used as part of the SOLVE ;;; mechanism, which uses an agenda and an AND/OR graph to implement a suggestions ;;; architecture, which operates at a higher level of processing than ;;; reflexive operations like limited backchaining and using reasoning sources. ;;; ;;; The goal of this distinction is to avoid the wandering off that tends to happen ;;; in large reasoning systems. In addition to the usual max depth/max nodes ;;; resource bounds (see backward.lsp), another way that FIRE restricts backchaining ;;; is to limit it to within a chainer. A chainer is a set of DNF clauses, ;;; identified as a subset in the KB, intended to handle the reflexive backchaining ;;; for a specific class of tasks or domain of interest. ;;; ;;; Generally there will be a large number of chainers in a KB, based on the tasks ;;; it is being used for and the KB contents; thus chainers provide a means of ;;; factoring the search space. Since chainers are constructed off-line and ;;; cached on disk, this also speeds up reasoning sessions, since the work of ;;; figuring out what is relevant and converting it to clausal form has already ;;; been carried out. ;;; ;;; A chainer is associated with a KB. The term by which a chainer is refered to ;;; must be a member of the collection Chainer. The relation chainerIncludes ;;; indicates which axioms in the KB belong to a particular chainer. Chainer ;;; membership is declarative so that FIRE-based systems can modify their own ;;; chainers, and hence learn to better control their reasoning over time. ;;; FIRE application developers can of course hard-wire their own chainers by using ;;; the same mechanisms. ;;; Things to do: ;;; 1. Support incremental updates during development. Like KB updates, ensuring that the changes made ;;; in a specific KB or image get saved in a way that can be propagated and reconstructed ;;; (It all must end up in a flat file somewhere along the line, or the knowledge will be ;;; lost when a cosmic ray flips a bit on a hard drive or a spec of dust causes a bit on ;;; a CD-ROM to be unreadable.) ;;; 3. Support autoload of chainers. Given a term that specifies the chainer, we should ;;; be able to automatically load an chainer for a KB when a reasoner first asks for it. Good ;;; way to save space when running on ancient (read: 2 year old) hardware. ;;;============================================================================== ;;; Three procedures are provided to create chainers. ;;; ;;; CREATE-CHAINER is used to gather axioms that take the form of implications, ;;; filtered by user-specifiable crieria. ;;; The :include-test keyword argument provides control over what axioms are ;;; included in a chainer. The default creates one massive chainer, which ;;; generally will be a pain to search. FIRE application designers will need ;;; to pick carefully what chainers they create to support their systems. ;;; ;;; Caveat: Certain things, like quantifiers in statements, are not currently ;;; supported. The procedure axiom-backchainable? should be incorporated ;;; in developer-authored tests to filter out those things that the system ;;; cannot handle, in addition to any application-specific filter criterion. ;;; ;;; The :predicate-test keyword argument allows a procedure to be specified ;;; that limits what predicates will be backchained over. Such procedures ;;; should use pragmas stored in the KB, as well as any other analyses ;;; available to avoid fruitless search. The default, predicate-backchainable? ;;; only eliminates relations that are NATs (e.g., created using KAPPA). ;;; ;;; CREATE-CHAINER-FROM-AXIOMS takes a list of axioms, assuming that they ;;; have already been filtered by some external processing, and creates a ;;; chainer from them. N.B. it is assumed that these axoims are actually ;;; in the KB. No checks are made about this, since users of FIRE ;;; applications will never be fooling around with these facilities! ;;; CREATE-CHAINER-FROM-PREDICATES takes a list of predicates and a depth ;;; argument (which defaults to :exhaustive). From a given list L of ;;; predicates, create a chainer whose rules R are defined recursively: ;;; ;;; - If r is a rule the predicate of whose conclusion is in L, then r is in R ;;; - If r is in R, if p is a predicate of an antecedent of r, and if s is a rule ;;; the predicate of the conclusion of which is p, then s is in R. ;;; ;;; In other words, given a list L of predicates, this process constructs a chainer ;;; which contains all those rules which would allow conclusions to be made ;;; involving all and only the predicates of L. If depth is set to exhaustive, this ;;; recursion terminates when one doesnt find any more new axioms; but since that ;;; could lead to huge indices, one can limit how deep we recurse. ;;; ;;; This would be useful for constructing "on-the-fly" indices which contain only ;;; those rules needed for making conclusions involving known predicates. For ;;; example, I might be interested in drawing conclusions about the predicate ;;; translationalConstraint; I would give the singleton list ;;; '(translationalConstraint) to this procedure, and it would construct an chainer ;;; which contains all those rules which would allow me to conclude ;;; translationalConstraint. PREDICATE-NOT-TO-BE-INDEXED? allows us to stop ;;; this process from including predicates like isa, and making the chainer explode. (defun create-chainer (title &key (include-test 'axiom-backchainable?) (predicate-test 'predicate-backchainable?) (term nil) (kb *kb*)) (unless term (setq term (make-CYC-term title))) ; maximize backward compatibility (let* ((axioms (get-all-axioms-from-kb kb)) (chainer (make-instance 'chainer :title title :term term :kb kb))) (dolist (axiom axioms) (when (funcall include-test axiom) (process-axiom-for-backchaining axiom chainer predicate-test))) (add-chainer-to-kb chainer kb))) ;;; Added by Dan Halstead 7/18/03: ;;; This will create a chainer from all of the rule macros as well as the explicit ;;; axioms in the KB (unless one specifies :all-macros or :all-axioms nil). (defun create-chainer-from-whole-kb (title &key (include-test 'axiom-backchainable?) (predicate-test 'predicate-backchainable?) (term nil) (all-macros t) (all-axioms t) (kb *kb*) verbose) (when verbose (format t "Creating to store all axioms and macros.~%" title)) (unless term (setq term (make-CYC-term title))) ; maximize backward compatibility (let* ((axioms (when all-axioms (when verbose (format t "Retrieving all axioms from KB.~%")) (get-all-axioms-from-kb kb))) (macros (when all-macros (get-all-macros-from-kb :kb kb :compile t :verbose verbose))) (axiom-list (append axioms (remove-if-not #'axiom-p macros))) (chainer (make-instance 'chainer :title title :term term :kb kb))) (when verbose (format t "Adding all clauses to chainer.~%")) (dolist (axiom axiom-list) (when (funcall include-test axiom) (process-axiom-for-backchaining axiom chainer predicate-test))) (add-chainer-to-kb chainer kb))) (defvar *rmp-expansions* nil "For debugging") (defun create-chainer-from-macros (title macros &key (term nil) (kb *kb*)) (unless term (setq term (make-CYC-term title))) (let ((chainer (make-instance 'chainer :title title :term term :kb kb))) (dolist (macro macros) (let ((axiom (expand macro))) (when (axiom-backchainable? axiom) (process-axiom-for-backchaining axiom chainer 'predicate-backchainable?) ;; Keep track of where clauses were expanded from, for debugging: ;;(push (list (clause-counter chainer) macro) *rmp-expansions*) ))) (add-chainer-to-kb chainer kb))) (defun create-chainer-from-axioms (title axioms &key (term nil) (kb *kb*)) (unless term (setq term (make-CYC-term title))) (let ((chainer (make-instance 'chainer :title title :term term :kb kb))) (dolist (axiom axioms) (process-axiom-for-backchaining axiom chainer 'always-true)) (add-chainer-to-kb chainer kb))) ;;; Recursive chainer construction from a list of predicates (defun create-chainer-from-predicates (title predlist &key (depth :exhaustive) (term nil) (kb *kb*) (all-axioms nil)) (unless all-axioms (setq all-axioms (get-all-axioms-from-kb kb))) (let ((filtered-axioms (get-axioms-recursively-from-predicates predlist :depth depth :all-axioms all-axioms))) (create-chainer-from-axioms title filtered-axioms :term term :kb kb))) (defun get-axioms-recursively-from-predicates (predlist &key (depth :exhaustive) (axioms nil) (all-axioms nil)) (when (or (equal depth 0) (null predlist)) (return-from get-axioms-recursively-from-predicates axioms)) (dolist (pred predlist) (dolist (ax (get-axioms-for-pred pred all-axioms)) (pushnew ax axioms))) (if (not (equal depth :exhaustive)) (decf depth)) (let ((nextpreds nil)) (dolist (ax axioms) (let ((ante-preds (predicates-in-antecedent ax))) (dolist (ap ante-preds) (if (and (not (member ap predlist)) (not (predicate-not-to-be-indexed? ap))) (pushnew ap nextpreds))))) (get-axioms-recursively-from-predicates nextpreds :depth depth :axioms axioms :all-axioms all-axioms))) ;;; Considering these predicates, especially in recursive chainer construction, ;;; might lead to an explosion, and all axioms getting sucked in. (defun predicate-not-to-be-indexed? (pred) (and (equal pred 'data::isa))) (defun get-axioms-for-pred (pred all-axioms) "Returns a list of axioms that have pred in the consequent" (let ((pred-axioms nil)) (dolist (axiom all-axioms) (if (member pred (predicates-in-consequent axiom)) (push axiom pred-axioms))) (values pred-axioms))) (defun get-all-axioms-from-kb (&optional (kb *kb*)) (mp:with-process-lock ((lock kb)) (union (dbex:extension-of-predicate 'data::implies 2) (dbex:extension-of-predicate 'data::equiv 2)))) ;;; =========================================================================== ;;; Chainer retrieval ;;; ;;; We assume that once a chainer has been retrieved that it isn't stale. ;;; But before we load a cached version, we check to see if it is still ;;; current. If not, we rebuild it. (defvar *autocache-chainer-files?* t) ;; For some apps we may not want to do this (defun retrieve-chainer (chainer-term parent) ;;; The chainers slot on a kb or reasoner is just a flat list. (find chainer-term (chainers parent) :key 'term :test 'equal)) (defmethod get-chainer ((chainer-term t) (parent knowledge-base)) (let ((chainer (retrieve-chainer chainer-term parent))) (cond ((chainer? chainer) chainer) (t (cond ((chainer-cached-in-file? chainer-term parent) (cond ((dumped-chainer-stale? chainer-term) (create-chainer-from-kb chainer-term :kb parent) (when *autocache-chainer-files?* (dump-chainer-file chainer-term parent))) (t (load-chainer-file chainer-term parent)))) (t (create-chainer-from-kb chainer-term :kb parent))) (retrieve-chainer chainer-term parent))))) (defmethod get-chainer ((chainer-term t) (parent reasoner)) (let ((chainer (retrieve-chainer chainer-term parent))) (if (chainer? chainer) chainer (let ((kb-chainer (get-chainer chainer-term (kb parent)))) ; load it in if necessary (if (chainer? kb-chainer) (add-chainer-to-reasoner kb-chainer parent) ))))) (defun add-chainer-to-kb (chainer kb) (let ((old-chainer (retrieve-chainer (term chainer) kb))) (when old-chainer (setf (chainers kb) (delete old-chainer (chainers kb)))) (push chainer (chainers kb)) chainer)) ;;; ADD-chainer-TO-REASONER adds a chainer to a reasoner. This makes it available ;;; for queries from that reasoner. (defun add-chainer-to-reasoner (chainer reasoner) (when (chainer? chainer) (pushnew chainer (chainers reasoner) :test 'equal :key 'term))) (defun add-all-chainers-to-reasoner (&optional (reasoner *reasoner*) (kb *kb*)) (dolist (index (chainers kb)) (add-chainer-to-reasoner index reasoner))) (defun clear-reasoner-chainers (&optional (reasoner *reasoner*)) (setf (chainers reasoner) nil)) (defun clear-kb-chainers (&optional (kb *kb*)) (setf (chainers kb) nil)) (defun create-chainer-from-kb (chainer-term &key (kb *kb*)) (let* ((contents (retrieve `(data::chainerContains ,chainer-term ?axiom) :response '?axiom)) (chainer (create-chainer-from-axioms (format nil "~A:~A ~A" chainer-term (concise-date-string) (concise-time-string)) contents :term chainer-term :kb kb))) (dump-chainer-file chainer-term kb) chainer)) (defun dumped-chainer-stale? (chainer &key (kb *kb*)) (let ((dumped-at (retrieve-latest-ut-assertion 'data::chainerDumpedAt chainer :kb kb)) (updated-at (retrieve-latest-ut-assertion 'data::chainerUpdatedAt chainer :kb kb))) (time-term-later? (third updated-at) (third dumped-at)))) ;;;========================================================================== ;;; Clause processing ;;; (defun always-true (x) (declare (ignore x)) t) (defun process-axiom-for-backchaining (axiom chainer predicate-test) ;;(format t "~%Axiom = ~s" axiom) (let ((clauses (canonicalize-axiom axiom))) (dolist (terms clauses) (let ((clause (make-instance 'clause :id (incf (clause-counter chainer)) :chainer chainer :terms terms :variables (formula-variables terms) :axiom axiom))) (setf (gethash (id clause) (clauses chainer)) clause) ;;(format t "~%Canonicalized clause = ~s" terms) ;; ** debugging (dolist (term-plus-orderings (derive-feasible-solution-orderings-for-terms terms)) ;;(format t "~% Term-plus-orderings = ~s" term-plus-orderings) ;; ** debugging (process-term-for-backchaining (car term-plus-orderings) clause (cdr term-plus-orderings) chainer predicate-test)))))) (defun process-term-for-backchaining (term clause orderings chainer predicate-test) ;; Recall terms are ( . ) ;; orderings are ( . ) (cond ((quantified-term? (car term)) (process-quantifier-for-backchaining (car term) (cdr term) clause predicate-test)) (t (let* ((predicate (caar term)) (polarity (cdr term))) (when (and (funcall predicate-test predicate) orderings ;; If no orderings, it won't work (not (outsourced-predicate? predicate))) ;; Heuristic (let ((entry (gethash predicate (table chainer)))) (unless entry (setf (gethash predicate (table chainer)) (setq entry (cons nil nil)))) ;; each entry is a clause id plus the ordering to use ;; for going through that clause. (ecase polarity (:true (push (list clause term orderings) (car entry))) (:false (push (list clause term orderings) (cdr entry)))))))))) ;;; Currently a no-op: (defun process-quantifier-for-backchaining (quantified-term polarity clause predicate-test) (let ((expansion (expansion quantified-term))) (dolist (terms expansion) ;;(format t "~%Expanded clause = ~s" terms) (dolist (term-plus-orderings (derive-feasible-solution-orderings-for-terms terms)) ;;(format t "~% Term-plus-orderings = ~s" term-plus-orderings) (when (and (consp term-plus-orderings) (quantified-term? (caar term-plus-orderings))) (process-quantifier-for-backchaining (caar term-plus-orderings) polarity clause predicate-test)))))) (defun lookup-clause (id chainer) (gethash id (clauses chainer))) ;; internals ; Used to determine whether a compiled macro is worth adding to the chainer. (defun axiom-p (rule) (or (eql (car rule) 'data::implies) (eql (car rule) 'data::equiv))) (defun applicable-clauses (operator polarity index) ;; Returns list of pairs, ( . ) (let ((entries (gethash operator (table index)))) (ecase polarity (:true (car entries)) (:false (cdr entries))))) (defun axiom-backchainable? (rule) (let ((antecedent (antecedent rule)) (consequent (consequent rule))) (unless (or (variable? consequent) (variable? antecedent) (not (listp consequent)) ;; Added (TRH) (not (listp antecedent))) (let ((antecedent-operator (formula-operator antecedent)) (consequent-operator (formula-operator consequent))) (unless (or (variable? antecedent-operator) (variable? consequent-operator)) (not (or (existential-formula? consequent) (skip-backchaining? (get-pragma consequent-operator))))))))) ;; N.B. Start prolific, but as we refine our control vocabulary, enforce it here. (defun predicate-backchainable? (predicate) (and (symbolp predicate) (not (retrieve `(data::backchainForbidden ,predicate) :number 1)))) (defun predicates-in-axiom (axiom) ;; Kind of overkill -- could be done more simply by tree-walking with recognition ;; of quantifiers. Fix later if needed. The functions predicate-in-antecedent, ;; and predicate-in-consequent, defined below use this, so might need to change ;; them if this is changed. (remove-duplicates (mapcan #'(lambda (terms) (mapcar 'caar terms)) (canonicalize-axiom axiom)))) (defun predicates-in-antecedent (axiom) (predicates-in-axiom (second axiom))) (defun predicates-in-consequent (axiom) (predicates-in-axiom (third axiom))) (defun generate-axiom-list-test (list-of-predicates) ;; For making tightly constrained backchainers (lambda (axiom) (and (axiom-backchainable? axiom) (intersection (predicates-in-axiom axiom) list-of-predicates)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Some debugging & support utilities (defun chainer-report (index fname &optional (show-details? t)) (with-open-file (fout fname :direction :output) (show-chainer index show-details? fout))) (defun show-chainer (index &optional (show-details? nil) (stream *standard-output*)) (format stream "~%Clause index ~A of KB ~A." (title index) (name (kb index))) (multiple-value-bind (n-entries max min mean) (calculate-chainer-table-stats index) (format stream "~% ~D clauses, ~D index entries, max = ~d, min = ~d, mean = ~D." (n-clauses index) n-entries max min mean)) (show-clauses-from-chainer index show-details? stream) (when show-details? (show-query-orderings-for-chainer index stream))) (defun calculate-chainer-table-stats (index) (let ((max -1000) (min 1.0e6) (sum 0) (count 0)) (maphash #'(lambda (key value) (declare (ignore key)) ;; Calculate pos/neg stats seperately later? (let ((size (+ (length (car value)) (length (cdr value))))) (if (> size max) (setq max size)) (if (< size min) (setq min size)) (incf count) (incf sum size))) (table index)) (if (equal count 0) (values 0 0 0 0) ;; avoid divide by zero. (values count max min (/ (float sum) (float count)))))) (defun show-clauses-from-chainer (index &optional (show-details? nil) (stream *standard-output*)) (dotimes (id (n-clauses index)) (show-clause (lookup-clause id index) show-details? stream))) (defun show-clause (clause &optional (show-details? t) (stream *standard-output*)) (format stream "~%Clause ~D: ~A." (id clause) (variables clause)) (pprint (terms clause) stream) (when show-details? (pprint (axiom clause) stream))) (defun map-chainer-clauses (proc index) (dotimes (id (n-clauses index) index) (funcall proc (lookup-clause id index)))) (defun clauses-identical? (c1 c2) (and (= (id c1) (id c2)) (equal (variables c1) (variables c2)) (equal (axiom c1) (axiom c2)) (equal (terms c1) (terms c2)))) (defun convert-to-ci-comps (entries) (mapcar #'(lambda (pair) (cons (id (car pair)) (cdr pair))) entries)) ;;;; ******* This is probably out of date -- doesn't deal with ;;;; ******* orderings and signatures (defun verify-chainers-identical (i1 i2) (and (map-chainer-clauses #'(lambda (c1) (let ((other (lookup-clause (id c1) i2))) (if (clause? other) (unless (clauses-identical? c1 other) (return-from verify-chainers-identical (values nil (list c1 other)))) (return-from verify-chainers-identical (values nil (list c1 other)))))) i1) ;; Should do both directions (let ((result t)) (maphash #'(lambda (key value) (let ((other (gethash key (table i2)))) (unless (and (equal (convert-to-ci-comps (car value)) (convert-to-ci-comps (car other))) (equal (convert-to-ci-comps (cdr value)) (convert-to-ci-comps (cdr other)))) (return-from verify-chainers-identical (values nil (list key value other)))))) (table i1)) result))) (defun show-hash-table (table &optional (stream *standard-output*)) (maphash #'(lambda (k v) (format stream "~A: ~A~%" k v)) table)) (defun show-query-orderings-for-chainer (chainer stream) (format stream "~%Query orderings:") (maphash #'(lambda (k v) ;; v = (( ... (clause pattern ordering+sig)...) ) (format stream "~% Predicate ~A:" k) (when (car v) (format stream "~% Positive occurrences:") (dolist (entry (car v)) (format stream "~% ~A in Clause ~D:" (cadr entry) (id (car entry))) (dolist (oentry (third entry)) (format stream "~% Ordering: ~A." (car oentry)) (format stream "~% Signature: ~A." (cdr oentry))))) (when (cdr v) (format stream "~% Negative occurrences:") (dolist (entry (car v)) (format stream "~% ~A in Clause ~D:" (cadr entry) (id (car entry))) (dolist (oentry (third entry)) (format stream "~% Ordering: ~A." (car oentry)) (format stream "~% Signature: ~A." (cdr oentry)))))) (table chainer))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;; Tracing (defun trace-chainer-construction () (trace fire::create-chainer-from-axioms fire::create-chainer-from-kb fire::create-chainer fire::canonicalize-axiom fire::derive-feasible-solution-orderings-for-terms fire::derive-feasible-solution-orderings-for-term fire::process-term-for-backchaining fire::process-quantifier-for-backchaining fire::axiom-backchainable? fire::predicates-in-axiom fire::analyze-term-predicate-types fire::generate-query-order fire::generate-feasible-query-orderings fire::generate-feasible-query-orderings-for )) (defun untrace-chainer-construction () (untrace fire::create-chainer-from-axioms fire::create-chainer-from-kb fire::create-chainer fire::canonicalize-axiom fire::derive-feasible-solution-orderings-for-terms fire::derive-feasible-solution-orderings-for-term fire::process-term-for-backchaining fire::process-quantifier-for-backchaining fire::axiom-backchainable? fire::predicates-in-axiom fire::analyze-term-predicate-types fire::generate-query-order fire::generate-feasible-query-orderings fire::generate-feasible-query-orderings-for ))