合一
维基百科,自由的 encyclopedia
在逻辑和计算机科学中,合一(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),因为高阶模式具有表现力,但它们相关的合一过程保留了更接近一阶合一的理论属性。
例如,对于多项式 X2 和 Y3 可以通过采纳 X = Z3 和 Y = Z2 而合一到 Z6。