在逻辑和电脑科学中，合一（unification），是方程求解表达式之间方程的算法过程。例如，使用 x, y, z 作为变量，单元素集合解的方程{cons(x, cons(x, nil)) = cons(2, y)}是一个语法一阶合一问题，具有替换{x ↦ 2, y ↦ cons(2, nil)}作为其唯一解。
合一算法首先由雅克·埃尔布朗 ( [1] [2] [3]发现，而第一个正式研究可归因于John Alan Robinson[4] [5]，他使用一阶句法合一作为基本构建块他对一阶逻辑的归结过程的研究是自动推理技术的一大进步，因为它消除了组合爆炸的一个来源：搜索项目实例。如今，自动推理仍然是合一的主要应用领域。语法一阶合一用于逻辑编程和编程语言类型系统实现，特别是基于 Hindley-Milner 的类型推论算法。语义合一用于 SMT 求解器、重写逻辑算法和安全协议分析。高阶合一用于证明助手，例如 Isabelle 和 Twelf ，并且高阶合一的受限形式（高阶模式合一）用于某些编程语言实现，例如lambdaProlog，因为高阶模式具有表现力，但它们相关的合一过程保留了更接近一阶合一的理论属性。
例如，对于多项式 X2 和 Y3 可以通过采纳 X = Z3 和 Y = Z2 而合一到 Z6。
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
引用
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
