;;;; -*- Mode: LISP; Syntax: Common-Lisp; Base: 10 -*- ;;;; --------------------------------------------------------------------- ;;;; File name: indexer.lsp ;;;; System: FIRE ;;;; Author: Praveen Paritosh ;;;; Created: October 23, 2001 21:05:00 ;;;; Purpose: Indexes axioms into a fast-loadable-and-dumpable structure ;;;; --------------------------------------------------------------------- ;;;; Modified: Monday, February 23, 2004 at 23:39:04 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, extracted from the KB, intended to ;;; handle the reflexive backchaining for a specific class of tasks or domain of interest. ;;; Generally there will be several chainers for 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 loaded from 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. It has a TITLE, which is a string, used to ;;; retrieve the chainer from the KB. It provides a rapid way of indexing into what clauses ;;; can provide a result, via the procedure APPLICABLE-CLAUSES. ;;; ;;; What goes into a chainer? That is determined currently by FIRE application developers. ;;; We want to experiment with automatic KB partitioning in the future, such as the work underway ;;; at KSL, as well as connection graph techniques and knowledge about available sources to ;;; use control knowledge to automatically chainers for efficient reasoning. This code ;;; provides a minimal useful infrastructure, with enough procedural hooks to support this ;;; experimentation while in the meantime allow some practical systems to be built. ;;; 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 an ;;; 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-LIST 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?) (kb *kb*)) (let* ((axioms (get-all-axioms-from-kb kb)) (chainer (make-instance 'chainer :title title :kb kb))) (dolist (axiom axioms (add-chainer-to-kb chainer kb)) (when (funcall include-test axiom) (process-axiom-for-backchaining axiom chainer predicate-test))))) ;;; Added by Dan Halstead 7/18/03: ;;; This will create a chainer from all of the macros as well as the explicit ;;; axioms in the KB (unless one specifies :all-macros or :all-axioms nil). (defun create-chainer-from-kb (title &key (include-test 'axiom-backchainable?) (predicate-test 'predicate-backchainable?) (all-macros t) (all-axioms t) (kb *kb*) verbose) (when verbose (format t "Creating to store all axioms and macros.~%" title)) (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 :kb kb))) (when verbose (format t "Adding all clauses to chainer.~%")) (dolist (axiom axiom-list (add-chainer-to-kb chainer kb)) (when (funcall include-test axiom) (process-axiom-for-backchaining axiom chainer predicate-test))))) (defvar *rmp-expansions* nil "For debugging") (defun create-chainer-from-macros (title macros &key (kb *kb*)) (let ((chainer (make-instance 'chainer :title title :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 (kb *kb*)) (let ((chainer (make-instance 'chainer :title title :kb kb))) (dolist (axiom axioms (add-chainer-to-kb chainer kb)) (process-axiom-for-backchaining axiom chainer 'always-true)))) ;;; Recursive chainer construction from a list of predicates (defun create-chainer-from-predicates (title predlist &key (depth :exhaustive) (kb *kb*) (all-axioms nil)) (if (null all-axioms) (setq all-axioms (get-all-axioms-from-kb kb))) (create-chainer-from-axioms title (get-axioms-recursively-from-predicates predlist :depth depth :all-axioms all-axioms) :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)))) (defun lookup-chainer (title kb) (find title (chainers kb) :test 'string-equal :key 'title)) (defun add-chainer-to-kb (chainer kb) (let ((old-chainer (lookup-chainer (title chainer) kb))) (when old-chainer (setf (chainers kb) (delete old-chainer (chainers kb)))) (push chainer (chainers kb)) chainer)) (defun always-true (x) (declare (ignore x)) t) (defun process-axiom-for-backchaining (axiom chainer predicate-test) (let ((clauses (canonicalize-axiom axiom))) (dolist (terms clauses) (let ((clause (make-instance 'clause :id (incf (clause-counter chainer)) :chainer chainer :terms terms :variables (find-clause-variables terms) :axiom axiom))) (setf (gethash (id clause) (clauses chainer)) clause) (dolist (term-plus-orderings (derive-feasible-solution-orderings-for-terms terms)) (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 ( . ) (unless (quantified-term? (car term)) (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))))))))) (defun lookup-clause (id chainer) (gethash id (clauses chainer))) (defun find-clause-variables (terms) (let ((ltre::*bound-vars* nil)) ;; Avoid accidents (ltre::pattern-free-variables terms))) ;;; ADD-chainer-TO-REASONER adds a chainer to a reasoner. This makes it available ;;; for queries from that reasoner. (defun add-chainer-to-reasoner (index reasoner) (when (chainer? index) (pushnew index (chainers reasoner) :test 'string-equal :key 'title))) (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)) ;; 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. ;; modified 7/16/03 (TRH) to check backchainForbidden. (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) (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)))