高阶统一
我正在研究一个更高阶的定理certificate，其中统一似乎是最困难的子问题。
如果Huet的algorithm仍然被认为是最先进的，那么是否有任何人有任何解释的链接，这些链接是由程序员而不是math家来理解的？
或甚至任何它在哪里工作的例子和通常的一阶algorithm都没有？
技术发展水平 – 是的，据我所知，所有的algorithm或多或less与Huet（我遵循逻辑编程理论，尽pipe我的专业知识是切向的）形状相同， 只要您需要完整的高阶匹配：子问题（匹配一个词的统一）和Dale Miller的模式演算是可以确定的。
请注意，Huetalgorithm在以下意义上是最好的 – 它就像是一个半决策algorithm，因为如果它们存在，它将会find统一者，但是如果它们不存在则不能保证终止。 既然我们知道高阶统一（事实上是二阶统一）是不可判定的，你不可能做得比这更好。
解释：Conal Elliott博士论文的前四章， 高级统一的扩展和应用应该适合这个法案。 那部分重达近80页，有一些密集型的理论，但是它的动机很好，是我见过的最可读的账户。
例子：Huet的algorithm会为这个例子提供商品：[X（o），Y（succ（0））]; 这必然会困扰一阶统一algorithm。
高阶统一（真正的二阶匹配）的一个例子是： f 3 == 3 + 3 ，其中==是模阿尔法，贝塔和eta转换（但没有分配任何意义的“+”）。 有四个解决scheme：
\ x -> x + x \ x -> x + 3 \ x -> 3 + x \ x -> 3 + 3
相比之下，一阶统一/匹配就没有办法解决。
与HOAS（高阶抽象语法）一起使用时，HOU非常方便，可以对variables绑定的语言进行编码，同时避免了variables捕获等的复杂性。
我第一次接触这个话题的是Gerard Huet和Bernard Lang所写的论文“certificate和应用二阶模式expression的程序转换”。 我记得，这篇论文是“写给程序员理解的”。 一旦你理解了二阶匹配，HOU就不会有太多的事情要去了。 Huet的一个关键结果是，灵活/灵活的情况（variables作为一个术语的头，而唯一的情况不会出现在匹配中）总是可以解决的。
我将在“自动推理手册”第2卷的章节中增加一章。 本章对初学者来说可能更容易理解，并且以Conal Elliott论文开始的λΠ演算结束。
预印本在这里find：
高阶统一和匹配
Gilles Dowek，2001
http://www.lsv.fr/~dowek/Publi/unification.ps
Conal Elliott论文在一个变体中更为正式和集中，最后还引入了一个λΠΣ演算，除了产品types之外，还有和型。
再见
还有Tobias Nipkow 1993年的论文“ 高阶模式function统一” （只有11页，其中4篇是参考书目和代码附录）。 摘要：
给出了所谓的更高阶模式 （$ \ lambda $ -terms的子类）的统一algorithm的完整开发。 起点是一个通过转化统一的表述，结果是一个直接可执行的function程序。 在最后的开发步骤中，结果以de Bruijn的符号来适应$ \ lambda $ -terms。 这些algorithm适用于简单types和无types的术语。
