形式陈述

给一阶项方程组 $s_i=t_i$，统一问题要求替换 $\sigma$ 使 $\sigma (s_i)=\sigma (t_i)$ 对所有 $i$ 成立。若存在统一子，标准算法通过删除相等式、分解同头函数、变量消去和 occurs check 求得最一般统一子 MGU；任一其他统一子都可写为 MGU 后再复合某个替换。 不含递归类型时，方程 $X=f(X)$ 必须因 occurs check 失败。

直觉

统一不是猜一个具体类型，而是保留所有可行解共有的最一般结构，把剩余自由度留给后续实例化。

例子与边界

方程 $f(X,a)=f(b,Y)$ 的 MGU 为 $[X\mapsto b,Y\mapsto a]$。省略 occurs check 会错误接受无限项；带结合、交换等理论的统一是不同且通常更难的问题。

推论与应用

它是 Hindley–Milner 类型推断、逻辑编程、项重写和自动定理证明的核心求解器。

参考资料

• Benjamin C. Pierce, Types and Programming Languages (2002), unification and type reconstruction.
• Philip Wadler et al., Programming Language Foundations in Agda (2026), substitution and typing infrastructure.