python - 在 Python 中实现 Prolog 统一算法？回溯

Question

我正在尝试实现统一，但遇到了问题......已经有十几个例子，但他们所做的只是把水搅浑。我比开明更困惑:

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

How can I implement the unification algorithm in a language like Java or C#?

Prolog 的艺术之一......和其他几个。
最大的问题是我无法清楚地说明问题。更多的数学或繁琐的解释让我更加困惑。

作为一个好的开始，遵循基于列表的表示(如在 lispy 情况下)似乎是个好主意，即:

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

except how do you represent lists themselves !? i.e. [H|T]

如果您能向我展示 Python 伪代码和/或更详细的算法描述或指向某个算法的指针，我会很高兴。

我掌握的一些要点是需要将general-unifier和var-unification中的代码分开，但是我看不到相互递归的情况! ... 等等。

作为旁注:我也很想请您提及您将如何处理回溯统一。我想我有回溯平方，但我知道在回溯时替换框架必须发生一些事情。

添加了当前代码的答案。

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

Answer 1

我将快速总结关于Unification Theory的章节来自 Handbook of Automated Reasoning 的 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平等的。例如。如果我们应用替换 {a/X, a/Y}到术语 date(X,1,2000) ，我们得到 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)} , 失败并发生检查

即使算法是不确定的(因为我们需要选择一个等式来处理)，顺序并不重要。因为您可以 promise 任何订单，所以永远没有必要撤消您的工作并尝试不同的等式。这种技术通常称为回溯，对于 Prolog 中的证明搜索是必需的，但不是统一本身。

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

[1] 如果我们尝试解决 X = f(X) ，我们会看到 X 需要采用 f(Y) 的形式应用分解。这导致解决问题f(Y) = f(f(Y))随后 Y = f(Y) .由于左侧总是有一个应用程序 f小于右侧，只要我们将项视为有限结构，它们就不能相等。