> For the complete documentation index, see [llms.txt](https://zlt-shadow.gitbook.io/sicp-in-python-cn/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://zlt-shadow.gitbook.io/sicp-in-python-cn/di-4-zhang-shu-ju-chu-li/4.5-lian-he.md). # 4.5 联合 本节描述用逻辑语言执行推理的查询解释器的实现。 解释器是一个一般的问题解决者，但是在它能解决的问题的规模和类型上有很大的限制。 虽然存在更复杂的逻辑程序设计语言，但构建高效推理程序仍然是计算机科学中一个活跃的研究课题。 查询解释器执行的基本操作称为联合。联合是将查询与事实相匹配的一般方法，每个查询都可能包含变量。查询解释器反复应用此操作，首先将原始查询与事实结论进行匹配，然后将事实假设与数据库中的其他结论进行匹配。 在此过程中，查询解释器在与查询相关的所有事实空间中执行搜索。 如果它找到一种方法，通过向变量赋值来支持该查询，那么它将作为成功的结果返回该赋值。 ### 4.5.1 模式匹配 为了返回与查询匹配的简单事实，解释器必须将包含变量的查询与不包含变量的事实匹配。 例如，如果变量?child的值为barack，则查询(query(父abraham ?child))和事实(fact(父abraham barack))匹配。 通常，如果存在变量名与值的绑定，将这些值替换到模式中就会生成表达式，那么模式就会匹配某个表达式(可能是嵌套的模式列表)。 例如，表达式((a b) c (a b))匹配模式(? 同样的表达式匹配模式((a ?y) ?z (a b))，变量?y绑定b，?z绑定c。 ### 4.5.2 表达事实和查询 通过导入提供的逻辑示例程序，可以复制以下示例。 ``` >>> from logic import * ``` 查询和事实都在逻辑语言中表示为Scheme列表，使用前一章中的相同的Pair类和nil对象。例如，查询表达式(?x c ?x)表示为嵌套的Pair实例。 ``` >>> read_line("(?x c ?x)") Pair('?x', Pair('c', Pair('?x', nil))) ``` 与在Scheme项目中一样，将符号绑定到值的环境用Frame类的实例表示，该实例有一个名为bindings的属性。 在逻辑语言中执行模式匹配的函数称为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。unify 的结果记录在env中的?x到(a b)的绑定中。 ### 4.5.3 联合算法 联合是模式匹配的概括，它试图找到两个可能都包含变量的表达式之间的映射。unify 函数通过递归过程实现联合，即对两个表达式的相应部分进行联合，直到达到矛盾或建立对所有变量的可行绑定。 让我们从一个例子开始。 模式(? x ?x)可以匹配模式((a ?y c) (a ?z))，因为有一个没有变量的表达式同时匹配:((a ? b c) (a ? b c))。 unify通过以下步骤确定这个解决方案： 1. 为了匹配每个模式的第一个元素，变量?x被绑定到表达式(a ?y c)。 2. 为了匹配每个模式的第二个元素，首先将变量?x替换为它的值。然后，通过将?y绑定到b，将?z绑定到c，将(a ?y c)匹配到(a ?y 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 bound to (a ?y c). bind函数递归和重复地将所有变量绑定到表达式中的值上，直到绑定的变量没有剩下为止。 ``` >>> print(bind(e, env)) ((a b c) (a b c)) ``` 一般来说，联合是要检查几个条件的。unify的实现直接遵循下面的描述。 1. 如果输入e和f是变量，则用它们的值来替换。 2. 如果e和f相等，则联合成功。 3. 如果e是一个变量，联合成功，e绑定到f。 4. 如果f是一个变量,联合成功，f绑定到e。 5. 如果都不是一个变量，这两个不列出，他们是不平等的，然后e和f不能联合，所以联合失败。 6. 如果这些情况都不成立，那么e和f都是一对，因此它们的第一个和第二个对应元素都是联合的。 ``` >>> def unify(e, f, env): """Destructively extend ENV so as to unify (make equal) e and f, returning True if this succeeds and False otherwise. ENV may be modified in either case (its existing bindings are never changed).""" 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 证明 考虑逻辑语言的一种方式是将其视为一个正式系统中断言的证明。 每个陈述的事实在一个正式系统中建立一个公理，每个查询必须由查询解释器根据这些公理建立。 也就是说，每个查询都断言对其变量进行了某种赋值，以便它的所有子表达式同时遵循系统的事实。 查询解释器的角色是验证这一点。 例如，考虑到关于狗的一系列事实，我们可以断言克林顿和一只棕褐色的狗有共同的祖先。 查询解释器只输出Success! 如果它能证明这个论断是正确的。 作为一种副产品，它告诉我们共同祖先和棕褐色狗的名字： ``` (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 ``` 结果中显示的三个作业中的每一个都是一个更大的证据，证明在给定事实的情况下查询是正确的。完整的证据应该包括所有使用的事实，例如包括(父母亚伯拉罕·克林顿)和(父母菲尔莫尔·亚伯拉罕)。 ### 4.5.5 搜索 为了从系统中已经建立的事实建立查询，查询解释器在所有可能的事实空间中执行搜索。 联合是模式匹配两个表达式的基本操作。查询解释器中的搜索过程选择要联合的表达式，以便找到一组连接在一起以建立查询的事实。 递归搜索函数实现了逻辑语言的搜索过程。 它将查询中的子句的Scheme列表、包含符号到值的当前绑定(最初为空)的环境env和已经连接在一起的规则链的深度作为输入。 ``` >>> def search(clauses, env, depth): """Search for an application of rules to establish all the CLAUSES, non-destructively extending the unifier ENV. Limit the search to the nested application of DEPTH rules.""" 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来检查不可能存在这样的联合。 如果这个递归调用没有产生任何结果，则使用剩下的子句继续搜索过程。 如果联合是可能的，我们马上就失败了。 如果我们的第一个子句没有被否定，那么对于数据库中的每个事实，搜索尝试将事实的第一个子句与查询的第一个子句联合起来。 联合在一个新的环境env\_head中执行。 作为联合的副作用，变量被绑定到env\_head中的值。 如果联合成功，则该子句与当前规则的结论相匹配。 下面的for语句试图建立该规则的假设，从而得出结论。在这里，递归规则的假设将被递归地传递给搜索以建立。 最后，对于每一次成功的事实搜索。 第二，生成的环境被绑定到env\_rule。 给定这些值到变量的绑定，最后的for语句在初始查询中搜索以建立其余的子句。 任何成功的结果都通过内部yield语句返回。 **独特的名字。**联合的前提是e和f之间没有共享变量。然而，我们经常在逻辑语言的事实和查询中重用变量名。 我们不想把?x和?x混淆；这些变量不相关。为了确保名称不会混淆，在将事实传递到unify之前，它的变量名将使用rename\_variables替换为唯一的名称，并为事实附加一个唯一的整数。 ``` >>> def rename_variables(expr, n): """Rename all variables in EXPR with an identifier N.""" 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 ``` 其余的细节，包括逻辑语言的用户界面和各种helper函数的定义，出现在[逻辑示例](http://composingprograms.com/examples/logic/logic.py.html)中。