合一算法（Unification）

合一是符号计算中的一种基本运算，指寻找一个变量替换，使得两个含变量的项在替换后变得完全相同，这样的替换称为合一子，而最通用的那个称为最一般合一子。

概述

合一的概念由雅克·埃尔布朗（Jacques Herbrand）提出，并由约翰·艾伦·罗宾逊（John Alan Robinson）在1965年结合归结原理给出实用算法。它是许多推理系统的引擎，因为判断两个模式能否匹配、如何匹配，本质上都是合一问题。

核心原理

• 项与替换：项由变量、常量和函数符号构成，替换是把变量映射到项的映射。
• 最一般合一子：若两项可合一，则存在一个最通用的合一子，其余合一子都是它的特例。
• 出现检查：为避免变量出现在自己被替换的项中导致无限循环，需要进行出现检查。
• 合一失败：当两项的顶层结构不同或出现检查失败时合一失败，表示两者无法相等。

应用场景

合一是逻辑编程语言执行的核心，程序运行时通过合一匹配规则头部与查询目标。它也是 Hindley-Milner 类型推断的关键步骤，编译器用合一求解类型变量的约束。此外，自动定理证明、归结推理、项重写系统都离不开合一。

常见问题

问：出现检查省略会怎样？答：若省略出现检查，遇到变量与包含自身的项合一时会构造出无限项，可能导致算法不终止或产生不合理的循环结构，某些系统为了效率默认省略并接受这种风险。

问：合一和模式匹配是一回事吗？答：模式匹配通常只允许一侧含变量，是合一的特例；合一则允许双方都含变量，需要同时确定两边变量的取值，因此更通用也更复杂。