我正在研究一个高阶定理证明器，其中统一似乎是最困难的子问题。
如果 Huet 的算法仍然被认为是最先进的，那么有没有人有任何链接到它的解释，这些解释是为了让程序员而不是数学家理解的？
或者甚至是它在哪里工作而通常的一阶算法不工作的任何例子？
问问题
5162 次
4 回答
55
最先进的技术——是的，据我所知，所有算法或多或少都与 Huet 的算法相同（我遵循逻辑编程理论，尽管我的专业知识是切线的），前提是您需要完整的高阶匹配：诸如更高阶的子问题阶匹配（一个术语闭合的统一）和戴尔米勒的模式演算是可判定的。
请注意，Huet 的算法在以下意义上是最好的——它就像一个半决策算法，如果它们存在，它将找到统一符，但如果它们不存在，则不能保证终止。因为我们知道高阶统一（实际上是二阶统一）是不可判定的，所以你不能做得比这更好。
说明：Conal Elliott 博士论文的前四章，高阶统一的扩展和应用应该符合要求。这部分有将近 80 页，包含一些密集的类型理论，但它的动机很好，并且是我见过的最易读的帐户。
例子：Huet 的算法会拿出这个例子的货：[X(o), Y(succ(0))]; 这必然会使一阶统一算法感到困惑。
于 2009-12-23T22:44:32.190 回答
27
高阶统一（实际上是二阶匹配）的一个示例是：f 3 == 3 + 3，其中==是模 alpha、beta 和 eta 转换（但不为“+”分配任何含义）。有四种解决方案：
\ x -> x + x
\ x -> x + 3
\ x -> 3 + x
\ x -> 3 + 3
相反，一阶统一/匹配不会给出解决方案。
HOU 与 HOAS（高阶抽象语法）一起使用时非常方便，可以对具有变量绑定的语言进行编码，同时避免变量捕获等复杂性。
我第一次接触这个主题是 Gerard Huet 和 Bernard Lang 的论文“证明和应用用二阶模式表达的程序转换”。我记得，这篇论文是“写给程序员理解的”。一旦你了解了二阶匹配，HOU 就不会再走太远了。Huet 的一个关键结果是灵活/灵活的情况（变量作为术语的头部，唯一没有出现在匹配中的情况）总是可以解决的。
于 2010-03-23T23:19:44.910 回答
7
我会在阅读清单中添加自动推理手册第 2 卷中的一章。本章对初学者来说可能更容易理解，并以 Conal Elliott 论文开始的 λΠ-演算结束。
在这里可以找到预印本：
高阶统一和匹配
Gilles Dowek，2001
http://www.lsv.fr/~dowek/Publi/unification.ps
Conal Elliott 论文更正式，更关注一个变体，最后还引入了 λΠΣ-演算，除了乘积类型外，它还具有和类型。
再见
于 2015-02-05T08:54:51.850 回答
5
还有Tobias Nipkow 1993 年的论文Functional Unification of Higher-Order Patterns（只有11 页，其中4 页是参考书目和代码附录）。摘要：
对所谓的高阶模式（$\lambda$-terms 的子类）的统一算法的完整开发进行了介绍。出发点是通过变换统一的公式，结果是直接可执行的功能程序。在最后的开发步骤中，结果将适应 de Bruijn 符号中的 $\lambda$-terms。该算法适用于简单类型和未类型化的术语。
于 2016-06-07T20:00:04.557 回答