15.3 回答查询 (Answering Queries)

在介绍了绑定的概念之后，我们可以更准确的说一下我们的程序将要做什么：它得到一个可能包含变量的表达式，根据我们给定的事实和规则返回使它正确的所有绑定。比如，我们只有下面这个事实：

  1. (parent donald nancy)

然后我们想让程序证明：

  1. (parent ?x ?y)

它会返回像下面这样的表达：

  1. (((?x . donald) (?y . nancy)))

它告诉我们只有一个可以让这个表达式为真的方法： ?x 是 donald 并且 ?y 是 nancy 。

在通往目标的路上，我们已经有了一个的重要部分：一个匹配函数。 下面是用来定义规则的一段代码：

  1. (defvar *rules* (make-hash-table))
  3. (defmacro <- (con &optional ant)
  4.   `(length (push (cons (cdr ',con) ',ant)
  5.                  (gethash (car ',con) *rules*))))

图 15.2 定义规则

规则将被包含于一个叫做 *rules* 的哈希表，通过头部 (head) 的判断式构建这个哈系表。这样做加强了我们无法使用判断式中的变量的限制。虽然我们可以通过把所有这样的规则放在分离的列表中来消除限制，但是如果这样做，当我们需要证明某件事的时侯不得不和每一个列表进行匹配。

我们将要使用同一个宏 <- 去定义事实 (facts)和规则 (rules)。一个事实将被表示成一个没有 body 部分的规则。这和我们对规则的定义保持一致。一个规则告诉我们你可以通过证明 body 部分来证明 head 部分，所以没有 body 部分的规则意味着你不需要通过证明任何东西来证明 head 部分。这里有两个对应的例子：

  1. > (<- (parent donald nancy))
  2. 1
  3. > (<- (child ?x ?y) (parent ?y ?x))
  4. 1

调用 <- 返回的是给定判断式下存储的规则数量；用 length 函数来包装 push 能使我们免于看到顶层中的一大堆返回值。

下面是我们的推论程序所需的大多数代码：

  1. (defun prove (expr &optional binds)
  2.   (case (car expr)
  3.     (and (prove-and (reverse (cdr expr)) binds))
  4.     (or  (prove-or (cdr expr) binds))
  5.     (not (prove-not (cadr expr) binds))
  6.     (t   (prove-simple (car expr) (cdr expr) binds))))
  8. (defun prove-simple (pred args binds)
  9.   (mapcan #'(lambda (r)
  10.               (multiple-value-bind (b2 yes)
  11.                                    (match args (car r)
  12.                                           binds)
  13.                 (when yes
  14.                   (if (cdr r)
  15.                       (prove (cdr r) b2)
  16.                       (list b2)))))
  17.           (mapcar #'change-vars
  18.                   (gethash pred *rules*))))
  20. (defun change-vars (r)
  21.   (sublis (mapcar #'(lambda (v) (cons v (gensym "?")))
  22.                   (vars-in r))
  23.           r))
  25. (defun vars-in (expr)
  26.   (if (atom expr)
  27.       (if (var? expr) (list expr))
  28.     (union (vars-in (car expr))
  29.            (vars-in (cdr expr)))))

图 15.3: 推论。

上面代码中的 prove 函数是推论进行的枢纽。它接受一个表达式和一个可选的绑定列表作为参数。如果表达式不包含逻辑操作，它调用 prove-simple 函数，前面所说的链接 (chaining)正是在这个函数里产生的。这个函数查看所有拥有正确判断式的规则，并尝试对每一个规则的 head 部分和它想要证明的事实做匹配。对于每一个匹配的 head ，使用匹配所产生的新的绑定在 body 上调用 prove 。对 prove 的调用所产生的绑定列表被 mapcan 收集并返回：

  1. > (prove-simple 'parent '(donald nancy) nil)
  2. (NIL)
  3. > (prove-simple 'child '(?x ?y) nil)
  4. (((#:?6 . NANCY) (#:?5 . DONALD) (?Y . #:?5) (?X . #:?6)))

以上两个返回值指出有一种方法可以证明我们的问题。（一个失败的证明将返回 nil。）第一个例子产生了一组空的绑定，第二个例子产生了这样的绑定： ?x 和 ?y 被（间接）绑定到 nancy 和 donald 。

顺便说一句，这是一个很好的例子来实践 2.13 节提出的观点。因为我们用函数式的风格来写这个程序，所以可以交互式地测试每一个函数。

第二个例子返回的值里那些 gensyms 是怎么回事？如果我们打算使用含有变量的规则，我们需要避免两个规则恰好包含相同的变量。如果我们定义如下两条规则：

  1. (<- (child ?x ?y) (parent ?y ?x))
  3. (<- (daughter ?y ?x) (and (child ?y ?x) (female ?y)))

第一条规则要表达的意思是：对于任何的 x 和 y ， 如果 y 是 x 的家长，则 x 是 y 的孩子。第二条则是：对于任何的 x 和 y ， 如果 y 是 x 的孩子并且 y 是女性，则 y 是 x 的女儿。在每一条规则内部，变量之间的关系是显著的，但是两条规则使用了相同的变量并非我们刻意为之。

如果我们使用上面所写的规则，它们将不会按预期的方式工作。如果我们尝试证明“ a 是 b 的女儿”，匹配到第二条规则的 head 部分时会将 a 绑定到 ?y ，将 b 绑定到 ?x。我们无法用这样的绑定匹配第一条规则的 head 部分：

  1. > (match '(child ?y ?x)
  2.          '(child ?x ?y)
  3.          '((?y . a) (?x . b)))
  4. NIL

为了保证一条规则中的变量只表示规则中各参数之间的关系，我们用 gensyms 来代替规则中的所有变量。这就是 change-vars 函数的目的。一个 gensym 不可能在另一个规则中作为变量出现。但是因为规则可以是递归的，我们必须防止出现一个规则和自身冲突的可能性，所以在定义和使用一个规则时都要调用 chabge-vars 函数。

现在只剩下定义用以证明复杂表达式的函数了。下面就是需要的函数：

  1. (defun prove-and (clauses binds)
  2.   (if (null clauses)
  3.       (list binds)
  4.       (mapcan #'(lambda (b)
  5.                   (prove (car clauses) b))
  6.               (prove-and (cdr clauses) binds))))
  8. (defun prove-or (clauses binds)
  9.   (mapcan #'(lambda (c) (prove c binds))
  10.           clauses))
  12. (defun prove-not (clause binds)
  13.   (unless (prove clause binds)
  14.     (list binds)))

图 15.4 逻辑操作符 (Logical operators)

操作一个 or 或者 not 表达式是非常简单的。操作 or 时，我们提取在 or 之间的每一个表达式返回的绑定。操作 not 时，当且仅当在 not 里的表达式产生 none 时，返回当前的绑定。

prove-and 函数稍微复杂一点。它像一个过滤器，它用之后的表达式所建立的每一个绑定来证明第一个表达式。这将导致 and 里的表达式以相反的顺序被求值。除非调用 prove 中的 prove-and 函数则会先逆转它们。

现在我们有了一个可以工作的程序，但它不是很友好。必须要解析 prove-and 返回的绑定列表是令人厌烦的，它们会变得更长随着规则变得更加复杂。下面有一个宏来帮助我们更愉快地使用这个程序：

  1. (defmacro with-answer (query &body body)
  2.   (let ((binds (gensym)))
  3.     `(dolist (,binds (prove ',query))
  4.        (let ,(mapcar #'(lambda (v)
  5.                          `(,v (binding ',v ,binds)))
  6.                      (vars-in query))
  7.          ,@body))))

图 15.5 介面宏 (Interface macro)

它接受一个 query （不被求值）和若干表达式构成的 body 作为参数，把 query 所生成的每一组绑定的值赋给 query 中对应的模式变量，并计算 body 。

  1. > (with-answer (parent ?x ?y)
  2.     (format t "~A is the parent of ~A.~%" ?x ?y))
  3. DONALD is the parent of NANCY.
  4. NIL

这个宏帮我们做了解析绑定的工作，同时为我们在程序中使用 prove 提供了一个便捷的方法。下面是这个宏展开的情况：

  1. (with-answer (p ?x ?y)
  2.   (f ?x ?y))
  4. ;;将被展开成下面的代码
  6. (dolist (#:g1 (prove '(p ?x ?y)))
  7.   (let ((?x (binding '?x #:g1))
  8.         (?y (binding '?y #:g1)))
  9.     (f ?x ?y)))

图 15.6: with-answer 调用的展开式

下面是使用它的一个例子：

  1. (<- (parent donald nancy))
  2. (<- (parent donald debbie))
  3. (<- (male donald))
  4. (<- (father ?x ?y) (and (parent ?x ?y) (male ?x)))
  5. (<- (= ?x ?y))
  6. (<- (sibling ?x ?y) (and (parent ?z ?x)
  7.                          (parent ?z ?y)
  8.                          (not (= ?x ?y))))
  10. ;;我们可以像下面这样做出推论
  12. > (with-answer (father ?x ?y)
  13.     (format t "~A is the father of ~A.~%" ?x ?y))
  14. DONALD is the father of DEBBIE.
  15. DONALD is the father of NANCY.
  16. NIL
  17. > (with-answer (sibling ?x ?y))
  18.     (format t "~A is the sibling of ~A.~%" ?x ?y))
  19. DEBBLE is the sibling of NANCY.
  20. NANCY is the  sibling of DEBBIE.
  21. NIL

图 15.7: 使用中的程序