algorithm - 高阶统一

Question

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

如果 Huet 的算法仍然被认为是最先进的，那么有没有人有任何指向它的解释的链接，这些解释是为了让程序员而不是数学家理解而编写的？

或者甚至是它起作用而通常的一阶算法不起作用的任何示例？

Answer 1

最先进的技术——是的，据我所知，所有算法都或多或少地采用与 Huet 相同的形式(我遵循逻辑编程理论，尽管我的专业知识是切线的)提供你需要完全高阶匹配:诸如高阶匹配(一项闭合的合一)和 Dale Miller 的模式演算等子问题是可判定的。

请注意，Huet 的算法在以下意义上是最好的 — 它类似于半决策算法，因为它会找到统一器(如果存在)，但如果不存在则不能保证终止。因为我们知道高阶统一(实际上是二阶统一)是不可判定的，所以没有比这更好的了。

说明:Conal Elliott 博士论文的前四章，Extensions and Applications of Higher-Order Unification应该符合要求。该部分将近 80 页，包含一些密集的类型理论，但它的动机很好，是我见过的最具可读性的说明。

示例:Huet 的算法将为该示例提供商品:[X(o), Y(succ(0))]；哪一个必然会困扰一阶统一算法。