高阶统一

Question

我正在研究一个高阶定理证明器,其中统一似乎是最困难的子问题.

如果Huet的算法仍然被认为是最先进的,那么是否有任何人有任何与其解释的链接,这些解释是由程序员而不是数学家所理解的？

或者甚至是它的工作原理和通常的一阶算法的例子都没有？

Answer 1

最先进的 - 是的,据我所知,所有的算法或多或少与Huet的形状相同(我遵循逻辑编程理论,虽然我的专业知识是切向的),只要你需要完全高阶匹配:子问题如更高 - 顺序匹配(一个术语被关闭的统一)和Dale Miller的模式演算是可判定的.

请注意,Huet的算法在以下意义上是最好的 - 它就像一个半决策算法,因为它会在它们存在的情况下找到它们,但如果它们不存在则不能保证终止.既然我们知道高阶统一(实际上是二阶统一)是不可判定的,那么你就不能做得更好.

解释:Conal Elliott博士论文的前四章,高阶统一的扩展和应用应符合该法案.这部分重约80页,有一些密集类型的理论,但它很有动力,是我见过的最易读的帐户.

示例:Huet的算法将为此示例提供货物:[X(o),Y(succ(0))]; 哪一种必然会困扰一阶统一算法.

Answer 2

高阶统一(实际上是二阶匹配)的一个例子是:f 3 == 3 + 3,其中==是模α,β和η-转换(但没有赋予"+"任何含义).有四种解决方案:

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

相反,一阶统一/匹配不会给出解决方案.

当与HOAS(高阶抽象语法)一起使用时,HOU非常方便,可以使用变量绑定对语言进行编码,同时避免变量捕获等的复杂性.

我第一次接触到这个主题的是Gerard Huet和Bernard Lang撰写的"证明和应用二阶模式表达的程序转换"一文.我记得,这篇论文"是为了让程序员理解".一旦你理解了二阶匹配,你就不会再进一步​​了.Huet的一个关键结果是灵活/灵活的情况(作为一个术语的头部的变量,以及唯一没有出现在匹配中的情况)总是可以解决的.

Answer 3

我会在阅读清单中添加"自动推理手册"第2卷的一章.本章可能更容易为初学者所用,并以ConΠElliott论文开始的λΠ-calculus结束.

这里有预印本:

高阶统一与匹配
Gilles Dowek,2001
http://www.lsv.fr/~dowek/Publi/unification.ps

Conal Elliott论文在一个变体上更为正式和集中,并且最后还引入了一个λΠΣ演算,除了产品类型之外还有和型.

再见

Answer 4

还有Tobias Nipkow 1993年的论文" 高阶模式的功能统一"(仅11页,其中4篇是参考书目和代码附录).摘要:

完整开发了所谓的高阶模式的统一算法,$\lambda $ -terms的子类.起点是通过变换统一的表述,结果是可直接执行的功能程序.在最后的开发步骤中,结果适用于de Bruijn符号中的$\lambda $ -terms.算法适用于简单类型和非类型化术语.