Higher-order critical pairs
Higher-order critical pairs
复制标题
高阶临界对
DOI：
10.1109/lics.1991.151658
复制
发表时间：
1991
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
T. Nipkow
引入了一个类似于一阶术语的统一属性的lambda -terms的子类，称为模式。高阶重写系统被定义为在左侧是模式的lambda –term上重写系统：这可以确保重写关系易于计算。临界对的概念被推广到高阶重写系统，并证明了临界对引理的类似物。模式的受限性质有助于获得这些结果。关键对引理应用于许多lambda-calculi和一些由高阶重写系统形式化的一阶逻辑。<< etx >>
A subclass of lambda -terms, called patterns, which have unification properties resembling those of first-order terms, is introduced. Higher-order rewrite systems are defined to be rewrite systems over lambda -terms whose left-hand sides are patterns: this guarantees that the rewrite relation is easily computable. The notion of critical pair is generalized to higher-order rewrite systems, and the analog of the critical pair lemma is proved. The restricted nature of patterns is instrumental in obtaining these results. The critical pair lemma is applied to a number of lambda -calculi and some first-order logic formalized by higher-order rewrite systems.<<ETX>>