一阶统一

统一不是给每个变量随便猜一个值，而是在保留尽可能多自由度的前提下让两棵项树结构一致。根函数符号必须相同，随后问题递归下降到对应子树；变量则像洞，可以被一棵不含自身的项填入。MGU 只记录被方程强迫的等式，任何更具体解都由继续实例化它得到。occurs check 是有限项世界的边界：允许 $x=f(x)$ 会要求一棵包含自身作为真子树的无限结构。

方程 $f(x,a)\doteq f(b,y)$ 分解为 $x\doteq b$ 与 $a\doteq y$，得到 MGU $\{x\mapsto b,y\mapsto a\}$。方程 $f(x,x)\doteq f(a,b)$ 在 $a\ne b$ 时失败，因为同一变量被迫同时等于两个不同常量。

$x\doteq f(x)$ 的 occurs check 失败；若省略检查，某些实现会得到有环的 rational tree，但那已不是标准有限一阶项的统一。带绑定器的语法才必须采用无捕获替换理路无捕获替换Capture-avoiding substitution用作用域感知的递归代入替换自由变量，同时保持代入项的自由变量不被捕获。，不能直接套用这里的结构替换。带交换律、结合律或高阶变量的统一也不再是这里的简单问题，复杂度与可判定性会显著改变。

一阶统一是Hindley–Milner 类型推断理路Hindley–Milner 类型推断Hindley–Milner type inference · HM type system为带 let 的秩一参数多态 λ 演算提供主类型性质与可判定类型推断的系统。的约束求解核心：类型构造器扮演函数符号，类型变量扮演一阶变量。Algorithm W理路Algorithm WAlgorithm W完整传播HM替换、区分环境共享与let泛化，并通过嵌套推断账本和MGU解集不变量构造主类型。在应用处统一函数类型与实参类型，并把得到的替换传播到环境。

逻辑编程、项重写、定理证明和模式匹配也依赖统一；算法正确性理路算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。需要同时证明返回替换确为统一子、最一般，并在不可统一时可靠失败。

W中的完整统一器不变量理路Algorithm WAlgorithm W完整传播HM替换、区分环境共享与let泛化，并通过嵌套推断账本和MGU解集不变量构造主类型。把“最一般”展开为原方程全部解与残余解的因子分解等式，并证明变量消去、构造器冲突与occurs-check的两向正确性；变量个数与类型树大小的字典序解释替换膨胀时为何仍终止。