合一

在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并(格的最小上界), 就是说，我们在项的集合上假定一个预序，其中 t* ≤ t 意味着 t* 是通过代换(substitute)在 t 中某些项的一个或多个自由变量而从 t 获得的。s 和 t 的同一 u，如果存在的话，是 s 和 t 二者的代换实例的一个项。s 和 t 的任何公共的代换实例也是 u 的实例。

例如，对于多项式 X² 和 Y³ 可以通过采纳 X = Z³ 和 Y = Z² 而同一到 Z⁶。

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.