;file: inference.lsp
;purpose: rule-based inference from Graham ANSI Common Lisp
;programmer: Tom Shultz
;started:
;current:
;Graham's code, commented by T. Shultz
(defun match (x y &optional binds)
"(x y &optional binds)
Bind variables to values in trees x & y."
(cond
((eql x y) (values binds t))
((assoc x binds) (match (binding x binds) y binds))
((assoc y binds) (match x (binding y binds) binds))
((var? x) (values (cons (cons x y) binds) t))
((var? y) (values (cons (cons y x) binds) t))
(t
(when (and (consp x) (consp y))
(multiple-value-bind (b2 yes)
(match (car x) (car y) binds)
(and yes (match (cdr x) (cdr y) b2)))))))
(defun var? (x)
"(x)
Is x a variable?"
(and (symbolp x)
(eql (char (symbol-name x) 0) #\?)))
(defun binding (x binds)
"(x binds)
Helping function for match."
(let ((b (assoc x binds)))
(if b
(or (binding (cdr b) binds)
(cdr b)))))
(defvar *rules* (make-hash-table)
"Initialize rules to a hash table for efficiency.")
(defmacro <- (con &optional ant)
"(con &optional ant)
Enter a rule, consequents first, or a fact, consequents only."
`(length (push (cons (cdr ',con) ',ant)
(gethash (car ',con) *rules*))))
(defun prove (expr &optional binds)
"(expr &optional binds)
Try to prove expr given optional binds."
(case (car expr)
(and (prove-and (reverse (cdr expr)) binds))
(or (prove-or (cdr expr) binds))
(not (prove-not (cadr expr) binds))
(t (prove-simple (car expr) (cdr expr) binds))))
(defun prove-simple (pred args binds)
"(pred args binds)
Examine all rules with predicate pred,
trying to match consequent of each with fact it is trying to prove.
Return lists of bindings.
For simple expressions without logical operators."
(mapcan #'(lambda (r)
(multiple-value-bind (b2 yes)
(match args (car r)
binds)
(when yes
(if (cdr r)
(prove (cdr r) b2)
(list b2)))))
(mapcar #'change-vars
(gethash pred *rules*))))
(defun change-vars (r)
"(r)
Replace variables in rule r with gensyms in case variable appears in other rules."
(sublis (mapcar #'(lambda (v) (cons v (gensym "?")))
(vars-in r))
r))
(defun vars-in (expr)
"(expr)
Helping function for change-vars."
(if (atom expr)
(if (var? expr) (list expr))
(union (vars-in (car expr))
(vars-in (cdr expr)))))
(defun prove-and (clauses binds)
"(clauses binds)
Try to prove the first expression for each set of bindings that work for remaining expressions."
(if (null clauses)
(list binds)
(mapcan #'(lambda (b)
(prove (car clauses) b))
(prove-and (cdr clauses) binds))))
(defun prove-or (clauses binds)
"(clauses binds)
Collect bindings returned by each disjunct expression."
(mapcan #'(lambda (c) (prove c binds))
clauses))
(defun prove-not (clause binds)
"(clause binds)
Return current bindings IFF expression yields no bindings."
(unless (prove clause binds)
(list binds)))
(defmacro with-answer (query &body body)
"(query &body body)
Decipher bindings by evaluating body of expressions
once for each set of bindings generated by query."
(let ((binds (gensym)))
`(dolist (,binds (prove ',query))
(let ,(mapcar #'(lambda (v)
`(,v (binding ',v ,binds)))
(vars-in query))
,@body))))
(defun hash-pairs (ht)
"(ht)
Fetch all the entries in hash table ht."
(let ((acc nil))
(maphash #'(lambda (k v)
(push (cons k v) acc))
ht)
acc))
;(hash-pairs *rules*)
;code added by T. Shultz to enable entry of list of facts
(defun rule (x)
"(x)
Enter rule x into hash table *rules*."
(let ((con (first x))
(ant (second x)))
(length (push (cons (cdr con) ant)
(gethash (car con) *rules*)))))
(defun fact (x)
"(x)
Enter fact x into hash table *rules*."
(length (push (list (cdr x))
(gethash (car x) *rules*))))
(defun enter-facts (x)
"(x)
Enter list of facts into hash table *rules*."
(do ((x x (cdr x)))
((null x))
(fact (car x))))