;;;; -*- Mode: LISP; Syntax: Common-Lisp; Base: 10 -*- ;;;; --------------------------------------------------------------------------- ;;;; File name: structural.lsp ;;;; System: FIRE ;;;; Author: Ken Forbus ;;;; Created: February 26, 2003 12:06:41 ;;;; Purpose: Handling structural queries in ASK ;;;; --------------------------------------------------------------------------- ;;;; Modified: Monday, February 23, 2004 at 23:12:46 by Kenneth Forbus ;;;; --------------------------------------------------------------------------- (in-package :fire) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Handling structural queries ;;; These relationships provide access to the structure of assertions themselves. ;;; Most of them are from Cyc, but we've defined a few of our own to support ;;; making dynamic case construction more declarative. ;;; ;;; This vocabulary will change very infrequently, hence we just hard-wire it. (defun structural-statement? (query) (structural-predicate? (car query))) (defun structural-predicate? (pred) (member pred (if (mixed-case?) '(data::someArgumentHasPredicate data::assertedTermSentences data::termOfUnit data::termFormulas data::operatorFormulas data::natArgument data::natFunction) '(data::some-argument-has-predicate data::asserted-term-sentences data::term-of-unit data::term-formulas data::operator-formulas data::nat-argument data::nat-function)))) (defun ask-structural-statement (query reasoner context number response effort) (declare (ignore context number effort)) ;; We ignore context because the structure of assertions is considered a universal. ;; We ignore number because we want to cache the results once and for all. ;; We ignore effort because these are simple enough that we want to just do them, ;; always. (Well, sort of simple -- retrieving references can be expensive, but all ;; the more reason to do it just once and cache.) (ecase (car query) ((data::someArgumentHasPredicate data::some-argument-has-predicate) (handle-someArgumentHasPredicate (car query) (cdr query) reasoner response)) ((data::assertedTermSentences data::asserted-term-sentences) (handle-assertedTermSentences (car query) (cdr query) reasoner response)) ((data::termOfUnit data::term-of-unit) (handle-termOfUnit (car query) (cdr query) reasoner response)) ((data::termFormulas data::term-formulas) (handle-termFormulas (car query) (cdr query) reasoner response)) ((data::operatorFormulas data::operator-formulas) (handle-operatorFormulas (car query) (cdr query) reasoner response)) ((data::natArgument data::natArgument) (handle-natArgument (car query) (cdr query) reasoner response)) ((data::natFunction data::natFunction) (handle-natFunction (car query) (cdr query) reasoner response)))) (defun expression-or-variable? (thing) (or (variable? thing) (and (listp thing) (not (null thing))) (symbolp thing) (numberp thing))) (defun justify-structural-result-as-premise (statement reasoner) ;; Some things are unchangable, and hence are safe to assert (ltre::assert! statement :structural-property (ltre reasoner))) ;;; someArgumentHasPredicate ; (someArgumentHasPredicate ?fact ?pred) is true iff there is some ; subexpression of an argument of ?fact such that ?pred is its functor. ; That is, it goes down the tree, not just one level (defmethod predicate-ask-signatures ((pred (eql 'data::someArgumentHasPredicate)) (reasoner reasoner)) '((:input-only :produces) (:input-only :input-only))) (defun handle-someArgumentHasPredicate (pred args reasoner response) (unless (and (listp args) (= (length args) 2) (expression-or-variable? (car args)) (expression-or-variable? (cadr args))) (error "Poorly formed someArgumentHasPredicate statement: ~A, ~A; ~A, ~A." pred args reasoner response)) (cond ((variable? (car args)) (cond ((variable? (cadr args)) ;; Fail, we're not going to go over whole KB ;; for every predicate and statement! nil) (t ;; This is a request for all of the facts that contain a given predicate ;; as an argument to a subexpression. ;; ***** Handle this one via an ASK to get the references, then filter? ;; ***** Punt for now. ))) ((variable? (cadr args)) ;; This is a request for all of the predicates within the subexpressions of FACT. (let* ((statement (car args)) (var (cadr args)) (arg-predicates (extract-all-subexpression-predicates (cdr statement))) (binding-lists nil)) (dolist (arg-pred arg-predicates) (justify-structural-result-as-premise (list pred statement arg-pred) reasoner) (push (list (cons var arg-pred)) binding-lists)) (let ((results (case response (:bindings binding-lists) (:pattern (mapcar #'(lambda (arg-pred) (list pred statement arg-pred)) arg-predicates)) (t (mapcar #'(lambda (bindings) (sublis bindings response)) binding-lists))))) (values results nil)))) ;; Simplest case: A check as to whether or not there is one. ;; Check cache first (t (let ((query (cons pred args))) (cond ((ltre:known? query (ltre reasoner)) ;; Don't recompute (cond ((ltre:true? query (ltre reasoner)) (values (case response (:bindings (list nil)) (:pattern (list query)) (t (list response))) nil)) (t (values nil nil)))) (t (let* ((statement (car args)) (arg-pred (cadr args)) (found? (some-subexpression-has-predicate? (cdr statement) arg-pred))) (cond (found? (justify-structural-result-as-premise query reasoner) (values (case response (:bindings (list nil)) (:pattern (list (cons pred args))) (t (list response))))) (t ;; Justify negation explicitly (justify-structural-result-as-premise (list :not query) reasoner) (values nil nil)))))))))) (defun some-subexpression-has-predicate? (subexpressions pred) (cond ((null subexpressions) nil) ((not (listp subexpressions)) nil) ((not (listp (car subexpressions))) (some-subexpression-has-predicate? (cdr subexpressions) pred)) ((equal (caar subexpressions) pred) t) (t (or (some-subexpression-has-predicate? (cdar subexpressions) pred) (some-subexpression-has-predicate? (cdr subexpressions) pred))))) (defun extract-all-subexpression-predicates (subexpressions) (extract-all-subexpression-predicates1 subexpressions nil)) (defun extract-all-subexpression-predicates1 (subexpressions preds) (cond ((null subexpressions) preds) ((not (listp subexpressions)) preds) ((not (listp (car subexpressions))) (extract-all-subexpression-predicates1 (cdr subexpressions) preds)) (t (pushnew (caar subexpressions) preds :test 'equal) (extract-all-subexpression-predicates1 (cdr subexpressions) (extract-all-subexpression-predicates1 (cdar subexpressions) preds))))) (defmethod predicate-ask-signatures ((pred (eql 'data::termOfUnit)) (reasoner reasoner)) ;; (termOfUnit ) '((:produces :input-only))) ;;; In Progress: (defun handle-termOfUnit (pred args reasoner response) (unless (and (listp args) (= (length args) 2) (expression-or-variable? (car args)) (expression-or-variable? (cadr args))) (error "Malformed termOfUnit expression: ~A, ~A; ~A, ~A" pred args reasoner response)) (let ((term (car args)) (nat (cadr args))) (cond ((variable? nat) nil) ;; Punt ((variable? term) ;; Find operator (when (listp nat) (case response (:bindings (list (list (cons term nat)))) (t (error "termOfUnit can only return bindings: ~A, ~A; ~A, ~A" pred args reasoner response))))) (t nil)))) ;;;; termFormulas (from Cyc) ; (termFormulas SENTENCE TERM) means that TERM appears somewhere in SENTENCE. ; This is a purely local query, hence it doesn't need to check to see if something is in ; the reasoner. ; Cases: ; ?term, constant sentence: Generates assertions for each term in the sentence. ; constant term, sentence: True or false depending on whether term is in sentence. ; Ambiguous from Cyc docs whether or not this is recursive. We're going to ; assume that it is. (defmethod predicate-ask-signatures ((pred (eql 'data::termFormulas)) (reasoner reasoner)) ;; (termFormulas ) '((:input-only :produces) (:input-only :input-only))) (defun handle-termFormulas (pred args reasoner response) (unless (and (listp args) (= (length args) 2) (expression-or-variable? (car args)) (expression-or-variable? (cadr args))) (error "Malformed termFormulas expression: ~A, ~A: ~A, ~A." pred args reasoner response)) (let ((qterm (cadr args)) (sentence (car args))) (cond ((variable? sentence) nil) ;; Must have an expression to operate on ((variable? qterm) ;; Generate statements per term (let ((terms (extract-terms-from-statement sentence)) (binding-lists nil)) (dolist (term terms) (justify-structural-result-as-premise (list pred sentence term) reasoner) (push (list (cons qterm term)) binding-lists)) (case response (:bindings binding-lists) (:pattern (mapcar #'(lambda (term) (list pred sentence term)) terms)) (t (mapcar #'(lambda (bindings) (sublis bindings response)) binding-lists))))) ((term-found-in-statement? qterm sentence) (case response (:bindings (list nil)) (:pattern (list (list pred sentence qterm))) (:response response))) (t nil)))) (defun term-found-in-statement? (term statement) (cond ((null statement) nil) ((equal term statement) t) ((listp statement) (cond ((function? (car statement)) nil) ;; Don't go inside term (t (dolist (arg (cdr statement)) (if (term-found-in-statement? term arg) (return-from term-found-in-statement? (values t))))))))) (defun extract-terms-from-statement (statement) (extract-terms-from-statement1 statement nil)) (defun extract-terms-from-statement1 (statement terms) (cond ((null statement) terms) ((listp statement) (cond ((function? (car statement)) (pushnew statement terms :test 'equal) terms) (t (dolist (arg (cdr statement) terms) (setq terms (extract-terms-from-statement1 arg terms)))))) (t (pushnew statement terms :test 'equal) terms))) ;;;; operatorFormulas (from Cyc) [Handle natFunction the same way] ; (operatorFormulas TERM FORMULA) means that TERM is the operator of FORMULA, i.e., ; appears in the zeroth position. ; Cases: ; constant term, constant formula: test ; constant term, variable formula: Don't do anything. See assertedTermSentences instead. ; variable term, constant formula: bind to operator of the formula. (defmethod predicate-ask-signatures ((pred (eql 'data::operatorFormulas)) (reasoner reasoner)) ;; (operatorFormulas ) '((:produces :input-only) (:input-only :input-only))) (defun handle-operatorFormulas (pred args reasoner response) (unless (and (listp args) (= (length args) 2) (expression-or-variable? (car args)) (expression-or-variable? (cadr args))) (error "Malformed operatorFormulas expression: ~A, ~A; ~A, ~A" pred args reasoner response)) (let ((op (car args)) (formula (cadr args))) (cond ((variable? formula) nil) ;; Punt ((variable? op) ;; Find operator (when (listp formula) (justify-structural-result-as-premise (list pred (car formula) formula) reasoner) (case response (:bindings (list (list (cons op (car formula))))) (:pattern (list (list pred (car formula) formula))) (t (list (sublis (list (cons op (car formula))) response)))))) ((equal (car formula) op) ;; Probably need variant check here in general (justify-structural-result-as-premise (cons pred args) reasoner) (case response (:bindings (list nil)) (:pattern (list (cons pred args))) (t (list response)))) (t nil)))) ;;;; assertedTermSentences (from Cyc) ; (assertedTermSentences TERM SENTENCE) means that SENTENCE, which is found in the KB, ; contains TERM. ; Cases: ; 1. constant TERM, constant SENTENCE: Check to see that SENTENCE is in KB, and if so, does it ; contain term. ; 2. variable TERM, constant SENTENCE: Check if sentence is in KB, and extract all terms. ; 3. constant TERM, variable SENTENCE: Retrieve all references to TERM in KB, remove those where ; it doesn't appear as a term (i.e., when it is used only as a predicate). (defmethod predicate-ask-signatures ((pred (eql 'data::assertedTermSentences)) (reasoner reasoner)) ;; (assertedTermSentences ) '(;; (:produces :input-only) ;; Harder than it looks (:input-only :produces) (:input-only :input-only))) (defun handle-assertedTermSentences (pred args reasoner response) (unless (and (listp args) (= (length args) 2) (expression-or-variable? (car args)) (expression-or-variable? (cadr args))) (error "Malformed assertedTermSentences expression: ~A, ~A: ~A, ~A." pred args reasoner response)) (let ((qterm (car args)) (qsentence (cadr args))) (cond ((variable? qterm) nil) ;;**** Not really right, but these are low ;; ***** priority so implement later. ((variable? qsentence) ;; the useful case (let ((sentences (retrieve-references qterm)) (binding-lists nil)) (dolist (sentence sentences) (let ((asn-form (make-in-kb-statement sentence))) (ltre::assume! asn-form :kb-lookup (ltre reasoner)) (ltre::assert! `(:implies ,asn-form ,(list pred qterm sentence)) :structural-plus-kb)) (push (list (cons qsentence sentence)) binding-lists)) (case response (:bindings binding-lists) (:pattern (mapcar #'(lambda (sentence) (list pred qterm sentence)) sentences)) (t (mapcar #'(lambda (bindings) (sublis bindings response)) binding-lists))))) (t ;; trivial case: no variables at all (and (term-found-in-statement? qterm qsentence) (ask-proposition qsentence reasoner nil 1 response nil)))))) ;;;; natFunction (from Cyc) ; (natFunction NAT FUNCTION) states that FUNCTION is the function used in the ; non-atomic term NAT. For example, (natFunction (JuvenileFn Dog) JuvenileFn). ; More precisely, (termOfUnit NAT (FUNCTION ...)) implies (natFunction NAT FUNCTION)." ; This predicate exists to make it easier and more efficient to write arity-independent ; rules about functional terms without having to resort to dotted variable syntax ; such as (termOfUnit ?NAT (?FUNCTION . ?ARGS)). ;; Note: natFunction is like operatorFormulas, but its arguments are reversed. (defmethod predicate-ask-signatures ((pred (eql 'data::natFunction)) (reasoner reasoner)) ;; (natFunction ) '((:input-only :input-only) (:input-only :produces))) (defun handle-natFunction (pred args reasoner response) (unless (and (listp args) (= (length args) 2) (expression-or-variable? (car args)) (expression-or-variable? (cadr args))) (error "Malformed natFunction expression: ~A, ~A; ~A, ~A" pred args reasoner response)) (let ((nat (car args)) (fn (cadr args))) (cond ((variable? nat) nil) ;; Punt ((variable? fn) ;; Find operator (when (listp nat) (case response (:bindings (list (list (cons fn (car nat))))) (:pattern (list (list pred nat (car nat)))) (t (list (sublis (list (cons fn (car nat))) response)))))) ((equal (car nat) fn) ;; Probably need variant check here in general (justify-structural-result-as-premise (cons pred args) reasoner) (case response (:bindings (list nil)) (:pattern (list (cons pred args))) (t (list response)))) (t nil)))) ;;;; FormulaArgument (from Cyc) [Handle natArgument the same way] ; (formulaArgument FORMULA N TERM) means that TERM appears as the Nth argument in FORMULA. ; Cases: ; All constants: test if true. ; Formula variable: punt, this is local. ; N variable only: See if TERM is one of the args, and bind it appropriately. ; TERM variable only: Bind it to Nth argument. ; Both N, TERM variable: Generate solutions for each argument. (defmethod predicate-ask-signatures ((pred (eql 'data::formulaArgument)) (reasoner reasoner)) ;; (formulaArgument ) '((:input-only :input-only :input-only) (:input-only :produces :input-only) (:input-only :input-only :produces) (:input-only :produces :produces))) ;;;; natArgument (from Cyc) ; (natArgument NAT N TERM) means that TERM is in the Nth argument position of ; the non-atomic term NAT. For example, (natArgument (JuvenileFn Dog) 1 Dog). ; Note that (termOfUnit NAT (FUNCTION ... ARGN ...)) implies (natArgument NAT N ARGN). ; This predicate exists to make it easier and more efficient to write arity-independent ; rules about functional terms without having to resort to dotted variable syntax ; such as (termOfUnit ?NAT (?FUNCTION . ?ARGS))." (defmethod predicate-ask-signatures ((pred (eql 'data::natArgument)) (reasoner reasoner)) ;; (natArgument ) '((:input-only :input-only :input-only) (:input-only :produces :input-only) (:input-only :input-only :produces) (:input-only :produces :produces))) (defun handle-natArgument (pred args reasoner response) (unless (and (listp args) (= (length args) 3) (expression-or-variable? (car args)) (expression-or-variable? (cadr args)) (expression-or-variable? (caddr args))) (error "Malformed natFunction expression: ~A, ~A; ~A, ~A" pred args reasoner response)) (let ((nat (car args)) (n (cadr args)) (term (caddr args))) (cond ((variable? nat) nil) ;; Punt ((and (variable? n) (variable? term)) ;; Generate multiple solutions ;; loop through nat arguments, accumulating bindings (let ((result nil) (i 1)) (when (listp nat) (dolist (natArg (cdr nat)) (case response (:bindings (push (list (cons n i) (cons term natArg)) result)) (:pattern (push (list pred nat i natArg) result)) (t (push (sublis (list (cons n i) (cons term natArg)) response) result))) (incf i))) result)) ((variable? n) ;; Find position of term (assume there's only one!) (let ((pos (position term nat :start 1))) (when (and pos (listp nat)) (case response (:bindings (list (list (cons n pos)))) (:pattern (list (list pred nat pos term))) (t (list (sublis (list (cons n pos)) response))))))) ((variable? term) ;; Find term (when (listp nat) (case response (:bindings (list (list (cons term (nth n nat))))) (:pattern (list (list pred nat n (nth n nat)))) (t (list (sublis (list (cons term (nth n nat))) response)))))) ((equal (nth n nat) term) ;; All constants ;; Probably need variant check here in general (justify-structural-result-as-premise (cons pred args) reasoner) (case response (:bindings (list nil)) (:pattern (list (cons pred args))) (t (list response)))) (t nil)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; End of Code