Prolog 中的合一

同一概念是在Prolog背后的主要想法。它表示绑定变量的内容的机制并可以看作为一种只一次的(one-time)赋值。在 Prolog 中，这种操作用符号 "=" 来指示。

在传统 Prolog 中，未实例化的变量X — 就是说在它上面以前没有进行合一，可以合一于一个原子、一个项、或另一个未实例化的变量，因此在效果上变成了它的别名。在很多现代 Prolog 方言和一阶逻辑演算中，变量不能合一于包含它的项；这叫做出现检查。

Prolog 原子只能合一于同一个原子。

类似的，项只能合一于另一个项，如果顶部函数符号和项的元数(arity)和这个项是一样的，并且参数可以同时合一。注意这是递归行为。

由于它的声明本性，一序列合一的次序(通常)是不重要的。

注意在一阶逻辑的术语中，原子是基本命题而且其合一同 Prolog 项一样。

合一的例子

A = A : 成功(重言式)

A = B, B = abc : A 和 B 二者合一于原子 abc

xyz = C, C = D : 合一是对称的

abc = abc : 合一成功

abc = xyz : 合一失败，因为原子是不同的

f(A) = f(B) : A 合一于 B

f(A) = g(B) : 失败，因为项的头部是不同的

f(A) = f(B, C) : 合一失败，因为项有不同的元数

f(g(A)) = f(B) : B 合一于项 g(A)

f(g(A), A) = f(B, xyz) : A 合一于原子 xyz 而 B 合一于项 g(xyz)

A = f(A) : 无限合一， A 合一于 f(f(f(f(...))))。在严格的一阶逻辑和很多现代 Prolog 方言中，这是禁止的(并由出现检查来强制)

A = abc, xyz = X, A = X : 合一失败； 效果上 abc = xyz

引用

F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.

F. Baader and W. Snyder, Unification Theory. In J.A. Robinson and A. Voronkov, editors,Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001.

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。