合一

维基百科，自由的百科全书

本文有关计算机科学主题。其他学科的条目参见合一 (消歧义)。

在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并(格的最小上界), 就是说，我们在项的集合上假定一个预序，其中 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 中，这种操作用符号 "=" 来指示。

1. 在传统 Prolog 中，未实例化的变量 X — 就是说在它上面以前没有进行合一，可以合一于一个原子、一个项、或另一个未实例化的变量，因此在效果上变成了它的别名。在很多现代 Prolog 方言和一阶逻辑演算中，变量不能合一于包含它的项；这叫做出现检查。
2. Prolog 原子只能合一于同一个原子。
3. 类似的，项只能合一于另一个项，如果顶部函数符号和项的元数(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.