统一的应用？

Question

Unification的(实际)应用是什么？它在现实世界中的实际应用是什么？

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

Answer 1

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

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

国际海事组织，理解它的更好的方法是用一些数学例子(统一曾经/是一个基本的关键机制，例如，在自动定理证明器研究的上下文中，AI的一个子领域；在type inference algorithms中的另一个用途)。下面的示例取自computer algebra systems (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|

诸若此类。

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

Answer 2

统一是type inference中的一个关键机制。实际上，在这种情况下的统一将极大地减少您手指的磨损。

Answer 3

例如，Prolog使用统一来查找满足规则的变量的值-有关示例，请参阅this explanation。我希望这是逻辑编程语言中的一种典型技术，尽管我没有使用其他语言的经验。