高阶统一

最先进的——是的,据我所知,所有的算法或多或少都与Huet的形状相同(我遵循逻辑编程理论,尽管我的专业知识是无关紧要的)。 假如 你需要完全的高阶匹配:诸如高阶匹配(一个术语闭合时的统一)和戴尔·米勒的模式演算等子问题是可以决定的。

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

说明:康纳·埃利奥特博士论文的前四章, Extensions and Applications of Higher-Order Unification 应该是合适的。这一部分大约有80页,有一些密集的类型理论,但它的动机很好,是我见过的最可读的描述。

示例:Huet的算法将为本例提供商品:【x(o),y(suc(0))】;这必然会困扰一阶统一算法。

高阶统一(实际上是二阶匹配)的一个例子是: f 3 == 3 + 3 在哪里 == 是模alpha、beta和eta转换(但不给“+”赋予任何含义)。有四种解决方案:

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

相比之下,一阶统一/匹配不会给出任何解决方案。

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

我第一次接触这个主题是杰拉德·休特和伯纳德·朗的论文“证明和应用用二阶模式表示的程序转换”。我记得,这篇论文是“为了让程序员理解而写的”。一旦你了解了二阶匹配,侯就不远了。Huet的一个关键结果是,灵活/灵活的情况(变量作为项的头,唯一不出现在匹配中的情况)总是可以解决的。

我会在阅读列表中增加第二卷的一章 自动推理手册。本章可能是 对初学者更容易接近,以微积分结束,其中 Conal Elliott论文开始。

这里有一份预印本:

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

Conal Elliott论文更正式,更关注一种变体, 最后还介绍了一种微积分,它也有求和类型。 除了产品类型。

拜伊

还有托比亚斯尼普科夫1993年的论文。 Functional Unification of Higher-Order Patterns (只有11页,其中4页是书目和代码附录)。摘要:

所谓统一算法的完整发展 高阶模式 ,它是$\lambda$术语的子类。其出发点是通过变换形成统一的公式,其结果是一个直接可执行的功能程序。在最后一个开发步骤中,结果将根据de Bruijn的符号中的\lambda$术语进行调整。这些算法既适用于简单类型的术语,也适用于非类型的术语。