在 Python 中实现 Prolog 统一算法？回溯
Implementing the Prolog Unification algorithm in Python? Backtracking
我正在尝试实现统一，但遇到了问题.. 已经有很多例子，但他们所做的只是把水搅浑。我比开悟更困惑：
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 伪代码 and/or 更详细的算法描述或指向一个的指针，我会很高兴。
我掌握的一些要点是需要将general-unifier和var-unification中的代码分开，但是我看不到相互递归的情况！ ...等等。
作为旁注：我也希望您提及您将如何处理回溯统一。我想我有回溯平方，但我知道回溯的替换框架必须发生一些事情。
使用当前代码添加了答案。
http://www.igrok.site/bi/Bi_language.html
关于Unification Theory by Baader and Snyder from the Handbook of Automated Reasoning的章节我会快速总结一下：
术语 由常量（以小写字母开头）和变量（以大写字母开头）构成：
- 没有参数的常量是一个术语：例如
car
- 以项为参数的常量，即所谓的函数应用，是一个项。例如
date(1,10,2000)
- 一个变量是一个术语，例如
Date（变量永远没有参数）
A substitution 是将项分配给变量的映射。在文献中，这通常写为 {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}，失败符号clash{f(X,X) = f(Y,g(Y))} 不可统一：
分解得到 {X=Y, X=g(Y)}，消除变量 X 得到 {Y=g(Y)}，失败并发生检查
即使算法是 non-deterministic（因为我们需要选择一个等式来处理），顺序并不重要。因为您可以接受任何订单，所以永远没有必要撤消您的工作并尝试使用不同的方程式。这种技术通常称为回溯，对于 Prolog 中的证明搜索是必需的，但对于统一本身不是必需的。
现在您只需为术语和替换选择合适的 data-structure，并实施将替换应用于术语的算法以及基于规则的统一算法。
[1] 如果我们尝试求解 X = f(X)，我们会发现 X 需要采用 f(Y) 形式才能应用分解。这导致解决问题 f(Y) = f(f(Y)) 和随后的 Y = f(Y)。由于左侧总是比右侧少一个 f 的应用，所以只要我们将项视为有限结构，它们就不可能相等。
I get more confused than enlightened
去过那里，做到了。
注意：对于任何引用的源代码，我都没有测试代码，不能说它是有效的，它们是作为示例给出的，看起来足够正确，我会加载它们和 运行 测试用例反对他们以确定其有效性。
首先：如果使用正确的术语，您将获得更好的搜索结果，请使用backward chaining instead of Backtracking. e.g. backward-chaining/inference.py
第二：了解您的问题列出了三个单独的阶段。
1.统一算法
2. 使用 Unification
的反向链接
3. 列表的数据结构。您不会将此实现为 Python 源代码，而是作为要传递给您的函数的文本。参见：cons
在转向反向链接之前，您应该首先开发并全面测试统一。然后在创建列表数据结构之前充分开发和测试反向链接。然后全面测试你的列表数据结构。
第三：统一算法的实现方式不止一种
一种。您注意到使用转换规则的方法，或者在 Baader 和 Snyder 的 Unification Theory 中被称为 A rule based approach，例如删除 分解等
b.我更喜欢 Baader 和 Snyder 在这个 OCaml example 或 Python 中给出的算法 Unification by recursive descent in Unification Theory ] 例子
C。我看过一些使用排列但目前找不到好的参考。
第四：根据个人经验，先用笔和纸了解每个阶段的工作原理，然后用代码实现。
第五：再次从个人经验来看，有很多关于如何做到这一点的信息，但数学和技术论文可能会令人困惑，因为许多掩盖了一些关键的东西a self-learner 或太密集。我建议您改为专注于查找源 code/data 结构的实现并使用它来学习。
第六：将您的结果与实际工作代码进行比较，例如SWI-Prolog.
在进入下一个阶段之前，每个阶段需要进行多少测试，并确保您拥有一套完整的测试用例。
当我想学习如何用函数式语言编写此代码时，阅读了关于 AI 的书籍 1 2 3 and The Programming Languages Zoo were invaluable. Had to install environments for Lisp and OCaml 但值得付出努力。
到目前为止，这适用于我提出的所有情况（除了需要发生检查的情况，我还没有这样做）：
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 案例应该失败：
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
我正在尝试实现统一，但遇到了问题.. 已经有很多例子，但他们所做的只是把水搅浑。我比开悟更困惑：
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 伪代码 and/or 更详细的算法描述或指向一个的指针，我会很高兴。
我掌握的一些要点是需要将general-unifier和var-unification中的代码分开，但是我看不到相互递归的情况！ ...等等。
作为旁注：我也希望您提及您将如何处理回溯统一。我想我有回溯平方，但我知道回溯的替换框架必须发生一些事情。
使用当前代码添加了答案。
http://www.igrok.site/bi/Bi_language.html
关于Unification Theory by Baader and Snyder from the Handbook of Automated Reasoning的章节我会快速总结一下：
术语 由常量（以小写字母开头）和变量（以大写字母开头）构成：
- 没有参数的常量是一个术语：例如
car - 以项为参数的常量，即所谓的函数应用，是一个项。例如
date(1,10,2000) - 一个变量是一个术语，例如
Date（变量永远没有参数）
A substitution 是将项分配给变量的映射。在文献中，这通常写为 {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}，失败符号clash{f(X,X) = f(Y,g(Y))}不可统一： 分解得到{X=Y, X=g(Y)}，消除变量X得到{Y=g(Y)}，失败并发生检查
即使算法是 non-deterministic（因为我们需要选择一个等式来处理），顺序并不重要。因为您可以接受任何订单，所以永远没有必要撤消您的工作并尝试使用不同的方程式。这种技术通常称为回溯，对于 Prolog 中的证明搜索是必需的，但对于统一本身不是必需的。
现在您只需为术语和替换选择合适的 data-structure，并实施将替换应用于术语的算法以及基于规则的统一算法。
[1] 如果我们尝试求解 X = f(X)，我们会发现 X 需要采用 f(Y) 形式才能应用分解。这导致解决问题 f(Y) = f(f(Y)) 和随后的 Y = f(Y)。由于左侧总是比右侧少一个 f 的应用，所以只要我们将项视为有限结构，它们就不可能相等。
I get more confused than enlightened
去过那里，做到了。
注意：对于任何引用的源代码，我都没有测试代码，不能说它是有效的，它们是作为示例给出的，看起来足够正确，我会加载它们和 运行 测试用例反对他们以确定其有效性。
首先：如果使用正确的术语，您将获得更好的搜索结果，请使用backward chaining instead of Backtracking. e.g. backward-chaining/inference.py
第二：了解您的问题列出了三个单独的阶段。
1.统一算法
2. 使用 Unification
的反向链接
3. 列表的数据结构。您不会将此实现为 Python 源代码，而是作为要传递给您的函数的文本。参见：cons
在转向反向链接之前，您应该首先开发并全面测试统一。然后在创建列表数据结构之前充分开发和测试反向链接。然后全面测试你的列表数据结构。
第三：统一算法的实现方式不止一种
一种。您注意到使用转换规则的方法，或者在 Baader 和 Snyder 的 Unification Theory 中被称为 A rule based approach，例如删除 分解等
b.我更喜欢 Baader 和 Snyder 在这个 OCaml example 或 Python 中给出的算法 Unification by recursive descent in Unification Theory ] 例子
C。我看过一些使用排列但目前找不到好的参考。
第四：根据个人经验，先用笔和纸了解每个阶段的工作原理，然后用代码实现。
第五：再次从个人经验来看，有很多关于如何做到这一点的信息，但数学和技术论文可能会令人困惑，因为许多掩盖了一些关键的东西a self-learner 或太密集。我建议您改为专注于查找源 code/data 结构的实现并使用它来学习。
第六：将您的结果与实际工作代码进行比较，例如SWI-Prolog.
在进入下一个阶段之前，每个阶段需要进行多少测试，并确保您拥有一套完整的测试用例。
当我想学习如何用函数式语言编写此代码时，阅读了关于 AI 的书籍 1 2 3 and The Programming Languages Zoo were invaluable. Had to install environments for Lisp and OCaml 但值得付出努力。
到目前为止，这适用于我提出的所有情况（除了需要发生检查的情况，我还没有这样做）：
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 案例应该失败：
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