统一的应用？

统一的(实际)应用是什么？它实际上在现实世界中使用的地方？

我无法理解它的真正含义以及为什么它被视为人工智能的一部分.

统一本质上是一种替代过程.我看到它被称为"双向匹配".

在Prolog中,在其他逻辑编程语言和直接基于重写逻辑的语言(Maude,Elan等等)中,自由(逻辑)变量与术语/值绑定的机制.在Concurrent Prolog中,这些变量被解释为通信通道.

IMO,理解它的更好方法是使用数学的一些例子(统一是/是基本的关键机制,例如,在自动定理证明研究的背景下,AI的子领域;在类型推理算法中的另一种用途).以下示例取自计算机代数系统(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|

(lhs of | 5 |统一为| 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|

等等.

(希望我没有任何错误,否则这可能会使初学者更加困惑.)

统一是类型推断的关键机制.实际上,在这种情况下统一将大大减少手指的磨损.