合一（Unification）有哪些（实际的）应用？它在现实世界中实际被用在哪里？

我不太理解它到底是什么，以及为什么它被认为是人工智能的一部分。

回答：

合一本质上是一个替换的过程。我见过它被称为“双向匹配”。

在 Prolog，其他逻辑编程语言，以及直接基于重写逻辑的语言（Maude, Elan, 等等…）中，合一是将自由（逻辑）变量绑定到项/值的机制。在并发 Prolog 中，这些变量被解释为通信通道。

我认为，理解它的更好方法是使用一些数学例子（合一曾经/现在都是一个基础的关键机制，例如，在自动化定理证明器研究的上下文中，它是人工智能的一个子领域；另一个用途是在类型推断算法中）。下面的例子取自计算机代数系统 (CAS)：

第一个例子：

给定一个集合 Q，以及其上的两个二元运算 * 和 +，如果满足以下条件，则 * 对 + 具有左分配律：

X * (Y + Z)   =   (X * Y) + (X * Z)   |1|

这是一个重写规则（一组重写规则是一个重写系统）。

如果我们想将此重写规则应用于一个特定情况，例如：

a * (1 + b)   |2|

我们将这个项 |2| 与 |1| 的左侧（lhs）合一（通过合一算法），我们得到这个（故意设计的）平凡的替换（最一般合一器，mgu）：

{X/a, Y/1, Z/b}   |3|

现在，将 |3| 应用于 |1| 的右侧（rhs），我们最终得到：

(a * 1) + (a * b)

这很简单，为了让你体会合一的作用，我将展示一个稍微复杂的例子。

第二个例子：

给定这个重写规则：

log(X,Y) + log(X,Z)   =>   log(X,Y*Z)   |4|

我们将其应用于这个等式：

log(e,(x+1)) + log(e,(x-1)) = k   |5|

（|5| 的 *lhs* 与 |4| 的 *lhs* 合一），所以我们有这个 *mgu*：

{X/e, Y/(x+1), Z/(x-1)}   |6|

请注意，X 和 x 是两个不同的变量。这里我们有两个变量 X 和 Y，它们匹配两个 复合项，(x+1) 和 (x-1)，而不是简单的值或变量。

我们将这个 *mgu*，|6|，应用于 |4| 的 *rhs*，然后将其放回 |5| 中；所以我们有：

log(e,(x+1)*(x-1)) = k   |7|

等等。

（希望我没有犯任何错误，否则可能会让新手更加困惑。）