我正在研究一个高阶定理证明者,其中的统一似乎是最困难的子问题。
如果Huet的算法仍被认为是最先进的,那么是否有人对它的解释有任何链接,这些解释是程序员而不是数学家可以理解的?
或什至有任何例子说明它在哪里工作,而通常的一阶算法不起作用?
最先进的技术—是的,据我所知,所有算法或多或少都与Huet的形状相同(我遵循逻辑编程理论,尽管我的专业知识是切线的), 前提是 您需要完全的高阶匹配:例如较高的子问题阶匹配(一个项闭合的统一)和戴尔·米勒的模式演算是可以确定的。
请注意,Huet的算法在以下意义上是最好的- 就像半决策算法,在这种情况下,它将找到联合者(如果存在),但不能保证终止。由于我们知道高阶统一(实际上是二阶统一)是无法确定的,因此您不能做得更好。
说明:Conal Elliott博士论文的前四章,高阶统一的扩展和应用都适合。该部分重约80页,带有一些密集型理论,但动机很好,是我所见过的最易读的文章。
示例:Huet算法将为该示例提供商品:[X(o),Y(succ(0))]; 哪一个必将使一阶统一算法感到困惑。