在Python中实现Prolog Unification算法？回溯

Question

在Python中实现Prolog Unification算法？回溯

pythonalgorithmprologbacktrackingunification

12

我正在尝试实现统一，但遇到了问题。虽然已经有了许多例子，但它们只是使问题更加混乱。我感到越来越困惑而不是受到启发：

http://www.cs.trincoll.edu/~ram/cpsc352/notes/unification.html

https://www.doc.ic.ac.uk/~sgc/teaching/pre2012/v231/lecture8.html [以下代码基于此介绍]

http://www.cs.bham.ac.uk/research/projects/poplog/paradigms_lectures/lecture20.html#representing

https://norvig.com/unify-bug.pdf

如何在Java或C#等语言中实现统一算法？

Prolog编程艺术以及其他一些书籍中都涉及到了统一算法。最大的问题在于我无法理清问题的明确陈述。更数学化或Lisp式的解释只会让我更加困惑。

作为一个很好的开始，似乎按照列表表示法进行编码是个好主意（就像Lisp中的情况一样），即：

pred(Var, val)  =becomes=> [pred, Var, val] 
p1(val1, p2(val2, Var1)) ==> [p1, val1, [p2, val2, Var1]]

除了如何表示列表本身之外，还有什么问题吗？即 [H|T]。我希望你能展示一些Python伪代码和/或更详细的算法描述，或者指向一个这样的资源。我理解的一些要点是需要将代码分为一般统一器和变量统一器，但我看不到相互递归的情况！等等。

作为一个附注：我也希望你能提及如何处理回溯的统一化。我认为我已经掌握了回溯，但我知道在回溯时替换框架需要进行某些操作。

添加了一个包含当前代码的答案。

http://www.igrok.site/bi/Bi_language.html

http://www.igrok.site/bi/TOC.html

https://github.com/vsraptor/bi/blob/master/lib/bi_engine.py

- sten

2

Prolog列表只是列表构造器“.”和空列表“[]”的语法糖。列表“[a，b，c]”等同于“[a | [b | [c | []]]]”。列表构造器“|”本身是二元函数符号“.”的语法糖。在内部，列表“[a，b，c]”看起来像“.(a，.(b，.(c，[])))”。在概念层面上，Prolog列表与其他术语没有不同的统一性。顺便说一句，在Lisp中，构造器“.”称为“cons”，空列表“[]”称为“NIL”。 - lambda.xy.x

2

to [a | [b | [c | [] ]]] - false

感兴趣的内容：PROLOG解释器的设计和实现。虽然这是用Pascal完成的，但作为Prolog任何实现方式的示例，其中许多概念仍然具有相关性。 - Guy Coder

3个回答

7

我感到比受启发更加困惑

已经有过这样的经历了。

注意：对于任何引用的源代码，我没有测试代码并且无法确认其有效性，它们仅作为示例提供，并且看起来足够正确，我会加载它们并运行测试用例以确定其有效性。

首先：如果您使用正确的术语，例如使用backward chaining而不是Backtracking，您将获得更好的搜索结果。例如backward-chaining/inference.py

第二：请理解您的问题列出了三个独立的阶段。
1. 合一算法
2. 使用合一的反向链接
3. 一个列表的数据结构。您不需要将其实现为Python源代码，而是作为要传递给函数的文本。请参见：cons

在进行反向链接之前，您应该首先开发并完全测试统一。然后在创建列表数据结构之前充分开发和测试反向链接。然后充分测试您的列表数据结构。

第三点：实现合一算法有不止一种方法。
a. 你提到了使用转换规则的方法，或者在Baader和Snyder的合一理论中被称为基于规则的方法，例如删除、分解等。
b. 我更喜欢在Baader和Snyder的合一理论中被称为递归下降合一的算法，在这个OCaml 示例或Python 示例中给出。
c. 我见过一些使用排列的方法，但目前找不到好的参考资料。

第四步：从个人经验中，先使用纸笔理解每个阶段的工作原理，然后再将其实现在代码中。 第五步：同样来自个人经验，有很多关于如何做到这一点的信息，但数学和技术论文可能会让自学者感到困惑，因为它们往往忽略了一些关键问题或过于密集。我建议你重点寻找源代码/数据结构的实现，并利用它来学习。 第六步：将你的结果与实际的工作代码进行比较，例如SWI-Prolog。

我无法强调测试每个阶段的重要性，确保你拥有完整的测试案例，然后再进入下一个阶段。

当我想学习如何使用函数式语言编写这个程序时，AI方面的书籍1 2 3和The Programming Languages Zoo非常有价值。虽然需要安装Lisp和OCaml的环境，但这样做是值得的。

- Guy Coder

谢谢。我需要重新读几遍。我已经开始按照你说的建立测试套件，修复了一些错误，我的当前版本（尚未发布）可以处理我能想到的每种情况。你说得对，与SWI进行比较有帮助。 - sten

我指的是回溯，也就是当推理链中的一个术语失败时，您如何解开反一致性！ - sten

当一个目标失败时，它不应该释放所有初始化的绑定吗！？ - sten

1

使用排列算法的可能性是采用显式代换 / λσ演算吗？ - lambda.xy.x

3

使用回溯算法时，请注意您正在操作实现的不同部分。假设您有一个规则p(X)：- q(X)。和一个目标p(a)。通过一致性，您将发现必须应用统一器a/X，将规则实例化为p(a)：- q(a)。并将q(a)作为新目标。如果此路径失败，则可以遵循头部一致的不同规则。保存此撤消信息的经典数据结构是堆栈（或在函数式编程中是累加器）。 - lambda.xy.x

0

到目前为止，这对我想到的所有情况都有效（除了一个需要出现检查的情况，我还没有做）：

def unify_var(self, var, val, subst):
#   print "var> ", var, val, subst

    if var in subst :   
        return self.unify(subst[var], val, subst)
    elif isinstance(val, str) and val in subst : 
        return self.unify(var, subst[val], subst)
    #elif (var occurs anywhere in x) then return failure
    else :
        #print "%s := %s" % (var, val)
        subst[var] = val ; return subst

def unify(self, sym1, sym2, subst):
    #print 'unify>', sym1, sym2, subst

    if subst is False : return False
    #when both symbols match
    elif isinstance(sym1, str) and isinstance(sym2, str) and sym1 == sym2 : return subst
    #variable cases
    elif isinstance(sym1, str) and is_var(sym1) : return self.unify_var(sym1, sym2, subst)
    elif isinstance(sym2, str) and is_var(sym2) : return self.unify_var(sym2, sym1, subst)
    elif isinstance(sym1, tuple) and isinstance(sym2, tuple) : #predicate case
        if len(sym1) == 0 and len(sym2) == 0 : return subst
        #Functors of structures have to match
        if isinstance(sym1[0], str) and  isinstance(sym2[0],str) and not (is_var(sym1[0]) or is_var(sym2[0])) and sym1[0] != sym2[0] : return False
        return self.unify(sym1[1:],sym2[1:], self.unify(sym1[0], sym2[0], subst))
    elif isinstance(sym1, list) and isinstance(sym2, list) : #list-case
        if len(sym1) == 0 and len(sym2) == 0 : return subst
        return self.unify(sym1[1:],sym2[1:], self.unify(sym1[0], sym2[0], subst))

    else: return False

FAIL cases应该失败：

OK: a <=> a : {}
OK: X <=> a : {'X': 'a'}
OK: ['a'] <=> ['a'] : {}
OK: ['X'] <=> ['a'] : {'X': 'a'}
OK: ['a'] <=> ['X'] : {'X': 'a'}
OK: ['X'] <=> ['X'] : {}
OK: ['X'] <=> ['Z'] : {'X': 'Z'}
OK: ['p', 'a'] <=> ['p', 'a'] : {}
OK: ['p', 'X'] <=> ['p', 'a'] : {'X': 'a'}
OK: ['p', 'X'] <=> ['p', 'X'] : {}
OK: ['p', 'X'] <=> ['p', 'Z'] : {'X': 'Z'}
OK: ['X', 'X'] <=> ['p', 'X'] : {'X': 'p'}
OK: ['p', 'X', 'Y'] <=> ['p', 'Y', 'X'] : {'X': 'Y'}
OK: ['p', 'X', 'Y', 'a'] <=> ['p', 'Y', 'X', 'X'] : {'Y': 'a', 'X': 'Y'}
 ================= STRUCT cases ===================
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('p', 'a')] : {'X': 'Y'}
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('p', 'Z')] : {'X': 'Y', 'Z': 'a'}
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('P', 'Z')] : {'X': 'Y', 'Z': 'a', 'P': 'p'}
OK: [('p', 'a', 'X')] <=> [('p', 'Y', 'b')] : {'Y': 'a', 'X': 'b'}
OK: ['X', 'Y'] <=> [('p', 'a'), 'X'] : {'Y': ('p', 'a'), 'X': ('p', 'a')}
OK: [('p', 'a')] <=> ['X'] : {'X': ('p', 'a')}
-----
FAIL: ['e', 'X', ('p1', 'a')] <=> ['e', 'Y', ('p2', 'Z')] : False
FAIL: ['e', 'X', ('p1', 'a')] <=> ['e', 'Y', ('p1', 'b')] : False
FAIL: [('p', 'a', 'X', 'X')] <=> [('p', 'a', 'a', 'b')] : False
(should fail, occurs) OK: [('p1', 'X', 'X')] <=> [('p1', 'Y', ('p2', 'Y'))] : {'Y': ('p2', 'Y'), 'X': 'Y'}
================= LIST cases ===================
OK: ['e', 'X', ['e', 'a']] <=> ['e', 'Y', ['e', 'a']] : {'X': 'Y'}
OK: ['e', 'X', ['a', 'a']] <=> ['e', 'Y', ['a', 'Z']] : {'X': 'Y', 'Z': 'a'}
OK: ['e', 'X', ['e', 'a']] <=> ['e', 'Y', ['E', 'Z']] : {'X': 'Y', 'Z': 'a', 'E': 'e'}
OK: ['e', 'X', ['e1', 'a']] <=> ['e', 'Y', ['e1', 'a']] : {'X': 'Y'}
OK: [['e', 'a']] <=> ['X'] : {'X': ['e', 'a']}
OK: ['X'] <=> [['e', 'a']] : {'X': ['e', 'a']}
================= FAIL cases ===================
FAIL: ['a'] <=> ['b'] : False
FAIL: ['p', 'a'] <=> ['p', 'b'] : False
FAIL: ['X', 'X'] <=> ['p', 'b'] : False

- sten

2

如果你从其他地方复制了代码，或者你的代码与复制的代码非常相似，那么你需要引用它，以便人们知道这一点。此外，这并不是真正的答案，应该作为问题的更新包含在内。 - Guy Coder

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- lambda.xy.x · Accepted Answer

我将快速概述Baader和Snyder在《自动推理手册》中关于统一理论的章节：

术语由常量（以小写字母开头）和变量（以大写字母开头）构建：

没有参数的常量是术语：例如car
带有术语作为参数的常量，即所谓的函数应用，是一个术语。例如date(1,10,2000)
变量是一个术语，例如Date（变量永远不带参数）

替换是将术语分配给变量的映射。在文献中，这通常写作{f(Y)/X, g(X)/Y}或带有箭头的形式{X→f(Y), Y→g(X)}。将替换应用于术语会将列表中的每个变量替换为相应的术语。例如，上面的替换应用于tuple(X,Y)会得到术语tuple(f(Y),g(X))。

给定两个项 s 和 t，一个统一器是一种替换，使得s和t相等。例如，如果我们对术语date(X,1,2000)应用替换{a/X，a/Y}，我们得到date(a,1,2000)，如果我们把它应用到date(Y,1,2000)上，我们也得到date(a,1,2000)。换句话说，（句法）相等性date(X,1,2000) = date(Y,1,2000)可以通过应用统一器{a/X，a/Y}来解决。另一个更简单的统一器是X/Y。这样的最简单的统一器被称为最一般统一器。对于我们的目的，我们只需要知道我们可以限制自己在搜索这样一个最一般的统一器，并且如果存在，它是唯一的（除了某些变量的名称）。

Mortelli 和 Montanari（见文章的第2.2节和参考文献）给出了一组规则来计算最通用的统一器（如果存在）。输入是一组术语对（例如 { f(X,b) = f(a,Y), X = Y } ），输出是最通用的统一器（如果存在）或失败（如果不存在）。在这个例子中，替换 {a/X, b/Y} 可以使第一对相等 (f(a,b) = f(a,b))，但是接下来的第二对不相等 (a = b 不成立)。

算法从集合中非确定地选择一个等式，并对其应用以下规则之一：

平凡情况：方程 s = s（或 X=X）已经相等，可以安全地删除。
分解：等式 f(u,v) = f(s,t) 被替换为等式 u=s 和 v=t。
符号冲突：等式 a=b 或 f(X) = g(X) 以失败结束。
定向：形如 t=X 的等式，其中 t 不是另一个变量，则翻转为 X=t，使变量在左侧。
出现检查：如果方程式的形式为 X=t，t 不是 X 本身，并且如果 X 在 t 中的某个位置出现，则失败。[1]
变量消除：如果我们有一个方程 X=t，其中 X 不出现在 t 中，我们可以将替换 t/X 应用于所有其他问题。

当没有规则可应用时，我们最终得到一组方程式{X=s，Y=t，...}，表示要应用的替换。

以下是更多示例：

{f(a,X) = f(Y,b)}是可统一的：分解得到{a=Y，X=b}并翻转得到{Y=a，X=b}
{f(a,X,X) = f(a,a,b)}不可统一：分解得到{a=a，X=a，X=b}，通过平凡性消除a=a，然后消除变量X以得到{a=b}并因符号冲突而失败
{f(X,X) = f(Y,g(Y))}不可统一：分解得到{X=Y，X=g(Y)}，消除变量X以得到{Y=g(Y)}，因出现检查而失败

尽管算法是非确定性的（因为我们需要选择一个等式来处理），但顺序并不重要。因为你可以承诺任何顺序，所以永远不必撤消你的工作并尝试使用另一个方程。这种技术通常称为回溯，在Prolog中进行证明搜索时是必需的，但对于统一本身则不是。

现在你只需要选择一个适合的术语和替换数据结构，并实现应用替换到术语的算法以及基于规则的统一算法。

[1] 如果我们尝试解决X = f(X)，我们会发现X需要是f(Y)的形式才能应用分解。这导致解决问题f(Y) = f(f(Y))，随后是Y = f(Y)。由于左侧始终比右侧少一个f的应用，只要我们将术语视为有限结构，它们就不能相等。