合一

在逻辑和计算机科学中，合一（unification），是方程求解表达式之间方程的算法过程。例如，使用 x, y, z 作为变量，单元素集合解的方程{cons(x, cons(x, nil)) = cons(2, y)}是一个语法一阶合一问题，具有替换{x ↦ 2, y ↦ cons(2, nil)}作为其唯一解。

合一算法首先由雅克·埃尔布朗 ( ^[1] ^[2] ^[3]发现，而第一个正式研究可归因于John Alan Robinson（英语：John Alan Robinson）^[4] ^[5]，他使用一阶句法合一作为基本构建块他对一阶逻辑的归结过程的研究是自动推理技术的一大进步，因为它消除了组合爆炸（英语：Combinatorial explosion）的一个来源：搜索项目实例。如今，自动推理仍然是合一的主要应用领域。语法一阶合一用于逻辑编程和编程语言类型系统实现，特别是基于 Hindley-Milner 的类型推论算法。语义合一用于 SMT 求解器、重写逻辑算法和安全协议分析。高阶合一用于证明助手，例如 Isabelle 和 Twelf ，并且高阶合一的受限形式（高阶模式合一）用于某些编程语言实现，例如lambdaProlog（英语：λProlog），因为高阶模式具有表现力，但它们相关的合一过程保留了更接近一阶合一的理论属性。

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

Prolog 中的合一的解释

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

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

^ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.
^ Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier. Lectures on Jacques Herbrand as a Logician (SEKI Report). 2009. arXiv:0902.4682  . |number=被忽略 (帮助)Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Lectures on Jacques Herbrand as a Logician (SEKI Report). DFKI. arXiv:0902.4682. Here: p.56
^ Jacques Herbrand. Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis论文). [2024-01-28]. （原始内容存档 (PDF)于2023-12-02）. Jacques Herbrand (1930). Recherches sur la théorie de la demonstration （页面存档备份，存于互联网档案馆） (PDF) (Ph.D. thesis). A. Vol. 1252. Université de Paris. Here: p.96-97
^ J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. Jan 1965, 12 (1): 23–41. S2CID 14389185. doi:10.1145/321250.321253  . J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32
^ J.A. Robinson. Computational logic: The unification computation. Machine Intelligence. 1971, 6: 63–72. J.A. Robinson (1971). "Computational logic: The unification computation" （页面存档备份，存于互联网档案馆）. Machine Intelligence. 6: 63–72.

[1] J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.

[2] Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier. Lectures on Jacques Herbrand as a Logician (SEKI Report). 2009. arXiv:0902.4682  . |number=被忽略 (帮助)Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Lectures on Jacques Herbrand as a Logician (SEKI Report). DFKI. arXiv:0902.4682. Here: p.56

[3] Jacques Herbrand. Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis论文). [2024-01-28]. （原始内容存档 (PDF)于2023-12-02）. Jacques Herbrand (1930). Recherches sur la théorie de la demonstration （页面存档备份，存于互联网档案馆） (PDF) (Ph.D. thesis). A. Vol. 1252. Université de Paris. Here: p.96-97

[Robinson.1965-4] J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. Jan 1965, 12 (1): 23–41. S2CID 14389185. doi:10.1145/321250.321253  . J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32

[5] J.A. Robinson. Computational logic: The unification computation. Machine Intelligence. 1971, 6: 63–72. J.A. Robinson (1971). "Computational logic: The unification computation" （页面存档备份，存于互联网档案馆）. Machine Intelligence. 6: 63–72.

[1]

[2]

[3]

[4]

[5]