我正在尝试实施统一，但遇到问题......已经有很多例子，但他们所做的只是浑水。我比开明更困惑：
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解释让我更加困惑。
作为一个良好的开端，遵循基于列表的表示似乎是个好主意（例如在lispy情况下），即：
pred(Var, val) =becomes=> [pred, Var, val]
p1(val1, p2(val2, Var1)) ==> [p1, val1, [p2, val2, Var1]]
除了你如何表示自己的名单！即[H | T]
我很乐意，如果你能告诉我一个Python伪代码和/或更详细的算法描述或指向一个。
我掌握的一些要点是需要在通用 - 统一和变量统一中分离代码，但后来我无法看到相互背叛的情况！ ... 等等。
作为旁注：我也很乐意提到你如何处理Backtracking上的统一。我想我已经回归平方，但我知道在回溯时替换帧会发生一些事情。
添加了当前代码的答案。
http://www.igrok.site/bi/Bi_language.html
我将很快总结一下来自Unification Theory的Baader和Snyder关于Handbook of Automated Reasoning的章节：
术语是从常量（以小写字母开头）和变量（以大写字母开头）构建的：
cardate(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，一个unifier是一个替换，使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)可以通过应用unifier {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应用小于右侧，所以只要我们看到一个术语为有限结构，它们就不能相等。
我比开明更困惑
去过也做过。
注意：对于引用的任何源代码，我没有测试代码并且不能说它是有效的，它们作为示例给出并且看起来足够正确，我将加载它们并针对它们运行测试用例以确定它们的有效性。
第一：如果您使用正确的术语，您将获得更好的搜索结果，使用backward chaining而不是Backtracking。例如backward-chaining/inference.py
第二：了解您的问题列出了三个单独的阶段。 1.统一算法 2.使用统一的后向链接 3.列表的数据结构。您不会将其实现为Python源代码，而是将其作为要传递给函数的文本。见：cons
在进行反向链接之前，您应首先开发并完全测试统一。然后在创建列表数据结构之前完全开发并测试反向链接。然后完全测试您的列表数据结构。
第三：实现统一算法的方法不止一种。 一个。您注意到使用转换规则的那个，或者由Baader和Snyder在Unification Theory中记为基于规则的方法，例如：删除分解等 湾我更喜欢通过在这个OCaml Unification Theory或Python example中给出的Baader和Snyder在example中的递归下降统一的算法 C。我见过一些使用排列但目前找不到好的参考。
第四：根据个人经验，首先通过使用笔和纸来了解每个阶段的工作原理，然后在代码中实现它。
第五：同样从个人经验来看，有很多关于如何做到这一点的信息，但是数学和技术论文可能会让人感到困惑，因为许多人对自学者至关重要的东西有所掩盖。我建议您专注于查找源代码/数据结构的实现并使用它来学习。
第六：将您的结果与实际工作代码进行比较，例如： SWI-Prolog。
在进入下一阶段之前，我不能强调你需要多少测试每个阶段，并确保你拥有一套完整的测试用例。
当我想学习如何用函数式语言编写这本书时，有关AI 1 2 3和The Programming Languages Zoo的书籍非常宝贵。不得不为Lisp和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