Canonical Forms and Unification
Canonical Forms and Unification
复制标题
规范形式和统一
DOI：
10.1007/3-540-10009-1_25
复制
发表时间：
1980
期刊：
影响因子：
--
通讯作者：
J. Hullot
中科院分区：
文献类型：
--
作者：
J. Hullot
Fay在[2，3]中描述了方程理论T的完全T-统一，该理论具有Knuth和Benzen [12]定义的完备约化集。该算法基本上依赖于使用Lankford定义的缩小过程[13]。本文首先研究了缩窄化与统一化之间的关系，并给出了一个新的Fay算法。然后，我们展示了如何消除许多冗余在这个算法中，并给出了一个充分条件终止的算法。在最后一部分中，我们展示了如何将以前的结果推广到各种类型的正则项重写系统。
Fay has described in [2,3] a complete T-unification for equational theories T which possess a complete set of reductions as defined by Knuth & Bendix [12]. This algorithm relies essentially on using the narrowing process defined by Lankford [13]. In this paper, we first study the relations between narrowing and unification and we give a new version of Fay's algorithm. We then show how to eliminate many redundancies in this algorithm and give a sufficient condition for the termination of the algorithm. In a last part, we show how to extend the previous results to various kinds of canonical term rewriting systems.