4.5 合一
本节介绍 logic 语言中查询解释器的实现，它负责进行推理。解释器是一种通用的问题求解器，但在能求解的问题规模和类型上有相当大的局限。更复杂的逻辑编程语言已经存在，但如何构建高效的推理过程，仍是计算机科学中一个活跃的研究课题。
查询解释器执行的基本操作称为合一（unification）。合一是把查询与事实匹配起来的一种通用方法，两者都可能含有变量。查询解释器反复执行这个操作：先把原始查询与各个事实的结论匹配，再把事实的假设与数据库中的其他结论匹配。在这个过程中，查询解释器会在与查询相关的所有事实中搜索。一旦找到为变量赋值、从而支持该查询的办法，它就把这个赋值作为成功的结果返回。
4.5.1 模式匹配
为了返回与查询匹配的简单事实，解释器必须把一个含有变量的查询与一个不含变量的事实匹配起来。例如，如果变量 ?child 取值 barack，查询 (query (parent abraham ?child)) 就与事实 (fact (parent abraham barack)) 匹配。
一般来说，如果存在一种从变量名到值的绑定，把这些值代入模式后能得到某个表达式，那么这个模式就与该表达式匹配（表达式可能是嵌套的 Scheme 列表）。
例如，表达式 ((a b) c (a b)) 与模式 (?x c ?x) 匹配，此时变量 ?x 绑定到值 (a b)。同一个表达式也与模式 ((a ?y) ?z (a b)) 匹配，此时变量 ?y 绑定到 b，?z 绑定到 c。
4.5.2 表示事实和查询
导入所提供的 logic 示例程序，就能复现下面的例子。
>>> from logic import *在 logic 语言里，查询和事实都用 Scheme 列表表示，沿用前一章的 Pair 类和 nil 对象。例如，查询表达式 (?x c ?x) 就表示为一串嵌套的 Pair 实例。
>>> read_line("(?x c ?x)")
Pair('?x', Pair('c', Pair('?x', nil)))与 Scheme 项目一样，把符号绑定到值的环境用 Frame 类的一个实例表示，该实例有一个名为 bindings 的属性。
在 logic 语言中执行模式匹配（pattern matching）的函数名为 unify。它接受两个输入 e 和 f，外加一个环境 env，用来记录变量到值的绑定。
>>> e = read_line("((a b) c (a b))")
>>> f = read_line("(?x c ?x)")
>>> env = Frame(None)
>>> unify(e, f, env)
True
>>> env.bindings
{'?x': Pair('a', Pair('b', nil))}
>>> print(env.lookup('?x'))
(a b)上面 unify 的返回值是 True，说明模式 f 能匹配表达式 e。合一的结果记录在 env 中，即把 ?x 绑定到 (a b)。
4.5.3 合一算法
合一是模式匹配的推广，它试图在两个都可能含变量的表达式之间找出一种映射。unify 函数用一个递归过程实现合一：对两个表达式对应的部分逐一合一，直到出现矛盾，或者为所有变量建立起一组可行的绑定。
先看一个例子。模式 (?x ?x) 能匹配模式 ((a ?y c) (a b ?z))，因为存在一个不含变量的表达式能同时匹配两者：((a b c) (a b c))。合一通过以下步骤找出这个解：
- 匹配每个模式的第一个元素，变量
?x与表达式(a ?y c)绑定。 - 匹配每个模式的第二个元素，首先把变量
?x替换为它的值。然后，把?y绑定到b、?z绑定到c，(a ?y c)就与(a b ?z)匹配。
因此，传入 unify 的环境里会包含 ?x、?y 和 ?z 的绑定：
>>> e = read_line("(?x ?x)")
>>> f = read_line(" ((a ?y c) (a b ?z))")
>>> env = Frame(None)
>>> unify(e, f, env)
True
>>> env.bindings
{'?z': 'c', '?y': 'b', '?x': Pair('a', Pair('?y', Pair('c', nil)))}合一的结果可能把一个变量绑定到一个同样含变量的表达式上，就像上面把 ?x 绑定到 (a ?y c) 那样。bind 函数会递归地、反复地把表达式中的所有变量替换为它们的值，直到不再剩下已绑定的变量。
>>> print(bind(e, env))
((a b c) (a b c))一般来说，合一要检查若干条件。unify 的实现直接照下面的描述来。
- 如果输入
e和f是变量，就用它们的值替换。 - 如果
e和f相等，合一成功。 - 如果
e是变量，合一成功，并把e绑定到f。 - 如果
f是变量，合一成功，并把f绑定到e。 - 如果两者都不是变量，也都不是列表，而且不相等，那么
e和f就无法合一，合一失败。 - 如果以上情况都不成立，那么
e和f都是对，因此要对它们第一个和第二个对应元素分别做合一。
>>> def unify(e, f, env):
"""以破坏性的方式扩展 ENV，使 e 和 f 合一（变得相等）；成功返回
True，否则返回 False。无论哪种情况 ENV 都可能被修改（它已有的
绑定永不改变）。"""
e = lookup(e, env)
f = lookup(f, env)
if e == f:
return True
elif isvar(e):
env.define(e, f)
return True
elif isvar(f):
env.define(f, e)
return True
elif scheme_atomp(e) or scheme_atomp(f):
return False
else:
return unify(e.first, f.first, env) and unify(e.second, f.second, env)4.5.4 证明
对 logic 语言的一种理解方式，是把它看作形式系统中断言的证明器。每个陈述的事实都在形式系统中确立了一条公理，而每个查询都必须由查询解释器从这些公理出发来确立。换句话说，每个查询都断言：存在某种变量赋值，使它的所有子表达式都能同时从系统的事实中推出。查询解释器的作用就是验证这一点是否成立。
例如，给定关于狗的一组事实，我们可以断言克林顿和某只棕褐色的狗存在共同的祖先。只有当查询解释器能够确定这个断言为真时，它才会输出 Success!。作为副产品，它还会告诉我们这只共同祖先和那只棕褐色狗的名称：
(fact (parent abraham barack))
(fact (parent abraham clinton))
(fact (parent delano herbert))
(fact (parent fillmore abraham))
(fact (parent fillmore delano))
(fact (parent fillmore grover))
(fact (parent eisenhower fillmore))
(fact (ancestor ?a ?y) (parent ?a ?y))
(fact (ancestor ?a ?y) (parent ?a ?z) (ancestor ?z ?y))
(fact (dog (name abraham) (color white)))
(fact (dog (name barack) (color tan)))
(fact (dog (name clinton) (color white)))
(fact (dog (name delano) (color white)))
(fact (dog (name eisenhower) (color tan)))
(fact (dog (name fillmore) (color brown)))
(fact (dog (name grover) (color tan)))
(fact (dog (name herbert) (color brown)))(query (ancestor ?a clinton)
(ancestor ?a ?brown-dog)
(dog (name ?brown-dog) (color brown)))
Success!
a: fillmore brown-dog: herbert
a: eisenhower brown-dog: fillmore
a: eisenhower brown-dog: herbert结果中显示的三个赋值，每一个都只是那个更大证明的一条线索：给定这些事实，该查询为真。完整的证明会包含用到的所有事实，比如 (parent abraham clinton) 和 (parent fillmore abraham)。
4.5.5 搜索
为了从系统中已经确立的事实出发确立一个查询，查询解释器会在所有可能的事实中搜索。合一是对两个表达式做模式匹配的基本操作。查询解释器里的搜索过程会选择要合一哪些表达式，以便找到一组串接起来就能确立该查询的事实。
递归的 search 函数实现了 logic 语言的搜索过程。它的输入包括：查询中子句（clause）组成的 Scheme 列表 clauses；记录当前符号到值绑定的环境 env（初始为空）；以及已经串接起来的规则链的深度 depth。
>>> def search(clauses, env, depth):
"""搜索规则的某种应用，以确立所有 CLAUSES，同时以非破坏性的方式
扩展合一器 ENV。把搜索限制在 DEPTH 层规则的嵌套应用内。"""
if clauses is nil:
yield env
elif DEPTH_LIMIT is None or depth <= DEPTH_LIMIT:
if clauses.first.first in ('not', '~'):
clause = ground(clauses.first.second, env)
try:
next(search(clause, glob, 0))
except StopIteration:
env_head = Frame(env)
for result in search(clauses.second, env_head, depth+1):
yield result
else:
for fact in facts:
fact = rename_variables(fact, get_unique_id())
env_head = Frame(env)
if unify(fact.first, clauses.first, env_head):
for env_rule in search(fact.second, env_head, depth+1):
for result in search(clauses.second, env_rule, depth+1):
yield result同时满足所有子句的搜索从第一个子句开始。在第一个子句被否定的特殊情况下，我们不再尝试用事实去合一查询的第一个子句，而是递归调用 search，检查这样的合一是否不存在。如果这次递归调用一无所获，我们就继续搜索其余子句；如果能够合一，就立即失败。
如果第一个子句没有被否定，那么对数据库中的每个事实，search 都会尝试把事实的第一个子句与查询的第一个子句合一。合并在一个新的环境 env_head 中进行。作为合一的副作用，变量会在 env_head 里绑定到相应的值。
如果合一成功，该子句就与当前规则的结论相匹配。接下来的 for 语句试图确立规则的假设，从而确立结论。正是在这里，递归规则的假设会被递归地传给 search，以便得到确立。
最后，每一次对 fact.second 的成功搜索，都会把得到的环境绑定到 env_rule。有了这些变量到值的绑定，最后的 for 语句继续搜索，以确立初始查询中剩下的子句。任何成功的结果都会由内层的 yield 语句返回。
唯一名称。 合一假设 e 和 f 之间不共享任何变量。然而在 logic 语言的事实和查询中，我们经常重复使用变量名。我们不希望把一个事实里的 ?x 和另一个事实里的 ?x 混为一谈，这两个变量毫无关系。为了确保变量名不会混淆，在把事实传给 unify 之前，先用 rename_variables 把它的变量名替换成唯一的名字，做法是为该事实追加一个唯一的整数。
>>> def rename_variables(expr, n):
"""用标识符 N 重命名 EXPR 中的所有变量。"""
if isvar(expr):
return expr + '_' + str(n)
elif scheme_pairp(expr):
return Pair(rename_variables(expr.first, n),
rename_variables(expr.second, n))
else:
return expr其余细节——包括 logic 语言的用户界面和各种辅助函数的定义——都出现在 logic 示例中。