我正在开发一个高阶定理证明器，其中合一似乎是最困难的子问题。

如果Huet的算法仍然被认为是最好的，那么是否有人有关于它的解释链接，这些解释是为程序员而不是数学家编写的？

或者甚至有任何例子说明它在哪里有效，而通常的一阶算法无效？

回答：

目前来说仍然是最先进的——是的，据我所知，所有算法或多或少都与Huet的算法具有相同的形式（我研究逻辑程序设计的理论，尽管我的专业知识是辅助性的），前提是你需要完整的高阶匹配：诸如高阶匹配（其中一个项是封闭的）之类的子问题，以及Dale Miller的模式演算，是可判定的。

请注意，Huet的算法在以下意义上是最好的——它就像一个半决策算法，因为它会找到合一者（如果它们存在），但如果它们不存在，则不能保证终止。由于我们知道高阶合一（实际上，二阶合一）是不可判定的，所以你不可能做得更好了。

解释：Conal Elliott的博士论文的前四章，高阶合一的扩展与应用应该符合要求。那部分几乎有80页，有一些密集的类型理论，但它有很好的动机，并且是我见过的最易读的解释。

例子：Huet的算法会为这个例子提供答案：[X(o), Y(succ(0))]；这必然会让一阶合一算法感到困惑。