Higher-Order Rewrite Systems and Their Confluence
Higher-Order Rewrite Systems and Their Confluence
复制标题
DOI：
10.1016/s0304-3975(97)00143-6
复制
发表时间：
1998-02
期刊：
影响因子：
--
通讯作者：
Richard Mayr;T. Nipkow
中科院分区：
文献类型：
--
作者：
Richard Mayr;T. Nipkow
我们研究了高阶重写系统（HRSs），它将项重写扩展到λ-项。HRS可以描述具有约束变量的项上的计算。我们发现，重写与HRSs是密切相关的无向方程推理。我们定义模式重写系统（PRS）作为一个特殊的情况下，HRSs和延伸的三个汇合结果从长期重写PRS：临界对引理Knuth和Benzen，汇合重写模方程La Huet，和汇合的正交PRS。
We study higher-order rewrite systems (HRSs) which extend term rewriting to λ-terms. HRSs can describe computations over terms with bound variables. We show that rewriting with HRSs is closely related to undirected equational reasoning. We define pattern rewrite systems (PRSs) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, confluence of rewriting modulo equations à la Huet, and confluence of orthogonal PRSs.