我将快速总结这一章统一论 https://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf巴德尔和斯奈德来自自动推理手册 https://www.sciencedirect.com/science/book/9780444508133:
Terms由常量（以小写字母开头）和变量（以大写字母开头）构建：
- 没有参数的常量是一个术语：例如
car
- 以项作为参数的常量，即所谓的函数应用，是项。例如
date(1,10,2000)
- 变量是一个术语，例如
Date（变量从来没有参数）
A 代换是一个将项分配给变量的映射。在文献中，这通常被写为{f(Y)/X, g(X)/Y}或用箭头{X→f(Y), Y→g(X)}。对术语应用替换会将每个变量替换为列表中相应的术语。例如。上述替换适用于tuple(X,Y)学期结果tuple(f(Y),g(X)).
给定两个术语s and t, a unifier是一个替代，使得s and 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 (or X=X) 已经相等并且可以安全地删除。
- 分解：等式
f(u,v) = f(s,t)被等式取代u=s and v=t.
- 符号冲突：平等
a=b or f(X) = g(X)进程失败而终止。
- 东方：形式的平等
t=X where t不是另一个变量被翻转到X=t使得变量位于左侧。
- 发生检查：方程是否具有以下形式
X=t, t is not X本身和如果X发生在某处t，我们失败了。 [1]
- 变量消除：我们有一个方程
X=t where 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 to get {a=b}并因符号冲突而失败
-
{f(X,X) = f(Y,g(Y))}不统一：
分解得到{X=Y, X=g(Y)}，消除变量X to get {Y=g(Y)}，失败并发生检查
尽管该算法是不确定的（因为我们需要选择一个等式来处理），但顺序并不重要。因为您可以承诺任何订单，所以无需撤消您的工作并尝试不同的方程式。这种技术通常称为回溯，对于 Prolog 中的证明搜索是必需的，但对于统一本身来说不是必需的。
现在，您只需为术语和替换选择合适的数据结构，并实现将替换应用于术语的算法以及基于规则的统一算法。
[1] 如果我们尝试解决X = f(X)，我们会看到 X 需要采用以下形式f(Y)应用分解。这会导致解决问题f(Y) = f(f(Y))随后Y = f(Y)。由于左侧总是有一个应用程序f小于右侧，只要我们将一项视为有限结构，它们就不能相等。
