Unification算法主要分为一阶（first order）和高阶（higher order）。 一阶的算法主要处理变量类型，例如，我们可以推导某个函数的参数的类型。而函数符号本身是不可变量化的，是常量，在重写逻辑里面也称为项代数（term algebra），也称为语法Unification；在SMT模型求解器里面称为未解释的函数符号（EUF, equality with uninterpreted function），是非常重要的一类等式模型。 如果加上等式理论，称为 E-unification，也称为语义Unification，因为用到等式推导来确定两个项是否相等（或函数）。一阶Unification也比较简单，也是一个decidable的算法。

Higher order对应的是带类型的lambda演算，因为函数本身也是一个变量，这就引入了自由变量与受限变量，scoping以及α、β、η等规约规则，这些概念的引入一方面大大增加了Unification的复杂性，但同时也能刻画更复杂的系统，现在的推理证明系统（λProlog和Twelf）就是建立在高阶Unification的基础上。一般说来，这算法是undecidable。但在实践中用得很好，也可以采用某些限制（例如，规定两个项中必须有一个是closed的），得到一个受限的decidable算法。

关于算法的一般说明就到这里，回到Unification算法，其难点主要在于两点，1是多态，polymorphism； 2是递归， recursion。对于一阶unification，如果同时引入这两点，就成为一个undecidable算法，也成为semi-unification，也对应上文提到的Microft-Milner类型系统。计算机科学家一开始没有意识到这一点，因为毕竟都在一阶系统里面，从直观上看也很想象存在一个undecidable算法。 具体一个例子可以在Andrew W. Appel   的编译器“虎书”《现代编译原理》可以找到

let function blowup<e> (i:int, x:e) :e =

    if i = 0 then x

    else blowup<list<e>>(i-1, list<e> {head = x, tail =nil}).head  

in blowup<int> (N,0)

这里的e类型变量，一开始是int，然后是list<int>, list< list<int>>等类型递归展开。因为是静态无法确定N的大小，所以我们无法确定应该展开多少次。

对于这个问题，一般的做法是不允许同时有多态和递归，这样就避免这个问题，但对于一般的类型系统，如果确实存在类似的类型，算法本身就不会终止，从而得到了一个semi-unification算法。（semi-unification算法的本身定义是包括等式和不等式的unification算法，但也正好等价于MM类型系统。）