高阶一致性算法

Question

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

如果Huet算法仍被认为是最先进的，有没有任何可以让程序员理解的解释它的链接？

或者哪些例子可以说明在哪些情况下它可以工作而通常的一阶算法不行？

- rwallace

Answer 1

技术前沿 -- 据我所知，所有算法在更高阶的匹配方面都与Huet的形式基本相同（我遵循逻辑编程理论，尽管我的专业是相关的）。如果您需要完全的高阶匹配：像高阶匹配（其中一个术语是封闭的）和Dale Miller的模式计算这样的子问题是可判定的。

请注意，从以下意义上说，Huet的算法是最好的 —— 它就像半决策算法一样，当存在统一器时，它将找到它们，但如果不存在，则不能保证终止。由于我们知道更高阶的一致性（确实，第二阶一致性）是不可判定的，因此你不能再做得更好了。

解释：Conal Elliott的博士论文中的前四章节《Higher-Order Unification的扩展和应用》应该满足您的需求。那一部分有近80页，涉及一些密集的类型理论，但其动机充分，并且是我见过的最易读的概述。

示例：对于这个例子 [X(o), Y(succ(0))]，Huet的算法将得到正确的结果，而这必然会困扰一种一阶一致性算法。

- Charles Stewart

---

这是一个罕见的情况，一个真正好的（无法通过谷歌搜索或难以搜索到）问题被提出，并且得到了难以获得的高质量答案。 - Larry Watanabe

给你们两个点赞——哈哈，这可能就是为什么你们的统计数据只有300-600而不是31,200之类的数字。你可能只回答那些很少有人能回答的问题。 - Larry Watanabe

你引用的确切的Conal Elliott提供了另一个答案 :-D。 - Blaisorblade

嗨，查尔斯，你熟悉“洞”和高阶一致性吗？请看我的评论在Conal的回答中。 - user502187

Answer 2

高阶一致性范例（实际上是二阶匹配）如下：f 3 == 3 + 3，其中==模拟了α、β和η变换（但不赋予“+”任何含义）。共有四个解：

\ x -> x + x
\ x -> x + 3
\ x -> 3 + x
\ x -> 3 + 3

相比之下，一阶单一化/匹配将不会产生解决方案。

HOU在与HOAS（高阶抽象语法）一起使用时非常方便，可以对具有变量绑定的语言进行编码，同时避免变量捕获等复杂性。

我对该主题的第一次接触是通过Gerard Huet和Bernard Lang的论文“Proving and Applying Program Transformations Expressed with Second Order Patterns”。 据我回忆，这篇论文是“为程序员编写的”。 一旦您理解了二阶匹配，HOU就没有太多困难了。 Huet的一个关键结果是灵活/灵活的情况（变量作为项头，并且唯一不出现在匹配中的情况）总是可解的。

- Conal

---

我不确定这些算法是否适用于“洞”。假设我有T == \f\x. (f x) = x + x。那么（T ），即具有f“洞”的原始T的形式为\x。（ x）= x + x。但由于捕获规则，现在还有一个副约束条件，即x不应出现在_中，因此唯一的解决方案是_ = \y.y+y而不是\y.y+x，\y.x+y，\y.x+x。还没有找到一篇论文以这种方式展示“洞”。 - user502187

Answer 3

我建议将自动推理手册第2卷中的一章添加到阅读列表中。这一章对初学者来说可能更易于理解，并以λΠ演算结束，正好与Conal Elliott的论文相呼应。

这里可以找到预印本：

Higher-Order Unification and Matching
Gilles Dowek, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps

Conal Elliott的论文更加正式，集中在一个变体上，并且最后引入了λΠΣ演算，除了积类型之外，还具有和类型。

再见

- user502187

Answer 4

还有Tobias Nipkow的1993年论文“高阶模式的功能统一”（仅11页，其中4页是参考文献和代码附录）。摘要如下：

本文介绍了针对所谓的高阶模式（$\lambda$-terms子类）的完整统一算法开发。起点是通过转换来表述统一，结果是一个可以直接执行的函数程序。最后在发展阶段中，将结果适应于de Bruijn符号化的$\lambda$-terms。这些算法适用于简单类型和非类型术语。

- Nathan

---

自从我写了这篇文章后，我也发现了 https://dl.acm.org/citation.cfm?id=1637839 的清晰度价值（Moore, Automatically Computing Functional Instantiations, ACL2 '09）。 - Nathan