然后我们想让程序证明：

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

    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 部分。这里有两个对应的例子：

    调用 <- 返回的是给定判断式下存储的规则数量；用 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))
    24. (defun vars-in (expr)
    25.   (if (atom expr)
    26.       (if (var? expr) (list expr))
    27.     (union (vars-in (car expr))
    28.            (vars-in (cdr expr)))))

    图 15.3: 推论。

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

    为了保证一条规则中的变量只表示规则中各参数之间的关系，我们用 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 或者 表达式是非常简单的。操作 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.        (let ,(mapcar #'(lambda (v)
    4.                          `(,v (binding ',v ,binds)))
    5.                      (vars-in query))
    6.          ,@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 提供了一个便捷的方法。下面是这个宏展开的情况：

    图 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.
    21. NIL

    图 15.7: 使用中的程序