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函数的定义，出现在逻辑示例中。

Previous4.4 逻辑编程Next4.6 分布式计算

Last updated

Was this helpful?